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