changeset 16:1f6cb90a3f66

More proving
author Sigurd Meldgaard <stm@daimi.au.dk>
date Wed, 20 May 2009 17:12:27 +0200
parents bf1e9000d33b
children e83209448370
files proofexample.thy
diffstat 1 files changed, 16 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/proofexample.thy	Wed May 20 14:37:24 2009 +0200
+++ b/proofexample.thy	Wed May 20 17:12:27 2009 +0200
@@ -2,25 +2,29 @@
 
 (* 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 "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
-
+lemma sorted_nth_mono:
+ "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
+by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
 (* Simulates: xst[mid] \<ge> 0 *)
 definition "simulator" :: "nat \<Rightarrow> nat \<Rightarrow> bool " where
   "simulator result mid = (result \<le> mid)"
 
+(* This was proved with the help of sledgehammer, and should be cleaned up *)
+
 lemma simulation_correct:
   assumes "sorted xs"
   "(xs ! result) = (0::int)"
   "(xs ! (result - 1)) < 0 \<or> (result = 0)"
-  shows "(simulator result index) = ((xs ! index) \<ge> 0)" sorry
+  "index < length xs"
+  shows "(simulator result index) \<Longrightarrow> ((xs ! index) \<ge> 0)"
+proof (auto simp: simulator_def)
+  from assms(1) assms(3) have "result \<le> index \<Longrightarrow> xs ! result \<le> xs ! index"
+    apply (metis assms(2) assms(4) assms(1) sorted_nth_mono)
+    done
+  then show "result \<le> index \<Longrightarrow> 0 \<le> xs ! index"
+    apply (metis assms(2))
+    done
+
+qed
 
 end