src/HOL/Bali/AxExample.thy
 author wenzelm Sat Jan 02 18:48:45 2016 +0100 (2016-01-02) changeset 62042 6c6ccf573479 parent 60754 02924903a6fd child 62390 842917225d56 permissions -rw-r--r--
isabelle update_cartouches -c -t;
1 (*  Title:      HOL/Bali/AxExample.thy
2     Author:     David von Oheimb
3 *)
5 subsection \<open>Example of a proof based on the Bali axiomatic semantics\<close>
7 theory AxExample
8 imports AxSem Example
9 begin
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>
14                               values obj (Inl (arr, Base)) = Some (Addr a) \<and>
15                               heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
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)
21 done
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
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
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
40 declare split_if_asm [split del]
41 declare lvar_def [simp]
43 ML \<open>
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
46     SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
47   | NONE => Seq.empty);
49 fun ax_tac ctxt =
50   REPEAT o resolve_tac ctxt [allI] THEN'
51   resolve_tac ctxt
52     @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
53 \<close>
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)}
58   .test [Class Base].
59   {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
60 apply (unfold test_def arr_viewed_from_def)
61 apply (tactic "ax_tac @{context} 1" (*;;*))
62 defer (* We begin with the last assertion, to synthesise the intermediate
63          assertions, like in the fashion of the weakest
64          precondition. *)
65 apply  (tactic "ax_tac @{context} 1" (* Try *))
66 defer
67 apply    (tactic \<open>inst1_tac @{context} "Q"
68                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" []\<close>)
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>" and Q = Q for Q in conseq2)
75 prefer 2
76 apply    simp
77 apply   (tactic "ax_tac @{context} 1" (* While *))
78 prefer 2
79 apply    (rule ax_impossible [THEN conseq1], clarsimp)
80 apply   (rule_tac P' = "Normal P" and P = P for P in conseq1)
81 prefer 2
82 apply    clarsimp
83 apply   (tactic "ax_tac @{context} 1")
84 apply   (tactic "ax_tac @{context} 1" (* AVar *))
85 prefer 2
86 apply    (rule ax_subst_Val_allI)
87 apply    (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"]\<close>)
88 apply    (simp del: avar_def2 peek_and_def2)
89 apply    (tactic "ax_tac @{context} 1")
90 apply   (tactic "ax_tac @{context} 1")
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)
95 apply   (tactic "ax_tac @{context} 1" (* FVar *))
96 apply    (tactic "ax_tac @{context} 2" (* StatRef *))
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
104 apply  (tactic "ax_tac @{context} 1")
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" and P = P for P in conseq1)
110 apply     (tactic "ax_tac @{context} 1" (* Methd *))
111 apply     (rule ax_thin [OF _ empty_subsetI])
112 apply     (simp (no_asm) add: body_def2)
113 apply     (tactic "ax_tac @{context} 1" (* Body *))
114 (* apply       (rule_tac [2] ax_derivs.Abrupt) *)
115 defer
116 apply      (simp (no_asm))
117 apply      (tactic "ax_tac @{context} 1") (* Comp *)
118             (* The first statement in the  composition
119                  ((Ext)z).vee = 1; Return Null
120                 will throw an exception (since z is null). So we can handle
121                 Return Null with the Abrupt rule *)
122 apply       (rule_tac [2] ax_derivs.Abrupt)
124 apply      (rule ax_derivs.Expr) (* Expr *)
125 apply      (tactic "ax_tac @{context} 1") (* Ass *)
126 prefer 2
127 apply       (rule ax_subst_Var_allI)
128 apply       (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"]\<close>)
129 apply       (rule allI)
130 apply       (tactic \<open>simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1\<close>)
131 apply       (rule ax_derivs.Abrupt)
132 apply      (simp (no_asm))
133 apply      (tactic "ax_tac @{context} 1" (* FVar *))
134 apply       (tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2")
135 apply      (tactic "ax_tac @{context} 1")
136 apply     (tactic \<open>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)" []\<close>)
137 apply     fastforce
138 prefer 4
139 apply    (rule ax_derivs.Done [THEN conseq1],force)
140 apply   (rule ax_subst_Val_allI)
141 apply   (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"]\<close>)
142 apply   (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
143 apply   (tactic "ax_tac @{context} 1")
144 prefer 2
145 apply   (rule ax_subst_Val_allI)
146 apply    (tactic \<open>inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"]\<close>)
147 apply    (simp del: peek_and_def2 heap_free_def2 normal_def2)
148 apply    (tactic "ax_tac @{context} 1")
149 apply   (tactic "ax_tac @{context} 1")
150 apply  (tactic "ax_tac @{context} 1")
151 apply  (tactic "ax_tac @{context} 1")
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
161 apply (tactic "ax_tac @{context} 1")
162 apply (tactic "ax_tac @{context} 1")
163 defer
164 apply  (rule ax_subst_Var_allI)
165 apply  (tactic \<open>inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"]\<close>)
166 apply  (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
167 apply  (tactic "ax_tac @{context} 1" (* NewC *))
168 apply  (tactic "ax_tac @{context} 1" (* ax_Alloc *))
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)
171 prefer 2
172 apply   (simp add: invocation_declclass_def dynmethd_def)
173 apply   (unfold dynlookup_def)
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))
180 apply   (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
181 apply   (rule ax_Init_Skip_lemma)
182 apply  (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
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" and P = P for P in conseq1)
189 apply     (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
190 apply     (tactic "ax_tac @{context} 1")
191 apply     (tactic "ax_tac @{context} 1")
192 apply     (rule_tac [2] ax_subst_Var_allI)
193 apply      (tactic \<open>inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"]\<close>)
194 apply     (tactic \<open>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\<close>)
195 apply      (tactic "ax_tac @{context} 2" (* NewA *))
196 apply       (tactic "ax_tac @{context} 3" (* ax_Alloc_Arr *))
197 apply       (tactic "ax_tac @{context} 3")
198 apply      (tactic \<open>inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"]\<close>)
199 apply      (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 2\<close>)
200 apply      (tactic "ax_tac @{context} 2")
201 apply     (tactic "ax_tac @{context} 1" (* FVar *))
202 apply      (tactic "ax_tac @{context} 2" (* StatRef *))
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>)
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
210 apply   (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
211 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
212 apply     (rule wf_tprg)
213 apply    clarsimp
214 apply   (tactic \<open>inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" []\<close>)
215 apply   clarsimp
216 apply  (tactic \<open>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)" []\<close>)
217 apply  clarsimp
218      (* end init *)
219 apply (rule conseq1)
220 apply (tactic "ax_tac @{context} 1")
221 apply clarsimp
222 done
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
237 apply  (tactic "ax_tac @{context} 1" (* Loop *))
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)
242 apply    (tactic "ax_tac @{context} 1")
243 apply   clarsimp
244 prefer 2
245 apply  clarsimp
246 apply (tactic "ax_tac @{context} 1" (* If *))
247 apply  (tactic
248   \<open>inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" []\<close>)
249 apply  (tactic "ax_tac @{context} 1")
250 apply  (rule conseq1)
251 apply   (tactic "ax_tac @{context} 1")
252 apply  clarsimp
253 apply (rule allI)
254 apply (rule ax_escape)
255 apply auto
256 apply  (rule conseq1)
257 apply   (tactic "ax_tac @{context} 1" (* Throw *))
258 apply   (tactic "ax_tac @{context} 1")
259 apply   (tactic "ax_tac @{context} 1")
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)
265 apply  (tactic "ax_tac @{context} 1")
266 apply  (tactic "ax_tac @{context} 1")
267 prefer 2
268 apply   (rule ax_subst_Var_allI)
269 apply   (tactic \<open>inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" []\<close>)
270 apply   (rule allI)
271 apply   (rule_tac P' = "Normal P" and P = P for P in conseq1)
272 prefer 2
273 apply    clarsimp
274 apply   (tactic "ax_tac @{context} 1")
275 apply   (rule conseq1)
276 apply    (tactic "ax_tac @{context} 1")
277 apply   clarsimp
278 apply  (tactic "ax_tac @{context} 1")
279 apply clarsimp
280 done
282 end