File Decl.ML

open Decl;


section "standard exception classes";

qed_goalw "ObjectC_neq_SXcptC" thy [ObjectC_def, SXcptC_def] 
"ObjectC \<noteq> SXcptC xn" (K [Simp_tac 1]);

qed_goalw "SXcptC_inject" thy [SXcptC_def] 
"(SXcptC xn = SXcptC xm) = (xn = xm)" (K [Auto_tac]);

Addsimps [ObjectC_neq_SXcptC,SXcptC_inject];


section "is_type";

qed_goal "type_is_iface" thy 
"\<And>X. is_type G (Iface I) \<Longrightarrow> is_iface G I" (K [Auto_tac]);
qed_goal "type_is_class" thy 
"\<And>X. is_type G (Class C) \<Longrightarrow> is_class G C" (K [Auto_tac]);


section "well-structuredness";

Goalw [ws_prog_def,ws_idecl_def,ws_cdecl_def] 
"\<lbrakk>\<forall>(I,si,ib)\<in>set (fst G). \<forall>J\<in>set si.   is_iface G J \<and> (J,I) \<notin> (subint1 G)^+;\
\ \<forall>(C,D ,cb)\<in>set (snd G). C\<noteq>Object \<longrightarrow> is_class G D \<and> (D,C) \<notin> (subcls1 G)^+ \
\\<rbrakk> \<Longrightarrow> ws_prog G";
b y eatac conjI 1 1;
qed "ws_progI";

Goalw [ws_prog_def, ws_idecl_def] 
"\<lbrakk>iface G I = Some (si,ib); J\<in>set si; ws_prog G\<rbrakk> \<Longrightarrow> \
\ is_iface G J \<and> (J,I)\<notin>(subint1 G)^+";
b y Clarify_tac 1;
b y datac (get_in_set RSN (2,bspec)) 1 1;
b y Clarsimp_tac 1;
qed "ws_prog_ideclD";
Goalw [ws_prog_def, ws_cdecl_def] 
"\<lbrakk>class G C = Some(sc,cb); C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow> \
\ is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+";
b y Clarify_tac 1;
b y datac (get_in_set RSN (2,bspec)) 1 1;
b y Clarsimp_tac 1;
qed "ws_prog_cdeclD";


section "subinterface and subclass relations";

qed_goalw "subint1I" thy [subint1_def] 
"\<And>G. \<lbrakk>iface G I = Some (si,ms); J \<in> set si\<rbrakk> \<Longrightarrow> (I,J) \<in> subint1 G" 
	(K [Auto_tac]);

qed_goalw "subcls1I"  thy [subcls1_def] 
"\<And>G. \<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,D) \<in> subcls1 G"
	 (K [Auto_tac]);

qed_goalw "subint1D" thy [subint1_def] 
  "\<And>G. (I,J)\<in>subint1 G\<Longrightarrow> \<exists>(si,ms)\<in>iface G I: J\<in>set si" (K [Auto_tac]);
qed_goalw "subcls1D" thy [subcls1_def] 
  "\<And>G. (C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>cb. class G C = Some (D,cb))" 
(K [Auto_tac]);

Goalw [subint1_def,dom_def] 
 "subint1 G = (\<Sigma> I\<in>dom (\<lambda>I. iface G I). set (fst (the (iface G I))))";
b y Auto_tac;
qed "subint1_def2";
Goalw [subcls1_def,dom_def] 
"subcls1 G = (\<Sigma>C\<in>dom (\<lambda>C. class G C). {D. C\<noteq>Object \<and> fst(the(class G C))=D})";
b y Auto_tac;
qed "subcls1_def2";


section "well-foundedness";

