author | wenzelm |
Tue, 10 Feb 2015 14:48:26 +0100 | |
changeset 59498 | 50b60f501b05 |
parent 58887 | 38db8ddc0f57 |
child 59755 | f8d164ab0dc1 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/AxExample.thy |
12854 | 2 |
Author: David von Oheimb |
3 |
*) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
4 |
|
58887 | 5 |
subsection {* Example of a proof based on the Bali axiomatic semantics *} |
12854 | 6 |
|
33965 | 7 |
theory AxExample |
8 |
imports AxSem Example |
|
9 |
begin |
|
12854 | 10 |
|
37956 | 11 |
definition |
12 |
arr_inv :: "st \<Rightarrow> bool" where |
|
13 |
"arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and> |
|
12854 | 14 |
values obj (Inl (arr, Base)) = Some (Addr a) \<and> |
37956 | 15 |
heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)" |
12854 | 16 |
|
17 |
lemma arr_inv_new_obj: |
|
18 |
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)" |
|
19 |
apply (unfold arr_inv_def) |
|
20 |
apply (force dest!: new_AddrD2) |
|
21 |
done |
|
22 |
||
23 |
lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s" |
|
24 |
apply (unfold arr_inv_def) |
|
25 |
apply (simp (no_asm)) |
|
26 |
done |
|
27 |
||
28 |
lemma arr_inv_gupd_Stat [simp]: |
|
29 |
"Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s" |
|
30 |
apply (unfold arr_inv_def) |
|
31 |
apply (simp (no_asm_simp)) |
|
32 |
done |
|
33 |
||
34 |
lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s" |
|
35 |
apply (unfold arr_inv_def) |
|
36 |
apply (simp (no_asm)) |
|
37 |
done |
|
38 |
||
39 |
||
40 |
declare split_if_asm [split del] |
|
41 |
declare lvar_def [simp] |
|
42 |
||
16121 | 43 |
ML {* |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
44 |
fun inst1_tac ctxt s t xs st = |
55151 | 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 |
|
47 |
| NONE => Seq.empty); |
|
20195 | 48 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
49 |
fun ax_tac ctxt = |
20195 | 50 |
REPEAT o rtac allI THEN' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
51 |
resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: |
27240 | 52 |
@{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)}); |
12854 | 53 |
*} |
54 |
||
55 |
||
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)} |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
58 |
.test [Class Base]. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
59 |
{\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" |
12854 | 60 |
apply (unfold test_def arr_viewed_from_def) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
61 |
apply (tactic "ax_tac @{context} 1" (*;;*)) |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
62 |
defer (* We begin with the last assertion, to synthesise the intermediate |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
63 |
assertions, like in the fashion of the weakest |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
64 |
precondition. *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
65 |
apply (tactic "ax_tac @{context} 1" (* Try *)) |
12854 | 66 |
defer |
27240 | 67 |
apply (tactic {* inst1_tac @{context} "Q" |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
68 |
"\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *}) |
12854 | 69 |
prefer 2 |
70 |
apply simp |
|
71 |
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1) |
|
72 |
prefer 2 |
|
73 |
apply clarsimp |
|
74 |
apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2) |
|
75 |
prefer 2 |
|
76 |
apply simp |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
77 |
apply (tactic "ax_tac @{context} 1" (* While *)) |
12854 | 78 |
prefer 2 |
79 |
apply (rule ax_impossible [THEN conseq1], clarsimp) |
|
80 |
apply (rule_tac P' = "Normal ?P" in conseq1) |
|
81 |
prefer 2 |
|
82 |
apply clarsimp |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
83 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
84 |
apply (tactic "ax_tac @{context} 1" (* AVar *)) |
12854 | 85 |
prefer 2 |
86 |
apply (rule ax_subst_Val_allI) |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
87 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
12854 | 88 |
apply (simp del: avar_def2 peek_and_def2) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
89 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
90 |
apply (tactic "ax_tac @{context} 1") |
12854 | 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) |
|
93 |
prefer 2 |
|
94 |
apply (clarsimp simp add: split_beta) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
95 |
apply (tactic "ax_tac @{context} 1" (* FVar *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
96 |
apply (tactic "ax_tac @{context} 2" (* StatRef *)) |
12854 | 97 |
apply (rule ax_derivs.Done [THEN conseq1]) |
98 |
apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) |
|
99 |
defer |
|
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) |
|
102 |
prefer 2 |
|
103 |
apply (simp add: arr_inv_new_obj) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
104 |
apply (tactic "ax_tac @{context} 1") |
12854 | 105 |
apply (rule_tac C = "Ext" in ax_Call_known_DynT) |
106 |
apply (unfold DynT_prop_def) |
|
107 |
apply (simp (no_asm)) |
|
108 |
apply (intro strip) |
|
109 |
apply (rule_tac P' = "Normal ?P" in conseq1) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
110 |
apply (tactic "ax_tac @{context} 1" (* Methd *)) |
12854 | 111 |
apply (rule ax_thin [OF _ empty_subsetI]) |
112 |
apply (simp (no_asm) add: body_def2) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
113 |
apply (tactic "ax_tac @{context} 1" (* Body *)) |
12854 | 114 |
(* apply (rule_tac [2] ax_derivs.Abrupt) *) |
115 |
defer |
|
116 |
apply (simp (no_asm)) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
117 |
apply (tactic "ax_tac @{context} 1") (* Comp *) |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
118 |
(* The first statement in the composition |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
119 |
((Ext)z).vee = 1; Return Null |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
120 |
will throw an exception (since z is null). So we can handle |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
121 |
Return Null with the Abrupt rule *) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
122 |
apply (rule_tac [2] ax_derivs.Abrupt) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
123 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
124 |
apply (rule ax_derivs.Expr) (* Expr *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
125 |
apply (tactic "ax_tac @{context} 1") (* Ass *) |
12854 | 126 |
prefer 2 |
127 |
apply (rule ax_subst_Var_allI) |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
128 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *}) |
12854 | 129 |
apply (rule allI) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
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 *}) |
12854 | 131 |
apply (rule ax_derivs.Abrupt) |
132 |
apply (simp (no_asm)) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
133 |
apply (tactic "ax_tac @{context} 1" (* FVar *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
134 |
apply (tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
135 |
apply (tactic "ax_tac @{context} 1") |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
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)" [] *}) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
37956
diff
changeset
|
137 |
apply fastforce |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
138 |
prefer 4 |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
12925
diff
changeset
|
139 |
apply (rule ax_derivs.Done [THEN conseq1],force) |
12854 | 140 |
apply (rule ax_subst_Val_allI) |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
141 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *}) |
26810
255a347eae43
Locally deleted some definitions that were applied too eagerly because
berghofe
parents:
26342
diff
changeset
|
142 |
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
143 |
apply (tactic "ax_tac @{context} 1") |
12854 | 144 |
prefer 2 |
145 |
apply (rule ax_subst_Val_allI) |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
146 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *}) |
26810
255a347eae43
Locally deleted some definitions that were applied too eagerly because
berghofe
parents:
26342
diff
changeset
|
147 |
apply (simp del: peek_and_def2 heap_free_def2 normal_def2) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
148 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
149 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
150 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
151 |
apply (tactic "ax_tac @{context} 1") |
12854 | 152 |
(* end method call *) |
153 |
apply (simp (no_asm)) |
|
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> |
|
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)" |
|
158 |
in conseq2) |
|
159 |
prefer 2 |
|
160 |
apply clarsimp |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
161 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
162 |
apply (tactic "ax_tac @{context} 1") |
12854 | 163 |
defer |
164 |
apply (rule ax_subst_Var_allI) |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
165 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *}) |
26810
255a347eae43
Locally deleted some definitions that were applied too eagerly because
berghofe
parents:
26342
diff
changeset
|
166 |
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
167 |
apply (tactic "ax_tac @{context} 1" (* NewC *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
168 |
apply (tactic "ax_tac @{context} 1" (* ax_Alloc *)) |
12854 | 169 |
(* just for clarification: *) |
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
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) |
12854 | 171 |
prefer 2 |
172 |
apply (simp add: invocation_declclass_def dynmethd_def) |
|
173 |
apply (unfold dynlookup_def) |
|
174 |
apply (simp add: dynmethd_Ext_foo) |
|
175 |
apply (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken) |
|
176 |
(* begin init *) |
|
177 |
apply (rule ax_InitS) |
|
178 |
apply force |
|
179 |
apply (simp (no_asm)) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
180 |
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
12854 | 181 |
apply (rule ax_Init_Skip_lemma) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
182 |
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
12854 | 183 |
apply (rule ax_InitS [THEN conseq1] (* init Base *)) |
184 |
apply force |
|
185 |
apply (simp (no_asm)) |
|
186 |
apply (unfold arr_viewed_from_def) |
|
187 |
apply (rule allI) |
|
188 |
apply (rule_tac P' = "Normal ?P" in conseq1) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
189 |
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
190 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
191 |
apply (tactic "ax_tac @{context} 1") |
12854 | 192 |
apply (rule_tac [2] ax_subst_Var_allI) |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
193 |
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *}) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
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 *}) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
195 |
apply (tactic "ax_tac @{context} 2" (* NewA *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
196 |
apply (tactic "ax_tac @{context} 3" (* ax_Alloc_Arr *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
197 |
apply (tactic "ax_tac @{context} 3") |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
198 |
apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *}) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
199 |
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *}) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
200 |
apply (tactic "ax_tac @{context} 2") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
201 |
apply (tactic "ax_tac @{context} 1" (* FVar *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
202 |
apply (tactic "ax_tac @{context} 2" (* StatRef *)) |
12854 | 203 |
apply (rule ax_derivs.Done [THEN conseq1]) |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
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)" [] *}) |
12854 | 205 |
apply (clarsimp split del: split_if) |
206 |
apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
|
207 |
apply (drule initedD) |
|
208 |
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
|
209 |
apply force |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48262
diff
changeset
|
210 |
apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *}) |
12854 | 211 |
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) |
212 |
apply (rule wf_tprg) |
|
213 |
apply clarsimp |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
214 |
apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *}) |
12854 | 215 |
apply clarsimp |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
216 |
apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *}) |
12854 | 217 |
apply clarsimp |
218 |
(* end init *) |
|
219 |
apply (rule conseq1) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
220 |
apply (tactic "ax_tac @{context} 1") |
12854 | 221 |
apply clarsimp |
222 |
done |
|
223 |
||
224 |
(* |
|
225 |
while (true) { |
|
226 |
if (i) {throw xcpt;} |
|
227 |
else i=j |
|
228 |
} |
|
229 |
*) |
|
230 |
lemma Loop_Xcpt_benchmark: |
|
231 |
"Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow> |
|
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 |
|
234 |
(Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" |
|
235 |
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12) |
|
236 |
apply safe |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
237 |
apply (tactic "ax_tac @{context} 1" (* Loop *)) |
12854 | 238 |
apply (rule ax_Normal_cases) |
239 |
prefer 2 |
|
240 |
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
|
241 |
apply (rule conseq1) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
242 |
apply (tactic "ax_tac @{context} 1") |
12854 | 243 |
apply clarsimp |
244 |
prefer 2 |
|
245 |
apply clarsimp |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
246 |
apply (tactic "ax_tac @{context} 1" (* If *)) |
12854 | 247 |
apply (tactic |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
248 |
{* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *}) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
249 |
apply (tactic "ax_tac @{context} 1") |
12854 | 250 |
apply (rule conseq1) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
251 |
apply (tactic "ax_tac @{context} 1") |
12854 | 252 |
apply clarsimp |
253 |
apply (rule allI) |
|
254 |
apply (rule ax_escape) |
|
255 |
apply auto |
|
256 |
apply (rule conseq1) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
257 |
apply (tactic "ax_tac @{context} 1" (* Throw *)) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
258 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
259 |
apply (tactic "ax_tac @{context} 1") |
12854 | 260 |
apply clarsimp |
261 |
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2) |
|
262 |
prefer 2 |
|
263 |
apply clarsimp |
|
264 |
apply (rule conseq1) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
265 |
apply (tactic "ax_tac @{context} 1") |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
266 |
apply (tactic "ax_tac @{context} 1") |
12854 | 267 |
prefer 2 |
268 |
apply (rule ax_subst_Var_allI) |
|
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
51717
diff
changeset
|
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)" [] *}) |
12854 | 270 |
apply (rule allI) |
271 |
apply (rule_tac P' = "Normal ?P" in conseq1) |
|
272 |
prefer 2 |
|
273 |
apply clarsimp |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
274 |
apply (tactic "ax_tac @{context} 1") |
12854 | 275 |
apply (rule conseq1) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
276 |
apply (tactic "ax_tac @{context} 1") |
12854 | 277 |
apply clarsimp |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58887
diff
changeset
|
278 |
apply (tactic "ax_tac @{context} 1") |
12854 | 279 |
apply clarsimp |
280 |
done |
|
281 |
||
282 |
end |
|
283 |