src/HOL/Bali/AxExample.thy
 author schirmer Thu, 31 Oct 2002 18:27:10 +0100 changeset 13688 a0b16d42d489 parent 12925 99131847fb93 child 14030 cd928c0ac225 permissions -rw-r--r--
"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.
```
(*  Title:      HOL/Bali/AxExample.thy
ID:         \$Id\$
Author:     David von Oheimb
*)

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

theory AxExample = AxSem + Example:

constdefs
arr_inv :: "st \<Rightarrow> bool"
"arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
values obj (Inl (arr, Base)) = Some (Addr a) \<and>
heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"

lemma arr_inv_new_obj:
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
apply (unfold arr_inv_def)
done

lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm))
done

lemma arr_inv_gupd_Stat [simp]:
"Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm_simp))
done

lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm))
done

declare split_if_asm [split del]
declare lvar_def [simp]

ML {*
fun inst1_tac s t = instantiate_tac [(s,t)];
val ax_tac = REPEAT o rtac allI THEN'
resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
thm "ax_Alloc"::thm "ax_Alloc_Arr"::
thm "ax_SXAlloc_Normal"::
funpow 7 tl (thms "ax_derivs.intros"))
*}

theorem ax_test: "tprg,({}::'a triple set)\<turnstile>
{Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)}
.test [Class Base].
{\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
apply (unfold test_def arr_viewed_from_def)
apply (tactic "ax_tac 1" (*;;*))
defer (* We begin with the last assertion, to synthesise the intermediate
assertions, like in the fashion of the weakest
precondition. *)
apply  (tactic "ax_tac 1" (* Try *))
defer
apply    (tactic {* inst1_tac "Q1"
"\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
prefer 2
apply    simp
apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
prefer 2
apply    clarsimp
apply   (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)
prefer 2
apply    simp
apply   (tactic "ax_tac 1" (* While *))
prefer 2
apply    (rule ax_impossible [THEN conseq1], clarsimp)
apply   (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
apply    clarsimp
apply   (tactic "ax_tac 1")
apply   (tactic "ax_tac 1" (* AVar *))
prefer 2
apply    (rule ax_subst_Val_allI)
apply    (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
apply    (simp del: avar_def2 peek_and_def2)
apply    (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
(* just for clarification: *)
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)
prefer 2
apply   (tactic "ax_tac 1" (* FVar *))
apply    (tactic "ax_tac 2" (* StatRef *))
apply   (rule ax_derivs.Done [THEN conseq1])
apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
defer
apply  (rule ax_SXAlloc_catch_SXcpt)
apply  (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2)
prefer 2
apply  (tactic "ax_tac 1")
apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
apply     (unfold DynT_prop_def)
apply     (simp (no_asm))
apply    (intro strip)
apply    (rule_tac P' = "Normal ?P" in conseq1)
apply     (tactic "ax_tac 1" (* Methd *))
apply     (rule ax_thin [OF _ empty_subsetI])
apply     (tactic "ax_tac 1" (* Body *))
(* apply       (rule_tac  ax_derivs.Abrupt) *)
defer
apply      (simp (no_asm))
apply      (tactic "ax_tac 1") (* Comp *)
(* The first statement in the  composition
((Ext)z).vee = 1; Return Null
will throw an exception (since z is null). So we can handle
Return Null with the Abrupt rule *)
apply       (rule_tac  ax_derivs.Abrupt)

apply      (rule ax_derivs.Expr) (* Expr *)
apply      (tactic "ax_tac 1") (* Ass *)
prefer 2
apply       (rule ax_subst_Var_allI)
apply       (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
apply       (rule allI)
apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
apply       (rule ax_derivs.Abrupt)
apply      (simp (no_asm))
apply      (tactic "ax_tac 1" (* FVar *))
apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
apply      (tactic "ax_tac 1")
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)" *})
apply     fastsimp
prefer 4
apply    (rule ax_derivs.Done [THEN conseq1],force)
apply   (rule ax_subst_Val_allI)
apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
apply   (simp (no_asm) del: peek_and_def2)
apply   (tactic "ax_tac 1")
prefer 2
apply   (rule ax_subst_Val_allI)
apply    (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
apply    (simp del: peek_and_def2)
apply    (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
(* end method call *)
apply (simp (no_asm))
(* just for clarification: *)
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>
invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)
\<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"
in conseq2)
prefer 2
apply  clarsimp
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
defer
apply  (rule ax_subst_Var_allI)
apply  (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
apply  (simp (no_asm) del: split_paired_All peek_and_def2)
apply  (tactic "ax_tac 1" (* NewC *))
apply  (tactic "ax_tac 1" (* ax_Alloc *))
(* just for clarification: *)
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)
prefer 2
apply   (unfold dynlookup_def)
apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
(* begin init *)
apply  (rule ax_InitS)
apply     force
apply    (simp (no_asm))
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
apply   (rule ax_Init_Skip_lemma)
apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
apply  (rule ax_InitS [THEN conseq1] (* init Base *))
apply      force
apply     (simp (no_asm))
apply    (unfold arr_viewed_from_def)
apply    (rule allI)
apply    (rule_tac P' = "Normal ?P" in conseq1)
apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
apply     (tactic "ax_tac 1")
apply     (tactic "ax_tac 1")
apply     (rule_tac  ax_subst_Var_allI)
apply      (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
apply      (tactic "ax_tac 2" (* NewA *))
apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply       (tactic "ax_tac 3")
apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
apply      (tactic "ax_tac 2")
apply     (tactic "ax_tac 1" (* FVar *))
apply      (tactic "ax_tac 2" (* StatRef *))
apply     (rule ax_derivs.Done [THEN conseq1])
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)" *})
apply     (clarsimp split del: split_if)
apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
apply     (drule initedD)
apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
apply    force
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply     (rule wf_tprg)
apply    clarsimp
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)" *})
apply   clarsimp
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)" *})
apply  clarsimp
(* end init *)
apply (rule conseq1)
apply (tactic "ax_tac 1")
apply clarsimp
done

(*
while (true) {
if (i) {throw xcpt;}
else i=j
}
*)
lemma Loop_Xcpt_benchmark:
"Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow>
G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}
.lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
(Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)
apply  safe
apply  (tactic "ax_tac 1" (* Loop *))
apply   (rule ax_Normal_cases)
prefer 2
apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
apply   (rule conseq1)
apply    (tactic "ax_tac 1")
apply   clarsimp
prefer 2
apply  clarsimp
apply (tactic "ax_tac 1" (* If *))
apply  (tactic
{* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
apply  (tactic "ax_tac 1")
apply  (rule conseq1)
apply   (tactic "ax_tac 1")
apply  clarsimp
apply (rule allI)
apply (rule ax_escape)
apply auto
apply  (rule conseq1)
apply   (tactic "ax_tac 1" (* Throw *))
apply   (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
apply  clarsimp
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)
prefer 2
apply  clarsimp
apply (rule conseq1)
apply  (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
prefer 2
apply   (rule ax_subst_Var_allI)
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)" *})
apply   (rule allI)
apply   (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
apply    clarsimp
apply   (tactic "ax_tac 1")
apply   (rule conseq1)
apply    (tactic "ax_tac 1")
apply   clarsimp
apply  (tactic "ax_tac 1")
apply clarsimp
done

end

```