### changeset 16:1f6cb90a3f66

More proving
author Sigurd Meldgaard Wed, 20 May 2009 17:12:27 +0200 bf1e9000d33b e83209448370 proofexample.thy 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```