File WellForm.ML

open WellForm;


section "wf_fdecl";

qed_goalw "wf_fdecl_def2" thy [wf_fdecl_def] 
	"\<And>fd. wf_fdecl G fd = is_type G (snd (snd fd))" (K [Simp_tac 1]);


section "wf_mdecl";

Goalw [wf_mdecl_def,wf_mhead_def] "\<And>X. \<lbrakk>(C = Object \<longrightarrow> ¬ static m); \
\ length pTs = length pns; \<forall>T\<in>set pTs. is_type G T; is_type G rT; \
\  nodups pns; unique lvars; \
\ (\<forall>pn\<in>set pns. table_of lvars pn = None);\
\ \<forall>(vn,T)\<in>set lvars. is_type G T; \
\ (G, table_of lvars(pns[\<mapsto>]pTs) (+)¬static m ?\<mapsto>Class C)\<turnstile>Body C blk res\<Colon>-T; \
\ G\<turnstile>T\<preceq>rT\<rbrakk> \<Longrightarrow> \
\ wf_mdecl G C ((mn, pTs), (m, pns, rT), lvars, blk, res)";
b y auto_tac (claset(), simpset() delsplits [split_if,split_if_asm]);
qed "wf_mdeclI";

Goalw [wf_mdecl_def] 
"wf_mdecl G C (sig,(m,pns,rT),lvars,blk,res) \<Longrightarrow> \
\wf_mhead G    sig (m,pns,rT) \<and> unique lvars \<and> \
\ (\<forall>pn\<in>set pns. table_of lvars pn = None) \<and> (\<forall>(vn,T)\<in>set lvars. is_type G T)";
b y Auto_tac;
qed "wf_mdeclD1";
Goalw [wf_mdecl_def] 
"wf_mdecl G C (sig,(m,pns,rT),lvars,blk,res) \<Longrightarrow> \
\(\<exists>T. (G,table_of lvars(pns[\<mapsto>](snd sig)) (+)¬ static m ?\<mapsto>Class C)\<turnstile>Body C blk res\<Colon>-T\<and>\
\  G\<turnstile>T\<preceq>rT)";
b y Auto_tac;
qed "wf_mdecl_bodyD";

qed_goalw "static_Object_methodsE" thy [wf_mdecl_def] 
 "\<And>sig. wf_mdecl G Object (sig, (True, pns, T), b) \<Longrightarrow> R" (K [Auto_tac]);
AddSEs [static_Object_methodsE];

qed_goalw "rT_is_type" thy [wf_mhead_def]
	"\<And>sig. wf_mhead G sig (m,pns,rT) \<Longrightarrow> is_type G rT" (K [Auto_tac]);


section "wf_idecl";

qed_goalw "wf_idecl_mhead" thy [wf_idecl_def] 
"\<And>m. \<lbrakk>wf_idecl G (I, is, ms); (s,mh)\<in>set ms\<rbrakk> \<Longrightarrow> \
\ wf_mhead G s mh \<and> ¬static (fst mh)" (K [Auto_tac]);

qed_goalw "wf_idecl_hidings" thy [wf_idecl_def, o_def] 
"\<And>X. wf_idecl G (I, is, ms) \<Longrightarrow> (\<lambda>s. o2s (table_of ms s)) hidings \
\ Un_tables ((\<lambda>J. imethds G J) `` set is) \
\ entails \<lambda>mh (md,mh'). G\<turnstile>mrt mh\<preceq>mrt mh'" (K [Asm_full_simp_tac 1]);

qed_goalw "wf_idecl_supD" thy [wf_idecl_def,ws_idecl_def] 
"\<And>X.\<lbrakk>wf_idecl G (I, is, ms); J \<in> set is\<rbrakk> \<Longrightarrow> is_iface G J \<and> (J, I) \<notin> (subint1 G)^+"
	 (K [Auto_tac]);


section "wf_cdecl";

qed_goalw "wf_cdecl_unique" thy [wf_cdecl_def] 
"\<And>X. wf_cdecl G (C,sc,si,fs,ms,ini) \<Longrightarrow> unique fs \<and> unique ms" (K [Auto_tac]);

qed_goalw "wf_cdecl_fdecl" thy [wf_cdecl_def] 
"\<And>X. \<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); f\<in>set fs\<rbrakk> \<Longrightarrow> wf_fdecl G f"(K[Auto_tac]);

qed_goalw "wf_cdecl_mdecl" thy [wf_cdecl_def] 
"\<And>X. \<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); m\<in>set ms\<rbrakk>\<Longrightarrow>wf_mdecl G C m"(K[Auto_tac]);

