1.1 --- a/src/HOL/IMP/HoareT.thy Wed May 29 23:11:21 2013 +0200
1.2 +++ b/src/HOL/IMP/HoareT.thy Thu May 30 13:59:20 2013 +1000
1.3 @@ -26,8 +26,8 @@
1.4 If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
1.5 \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
1.6 While:
1.7 - "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
1.8 - \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
1.9 + "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)} \<rbrakk>
1.10 + \<Longrightarrow> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}" |
1.11 conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow>
1.12 \<turnstile>\<^sub>t {P'}c{Q'}"
1.13
1.14 @@ -47,11 +47,16 @@
1.15 by (simp add: strengthen_pre[OF _ Assign])
1.16
1.17 lemma While':
1.18 -assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}"
1.19 +assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> T n s} c {\<lambda>s. P s \<and> (\<exists>n'. T n' s \<and> n' < n)}"
1.20 and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
1.21 -shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}"
1.22 +shows "\<turnstile>\<^sub>t {\<lambda>s. P s \<and> (\<exists>n. T n s)} WHILE b DO c {Q}"
1.23 by(blast intro: assms(1) weaken_post[OF While assms(2)])
1.24
1.25 +lemma While_fun:
1.26 + "\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk>
1.27 + \<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"
1.28 + by (rule While [where T="\<lambda>n s. f s = n", simplified])
1.29 +
1.30 text{* Our standard example: *}
1.31
1.32 abbreviation "w n ==
1.33 @@ -63,14 +68,13 @@
1.34 prefer 2
1.35 apply(rule While'
1.36 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
1.37 - and f = "\<lambda>s. nat (n - s ''y'')"])
1.38 + and T = "\<lambda>n' s. n' = nat (n - s ''y'')"])
1.39 apply(rule Seq)
1.40 prefer 2
1.41 apply(rule Assign)
1.42 apply(rule Assign')
1.43 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
1.44 apply clarsimp
1.45 -apply fastforce
1.46 apply(rule Seq)
1.47 prefer 2
1.48 apply(rule Assign)
1.49 @@ -83,16 +87,16 @@
1.50
1.51 theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}"
1.52 proof(unfold hoare_tvalid_def, induct rule: hoaret.induct)
1.53 - case (While P b f c)
1.54 - show ?case
1.55 - proof
1.56 - fix s
1.57 - show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)"
1.58 - proof(induction "f s" arbitrary: s rule: less_induct)
1.59 + case (While P b T c)
1.60 + {
1.61 + fix s n
1.62 + have "\<lbrakk> P s; T n s \<rbrakk> \<Longrightarrow> \<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t"
1.63 + proof(induction "n" arbitrary: s rule: less_induct)
1.64 case (less n)
1.65 thus ?case by (metis While(2) WhileFalse WhileTrue)
1.66 qed
1.67 - qed
1.68 + }
1.69 + thus ?case by auto
1.70 next
1.71 case If thus ?case by auto blast
1.72 qed fastforce+
1.73 @@ -138,24 +142,10 @@
1.74
1.75 lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'"
1.76 proof(induction arbitrary: n' rule:Its.induct)
1.77 -(* new release:
1.78 case Its_0 thus ?case by(metis Its.cases)
1.79 next
1.80 case Its_Suc thus ?case by(metis Its.cases big_step_determ)
1.81 qed
1.82 -*)
1.83 - case Its_0
1.84 - from this(1) Its.cases[OF this(2)] show ?case by metis
1.85 -next
1.86 - case (Its_Suc b s c s' n n')
1.87 - note C = this
1.88 - from this(5) show ?case
1.89 - proof cases
1.90 - case Its_0 with Its_Suc(1) show ?thesis by blast
1.91 - next
1.92 - case Its_Suc with C show ?thesis by(metis big_step_determ)
1.93 - qed
1.94 -qed
1.95
1.96 text{* For all terminating loops, @{const Its} yields a result: *}
1.97
1.98 @@ -166,18 +156,6 @@
1.99 case WhileTrue thus ?case by (metis Its_Suc)
1.100 qed
1.101
1.102 -text{* Now the relation is turned into a function with the help of
1.103 -the description operator @{text THE}: *}
1.104 -
1.105 -definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where
1.106 -"its b c s = (THE n. Its b c s n)"
1.107 -
1.108 -text{* The key property: every loop iteration increases @{const its} by 1. *}
1.109 -
1.110 -lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk>
1.111 - \<Longrightarrow> its b c s = Suc(its b c s')"
1.112 -by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality)
1.113 -
1.114 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
1.115 proof (induction c arbitrary: Q)
1.116 case SKIP show ?case by simp (blast intro:hoaret.Skip)
1.117 @@ -190,18 +168,35 @@
1.118 next
1.119 case (While b c)
1.120 let ?w = "WHILE b DO c"
1.121 + let ?T = "\<lambda>n s. Its b c s n"
1.122 + have "\<forall>s. wp\<^sub>t (WHILE b DO c) Q s \<longrightarrow> wp\<^sub>t (WHILE b DO c) Q s \<and> (\<exists>n. Its b c s n)"
1.123 + unfolding wpt_def by (metis WHILE_Its)
1.124 + moreover
1.125 { fix n
1.126 - have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow>
1.127 - wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s"
1.128 - unfolding wpt_def by (metis WhileE its_Suc lessI)
1.129 + { fix s t
1.130 + assume "bval b s" "?T n s" "(?w, s) \<Rightarrow> t" "Q t"
1.131 + from `bval b s` `(?w, s) \<Rightarrow> t` obtain s' where
1.132 + "(c,s) \<Rightarrow> s'" "(?w,s') \<Rightarrow> t" by auto
1.133 + from `(?w, s') \<Rightarrow> t` obtain n'' where "?T n'' s'" by (blast dest: WHILE_Its)
1.134 + with `bval b s` `(c, s) \<Rightarrow> s'`
1.135 + have "?T (Suc n'') s" by (rule Its_Suc)
1.136 + with `?T n s` have "n = Suc n''" by (rule Its_fun)
1.137 + with `(c,s) \<Rightarrow> s'` `(?w,s') \<Rightarrow> t` `Q t` `?T n'' s'`
1.138 + have "wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
1.139 + by (auto simp: wpt_def)
1.140 + }
1.141 + hence "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> ?T n s \<longrightarrow>
1.142 + wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> (\<exists>n'. ?T n' s' \<and> n' < n)) s"
1.143 + unfolding wpt_def by auto
1.144 + (* by (metis WhileE Its_Suc Its_fun WHILE_Its lessI) *)
1.145 note strengthen_pre[OF this While]
1.146 } note hoaret.While[OF this]
1.147 moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def)
1.148 - ultimately show ?case by(rule weaken_post)
1.149 + ultimately show ?case by (rule conseq)
1.150 qed
1.151
1.152
1.153 -text{*\noindent In the @{term While}-case, @{const its} provides the obvious
1.154 +text{*\noindent In the @{term While}-case, @{const Its} provides the obvious
1.155 termination argument.
1.156
1.157 The actual completeness theorem follows directly, in the same manner