File AxExample.ML

context AxExample.thy;

Goalw [arr_inv_def] 
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)";
b y force_tac (claset() addSDs [new_AddrD2], simpset()) 1;
qed "arr_inv_new_obj";

Goalw [arr_inv_def] "arr_inv (set_locals l s) = arr_inv s";
b y Simp_tac 1;
qed "arr_inv_set_locals";
Addsimps [arr_inv_set_locals];

Goalw [arr_inv_def] "Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s";
b y Asm_simp_tac 1;
qed "arr_inv_gupd_Stat";
Addsimps [arr_inv_gupd_Stat];

Goalw [arr_inv_def] "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s";
b y Simp_tac 1;
qed "arr_inv_lupd";
Addsimps [arr_inv_lupd];

Delsplits [split_if_asm];
Addsimps[lvar_def];

Goalw [test_def,arr_viewed_from_def] "tprg,({}::'a triple set)\<turnstile>\
\ {Normal (\<lambda>Y s Z::'a. heap_free 4 s \<and> ¬initd Base s \<and> ¬ initd Ext s)}\
\ .test [Class Base]. {\<lambda>Y s Z. fst s = Some (StdXcpt IndOutBound)}";
b y ax_tac 1; (*;;*) 
b y defer_tac 1;
b y  ax_tac 1; (* Try *)
b y    defer_tac 1;
b y    inst1_tac "Q1" "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer";
b y    Simp_tac 2;
b y   res_inst_tac [("P'","Normal (\<lambda>Y s Z. arr_inv (snd s))")] conseq1 1;
b y    Clarsimp_tac 2;
b y    res_inst_tac [("Q'","(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<bullet>")] conseq2 1;
b y    Simp_tac 2;
b y   ax_tac 1; (* While *)
b y    EVERY'[rtac (ax_impossible RS conseq1), Clarsimp_tac] 2;
b y   Normal_tac 1;
b y   ax_tac 1;
b y   ax_tac 1; (* AVar *)
b y    rtac ax_subst_Val_allI 2;
b y    inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u";
b y    simp_tac (simpset() delsimps [avar_def2,peek_and_def2]) 2;
b y    ax_tac 2;
b y   ax_tac 1;
      (* just for clarification: *)
b y   res_inst_tac [("Q'","Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg #2) v u)) = Some (StdXcpt IndOutBound))")] conseq2 1;
b y    clarsimp_tac (claset(), simpset()addsimps[split_beta]) 2;
b y   ax_tac 1; (* FVar *)
b y    ax_tac 2; (* StatRef *)
b y   rtac (ax_derivs.Done RS conseq1) 1;
b y   clarsimp_tac (claset(), 
                   simpset() addsimps [arr_inv_def,inited_def,in_bounds_def]) 1;
b y  defer_tac 1;
b y  rtac ax_SXAlloc_catch_SXcpt 1;
b y  res_inst_tac [("Q'","(\<lambda>Y (x, s) Z. x = Some (StdXcpt NullPointer) \<and> \
\ arr_inv s) \<and>. heap_free 2")] conseq2 1;
b y   simp_tac (simpset() addsimps [arr_inv_new_obj]) 2;
b y  ax_tac 1;
b y  res_inst_tac [("C","Ext")] ax_Call_known_DynT 1;
b y      simp_tac (simpset() delsimps [Pair_eq]) 1;
b y     rewtac DynT_prop_def;
b y     Simp_tac 1;
b y    strip_tac 1;
b y    Normal_tac 1;
b y     ax_tac 1; (* Methd *)
b y     rtac (empty_subsetI RSN (2,ax_thin)) 1;
b y     simp_tac (simpset() addsimps [body_def2]) 1;
b y     ax_tac 1; (* Body *)
b y       rtac ax_derivs.Xcpt 3;
b y      defer_tac 1;
b y      Simp_tac 1;
b y      ax_tac 1;
b y      ax_tac 1; (* Ass *)
b y       rtac ax_subst_Var_allI 2;
b y       inst1_tac "P'38" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p";
b y       rtac allI 2;
b y       simp_tac (simpset() delloop "split_all_tac"delsimps[peek_and_def2]) 2;
b y       rtac ax_derivs.Xcpt 2;
b y      Simp_tac 1;
b y      ax_tac 1; (* FVar *)
b y       EVERY'[ax_tac, ax_tac, ax_tac] 2;
b y      ax_tac 1;
b y     inst1_tac "R16" "\<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 2)";
b y     EVERY'[rtac (ax_derivs.Done RS conseq1), Force_tac] 5;
b y    Force_tac 1;
b y   rtac ax_subst_Val_allI 1;
b y   inst1_tac "P'36" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u";
b y   simp_tac (simpset() delsimps[peek_and_def2]) 1;
b y   ax_tac 1;
b y   rtac ax_subst_Val_allI 2;
b y    inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)";
b y    simp_tac (simpset() delsimps[peek_and_def2]) 2;
b y    ax_tac 2;
b y   ax_tac 1;
b y  ax_tac 1;
b y  ax_tac 1;
(* end method call *)
b y Simp_tac 1;
    (* just for clarification: *)
