src/HOL/IMP/Hoare.thy
changeset 12434 ff2efde4574d
parent 12431 07ec657249e5
child 12546 0c90e581379f
     1.1 --- a/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:37:42 2001 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Sun Dec 09 15:26:13 2001 +0100
     1.3 @@ -101,10 +101,11 @@
     1.4  apply (simp (no_asm_simp))
     1.5  done
     1.6  
     1.7 -declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp]
     1.8 +lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
     1.9  
    1.10  (*Not suitable for rewriting: LOOPS!*)
    1.11 -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.12 +lemma wp_While_if: 
    1.13 +  "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
    1.14  apply (simp (no_asm))
    1.15  done
    1.16  
    1.17 @@ -132,7 +133,7 @@
    1.18  
    1.19  declare C_while [simp del]
    1.20  
    1.21 -declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!]
    1.22 +lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If 
    1.23  
    1.24  lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
    1.25  apply (induct_tac "c")