1067 end |
1072 end |
1068 *} |
1073 *} |
1069 |
1074 |
1070 |
1075 |
1071 ML {* |
1076 ML {* |
1072 fun lift_thm lthy qty qty_name rsp_thms defs t = let |
1077 fun lift_thm lthy qty qty_name rsp_thms defs rthm = let |
|
1078 val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) |
|
1079 |
1073 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
1080 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
1074 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
1081 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
1075 val consts = lookup_quot_consts defs; |
1082 val consts = lookup_quot_consts defs; |
1076 val t_a = atomize_thm t; |
1083 val t_a = atomize_thm rthm; |
|
1084 |
|
1085 val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) |
|
1086 |
1077 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
1087 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
|
1088 |
|
1089 val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) |
|
1090 |
1078 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
1091 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
|
1092 |
|
1093 val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) |
|
1094 |
1079 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
1095 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
1080 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
1096 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
1081 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
1097 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
1082 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
1098 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
1099 |
|
1100 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) |
|
1101 |
1083 val abs = findabs rty (prop_of t_a); |
1102 val abs = findabs rty (prop_of t_a); |
1084 val aps = findaps rty (prop_of t_a); |
1103 val aps = findaps rty (prop_of t_a); |
1085 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
1104 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
1086 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1105 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
1087 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
1106 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
1107 |
|
1108 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) |
|
1109 |
1088 val defs_sym = flat (map (add_lower_defs lthy) defs); |
1110 val defs_sym = flat (map (add_lower_defs lthy) defs); |
1089 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1111 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1090 val t_id = simp_ids lthy t_l; |
1112 val t_id = simp_ids lthy t_l; |
|
1113 |
|
1114 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) |
|
1115 |
1091 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
1116 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
1117 |
|
1118 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) |
|
1119 |
1092 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1120 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
1121 |
|
1122 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) |
|
1123 |
1093 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
1124 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
1125 |
|
1126 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) |
|
1127 |
1094 val t_rv = ObjectLogic.rulify t_r |
1128 val t_rv = ObjectLogic.rulify t_r |
|
1129 |
|
1130 val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv)) |
1095 in |
1131 in |
1096 Thm.varifyT t_rv |
1132 Thm.varifyT t_rv |
1097 end |
1133 end |
1098 *} |
1134 *} |
1099 |
1135 |