37 |
37 |
38 |
38 |
39 declare split_if_asm [split del] |
39 declare split_if_asm [split del] |
40 declare lvar_def [simp] |
40 declare lvar_def [simp] |
41 |
41 |
42 ML {* |
42 ML_setup {* |
43 fun inst1_tac s t = instantiate_tac [(s,t)]; |
43 fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of |
|
44 SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty; |
44 val ax_tac = REPEAT o rtac allI THEN' |
45 val ax_tac = REPEAT o rtac allI THEN' |
45 resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN":: |
46 resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN":: |
46 thm "ax_Alloc"::thm "ax_Alloc_Arr":: |
47 thm "ax_Alloc"::thm "ax_Alloc_Arr":: |
47 thm "ax_SXAlloc_Normal":: |
48 thm "ax_SXAlloc_Normal":: |
48 funpow 7 tl (thms "ax_derivs.intros")) |
49 funpow 7 tl (thms "ax_derivs.intros")) |
58 defer (* We begin with the last assertion, to synthesise the intermediate |
59 defer (* We begin with the last assertion, to synthesise the intermediate |
59 assertions, like in the fashion of the weakest |
60 assertions, like in the fashion of the weakest |
60 precondition. *) |
61 precondition. *) |
61 apply (tactic "ax_tac 1" (* Try *)) |
62 apply (tactic "ax_tac 1" (* Try *)) |
62 defer |
63 defer |
63 apply (tactic {* inst1_tac "Q1" |
64 apply (tactic {* inst1_tac "Q" |
64 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *}) |
65 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *}) |
65 prefer 2 |
66 prefer 2 |
66 apply simp |
67 apply simp |
67 apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1) |
68 apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1) |
68 prefer 2 |
69 prefer 2 |
78 apply clarsimp |
79 apply clarsimp |
79 apply (tactic "ax_tac 1") |
80 apply (tactic "ax_tac 1") |
80 apply (tactic "ax_tac 1" (* AVar *)) |
81 apply (tactic "ax_tac 1" (* AVar *)) |
81 prefer 2 |
82 prefer 2 |
82 apply (rule ax_subst_Val_allI) |
83 apply (rule ax_subst_Val_allI) |
83 apply (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
84 apply (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
84 apply (simp del: avar_def2 peek_and_def2) |
85 apply (simp del: avar_def2 peek_and_def2) |
85 apply (tactic "ax_tac 1") |
86 apply (tactic "ax_tac 1") |
86 apply (tactic "ax_tac 1") |
87 apply (tactic "ax_tac 1") |
87 (* just for clarification: *) |
88 (* just for clarification: *) |
88 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) |
89 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) |
119 |
120 |
120 apply (rule ax_derivs.Expr) (* Expr *) |
121 apply (rule ax_derivs.Expr) (* Expr *) |
121 apply (tactic "ax_tac 1") (* Ass *) |
122 apply (tactic "ax_tac 1") (* Ass *) |
122 prefer 2 |
123 prefer 2 |
123 apply (rule ax_subst_Var_allI) |
124 apply (rule ax_subst_Var_allI) |
124 apply (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *}) |
125 apply (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *}) |
125 apply (rule allI) |
126 apply (rule allI) |
126 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *}) |
127 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *}) |
127 apply (rule ax_derivs.Abrupt) |
128 apply (rule ax_derivs.Abrupt) |
128 apply (simp (no_asm)) |
129 apply (simp (no_asm)) |
129 apply (tactic "ax_tac 1" (* FVar *)) |
130 apply (tactic "ax_tac 1" (* FVar *)) |
130 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") |
131 apply (tactic "ax_tac 1") |
132 apply (tactic "ax_tac 1") |
132 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)" *}) |
133 apply (tactic {* inst1_tac "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)" *}) |
133 apply fastsimp |
134 apply fastsimp |
134 prefer 4 |
135 prefer 4 |
135 apply (rule ax_derivs.Done [THEN conseq1],force) |
136 apply (rule ax_derivs.Done [THEN conseq1],force) |
136 apply (rule ax_subst_Val_allI) |
137 apply (rule ax_subst_Val_allI) |
137 apply (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
138 apply (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
138 apply (simp (no_asm) del: peek_and_def2) |
139 apply (simp (no_asm) del: peek_and_def2) |
139 apply (tactic "ax_tac 1") |
140 apply (tactic "ax_tac 1") |
140 prefer 2 |
141 prefer 2 |
141 apply (rule ax_subst_Val_allI) |
142 apply (rule ax_subst_Val_allI) |
142 apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *}) |
143 apply (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *}) |
143 apply (simp del: peek_and_def2) |
144 apply (simp del: peek_and_def2) |
144 apply (tactic "ax_tac 1") |
145 apply (tactic "ax_tac 1") |
145 apply (tactic "ax_tac 1") |
146 apply (tactic "ax_tac 1") |
146 apply (tactic "ax_tac 1") |
147 apply (tactic "ax_tac 1") |
147 apply (tactic "ax_tac 1") |
148 apply (tactic "ax_tac 1") |
156 apply clarsimp |
157 apply clarsimp |
157 apply (tactic "ax_tac 1") |
158 apply (tactic "ax_tac 1") |
158 apply (tactic "ax_tac 1") |
159 apply (tactic "ax_tac 1") |
159 defer |
160 defer |
160 apply (rule ax_subst_Var_allI) |
161 apply (rule ax_subst_Var_allI) |
161 apply (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *}) |
162 apply (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *}) |
162 apply (simp (no_asm) del: split_paired_All peek_and_def2) |
163 apply (simp (no_asm) del: split_paired_All peek_and_def2) |
163 apply (tactic "ax_tac 1" (* NewC *)) |
164 apply (tactic "ax_tac 1" (* NewC *)) |
164 apply (tactic "ax_tac 1" (* ax_Alloc *)) |
165 apply (tactic "ax_tac 1" (* ax_Alloc *)) |
165 (* just for clarification: *) |
166 (* just for clarification: *) |
166 apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2) |
167 apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2) |
184 apply (rule_tac P' = "Normal ?P" in conseq1) |
185 apply (rule_tac P' = "Normal ?P" in conseq1) |
185 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
186 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
186 apply (tactic "ax_tac 1") |
187 apply (tactic "ax_tac 1") |
187 apply (tactic "ax_tac 1") |
188 apply (tactic "ax_tac 1") |
188 apply (rule_tac [2] ax_subst_Var_allI) |
189 apply (rule_tac [2] ax_subst_Var_allI) |
189 apply (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) |
190 apply (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) |
190 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *}) |
191 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *}) |
191 apply (tactic "ax_tac 2" (* NewA *)) |
192 apply (tactic "ax_tac 2" (* NewA *)) |
192 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
193 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
193 apply (tactic "ax_tac 3") |
194 apply (tactic "ax_tac 3") |
194 apply (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) |
195 apply (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) |
195 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *}) |
196 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *}) |
196 apply (tactic "ax_tac 2") |
197 apply (tactic "ax_tac 2") |
197 apply (tactic "ax_tac 1" (* FVar *)) |
198 apply (tactic "ax_tac 1" (* FVar *)) |
198 apply (tactic "ax_tac 2" (* StatRef *)) |
199 apply (tactic "ax_tac 2" (* StatRef *)) |
199 apply (rule ax_derivs.Done [THEN conseq1]) |
200 apply (rule ax_derivs.Done [THEN conseq1]) |
200 apply (tactic {* inst1_tac "Q22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *}) |
201 apply (tactic {* inst1_tac "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *}) |
201 apply (clarsimp split del: split_if) |
202 apply (clarsimp split del: split_if) |
202 apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
203 apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
203 apply (drule initedD) |
204 apply (drule initedD) |
204 apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
205 apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
205 apply force |
206 apply force |
206 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
207 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
207 apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) |
208 apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) |
208 apply (rule wf_tprg) |
209 apply (rule wf_tprg) |
209 apply clarsimp |
210 apply clarsimp |
210 apply (tactic {* inst1_tac "P22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *}) |
211 apply (tactic {* inst1_tac "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *}) |
211 apply clarsimp |
212 apply clarsimp |
212 apply (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *}) |
213 apply (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *}) |
213 apply clarsimp |
214 apply clarsimp |
214 (* end init *) |
215 (* end init *) |
215 apply (rule conseq1) |
216 apply (rule conseq1) |
260 apply (rule conseq1) |
261 apply (rule conseq1) |
261 apply (tactic "ax_tac 1") |
262 apply (tactic "ax_tac 1") |
262 apply (tactic "ax_tac 1") |
263 apply (tactic "ax_tac 1") |
263 prefer 2 |
264 prefer 2 |
264 apply (rule ax_subst_Var_allI) |
265 apply (rule ax_subst_Var_allI) |
265 apply (tactic {* inst1_tac "P'29" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *}) |
266 apply (tactic {* inst1_tac "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *}) |
266 apply (rule allI) |
267 apply (rule allI) |
267 apply (rule_tac P' = "Normal ?P" in conseq1) |
268 apply (rule_tac P' = "Normal ?P" in conseq1) |
268 prefer 2 |
269 prefer 2 |
269 apply clarsimp |
270 apply clarsimp |
270 apply (tactic "ax_tac 1") |
271 apply (tactic "ax_tac 1") |