WT.ML
Back to theory WT
goal thy
"XT >>= [] = (XT=[])";
by (case_tac "XT=[]" 1);
by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
qed "sup_loc_Nil";
goal thy
"XT >>= (Y#YT) = (? X XT'. XT=X#XT' & X>=Y & XT'>>=YT)";
by (case_tac "XT=[]" 1);
by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
qed "sup_loc_Cons";
(************************************************************************************************************)
goal thy
"!xs. map f xs = map f ys --> (!x y. (f x = f y) = (x = y)) --> xs=ys";
by (induct_tac "ys" 1);
by (asm_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addss (simpset() addsimps [map_eq_Cons])) 1);
qed_spec_mp "map_inject";
goal thy
"tysl2tys I_ [PTS Integer] = PTS Integer";
by (asm_full_simp_tac (simpset() addsimps [select_equality,tysl2tys_def]) 1);
qed_spec_mp "tysl2tys_I";
goal thy
"tysl2tys A_ (map RTS rs) = RTS (concat rs)";
by (simp_tac (simpset() addsimps [tysl2tys_def]) 1);
by (res_inst_tac [("f","concat")] arg_cong 1);
by (fast_tac (claset() addDs [map_inject] addss (simpset() addsimps [select_equality])) 1);
qed_spec_mp "tysl2tys_A";
goal thy
"ins_type_tysl_ok X ts --> (Xa >= (US (tysl2tys X ts))) --> t : set ts --> (Xa >= (US t))";
by (force_tac (claset(), simpset()
addsplits [any.split,tys.split,ins_type.split,any.split_asm,tys.split_asm,ins_type.split_asm]
addsimps [ins_type_tysl_ok_def,sup_any_def,tysl2tys_I,tysl2tys_A]) 1);
qed_spec_mp "ins_type_tylist_ok_lemma";
goalw thy [wf_classfiles_def,wf_class_def,d_implements_def]
"!!dummy.\
\[| wf_classfiles CFS; \
\ d_implements CFS cn si |] \
\==> method_impl_ok CFS cn si";
by (Clarify_tac 1);
by (eres_inst_tac [("x","cn")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [is_class_def]) 1);
by (case_tac "no_super (CFS !! cn)" 1);
by (fast_tac (claset() addss (simpset())) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,rtrancl_eq_or_trancl]) 1);
qed "wf_cs7";
goalw thy [wf_classfiles_def,wf_class_def,d_implements_def]
"!!dummy.\
\[| wf_classfiles CFS; \
\ d_implements CFS cn si'; (si,si') : (d_superinterface_rel CFS)^+ |] \
\==> method_impl_ok CFS cn si";
by (Clarify_tac 1);
by (eres_inst_tac [("x","cn")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [is_class_def]) 1);
by (case_tac "no_super (CFS !! cn)" 1);
by (fast_tac (claset() addss (simpset())) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,rtrancl_eq_or_trancl]) 1);
qed "wf_cs8";
goalw thy [method_impl_ok_def,method_over_ok_def]
"wf_classfiles CFS --> method_impl_ok CFS cn si --> (cn,cna) : (d_superclass_rel CFS)^* \
\--> method_over_ok CFS cna si";
by (Clarify_tac 1);
by (eres_inst_tac [("x","(a,b)")] allE 1);
by (eres_inst_tac [("x","rd'")] allE 1);
by (eres_inst_tac [("x","ins'")] allE 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
bd rtrancl_trans 1;
back();
ba 1;
bd wf_cs9 1;
ba 1;
back();
by (asm_full_simp_tac (simpset() addsimps [method_over_ok_def]) 1);
by (fast_tac (claset() addss (simpset() delsimps [split_paired_All])) 1);
qed_spec_mp "method_impl_ok_method_over_ok_trans";
goal thy
"wf_classfiles CFS \
\ --> implements (CFS, sc, si) \
\ --> (!cn. (sc,cn) : (d_superclass_rel CFS)^* \
\ --> method_over_ok CFS cn si)";
by (res_inst_tac [("u","CFS"),("v","sc"),("w","si")] implements.induct 1);
br wf_implements_term_rel 1;
by (asm_full_simp_tac (simpset() addsimps [implements_term_rel_def]) 1);
by (case_tac "cn=Object" 1);
by (asm_full_simp_tac (simpset() addsimps [not_implements_Object]) 1);
br impI 1;
br (implements_rec RS ssubst) 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
br conjI 1;
by (fast_tac (claset() addDs [in_superclasses_not_Object2]
addIs [wf_cs9,wf_cs7,method_impl_ok_method_over_ok_trans]) 1);
br conjI 1;
by (fast_tac (claset() addDs [in_superclasses_not_Object2]
addIs [wf_cs9,wf_cs8,method_impl_ok_method_over_ok_trans]) 1);
by (asm_full_simp_tac (simpset() addsimps [wf_d_superclass_rel]) 1);
by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl] addss (simpset())) 1);
qed_spec_mp "wf_cs10";
(**
goal thy
"!!dummy.\
\[| wf_classfiles CFS; wideRefConvertible CFS (CT cn) (IT mc) |] \
\==> method_over_ok CFS cn mc";
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addIs [wf_cs10]) 1);
qed "wideRefConvertible_imp_method_over_ok2";
**)
goal thy
"!!dummy. \
\ [|wf_classfiles CFS; (cn', cn) : (d_superclass_rel CFS)^* |] \
\ ==> is_class CFS cn --> get_methods (CFS !! cn') (mn, pd) = Some (rd, ins') \
\ --> is_class CFS (dyn_class (CFS, (mn,pd), cn)) & \
\ (dyn_class (CFS, (mn,pd), cn), cn) : (d_superclass_rel CFS)^* & \
\ (? ins'. get_methods (CFS !! dyn_class (CFS, (mn,pd), cn)) (mn,pd) = Some (rd, ins'))";
be rtrancl_induct 1;
by (asm_full_simp_tac (simpset() delsplits [split_if] addsimps [dyn_class_rec,Let_def]) 1);
by (Clarify_tac 1);
by (case_tac "get_methods (CFS !! z) (mn,pd) = None" 1);
by (fast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl] addss (simpset()
addsimps [dyn_class_None,d_superclass_rel_def])) 1);
(* ???? *)
by (auto_tac (claset() addIs [rtrancl_trans,r_into_rtrancl,wf_cs9,method_over_ok_lemma],
simpset() addsimps [dyn_class_not_None,d_superclass_rel_def]));
by (Clarify_tac 1);
by (fold_tac [d_superclass_rel_def]);
bd rtrancl_trans 1;
br r_into_rtrancl 1;
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
by (Fast_tac 1);
bd wf_cs9 1;
ba 1;
back();
bd method_over_ok_lemma 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Force_tac 1);
(**
by (deepen_tac (claset() addIs [rtrancl_trans,r_into_rtrancl,wf_cs9,method_over_ok_lemma] addss
(simpset() addsimps [dyn_class_not_None,d_superclass_rel_def])) 0 1);
**)
qed_spec_mp "get_methods_super_impl_get_methods_obj";
goalw thy [method_impl_ok_def]
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS cn; method_impl_ok CFS cn mi; get_methods (CFS !! mi) (mn,pd) = Some (rd, ins) |] \
\ ==> is_class CFS (dyn_class (CFS, (mn,pd), cn)) & \
\ (dyn_class (CFS, (mn,pd), cn), cn) : (d_superclass_rel CFS)^* & \
\ (? ins'. get_methods (CFS !! dyn_class (CFS, (mn,pd), cn)) (mn,pd) = Some (rd, ins'))";
by (fast_tac (claset() addDs [get_methods_super_impl_get_methods_obj] addss (simpset())) 1);
qed_spec_mp "method_impl_ok_imp_dyn_class_lemma";
(****
goal thy
"!!dummy. \
\ wf_classfiles CFS \
\ --> wideRefConvertible CFS (AT at) (IT mi) \
\ --> get_methods (CFS !! mi) (mn,pd) = Some (rd,ins) \
\ --> dc=dyn_class (CFS, (mn,pd) , oc) \
\ --> is_class CFS dc & wideRefConvertible CFS (AT at) (CT dc) & \
\ (? ins'. get_methods (CFS !! dc) (mn,pd) = Some (rd,ins'))";
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "get_methods_inter_impl_get_methods3_AT";
(* gilt trivialerweise *)
****)
(** hier wird nicht "is_inter mi" benoetig, weil es schon in wRC=implements drinsteckt **)
goal thy
"!!dummy. \
\ wf_classfiles CFS \
\ --> implements (CFS, oc, mi) \
\ --> get_methods (CFS !! mi) (mn,pd) = Some (rd,ins) \
\ --> dc=dyn_class (CFS, (mn,pd) , oc) \
\ --> is_class CFS dc & (dc,oc) : (d_superclass_rel CFS)^* & \
\ (? ins'. get_methods (CFS !! dc) (mn,pd) = Some (rd,ins'))";
by (res_inst_tac [("u","CFS"),("v","oc"),("w","mi")] implements.induct 1);
br wf_implements_term_rel 1;
by (asm_full_simp_tac (simpset() addsimps [implements_term_rel_def,d_superclass_rel_def]) 1);
br impI 1;
br (implements_rec RS ssubst) 1;
ba 1;
by (Clarify_tac 1);
be disjE 1;
by (blast_tac (claset() addDs [method_impl_ok_imp_dyn_class_lemma,wf_cs7,d_implements_imp_class_inter]) 1);
be disjE 1;
by (deepen_tac (claset() addDs [method_impl_ok_imp_dyn_class_lemma,wf_cs8,d_implements_imp_class_inter]) 0 1);
by (case_tac "get_methods (CFS !! cn) (mn, pd) = None" 1);
by (fast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl] addss (simpset()
addsimps [wf_d_superclass_rel,dyn_class_None,d_superclass_imp_class])) 1);
by (fast_tac (claset() addIs [wf_cs10,method_over_ok_lemma,r_into_rtrancl] addss (simpset()
addsimps [dyn_class_not_None,d_superclass_imp_class])) 1);
qed_spec_mp "get_methods_inter_impl_get_methods_obj";
goal thy
"!!dummy ml. \
\[| wf_classfiles CFS; r:set rs; \
\ wideRefConvertible CFS (CT oc) r; inv_methref_ok CFS mci rs inv_com; is_class CFS oc |] \
\ ==> get_methods (CFS !! mci) ml = Some (rd,ins) \
\ --> dc=dyn_class (CFS, ml, oc) \
\ --> is_class CFS dc & (dc,oc) : (d_superclass_rel CFS)^* & \
\ (? ins'. get_methods (CFS !! dc) ml = Some (rd,ins'))";
by (exhaust_tac "inv_com" 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
br get_methods_super_impl_get_methods_obj 1;
ba 1;
ba 3;
be disjE 1;
by (fast_tac (claset() addDs [implements_impl_is_inter] addss (simpset() addsimps [in_superclass_rel_Object2])) 1);
by (fast_tac (claset() addDs [rtrancl_trans] addss (simpset() addsimps [])) 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
br get_methods_inter_impl_get_methods_obj 1;
ba 1;
ba 2;
be disjE 1;
by (Clarify_tac 1);
by (fast_tac (claset() addIs [implements_superinterface_trans2] addss (simpset())) 1);
by (Clarify_tac 1);
by (fast_tac (claset() addIs [implements_superclass_rel_trans2] addss (simpset())) 1);
br refl 1;
qed_spec_mp "inv_methref_ok_impl_get_methods_CT";
goal thy
"!!dummy ml. \
\[| wf_classfiles CFS; r:set rs; \
\ wideRefConvertible CFS (AT (fd2tys CFS fd)) r; inv_methref_ok CFS mci rs inv_com |] \
\ ==> get_methods (CFS !! mci) ml = Some (rd,ins) \
\ --> dc=dyn_class (CFS, ml, Object) \
\ --> dc=Object & \
\ (? ins'. get_methods (CFS !! dc) ml = Some (rd,ins'))";
by (exhaust_tac "inv_com" 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
be disjE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (forward_tac [in_superclasses_not_Object3] 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
be disjE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addDs [not_implements_Object]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "inv_methref_ok_impl_get_methods_AT";
goal thy
"!!dummy ml. \
\[| wf_classfiles CFS; r:set rs; \
\ wideRefConvertible CFS (AT (fd2tys CFS fd)) r; inv_methref_ok CFS mci rs inv_com |] \
\ ==> get_methods (CFS !! mci) ml = Some (rd,ins) \
\ --> dc=dyn_class (CFS, ml, Object) \
\ --> is_class CFS dc & wideRefConvertible CFS (AT (fd2tys CFS fd)) (CT dc) & \
\ (? ins'. get_methods (CFS !! dc) ml = Some (rd,ins'))";
by (exhaust_tac "inv_com" 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
be disjE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (forward_tac [in_superclasses_not_Object3] 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","r")] ballE 1);
by (Fast_tac 2);
be disjE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addDs [not_implements_Object]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "inv_methref_ok_impl_get_methods_AT";