34 (* |
34 (* |
35 Soundness (and part of) relative completeness of Hoare rules |
35 Soundness (and part of) relative completeness of Hoare rules |
36 wrt denotational semantics |
36 wrt denotational semantics |
37 *) |
37 *) |
38 |
38 |
39 lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}" |
39 lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}" |
40 apply (erule hoare.conseq) |
40 by (blast intro: conseq) |
41 apply assumption |
|
42 apply fast |
|
43 done |
|
44 |
41 |
45 lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}" |
42 lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}" |
46 apply (rule hoare.conseq) |
43 by (blast intro: conseq) |
47 prefer 2 apply (assumption) |
|
48 apply fast |
|
49 apply fast |
|
50 done |
|
51 |
44 |
52 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}" |
45 lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}" |
53 apply (unfold hoare_valid_def) |
46 proof(induct rule: hoare.induct) |
54 apply (induct set: hoare) |
47 case (While P b c) |
55 apply (simp_all (no_asm_simp)) |
48 { fix s t |
56 apply fast |
49 let ?G = "Gamma b (C c)" |
57 apply fast |
50 assume "(s,t) \<in> lfp ?G" |
58 apply (rule allI, rule allI, rule impI) |
51 hence "P s \<longrightarrow> P t \<and> \<not> b t" |
59 apply (erule lfp_induct2) |
52 proof(rule lfp_induct2) |
60 apply (rule Gamma_mono) |
53 show "mono ?G" by(rule Gamma_mono) |
61 apply (unfold Gamma_def) |
54 next |
62 apply fast |
55 fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})" |
63 done |
56 thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps |
|
57 by(auto simp: hoare_valid_def Gamma_def) |
|
58 qed |
|
59 } |
|
60 thus ?case by(simp add:hoare_valid_def) |
|
61 qed (auto simp: hoare_valid_def) |
|
62 |
64 |
63 |
65 lemma wp_SKIP: "wp \<SKIP> Q = Q" |
64 lemma wp_SKIP: "wp \<SKIP> Q = Q" |
66 apply (unfold wp_def) |
65 by (simp add: wp_def) |
67 apply (simp (no_asm)) |
|
68 done |
|
69 |
66 |
70 lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))" |
67 lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))" |
71 apply (unfold wp_def) |
68 by (simp add: wp_def) |
72 apply (simp (no_asm)) |
|
73 done |
|
74 |
69 |
75 lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)" |
70 lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)" |
76 apply (unfold wp_def) |
71 by (rule ext) (auto simp: wp_def) |
77 apply (simp (no_asm)) |
|
78 apply (rule ext) |
|
79 apply fast |
|
80 done |
|
81 |
72 |
82 lemma wp_If: |
73 lemma wp_If: |
83 "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))" |
74 "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))" |
84 apply (unfold wp_def) |
75 by (rule ext) (auto simp: wp_def) |
85 apply (simp (no_asm)) |
|
86 apply (rule ext) |
|
87 apply fast |
|
88 done |
|
89 |
76 |
90 lemma wp_While_True: |
77 lemma wp_While_If: |
91 "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s" |
78 "wp (\<WHILE> b \<DO> c) Q s = |
92 apply (unfold wp_def) |
79 wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s" |
93 apply (subst C_While_If) |
80 by(simp only: wp_def C_While_If) |
94 apply (simp (no_asm_simp)) |
|
95 done |
|
96 |
|
97 lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s" |
|
98 apply (unfold wp_def) |
|
99 apply (subst C_While_If) |
|
100 apply (simp (no_asm_simp)) |
|
101 done |
|
102 |
|
103 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False |
|
104 |
81 |
105 (*Not suitable for rewriting: LOOPS!*) |
82 (*Not suitable for rewriting: LOOPS!*) |
106 lemma wp_While_if: |
83 lemma wp_While_if: |
107 "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)" |
84 "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)" |
108 by simp |
85 by(simp add:wp_While_If wp_If wp_SKIP) |
|
86 |
|
87 lemma wp_While_True: "b s ==> |
|
88 wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s" |
|
89 by(simp add: wp_While_if) |
|
90 |
|
91 lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s" |
|
92 by(simp add: wp_While_if) |
|
93 |
|
94 lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False |
109 |
95 |
110 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s = |
96 lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s = |
111 (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))" |
97 (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))" |
112 apply (simp (no_asm)) |
98 apply (simp (no_asm)) |
113 apply (rule iffI) |
99 apply (rule iffI) |
130 declare C_while [simp del] |
116 declare C_while [simp del] |
131 |
117 |
132 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If |
118 lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If |
133 |
119 |
134 lemma wp_is_pre: "|- {wp c Q} c {Q}" |
120 lemma wp_is_pre: "|- {wp c Q} c {Q}" |
135 apply (induct c arbitrary: Q) |
121 proof(induct c arbitrary: Q) |
136 apply (simp_all (no_asm)) |
122 case SKIP show ?case by auto |
137 apply fast+ |
123 next |
138 apply (blast intro: hoare_conseq1) |
124 case Assign show ?case by auto |
139 apply (rule hoare_conseq2) |
125 next |
140 apply (rule hoare.While) |
126 case Semi thus ?case by auto |
141 apply (rule hoare_conseq1) |
127 next |
142 prefer 2 apply fast |
128 case (Cond b c1 c2) |
143 apply safe |
129 let ?If = "IF b THEN c1 ELSE c2" |
144 apply simp |
130 show ?case |
145 apply simp |
131 proof(rule If) |
146 done |
132 show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}" |
|
133 proof(rule strengthen_pre[OF _ Cond(1)]) |
|
134 show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto |
|
135 qed |
|
136 show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}" |
|
137 proof(rule strengthen_pre[OF _ Cond(2)]) |
|
138 show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto |
|
139 qed |
|
140 qed |
|
141 next |
|
142 case (While b c) |
|
143 let ?w = "WHILE b DO c" |
|
144 have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}" |
|
145 proof(rule hoare.While) |
|
146 show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}" |
|
147 proof(rule strengthen_pre[OF _ While(1)]) |
|
148 show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto |
|
149 qed |
|
150 qed |
|
151 thus ?case |
|
152 proof(rule weaken_post) |
|
153 show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto |
|
154 qed |
|
155 qed |
147 |
156 |
148 lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}" |
157 lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}" |
149 apply (rule hoare_conseq1 [OF _ wp_is_pre]) |
158 proof(rule conseq) |
150 apply (unfold hoare_valid_def wp_def) |
159 show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms |
151 apply fast |
160 by (auto simp: hoare_valid_def wp_def) |
152 done |
161 show "|- {wp c Q} c {Q}" by(rule wp_is_pre) |
|
162 show "\<forall>s. Q s \<longrightarrow> Q s" by auto |
|
163 qed |
153 |
164 |
154 end |
165 end |