187 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) |
187 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) |
188 apply (tactic "ax_tac 1") |
188 apply (tactic "ax_tac 1") |
189 apply (tactic "ax_tac 1") |
189 apply (tactic "ax_tac 1") |
190 apply (rule_tac [2] ax_subst_Var_allI) |
190 apply (rule_tac [2] ax_subst_Var_allI) |
191 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) |
191 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) |
192 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) |
192 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) |
193 apply (tactic "ax_tac 2" (* NewA *)) |
193 apply (tactic "ax_tac 2" (* NewA *)) |
194 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
194 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
195 apply (tactic "ax_tac 3") |
195 apply (tactic "ax_tac 3") |
196 apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) |
196 apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) |
197 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *}) |
197 apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *}) |