equal
deleted
inserted
replaced
35 apply (unfold arr_inv_def) |
35 apply (unfold arr_inv_def) |
36 apply (simp (no_asm)) |
36 apply (simp (no_asm)) |
37 done |
37 done |
38 |
38 |
39 |
39 |
40 declare split_if_asm [split del] |
40 declare if_split_asm [split del] |
41 declare lvar_def [simp] |
41 declare lvar_def [simp] |
42 |
42 |
43 ML \<open> |
43 ML \<open> |
44 fun inst1_tac ctxt s t xs st = |
44 fun inst1_tac ctxt s t xs st = |
45 (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of |
45 (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of |
200 apply (tactic "ax_tac @{context} 2") |
200 apply (tactic "ax_tac @{context} 2") |
201 apply (tactic "ax_tac @{context} 1" (* FVar *)) |
201 apply (tactic "ax_tac @{context} 1" (* FVar *)) |
202 apply (tactic "ax_tac @{context} 2" (* StatRef *)) |
202 apply (tactic "ax_tac @{context} 2" (* StatRef *)) |
203 apply (rule ax_derivs.Done [THEN conseq1]) |
203 apply (rule ax_derivs.Done [THEN conseq1]) |
204 apply (tactic \<open>inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" []\<close>) |
204 apply (tactic \<open>inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" []\<close>) |
205 apply (clarsimp split del: split_if) |
205 apply (clarsimp split del: if_split) |
206 apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
206 apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
207 apply (drule initedD) |
207 apply (drule initedD) |
208 apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
208 apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
209 apply force |
209 apply force |
210 apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>) |
210 apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>) |