(*  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 ‹
  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);

  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 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↓=♢" 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 context "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 context "P'" "λa vs l vf. PP a vs l vf←x ∧. p" ["PP", "x", "p"]›)
apply       (rule allI)
apply       (tactic ‹simp_tac (context |> 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 context "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 context "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 context "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 context "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 (context |> Simplifier.del_loop "split_all_tac") 1›)
apply   (rule ax_Init_Skip_lemma)
apply  (tactic ‹simp_tac (context |> 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 (context |> 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 context "P'" "λvf l vfa. Normal (P vf l vfa)" ["P"]›)
apply     (tactic ‹simp_tac (context |> 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 context "P" "λvf l vfa. Normal (P vf l vfa←♢)" ["P"]›)
apply      (tactic ‹simp_tac (context |> 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 context "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 (context |> 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 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 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 context "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 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" 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