Goal "finite (subint1 G)";
b y stac subint1_def2 1;
b y rtac finite_SigmaI 1;
b y  rtac finite_dom_map_of 1;
b y Simp_tac 1;
qed "finite_subint1";
Goal "finite (subcls1 G)";
b y stac subcls1_def2 1;
b y rtac finite_SigmaI 1;
b y  rtac finite_dom_map_of 1;
b y res_inst_tac [("B","{fst (the (class G C))}")] finite_subset 1;
b y  Auto_tac;
qed "finite_subcls1";

Goal "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}";
b y force_tac (claset()addDs[subint1D,ws_prog_ideclD RS conjunct2],simpset()) 1;
qed "subint1_irrefl_lemma1";
Goal "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}";
b y force_tac (claset()addDs[subcls1D,ws_prog_cdeclD RS conjunct2],simpset()) 1;
qed "subcls1_irrefl_lemma1";

qed_goal "irrefl_tranclI'" Trancl.thy 
  "!!r. r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+" (K [
	rtac allI 1, etac irrefl_tranclI 1]);

val subint1_irrefl_lemma2 = subint1_irrefl_lemma1 RS irrefl_tranclI';
val subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 RS irrefl_tranclI';

bind_thm ("subint1_irrefl",
	   permute_prems 0 1 (subint1_irrefl_lemma2 RS irrefl_trancl_rD));
bind_thm ("subcls1_irrefl",
           permute_prems 0 1 (subcls1_irrefl_lemma2 RS irrefl_trancl_rD));

bind_thm ("subint1_acyclic", subint1_irrefl_lemma2 RS acyclicI);
bind_thm ("subcls1_acyclic", subcls1_irrefl_lemma2 RS acyclicI);

bind_thm ("wf_subint1", 
	   subint1_acyclic RS(finite_subint1 RS finite_acyclic_wf_converse));
bind_thm ("wf_subcls1", 
	   subcls1_acyclic RS(finite_subcls1 RS finite_acyclic_wf_converse));

bind_thm ("subint1_induct",full_simplify (simpset()) (wf_subint1 RS wf_induct));
bind_thm ("subcls1_induct",full_simplify (simpset()) (wf_subcls1 RS wf_induct));

(* unused *)
Goal  "ws_prog G \<Longrightarrow> wf (((subint1 G)^+)^-1)";
b y etac (wf_subint1 RS wf_converse_trancl) 1;
qed "wf_subint_";
Goal "ws_prog G \<Longrightarrow> wf (((subcls1 G)^+)^-1)";
b y etac (wf_subcls1 RS wf_converse_trancl) 1;
qed "wf_subcls_";

Goal "\<lbrakk>is_iface G I; ws_prog G;\
\ \<And>I is ms. \<lbrakk>iface G I = Some (is, ms) \<and>\
\  (\<forall>J \<in> set is. (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I\<rbrakk> \<Longrightarrow> P I"; 
b y cut_facts_tac (premises()) 1; (* sic! *)
b y make_imp_tac 1;
b y rtac subint1_induct 1;
b y  atac 1;
b y Safe_tac;
b y resolve_tac (premises()) 1;
b y rtac conjI 1;
b y  atac 1;
b y rtac ballI 1;
b y fatac subint1I 1 1;
b y datac ws_prog_ideclD 2 1;
b y Fast_tac 1;
qed "ws_subint1_induct";

Goal "\<lbrakk>is_class G C; ws_prog G; \
\ \<And>C D si fs ms ini. \<lbrakk>class G C = Some (D,si,fs,ms,ini) \<and> \
\(C \<noteq> Object \<longrightarrow> (C,D)\<in>subcls1 G \<and> P D \<and> is_class G D)\<rbrakk> \<Longrightarrow> P C \
\     \<rbrakk> \<Longrightarrow> P C"; 
b y cut_facts_tac (premises()) 1; (* sic! *)
b y make_imp_tac 1;
b y rtac subcls1_induct 1;
b y  atac 1;
b y Safe_tac;
b y resolve_tac (premises()) 1;
b y rtac conjI 1;
b y  atac 1;
b y rtac impI 1;
b y fatac subcls1I 1 1;
b y datac ws_prog_cdeclD 2 1;
b y Fast_tac 1;
qed "ws_subcls1_induct";


