49 by auto |
49 by auto |
50 |
50 |
51 text{* Disable L WHILE equation and reason only with L WHILE constraints *} |
51 text{* Disable L WHILE equation and reason only with L WHILE constraints *} |
52 declare L.simps(5)[simp del] |
52 declare L.simps(5)[simp del] |
53 |
53 |
54 subsection "Soundness" |
54 subsection "Correctness" |
55 |
55 |
56 theorem L_sound: |
56 theorem L_correct: |
57 "(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
57 "(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
58 \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
58 \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
59 proof (induction arbitrary: X t rule: big_step_induct) |
59 proof (induction arbitrary: X t rule: big_step_induct) |
60 case Skip then show ?case by auto |
60 case Skip then show ?case by auto |
61 next |
61 next |
112 "bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" | |
112 "bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" | |
113 "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" | |
113 "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" | |
114 "bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" | |
114 "bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" | |
115 "bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)" |
115 "bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)" |
116 |
116 |
117 text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the |
117 text{* We could prove the analogous lemma to @{thm[source]L_correct}, and the |
118 proof would be very similar. However, we phrase it as a semantics |
118 proof would be very similar. However, we phrase it as a semantics |
119 preservation property: *} |
119 preservation property: *} |
120 |
120 |
121 theorem bury_sound: |
121 theorem bury_correct: |
122 "(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
122 "(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
123 \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X" |
123 \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X" |
124 proof (induction arbitrary: X t rule: big_step_induct) |
124 proof (induction arbitrary: X t rule: big_step_induct) |
125 case Skip then show ?case by auto |
125 case Skip then show ?case by auto |
126 next |
126 next |
167 where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X" |
167 where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X" |
168 by auto |
168 by auto |
169 with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto |
169 with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto |
170 qed |
170 qed |
171 |
171 |
172 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'" |
172 corollary final_bury_correct: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'" |
173 using bury_sound[of c s s' UNIV] |
173 using bury_correct[of c s s' UNIV] |
174 by (auto simp: fun_eq_iff[symmetric]) |
174 by (auto simp: fun_eq_iff[symmetric]) |
175 |
175 |
176 text{* Now the opposite direction. *} |
176 text{* Now the opposite direction. *} |
177 |
177 |
178 lemma SKIP_bury[simp]: |
178 lemma SKIP_bury[simp]: |
193 |
193 |
194 lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow> |
194 lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow> |
195 (EX c'. c = WHILE b DO c' & bc' = bury c' (L (WHILE b DO c') X))" |
195 (EX c'. c = WHILE b DO c' & bc' = bury c' (L (WHILE b DO c') X))" |
196 by (cases c) auto |
196 by (cases c) auto |
197 |
197 |
198 theorem bury_sound2: |
198 theorem bury_correct2: |
199 "(bury c X,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
199 "(bury c X,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
200 \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
200 \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
201 proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct) |
201 proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct) |
202 case Skip then show ?case by auto |
202 case Skip then show ?case by auto |
203 next |
203 next |
255 where "(w,t2) \<Rightarrow> t3" "s3 = t3 on X" |
255 where "(w,t2) \<Rightarrow> t3" "s3 = t3 on X" |
256 by auto |
256 by auto |
257 with `bval b t1` `(c', t1) \<Rightarrow> t2` w show ?case by auto |
257 with `bval b t1` `(c', t1) \<Rightarrow> t2` w show ?case by auto |
258 qed |
258 qed |
259 |
259 |
260 corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'" |
260 corollary final_bury_correct2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'" |
261 using bury_sound2[of c UNIV] |
261 using bury_correct2[of c UNIV] |
262 by (auto simp: fun_eq_iff[symmetric]) |
262 by (auto simp: fun_eq_iff[symmetric]) |
263 |
263 |
264 corollary bury_sim: "bury c UNIV \<sim> c" |
264 corollary bury_sim: "bury c UNIV \<sim> c" |
265 by(metis final_bury_sound final_bury_sound2) |
265 by(metis final_bury_correct final_bury_correct2) |
266 |
266 |
267 end |
267 end |