src/HOL/MicroJava/J/Example.ML

added type annotation to Call

Addsimps [inj_cnam_, inj_vnam_];
Addsimps [Base_not_Object,Ext_not_Object];
Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];

bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps")));
Goal "map_of ((aa,bb)#ps) aa = Some bb";
by (Simp_tac 1);
qed "map_of_Cons1";
Goal "aa\\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa";
by (Asm_simp_tac 1);
qed "map_of_Cons2";
Delsimps[map_of_Cons]; (* sic! *)
Addsimps[map_of_Cons1, map_of_Cons2];

Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
by (Simp_tac 1);
qed "class_tprg_Object";

Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Base = Some (Object, \
	\ [(vee, PrimT Boolean)], \
        \ [((foo, [Class Base]), Class Base, foo_Base)])";
by (Simp_tac 1);
qed "class_tprg_Base";

Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Ext = Some (Base, \
	\ [(vee, PrimT Integer)], \
        \ [((foo, [Class Base]), Class Ext, foo_Ext)])";
by (Simp_tac 1);
qed "class_tprg_Ext";

Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];

Goal "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
qed "not_Object_subcls";
AddSEs [not_Object_subcls];

Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
be rtrancl_induct 1;
by  Auto_tac;
bd subcls1D 1;
by Auto_tac;
qed "subcls_ObjectD";
AddSDs[subcls_ObjectD];

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

Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
by (auto_tac (claset(),simpset()addsplits[split_if_asm]addsimps[map_of_Cons]));
qed "class_tprgD";

Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
by (ftac class_tprgD 1);
by (auto_tac (claset() addSDs [],simpset()));
bd rtranclD 1;
by Auto_tac;
qed "not_class_subcls_class";
AddSEs [not_class_subcls_class];

goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg";
by (Simp_tac 1);
qed "unique_classes";

bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);

Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
br subcls_direct 1;
by Auto_tac;
qed "Ext_subcls_Base";
Addsimps [Ext_subcls_Base];

Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
br widen.subcls 1;
by (Simp_tac 1);
qed "Ext_widen_Base";
Addsimps [Ext_widen_Base];

AddSIs ty_expr_ty_exprs_wt_stmt.intrs;


Goal "acyclic (subcls1 tprg)";
br acyclicI 1;
by Safe_tac ;
qed "acyclic_subcls1_";

val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);


val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);

Goal "fields (tprg, Object) = []";
by (stac fields_rec_ 1);
by   Auto_tac;
qed "fields_Object";
Addsimps [fields_Object];

Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
by (stac fields_rec_ 1);
by   Auto_tac;
qed "fields_Base";
Addsimps [fields_Base];

Goal "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @\
                                    \ fields (tprg, Base)";
br trans 1;
br  fields_rec_ 1;
by   Auto_tac;
qed "fields_Ext";
Addsimps [fields_Ext];

val method_rec_ = wf_subcls1_ RS method_rec_lemma;

Goal "method (tprg,Object) = map_of []";
by (stac method_rec_ 1);
by  Auto_tac;
qed "method_Object";
Addsimps [method_Object];

Goal "method (tprg, Base) = map_of \
\ [((foo, [Class Base]), Base, (Class Base, foo_Base))]";
br trans 1;
br  method_rec_ 1;
by  Auto_tac;
qed "method_Base";
Addsimps [method_Base];

Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \
\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
br trans 1;
br  method_rec_ 1;
by  Auto_tac;
qed "method_Ext";
Addsimps [method_Ext];

Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def] 
"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))";
by Auto_tac;
qed "wf_foo_Base";

Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def] 
"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))";
by Auto_tac;
br  ty_expr_ty_exprs_wt_stmt.Cast 1;
by   (Simp_tac 2);
br   cast.subcls 2;
by   (rewtac field_def);
by   Auto_tac;
qed "wf_foo_Ext";

Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def] 
"wf_cdecl wf_java_mdecl tprg ObjectC";
by (Simp_tac 1);
qed "wf_ObjectC";

Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def] 
"wf_cdecl wf_java_mdecl tprg BaseC";
by (Simp_tac 1);
by (fold_goals_tac [BaseC_def]);
br (wf_foo_Base RS conjI) 1;
by Auto_tac;
qed "wf_BaseC";

Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def] 
"wf_cdecl wf_java_mdecl tprg ExtC";
by (Simp_tac 1);
by (fold_goals_tac [ExtC_def]);
br (wf_foo_Ext RS conjI) 1;
by Auto_tac;
bd rtranclD 1;
by Auto_tac;
qed "wf_ExtC";

Goalw [wf_prog_def,Let_def] 
"wf_prog wf_java_mdecl tprg";
by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1);
qed "wf_tprg";

Goalw [appl_methds_def] 
"appl_methds tprg Base (foo, [NT]) = \
\ {((Class Base, Class Base), [Class Base])}";
by (Simp_tac 1);
by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1);
by  (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def]));
qed "appl_methds_foo_Base";

Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \
\ {((Class Base, Class Base), [Class Base])}";
by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base]));
qed "max_spec_foo_Base";

fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
(* ?pTs' = [Class Base] *)
by t;		(* ;; *)
by  t;		(* Expr *)
by  t;		(* LAss *)
by    t;	(* LAcc *)
by     (Simp_tac 1);
by    (Simp_tac 1);
by   t;	(* NewC *)
by   (Simp_tac 1);
by  (Simp_tac 1);
by t;	(* Expr *)
by t;	(* Call *)
by   t;	(* LAcc *)
by    (Simp_tac 1);
by   (Simp_tac 1);
by  t;	(* Cons *)
by   t;	(* Lit *)
by   (Simp_tac 1);
by  t;	(* Nil *)
by (Simp_tac 1);
br max_spec_foo_Base 1;
qed "wt_test";

fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm;

Delsplits[split_if];
Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
Goalw [test_def] 
" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
\ tprg\\<turnstile>s0 -test-> ?s";
(* ?s = s3 *)
by e;		(* ;; *)
by  e;		(* Expr *)
by  e;		(* LAss *)
by   e;	(* NewC *)
by    (Force_tac 1);
by   (Force_tac 1);
by  (Simp_tac 1);
be thin_rl 1;
by e;	(* Expr *)
by e;	(* Call *)
by       e;	(* LAcc *)
by      (Force_tac 1);
by     e;	(* Cons *)
by      e;	(* Lit *)
by     e;	(* Nil *)
by    (Simp_tac 1);
by   (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1);
by  (Simp_tac 1);
by  e;	(* Expr *)
by  e;	(* FAss *)
by       e;(* Cast *)
by        e;(* LAcc *)
by       (Simp_tac 1);
by      (Simp_tac 1);
by     (Simp_tac 1);
by     e;(* XcptE *)
by    (Simp_tac 1);
by   (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq,
             Force_tac] 1);
by  (Simp_tac 1);
by (Simp_tac 1);
by e;	(* XcptE *)
bind_thm ("exec_test", simplify (simpset()) (result()));