relational version of HoareT
authorkleing
Thu May 30 13:59:20 2013 +1000 (2013-05-30)
changeset 52227f9e68ba3f004
parent 52226 0d3165844048
child 52228 ee8e3eaad24c
relational version of HoareT
src/HOL/IMP/HoareT.thy
     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