converted proofs to Isar
authornipkow
Thu Mar 11 19:05:46 2010 +0100 (2010-03-11)
changeset 35735f139a9bb6501
parent 35711 548d3f16404b
child 35736 017dc733e078
converted proofs to Isar
src/HOL/IMP/Hoare.thy
     1.1 --- a/src/HOL/IMP/Hoare.thy	Thu Mar 11 12:22:11 2010 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Mar 11 19:05:46 2010 +0100
     1.3 @@ -36,76 +36,62 @@
     1.4  wrt denotational semantics
     1.5  *)
     1.6  
     1.7 -lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
     1.8 -apply (erule hoare.conseq)
     1.9 -apply  assumption
    1.10 -apply fast
    1.11 -done
    1.12 +lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    1.13 +by (blast intro: conseq)
    1.14  
    1.15 -lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    1.16 -apply (rule hoare.conseq)
    1.17 -prefer 2 apply    (assumption)
    1.18 -apply fast
    1.19 -apply fast
    1.20 -done
    1.21 +lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    1.22 +by (blast intro: conseq)
    1.23  
    1.24  lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    1.25 -apply (unfold hoare_valid_def)
    1.26 -apply (induct set: hoare)
    1.27 -     apply (simp_all (no_asm_simp))
    1.28 -  apply fast
    1.29 - apply fast
    1.30 -apply (rule allI, rule allI, rule impI)
    1.31 -apply (erule lfp_induct2)
    1.32 - apply (rule Gamma_mono)
    1.33 -apply (unfold Gamma_def)
    1.34 -apply fast
    1.35 -done
    1.36 +proof(induct rule: hoare.induct)
    1.37 +  case (While P b c)
    1.38 +  { fix s t
    1.39 +    let ?G = "Gamma b (C c)"
    1.40 +    assume "(s,t) \<in> lfp ?G"
    1.41 +    hence "P s \<longrightarrow> P t \<and> \<not> b t"
    1.42 +    proof(rule lfp_induct2)
    1.43 +      show "mono ?G" by(rule Gamma_mono)
    1.44 +    next
    1.45 +      fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
    1.46 +      thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
    1.47 +        by(auto simp: hoare_valid_def Gamma_def)
    1.48 +    qed
    1.49 +  }
    1.50 +  thus ?case by(simp add:hoare_valid_def)
    1.51 +qed (auto simp: hoare_valid_def)
    1.52 +
    1.53  
    1.54  lemma wp_SKIP: "wp \<SKIP> Q = Q"
    1.55 -apply (unfold wp_def)
    1.56 -apply (simp (no_asm))
    1.57 -done
    1.58 +by (simp add: wp_def)
    1.59  
    1.60  lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    1.61 -apply (unfold wp_def)
    1.62 -apply (simp (no_asm))
    1.63 -done
    1.64 +by (simp add: wp_def)
    1.65  
    1.66  lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    1.67 -apply (unfold wp_def)
    1.68 -apply (simp (no_asm))
    1.69 -apply (rule ext)
    1.70 -apply fast
    1.71 -done
    1.72 +by (rule ext) (auto simp: wp_def)
    1.73  
    1.74  lemma wp_If:
    1.75   "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    1.76 -apply (unfold wp_def)
    1.77 -apply (simp (no_asm))
    1.78 -apply (rule ext)
    1.79 -apply fast
    1.80 -done
    1.81 +by (rule ext) (auto simp: wp_def)
    1.82  
    1.83 -lemma wp_While_True:
    1.84 -  "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    1.85 -apply (unfold wp_def)
    1.86 -apply (subst C_While_If)
    1.87 -apply (simp (no_asm_simp))
    1.88 -done
    1.89 -
    1.90 -lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
    1.91 -apply (unfold wp_def)
    1.92 -apply (subst C_While_If)
    1.93 -apply (simp (no_asm_simp))
    1.94 -done
    1.95 -
    1.96 -lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    1.97 +lemma wp_While_If:
    1.98 + "wp (\<WHILE> b \<DO> c) Q s =
    1.99 +  wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
   1.100 +by(simp only: wp_def C_While_If)
   1.101  
   1.102  (*Not suitable for rewriting: LOOPS!*)
   1.103  lemma wp_While_if:
   1.104    "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
   1.105 -  by simp
   1.106 +by(simp add:wp_While_If wp_If wp_SKIP)
   1.107 +
   1.108 +lemma wp_While_True: "b s ==>
   1.109 +  wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
   1.110 +by(simp add: wp_While_if)
   1.111 +
   1.112 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
   1.113 +by(simp add: wp_While_if)
   1.114 +
   1.115 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
   1.116  
   1.117  lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
   1.118     (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
   1.119 @@ -132,23 +118,48 @@
   1.120  lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
   1.121  
   1.122  lemma wp_is_pre: "|- {wp c Q} c {Q}"
   1.123 -apply (induct c arbitrary: Q)
   1.124 -    apply (simp_all (no_asm))
   1.125 -    apply fast+
   1.126 - apply (blast intro: hoare_conseq1)
   1.127 -apply (rule hoare_conseq2)
   1.128 - apply (rule hoare.While)
   1.129 - apply (rule hoare_conseq1)
   1.130 -  prefer 2 apply fast
   1.131 -  apply safe
   1.132 - apply simp
   1.133 -apply simp
   1.134 -done
   1.135 +proof(induct c arbitrary: Q)
   1.136 +  case SKIP show ?case by auto
   1.137 +next
   1.138 +  case Assign show ?case by auto
   1.139 +next
   1.140 +  case Semi thus ?case by auto
   1.141 +next
   1.142 +  case (Cond b c1 c2)
   1.143 +  let ?If = "IF b THEN c1 ELSE c2"
   1.144 +  show ?case
   1.145 +  proof(rule If)
   1.146 +    show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
   1.147 +    proof(rule strengthen_pre[OF _ Cond(1)])
   1.148 +      show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
   1.149 +    qed
   1.150 +    show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
   1.151 +    proof(rule strengthen_pre[OF _ Cond(2)])
   1.152 +      show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
   1.153 +    qed
   1.154 +  qed
   1.155 +next
   1.156 +  case (While b c)
   1.157 +  let ?w = "WHILE b DO c"
   1.158 +  have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
   1.159 +  proof(rule hoare.While)
   1.160 +    show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
   1.161 +    proof(rule strengthen_pre[OF _ While(1)])
   1.162 +      show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
   1.163 +    qed
   1.164 +  qed
   1.165 +  thus ?case
   1.166 +  proof(rule weaken_post)
   1.167 +    show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
   1.168 +  qed
   1.169 +qed
   1.170  
   1.171 -lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
   1.172 -apply (rule hoare_conseq1 [OF _ wp_is_pre])
   1.173 -apply (unfold hoare_valid_def wp_def)
   1.174 -apply fast
   1.175 -done
   1.176 +lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
   1.177 +proof(rule conseq)
   1.178 +  show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
   1.179 +    by (auto simp: hoare_valid_def wp_def)
   1.180 +  show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
   1.181 +  show "\<forall>s. Q s \<longrightarrow> Q s" by auto
   1.182 +qed
   1.183  
   1.184  end