src/HOL/IMP/Hoare.thy
changeset 18372 2bffdf62fe7f
parent 16417 9bc16273c2d4
child 20503 503ac4c5ef91
     1.1 --- a/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:41 2005 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Thu Dec 08 20:15:50 2005 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  constdefs wp :: "com => assn => assn"
     1.5            "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
     1.6  
     1.7 -(*  
     1.8 +(*
     1.9  Soundness (and part of) relative completeness of Hoare rules
    1.10  wrt denotational semantics
    1.11  *)
    1.12 @@ -52,7 +52,7 @@
    1.13  
    1.14  lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    1.15  apply (unfold hoare_valid_def)
    1.16 -apply (erule hoare.induct)
    1.17 +apply (induct set: hoare)
    1.18       apply (simp_all (no_asm_simp))
    1.19    apply fast
    1.20   apply fast
    1.21 @@ -80,7 +80,7 @@
    1.22  apply fast
    1.23  done
    1.24  
    1.25 -lemma wp_If: 
    1.26 +lemma wp_If:
    1.27   "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
    1.28  apply (unfold wp_def)
    1.29  apply (simp (no_asm))
    1.30 @@ -88,7 +88,7 @@
    1.31  apply fast
    1.32  done
    1.33  
    1.34 -lemma wp_While_True: 
    1.35 +lemma wp_While_True:
    1.36    "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
    1.37  apply (unfold wp_def)
    1.38  apply (subst C_While_If)
    1.39 @@ -104,12 +104,11 @@
    1.40  lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
    1.41  
    1.42  (*Not suitable for rewriting: LOOPS!*)
    1.43 -lemma wp_While_if: 
    1.44 +lemma wp_While_if:
    1.45    "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    1.46 -apply (simp (no_asm))
    1.47 -done
    1.48 +  by simp
    1.49  
    1.50 -lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =  
    1.51 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
    1.52     (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
    1.53  apply (simp (no_asm))
    1.54  apply (rule iffI)
    1.55 @@ -131,18 +130,17 @@
    1.56  
    1.57  declare C_while [simp del]
    1.58  
    1.59 -lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If 
    1.60 +lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
    1.61  
    1.62 -lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
    1.63 -apply (induct_tac "c")
    1.64 +lemma wp_is_pre: "|- {wp c Q} c {Q}"
    1.65 +apply (induct c fixing: Q)
    1.66      apply (simp_all (no_asm))
    1.67      apply fast+
    1.68   apply (blast intro: hoare_conseq1)
    1.69 -apply safe
    1.70  apply (rule hoare_conseq2)
    1.71   apply (rule hoare.While)
    1.72   apply (rule hoare_conseq1)
    1.73 -  prefer 2 apply (fast)
    1.74 +  prefer 2 apply fast
    1.75    apply safe
    1.76   apply simp
    1.77  apply simp