(* Title: HOL/Bali/AxExample.thy Author: David von Oheimb *) header {* Example of a proof based on the Bali axiomatic semantics *} theory AxExample imports AxSem Example begin definition arr_inv :: "st \ bool" where "arr_inv = (\s. \obj a T el. globs s (Stat Base) = Some obj \ values obj (Inl (arr, Base)) = Some (Addr a) \ heap s a = Some \tag=Arr T 2,values=el\)" lemma arr_inv_new_obj: "\a. \arr_inv s; new_Addr (heap s)=Some a\ \ arr_inv (gupd(Inl a\x) s)" apply (unfold arr_inv_def) apply (force dest!: new_AddrD2) 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 \ C \ arr_inv (gupd(Stat C\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\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 ctxt s t st = case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty; 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} :: @{thms ax_derivs.intros(8-)}); *} theorem ax_test: "tprg,({}::'a triple set)\ {Normal (\Y s Z::'a. heap_free four s \ \initd Base s \ \ initd Ext s)} .test [Class Base]. {\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 @{context} "Q" "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" *}) prefer 2 apply simp apply (rule_tac P' = "Normal (\Y s Z. arr_inv (snd s))" in conseq1) prefer 2 apply clarsimp apply (rule_tac Q' = "(\Y s Z. ?Q Y s Z)\=False\=\" 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 @{context} "P'" "\u a. Normal (?PP a\?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 (\Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2) prefer 2 apply (clarsimp simp add: split_beta) 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' = "(\Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \ arr_inv s) \. heap_free two" in conseq2) prefer 2 apply (simp add: arr_inv_new_obj) 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 (simp (no_asm) add: body_def2) apply (tactic "ax_tac 1" (* Body *)) (* apply (rule_tac [2] 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 [2] 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 @{context} "P'" "\a vs l vf. ?PP a vs l vf\?x \. ?p" *}) apply (rule allI) apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_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 @{context} "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. 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 @{context} "P'" "\u a. Normal (?PP a\?x) u" *}) apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) apply (tactic "ax_tac 1") prefer 2 apply (rule ax_subst_Val_allI) apply (tactic {* inst1_tac @{context} "P'" "\aa v. Normal (?QQ aa v\?y)" *}) apply (simp del: peek_and_def2 heap_free_def2 normal_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 ((\Y (x, s) Z. arr_inv s \ (\a. the (locals s (VName e)) = Addr a \ obj_class (the (globs s (Inl a))) = Ext \ invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) \name = foo, parTs = [Class Base]\ = Ext)) \. initd Ext \. 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 @{context} "P'" "\u vf. Normal (?PP vf \. ?p) u" *}) apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) apply (tactic "ax_tac 1" (* NewC *)) apply (tactic "ax_tac 1" (* ax_Alloc *)) (* just for clarification: *) apply (rule_tac Q' = "Normal ((\Y s Z. arr_inv (store s) \ vf=lvar (VName e) (store s)) \. heap_free three \. initd Ext)" in conseq2) prefer 2 apply (simp add: invocation_declclass_def dynmethd_def) apply (unfold dynlookup_def) apply (simp add: dynmethd_Ext_foo) 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 [2] ax_subst_Var_allI) apply (tactic {* inst1_tac @{context} "P'" "\vf l vfa. Normal (?P vf l vfa)" *}) apply (tactic {* simp_tac (@{simpset} 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 *}) apply (tactic "ax_tac 2" (* NewA *)) apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) apply (tactic "ax_tac 3") apply (tactic {* inst1_tac @{context} "P" "\vf l vfa. Normal (?P vf l vfa\\)" *}) 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 @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. 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 @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" *}) apply clarsimp apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ 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 = (\Y (x,s) Z. x \ None \ the_Bool (the (locals s i))) \ G,({}::'a triple set)\{Normal (\Y s Z::'a. True)} .lab1\ 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\=False\=\" 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 @{context} "P'" "Normal (\s.. (\Y s Z. True)\=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 (\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 @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ 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