src/HOL/IMP/Hoare.thy
 changeset 12431 07ec657249e5 parent 9241 f961c1fdff50 child 12434 ff2efde4574d
```     1.1 --- a/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:35:11 2001 +0100
1.2 +++ b/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:35:36 2001 +0100
1.3 @@ -2,34 +2,157 @@
1.4      ID:         \$Id\$
1.5      Author:     Tobias Nipkow
1.7 -
1.8 -Inductive definition of Hoare logic
1.9  *)
1.10
1.11 -Hoare = Denotation + Inductive +
1.12 +header "Inductive Definition of Hoare Logic"
1.13 +
1.14 +theory Hoare = Denotation:
1.15
1.16 -types assn = state => bool
1.17 +types assn = "state => bool"
1.18
1.19 -constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
1.20 +constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
1.21            "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
1.22
1.23  consts hoare :: "(assn * com * assn) set"
1.24 -syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
1.25 +syntax "@hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
1.26  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
1.27
1.28  inductive hoare
1.29 -intrs
1.30 -  skip "|- {P}SKIP{P}"
1.31 -  ass  "|- {%s. P(s[x::=a s])} x:==a {P}"
1.32 -  semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
1.33 -  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
1.34 -      |- {P} IF b THEN c ELSE d {Q}"
1.35 -  While "|- {%s. P s & b s} c {P} ==>
1.36 -         |- {P} WHILE b DO c {%s. P s & ~b s}"
1.37 -  conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
1.38 +intros
1.39 +  skip: "|- {P}\<SKIP>{P}"
1.40 +  ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
1.41 +  semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
1.42 +  If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
1.43 +      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
1.44 +  While: "|- {%s. P s & b s} c {P} ==>
1.45 +         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
1.46 +  conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
1.47            |- {P'}c{Q'}"
1.48
1.49 -constdefs wp :: com => assn => assn
1.50 +constdefs wp :: "com => assn => assn"
1.51            "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
1.52
1.53 +(*
1.54 +Soundness (and part of) relative completeness of Hoare rules
1.55 +wrt denotational semantics
1.56 +*)
1.57 +
1.58 +lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
1.59 +apply (erule hoare.conseq)
1.60 +apply  assumption
1.61 +apply fast
1.62 +done
1.63 +
1.64 +lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
1.65 +apply (rule hoare.conseq)
1.66 +prefer 2 apply    (assumption)
1.67 +apply fast
1.68 +apply fast
1.69 +done
1.70 +
1.71 +lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
1.72 +apply (unfold hoare_valid_def)
1.73 +apply (erule hoare.induct)
1.74 +     apply (simp_all (no_asm_simp))
1.75 +  apply fast
1.76 + apply fast
1.77 +apply (rule allI, rule allI, rule impI)
1.78 +apply (erule lfp_induct2)
1.79 + apply (rule Gamma_mono)
1.80 +apply (unfold Gamma_def)
1.81 +apply fast
1.82 +done
1.83 +
1.84 +lemma wp_SKIP: "wp \<SKIP> Q = Q"
1.85 +apply (unfold wp_def)
1.86 +apply (simp (no_asm))
1.87 +done
1.88 +
1.89 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
1.90 +apply (unfold wp_def)
1.91 +apply (simp (no_asm))
1.92 +done
1.93 +
1.94 +lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
1.95 +apply (unfold wp_def)
1.96 +apply (simp (no_asm))
1.97 +apply (rule ext)
1.98 +apply fast
1.99 +done
1.100 +
1.101 +lemma wp_If:
1.102 + "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
1.103 +apply (unfold wp_def)
1.104 +apply (simp (no_asm))
1.105 +apply (rule ext)
1.106 +apply fast
1.107 +done
1.108 +
1.109 +lemma wp_While_True:
1.110 +  "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
1.111 +apply (unfold wp_def)
1.112 +apply (subst C_While_If)
1.113 +apply (simp (no_asm_simp))
1.114 +done
1.115 +
1.116 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
1.117 +apply (unfold wp_def)
1.118 +apply (subst C_While_If)
1.119 +apply (simp (no_asm_simp))
1.120 +done
1.121 +
1.122 +declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp]
1.123 +
1.124 +(*Not suitable for rewriting: LOOPS!*)
1.125 +lemma wp_While_if: "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
1.126 +apply (simp (no_asm))
1.127 +done
1.128 +
1.129 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
1.130 +   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
1.131 +apply (simp (no_asm))
1.132 +apply (rule iffI)
1.133 + apply (rule weak_coinduct)
1.134 +  apply (erule CollectI)
1.135 + apply safe
1.136 +  apply (rotate_tac -1)
1.137 +  apply simp
1.138 + apply (rotate_tac -1)
1.139 + apply simp
1.140 +apply (simp add: wp_def Gamma_def)
1.141 +apply (intro strip)
1.142 +apply (rule mp)
1.143 + prefer 2 apply (assumption)
1.144 +apply (erule lfp_induct2)
1.145 +apply (fast intro!: monoI)
1.146 +apply (subst gfp_unfold)
1.147 + apply (fast intro!: monoI)
1.148 +apply fast
1.149 +done
1.150 +
1.151 +declare C_while [simp del]
1.152 +
1.153 +declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!]
1.154 +
1.155 +lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
1.156 +apply (induct_tac "c")
1.157 +    apply (simp_all (no_asm))
1.158 +    apply fast+
1.159 + apply (blast intro: hoare_conseq1)
1.160 +apply safe
1.161 +apply (rule hoare_conseq2)
1.162 + apply (rule hoare.While)
1.163 + apply (rule hoare_conseq1)
1.164 +  prefer 2 apply (fast)
1.165 +  apply safe
1.166 + apply (rotate_tac -1, simp)
1.167 +apply (rotate_tac -1, simp)
1.168 +done
1.169 +
1.170 +lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
1.171 +apply (rule hoare_conseq1 [OF _ wp_is_pre])
1.172 +apply (unfold hoare_valid_def wp_def)
1.173 +apply fast
1.174 +done
1.175 +
1.176  end
```