12854

1 
(* Title: isabelle/Bali/AxExample.thy


2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 2000 Technische Universitaet Muenchen


5 
*)


6 
header {* Example of a proof based on the Bali axiomatic semantics *}


7 


8 
theory AxExample = AxSem + Example:


9 


10 
constdefs


11 
arr_inv :: "st \<Rightarrow> bool"


12 
"arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>


13 
values obj (Inl (arr, Base)) = Some (Addr a) \<and>


14 
heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"


15 


16 
lemma arr_inv_new_obj:


17 
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"


18 
apply (unfold arr_inv_def)


19 
apply (force dest!: new_AddrD2)


20 
done


21 


22 
lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s"


23 
apply (unfold arr_inv_def)


24 
apply (simp (no_asm))


25 
done


26 


27 
lemma arr_inv_gupd_Stat [simp]:


28 
"Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s"


29 
apply (unfold arr_inv_def)


30 
apply (simp (no_asm_simp))


31 
done


32 


33 
lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s"


34 
apply (unfold arr_inv_def)


35 
apply (simp (no_asm))


36 
done


37 


38 


39 
declare split_if_asm [split del]


40 
declare lvar_def [simp]


41 


42 
ML {*


43 
fun inst1_tac s t = instantiate_tac [(s,t)];


44 
val ax_tac = REPEAT o rtac allI THEN'


45 
resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::


46 
thm "ax_Alloc"::thm "ax_Alloc_Arr"::


47 
thm "ax_SXAlloc_Normal"::


48 
funpow 7 tl (thms "ax_derivs.intros"))


49 
*}


50 


51 


52 
theorem ax_test: "tprg,({}::'a triple set)\<turnstile>


53 
{Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)}


54 
.test [Class Base]. {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"


55 
apply (unfold test_def arr_viewed_from_def)


56 
apply (tactic "ax_tac 1" (*;;*))


57 
defer


58 
apply (tactic "ax_tac 1" (* Try *))


59 
defer


60 
apply (tactic {* inst1_tac "Q1"


61 
"\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})


62 
prefer 2


63 
apply simp


64 
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)


65 
prefer 2


66 
apply clarsimp


67 
apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)


68 
prefer 2


69 
apply simp


70 
apply (tactic "ax_tac 1" (* While *))


71 
prefer 2


72 
apply (rule ax_impossible [THEN conseq1], clarsimp)


73 
apply (rule_tac P' = "Normal ?P" in conseq1)


74 
prefer 2


75 
apply clarsimp


76 
apply (tactic "ax_tac 1")


77 
apply (tactic "ax_tac 1" (* AVar *))


78 
prefer 2


79 
apply (rule ax_subst_Val_allI)


80 
apply (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})


81 
apply (simp del: avar_def2 peek_and_def2)


82 
apply (tactic "ax_tac 1")


83 
apply (tactic "ax_tac 1")


84 
(* just for clarification: *)


85 
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)


86 
prefer 2


87 
apply (clarsimp simp add: split_beta)


88 
apply (tactic "ax_tac 1" (* FVar *))


89 
apply (tactic "ax_tac 2" (* StatRef *))


90 
apply (rule ax_derivs.Done [THEN conseq1])


91 
apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def)


92 
defer


93 
apply (rule ax_SXAlloc_catch_SXcpt)


94 
apply (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2)


95 
prefer 2


96 
apply (simp add: arr_inv_new_obj)


97 
apply (tactic "ax_tac 1")


98 
apply (rule_tac C = "Ext" in ax_Call_known_DynT)


99 
apply (unfold DynT_prop_def)


100 
apply (simp (no_asm))


101 
apply (intro strip)


102 
apply (rule_tac P' = "Normal ?P" in conseq1)


103 
apply (tactic "ax_tac 1" (* Methd *))


104 
apply (rule ax_thin [OF _ empty_subsetI])


105 
apply (simp (no_asm) add: body_def2)


106 
apply (tactic "ax_tac 1" (* Body *))


107 
(* apply (rule_tac [2] ax_derivs.Abrupt) *)


108 
defer


109 
apply (simp (no_asm))


110 
apply (tactic "ax_tac 1")


111 
apply (tactic "ax_tac 1") (* Ass *)


112 
prefer 2


113 
apply (rule ax_subst_Var_allI)


114 
apply (tactic {* inst1_tac "P'27" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})


115 
apply (rule allI)


116 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})


117 
apply (rule ax_derivs.Abrupt)


118 
apply (simp (no_asm))


119 
apply (tactic "ax_tac 1" (* FVar *))


120 
apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")


121 
apply (tactic "ax_tac 1")


122 
apply clarsimp


123 
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> hd vs = Null) \<and>. heap_free two)" *})


124 
prefer 5


125 
apply (rule ax_derivs.Done [THEN conseq1], force)


126 
apply force


127 
apply (rule ax_subst_Val_allI)


128 
apply (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})


