File Example.ML

open Example;

AddIs [widen.null];
Goalw [wf_fdecl_def] "\<And>fd. wf_fdecl G fd = is_type G (snd (snd fd))";
b y Simp_tac 1;
qed "wf_fdecl_def2";
AddIffs [wf_fdecl_def2];

Addsimps [inj_tnam_, inj_enam_];
Addsimps [Object_mdecls_def,SXcpt_mdecls_def];

qed_goal "no_iface" thy "¬ is_iface tprg I" (K [Simp_tac 1]);
qed_goalw "no_subint1" thy [subint1_def] 
		"subint1 tprg = {}" (K [Auto_tac]);
Addsimps [no_iface, no_subint1];

qed_goalw "table_classes_Object" thy [classes_def, standard_classes_def,ObjectC_def] 
 	"table_of classes Object = Some (arbitrary, [], [], Object_mdecls, Skip)" 
	(K [Simp_tac 1]);
qed_goalw "table_classes_SXcpt" thy [classes_def, standard_classes_def, ObjectC_def,SXcptC_def] 
  "table_of classes (SXcpt xn) = Some (if xn = Throwable then Object \
\ else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)" (K [
	induct_tac "xn" 1, ALLGOALS Simp_tac]);
Goalw [classes_def, ObjectC_def,SXcptC_def] 
 	"table_of classes Base = Some BaseCl";
b y Simp_tac 1;
qed "table_classes_Base";
Goalw [classes_def, ObjectC_def,SXcptC_def]
    "table_of classes Ext = Some ExtCl";
b y Simp_tac 1; 
qed "table_classes_Ext";
Addsimps [table_classes_Object, table_classes_SXcpt, 
	  table_classes_Base, table_classes_Ext];

Goal "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R";
b y auto_tac (claset() addSDs [tranclD,subcls1D],simpset());
qed "not_Object_subcls_any"; 
AddSEs [not_Object_subcls_any];

Goal "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R";
b y auto_tac (claset() addSDs [tranclD,subcls1D],simpset());
qed "not_Throwable_subcls_SXcpt"; 
AddSEs [not_Throwable_subcls_SXcpt];

Goal "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R";
b y auto_tac (claset() addSDs [tranclD,subcls1D],simpset());
b y dtac rtranclD 1;
b y Auto_tac;
qed "not_SXcpt_n_subcls_SXcpt_n"; 
AddSEs [not_SXcpt_n_subcls_SXcpt_n];

Goal "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R";
b y auto_tac (claset() addSDs [tranclD,subcls1D],simpset()addsimps[BaseCl_def]);
qed "not_Base_subcls_Ext";
AddSEs [not_Base_subcls_Ext];

Goal "(TName tn, TName tn) \<in> (subcls1 tprg)^+ \<longrightarrow> R";
b y res_inst_tac [("n1","tn")] (surj_tnam_  RS exE) 1;
b y etac ssubst 1;
b y rtac tnam_.induct 1;
b y  Safe_tac;
b y auto_tac (claset() addSDs [tranclD,subcls1D],
              simpset()addsimps[BaseCl_def,ExtCl_def]);
b y dtac rtranclD 1;
b y Auto_tac;
qed_spec_mp "not_TName_n_subcls_TName_n";
AddSEs [not_TName_n_subcls_TName_n];

Goalw [classes_def, standard_classes_def,ObjectC_def,SXcptC_def] "unique classes";
b y EVERY[REPEAT (rtac unique_ConsI 1 THEN Force_tac 2), Simp_tac 1];
qed "unique_classes";

Goal "tprg\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable";
b y rtac SXcpt_subcls_Throwable_lemma 1;
b y Force_tac 1;
qed "SXcpt_subcls_Throwable_";
Addsimps [SXcpt_subcls_Throwable_];

Goal "tprg\<turnstile>Ext \<preceq>C Base";
b y rtac subcls_direct 1;
b y  simp_tac (simpset()addsimps[ExtCl_def]) 1;
b y Simp_tac 1;
qed "Ext_subcls_Base"; 
Addsimps [Ext_subcls_Base];

AddSIs (map (rewrite_rule [id_def]) wt.intrs); (* wt.Skip,wt.Init already in claset *)


Goalw [ws_cdecl_def] "ws_cdecl tprg Object any";
b y Auto_tac;
qed "ws_cdecl_Object";

Goalw [ws_cdecl_def] "ws_cdecl tprg (SXcpt Throwable) Object";
b y Auto_tac;
qed "ws_cdecl_Throwable";

Goalw [ws_cdecl_def] "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)";
b y Auto_tac;
qed "ws_cdecl_SXcpt";

Goalw [ws_cdecl_def] "ws_cdecl tprg Base Object";
b y Auto_tac;
qed "ws_cdecl_Base";

Goalw [ws_cdecl_def] "ws_cdecl tprg Ext Base";
b y Auto_tac;
qed "ws_cdecl_Ext";
AddSIs[ws_cdecl_Object,ws_cdecl_Throwable,ws_cdecl_SXcpt,ws_cdecl_Base, 
	ws_cdecl_Ext];

Goal "G=tprg \<Longrightarrow> (\<forall>(C,(sc,cb))\<in>set classes. ws_cdecl G C sc)";
b y simp_tac (simpset() addsimps [classes_def,BaseCl_def,ExtCl_def]) 1;
b y auto_tac (claset(),simpset() addsimps 
				[standard_classes_def,ObjectC_def,SXcptC_def]);
qed "ws_cdecl_all";

Goalw [ws_prog_def] "ws_prog tprg";
b y auto_tac (claset() addSIs[ws_cdecl_all], simpset());
qed "ws_tprg";

Goal "wf_prog G \<Longrightarrow> fields G Object = []";
b y (rtac fields_emptyI THEN_ALL_NEW Force_tac) 1;

val fields_tac = rtac (ws_tprg RS fields_emptyI) THEN' REPEAT o Force_tac;
Goal "fields tprg Object = []";
b y fields_tac 1;
qed "fields_Object_";
Addsimps [fields_Object_];
Goal "fields tprg (SXcpt Throwable) = []";
b y fields_tac 1;
qed "fields_Throwable_";
Addsimps [fields_Throwable_];
Goal "fields tprg (SXcpt xn) = []";
b y case_tac "xn = Throwable" 1;
b y  Asm_simp_tac 1;
b y fields_tac 1;
qed "fields_SXcpt_";
Addsimps [fields_SXcpt_];

val fields_rec_ = ws_tprg RSN (2, fields_rec);

Goal "fields tprg Base = [((vee, Base), (False,PrimT Boolean))]";
b y stac fields_rec_ 1;
b y   auto_tac (claset(),simpset()addsimps[BaseCl_def]);
qed "fields_Base";
Addsimps [fields_Base];
Goal "fields tprg Ext  = [((vee, Ext ), (False,PrimT Integer))] @\
                                    \ fields tprg Base";
b y rtac trans 1;
b y rtac fields_rec_ 1;
b y   auto_tac (claset(),simpset()addsimps[ExtCl_def]);
qed "fields_Ext";
Addsimps [fields_Ext];

val cmethd_rec_ = ws_tprg RSN (2, cmethd_rec);

Goal "cmethd tprg Object = table_of []";
b y stac cmethd_rec_ 1;
b y  Simp_tac 2;
b y  Simp_tac 1;
b y  Fast_tac 1;
b y  Simp_tac 1;
b y  Auto_tac;
qed "cmethd_Object_";
Addsimps [cmethd_Object_];
Goal "cmethd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]";
b y rtac trans 1;
b y rtac cmethd_rec_ 1;
b y   auto_tac (claset(),simpset()addsimps[BaseCl_def]);
qed "cmethd_Base";
Addsimps [cmethd_Base];

Goal "cmethd tprg Ext = (cmethd tprg Base \<oplus> \
\ table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo])";
b y rtac trans 1;
b y rtac cmethd_rec_ 1;
b y   auto_tac (claset(),simpset()addsimps[ExtCl_def]);
qed "cmethd_Ext";
Addsimps [cmethd_Ext];


