# HG changeset patch # User kleing # Date 1369886360 -36000 # Node ID f9e68ba3f004e9eecebb46d3cef7375207446146 # Parent 0d3165844048a5d80b901a17f67cf1cd28a266fd relational version of HoareT diff -r 0d3165844048 -r f9e68ba3f004 src/HOL/IMP/HoareT.thy --- a/src/HOL/IMP/HoareT.thy Wed May 29 23:11:21 2013 +0200 +++ b/src/HOL/IMP/HoareT.thy Thu May 30 13:59:20 2013 +1000 @@ -26,8 +26,8 @@ If: "\ \\<^sub>t {\s. P s \ bval b s} c\<^isub>1 {Q}; \\<^sub>t {\s. P s \ \ bval b s} c\<^isub>2 {Q} \ \ \\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" | While: - "\ \n::nat. \\<^sub>t {\s. P s \ bval b s \ f s = n} c {\s. P s \ f s < n}\ - \ \\<^sub>t {P} WHILE b DO c {\s. P s \ \bval b s}" | + "\ \n::nat. \\<^sub>t {\s. P s \ bval b s \ T n s} c {\s. P s \ (\n'. T n' s \ n' < n)} \ + \ \\<^sub>t {\s. P s \ (\n. T n s)} WHILE b DO c {\s. P s \ \bval b s}" | conseq: "\ \s. P' s \ P s; \\<^sub>t {P}c{Q}; \s. Q s \ Q' s \ \ \\<^sub>t {P'}c{Q'}" @@ -47,11 +47,16 @@ by (simp add: strengthen_pre[OF _ Assign]) lemma While': -assumes "\n::nat. \\<^sub>t {\s. P s \ bval b s \ f s = n} c {\s. P s \ f s < n}" +assumes "\n::nat. \\<^sub>t {\s. P s \ bval b s \ T n s} c {\s. P s \ (\n'. T n' s \ n' < n)}" and "\s. P s \ \ bval b s \ Q s" -shows "\\<^sub>t {P} WHILE b DO c {Q}" +shows "\\<^sub>t {\s. P s \ (\n. T n s)} WHILE b DO c {Q}" by(blast intro: assms(1) weaken_post[OF While assms(2)]) +lemma While_fun: + "\ \n::nat. \\<^sub>t {\s. P s \ bval b s \ f s = n} c {\s. P s \ f s < n}\ + \ \\<^sub>t {P} WHILE b DO c {\s. P s \ \bval b s}" + by (rule While [where T="\n s. f s = n", simplified]) + text{* Our standard example: *} abbreviation "w n == @@ -63,14 +68,13 @@ prefer 2 apply(rule While' [where P = "\s. s ''x'' = \ {1..s ''y''} \ 0 \ s ''y'' \ s ''y'' \ n" - and f = "\s. nat (n - s ''y'')"]) + and T = "\n' s. n' = nat (n - s ''y'')"]) apply(rule Seq) prefer 2 apply(rule Assign) apply(rule Assign') apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) apply clarsimp -apply fastforce apply(rule Seq) prefer 2 apply(rule Assign) @@ -83,16 +87,16 @@ theorem hoaret_sound: "\\<^sub>t {P}c{Q} \ \\<^sub>t {P}c{Q}" proof(unfold hoare_tvalid_def, induct rule: hoaret.induct) - case (While P b f c) - show ?case - proof - fix s - show "P s \ (\t. (WHILE b DO c, s) \ t \ P t \ \ bval b t)" - proof(induction "f s" arbitrary: s rule: less_induct) + case (While P b T c) + { + fix s n + have "\ P s; T n s \ \ \t. (WHILE b DO c, s) \ t \ P t \ \ bval b t" + proof(induction "n" arbitrary: s rule: less_induct) case (less n) thus ?case by (metis While(2) WhileFalse WhileTrue) qed - qed + } + thus ?case by auto next case If thus ?case by auto blast qed fastforce+ @@ -138,24 +142,10 @@ lemma Its_fun: "Its b c s n \ Its b c s n' \ n=n'" proof(induction arbitrary: n' rule:Its.induct) -(* new release: case Its_0 thus ?case by(metis Its.cases) next case Its_Suc thus ?case by(metis Its.cases big_step_determ) qed -*) - case Its_0 - from this(1) Its.cases[OF this(2)] show ?case by metis -next - case (Its_Suc b s c s' n n') - note C = this - from this(5) show ?case - proof cases - case Its_0 with Its_Suc(1) show ?thesis by blast - next - case Its_Suc with C show ?thesis by(metis big_step_determ) - qed -qed text{* For all terminating loops, @{const Its} yields a result: *} @@ -166,18 +156,6 @@ case WhileTrue thus ?case by (metis Its_Suc) qed -text{* Now the relation is turned into a function with the help of -the description operator @{text THE}: *} - -definition its :: "bexp \ com \ state \ nat" where -"its b c s = (THE n. Its b c s n)" - -text{* The key property: every loop iteration increases @{const its} by 1. *} - -lemma its_Suc: "\ bval b s; (c, s) \ s'; (WHILE b DO c, s') \ t\ - \ its b c s = Suc(its b c s')" -by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality) - lemma wpt_is_pre: "\\<^sub>t {wp\<^sub>t c Q} c {Q}" proof (induction c arbitrary: Q) case SKIP show ?case by simp (blast intro:hoaret.Skip) @@ -190,18 +168,35 @@ next case (While b c) let ?w = "WHILE b DO c" + let ?T = "\n s. Its b c s n" + have "\s. wp\<^sub>t (WHILE b DO c) Q s \ wp\<^sub>t (WHILE b DO c) Q s \ (\n. Its b c s n)" + unfolding wpt_def by (metis WHILE_Its) + moreover { fix n - have "\s. wp\<^sub>t ?w Q s \ bval b s \ its b c s = n \ - wp\<^sub>t c (\s'. wp\<^sub>t ?w Q s' \ its b c s' < n) s" - unfolding wpt_def by (metis WhileE its_Suc lessI) + { fix s t + assume "bval b s" "?T n s" "(?w, s) \ t" "Q t" + from `bval b s` `(?w, s) \ t` obtain s' where + "(c,s) \ s'" "(?w,s') \ t" by auto + from `(?w, s') \ t` obtain n'' where "?T n'' s'" by (blast dest: WHILE_Its) + with `bval b s` `(c, s) \ s'` + have "?T (Suc n'') s" by (rule Its_Suc) + with `?T n s` have "n = Suc n''" by (rule Its_fun) + with `(c,s) \ s'` `(?w,s') \ t` `Q t` `?T n'' s'` + have "wp\<^sub>t c (\s'. wp\<^sub>t ?w Q s' \ (\n'. ?T n' s' \ n' < n)) s" + by (auto simp: wpt_def) + } + hence "\s. wp\<^sub>t ?w Q s \ bval b s \ ?T n s \ + wp\<^sub>t c (\s'. wp\<^sub>t ?w Q s' \ (\n'. ?T n' s' \ n' < n)) s" + unfolding wpt_def by auto + (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *) note strengthen_pre[OF this While] } note hoaret.While[OF this] moreover have "\s. wp\<^sub>t ?w Q s \ \ bval b s \ Q s" by (auto simp add:wpt_def) - ultimately show ?case by(rule weaken_post) + ultimately show ?case by (rule conseq) qed -text{*\noindent In the @{term While}-case, @{const its} provides the obvious +text{*\noindent In the @{term While}-case, @{const Its} provides the obvious termination argument. The actual completeness theorem follows directly, in the same manner