equal
deleted
inserted
replaced
322 next |
322 next |
323 case Assign thus ?case |
323 case Assign thus ?case |
324 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
324 by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
325 split: option.splits del:subsetD) |
325 split: option.splits del:subsetD) |
326 next |
326 next |
327 case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) |
327 case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
328 by (metis le_post post_map_acom) |
328 by (metis le_post post_map_acom) |
329 next |
329 next |
330 case (If b c1 c2 P) |
330 case (If b c1 c2 P) |
331 then obtain c1' c2' P' where |
331 then obtain c1' c2' P' where |
332 "c' = IF b THEN c1' ELSE c2' {P'}" |
332 "c' = IF b THEN c1' ELSE c2' {P'}" |