b y res_inst_tac [("Q'","Normal ((\<lambda>Y (x, s) Z. arr_inv s \<and> (\<exists>a. the (locals s (Inl e)) = Addr a \<and> obj_class (the (globs s (Inl a))) = Ext)) \<and>. initd Ext \<and>. heap_free 2)")] conseq2 1;
b y  clarsimp_tac (claset(), simpset() addsimps [heap_def,o_def(*###*)]) 2;
b y ax_tac 1;
b y ax_tac 1;
b y  defer_tac 1;
b y  rtac ax_subst_Var_allI 1;
b y  inst1_tac "P'16" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u";
b y  simp_tac (simpset() delsimps [split_paired_All]delsimps[peek_and_def2]) 1;
b y  ax_tac 1; (* NewC *)
b y  ax_tac 1; (* ax_Alloc *)
     (* just for clarification: *)
b y  res_inst_tac [("Q'","Normal ((\<lambda>Y s Z. arr_inv (snd s) \<and> vf=lvar (EName e) (snd s))  \<and>. heap_free 3 \<and>. initd Ext)")] conseq2 1;
b y   force_tac (claset()addSEs[arr_inv_new_obj,atleast_free_SucD,atleast_free_weaken], simpset()) 2;
     (* begin init *)
b y  rtac ax_InitS 1;
b y     Force_tac 1;
b y    Simp_tac 1;
b y   rtac ax_Init_Skip_lemma 1;
b y  simp_tac (simpset() delloop "split_all_tac") 1;
b y  rtac (ax_InitS RS conseq1) 1; (* init Base *)
b y      Force_tac 1;
b y     Simp_tac 1;
b y    rewtac arr_viewed_from_def;
b y    rtac allI 1;
b y    Normal_tac 1;
b y     ax_tac 1;
b y     ax_tac 1;
b y     rtac ax_subst_Var_allI 2;
b y      inst1_tac "P'53" "\<lambda>vf l vfa. Normal (?P vf l vfa)";
b y     simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All]delsimps[peek_and_def2]) 2;
b y      ax_tac 2; (* NewA *)
b y       ax_tac 3; (* ax_Alloc_Arr *)
b y       ax_tac 3;
b y      inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<bullet>)";
b y      simp_tac (simpset() delloop "split_all_tac") 2;
b y      ax_tac 2;
b y     ax_tac 1; (* FVar *)
b y      ax_tac 2; (* StatRef *)
b y     rtac (ax_derivs.Done RS conseq1) 1;
b y     inst1_tac "Q35" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (EName e) (snd s)) \<and>. heap_free 4 \<and>. initd Base \<and>. initd Ext)";
b y     clarsimp_tac (claset(), simpset() delsplits [split_if]) 1;
b y     ftac (atleast_free_weaken RS atleast_free_weaken) 1;
b y     dtac initedD 1;
b y     clarsimp_tac (claset() addSEs [atleast_free_SucD], 
                      simpset() addsimps [arr_inv_def]) 1;
b y    Force_tac 1;
b y   rtac (ax_triv_Init_Object RS peek_and_forget2 RS conseq1) 1;
b y     rtac wf_tprg 1;
b y    Clarsimp_tac 1;
b y   inst1_tac "P35" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (EName e) (snd s)) \<and>. heap_free 4 \<and>. initd Ext)";
b y   Clarsimp_tac 1;
b y  inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (EName e) (snd s)) \<and>. heap_free 4 \<and>. Not \<circ> initd Base)";
b y  Clarsimp_tac 1;
     (* end init *)
b y rtac conseq1 1;
b y ax_tac 1;
b y Clarsimp_tac 1;
qed "ax_test";

(*
while (true) {
  if (i) {throw xcpt;}
  else i=j
}
*)
Goal "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)} \
\ .While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else \
\     (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}";
b y res_inst_tac [("P'","Q"),("Q'","Q\<leftarrow>=False\<down>=\<bullet>")] conseq12 1;
b y  Safe_tac;
b y  ax_tac 1; (* Loop *)
b y   Xcpt_cases_tac 1;
b y   rtac conseq1 1;
b y    ax_tac 1;
b y   Clarsimp_tac 1;
b y  Clarsimp_tac 2;
b y ax_tac 1; (* If *)
b y  inst1_tac "P'25" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))";
b y  ax_tac 1;
b y  rtac conseq1 1;
b y   ax_tac 1;
b y  Clarsimp_tac 1;
b y rtac allI 1;
b y rtac ax_escape 1;
b y Auto_tac;
b y  rtac conseq1 1;
b y   ax_tac 1; (* Throw *)
b y   ax_tac 1;
b y   ax_tac 1;
b y  Clarsimp_tac 1;
b y res_inst_tac [("Q'","Normal (\<lambda>Y s Z. True)")] conseq2 1;
b y  Clarsimp_tac 2;
b y rtac conseq1 1;
b y  ax_tac 1;
b y  ax_tac 1;
b y   rtac ax_subst_Var_allI 2;
b y   inst1_tac "P'37" 
                "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)";
b y   rtac allI 2;
b y   Normal_tac 2;
b y   ax_tac 2;
b y   rtac conseq1 2;
b y    ax_tac 2;
b y   Clarsimp_tac 2;
b y  ax_tac 1;
b y Clarsimp_tac 1;
qed "Loop_Xcpt_benchmark";