1142 in |
1142 in |
1143 lthy2 |
1143 lthy2 |
1144 end |
1144 end |
1145 *} |
1145 *} |
1146 |
1146 |
1147 ML {* |
1147 (******************************************) |
1148 fun my_lift qtrm rthm lthy = |
1148 (* version with explicit qtrm *) |
|
1149 (******************************************) |
|
1150 |
|
1151 (* exception for when qtrm and rtrm do not match *) |
|
1152 ML {* exception LIFT_MATCH of string *} |
|
1153 |
|
1154 ML {* |
|
1155 fun mk_resp_arg lthy (rty, qty) = |
1149 let |
1156 let |
1150 val thy = ProofContext.theory_of lthy |
1157 val thy = ProofContext.theory_of lthy |
1151 |
1158 in |
1152 val a_rthm = atomize_thm rthm |
1159 case (rty, qty) of |
1153 val a_qtrm = ObjectLogic.atomize_term thy qtrm |
1160 (Type (s, tys), Type (s', tys')) => |
1154 |
1161 if s = s' |
1155 val _ = Syntax.string_of_term lthy (prop_of a_rthm) |> writeln |
1162 then let |
1156 val _ = Syntax.string_of_term lthy a_qtrm |> writeln |
1163 val SOME map_info = maps_lookup thy s |
1157 in |
1164 val args = map (mk_resp_arg lthy) (tys ~~tys') |
1158 (a_rthm, a_qtrm) |
1165 in |
|
1166 list_comb (Const (#relfun map_info, dummyT), args) |
|
1167 end |
|
1168 else let |
|
1169 val SOME qinfo = quotdata_lookup_thy thy s' |
|
1170 in |
|
1171 #rel qinfo |
|
1172 end |
|
1173 | _ => HOLogic.eq_const dummyT |
1159 end |
1174 end |
1160 *} |
1175 *} |
1161 |
1176 |
|
1177 ML {* |
|
1178 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
|
1179 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
|
1180 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
|
1181 val mk_resp = Const (@{const_name Respects}, dummyT) |
|
1182 *} |
|
1183 |
|
1184 ML {* |
|
1185 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
|
1186 (* abstracted variables do not have to be treated specially *) |
|
1187 fun apply_subt f trm1 trm2 = |
|
1188 case (trm1, trm2) of |
|
1189 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
|
1190 | _ => f trm1 trm2 |
|
1191 |
|
1192 fun qnt_typ ty = domain_type (domain_type ty) |
|
1193 *} |
|
1194 |
|
1195 ML {* |
|
1196 fun REGULARIZE_aux lthy rtrm qtrm = |
|
1197 case (rtrm, qtrm) of |
|
1198 (Abs (x, T, t), Abs (x', T', t')) => |
|
1199 let |
|
1200 val subtrm = REGULARIZE_aux lthy t t' |
|
1201 in |
|
1202 if T = T' |
|
1203 then Abs (x, T, subtrm) |
|
1204 else mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm |
|
1205 end |
|
1206 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
|
1207 let |
|
1208 val subtrm = apply_subt (REGULARIZE_aux lthy) t t' |
|
1209 in |
|
1210 if ty = ty' |
|
1211 then Const (@{const_name "All"}, ty) $ subtrm |
|
1212 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
1213 end |
|
1214 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
1215 let |
|
1216 val subtrm = apply_subt (REGULARIZE_aux lthy) t t' |
|
1217 in |
|
1218 if ty = ty' |
|
1219 then Const (@{const_name "Ex"}, ty) $ subtrm |
|
1220 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
1221 end |
|
1222 (* FIXME: why is there a case for equality? is it correct? *) |
|
1223 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
|
1224 let |
|
1225 val subtrm = REGULARIZE_aux lthy t t' |
|
1226 in |
|
1227 if ty = ty' |
|
1228 then Const (@{const_name "op ="}, ty) $ subtrm |
|
1229 else mk_resp_arg lthy (ty, ty') $ subtrm |
|
1230 end |
|
1231 | (t1 $ t2, t1' $ t2') => |
|
1232 (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2') |
|
1233 | (Free (x, ty), Free (x', ty')) => |
|
1234 if x = x' |
|
1235 then rtrm |
|
1236 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
|
1237 | (Bound i, Bound i') => |
|
1238 if i = i' |
|
1239 then rtrm |
|
1240 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
|
1241 | (Const (s, ty), Const (s', ty')) => |
|
1242 if s = s' andalso ty = ty' |
|
1243 then rtrm |
|
1244 else rtrm (* FIXME: check correspondence according to definitions *) |
|
1245 | _ => raise LIFT_MATCH "quotient and lifted theorem do not match" |
|
1246 *} |
|
1247 |
|
1248 ML {* |
|
1249 fun REGULARIZE_trm lthy rtrm qtrm = |
|
1250 REGULARIZE_aux lthy rtrm qtrm |
|
1251 |> Syntax.check_term lthy |
|
1252 |
|
1253 *} |
|
1254 |
1162 end |
1255 end |
1163 |
1256 |