128 apply (rule ax_derivs.Abrupt) |
128 apply (rule ax_derivs.Abrupt) |
129 apply (simp (no_asm)) |
129 apply (simp (no_asm)) |
130 apply (tactic "ax_tac 1" (* FVar *)) |
130 apply (tactic "ax_tac 1" (* FVar *)) |
131 apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") |
131 apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") |
132 apply (tactic "ax_tac 1") |
132 apply (tactic "ax_tac 1") |
133 apply (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *}) |
133 apply (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *}) |
134 apply fastsimp |
134 apply fastsimp |
135 prefer 4 |
135 prefer 4 |
136 apply (rule ax_derivs.Done [THEN conseq1],force) |
136 apply (rule ax_derivs.Done [THEN conseq1],force) |
137 apply (rule ax_subst_Val_allI) |
137 apply (rule ax_subst_Val_allI) |
138 apply (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
138 apply (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
139 apply (simp (no_asm) del: peek_and_def2) |
139 apply (simp (no_asm) del: peek_and_def2) |
140 apply (tactic "ax_tac 1") |
140 apply (tactic "ax_tac 1") |
141 prefer 2 |
141 prefer 2 |
142 apply (rule ax_subst_Val_allI) |
142 apply (rule ax_subst_Val_allI) |
143 apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *}) |
143 apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *}) |