129 
apply (simp (no_asm) del: peek_and_def2)


130 
apply (tactic "ax_tac 1")


131 
prefer 2


132 
apply (rule ax_subst_Val_allI)


133 
apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})


134 
apply (simp del: peek_and_def2)


135 
apply (tactic "ax_tac 1")


136 
apply (tactic "ax_tac 1")


137 
apply (tactic "ax_tac 1")


138 
apply (tactic "ax_tac 1")


139 
(* end method call *)


140 
apply (simp (no_asm))


141 
(* just for clarification: *)


142 
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>


143 
invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)


144 
\<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"


145 
in conseq2)


146 
prefer 2


147 
apply clarsimp


148 
apply (tactic "ax_tac 1")


149 
apply (tactic "ax_tac 1")


150 
defer


151 
apply (rule ax_subst_Var_allI)


152 
apply (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})


153 
apply (simp (no_asm) del: split_paired_All peek_and_def2)


154 
apply (tactic "ax_tac 1" (* NewC *))


155 
apply (tactic "ax_tac 1" (* ax_Alloc *))


156 
(* just for clarification: *)


157 
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)


158 
prefer 2


159 
apply (simp add: invocation_declclass_def dynmethd_def)


160 
apply (unfold dynlookup_def)


161 
apply (simp add: dynmethd_Ext_foo)


162 
apply (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)


163 
(* begin init *)


164 
apply (rule ax_InitS)


165 
apply force


166 
apply (simp (no_asm))


167 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})


168 
apply (rule ax_Init_Skip_lemma)


169 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})


170 
apply (rule ax_InitS [THEN conseq1] (* init Base *))


171 
apply force


172 
apply (simp (no_asm))


173 
apply (unfold arr_viewed_from_def)


174 
apply (rule allI)


175 
apply (rule_tac P' = "Normal ?P" in conseq1)


176 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})


177 
apply (tactic "ax_tac 1")


178 
apply (tactic "ax_tac 1")


179 
apply (rule_tac [2] ax_subst_Var_allI)


180 
apply (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})


181 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})


182 
apply (tactic "ax_tac 2" (* NewA *))


183 
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))


184 
apply (tactic "ax_tac 3")


185 
apply (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})


186 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})


187 
apply (tactic "ax_tac 2")


188 
apply (tactic "ax_tac 1" (* FVar *))


189 
apply (tactic "ax_tac 2" (* StatRef *))


190 
apply (rule ax_derivs.Done [THEN conseq1])


191 
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)" *})


192 
apply (clarsimp split del: split_if)


193 
apply (frule atleast_free_weaken [THEN atleast_free_weaken])


194 
apply (drule initedD)


195 
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)


196 
apply force


197 
apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})


198 
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])


199 
apply (rule wf_tprg)


200 
apply clarsimp


201 
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)" *})


202 
apply clarsimp


203 
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)" *})


204 
apply clarsimp


205 
(* end init *)


206 
apply (rule conseq1)


207 
apply (tactic "ax_tac 1")


208 
apply clarsimp


209 
done


210 


211 
(*


212 
while (true) {


213 
if (i) {throw xcpt;}


214 
else i=j


215 
}


216 
*)


217 
lemma Loop_Xcpt_benchmark:


218 
"Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow>


219 
G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}


220 
.lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else


221 
(Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"


222 
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)


223 
apply safe


224 
apply (tactic "ax_tac 1" (* Loop *))


225 
apply (rule ax_Normal_cases)


226 
prefer 2


227 
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)


228 
apply (rule conseq1)


229 
apply (tactic "ax_tac 1")


230 
apply clarsimp


231 
prefer 2


232 
apply clarsimp


233 
apply (tactic "ax_tac 1" (* If *))


234 
apply (tactic


235 
{* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})


236 
apply (tactic "ax_tac 1")


237 
apply (rule conseq1)


238 
apply (tactic "ax_tac 1")


239 
apply clarsimp


240 
apply (rule allI)


241 
apply (rule ax_escape)


242 
apply auto


243 
apply (rule conseq1)


244 
apply (tactic "ax_tac 1" (* Throw *))


245 
apply (tactic "ax_tac 1")


246 
apply (tactic "ax_tac 1")


247 
apply clarsimp


248 
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)


249 
prefer 2


250 
apply clarsimp


251 
apply (rule conseq1)


252 
apply (tactic "ax_tac 1")


253 
apply (tactic "ax_tac 1")


254 
prefer 2


255 
apply (rule ax_subst_Var_allI)


256 
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)" *})


257 
apply (rule allI)


258 
apply (rule_tac P' = "Normal ?P" in conseq1)


259 
prefer 2


260 
apply clarsimp


261 
apply (tactic "ax_tac 1")


262 
apply (rule conseq1)


263 
apply (tactic "ax_tac 1")


264 
apply clarsimp


265 
apply (tactic "ax_tac 1")


266 
apply clarsimp


267 
done


268 


269 
end


270 
