File Example.ML

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_];


section "table_of classes and interfaces";

val classes_def = clsses_def;
val table_classes_defs = 
    [classes_def, standard_classes_def, ObjectC_def, SXcptC_def];

Goalw [ifaces_def] "table_of ifaces = empty(HasFoo\<mapsto>HasFooInt)";
b y Simp_tac 1;
qed "table_ifaces";
Addsimps[table_ifaces];

Goalw table_classes_defs
 "table_of classes Object = Some (arbitrary, [], [], Object_mdecls, Skip)";
b y Simp_tac 1;
qed "table_classes_Object";

Goalw table_classes_defs
  "table_of classes (SXcpt xn) = Some (if xn = Throwable then Object \
\ else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)";
b y (induct_tac "xn" THEN_ALL_NEW Simp_tac) 1;
qed "table_classes_SXcpt"; 

Goalw table_classes_defs
 	"table_of classes HasFoo = None";
b y Simp_tac 1;
qed "table_classes_HasFoo";

Goalw table_classes_defs "table_of classes Base = Some BaseCl";
b y Simp_tac 1;
qed "table_classes_Base";
Goalw table_classes_defs "table_of classes Ext = Some ExtCl";
b y Simp_tac 1; 
qed "table_classes_Ext";

Addsimps [table_classes_Object, table_classes_SXcpt, table_classes_HasFoo,
	  table_classes_Base, table_classes_Ext];


section "well-structuredness";

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 [ws_idecl_def] "ws_idecl tprg HasFoo []";
b y Simp_tac  1;
qed "ws_idecl_HasFoo";

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";

val ws_cdecls = [ws_cdecl_SXcpt, ws_cdecl_Object, ws_cdecl_Throwable,
       ws_cdecl_Base, ws_cdecl_Ext];

Delrules [not_Object_subcls_any,
          not_Throwable_subcls_SXcpt, not_SXcpt_n_subcls_SXcpt_n, 
          not_Base_subcls_Ext, not_TName_n_subcls_TName_n];

Goal "G=tprg \<Longrightarrow> (\<forall>(I,(si,ib))\<in>set ifaces. ws_idecl G I si)";
b y simp_tac (simpset() addsimps [ifaces_def, HasFooInt_def]) 1;
b y auto_tac (claset() addSIs [ws_idecl_HasFoo], simpset());
qed "ws_idecl_all";

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() addSIs ws_cdecls,
            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_idecl_all,ws_cdecl_all], simpset());
qed "ws_tprg";


section "misc program properties (independent of well-structuredness)";

Goalw [ifaces_def] "is_iface tprg I = (I = HasFoo)";
b y Simp_tac 1;
qed "single_iface";

Goalw [subint1_def,ifaces_def,HasFooInt_def] "subint1 tprg = {}";
b y Auto_tac;
qed "empty_subint1";
Addsimps [single_iface, empty_subint1];

Goalw [ifaces_def] "unique ifaces";
b y Simp_tac 1;
qed "unique_ifaces";

Goalw table_classes_defs "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];


section "fields and methods";

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_tprg_Object";
Addsimps [fields_tprg_Object];

