--- 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