1068 end) |
1068 end) |
1069 *} |
1069 *} |
1070 |
1070 |
1071 section {* General outline of the lifting procedure *} |
1071 section {* General outline of the lifting procedure *} |
1072 |
1072 |
1073 |
|
1074 (* **************************************** *) |
|
1075 (* *) |
|
1076 (* - A is the original raw theorem *) |
1073 (* - A is the original raw theorem *) |
1077 (* - B is the regularized theorem *) |
1074 (* - B is the regularized theorem *) |
1078 (* - C is the rep/abs injected version of B *) |
1075 (* - C is the rep/abs injected version of B *) |
1079 (* - D is the lifted theorem *) |
1076 (* - D is the lifted theorem *) |
1080 (* *) |
1077 (* *) |
1081 (* - b is the regularization step *) |
1078 (* - b is the regularization step *) |
1082 (* - c is the rep/abs injection step *) |
1079 (* - c is the rep/abs injection step *) |
1083 (* - d is the cleaning part *) |
1080 (* - d is the cleaning part *) |
1084 |
1081 |
1085 lemma procedure: |
1082 lemma lifting_procedure: |
1086 assumes a: "A" |
1083 assumes a: "A" |
1087 and b: "A \<Longrightarrow> B" |
1084 and b: "A \<Longrightarrow> B" |
1088 and c: "B = C" |
1085 and c: "B = C" |
1089 and d: "C = D" |
1086 and d: "C = D" |
1090 shows "D" |
1087 shows "D" |
1117 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1114 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1118 in |
1115 in |
1119 Drule.instantiate' [] |
1116 Drule.instantiate' [] |
1120 [SOME (cterm_of thy rtrm'), |
1117 [SOME (cterm_of thy rtrm'), |
1121 SOME (cterm_of thy reg_goal), |
1118 SOME (cterm_of thy reg_goal), |
1122 SOME (cterm_of thy inj_goal)] @{thm procedure} |
1119 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1123 end |
1120 end |
1124 *} |
1121 *} |
1125 |
1122 |
1126 (* Left for debugging *) |
1123 (* Left for debugging *) |
1127 ML {* |
1124 ML {* |
1136 EVERY1 [rtac rule, rtac rthm'] |
1133 EVERY1 [rtac rule, rtac rthm'] |
1137 end) lthy |
1134 end) lthy |
1138 *} |
1135 *} |
1139 |
1136 |
1140 ML {* |
1137 ML {* |
|
1138 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1141 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1139 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1142 ObjectLogic.full_atomize_tac |
1140 ObjectLogic.full_atomize_tac |
1143 THEN' gen_frees_tac lthy |
1141 THEN' gen_frees_tac lthy |
1144 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1142 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1145 let |
1143 let |
1146 val rthm' = atomize_thm rthm |
1144 val rthm' = atomize_thm rthm |
1147 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1145 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1148 val aps = find_aps (prop_of rthm') (term_of concl) |
1146 val aps = find_aps (prop_of rthm') (term_of concl) |
1149 in |
1147 in |
1150 EVERY1 [rtac rule, |
1148 EVERY1 |
1151 RANGE [rtac rthm', |
1149 [rtac rule, |
1152 regularize_tac lthy [rel_eqv] rel_refl, |
1150 RANGE [rtac rthm', |
1153 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1151 regularize_tac lthy [rel_eqv] rel_refl, |
1154 clean_tac lthy quot defs reps_same absrep aps]] |
1152 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
|
1153 clean_tac lthy quot defs reps_same absrep aps]] |
1155 end) lthy |
1154 end) lthy |
1156 *} |
1155 *} |
1157 |
1156 |
1158 end |
1157 end |
1159 |
1158 |