equal
deleted
inserted
replaced
141 with G app |
141 with G app |
142 show ?thesis |
142 show ?thesis |
143 by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 |
143 by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 |
144 sup_loc_length sup_state_conv) |
144 sup_loc_length sup_state_conv) |
145 next |
145 next |
146 case Bipush |
146 case LitPush |
147 with G app |
|
148 show ?thesis by simp |
|
149 next |
|
150 case Aconst_null |
|
151 with G app |
147 with G app |
152 show ?thesis by simp |
148 show ?thesis by simp |
153 next |
149 next |
154 case New |
150 case New |
155 with G app |
151 with G app |
353 case Store |
349 case Store |
354 with G s step app1 app2 |
350 with G s step app1 app2 |
355 show ?thesis |
351 show ?thesis |
356 by (clarsimp simp add: sup_state_conv sup_loc_update) |
352 by (clarsimp simp add: sup_state_conv sup_loc_update) |
357 next |
353 next |
358 case Bipush |
354 case LitPush |
359 with G s step app1 app2 |
355 with G s step app1 app2 |
360 show ?thesis |
356 show ?thesis |
361 by (clarsimp simp add: sup_state_Cons1) |
357 by (clarsimp simp add: sup_state_Cons1) |
362 next |
358 next |
363 case New |
359 case New |
364 with G s step app1 app2 |
|
365 show ?thesis |
|
366 by (clarsimp simp add: sup_state_Cons1) |
|
367 next |
|
368 case Aconst_null |
|
369 with G s step app1 app2 |
360 with G s step app1 app2 |
370 show ?thesis |
361 show ?thesis |
371 by (clarsimp simp add: sup_state_Cons1) |
362 by (clarsimp simp add: sup_state_Cons1) |
372 next |
363 next |
373 case Getfield |
364 case Getfield |