958 in |
958 in |
959 t_eq |
959 t_eq |
960 end |
960 end |
961 *} |
961 *} |
962 |
962 |
|
963 ML {* |
|
964 fun applic_prs lthy rty qty absrep ty = |
|
965 let |
|
966 fun absty ty = |
|
967 old_exchange_ty rty qty ty |
|
968 fun mk_rep tm = |
|
969 let |
|
970 val ty = old_exchange_ty rty qty (fastype_of tm) |
|
971 in fst (old_get_fun repF rty qty lthy ty) $ tm end; |
|
972 fun mk_abs tm = |
|
973 let |
|
974 val ty = old_exchange_ty rty qty (fastype_of tm) in |
|
975 fst (old_get_fun absF rty qty lthy ty) $ tm end; |
|
976 val (l, ltl) = Term.strip_type ty; |
|
977 val nl = map absty l; |
|
978 val vs = map (fn _ => "x") l; |
|
979 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
|
980 val args = map Free (vfs ~~ nl); |
|
981 val lhs = list_comb((Free (fname, nl ---> ltl)), args); |
|
982 val rargs = map mk_rep args; |
|
983 val f = Free (fname, nl ---> ltl); |
|
984 val rhs = mk_abs (list_comb((mk_rep f), rargs)); |
|
985 val eq = Logic.mk_equals (rhs, lhs); |
|
986 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
|
987 val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps}); |
|
988 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
|
989 val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; |
|
990 in |
|
991 singleton (ProofContext.export lthy' lthy) t_id |
|
992 end |
|
993 *} |
963 |
994 |
964 ML {* |
995 ML {* |
965 fun lookup_quot_data lthy qty = |
996 fun lookup_quot_data lthy qty = |
966 let |
997 let |
967 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
998 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
979 fun lookup_quot_thms lthy qty_name = |
1010 fun lookup_quot_thms lthy qty_name = |
980 let |
1011 let |
981 val thy = ProofContext.theory_of lthy; |
1012 val thy = ProofContext.theory_of lthy; |
982 val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") |
1013 val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") |
983 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
1014 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
|
1015 val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") |
984 val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) |
1016 val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) |
985 in |
1017 in |
986 (trans2, reps_same, quot) |
1018 (trans2, reps_same, absrep, quot) |
987 end |
1019 end |
988 *} |
1020 *} |
989 |
1021 |
990 ML {* |
1022 ML {* |
991 fun lookup_quot_consts defs = |
1023 fun lookup_quot_consts defs = |
998 *} |
1030 *} |
999 |
1031 |
1000 ML {* |
1032 ML {* |
1001 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
1033 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
1002 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
1034 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
1003 val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name; |
1035 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
1004 val consts = lookup_quot_consts defs; |
1036 val consts = lookup_quot_consts defs; |
1005 val t_a = atomize_thm t; |
1037 val t_a = atomize_thm t; |
1006 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
1038 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
1007 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
1039 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
1008 val (alls, exs) = findallex rty qty (prop_of t_a); |
1040 val (alls, exs) = findallex rty qty (prop_of t_a); |
1009 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
1041 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
1010 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
1042 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
1011 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
1043 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
1012 val abs = findabs rty (prop_of t_a); |
1044 val abs = findabs rty (prop_of t_a); |
1013 val aps = findaps rty (prop_of t_a); |
1045 val aps = findaps rty (prop_of t_a); |
1014 val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps; |
1046 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
1015 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1047 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1016 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1048 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1017 val defs_sym = add_lower_defs lthy defs; |
1049 val defs_sym = add_lower_defs lthy defs; |
1018 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1050 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1019 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
1051 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |