src/HOL/MicroJava/J/Example.ML

minor corrections

open Example;

AddIs [widen.null];

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

val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"] 
"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
Delsimps[map_of_Cons]; (* sic! *)
Addsimps[map_of_Cons1, map_of_Cons2];

val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def] 
 	"class tprg Object = Some (None, [], [])" 
	(K [Simp_tac 1]);
val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
 ExtC_def] "class tprg Base = Some (Some Object, \
	\ [(vee, PrimT Boolean)], \
        \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
	Simp_tac 1]);
val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
 ExtC_def] "class tprg Ext = Some (Some Base, \
	\ [(vee, PrimT Integer)], \
        \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
	Simp_tac 1]);
Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];

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

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

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

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

Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> 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);

Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
br subcls_direct 1;
by (Simp_tac 1);
qed "Ext_subcls_Base";
Addsimps [Ext_subcls_Base];

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


Addsimps[is_class_def];

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) \\<oplus> 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\\<Colon>=NewC Ext);; Expr(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] 
" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
\ tprg\\<turnstile>s0 -test\\<rightarrow> ?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()));