Goal "fields tprg (SXcpt Throwable) = []";
b y fields_tac 1;
qed "fields_tprg_Throwable";
Addsimps [fields_tprg_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_tprg_SXcpt";
Addsimps [fields_tprg_SXcpt];

val fields_rec_ = ws_tprg RSN (2, fields_rec);

Goal "fields tprg Base = [((arr, Base), (True,  PrimT Boolean.[])),\
\                         ((vee, Base), (False, Iface HasFoo    ))]";
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 imethds_rec_ = ws_tprg RSN (2, imethds_rec);
val cmethd_rec_  = ws_tprg RSN (2, cmethd_rec);

Goal "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))";
b y rtac trans 1;
b y rtac imethds_rec_ 1;
b y  auto_tac (claset(),simpset()addsimps[HasFooInt_def]);
qed "imethds_HasFoo";
Addsimps [imethds_HasFoo];

Goal "cmethd tprg Object = empty";
b y stac cmethd_rec_ 1;
b y auto_tac (claset(), simpset() addsimps [Object_mdecls_def]);
qed "cmethd_tprg_Object";
Addsimps [cmethd_tprg_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 ++ \
\ 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];


section "well-formedness";

Goalw [wf_idecl_def, HasFooInt_def] "wf_idecl tprg (HasFoo, HasFooInt)";
b y auto_tac (claset()addSIs[wf_mheadI,ws_idecl_HasFoo],
              simpset()addsimps[foo_sig_def,foo_mhead_def]);
qed "wf_HasFoo";

val Base_foo_defs = [Base_foo_def,foo_sig_def,foo_mhead_def];
val Ext_foo_defs  = [Ext_foo_def,foo_sig_def];
Delrules [wt.Skip,wt.Init];
val wtIs = wt_Call::wt_StatRef::map (rewrite_rule [id_def]) wt.intrs;

Goalw Base_foo_defs "wf_mdecl tprg Base Base_foo";
b y auto_tac (claset() addSIs [wf_mdeclI,wf_mheadI] addSIs wtIs, simpset());
qed "wf_Base_foo";

Goalw Ext_foo_defs "wf_mdecl tprg Ext Ext_foo";
b y auto_tac (claset() addSIs [wf_mdeclI,wf_mheadI] addSIs wtIs, simpset());
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 (claset() addSIs wtIs, simpset());
qed "wf_Ext_foo";

Goalw [wf_cdecl_def, BaseCl_def, arr_viewed_from_def] "wf_cdecl tprg (Base,BaseCl)";
b y auto_tac (claset()addSIs[wf_Base_foo],simpset());
b y       auto_tac (claset() addSIs [ws_cdecl_Base],
              simpset()addsimps[Base_foo_def,foo_mhead_def]);
b y auto_tac (claset() addSIs wtIs,simpset()addsimps[cfield_def]);
qed "wf_BaseC";

Goalw [wf_cdecl_def, ExtCl_def] "wf_cdecl tprg (Ext,ExtCl)";
b y auto_tac (claset()addSIs[wf_Ext_foo,ws_cdecl_Ext],simpset());
b y auto_tac (claset() addDs [get_in_set], simpset()addsimps
	        (Base_foo_defs@[Ext_foo_def,hiding_entails_def]));
qed "wf_ExtC";

Goal "p=tprg \<Longrightarrow> Ball (set ifaces) (wf_idecl p)";
b y simp_tac (simpset() addsimps [ifaces_def]) 1;
b y Asm_simp_tac 1;
b y rtac wf_HasFoo 1;
qed "wf_idecl_all";


Goalw [standard_classes_def,Let_def,
       ObjectC_def,SXcptC_def,Object_mdecls_def,SXcpt_mdecls_def] 
"Ball (set standard_classes) (wf_cdecl tprg)";
b y simp_tac (simpset() addsimps (wf_cdecl_def::ws_cdecls)) 1;
qed "wf_cdecl_all_standard_classes";

Goal "p=tprg \<Longrightarrow> Ball (set classes) (wf_cdecl p)";
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 rtac wf_cdecl_all_standard_classes 1;
qed "wf_cdecl_all";

Goalw [wf_prog_def,Let_def] "wf_prog tprg";
b y simp_tac (simpset() addsimps [unique_ifaces, unique_classes]) 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 auto_tac (claset() addSIs [wf_idecl_all, wf_cdecl_all],simpset());
qed "wf_tprg";


section "max_spec";

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

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


section "well-typedness";

fun t thm = resolve_tac wtIs 1 thm;
Goalw [test_def,arr_viewed_from_def] 
      "(tprg, empty(EName e\<mapsto>Class Base))\<turnstile>test ?pTs\<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    Simp_tac 4;
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 max_spec_Base_foo 1;
b y    Simp_tac 1;
b y   Simp_tac 1;
b y  Simp_tac 1;
b y t;		(* While *)
b y  t;		(* Acc *)
b y   t;	(* AVar *)
b y   t;	(* Acc *)
b y   t;	(* FVar *)
b y    t;	(* StatRef *)
b y    Simp_tac 1;
b y   simp_tac (simpset()addsimps[cfield_def]) 1;
b y  t;		(* LVar *)
b y  Simp_tac 1;
b y t;		(* Skip *)
qed "wt_test";

Goal"\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow> \
\ new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n";
b y ftac atleast_free_SucD 1;
b y dtac (atleast_free_Suc RS iffD1) 1;
b y Clarsimp_tac 1;
b y ftac new_Addr_SomeI 1;
b y Force_tac 1;
qed "alloc_one";

Addsimps [fvar_def2, avar_def2, init_lvars_def2];
Addsimps [init_obj_def, var_tys_def, fields_table_def];
Addsimps([BaseCl_def, ExtCl_def, Ext_foo_def] @ Base_foo_defs);

val eval_Is = eval_Init :: eval_StatRef :: 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;
val refl_tac = fast_tac HOL_cs;


Delsimps[Pair_eq];
Goalw [test_def,arr_viewed_from_def] 
"\<lbrakk>the (new_Addr (heap  s1)) = a; \
\ the (new_Addr (heap ?s2)) = b; \
\ the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow> \
\ atleast_free  (heap s0) 4 \<Longrightarrow> \
\ tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'";
(* ?s9' = s9' *)
b y Full_simp_tac 1;
b y EVERY'[datac alloc_one 1, Clarsimp_tac] 1;
b y e;		(* ;; *)
b y  thin_tac "the (new_Addr ?h) = c" 1;
b y  thin_tac "new_Addr ?h = Some a" 2;
b y  thin_tac "atleast_free ?h 4" 2;
b y  e;		(* Expr *)
b y  e;		(* Ass *)
b y   e;	(* LVar *)
b y  e;		(* NewC *)
      (* begin init Ext *)
b y   thin_tac "the (new_Addr ?h) = b" 1;
b y   thin_tac "atleast_free ?h 3" 1;
b y   thin_tac "atleast_free ?h 4" 2;
b y   thin_tac "new_Addr ?h = Some a" 2;
b y   e;	(* Init Ext *)
b y   Simp_tac 1;
b y   EVERY[rtac conjI 1, refl_tac 2];
b y   e;	(* Init Base *)
b y   simp_tac (simpset() addsimps [arr_viewed_from_def]) 1;
b y   rtac conjI 1;
b y    e;	(* Init Object *)
b y    Simp_tac 1;
b y    refl_tac 1;
b y   Simp_tac 1;
b y   EVERY[rtac conjI 1, rtac refl 2];
b y   e;	(* Expr *)
b y   e;	(* Ass *)
b y    e;	(* FVar *)
b y      EVERY'[rtac init_done, Simp_tac] 1;
b y     e;	(* StatRef *)
b y    Simp_tac 1;
b y   e;	(* NewA *)
b y     Simp_tac 1;
b y    e;	(* Lit *)
b y   Simp_tac 1;
b y   rtac halloc.New 1;
b y    Asm_simp_tac 1;
b y   EVERY'[dtac atleast_free_weaken,rotate_tac ~1,dtac atleast_free_weaken] 1;
b y   Asm_simp_tac 1;
b y  simp_tac (simpset() addsimps [upd_gobj_def]) 1;
      (* end init Ext *)
b y  rtac halloc.New 1;
b y   dtac alloc_one 1;
b y    Fast_tac 2;
b y   Asm_simp_tac 1;
b y  dtac atleast_free_weaken 1;
b y  Force_tac 1;
b y Simp_tac 1;
b y dtac alloc_one 1;
b y  Asm_simp_tac 1;
b y Clarsimp_tac 1;
b y thin_tac "atleast_free ?h 3" 1;
b y dres_inst_tac [("x","a")] (new_AddrD2 RS spec) 1;
b y Full_simp_tac 1;
b y e;		(* Try *)
b y   e;	(* Expr *)
      (* begin method call *)
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    e;	(* XcptE *)
b y   Simp_tac 1;
b y   rtac (refl RS conjI) 1;
b y   e; 	(* XcptE *)
b y  Simp_tac 1;
      (* end method call *)
b y  resolve_tac sxalloc.intrs 1;
b y  rtac halloc.New 1;
b y   etac (alloc_one RS conjunct1) 1;
b y   Asm_simp_tac 1;
b y  Asm_simp_tac 1;
b y simp_tac (simpset()addsimps[gupd_def,lupd_def,obj_ty_def]
			delsplits [split_if]) 1;
b y dtac (alloc_one RS conjunct1) 1;
b y  Asm_simp_tac 1;
b y thin_tac "atleast_free ?h 2" 1;
b y dres_inst_tac [("x","a")] (new_AddrD2 RS spec) 1;
b y Asm_full_simp_tac 1;
b y e;		(* While *)
b y  e;		(* Acc *)
b y  e;		(* AVar *)
b y    e;	(* Acc *)
b y    e;	(* FVar *)
b y      EVERY'[rtac init_done, Simp_tac] 1;
b y     e;	(* StatRef *)
b y    Simp_tac 1;
b y   e;	(* Lit *)
b y  Asm_simp_tac 1;
b y auto_tac (HOL_cs, simpset() addsimps [in_bounds_def]);
b y e;   	(* XcptE *)
qed "exec_test";
Addsimps[Pair_eq];