qed_goalw "wf_cdecl_impD" thy [wf_cdecl_def] 
"\<And>X. \<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); I\<in>set si\<rbrakk> \<Longrightarrow> is_iface G I \<and> \
\   (\<forall>s. \<forall>(md',mh') \<in> imethds G I s. \
\    (\<exists>(md,(mh,b))\<in>cmethd G C s: G\<turnstile>mrt mh\<preceq>mrt mh' \<and> ¬static (fst mh)))"
 (K [Auto_tac]);

qed_goalw "wf_cdecl_supD" thy [wf_cdecl_def,ws_cdecl_def] 
"\<And>X. \<lbrakk>wf_cdecl G (C,sc,si,fs,ms,ini); C \<noteq> Object\<rbrakk> \<Longrightarrow> \
\ is_class G sc \<and> (sc,C) \<notin> (subcls1 G)^+ \<and> (table_of ms hiding cmethd  G sc \
\ entails (\<lambda>(mh,b) (md',(mh',b')). G\<turnstile>mrt mh\<preceq>mrt mh' \<and> fst mh' = fst mh))"
 (K [Auto_tac]);

qed_goalw "wf_cdecl_wt_init" thy [wf_cdecl_def] 
"\<And>X. wf_cdecl G (C, sco, si, fs, ms, ini) \<Longrightarrow> (G, empty)\<turnstile>ini\<Colon>\<surd>" (K[Auto_tac]);


section "wf_prog";

qed_goalw "wf_prog_idecl" thy [wf_prog_def, Let_def]
 "\<And>X. \<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)" (K [
	Asm_full_simp_tac 1,
	fast_tac (set_cs addDs [get_in_set]) 1]);

qed_goalw "wf_prog_cdecl" thy [wf_prog_def, Let_def]
 "\<And>X. \<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)" (K [
	Asm_full_simp_tac 1,
	fast_tac (set_cs addDs [get_in_set]) 1]);

Goalw [wf_prog_def,Let_def] "wf_prog G \<Longrightarrow> ws_prog G";
b y rtac ws_progI 1;
b y  ALLGOALS Simp_tac;
b y  ALLGOALS (fast_tac (claset() addSDs [wf_idecl_supD,wf_cdecl_supD]));
qed "wf_ws_prog";
AddSEs[wf_ws_prog];
Addsimps[wf_ws_prog];

qed_goalw "class_Object" thy [wf_prog_def, Let_def, ObjectC_def]
"\<And>X. wf_prog G \<Longrightarrow> class G Object = Some (arbitrary,[],[],Object_mdecls,Skip)" 
(K [
	safe_tac set_cs,
	rotate_tac 4 1,
	dtac in_set_get 1,
	 Auto_tac]);
Addsimps [class_Object];

qed_goalw "class_SXcpt" thy [wf_prog_def, Let_def, SXcptC_def]
	"\<And>X. wf_prog G \<Longrightarrow> class G (SXcpt xn) = Some (if xn = Throwable \
\ then Object else SXcpt Throwable, [], [], SXcpt_mdecls, Skip)" (K [
	Safe_tac,
	dtac spec 1,
	rotate_tac 4 1,
	dtac in_set_get 1,
	 Auto_tac]);
Addsimps [class_SXcpt];

qed_goalw "wf_ObjectC" thy [wf_cdecl_def,ws_cdecl_def,ObjectC_def]
	"wf_cdecl G ObjectC = (¬is_iface G Object \<and> Ball (set Object_mdecls) \
\ (wf_mdecl G Object) \<and> unique Object_mdecls)" (K [Simp_tac 1]);
Addsimps [wf_ObjectC];

qed_goalw "wf_SXcptC" thy [wf_cdecl_def,ws_cdecl_def,SXcptC_def, Let_def]
"wf_cdecl G (SXcptC xn) = (¬is_iface G (SXcpt xn) \<and> Ball (set SXcpt_mdecls) \
\ (wf_mdecl G (SXcpt xn)) \<and> unique SXcpt_mdecls \<and>\
\ (let sc = if xn = Throwable then Object else SXcpt Throwable in \
\  is_class G sc \<and> (sc,SXcpt xn)\<notin> (subcls1 G)^+  \<and> \
\ (table_of SXcpt_mdecls hiding cmethd G sc entails \<lambda>(mh,b) (md',mh',b'). \
\  G\<turnstile>snd (snd mh)\<preceq>snd (snd mh') \<and> fst mh' = fst mh)))" (K [Simp_tac 1]);
Addsimps [wf_SXcptC];

