1045 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
1045 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
1046 |
1046 |
1047 fun inst_spec_tac ctrms = |
1047 fun inst_spec_tac ctrms = |
1048 EVERY' (map (dtac o inst_spec) ctrms) |
1048 EVERY' (map (dtac o inst_spec) ctrms) |
1049 |
1049 |
1050 fun abs_list xs trm = |
1050 fun all_list xs trm = |
1051 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
1051 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
1052 |
1052 |
1053 fun apply_under_Trueprop f = |
1053 fun apply_under_Trueprop f = |
1054 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
1054 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
1055 |
1055 |
1057 SUBGOAL (fn (concl, i) => |
1057 SUBGOAL (fn (concl, i) => |
1058 let |
1058 let |
1059 val thy = ProofContext.theory_of ctxt |
1059 val thy = ProofContext.theory_of ctxt |
1060 val vrs = Term.add_frees concl [] |
1060 val vrs = Term.add_frees concl [] |
1061 val cvrs = map (cterm_of thy o Free) vrs |
1061 val cvrs = map (cterm_of thy o Free) vrs |
1062 val concl' = apply_under_Trueprop (abs_list vrs) concl |
1062 val concl' = apply_under_Trueprop (all_list vrs) concl |
1063 val goal = Logic.mk_implies (concl', concl) |
1063 val goal = Logic.mk_implies (concl', concl) |
1064 val rule = Goal.prove ctxt [] [] goal |
1064 val rule = Goal.prove ctxt [] [] goal |
1065 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
1065 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
1066 in |
1066 in |
1067 rtac rule i |
1067 rtac rule i |
1090 shows "D" |
1090 shows "D" |
1091 using a b c d |
1091 using a b c d |
1092 by simp |
1092 by simp |
1093 |
1093 |
1094 ML {* |
1094 ML {* |
1095 fun lift_error ctxt fun_str rtrm qtrm = |
1095 fun lift_match_error ctxt fun_str rtrm qtrm = |
1096 let |
1096 let |
1097 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1097 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1098 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1098 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1099 val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
1099 val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
1100 "and the lifted theorem\n", rtrm_str, "do not match"] |
1100 "and the lifted theorem\n", rtrm_str, "do not match"] |
1109 val thy = ProofContext.theory_of ctxt |
1109 val thy = ProofContext.theory_of ctxt |
1110 val rtrm' = HOLogic.dest_Trueprop rtrm |
1110 val rtrm' = HOLogic.dest_Trueprop rtrm |
1111 val qtrm' = HOLogic.dest_Trueprop qtrm |
1111 val qtrm' = HOLogic.dest_Trueprop qtrm |
1112 val reg_goal = |
1112 val reg_goal = |
1113 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1113 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1114 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1114 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1115 val inj_goal = |
1115 val inj_goal = |
1116 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1116 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1117 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm |
1117 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1118 in |
1118 in |
1119 Drule.instantiate' [] |
1119 Drule.instantiate' [] |
1120 [SOME (cterm_of thy rtrm'), |
1120 [SOME (cterm_of thy rtrm'), |
1121 SOME (cterm_of thy reg_goal), |
1121 SOME (cterm_of thy reg_goal), |
1122 SOME (cterm_of thy inj_goal)] |
1122 SOME (cterm_of thy inj_goal)] @{thm procedure} |
1123 @{thm procedure} |
|
1124 end |
1123 end |
1125 *} |
1124 *} |
1126 |
1125 |
1127 (* Left for debugging *) |
1126 (* Left for debugging *) |
1128 ML {* |
1127 ML {* |
1132 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1131 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1133 let |
1132 let |
1134 val rthm' = atomize_thm rthm |
1133 val rthm' = atomize_thm rthm |
1135 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1134 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1136 in |
1135 in |
1137 rtac rule THEN' rtac rthm' |
1136 EVERY1 [rtac rule, rtac rthm'] |
1138 end 1) lthy |
1137 end) lthy |
1139 *} |
1138 *} |
1140 |
1139 |
1141 ML {* |
1140 ML {* |
1142 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1141 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1143 ObjectLogic.full_atomize_tac |
1142 ObjectLogic.full_atomize_tac |
1146 let |
1145 let |
1147 val rthm' = atomize_thm rthm |
1146 val rthm' = atomize_thm rthm |
1148 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1147 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1149 val aps = find_aps (prop_of rthm') (term_of concl) |
1148 val aps = find_aps (prop_of rthm') (term_of concl) |
1150 in |
1149 in |
1151 rtac rule THEN' |
1150 EVERY1 [rtac rule, |
1152 RANGE [rtac rthm', |
1151 RANGE [rtac rthm', |
1153 regularize_tac lthy [rel_eqv] rel_refl, |
1152 regularize_tac lthy [rel_eqv] rel_refl, |
1154 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1153 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1155 clean_tac lthy quot defs reps_same absrep aps] |
1154 clean_tac lthy quot defs reps_same absrep aps]] |
1156 end 1) lthy |
1155 end) lthy |
1157 *} |
1156 *} |
1158 |
1157 |
1159 end |
1158 end |
1160 |
1159 |
1161 |
1160 |