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 |
46 SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st |
46 SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st |
47 | NONE => Seq.empty); |
47 | NONE => Seq.empty); |
48 |
48 |
49 val ax_tac = |
49 fun ax_tac ctxt = |
50 REPEAT o rtac allI THEN' |
50 REPEAT o rtac allI THEN' |
51 resolve_tac (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: |
51 resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: |
52 @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)}); |
52 @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)}); |
53 *} |
53 *} |
54 |
54 |
55 |
55 |
56 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> |
56 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> |
57 {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} |
57 {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} |
58 .test [Class Base]. |
58 .test [Class Base]. |
59 {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" |
59 {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" |
60 apply (unfold test_def arr_viewed_from_def) |
60 apply (unfold test_def arr_viewed_from_def) |
61 apply (tactic "ax_tac 1" (*;;*)) |
61 apply (tactic "ax_tac @{context} 1" (*;;*)) |
62 defer (* We begin with the last assertion, to synthesise the intermediate |
62 defer (* We begin with the last assertion, to synthesise the intermediate |
63 assertions, like in the fashion of the weakest |
63 assertions, like in the fashion of the weakest |
64 precondition. *) |
64 precondition. *) |
65 apply (tactic "ax_tac 1" (* Try *)) |
65 apply (tactic "ax_tac @{context} 1" (* Try *)) |
66 defer |
66 defer |
67 apply (tactic {* inst1_tac @{context} "Q" |
67 apply (tactic {* inst1_tac @{context} "Q" |
68 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *}) |
68 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *}) |
69 prefer 2 |
69 prefer 2 |
70 apply simp |
70 apply simp |
72 prefer 2 |
72 prefer 2 |
73 apply clarsimp |
73 apply clarsimp |
74 apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2) |
74 apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2) |
75 prefer 2 |
75 prefer 2 |
76 apply simp |
76 apply simp |
77 apply (tactic "ax_tac 1" (* While *)) |
77 apply (tactic "ax_tac @{context} 1" (* While *)) |
78 prefer 2 |
78 prefer 2 |
79 apply (rule ax_impossible [THEN conseq1], clarsimp) |
79 apply (rule ax_impossible [THEN conseq1], clarsimp) |
80 apply (rule_tac P' = "Normal ?P" in conseq1) |
80 apply (rule_tac P' = "Normal ?P" in conseq1) |
81 prefer 2 |
81 prefer 2 |
82 apply clarsimp |
82 apply clarsimp |
83 apply (tactic "ax_tac 1") |
83 apply (tactic "ax_tac @{context} 1") |
84 apply (tactic "ax_tac 1" (* AVar *)) |
84 apply (tactic "ax_tac @{context} 1" (* AVar *)) |
85 prefer 2 |
85 prefer 2 |
86 apply (rule ax_subst_Val_allI) |
86 apply (rule ax_subst_Val_allI) |
87 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
87 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
88 apply (simp del: avar_def2 peek_and_def2) |
88 apply (simp del: avar_def2 peek_and_def2) |
89 apply (tactic "ax_tac 1") |
89 apply (tactic "ax_tac @{context} 1") |
90 apply (tactic "ax_tac 1") |
90 apply (tactic "ax_tac @{context} 1") |
91 (* just for clarification: *) |
91 (* just for clarification: *) |
92 apply (rule_tac Q' = "Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2) |
92 apply (rule_tac Q' = "Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2) |
93 prefer 2 |
93 prefer 2 |
94 apply (clarsimp simp add: split_beta) |
94 apply (clarsimp simp add: split_beta) |
95 apply (tactic "ax_tac 1" (* FVar *)) |
95 apply (tactic "ax_tac @{context} 1" (* FVar *)) |
96 apply (tactic "ax_tac 2" (* StatRef *)) |
96 apply (tactic "ax_tac @{context} 2" (* StatRef *)) |
97 apply (rule ax_derivs.Done [THEN conseq1]) |
97 apply (rule ax_derivs.Done [THEN conseq1]) |
98 apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) |
98 apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) |
99 defer |
99 defer |
100 apply (rule ax_SXAlloc_catch_SXcpt) |
100 apply (rule ax_SXAlloc_catch_SXcpt) |
101 apply (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2) |
101 apply (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2) |
102 prefer 2 |
102 prefer 2 |
103 apply (simp add: arr_inv_new_obj) |
103 apply (simp add: arr_inv_new_obj) |
104 apply (tactic "ax_tac 1") |
104 apply (tactic "ax_tac @{context} 1") |
105 apply (rule_tac C = "Ext" in ax_Call_known_DynT) |
105 apply (rule_tac C = "Ext" in ax_Call_known_DynT) |
106 apply (unfold DynT_prop_def) |
106 apply (unfold DynT_prop_def) |
107 apply (simp (no_asm)) |
107 apply (simp (no_asm)) |
108 apply (intro strip) |
108 apply (intro strip) |
109 apply (rule_tac P' = "Normal ?P" in conseq1) |
109 apply (rule_tac P' = "Normal ?P" in conseq1) |
110 apply (tactic "ax_tac 1" (* Methd *)) |
110 apply (tactic "ax_tac @{context} 1" (* Methd *)) |
111 apply (rule ax_thin [OF _ empty_subsetI]) |
111 apply (rule ax_thin [OF _ empty_subsetI]) |
112 apply (simp (no_asm) add: body_def2) |
112 apply (simp (no_asm) add: body_def2) |
113 apply (tactic "ax_tac 1" (* Body *)) |
113 apply (tactic "ax_tac @{context} 1" (* Body *)) |
114 (* apply (rule_tac [2] ax_derivs.Abrupt) *) |
114 (* apply (rule_tac [2] ax_derivs.Abrupt) *) |
115 defer |
115 defer |
116 apply (simp (no_asm)) |
116 apply (simp (no_asm)) |
117 apply (tactic "ax_tac 1") (* Comp *) |
117 apply (tactic "ax_tac @{context} 1") (* Comp *) |
118 (* The first statement in the composition |
118 (* The first statement in the composition |
119 ((Ext)z).vee = 1; Return Null |
119 ((Ext)z).vee = 1; Return Null |
120 will throw an exception (since z is null). So we can handle |
120 will throw an exception (since z is null). So we can handle |
121 Return Null with the Abrupt rule *) |
121 Return Null with the Abrupt rule *) |
122 apply (rule_tac [2] ax_derivs.Abrupt) |
122 apply (rule_tac [2] ax_derivs.Abrupt) |
123 |
123 |
124 apply (rule ax_derivs.Expr) (* Expr *) |
124 apply (rule ax_derivs.Expr) (* Expr *) |
125 apply (tactic "ax_tac 1") (* Ass *) |
125 apply (tactic "ax_tac @{context} 1") (* Ass *) |
126 prefer 2 |
126 prefer 2 |
127 apply (rule ax_subst_Var_allI) |
127 apply (rule ax_subst_Var_allI) |
128 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *}) |
128 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *}) |
129 apply (rule allI) |
129 apply (rule allI) |
130 apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *}) |
130 apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *}) |
131 apply (rule ax_derivs.Abrupt) |
131 apply (rule ax_derivs.Abrupt) |
132 apply (simp (no_asm)) |
132 apply (simp (no_asm)) |
133 apply (tactic "ax_tac 1" (* FVar *)) |
133 apply (tactic "ax_tac @{context} 1" (* FVar *)) |
134 apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") |
134 apply (tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2") |
135 apply (tactic "ax_tac 1") |
135 apply (tactic "ax_tac @{context} 1") |
136 apply (tactic {* inst1_tac @{context} "R" "\<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)" [] *}) |
136 apply (tactic {* inst1_tac @{context} "R" "\<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)" [] *}) |
137 apply fastforce |
137 apply fastforce |
138 prefer 4 |
138 prefer 4 |
139 apply (rule ax_derivs.Done [THEN conseq1],force) |
139 apply (rule ax_derivs.Done [THEN conseq1],force) |
140 apply (rule ax_subst_Val_allI) |
140 apply (rule ax_subst_Val_allI) |
141 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
141 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
142 apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) |
142 apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) |
143 apply (tactic "ax_tac 1") |
143 apply (tactic "ax_tac @{context} 1") |
144 prefer 2 |
144 prefer 2 |
145 apply (rule ax_subst_Val_allI) |
145 apply (rule ax_subst_Val_allI) |
146 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *}) |
146 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *}) |
147 apply (simp del: peek_and_def2 heap_free_def2 normal_def2) |
147 apply (simp del: peek_and_def2 heap_free_def2 normal_def2) |
148 apply (tactic "ax_tac 1") |
148 apply (tactic "ax_tac @{context} 1") |
149 apply (tactic "ax_tac 1") |
149 apply (tactic "ax_tac @{context} 1") |
150 apply (tactic "ax_tac 1") |
150 apply (tactic "ax_tac @{context} 1") |
151 apply (tactic "ax_tac 1") |
151 apply (tactic "ax_tac @{context} 1") |
152 (* end method call *) |
152 (* end method call *) |
153 apply (simp (no_asm)) |
153 apply (simp (no_asm)) |
154 (* just for clarification: *) |
154 (* just for clarification: *) |
155 apply (rule_tac Q' = "Normal ((\<lambda>Y (x, s) Z. arr_inv s \<and> (\<exists>a. the (locals s (VName e)) = Addr a \<and> obj_class (the (globs s (Inl a))) = Ext \<and> |
155 apply (rule_tac Q' = "Normal ((\<lambda>Y (x, s) Z. arr_inv s \<and> (\<exists>a. the (locals s (VName e)) = Addr a \<and> obj_class (the (globs s (Inl a))) = Ext \<and> |
156 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) |
156 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) |
157 \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)" |
157 \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)" |
158 in conseq2) |
158 in conseq2) |
159 prefer 2 |
159 prefer 2 |
160 apply clarsimp |
160 apply clarsimp |
161 apply (tactic "ax_tac 1") |
161 apply (tactic "ax_tac @{context} 1") |
162 apply (tactic "ax_tac 1") |
162 apply (tactic "ax_tac @{context} 1") |
163 defer |
163 defer |
164 apply (rule ax_subst_Var_allI) |
164 apply (rule ax_subst_Var_allI) |
165 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *}) |
165 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *}) |
166 apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) |
166 apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) |
167 apply (tactic "ax_tac 1" (* NewC *)) |
167 apply (tactic "ax_tac @{context} 1" (* NewC *)) |
168 apply (tactic "ax_tac 1" (* ax_Alloc *)) |
168 apply (tactic "ax_tac @{context} 1" (* ax_Alloc *)) |
169 (* just for clarification: *) |
169 (* just for clarification: *) |
170 apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2) |
170 apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2) |
171 prefer 2 |
171 prefer 2 |
172 apply (simp add: invocation_declclass_def dynmethd_def) |
172 apply (simp add: invocation_declclass_def dynmethd_def) |
173 apply (unfold dynlookup_def) |
173 apply (unfold dynlookup_def) |
185 apply (simp (no_asm)) |
185 apply (simp (no_asm)) |
186 apply (unfold arr_viewed_from_def) |
186 apply (unfold arr_viewed_from_def) |
187 apply (rule allI) |
187 apply (rule allI) |
188 apply (rule_tac P' = "Normal ?P" in conseq1) |
188 apply (rule_tac P' = "Normal ?P" in conseq1) |
189 apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
189 apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
190 apply (tactic "ax_tac 1") |
190 apply (tactic "ax_tac @{context} 1") |
191 apply (tactic "ax_tac 1") |
191 apply (tactic "ax_tac @{context} 1") |
192 apply (rule_tac [2] ax_subst_Var_allI) |
192 apply (rule_tac [2] ax_subst_Var_allI) |
193 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *}) |
193 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *}) |
194 apply (tactic {* simp_tac (@{context} 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 *}) |
194 apply (tactic {* simp_tac (@{context} 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 *}) |
195 apply (tactic "ax_tac 2" (* NewA *)) |
195 apply (tactic "ax_tac @{context} 2" (* NewA *)) |
196 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
196 apply (tactic "ax_tac @{context} 3" (* ax_Alloc_Arr *)) |
197 apply (tactic "ax_tac 3") |
197 apply (tactic "ax_tac @{context} 3") |
198 apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *}) |
198 apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *}) |
199 apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *}) |
199 apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *}) |
200 apply (tactic "ax_tac 2") |
200 apply (tactic "ax_tac @{context} 2") |
201 apply (tactic "ax_tac 1" (* FVar *)) |
201 apply (tactic "ax_tac @{context} 1" (* FVar *)) |
202 apply (tactic "ax_tac 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 {* 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)" [] *}) |
204 apply (tactic {* 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)" [] *}) |
205 apply (clarsimp split del: split_if) |
205 apply (clarsimp split del: split_if) |
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) |
232 G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)} |
232 G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)} |
233 .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else |
233 .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else |
234 (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" |
234 (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" |
235 apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12) |
235 apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12) |
236 apply safe |
236 apply safe |
237 apply (tactic "ax_tac 1" (* Loop *)) |
237 apply (tactic "ax_tac @{context} 1" (* Loop *)) |
238 apply (rule ax_Normal_cases) |
238 apply (rule ax_Normal_cases) |
239 prefer 2 |
239 prefer 2 |
240 apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
240 apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
241 apply (rule conseq1) |
241 apply (rule conseq1) |
242 apply (tactic "ax_tac 1") |
242 apply (tactic "ax_tac @{context} 1") |
243 apply clarsimp |
243 apply clarsimp |
244 prefer 2 |
244 prefer 2 |
245 apply clarsimp |
245 apply clarsimp |
246 apply (tactic "ax_tac 1" (* If *)) |
246 apply (tactic "ax_tac @{context} 1" (* If *)) |
247 apply (tactic |
247 apply (tactic |
248 {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *}) |
248 {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *}) |
249 apply (tactic "ax_tac 1") |
249 apply (tactic "ax_tac @{context} 1") |
250 apply (rule conseq1) |
250 apply (rule conseq1) |
251 apply (tactic "ax_tac 1") |
251 apply (tactic "ax_tac @{context} 1") |
252 apply clarsimp |
252 apply clarsimp |
253 apply (rule allI) |
253 apply (rule allI) |
254 apply (rule ax_escape) |
254 apply (rule ax_escape) |
255 apply auto |
255 apply auto |
256 apply (rule conseq1) |
256 apply (rule conseq1) |
257 apply (tactic "ax_tac 1" (* Throw *)) |
257 apply (tactic "ax_tac @{context} 1" (* Throw *)) |
258 apply (tactic "ax_tac 1") |
258 apply (tactic "ax_tac @{context} 1") |
259 apply (tactic "ax_tac 1") |
259 apply (tactic "ax_tac @{context} 1") |
260 apply clarsimp |
260 apply clarsimp |
261 apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2) |
261 apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2) |
262 prefer 2 |
262 prefer 2 |
263 apply clarsimp |
263 apply clarsimp |
264 apply (rule conseq1) |
264 apply (rule conseq1) |
265 apply (tactic "ax_tac 1") |
265 apply (tactic "ax_tac @{context} 1") |
266 apply (tactic "ax_tac 1") |
266 apply (tactic "ax_tac @{context} 1") |
267 prefer 2 |
267 prefer 2 |
268 apply (rule ax_subst_Var_allI) |
268 apply (rule ax_subst_Var_allI) |
269 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *}) |
269 apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *}) |
270 apply (rule allI) |
270 apply (rule allI) |
271 apply (rule_tac P' = "Normal ?P" in conseq1) |
271 apply (rule_tac P' = "Normal ?P" in conseq1) |
272 prefer 2 |
272 prefer 2 |
273 apply clarsimp |
273 apply clarsimp |
274 apply (tactic "ax_tac 1") |
274 apply (tactic "ax_tac @{context} 1") |
275 apply (rule conseq1) |
275 apply (rule conseq1) |
276 apply (tactic "ax_tac 1") |
276 apply (tactic "ax_tac @{context} 1") |
277 apply clarsimp |
277 apply clarsimp |
278 apply (tactic "ax_tac 1") |
278 apply (tactic "ax_tac @{context} 1") |
279 apply clarsimp |
279 apply clarsimp |
280 done |
280 done |
281 |
281 |
282 end |
282 end |
283 |
283 |