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.6      Copyright   1995 TUM
     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