section "general recursion operators";

Goalw [ws_wfrel_def] "(\<And>G. ws_prog G \<Longrightarrow> wf ((Rf G)^-1)) \<Longrightarrow> wf (ws_wfrel Rf)";
b y res_inst_tac [("f1","id")] (wf_rel_lemma RS wf_subset) 1;
b y force_tac (claset() delrules [splitI2'] addSEs (premises()),simpset()) 1;
qed "ws_wfrel_lemma";

Goal "wf (ws_wfrel subint1)";
b y rtac ws_wfrel_lemma 1;
b y etac wf_subint1 1;
qed "wf_iface_wfrel";
Goal "wf (ws_wfrel subcls1)";
b y rtac ws_wfrel_lemma 1;
b y etac wf_subcls1 1;
qed "wf_class_wfrel";

Goal "\<And>i. \<lbrakk>iface G I = Some (si,ib); ws_prog G\<rbrakk> \<Longrightarrow> \
\ iface_rec (G,I) f = f I ib ((\<lambda>J. iface_rec (G,J) f)``set si)";
b y stac (wf_iface_wfrel RS (hd iface_rec.simps)) 1;
b y auto_tac (claset() addIs [subint1I], simpset() addsimps [ws_wfrel_def]);
qed "iface_rec";
Goal "\<lbrakk>class G C = Some (sc,si,cb); ws_prog G\<rbrakk> \<Longrightarrow> \
\class_rec (G,C) t f = f C cb (if C = Object then t else class_rec (G,sc) t f)";
b y stac (wf_class_wfrel RS (hd class_rec.simps)) 1;
back();
b y auto_tac (claset() addIs [subcls1I], simpset() addsimps [ws_wfrel_def]);
qed "class_rec";


section "imethds";

Goalw [imeths_def] "\<lbrakk>iface G I = Some (is,ms); ws_prog G\<rbrakk> \<Longrightarrow> \
\ imethds G I = Un_tables ((\<lambda>J. imethds  G J)``set is) \<oplus>\<oplus> \
\                         (o2s \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) ms))";
b y eatac (iface_rec RS trans) 1 1;
b y Clarsimp_tac 1;
qed "imethds_rec";

(* local lemma *)
Goal "\<lbrakk>iface G md = Some (is, ms); ws_prog G; table_of ms sig = Some mh\<rbrakk> \<Longrightarrow> \
\ (md, mh) \<in> imethds G md sig";
b y EVERY'[stac imethds_rec, atac, atac] 1;
b y rtac (disjI1 RS (overrides_Some_iff RS iffD2)) 1;
b y auto_tac (claset() addEs [table_of_map_SomeI], simpset());
qed "imethds_norec";

Goal "\<lbrakk>(md,mh) \<in> imethds G I sig; ws_prog G; is_iface G I\<rbrakk> \<Longrightarrow> \
\ (\<exists>is ms. iface G md = Some (is, ms) \<and> table_of ms sig = Some mh) \<and> \
\ (I,md) \<in> (subint1 G)^* \<and> (md,mh) \<in> imethds G md sig";
b y make_imp_tac 1;
b y EVERY'[rtac ws_subint1_induct, atac, atac] 1;
b y EVERY'[stac imethds_rec, etac conjunct1, atac] 1;
b y force_tac (claset() addEs [imethds_norec]addIs[rtrancl_into_rtrancl2], 
		simpset()) 1;
qed "imethds_defpl";


section "cmethd";

Goalw [cmethd_def] "\<lbrakk>class G C = Some (sc,si,fs,ms,ini); ws_prog G\<rbrakk> \<Longrightarrow> \
\ cmethd G C = (if C = Object then empty else cmethd G sc) \<oplus> \
\ table_of (map (\<lambda>(s,m). (s,(C,m))) ms)";
b y eatac (class_rec RS trans) 1 1;
b y Clarsimp_tac 1;
qed "cmethd_rec";

(* local lemma *)
Goal "\<lbrakk>class G md = Some (D, si, fs, ms, ini); ws_prog G; \
\ table_of ms sig = Some m\<rbrakk> \<Longrightarrow> cmethd G md sig = Some (md, m)";
b y EVERY'[stac cmethd_rec, atac, atac] 1;
b y rtac (disjI1 RS (override_Some_iff RS iffD2)) 1;
b y auto_tac (claset() addEs [table_of_map_SomeI], simpset());
qed "cmethd_norec";

Goal "\<And>X. \<lbrakk>cmethd G C sig = Some (md, m); ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> \
\ (\<exists>D si fs ms ini. class G md = Some (D,si,fs,ms,ini) \<and> table_of ms sig = Some m) \<and>\
\ (C,md)\<in>(subcls1 G)^* \<and> cmethd G md sig = Some (md, m)"; 
b y make_imp_tac 1;
b y EVERY'[rtac ws_subcls1_induct, atac, atac] 1;
b y EVERY'[stac cmethd_rec, etac conjunct1, atac] 1;
b y force_tac (claset() addEs [cmethd_norec]addIs[rtrancl_into_rtrancl2], 	
		simpset()) 1;
qed "cmethd_defpl";

(*unused*)
Goal "ws_prog G \<Longrightarrow> finite {cmethd G C sig |sig C. is_class G C}";
b y rtac finite_SetCompr2 1;
b y  fold_goals_tac [dom_def];
b y  rtac finite_dom_map_of 1;
b y strip_tac 1;
b y eatac ws_subcls1_induct 1 1;
b y EVERY'[stac cmethd_rec, etac conjunct1, atac] 1;
b y auto_tac (claset() addSIs [finite_range_map_of] 
			addSEs [finite_range_map_of_override], simpset());
qed "finite_cmethd";

Goal "\<lbrakk>ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> finite (dom (cmethd G C))";
b y eatac ws_subcls1_induct 1 1;
b y EVERY'[stac cmethd_rec, etac conjunct1, atac] 1;
b y auto_tac (claset() addSIs [finite_dom_map_of], simpset());
qed "finite_dom_cmethd";


section "fields";

qed_goalw "fields_rec" thy [fields_def] 
"\<And>X. \<lbrakk>class G C = Some (sc,si,fs,ms,ini); ws_prog G\<rbrakk> \<Longrightarrow> \
\ fields G C = map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
\ (if C = Object then [] else fields G sc)"
	(K [eatac (class_rec RS trans) 1 1, Clarsimp_tac 1]);

(* local lemma *)
Goal "\<lbrakk>class G fd = Some (D, si, fs, ms, ini); ws_prog G; \
\ table_of fs fn = Some f\<rbrakk> \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f";
b y EVERY'[stac fields_rec, atac, atac] 1;
b y stac (map_of_override RS sym) 1;
b y rtac (disjI1 RS (override_Some_iff RS iffD2)) 1;
b y auto_tac (claset() addEs [table_of_map2_SomeI], simpset());
qed "fields_norec";

Goal "\<lbrakk>table_of (fields G C) (fn,fd) = Some f; ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> \
\ (\<exists>D si fs ms ini. class G fd = Some (D,si,fs,ms,ini) \<and> table_of fs fn = Some f) \<and>\
\ (C,fd)\<in>(subcls1 G)^* \<and> table_of (fields G fd) (fn,fd) = Some f";
b y make_imp_tac 1;
b y EVERY'[rtac ws_subcls1_induct, atac, atac] 1;
b y EVERY'[stac fields_rec, etac conjunct1, atac] 1;
b y auto_tac (claset() addEs [fields_norec]addIs[rtrancl_into_rtrancl2],
	simpset()addsimps[map_of_override RS sym]delsimps[map_of_override]);
qed "fields_defpl";

Goal "\<And>y. \<lbrakk>ws_prog G; class G C = Some (sc, is, [], m, c); \
\ C \<noteq> Object \<longrightarrow> class G sc = Some y \<and> fields G sc = []\<rbrakk> \<Longrightarrow> \
\ fields G C = []";
b y stac fields_rec 1;
b y   atac 1;
b y  Auto_tac;
qed "fields_emptyI";

(* easier than with table_of *)
Goal "\<lbrakk> x \<in> set (fields G C); (D,C)\<in>(subcls1 G)^*; ws_prog G\<rbrakk> \<Longrightarrow> x \<in> set (fields G D)";
b y make_imp_tac 1;
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 fields_rec, atac, atac] 1;
b y Auto_tac;
qed "fields_mono_lemma";

Goal "\<lbrakk>((fn, C), f1) \<in> set (fields G D); (fn, f2) \<in> set fs; ws_prog G; \
\ class G C = Some (D, si, fs, m_i); C \<noteq> Object; class G D = Some c\<rbrakk> \<Longrightarrow> R";
b y fatac (ws_prog_cdeclD RS conjunct2) 2 1;
b y dtac weak_in_set_get 1;
b y fatac (subcls1I RS subcls1_irrefl) 2 1;
b y auto_tac (claset() addDs [fields_defpl RS conjunct2 RS conjunct1 RS 
	rtranclD], simpset());
qed "ws_unique_fields_lemma";

Goal "\<lbrakk>is_class G C; ws_prog G;\
\      \<And>C D s fs r. \<lbrakk>class G C = Some (D, s, fs, r)\<rbrakk> \<Longrightarrow> unique fs \<rbrakk> \<Longrightarrow> \
\     unique (fields G C)";
b y cut_facts_tac (premises()) 1;
b y EVERY'[rtac ws_subcls1_induct, atac, atac] 1;
b y EVERY'[stac fields_rec, etac conjunct1, atac] 1;
b y auto_tac (claset() addSIs[unique_map_inj,injI] addSEs [unique_append,
 ws_unique_fields_lemma,hd(tl(tl(premises()))),fields_norec],simpset());
qed "ws_unique_fields";


section "cfield";

qed_goalw "cfield_fields" thy [cfield_def] "\<And>X. \
\ cfield  G C fn = Some (fd, fT) \<Longrightarrow> table_of (fields  G C) (fn, fd) = Some fT"
(K [rtac table_of_remap_SomeD 1, Asm_full_simp_tac 1]);

Goal "\<lbrakk>is_class G C; cfield G C en = Some (fd, b, fT); ws_prog G\<rbrakk> \<Longrightarrow> \
\ is_class G fd";
b y dtac cfield_fields 1;
b y datac (fields_defpl RS conjunct1) 2 1;
b y Clarsimp_tac 1;
qed "cfield_defpl_is_class";


section "is_methd";

Goalw [is_methd_def] 
"\<lbrakk>class G C = Some y; cmethd G C sig = Some b\<rbrakk> \<Longrightarrow> is_methd G C sig";
b y Auto_tac;
qed "is_methdI";

Goalw [is_methd_def] 
"is_methd G C sig \<Longrightarrow> class G C \<noteq> None \<and> cmethd G C sig \<noteq> None";
b y Auto_tac;
qed "is_methdD";

Goalw [is_methd_def] "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))";
b y stac SetCompr_Sigma_eq 1;
b y rtac finite_SigmaI 1;
b y  full_simp_tac (HOL_basic_ss addsimps [mem_Collect_eq]) 2;
b y  fold_goals_tac [dom_def];
b y  rtac finite_dom_map_of 1;
b y eatac finite_dom_cmethd 1 1;
qed "finite_is_methd";