Mercurial > pysmcl
changeset 9:663724fe2fb3
Updated the example proof
author | Sigurd Meldgaard <stm@daimi.au.dk> |
---|---|
date | Wed, 20 May 2009 13:48:23 +0200 |
parents | 6fde853a56db |
children | d85656eb00e1 |
files | proofexample.thy |
diffstat | 1 files changed, 8 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/proofexample.thy Mon May 18 09:57:00 2009 +0200 +++ b/proofexample.thy Wed May 20 13:48:23 2009 +0200 @@ -1,31 +1,18 @@ theory proofexample imports Main begin -value "sorted [-1, 0, 0, 5::int]" - -lemma "[] \<noteq> [1::nat]" - apply (rule list.distinct) -done - -lemma assumes ab: "A \<and> B" - shows "B \<and> A" -using ab -proof - assume "B" "A" thus ?thesis .. -qed - -lemma assumes "A" shows "A" -proof - - show "A" by (rule assms) -qed +(* Some examples of how a proof-burden with its proof for a simulator could look *) lemma sorted_mono[simp]: assumes "sorted (xs::int list)" - shows "mono (\<lambda> x . xs ! x)" -proof + shows "xs \<noteq> [] \<longrightarrow> mono (\<lambda> a . xs ! a)" +proof (induct xs rule: sorted.induct) + case 1 show ?case sorry + case (2 element) show ?case sorry + case 3 show ?case sorry +qed -qed (* Simulates: xst[mid] \<ge> 0 *) definition "simulator" :: "nat \<Rightarrow> nat \<Rightarrow> bool " where "simulator result mid = (result \<le> mid)" @@ -34,14 +21,6 @@ assumes "sorted xs" "(xs ! result) = (0::int)" "(xs ! (result - 1)) < 0 \<or> (result = 0)" - shows "(simulator result index) = ((xs ! index) \<ge> 0)" -proof - have "mono (\<lambda> x . xs ! - assume "simulator result index" - have "xs ! index \<ge> 0" sorry - -qed - + shows "(simulator result index) = ((xs ! index) \<ge> 0)" sorry end - \ No newline at end of file