### changeset 9:663724fe2fb3

Updated the example proof
author Sigurd Meldgaard Wed, 20 May 2009 13:48:23 +0200 6fde853a56db d85656eb00e1 proofexample.thy 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```