equal
deleted
inserted
replaced
64 next |
64 next |
65 case Assign thus ?case |
65 case Assign thus ?case |
66 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
66 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
67 split: option.splits del:subsetD) |
67 split: option.splits del:subsetD) |
68 next |
68 next |
69 case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) |
69 case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
70 by (metis le_post post_map_acom) |
70 by (metis le_post post_map_acom) |
71 next |
71 next |
72 case (If b c1 c2 P) |
72 case (If b c1 c2 P) |
73 then obtain c1' c2' P' where |
73 then obtain c1' c2' P' where |
74 "c' = IF b THEN c1' ELSE c2' {P'}" |
74 "c' = IF b THEN c1' ELSE c2' {P'}" |