equal
deleted
inserted
replaced
330 next |
330 next |
331 case Assign thus ?case |
331 case Assign thus ?case |
332 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
332 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
333 split: option.splits del:subsetD) |
333 split: option.splits del:subsetD) |
334 next |
334 next |
335 case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) |
335 case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
336 by (metis le_post post_map_acom) |
336 by (metis le_post post_map_acom) |
337 next |
337 next |
338 case (If b C1 C2 P) |
338 case (If b C1 C2 P) |
339 then obtain D1 D2 P' where |
339 then obtain D1 D2 P' where |
340 "C' = IF b THEN D1 ELSE D2 {P'}" |
340 "C' = IF b THEN D1 ELSE D2 {P'}" |