equal
deleted
inserted
replaced
99 apply (unfold wp_def) |
99 apply (unfold wp_def) |
100 apply (subst C_While_If) |
100 apply (subst C_While_If) |
101 apply (simp (no_asm_simp)) |
101 apply (simp (no_asm_simp)) |
102 done |
102 done |
103 |
103 |
104 declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp] |
104 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False |
105 |
105 |
106 (*Not suitable for rewriting: LOOPS!*) |
106 (*Not suitable for rewriting: LOOPS!*) |
107 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)" |
107 lemma wp_While_if: |
|
108 "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)" |
108 apply (simp (no_asm)) |
109 apply (simp (no_asm)) |
109 done |
110 done |
110 |
111 |
111 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s = |
112 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s = |
112 (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))" |
113 (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))" |
130 apply fast |
131 apply fast |
131 done |
132 done |
132 |
133 |
133 declare C_while [simp del] |
134 declare C_while [simp del] |
134 |
135 |
135 declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!] |
136 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If |
136 |
137 |
137 lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}" |
138 lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}" |
138 apply (induct_tac "c") |
139 apply (induct_tac "c") |
139 apply (simp_all (no_asm)) |
140 apply (simp_all (no_asm)) |
140 apply fast+ |
141 apply fast+ |