Goalw [Base_foo_def] "wf_mdecl tprg Base Base_foo";
b y rtac wf_mdeclI 1;
b y Auto_tac;
qed "wf_Base_foo";
Goalw [Ext_foo_def] "wf_mdecl tprg Ext Ext_foo";
b y rtac wf_mdeclI 1;
b y Auto_tac;
b y  rtac wt.Cast 1;
b y    Simp_tac 2;
b y   rtac (narrow.subcls RS cast.narrow) 2;
b y   rewtac cfield_def;
b y   Auto_tac;
qed "wf_Ext_foo";

Goalw [wf_cdecl_def, BaseCl_def] "wf_cdecl tprg (Base,BaseCl)";
b y auto_tac (claset()addSIs[wf_Base_foo],simpset());
qed "wf_BaseC";
Goalw [wf_cdecl_def, ExtCl_def] "wf_cdecl tprg (Ext,ExtCl)";
b y auto_tac (claset()addSIs[wf_Ext_foo],simpset());
b y force_tac (claset() addDs [get_in_set], 
	       simpset()addsimps[Base_foo_def,Ext_foo_def,hiding_entails_def])1;
qed "wf_ExtC";


Goalw [wf_prog_def,Let_def] "wf_prog tprg";
b y Simp_tac 1;
b y rtac conjI 1;
b y  (simp_tac (simpset()addsimps[classes_def,standard_classes_def]) 1);
b y rtac conjI 1;
b y  cut_facts_tac [xn_cases] 1;
b y  (asm_simp_tac (simpset()addsimps[classes_def,standard_classes_def]) 1);
b y rtac conjI 1;
b y  rtac unique_classes 2;
b y subgoal_tac "\<forall>p. p=tprg \<longrightarrow> Ball (set classes) (wf_cdecl p)" 1;
b y  Fast_tac 1;
b y strip_tac 1;
b y simp_tac (simpset() addsimps [classes_def]) 1;
b y Asm_simp_tac 1;
b y   rtac (wf_BaseC RS conjI) 1;
b y  rtac (wf_ExtC RS conjI) 1;
b y auto_tac (claset(),simpset() addsimps [standard_classes_def,Let_def]);
qed "wf_tprg";

Goalw [appl_methds_def] 
"appl_methds tprg (ClassT Base) (foo, [NT]) = \
\ {((ClassT Base, fst (snd (Base_foo))), [Class Base])}";
b y Simp_tac 1;
b y subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base" 1;
b y  rewtac cmheads_def;
b y  auto_tac (claset(),simpset() addsimps [Base_foo_def]);
qed "appl_methds_Base_foo";

Goalw [max_spec_def] "max_spec tprg (ClassT Base) (foo, [NT]) = \
\ {((ClassT Base, fst (snd Base_foo)), [Class Base])}";
b y simp_tac (simpset() addsimps [appl_methds_Base_foo]) 1;
b y Auto_tac;
qed "max_spec_Base_foo";

