80 |
80 |
81 |
81 |
82 lemma defs_restrict: |
82 lemma defs_restrict: |
83 "defs c t |` (- lnames c) = t |` (- lnames c)" |
83 "defs c t |` (- lnames c) = t |` (- lnames c)" |
84 proof (induction c arbitrary: t) |
84 proof (induction c arbitrary: t) |
85 case (Semi c1 c2) |
85 case (Seq c1 c2) |
86 hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" |
86 hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" |
87 by simp |
87 by simp |
88 hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = |
88 hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = |
89 t |` (- lnames c1) |` (-lnames c2)" by simp |
89 t |` (- lnames c1) |` (-lnames c2)" by simp |
90 moreover |
90 moreover |
91 from Semi |
91 from Seq |
92 have "defs c2 (defs c1 t) |` (- lnames c2) = |
92 have "defs c2 (defs c1 t) |` (- lnames c2) = |
93 defs c1 t |` (- lnames c2)" |
93 defs c1 t |` (- lnames c2)" |
94 by simp |
94 by simp |
95 hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) = |
95 hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) = |
96 defs c1 t |` (- lnames c2) |` (- lnames c1)" |
96 defs c1 t |` (- lnames c2) |` (- lnames c1)" |
119 next |
119 next |
120 case Assign |
120 case Assign |
121 thus ?case |
121 thus ?case |
122 by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) |
122 by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) |
123 next |
123 next |
124 case (Semi c1 s1 s2 c2 s3) |
124 case (Seq c1 s1 s2 c2 s3) |
125 have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems]) |
125 have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems]) |
126 hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2)) |
126 hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2)) |
127 thus ?case by simp |
127 thus ?case by simp |
128 next |
128 next |
129 case (IfTrue b s c1 s') |
129 case (IfTrue b s c1 s') |
130 hence "approx (defs c1 t) s'" by simp |
130 hence "approx (defs c1 t) s'" by simp |
131 thus ?case by (simp add: approx_merge) |
131 thus ?case by (simp add: approx_merge) |
153 "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'" |
153 "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'" |
154 proof (induction arbitrary: t rule: big_step_induct) |
154 proof (induction arbitrary: t rule: big_step_induct) |
155 case Assign |
155 case Assign |
156 thus ?case by (clarsimp simp: approx_def) |
156 thus ?case by (clarsimp simp: approx_def) |
157 next |
157 next |
158 case (Semi c1 s1 s2 c2 s3) |
158 case (Seq c1 s1 s2 c2 s3) |
159 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" |
159 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" |
160 by (simp add: Int_commute) |
160 by (simp add: Int_commute) |
161 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2" |
161 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2" |
162 by (rule Semi) |
162 by (rule Seq) |
163 hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2" |
163 hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2" |
164 by (simp add: Int_commute) |
164 by (simp add: Int_commute) |
165 hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3" |
165 hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3" |
166 by (rule Semi) |
166 by (rule Seq) |
167 thus ?case by simp |
167 thus ?case by simp |
168 next |
168 next |
169 case (IfTrue b s c1 s' c2) |
169 case (IfTrue b s c1 s' c2) |
170 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" |
170 hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" |
171 by (simp add: Int_commute) |
171 by (simp add: Int_commute) |
291 |
291 |
292 |
292 |
293 lemma bdefs_restrict: |
293 lemma bdefs_restrict: |
294 "bdefs c t |` (- lnames c) = t |` (- lnames c)" |
294 "bdefs c t |` (- lnames c) = t |` (- lnames c)" |
295 proof (induction c arbitrary: t) |
295 proof (induction c arbitrary: t) |
296 case (Semi c1 c2) |
296 case (Seq c1 c2) |
297 hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" |
297 hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" |
298 by simp |
298 by simp |
299 hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = |
299 hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = |
300 t |` (- lnames c1) |` (-lnames c2)" by simp |
300 t |` (- lnames c1) |` (-lnames c2)" by simp |
301 moreover |
301 moreover |
302 from Semi |
302 from Seq |
303 have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = |
303 have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = |
304 bdefs c1 t |` (- lnames c2)" |
304 bdefs c1 t |` (- lnames c2)" |
305 by simp |
305 by simp |
306 hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) = |
306 hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) = |
307 bdefs c1 t |` (- lnames c2) |` (- lnames c1)" |
307 bdefs c1 t |` (- lnames c2) |` (- lnames c1)" |
332 next |
332 next |
333 case Assign |
333 case Assign |
334 thus ?case |
334 thus ?case |
335 by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) |
335 by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) |
336 next |
336 next |
337 case (Semi c1 s1 s2 c2 s3) |
337 case (Seq c1 s1 s2 c2 s3) |
338 have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems]) |
338 have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems]) |
339 hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2)) |
339 hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2)) |
340 thus ?case by simp |
340 thus ?case by simp |
341 next |
341 next |
342 case (IfTrue b s c1 s') |
342 case (IfTrue b s c1 s') |
343 hence "approx (bdefs c1 t) s'" by simp |
343 hence "approx (bdefs c1 t) s'" by simp |
344 thus ?case using `bval b s` `approx t s` |
344 thus ?case using `bval b s` `approx t s` |
375 case SKIP show ?case by simp |
375 case SKIP show ?case by simp |
376 next |
376 next |
377 case Assign |
377 case Assign |
378 thus ?case by (simp add: equiv_up_to_def) |
378 thus ?case by (simp add: equiv_up_to_def) |
379 next |
379 next |
380 case Semi |
380 case Seq |
381 thus ?case by (auto intro!: equiv_up_to_semi) |
381 thus ?case by (auto intro!: equiv_up_to_seq) |
382 next |
382 next |
383 case (If b c1 c2) |
383 case (If b c1 c2) |
384 hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> |
384 hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> |
385 IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t" |
385 IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t" |
386 by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) |
386 by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) |