File AxExample.ML

open AxExample;

Delsplits [split_if_asm];
Addsimps[lvar_def];

Goalw [test_def] "enough_mem \<Longrightarrow> tprg,{}\<turnstile>{Normal (\<lambda>Ys Z. True)} .test. \
\ {(\<lambda>Ys Z. True) \<and>. (\<lambda>s. tprg,s\<turnstile>catch SXcpt NP)}";
b y ax_tac 1;
b y defer_tac 1;
b y  ax_tac 1;
b y    defer_tac 1;
b y    inst1_tac "Q1" "(\<lambda>Ys Z. True) \<and>. (\<lambda>s. tprg,s\<turnstile>catch SXcpt NP)";
b y    Clarsimp_tac 2;
b y   Simp_tac 1;
b y   Normal_tac 1;
b y   ax_tac 1;
b y   ax_tac 1;
b y   Simp_tac 1;
b y   rtac conseq1 1;
b y    ax_tac 1;
b y   clarsimp_tac (claset(),simpset() addsimps[throw_def,catch_def])1;
b y  defer_tac 1;
b y  rtac conseq2 1;
b y   etac ax_SXAlloc_catch_SXcpt 1;
b y   Fast_tac 2;
b y  Simp_tac 1;
b y  ax_tac 1;
b y  res_inst_tac [("C","Ext")] ax_Call_known_DynT 1;
b y  Simp_tac 1;
b y     Force_tac 1;
b y    defern_tac 2;
b y    inst1_tac "R24" "Normal ?R";
b y    Normal_tac 1;
b y    ax_tac 1;
b y    rtac (empty_subsetI RSN (2,ax_thin)) 1;
b y    simp_tac (simpset() addsimps [body_def2]) 1;
b y    ax_tac 1;
b y      defern_tac 2;
b y      rtac ax_derivs.Xcpt 1;
b y     defern_tac 4;
b y     ax_tac 1;
b y     ax_tac 1;
b y      rtac ax_derivs.Xcpt 2;
b y     Simp_tac 1;
b y     ax_tac 1;
b y      defer_tac 1;
b y      ax_tac 1;
b y      ax_tac 1;
b y      ax_tac 1;
b y     defern_tac 3;
b y     simp_tac (simpset() addsimps [RefVar_def,Let_def]) 2;
b y     ax_tac 2;
b y    Simp_tac 1;
b y    rtac peek_and_forget1_Normal 1;
b y    ax_tac 1;
b y   defern_tac 2;
b y   Simp_tac 1;
b y   ax_tac 1;
b y    ax_tac 2;
b y   ax_tac 1;
b y  ax_tac 2;
b y  ax_tac 2;
b y Simp_tac 1;
b y ax_tac 1;
b y ax_tac 1;
b y defer_tac 1;
b y  Simp_tac 1;
b y  ax_tac 1;
b y  ax_tac 1;
b y   atac 1;
b y  Simp_tac 1;
b y  rtac conseq2 1;
b y  inst1_tac "Q'51" "Normal (\<lambda>s:(\<lambda>Ys Z. True)\<down>#Var (lvar (EName e) s)) \<and>.\
\                      initd Ext";
b y   Clarsimp_tac 2;
b y  rtac ax_triv_InitS 1;
b y     Force_tac 1;
b y    Simp_tac 1;
b y   Clarsimp_tac 1;
b y  rtac peek_and_forget2 1;
b y  rtac ax_triv_InitS 1;
b y     Force_tac 1;
b y    Simp_tac 1;
b y   Clarsimp_tac 1;
b y  rtac peek_and_forget2 1;
b y  rtac ax_triv_Init_Object 1;
b y   rtac wf_tprg 1;
b y  Clarsimp_tac 1;
b y stac peek_and_and 1;
b y rtac ax_LVar2 1;
qed "ax_test";

(*Goal "G,{}\<turnstile>{} Expr(LVar z:=NewC C);; {t,cT,mode}e..m({[]}[])-\<succ> {}"*)