fun t thm = resolve_tac (wt_Call::wt.intrs) 1 thm;
Goal "(tprg, empty(EName e\<mapsto>Class Base))\<turnstile>\
\ Expr(e:==NewC Ext);; \
\ Try Expr({ClassT Base,ClassT Base,IntVir}!!e..foo({?pTs'}[Lit Null])) Catch((SXcpt NullPointer) z) (Throw (!!z))\<Colon>\<surd>";
(* ?pTs' = [Class Base] *)
b y t;		(* ;; *)
b y  t;		(* Expr *)
b y  t;		(* Ass *)
b y     t;	(* LVar *)
b y      Simp_tac 1;
b y     Simp_tac 1;
b y    Simp_tac 1;
b y   t;	(* NewC *)
b y   Simp_tac 1;
b y  Simp_tac 1;
b y t;		(* Try *)
b y    t;	(* Expr *)
b y    t;	(* Call *)
b y       t;	(* Acc *)
b y       t;	(* LVar *)
b y        Simp_tac 1;
b y       Simp_tac 1;
b y      t;	(* Cons *)
b y       t;	(* Lit *)
b y       Simp_tac 1;
b y      t;	(* Nil *)
b y     Simp_tac 1;
b y     rtac (simplify (simpset() addsimps [Base_foo_def]) max_spec_Base_foo) 1;
b y    Simp_tac 1;
b y   Simp_tac 1;
b y  Simp_tac 1;
b y t;		(* Throw *)
b y  t;		(* Acc *)
b y  t;		(* LVar *)
b y   Simp_tac 1;
b y  Simp_tac 1;
b y Simp_tac 1;
qed "wt_test";

val eval_Is = eval_Init :: XcptIs @ map (
 simplify (simpset() addsimps [lvar_def]) o 
 rewrite_rule [assign_def,Let_def]) eval.intrs;
fun e thm = resolve_tac eval_Is 1 thm;


Addsimps[fvar_def2, avar_def2, init_lvars_def2];
Addsimps[init_obj_def, var_tys_def, fields_table_def];
Addsimps[BaseCl_def, ExtCl_def, Base_foo_def, Ext_foo_def];
Goalw [test_def] 
"\<lbrakk>new_Addr (heap (snd (s0::state))) = Some a; \
\ new_Addr (heap     (?s1::st))     = Some b; enough_mem\<rbrakk> \<Longrightarrow> \
\ tprg\<turnstile>s0' \<midarrow>test\<rightarrow> ?s";
(* ?s = s7 *)
b y e;		(* ;; *)
b y  e;		(* Expr *)
b y  e;		(* Ass *)
b y   e;	(* LVar *)
b y  e;		(* NewC *)
b y   e;	(* Init *)
b y   Simp_tac 1;
b y   EVERY[rtac conjI 1, rtac (refl RS (refl RS conjI)) 2];
b y   e;	(* Init *)
b y   Simp_tac 1;
b y   EVERY[rtac conjI 1, rtac (refl RS (refl RS conjI)) 2];
b y   e;	(* Init *)
b y   Simp_tac 1;
b y   EVERY[rtac conjI 1, rtac (refl RS (refl RS conjI)) 2];
b y   Simp_tac 1;
b y  Simp_tac 1;
b y  EVERY'[rtac halloc.New, Asm_full_simp_tac, datac enough_memD 1] 1;
b y  Force_tac 1;
b y etac thin_rl 1;
b y Full_simp_tac 1;
b y e;		(* Try *)
b y   e;	(* Expr *)
b y   e;	(* Call *)
b y      e;	(* Acc *)
b y      e;	(* LVar *)
b y     e;	(* Cons *)
b y      e;	(* Lit *)
b y     e;	(* Nil *)
b y    Simp_tac 1;
b y   Simp_tac 1;
b y   e;     (* Methd *)
b y   simp_tac (simpset() addsimps [body_def,Let_def]) 1;
b y   e;     (* Body *)
b y     EVERY'[rtac init_done, Simp_tac] 1;
b y    e;	(* Expr *)
b y    e;	(* Ass *)
b y     e; (* FVar *)
b y       EVERY'[rtac init_done, Simp_tac] 1;
b y      e;(* Cast *)
b y       e;(* Acc *)
b y       e;(* LVar *)
b y      Simp_tac 1;
b y     simp_tac(simpset() delsplits [split_if]) 1;
b y     EVERY'[rtac (refl RS conjI), rtac (refl RS conjI), rtac refl] 1;
b y    e;	(* XcptE *)
b y   Simp_tac 1;
b y   fast_tac (HOL_cs addSIs XcptIs) 1;
b y  Simp_tac 1;
b y  resolve_tac sxalloc.intrs 1;
b y  EVERY'[rtac halloc.New, Asm_full_simp_tac, datac enough_memD 1] 1;
b y  Force_tac 1;
b y simp_tac (simpset()addsimps[gupd_def,lupd_def,obj_ty_def]
			delsplits [split_if]) 1;
b y e;	(* Throw *)
b y e;	(* Acc *)
b y e;	(* LVar *)
bind_thm ("exec_test", simplify (simpset()addsimps[throw_def]) (result()));