(* Title: HOL/Bali/AxExample.thy
Author: David von Oheimb
*)
subsection ‹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 if_split_asm [split del]
declare lvar_def [simp]
ML
‹
fun inst1_tac ctxt s t xs st =
(
case AList.lookup (op =) (rev (
Term.add_var_names (
Thm.prop_of st) [])) s of
SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
| NONE => Seq.empty);
fun ax_tac ctxt =
REPEAT o resolve_tac ctxt [allI]
THEN'
resolve_tac ctxt
@{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal 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 \<^context> 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 \<^context> 1" (* Try *))
defer
apply (tactic
‹inst1_tac
🍋 "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\=\" and Q = Q for Q in conseq2)
prefer 2
apply simp
apply (tactic
"ax_tac \<^context> 1" (* While *))
prefer 2
apply (rule ax_impossible [
THEN conseq1], clarsimp)
apply (rule_tac P
' = "Normal P" and P = P for P in conseq1)
prefer 2
apply clarsimp
apply (tactic
"ax_tac \<^context> 1")
apply (tactic
"ax_tac \<^context> 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
apply (tactic
‹inst1_tac
🍋 "P'" "\a. Normal (PP a\x)" [
"PP",
"x"]
›)
apply (simp del: avar_def2 peek_and_def2)
apply (tactic
"ax_tac \<^context> 1")
apply (tactic
"ax_tac \<^context> 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 \<^context> 1" (* FVar *))
apply (tactic
"ax_tac \<^context> 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 \<^context> 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" and P = P for P in conseq1)
apply (tactic
"ax_tac \<^context> 1" (* Methd *))
apply (rule ax_thin [OF _ empty_subsetI])
apply (simp (no_asm) add: body_def2)
apply (tactic
"ax_tac \<^context> 1" (* Body *))
(* apply (rule_tac [2] ax_derivs.Abrupt) *)
defer
apply (simp (no_asm))
apply (tactic
"ax_tac \<^context> 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 \<^context> 1")
(* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
apply (tactic
‹inst1_tac
🍋 "P'" "\a vs l vf. PP a vs l vf\x \. p" [
"PP",
"x",
"p"]
›)
apply (rule allI)
apply (tactic
‹simp_tac (
🍋 |> Simplifier.del_loop
"split_all_tac" |> Simplifier.del_simps
[@{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 \<^context> 1" (* FVar *))
apply (tactic "ax_tac \<^context> 2", tactic "ax_tac \<^context> 2", tactic "ax_tac \<^context> 2")
apply (tactic "ax_tac \<^context> 1")
apply (tactic ‹inst1_tac 🍋 "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" []›)
apply fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
apply (tactic ‹inst1_tac 🍋 "P'" "\a. Normal (PP a\x)" ["PP", "x"]›)
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac \<^context> 1")
prefer 2
apply (rule ax_subst_Val_allI)
apply (tactic ‹inst1_tac 🍋 "P'" "\aa v. Normal (QQ aa v\y)" ["QQ", "y"]›)
apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac \<^context> 1")
apply (tactic "ax_tac \<^context> 1")
apply (tactic "ax_tac \<^context> 1")
apply (tactic "ax_tac \<^context> 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 \<^context> 1")
apply (tactic "ax_tac \<^context> 1")
defer
apply (rule ax_subst_Var_allI)
apply (tactic ‹inst1_tac 🍋 "P'" "\vf. Normal (PP vf \. p)" ["PP", "p"]›)
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac \<^context> 1" (* NewC *))
apply (tactic "ax_tac \<^context> 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 (🍋 |> Simplifier.del_loop "split_all_tac") 1›)
apply (rule ax_Init_Skip_lemma)
apply (tactic ‹simp_tac (🍋 |> Simplifier.del_loop "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" and P = P for P in conseq1)
apply (tactic ‹simp_tac (🍋 |> Simplifier.del_loop "split_all_tac") 1›)
apply (tactic "ax_tac \<^context> 1")
apply (tactic "ax_tac \<^context> 1")
apply (rule_tac [2] ax_subst_Var_allI)
apply (tactic ‹inst1_tac 🍋 "P'" "\vf l vfa. Normal (P vf l vfa)" ["P"]›)
apply (tactic ‹simp_tac (🍋 |> Simplifier.del_loop "split_all_tac" |> Simplifier.del_simps [@{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 \<^context> 2" (* NewA *))
apply (tactic "ax_tac \<^context> 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac \<^context> 3")
apply (tactic ‹inst1_tac 🍋 "P" "\vf l vfa. Normal (P vf l vfa\\)" ["P"]›)
apply (tactic ‹simp_tac (🍋 |> Simplifier.del_loop "split_all_tac") 2›)
apply (tactic "ax_tac \<^context> 2")
apply (tactic "ax_tac \<^context> 1" (* FVar *))
apply (tactic "ax_tac \<^context> 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
apply (tactic ‹inst1_tac 🍋 "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" []›)
apply (clarsimp split del: if_split)
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 (🍋 |> Simplifier.del_loop "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 🍋 "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" []›)
apply clarsimp
apply (tactic ‹inst1_tac 🍋 "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 \<^context> 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 \<^context> 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 \<^context> 1")
apply clarsimp
prefer 2
apply clarsimp
apply (tactic "ax_tac \<^context> 1" (* If *))
apply (tactic
‹inst1_tac 🍋 "P'" "Normal (\s.. (\Y s Z. True)\=Val (the (locals s i)))" []›)
apply (tactic "ax_tac \<^context> 1")
apply (rule conseq1)
apply (tactic "ax_tac \<^context> 1")
apply clarsimp
apply (rule allI)
apply (rule ax_escape)
apply auto
apply (rule conseq1)
apply (tactic "ax_tac \<^context> 1" (* Throw *))
apply (tactic "ax_tac \<^context> 1")
apply (tactic "ax_tac \<^context> 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 \<^context> 1")
apply (tactic "ax_tac \<^context> 1")
prefer 2
apply (rule ax_subst_Var_allI)
apply (tactic ‹inst1_tac 🍋 "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" and P = P for P in conseq1)
prefer 2
apply clarsimp
apply (tactic "ax_tac \<^context> 1")
apply (rule conseq1)
apply (tactic "ax_tac \<^context> 1")
apply clarsimp
apply (tactic "ax_tac \<^context> 1")
apply clarsimp
done
end
