equal
deleted
inserted
replaced
94 next |
94 next |
95 case Assign thus ?case |
95 case Assign thus ?case |
96 by(fastforce simp: Assign_le map_acom_Assign wt_st_def |
96 by(fastforce simp: Assign_le map_acom_Assign wt_st_def |
97 intro: aval'_sound in_gamma_update split: option.splits) |
97 intro: aval'_sound in_gamma_update split: option.splits) |
98 next |
98 next |
99 case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) |
99 case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
100 by (metis le_post post_map_acom wt_post) |
100 by (metis le_post post_map_acom wt_post) |
101 next |
101 next |
102 case (If b C1 C2 P) |
102 case (If b C1 C2 P) |
103 then obtain C1' C2' P' where |
103 then obtain C1' C2' P' where |
104 "C' = IF b THEN C1' ELSE C2' {P'}" |
104 "C' = IF b THEN C1' ELSE C2' {P'}" |