qed_goal "Object_is_class" thy "\<And>X. wf_prog G \<Longrightarrow> is_class G Object" (K [
	Asm_simp_tac 1]);
Addsimps [Object_is_class];
AddSEs [Object_is_class];

qed_goal "SXcpt_is_class" thy "\<And>X. wf_prog G \<Longrightarrow> is_class G (SXcpt xn)" (K[
	Asm_simp_tac 1]);
Addsimps [SXcpt_is_class];
AddSEs [SXcpt_is_class];

qed_goal "cmethd_Object" thy "\<And>X. wf_prog G \<Longrightarrow> cmethd G Object = \
\ table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)"
	(K [stac cmethd_rec 1,Auto_tac]);

Goal "wf_prog G \<Longrightarrow> fields G Object = []";
b y (rtac fields_emptyI THEN' REPEAT o Force_tac) 1;
qed "fields_Object";
Addsimps [fields_Object];

qed_goalw "cfield_Object" thy [cfield_def]
 "\<And>X. wf_prog G \<Longrightarrow> cfield G Object = empty" (K [Asm_simp_tac 1]);
Addsimps [cfield_Object];

Goal "wf_prog G \<Longrightarrow> fields G (SXcpt Throwable) = []";
b y (rtac fields_emptyI THEN' REPEAT o Force_tac) 1;
qed "fields_Throwable";
Addsimps [fields_Throwable];

Goal "wf_prog G \<Longrightarrow> fields G (SXcpt xn) = []";
b y case_tac "xn = Throwable" 1;
b y  Asm_simp_tac 1;
b y (rtac fields_emptyI THEN' REPEAT o Force_tac) 1;
qed "fields_SXcpt";
Addsimps [fields_SXcpt];

bind_thm ("widen_trans", wf_ws_prog RSN (3,ws_widen_trans));
qed_goal "widen_trans2" thy "\<And>X. \<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
	(K [eatac widen_trans 2 1]);
AddEs [widen_trans, widen_trans2];

qed_goal "Xcpt_subcls_Throwable" thy 
"\<And>X. wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable" (K [
	rtac SXcpt_subcls_Throwable_lemma 1,
	Auto_tac]);
Addsimps [Xcpt_subcls_Throwable];

Goal "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (fields G C)";
b y etac ws_unique_fields 1;
b y  etac wf_ws_prog 1;
b y Safe_tac;
b y eatac (wf_prog_cdecl RS (wf_cdecl_unique RS conjunct1)) 1 1;
qed "unique_fields";

Goal "\<lbrakk>table_of (fields G C) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog G\<rbrakk>\
\  \<Longrightarrow> table_of (fields G D) fn = Some f";
b y rtac in_set_get 1;
b y  eatac unique_fields 1 1;
b y eatac (get_in_set RS fields_mono_lemma) 1 1;
b y etac wf_ws_prog 1;
qed "fields_mono";

Goal "\<And>m.\<lbrakk>table_of (fields G C) m = Some(f,T); wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> \
\ is_type G T"; 
b y ftac wf_ws_prog 1;
b y force_tac(claset() addDs[fields_defpl RS conjunct1,
	wf_prog_cdecl RS wf_cdecl_fdecl],simpset() addsimps[wf_fdecl_def2]) 1;
qed "fields_is_type";
AddEs [fields_is_type];


Goal "\<lbrakk>(md,mh) \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow> \
\ wf_mhead G sig mh \<and> ¬ static (fst mh)";
b y ftac wf_ws_prog 1;
b y datac (imethds_defpl RS conjunct1) 2 1;
b y Clarify_tac 1;
b y EVERY'[fatac wf_prog_idecl 1, etac wf_idecl_mhead, etac get_in_set] 1;
qed_spec_mp "imethds_wf_mhead";

Goal "\<And>X. \<lbrakk>cmethd G C sig = Some (md,m); wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow> \
\ G\<turnstile>C\<preceq>C md \<and> is_class G md \<and> wf_mdecl G md (sig,m)";
b y ftac wf_ws_prog 1;
b y datac cmethd_defpl 1 1;
b y  Fast_tac 1;
b y Clarsimp_tac 1;
b y EVERY'[fatac wf_prog_cdecl 1, etac wf_cdecl_mdecl, etac get_in_set] 1;
qed "cmethd_wf_mdecl";

val cmethd_rT_is_type = cmethd_wf_mdecl RS conjunct2 RS conjunct2 RS 
		(wf_mdeclD1 RS conjunct1) RS rT_is_type;


(* local lemma *)
Goal  "\<And>sig. \<lbrakk>G\<turnstile>C\<preceq>C C'; is_class G C'; wf_prog G\<rbrakk> \<Longrightarrow> \
\ \<forall>(md ,(m ,pns ,rT ),mb )\<in>cmethd G C' sig: \
\ \<exists>(md',(m',pns',rT'),mb')\<in>cmethd G C  sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT";
b y etac converse_rtrancl_induct 1;
b y  Clarsimp_tac 1;
b y dtac subcls1D 1;
b y Clarsimp_tac 1;
b y EVERY'[stac cmethd_rec, atac, etac wf_ws_prog] 1;
b y rewtac override_def;
b y Clarsimp_tac 1;
b y datac (wf_prog_cdecl RS wf_cdecl_supD) 2 1;
b y Clarsimp_tac 1;
b y datac hiding_entailsD 2 1;
b y Clarsimp_tac 1;
b y Fast_tac 1;
bind_thm ("subcls_methd", result() RS ospec);

(* local lemma *)
Goal "\<And>X. \<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow> \
\ \<forall>(md, m ,pns ,rT ) \<in> imethds G J sig. \
\ \<exists>(md',m',pns',rT') \<in> imethds G I sig. static m'=static m \<and> G\<turnstile>rT'\<preceq>rT";
b y etac converse_rtrancl_induct 1;
b y  clarsimp_tac (claset()addSEs[permute_prems 0 1 bexI], simpset()) 1;
b y dtac subint1D 1;
b y Clarify_tac 1;
b y etac (permute_prems 1 1 ballE) 1;
b y  contr_tac 1;
b y thin_tac "?x \<in> imethds G J sig" 1;
b y Clarsimp_tac 1;
b y EVERY'[stac imethds_rec, atac, etac wf_ws_prog] 1;
b y rewtac overrides_def;
b y datac wf_prog_idecl 1 1;
b y auto_tac (claset()addSIs[table_of_map_SomeI,permute_prems 0 1 bexI] 
       addDs[wf_idecl_mhead,
	     (wf_idecl_supD RS conjunct1) RSN (3,imethds_wf_mhead)],simpset());
b y auto_tac (claset() addSDs [wf_idecl_hidings RS hidings_entailsD],simpset());
qed "subint_widen_imethds";

(* local lemma *)
Goal "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; (md, m, pn, rT) \<in> imethds G I sig\<rbrakk> \<Longrightarrow> \
\ \<exists>(md',(m',pn',rT'),mb)\<in>cmethd G C sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT";
b y dtac implmt1D 1;
b y Clarify_tac 1;
b y datac (wf_prog_cdecl RS wf_cdecl_impD) 2 1;
b y EVERY'[fatac imethds_wf_mhead 1, Asm_simp_tac] 1;
b y Force_tac 1;
qed "implmt1_methd";

(* local lemma *)
Goal "\<And>X. \<lbrakk>wf_prog G; G\<turnstile>T''\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow> \
\(\<forall>(md, (m ,pn ,rT ))    \<in>imethds G I   sig. \
\ \<exists>(md',(m',pn',rT'),mb')\<in>cmethd  G T'' sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT)";
b y ftac implmt_is_class 1;
b y etac implmt.induct 1;
b y   Safe_tac;
b y   force_tac (claset() addSDs [implmt1_methd],simpset()) 1;
b y  EVERY'[datac subint_widen_imethds 1, Asm_simp_tac] 1;
b y  datac bspec 1 1;
b y  Clarify_tac 1;
b y  datac implmt1_methd 2 1;
b y  Force_tac 1;
b y ftac subcls1D 1;
b y datac bspec 1 1;
b y force_tac (claset() addSDs [implmt_is_class,r_into_rtrancl RS subcls_methd,
	implmt1_methd],simpset()) 1;
qed_spec_mp "implmt_methd";

Goal "(md,mh) \<in> mheads G t sig \<longrightarrow> (\<exists>C D b. t = ClassT C \<and> md = ClassT D \<and> cmethd G C sig = Some (D, mh, b)) \<or> (\<exists>I. t = IfaceT I \<and> (\<exists>I'. (I',mh) \<in> imethds G I sig) \<or> (\<exists>D b. cmethd G Object sig = Some (D, mh, b))) \<or> (\<exists>T D b. t = ArrayT T \<and> cmethd G Object sig = Some (D, mh, b))";
b y rtac (ref_ty_ty.induct RS conjunct1) 1;
b y      auto_tac (claset(), simpset() addsimps [cmheads_def]);
qed_spec_mp "mheadsD";

Goal "\<And>sig mh. \
\\<lbrakk>(md , m ,pn, rT )\<in>mheads G t sig; wf_prog G; class G C = Some y; \
\  if (\<exists>T. t=ArrayT T) then C=Object else G\<turnstile>Class C\<preceq>RefT t; isrtype G t\<rbrakk> \<Longrightarrow> \
\ \<exists>(md',(m',pn',rT'),mb)\<in>cmethd G C sig: static m'=static m \<and> G\<turnstile>rT'\<preceq>rT";
b y dtac mheadsD 1;
b y Safe_tac;
b y    ALLGOALS Clarsimp_tac;
b y   force_tac (claset() addSDs [subcls_methd] delrules [bexI],simpset()) 1;
b y  EVERY'[datac implmt_methd 1, Asm_simp_tac, datac bspec 1, Clarsimp_tac] 1;
b y dtac (permute_prems 0 ~1 subcls_methd) 1;
b y auto_tac (claset() addSIs[subcls_ObjectI], simpset());
qed "class_mheadsD";

Goalw [empty_dt_def] "\<And>G. \<lbrakk>(G,L),dt\<Turnstile>v\<Colon>T\<rbrakk> \<Longrightarrow> wf_prog G \<longrightarrow> dt=empty_dt \<longrightarrow> \
\ (case T of Inl T \<Rightarrow> is_type G T | Inr Ts \<Rightarrow> Ball (set Ts) (is_type G))";
b y pair_tac "G" 1;
b y etac wt.induct 1;
b y auto_tac (claset(), simpset() delsplits [split_if_asm] delsimps[snd_conv]);
b y    etac typeof_empty_is_type 1;
b y   EVERY' [fatac (wf_prog_cdecl RS wf_cdecl_supD) 1, rotate_tac ~1, 
	force_tac (claset(), simpset() delsimps[snd_conv]), Clarsimp_tac] 1;
b y  dtac (max_spec2mheads RS conjunct1 RS mheadsD) 1;
b y  dtac cfield_fields 2;
b y  auto_tac (claset() addEs [cmethd_rT_is_type, 
		imethds_wf_mhead RS conjunct1 RS rT_is_type], 
		simpset()delsimps[fst_conv,snd_conv]);
qed "wt_is_type";
qed_goal "ty_expr_is_type" thy 
"\<And>X. \<lbrakk>(G, L)\<turnstile>e\<Colon>-T; wf_prog G\<rbrakk> \<Longrightarrow> is_type G T" 
 (K [dtac wt_is_type 1,Auto_tac]);
qed_goal "ty_var_is_type" thy 
"\<And>X. \<lbrakk>(G, L)\<turnstile>v\<Colon>=T; wf_prog G\<rbrakk> \<Longrightarrow> is_type G T"
 (K [dtac wt_is_type 1,Auto_tac]);
qed_goal "ty_exprs_is_type" thy 
"\<And>X. \<lbrakk>(G, L)\<turnstile>es\<Colon>\<doteq>Ts; wf_prog G\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type G)" 
 (K [dtac wt_is_type 1,Auto_tac]);

Goal "\<lbrakk>(cT, m, pns, rT) \<in> mheads G t sig; wf_prog G; (G, L)\<turnstile>e\<Colon>-RefT t; \
\      m \<or> e = Super\<rbrakk> \<Longrightarrow> \<exists>C D b. t = ClassT C \<and> cT = ClassT D \<and> \
\      cmethd G C sig = Some (D, (m, pns, rT), b)";
b y fatac ty_expr_is_type 1 1;
b y case_tac "m" 1;
b y  force_tac (claset() addSDs [mheadsD,imethds_wf_mhead, cmethd_wf_mdecl],simpset()) 1;
b y EVERY'[Clarsimp_tac, eresolve_tac wt_elim_cases] 1;
b y auto_tac (claset(), simpset() addsimps [cmheads_def]);
qed "static_mheadsD";

Goal "\<lbrakk>cmethd G C sig = Some (md, (m, pns, rT), lvars, blk, res); wf_prog G; \
\ class G C = Some y\<rbrakk> \<Longrightarrow> \
\\<exists>T. (G, table_of lvars(pns[\<mapsto>]snd sig) (+)¬m ?\<mapsto>Class md)\<turnstile>Methd C sig\<Colon>-T \<and>\
\ G\<turnstile>T\<preceq>rT";
b y EVERY'[fatac cmethd_wf_mdecl 2, Clarify_tac] 1;
b y force_tac (claset() addSDs [wf_mdecl_bodyD] addSIs [wt.Methd], simpset()) 1;
qed "wt_MethdI";