WellForm.ML
Back to theory WellForm
goal thy
"(dc,oc) : r^* = (oc=dc | (dc,oc) : r^+)";
by (fast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1,trancl_into_rtrancl]) 1);
qed_spec_mp "rtrancl_eq_or_trancl";
(***
val subset_lemma = prove_goal thy
"{(C,D). P C & Q D & R C D} <= {(C,D). P C & Q D}" (K [Fast_tac 1]);
(* von David *)
***)
val subset_lemma = prove_goal thy
"{(C,D). (P1 C & P2 C) & (Q1 D & Q2 D) & R C D} <= {(C,D). P1 C & Q1 D}" (K [Fast_tac 1]);
goalw thy [d_superinterface_rel_def,wf_classfiles_def,is_inter_def]
"!!dummy.\
\ wf_classfiles CFS ==> finite (d_superinterface_rel CFS)";
br (subset_lemma RS finite_subset) 1;
bd conjunct1 1;
by (Force_tac 1);
qed "finite_d_superinterface_rel";
goalw thy [d_superclass_rel_def,wf_classfiles_def,is_class_def]
"!!dummy.\
\ wf_classfiles CFS ==> finite (d_superclass_rel CFS)";
br (subset_lemma RS finite_subset) 1;
bd conjunct1 1;
by (Force_tac 1);
qed "finite_d_superclass_rel";
goalw thy [wf_classfiles_def,wf_inter_def,is_inter_def]
"!!dummy.\
\[| wf_classfiles CFS; si : get_superinterfaces (CFS !! i); is_inter CFS i |] \
\==> (i,si) ~: (d_superinterface_rel CFS)^*";
by (Fast_tac 1);
qed "wf_cs1";
goal thy
"!!dummy.\
\[| wf_classfiles CFS; \
\ (si,i) : (d_superinterface_rel CFS)^+ |] \
\==> i~=si";
by (Clarify_tac 1);
be tranclE 1;
by (fast_tac (claset() addDs [wf_cs1]
addss (simpset() addsimps [d_superinterface_rel_def])) 1);
by (fast_tac (claset() addDs [wf_cs1,trancl_into_rtrancl]
addss (simpset() addsimps [d_superinterface_rel_def])) 1);
qed "d_superinterface_rel_irrefl";
goalw thy [acyclic_def]
"!!dummy.\
\ wf_classfiles CFS ==> acyclic (d_superinterface_rel CFS)";
by (fast_tac (claset() addDs [d_superinterface_rel_irrefl]) 1);
qed "acyclic_d_superinterface_rel";
goal thy
"!!dummy.\
\ wf_classfiles CFS ==> wf (d_superinterface_rel CFS)";
br finite_acyclic_wf 1;
be finite_d_superinterface_rel 1;
be acyclic_d_superinterface_rel 1;
qed "wf_d_superinterface_rel";
context WF.thy;
Goalw [wf_def] "wf{((A,x),(B,y)) . A=B & wf(R(f A)) & (x,y):R(f A)}";
by(full_simp_tac (simpset_of WF.thy delcongs [imp_cong]) 1);
by(strip_tac 1);
by(rename_tac "A x" 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 WF.thy[wf_def]"wf{((A,x,m),(B,y,n)) . A=B & m=n & wf(R(A)) & (x,y):R(A)}";
by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
by(strip_tac 1);
by(rename_tac "A x m" 1);
by(case_tac "wf(R A)" 1);
by (eres_inst_tac [("a","x")] wf_induct 1);
by (EVERY1[etac allE, etac allE, etac allE, etac mp, rtac allI, rtac allI, rtac allI]);
by (Fast_tac 1);
by(rewrite_goals_tac [wf_def]);
by(Blast_tac 1);
val wf_rel_lemma2 = result();
goalw WF.thy[wf_def]"wf{((A,x,m),(B,y,n)) . A=B & x=y & wf(R(A)) & (m,n):R(A)}";
by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
by(strip_tac 1);
by(rename_tac "A x m" 1);
by(case_tac "wf(R A)" 1);
by (eres_inst_tac [("a","m")] wf_induct 1);
by (EVERY1[etac allE, etac allE, etac allE, etac mp, rtac allI, rtac allI, rtac allI]);
by (Fast_tac 1);
by(rewrite_goals_tac [wf_def]);
by(Blast_tac 1);
val wf_rel_lemma3 = result();
context thy;
(* von David *)
(******************** all_superclasses ********************)
goal thy
"!!dummy.\
\[| (cn,sc) : (d_superclass_rel CFS)^* |]\
\==> (is_class CFS cn --> is_class CFS sc)";
be rtranclE 1;
by (Fast_tac 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed_spec_mp "in_d_superclass_rel_is_class";
goal thy
"!!dummy.\
\[| (cn,sc) : (d_superclass_rel CFS)^* |]\
\==> (is_class CFS sc --> is_class CFS cn)";
be rtrancl_induct 1;
by (Fast_tac 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed_spec_mp "in_d_superclass_rel_is_class2";
goalw thy [wf_classfiles_def,wf_class_def,d_superclass_rel_def]
"!!dummy.\
\[| wf_classfiles CFS; (sc,cn) : (d_superclass_rel CFS)^+ |]\
\==> cn~=Object";
be tranclE 1;
by (fast_tac (claset() addss (simpset())) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed "in_superclasses_not_Object";
goalw thy [wf_classfiles_def,wf_class_def,d_superclass_rel_def]
"!!dummy.\
\[| wf_classfiles CFS; sc~=Object; (sc,cn) : (d_superclass_rel CFS)^* |]\
\==> cn~=Object";
be rtranclE 1;
by (fast_tac (claset() addss (simpset())) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed "in_superclasses_not_Object2";
goalw thy [wf_classfiles_def,wf_class_def,d_superclass_rel_def]
"!!dummy.\
\[| wf_classfiles CFS; (sc,Object) : (d_superclass_rel CFS)^* |]\
\==> sc=Object";
be rtranclE 1;
by (fast_tac (claset() addss (simpset())) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed "in_superclasses_not_Object3";
goal thy
"!!dummy.\
\[| wf_classfiles CFS |] \
\==> (sc,Object) ~: (d_superclass_rel CFS)^+";
by (fast_tac (claset() addDs [in_superclasses_not_Object] addss (simpset())) 1);
qed "wf_cs0";
goalw thy [wf_classfiles_def,wf_class_def,is_class_def]
"!!dummy.\
\[| wf_classfiles CFS; get_superclass (CFS !! cn) = sc; is_class CFS cn; cn ~= Object |] \
\==> (cn,sc) ~: (d_superclass_rel CFS)^*";
by (case_tac "no_super (CFS !! cn)" 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","cn")] allE 1);
by (fast_tac (claset() addss (simpset() addsimps [])) 1);
by (fast_tac (claset() addss (simpset() addsimps [Let_def])) 1);
qed "wf_cs3";
goalw thy [wf_classfiles_def,wf_class_def,is_class_def]
"!!dummy.\
\[| wf_classfiles CFS; cn~=Object; get_superclass (CFS !! cn) = sc; is_class CFS cn |] \
\==> sc~=cn & is_class CFS sc";
by (case_tac "no_super (CFS !! cn)" 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","cn")] allE 1);
by (fast_tac (claset() addss (simpset())) 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","cn")] allE 1);
by (fast_tac (claset() addDs [trancl_into_rtrancl] addss (simpset() addsimps [Let_def])) 1);
qed "wf_cs4";
goal thy
"!!dummy.\
\[| wf_classfiles CFS; \
\ (sc,cn) : (d_superclass_rel CFS)^+ |] \
\==> cn~=sc";
by (Clarify_tac 1);
be tranclE 1;
by (fast_tac (claset() addDs [wf_cs3]
addss (simpset() addsimps [d_superclass_rel_def])) 1);
by (fast_tac (claset() addDs [wf_cs3] addIs [trancl_into_rtrancl]
addss (simpset() addsimps [d_superclass_rel_def])) 1);
qed "d_superclass_rel_irrefl";
goalw thy [acyclic_def]
"!!dummy.\
\ wf_classfiles CFS ==> acyclic (d_superclass_rel CFS)";
by (fast_tac (claset() addDs [d_superclass_rel_irrefl]) 1);
qed "acyclic_d_superclass_rel";
goal thy
"!!dummy.\
\ wf_classfiles CFS ==> wf (d_superclass_rel CFS)";
br finite_acyclic_wf 1;
be finite_d_superclass_rel 1;
be acyclic_d_superclass_rel 1;
qed "wf_d_superclass_rel";
goalw thy [implements_term_rel_def,split_def]
"wf implements_term_rel";
by (res_inst_tac [("R1","d_superclass_rel")] (wf_rel_lemma2 RS wf_subset) 1);
by (asm_full_simp_tac (simpset() addsimps [split_def]) 1);
qed "wf_implements_term_rel";
goal thy
"!!dummy.\
\[| wf_classfiles CFS |] \
\==> implements (CFS, cn, si) = \
\ ((d_implements CFS cn si) | \
\ (? si'. d_implements CFS cn si' & (si,si') : (d_superinterface_rel CFS)^+) | \
\ (? sc. (sc,cn) : d_superclass_rel CFS & implements (CFS, sc, si)))";
br (hd(implements.rules) RS ssubst) 1;
br wf_implements_term_rel 1;
by (fast_tac (claset() addss (simpset() addsimps [implements_term_rel_def,d_superclass_rel_def])) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,wf_cs4,wf_d_superclass_rel]) 1);
qed "implements_rec";
goalw thy [get_all_fields_term_rel_def,split_def]
"wf get_all_fields_term_rel";
by (res_inst_tac [("R1","d_superclass_rel")] (wf_rel_lemma RS wf_subset) 1);
by (asm_full_simp_tac (simpset() addsimps [split_def]) 1);
by (Force_tac 1);
qed "wf_get_all_fields_term_rel";
goal thy
"!!dummy.\
\[| wf_classfiles CFS; is_class CFS cn |] \
\==> get_all_fields (CFS,cn) = \
\ (let fs = get_fields (CFS !! cn) \
\ in \
\ if cn=Object \
\ then fs \
\ else (let sc = get_superclass (CFS !! cn) \
\ in \
\ (get_all_fields (CFS, sc)) ++ fs))";
br (hd(get_all_fields.rules) RS ssubst) 1;
br wf_get_all_fields_term_rel 1;
by (fast_tac (claset() addss (simpset() addsimps [get_all_fields_term_rel_def,d_superclass_rel_def])) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,wf_cs4,wf_d_superclass_rel]) 1);
qed "get_all_fields_rec";
goalw thy [wf_classfiles_def,wf_class_def,is_class_def]
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> is_class CFS Object & get_superinterfaces (CFS !! Object)={} & \
\ get_fields (CFS !! Object) = empty";
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","Object")] allE 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "wf_cs6";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> ~ implements (CFS, Object, i)";
br (implements_rec RS ssubst) 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps
[wf_classfiles_def,wf_class_def,d_superclass_rel_def,d_implements_def,is_class_def]) 1);
qed "not_implements_Object";
goalw thy [d_superinterface_rel_def]
"!!dummy.\
\[| (si,i) : (d_superinterface_rel CFS)^+ |] ==> is_inter CFS si & is_inter CFS i";
be trancl_induct 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "in_superinterface_rel_imp_is_inter";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> implements (CFS, cn, si) --> is_class CFS cn & is_inter CFS si";
by (forward_tac [wf_d_superclass_rel] 1);
by (eres_inst_tac [("a","cn")] wf_induct 1);
by (rotate_tac ~1 1);
br (implements_rec RS ssubst) 1;
ba 1;
by (fast_tac (claset() addss (simpset() addsimps
[d_superclass_rel_def,d_implements_def,in_superinterface_rel_imp_is_inter])) 1);
qed_spec_mp "implements_impl_is_inter";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> (sc,Object) ~: (d_superclass_rel CFS)^+";
br notI 1;
be tranclE 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed "not_in_superclass_rel_Object";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> implements (CFS,cn,i) --> (si,i) : (d_superinterface_rel CFS)^+ --> implements (CFS,cn,si)";
by (forward_tac [wf_d_superclass_rel] 1);
by (eres_inst_tac [("a","cn")] wf_induct 1);
by (rotate_tac ~1 1);
br (implements_rec RS ssubst) 1;
ba 1;
by (strip_tac 1);
by (dres_inst_tac [("P","%x. x")] (implements_rec RS subst) 1);
ba 1;
by (eres_inst_tac [("x","get_superclass (CFS !! x)")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
be disjE 1;
by (fast_tac (claset() addss (simpset() addsimps [])) 1);
be disjE 1;
by (fast_tac (claset() addDs [trancl_trans] addss (simpset() addsimps [])) 1);
by (fast_tac (claset() addDs [trancl_trans] addss (simpset() addsimps [])) 1);
qed_spec_mp "implements_superinterface_trans";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS |] \
\ ==> implements (CFS,cn,i) --> (si,i) : (d_superinterface_rel CFS)^* --> implements (CFS,cn,si)";
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (Clarify_tac 1);
br conjI 1;
by (Clarify_tac 1);
by (fast_tac (claset() addIs [implements_superinterface_trans]) 1);
qed_spec_mp "implements_superinterface_trans2";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS; \
\ (sc,cn) : (d_superclass_rel CFS)^+ ; implements (CFS,sc,si) |] \
\ ==> implements (CFS,cn,si)";
be trancl_induct 1;
br (implements_rec RS ssubst) 1;
ba 1;
bd (implements_rec RS subst) 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
br (implements_rec RS ssubst) 1;
ba 1;
bd (implements_rec RS subst) 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed_spec_mp "implements_superclass_rel_trans";
goal thy
"!!dummy. \
\ [| wf_classfiles CFS; \
\ (sc,cn) : (d_superclass_rel CFS)^* ; implements (CFS,sc,si) |] \
\ ==> implements (CFS,cn,si)";
be rtrancl_induct 1;
ba 1;
br (implements_rec RS ssubst) 1;
ba 1;
bd (implements_rec RS subst) 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed_spec_mp "implements_superclass_rel_trans2";
goal thy
"!!dummy.\
\[| wf_classfiles CFS |] \
\==> is_class CFS cn & cn ~= Object --> (Object,cn) : (d_superclass_rel CFS)^+";
by (forward_tac [wf_d_superclass_rel] 1);
be wf_induct 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
by (fast_tac (claset() addDs [wf_cs4] addEs [trancl_trans] addIs [r_into_trancl]
addss (simpset() addsimps [d_superclass_rel_def])) 1);
qed_spec_mp "in_superclass_rel_Object";
goal thy
"!!dummy.\
\[| wf_classfiles CFS |] \
\==> is_class CFS cn --> (Object,cn) : (d_superclass_rel CFS)^*";
by (case_tac "cn=Object" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addEs [trancl_trans] addIs [trancl_into_rtrancl,in_superclass_rel_Object]
addss (simpset() addsimps [])) 1);
qed_spec_mp "in_superclass_rel_Object2";
goalw thy [dyn_class_term_rel_def,split_def]
"wf dyn_class_term_rel";
by (res_inst_tac [("R1","d_superclass_rel")] (wf_rel_lemma3 RS wf_subset) 1);
by (asm_full_simp_tac (simpset() addsimps [split_def]) 1);
qed "wf_dyn_class_term_rel";
goal thy
"!!dummy.\
\[| wf_classfiles CFS; is_class CFS cn |] \
\==> dyn_class (CFS, ml, cn) = \
\ (let ms = get_methods (CFS !! cn) \
\ in \
\ if ms ml ~= None \
\ then cn \
\ else if cn = Object \
\ then arbitrary \
\ else (let sc = get_superclass (CFS !! cn) \
\ in \
\ dyn_class (CFS, ml, sc)))";
br (hd(dyn_class.rules) RS ssubst) 1;
br wf_dyn_class_term_rel 1;
by (fast_tac (claset() addss (simpset() addsimps [dyn_class_term_rel_def,d_superclass_rel_def])) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,wf_cs4,wf_d_superclass_rel]) 1);
qed "dyn_class_rec";
goalw thy [d_superclass_rel_def]
"(sc,cn) : d_superclass_rel CFS --> is_class CFS cn & is_class CFS sc & cn~= Object & get_superclass (CFS !! cn) = sc";
by (Simp_tac 1);
qed_spec_mp "d_superclass_imp_class";
goal thy
"!!dummy. \
\ [| (sc,cn) : (d_superclass_rel CFS)^+ |] \
\ ==> is_class CFS cn & is_class CFS sc";
be trancl_induct 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
qed "in_superclass_rel_imp_is_class";
goalw thy [d_implements_def]
"d_implements CFS cn si --> is_class CFS cn & is_inter CFS si";
by (Simp_tac 1);
qed_spec_mp "d_implements_imp_class_inter";