WellForm.ML
Back to theory WellForm
open WellForm;
val wf_fdecl_def2 = prove_goalw thy [wf_fdecl_def]
"!!fd. wf_fdecl G fd = is_type G (snd fd)" (K [Simp_tac 1]);
goalw thy [wf_mdecl_def,Let_def,wf_mhead_def] "!!X. [|is_type G md; is_type G pT;\
\pn ~= This; unique lvars; table_of lvars This = None; table_of lvars pn = None;\
\(!(vn,T):set lvars. is_type G T); E=(G, table_of lvars[This|->Class C][pn|->md]);\
\E|-mb::<>; E|-res::T; G|-T<=:pT|] \
\==> wf_mdecl G C ((mn, md), (pn, pT), lvars, mb, res)";
b y Asm_simp_tac 1;
b y eres_inst_tac [("s","E")] subst 1;
b y Fast_tac 1;
val wf_mdeclI = result();
val wf_mdeclD = prove_goalw thy [wf_mdecl_def, Let_def]
"!!X. wf_mdecl G C ((mn,pT),(pn,rT),lvars,blk,res) ==> \
\ wf_mhead G (mn,pT) (pn,rT) & \
\ unique lvars & table_of lvars This = None & table_of lvars pn = None & \
\ (!(vn,T):set lvars. is_type G T) & \
\ (G,table_of lvars[This|->Class C][pn|->pT])|-blk::<> & \
\ (? T. (G,table_of lvars[This|->Class C][pn|->pT])|-res::T & G|-T<=:rT)"
(K [Auto_tac]);
val wf_idecl_mhead = prove_goalw thy [wf_idecl_def]
"!!s m. [|wf_idecl G (I, is, ms); (s,m):set ms|] ==> wf_mhead G s m" (K [
Asm_full_simp_tac 1, Fast_tac 1]);
val wf_idecl_hidings = prove_goalw thy [wf_idecl_def, o_def]
"!!X. wf_idecl G (I, is, ms) ==> (%s. o2s (table_of ms s)) hidings \
\ Un_tables ((%J. imethds G J) `` set is) \
\ entails %(pn,rT) (md,pn',rT'). G|-rT<=:rT'" (K [Asm_full_simp_tac 1]);
(*
val it = "wf_idecl ?G ==
%(I,is,ms).
Ball (set is) (is_iface G) &
(! J:set is. (J, I) ~: subint G) &
unique ms &
*)
val wf_idecl_supD = prove_goalw thy [wf_idecl_def]
"!!X. [|wf_idecl G (I, is, ms); J : set is|] ==> is_iface G J" (K [
Asm_full_simp_tac 1]);
val wf_cdecl_unique = prove_goalw thy [wf_cdecl_def]
"!!X. wf_cdecl G (C, sc, si, fs, ms) ==> unique fs & unique ms" (K [Auto_tac]);
val wf_cdecl_fdecl = prove_goalw thy [wf_cdecl_def]
"!!X. [|wf_cdecl G (C, sc, si, fs, ms); f:set fs|] ==> wf_fdecl G f" (K [Auto_tac]);
val wf_cdecl_mdecl = prove_goalw thy [wf_cdecl_def]
"!!X. [|wf_cdecl G (C, sc, si, fs, ms); m:set ms|] ==> wf_mdecl G C m"(K[Auto_tac]);
val wf_cdecl_impD = prove_goalw thy [wf_cdecl_def]
"!!X. [|wf_cdecl G (C, sc, si, fs, ms); I:set si|] ==> is_iface G I & \
\ (!s. !(md',(pn',rT')) : imethds G I s. \
\ (? md pn rT b. cmethd G C s = Some (md,((pn,rT),b)) & G|-rT<=:rT'))"
(K [Auto_tac]);
val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
"!!X. [|wf_cdecl G (C, sc, si, fs, ms); C ~= Object|] ==> ? D. sc = Some D & \
\ is_class G D & ~ G|-D<:C C & (table_of ms hiding cmethd G D \
\ entails (%((pn,rT),b) (md,((pn',rT'),b')). G|-rT<=:rT'))"
(K [Auto_tac]);
val iface_wf = prove_goalw thy [wf_prog_def, Let_def]
"!!X. [|iface G I = Some i; wf_prog G|] ==> wf_idecl G (I,i)" (K [
Asm_full_simp_tac 1,
fast_tac (set_cs addDs [get_in_set]) 1]);
val class_wf = prove_goalw thy [wf_prog_def, Let_def]
"!!X. [|class G C = Some c; wf_prog G|] ==> wf_cdecl G (C,c)" (K [
Asm_full_simp_tac 1,
fast_tac (set_cs addDs [get_in_set]) 1]);
val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def]
"!!X. wf_prog G ==> class G Object = Some (None, [], [], [])" (K [
safe_tac set_cs,
rotate_tac 4 1,
dtac in_set_get 1,
Auto_tac]);
Addsimps [class_Object];
val class_SXcpt = prove_goalw thy [wf_prog_def, Let_def, SXcptC_def]
"!!X. wf_prog G ==> class G (SXcpt xn) = Some (Some (if xn = Throwable \
\ then Object else SXcpt Throwable), [], [], [])" (K [
Safe_tac,
dtac spec 1,
rotate_tac 4 1,
dtac in_set_get 1,
Auto_tac]);
Addsimps [class_SXcpt];
val wf_emptyC = prove_goalw thy [wf_cdecl_def]
"wf_cdecl G (C , sc, [], [], []) = (~ is_iface G C & \
\ (case sc of None => C = Object | Some D => is_class G D & ~ G|-D<:C C))"
(K [Simp_tac 1]);
Addsimps [wf_emptyC];
val wf_ObjectC = prove_goalw thy [ObjectC_def]
"wf_cdecl G ObjectC = (~ is_iface G Object)" (K [Simp_tac 1]);
Addsimps [wf_ObjectC];
val wf_SXcptC = prove_goalw thy [SXcptC_def, Let_def]
"wf_cdecl G (SXcptC xn) = (~ is_iface G (SXcpt xn) & \
\ (let sc = if xn = Throwable then Object else SXcpt Throwable in \
\ is_class G sc & ~ G|-sc<:C SXcpt xn))" (K [Simp_tac 1]);
Addsimps [wf_SXcptC];
val is_class_Object = prove_goal thy "!!X. wf_prog G ==> is_class G Object" (K [
rtac is_classI 1, Asm_simp_tac 1]);
Addsimps [is_class_Object];
val is_class_SXcpt = prove_goal thy "!!X. wf_prog G ==> is_class G (SXcpt xn)" (K[
rtac is_classI 1, Asm_simp_tac 1]);
Addsimps [is_class_SXcpt];
AddSIs [is_class_SXcpt];
goal thy "!!X. [|is_class G Object; is_class G (SXcpt Throwable); \
\ class G (SXcpt xn) = Some (Some (if xn = Throwable then Object else \
\ SXcpt Throwable), rest)|] ==> G|-Class (SXcpt xn)<=:Class (SXcpt Throwable)";
b y case_tac "xn = Throwable" 1;
b y ALLGOALS Asm_full_simp_tac;
b y etac (subcls1I RS subcls.direct RS widen.subcls) 1;
b y atac 1;
val widen_SXcpt_Throwable_lemma = result();
val widen_xcpt_Throwable = prove_goal thy
"!!X. wf_prog G ==> G|-Class (SXcpt xn)<=:Class (SXcpt Throwable)" (K [
rtac widen_SXcpt_Throwable_lemma 1,
Auto_tac]);
Addsimps [widen_xcpt_Throwable];
val subcls_ObjectE = prove_goal thy "!!X. [|G|-Object<:C D; wf_prog G|] ==> R" (K [
dtac subclsD 1,
auto_tac(claset() addDs [subcls1D], simpset())]);
val implmt_ObjectE = prove_goal thy "!!X. [|G|-Object~=>I; wf_prog G|] ==> R" (K [
dtac implmtD 1,
auto_tac(claset() addDs [implmt1D,
subcls.direct RS subcls_ObjectE], simpset())]);
goal thy "!!X. wf_prog G ==> (subint1 G)^-1 Int (subint1 G)^+ = {}";
b y Safe_tac ;
b y dtac subint1D 1;
b y Clarify_tac 1;
b y ex_ftac is_ifaceD 1;
b y dtac iface_wf 1;
b y atac 1;
b y rewtac wf_idecl_def;
b y Asm_full_simp_tac 1;
b y Fast_tac 1;
val subint1_wf_lemma = result();
goal thy "!!X. wf_prog G ==> (subcls1 G)^-1 Int (subcls1 G)^+ = {}";
b y Safe_tac ;
b y dtac subcls1D 1;
b y Clarify_tac 1;
b y ex_ftac is_classD 1;
b y dtac class_wf 1;
b y atac 1;
b y rewtac wf_cdecl_def;
b y Asm_full_simp_tac 1;
val subcls1_wf_lemma = result();
val acyclic_subint1 = subint1_wf_lemma RS irrefl_tranclI RS acyclicI;
val acyclic_subcls1 = subcls1_wf_lemma RS irrefl_tranclI RS acyclicI;
(*
val subint_asym = prove_goal thy "!!X. [|wf_prog G; G|-I<:I J|] ==> ~ G|-J<:I I" (K [
dtac subintD 1,
fast_tac (HOL_cs addSDs [subint1_wfD] addIs [subint.trans]) 1]);
val subcls_asym = prove_goal thy "!!X. [|wf_prog G; G|-C<:C D|] ==> ~ G|-D<:C C" (K [
dtac subclsD 1,
fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [subcls.trans]) 1]);
*)
val subint_irrefl = prove_goal thy "!!X. [|wf_prog G; G|-I<:I J|] ==> I ~= J" (K [
dtac (subint1_wf_lemma RS irrefl_tranclI) 1,
etac swap2 1,
stac (subint1_trancl RS sym) 1,
Fast_tac 1]);
val subcls_irrefl = prove_goal thy "!!X. [|G|-C<:C D; wf_prog G|] ==> C ~= D" (K [
dtac (subcls1_wf_lemma RS irrefl_tranclI) 1,
etac swap2 1,
stac (subcls1_trancl RS sym) 1,
Fast_tac 1]);
val wf_subint1=acyclic_subint1 RS(finite_subint1 RS finite_acyclic_wf_converse);
val wf_subcls1=acyclic_subcls1 RS(finite_subcls1 RS finite_acyclic_wf_converse);
val wf_subint = prove_goal thy "!!X. wf_prog G ==> wf ((subint G)^-1)" (K [
stac (subint1_trancl RS sym) 1,
etac (wf_subint1 RS wf_converse_trancl) 1]);
val wf_subcls = prove_goal thy "!!X. wf_prog G ==> wf ((subcls G)^-1)" (K [
stac (subcls1_trancl RS sym) 1,
etac (wf_subcls1 RS wf_converse_trancl) 1]);
val subint_induct = prove_goal thy
"[|wf_prog G; !!I. !J. G|-I<:I J --> P J ==> P I|] ==> P I" (fn prems => [
cut_facts_tac prems 1, (* sic! *)
dtac wf_subint 1,
eres_inst_tac [("a","I")] wf_induct 1,
resolve_tac (tl prems) 1,
Auto_tac]);
val subcls_induct = prove_goal thy
"[|wf_prog G; !!C. !D. G|-C<:C D --> P D ==> P C|] ==> P C" (fn prems => [
cut_facts_tac prems 1, (* sic! *)
dtac wf_subcls 1,
eres_inst_tac [("a","C")] wf_induct 1,
resolve_tac (tl prems) 1,
Auto_tac]);
val prems = goal thy "[|is_iface G I; wf_prog G; \
\ !!I is ms. [|is_iface G I; iface G I = Some (is, ms) & wf_idecl G (I, is, ms) & \
\ (!J : set is. G|-I<:I1J & is_iface G J & P J)|] ==> P I|] ==> P I";
b y cut_facts_tac prems 1; (* sic! *)
b y rtac impE 1;
b y atac 2;
b y atac 2;
b y etac thin_rl 1;
b y rtac subint_induct 1;
b y atac 1;
b y rtac impI 1;
b y ex_ftac is_ifaceD 1;
b y forward_tac [iface_wf] 1;
b y atac 1;
b y rtac (hd (tl (tl prems))) 1;
b y atac 1;
b y subgoal_tac "! J:set is. G|-I<:I1J & is_iface G J" 1;
b y SELECT_GOAL (auto_tac (claset() addIs [subint.direct], simpset())) 1;
b y rtac ballI 1;
b y dtac wf_idecl_supD 1;
b y atac 1;
b y auto_tac (claset() addIs [subint1I], simpset());
val subint1_induct = result();
val prems = goal thy "[|is_class G C; wf_prog G; P Object; \
\!!C D si fs ms. [|C ~= Object; is_class G C; class G C = Some (Some D,si,fs,ms) & \
\ wf_cdecl G (C, Some D,si,fs,ms) & G|-C<:C1D & is_class G D & P D|] ==> P C\
\ |] ==> P C";
b y cut_facts_tac prems 1; (* sic! *)
b y rtac impE 1;
b y atac 2;
b y atac 2;
b y etac thin_rl 1;
b y rtac subcls_induct 1;
b y atac 1;
b y rtac impI 1;
b y case_tac "C = Object" 1;
b y Fast_tac 1;
b y ex_ftac is_classD 1;
b y forward_tac [class_wf] 1;
b y atac 1;
b y forward_tac [wf_cdecl_supD] 1;
b y atac 1;
b y Clarify_tac 1;
b y rtac (hd (tl (tl (tl prems)))) 1;
b y atac 1;
b y atac 1;
b y subgoal_tac "G|-C<:C1D" 1;
b y fast_tac (HOL_cs addIs [subcls.direct]) 1;
b y etac subcls1I 1;
b y atac 1;
val subcls1_induct = result();
section "recursion operators";
(* A particular thm about wf;
looks like it is an odd instance of something more general
*)
goalw WF.thy [wf_def] "wf{((x,A),(y,B)) . A=B & wf(R(f A)) & (x,y):R(f A)}";
by(full_simp_tac (simpset() delcongs [imp_cong]) 1);
by(strip_tac 1);
by(rename_tac "x A" 1);
by(case_tac "wf(R(f A))" 1);
by (eres_inst_tac [("a","x")] wf_induct 1);
by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
by (Fast_tac 1);
by(rewrite_goals_tac [wf_def]);
by(Blast_tac 1);
val wf_rel_lemma = result();
goalw thy [iface_wfrel_def] "wf iface_wfrel";
b y res_inst_tac [("f1","fst")] (wf_rel_lemma RS wf_subset) 1;
b y Auto_tac;
val wf_iface_wfrel = result();
goalw thy [class_wfrel_def] "wf class_wfrel";
b y res_inst_tac [("f1","fst")] (wf_rel_lemma RS wf_subset) 1;
b y Auto_tac;
val wf_class_wfrel = result();
goal thy "!!X. [|wf ((subint1 G)^-1); \
\ iface G I = Some i; !I:set (fst i). is_iface G I|] ==> \
\ iface_rec (I,G, f) = f I i ((%J. iface_rec (J,G,f))``set (fst i))";
b y stac (wf_iface_wfrel RS (hd iface_rec.rules)) 1;
b y asm_simp_tac (simpset() addsimps [wf_iface_wfrel]) 1;
b y auto_tac (claset() addIs [subint1I], simpset() addsimps [iface_wfrel_def]);
val iface_rec = result();
goal thy "!!X. [|wf ((subcls1 G)^-1); \
\ class G C = Some c; !C. Some C = fst c --> is_class G C|] ==> \
\ class_rec (C,G,t,f) = f C c (case (fst c) of None => t | Some D => \
\ class_rec (D,G,t,f))";
b y stac (wf_class_wfrel RS (hd class_rec.rules)) 1;
b y asm_simp_tac (simpset() addsimps [wf_class_wfrel]) 1;
b y auto_tac (claset() addIs [subcls1I], simpset() addsimps [class_wfrel_def]);
val class_rec = result();
val imethds_rec = prove_goalw thy [imeths_def] "!!X. [|wf ((subint1 G)^-1); \
\ iface G I = Some (is,ms); !I:set is. is_iface G I|] ==> imethds G I = \
\ Un_tables ((%J. imethds G J)``set is) ++++ \
\ (o2s o table_of (map (%(s,mh). (s,IfaceT I,mh)) ms))"
(K [asm_simp_tac (simpset() addsimps [iface_rec]) 1]);
val cmethd_rec = prove_goalw thy [cmethd_def] "!!X. [|wf ((subcls1 G)^-1); \
\ class G C = Some (sc,si,fs,ms); !C. sc=Some C --> is_class G C|] ==> \
\ cmethd G C = (case sc of None => empty | Some D => cmethd G D) ++ \
\ table_of (map (%(s,m). (s,(ClassT C,m))) ms)"
(K [asm_simp_tac (simpset() addsimps [class_rec]) 1]);
val fields_rec = prove_goalw thy [fields_def] "!!X. [|wf ((subcls1 G)^-1); \
\ class G C = Some (sc,si,fs,ms); !C. sc=Some C --> is_class G C|] ==> \
\ fields G C = map (%(fn,ft). ((fn,ClassT C),ft)) fs @ \
\ (case sc of None => [] | Some D => fields G D)"
(K [asm_simp_tac (simpset() addsimps [class_rec]) 1]);
goal thy "!!X. [|iface G I = Some (is,ms); wf_prog G|] ==> imethds G I = \
\ Un_tables ((%J. imethds G J)``set is) ++++ \
\ (o2s o table_of (map (%(s,mh). (s,IfaceT I,mh)) ms))";
b y rtac imethds_rec 1;
b y etac wf_subint1 1;
b y atac 1;
b y fast_tac (set_cs addEs [iface_wf RS wf_idecl_supD]) 1;
val wf_imethds_rec = result();
goal thy "!!X. [|class G C = Some (sc,si,fs,ms); wf_prog G|] ==> cmethd G C = \
\ (case sc of None => empty | Some D => cmethd G D) ++ \
\ table_of (map (%(s,m). (s,(ClassT C,m))) ms)";
b y rtac cmethd_rec 1;
b y etac wf_subcls1 1;
b y atac 1;
b y case_tac "C = Object" 1;
b y rotate_tac 1 1 THEN Asm_full_simp_tac 1; (*### conditional rewrite for class*)
b y fast_tac (claset() addSDs [class_wf RS wf_cdecl_supD]) 1;
val wf_cmethd_rec = result();
goal thy "!!X. [|class G C = Some (sc,si,fs,ms); wf_prog G|] ==> fields G C = \
\ map (%(fn,ft). ((fn,ClassT C),ft)) fs @ \
\ (case sc of None => [] | Some D => fields G D)";
b y rtac fields_rec 1;
b y etac wf_subcls1 1;
b y atac 1;
b y case_tac "C = Object" 1;
b y rotate_tac 1 1 THEN Asm_full_simp_tac 1; (*### conditional rewrite for class*)
b y fast_tac (claset() addSDs [class_wf RS wf_cdecl_supD]) 1;
val wf_fields_rec = result();
val cmethd_Object = prove_goal thy "!!X. wf_prog G ==> cmethd G Object = empty"
(K [stac wf_cmethd_rec 1,Auto_tac]);
val fields_Object = prove_goal thy "!!X. wf_prog G ==> fields G Object = []"(K [
stac wf_fields_rec 1,Auto_tac]);
Addsimps [cmethd_Object, fields_Object];
val cfield_Object = prove_goalw thy [cfield_def]
"!!X. wf_prog G ==> cfield G Object = empty" (K [Asm_simp_tac 1]);
Addsimps [cfield_Object];
val subcls_C_Object = prove_goal thy
"!!X. [|is_class G C; wf_prog G|] ==> C ~= Object --> G|-C<:C Object" (K [
etac subcls1_induct 1,
atac 1,
Fast_tac 1,
safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
fast_tac (HOL_cs addIs [subcls.direct]) 1,
rtac subcls.trans 1,
atac 2,
rtac subcls.direct 1,
rtac subcls1I 1,
ALLGOALS Asm_simp_tac]) RS mp;
val is_type_rTI = prove_goalw thy [wf_mhead_def]
"!!sig. wf_mhead G sig (pn,rT) ==> is_type G rT"
(K [Auto_tac (*addloop (split_asm_tac [expand_split_asm])*)]);
val widen_Class_Object = prove_goal thy
"!!X. [|wf_prog G; is_class G C|] ==> G|-Class C<=:Class Object" (K [
case_tac "C=Object" 1,
hyp_subst_tac 1,
Asm_simp_tac 1,
rtac widen.subcls 1,
fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
val widen_trans = prove_goal thy "!!X. [|G|-S<=:U; G|-U<=:T; wf_prog G|] ==> G|-S<=:T" (K [
fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
subcls_ObjectE, implmt_ObjectE]) 1]);
val widen_trans2 = prove_goal thy "!!X. [|G|-U<=:T; G|-S<=:U; wf_prog G|] ==> G|-S<=:T" (K [
fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
subcls_ObjectE, implmt_ObjectE]) 1]);
AddEs [widen_trans, widen_trans2];
val fields_mono = prove_goal thy
"!!X. [|G|-C'<:C C; wf_prog G|] ==> \
\ x : set (fields G C) --> x : set (fields G C')" (K [
etac subcls.induct 1,
safe_tac (HOL_cs addSDs [subcls1D]),
ex_ftac is_classD 1,
stac wf_fields_rec 1,
Auto_tac]) RS mp;
goal thy "!!X. [|is_class G C; wf_prog G|] ==> \
\ !((fn,fd),fT):set (fields G C). G|-Class C<=:RefT fd";
b y etac subcls1_induct 1;
b y atac 1;
b y Asm_simp_tac 1;
b y safe_tac HOL_cs;
b y stac wf_fields_rec 1;
b y atac 1;
b y atac 1;
b y dtac (subcls.direct RS widen.subcls) 1;
b y Force_tac 1;
val widen_fields_defpl' = result();
goal thy "!!X. [|((fn,fd),fT) : set (fields G C); is_class G C; wf_prog G|] ==> \
\ G|-Class C<=:RefT fd";
b y dtac widen_fields_defpl' 1;
b y atac 1;
b y Force_tac 1;
val widen_fields_defpl = result();
goal thy "!!X. [|is_class G C; wf_prog G|] ==> unique (fields G C)";
b y etac subcls1_induct 1;
b y atac 1;
b y Asm_simp_tac 1;
b y stac wf_fields_rec 1;
b y Auto_tac;
b y etac unique_append 1;
b y rtac unique_map_inj 1;
b y fast_tac (claset() addSDs [wf_cdecl_unique RS conjunct1]) 1;
b y fast_tac (claset() addSIs [injI]) 1;
b y safe_tac (claset() addSDs [wf_cdecl_supD]);
b y Asm_full_simp_tac 1;
b y dtac split_Pair_eq 1;
b y dtac widen_fields_defpl 1;
b y atac 1;
b y atac 1;
b y Asm_full_simp_tac 1;
b y fast_tac (set_cs addDs [widen_Class_Class,subcls.direct RS subcls_irrefl])1;
val unique_fields = result();
goal thy "!!X. [|is_class G C; wf_prog G|] ==> \
\ !((fn,fd),T):set (fields G C). is_type G T";
b y etac subcls1_induct 1;
b y atac 1;
b y Asm_simp_tac 1;
b y stac wf_fields_rec 1;
b y Fast_tac 1;
b y atac 1;
b y auto_tac(claset() addDs[wf_cdecl_fdecl],simpset() addsimps [wf_fdecl_def2]);
val is_type_fields = result() RS bspec;
goal thy
"!!X. [|wf_prog G; G|-Class C'<=:Class C; table_of (fields G C) f = Some ft|] ==> \
\ table_of (fields G C') f = Some ft";
b y dtac widen_Class_Class 1;
b y etac disjE 1;
b y Asm_simp_tac 1;
b y rtac table_of_mono 1;
b y atac 3;
b y rtac unique_fields 1;
b y etac (subcls_is_class RS conjunct1) 1;
b y atac 1;
b y fast_tac (HOL_cs addEs [fields_mono]) 1;
val widen_fields_mono = result();
val cfs_fields_lemma = prove_goalw thy [cfield_def] "!!X. \
\ cfield G C fn = Some (fd, fT) ==> table_of (fields G C) (fn, fd) = Some fT"
(K [rtac table_of_map_Some 1, Asm_full_simp_tac 1]);
val widen_cfs_fields = prove_goal thy "!!X. [|cfield G C fn = Some (fd, fT);\
\ G|-Class C'<=:Class C; wf_prog G|] ==> table_of (fields G C') (fn, fd) = Some fT"
(K[fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
goal thy "!!X. [|is_iface G I; wf_prog G|] ==> (md,mh) : imethds G I sig --> \
\wf_mhead G sig mh";
b y etac subint1_induct 1;
b y atac 1;
b y stac wf_imethds_rec 1;
b y Fast_tac 1;
b y atac 1;
b y Clarify_tac 1;
b y dtac overrides_SomeD 1;
b y force_tac (claset() addEs [wf_idecl_mhead, get_in_set], simpset()) 1;
val imethds_wf_mhead = result() RS mp;
goal thy "!!X. [|is_class G C; wf_prog G|] ==> cmethd G C sig = Some (md,mh,m)\
\ --> (? C'. md = ClassT C' & G|-Class C<=:Class C'& wf_mdecl G C' (sig,(mh,m)))";
b y etac subcls1_induct 1;
b y atac 1;
b y Force_tac 1;
b y etac conjE 1;
b y stac wf_cmethd_rec 1;
b y atac 1;
b y atac 1;
b y Clarify_tac 1;
b y dtac override_SomeD 1;
b y etac disjE 1;
b y dtac table_of_mapf_SomeD 1;
b y force_tac (claset() addEs [wf_cdecl_mdecl], simpset()) 1;
b y force_tac (claset() addIs [
subcls1I RS subcls.direct RS widen.subcls], simpset()) 1;
val cmethd_wf_mdecl' = result() RS mp;
goal thy "!!X. [|cmethd G C sig = Some (md,mh,m); is_class G C; wf_prog G|] ==> \
\ ? C'. md = ClassT C' & G|-Class C<=:Class C'& wf_mdecl G C' (sig,(mh,m))";
b y fast_tac (HOL_cs addEs [cmethd_wf_mdecl']) 1;
val cmethd_wf_mdecl = result();
goal thy "!!sig. [|G|-T<:C T'; wf_prog G|] ==> \
\ !md pn rT mb . cmethd G T' sig = Some (md ,(pn ,rT ),mb )-->\
\(? md' pn' rT'. (? mb'. cmethd G T sig = Some (md',(pn',rT'),mb')) & G|-rT'<=:rT)";
b y etac subcls.induct 1;
b y Clarify_tac 2;
b y EVERY'[dtac spec, dtac spec, dtac spec, dtac spec, mp_tac] 2;
b y Fast_tac 2;
b y subgoal_tac "C ~= Object" 1;
b y fast_tac (claset() addEs [subcls.direct RS subcls_ObjectE]) 2;
b y safe_tac (HOL_cs addSDs [subcls1D]);
b y stac wf_cmethd_rec 1;
b y atac 1;
b y atac 1;
b y rewtac override_def;
b y Asm_simp_tac 1;
b y rtac conjI 1;
b y fast_tac (claset() addDs [cmethd_wf_mdecl,
(wf_mdeclD RS conjunct1) RS is_type_rTI]) 1;
b y auto_tac (claset() addDs [class_wf RS wf_cdecl_supD, hiding_entailsD]
, simpset());
val subcls_widen_methd = result() RS spec RS spec RS spec RS spec RS mp;
goal thy "!!X. [|G|-I<:I J; wf_prog G|] ==> \
\ !(md, (pn ,rT )) : imethds G J sig. \
\ (? (md',(pn',rT')) : imethds G I sig. G|-rT'<=:rT)";
b y etac subint.induct 1;
b y Clarify_tac 2;
b y EVERY'[dtac bspec, atac] 2;
b y Clarify_tac 2;
b y EVERY'[dtac bspec, atac] 2;
b y fast_tac (claset() addSEs [widen_trans] (* sic! *)) 2;
b y dtac subint1D 1;
b y Clarify_tac 1;
b y stac wf_imethds_rec 1;
b y atac 1;
b y atac 1;
b y simp_tac (simpset() addsimps [overrides_def, o_def]) 1;
b y Safe_tac;
b y fast_tac (claset() addEs [imethds_wf_mhead RS is_type_rTI RS widen.refl])1;
b y not_None_tac 1;
b y force_tac (claset() addDs [iface_wf RS wf_idecl_hidings, hidings_entailsD]
, simpset()) 1;
val subint_widen_imethds = result();
goal thy "!!X. [|G|-C~=>1I; wf_prog G; (md, (pn,rT)) : imethds G I sig|] ==> \
\ ? md' pn' rT' mb'. cmethd G C sig = Some (md' ,(pn', rT'), mb') & G|-rT'<=:rT";
b y dtac implmt1D 1;
b y fast_tac (claset() addSDs [class_wf, wf_cdecl_impD]) 1;
val implmt1_widen_methd = result();
goal thy "!!X. [|wf_prog G; G|-T''~=>tname|] ==> \
\ !md pn rT. !(md, (pn, rT)) : imethds G tname sig. \
\ (? md' pn' rT' mb'. cmethd G T'' sig = Some (md',(pn',rT'),mb') & G|-rT'<=:rT)";
b y etac implmt.induct 1;
b y Safe_tac;
b y fast_tac (HOL_cs addEs [implmt1_widen_methd]) 1;
b y fast_tac (claset() addDs [implmt1_widen_methd]
addSDs [subint_widen_imethds]) 1;
b y fast_tac (claset() addSDs [implmt1_widen_methd]
addDs [subcls.direct RS subcls_widen_methd]) 1;
val implmt_widen_methd = result();
goal thy
"!!sig. [|(md ,(pn,rT)) : mheads G T sig; wf_prog G; G|-Class T''<=:RefT T|] ==>\
\? md' pn' rT' mb'. cmethd G T'' sig = Some (md',(pn',rT'),mb') & G|-rT'<=:rT";
b y forward_tac [widen_Class_RefT] 1;
b y Safe_tac;
b y dtac widen_Class_Iface 2;
b y dtac implmt_widen_methd 2;
b y Fast_tac 2;
b y Force_tac 2;
b y forward_tac [widen_Class_Class] 1;
b y force_tac (claset() addDs [cmethd_wf_mdecl,
(wf_mdeclD RS conjunct1) RS is_type_rTI,subcls_widen_methd], simpset()) 1;
val widen_methd = result();
goal thy
"!!X. [|(md, (pn,rT)) : mheads G T (mn, pT); G|-Class T''<=:RefT T; wf_prog G|] ==> \
\ ? T' pn' rT' lvars blk res. \
\ cmethd G T'' (mn, pT) = Some (ClassT T', (pn', rT'), lvars, blk, res) & \
\ G|-rT'<=:rT & G|-Class T''<=:Class T' & (! (f,T):set lvars. is_type G T) & \
\ (let E=(G,table_of lvars[This|->Class T'][pn'|->pT]) in \
\ E|-blk::<> & (? T. E|-res::T & G|-T<=:rT'))";
b y forward_tac [widen_is_type RS conjunct1] 1;
b y dtac widen_methd 1;
b y atac 1;
b y atac 1;
b y Clarify_tac 1;
b y Asm_full_simp_tac 1;
b y dtac cmethd_wf_mdecl 1;
b y atac 1;
b y atac 1;
b y auto_tac (claset() addSDs [wf_mdeclD], simpset() addsimps [Let_def]);
val Call_lemma = result();
goal thy "!!x. wf_prog G ==> x : mheads G T sig --> G|-Ta[.]<=:RefT T --> R";
b y Rt.induct_tac "T" 1;
b y Auto_tac;
b y etac widen_Array_Iface 1;
b y dtac widen_Array_Class 1;
b y rotate_tac 1 1; (*###wf_prog*)
b y Auto_tac;
val mheads_ArrayD = result() RS mp RS mp;