948 end |
948 end |
949 handle _ => thm |
949 handle _ => thm |
950 *} |
950 *} |
951 |
951 |
952 ML {* |
952 ML {* |
953 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let |
953 fun lookup_quot_data lthy qty = |
|
954 let |
|
955 val SOME quotdata = find_first (fn x => #qtyp x = qty) (quotdata_lookup lthy) |
|
956 val rty = #rtyp quotdata |
|
957 val rel = #rel quotdata |
|
958 val rel_eqv = #equiv_thm quotdata |
|
959 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv] |
|
960 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] |
|
961 in |
|
962 (rty, rel, rel_refl, rel_eqv) |
|
963 end |
|
964 *} |
|
965 |
|
966 ML {* |
|
967 fun lookup_quot_thms lthy qty_name = |
|
968 let |
|
969 val thy = ProofContext.theory_of lthy; |
|
970 val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") |
|
971 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
|
972 val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) |
|
973 in |
|
974 (trans2, reps_same, quot) |
|
975 end |
|
976 *} |
|
977 |
|
978 ML {* |
|
979 fun lookup_quot_consts defs = |
|
980 let |
|
981 fun dest_term (a $ b) = (a, b); |
|
982 val def_terms = map (snd o Logic.dest_equals o concl_of) defs; |
|
983 in |
|
984 map (fst o dest_Const o snd o dest_term) def_terms |
|
985 end |
|
986 *} |
|
987 |
|
988 ML {* |
|
989 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
|
990 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
|
991 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
|
992 val consts = lookup_quot_consts defs; |
954 val t_a = atomize_thm t; |
993 val t_a = atomize_thm t; |
955 val t_r = regularize t_a rty rel rel_eqv lthy; |
994 val t_r = regularize t_a rty rel rel_eqv lthy; |
956 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
995 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
957 val abs = findabs rty (prop_of t_a); |
996 val abs = findabs rty (prop_of t_a); |
958 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
997 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
959 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
998 val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; |
960 val t_a = simp_allex_prs lthy quot t_l; |
999 val t_a = simp_allex_prs lthy quot t_l; |
961 val t_defs_sym = add_lower_defs lthy t_defs; |
1000 val defs_sym = add_lower_defs lthy defs; |
962 val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a; |
1001 val t_d = repeat_eqsubst_thm lthy defs_sym t_a; |
963 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
1002 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
964 in |
1003 in |
965 ObjectLogic.rulify t_r |
1004 ObjectLogic.rulify t_r |
966 end |
1005 end |
967 *} |
1006 *} |
968 |
1007 |
969 end |
1008 |
|
1009 end |
|
1010 |