555 end |
555 end |
556 handle TYPE _ => [] |
556 handle TYPE _ => [] |
557 *} |
557 *} |
558 |
558 |
559 ML {* |
559 ML {* |
560 fun get_fun_new flag (rty, qty) lthy ty = |
560 fun negF absF = repF |
|
561 | negF repF = absF |
|
562 |
|
563 fun get_fun flag qenv lthy ty = |
|
564 let |
|
565 |
|
566 fun get_fun_aux s fs = |
|
567 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
|
568 SOME info => list_comb (Const (#mapfun info, dummyT), fs) |
|
569 | NONE => error ("no map association for type " ^ s)) |
|
570 |
|
571 fun get_const flag qty = |
|
572 let |
|
573 val thy = ProofContext.theory_of lthy |
|
574 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
575 in |
|
576 case flag of |
|
577 absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) |
|
578 | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) |
|
579 end |
|
580 |
|
581 fun mk_identity ty = Abs ("", ty, Bound 0) |
|
582 |
|
583 in |
|
584 if (AList.defined (op=) qenv ty) |
|
585 then (get_const flag ty) |
|
586 else (case ty of |
|
587 TFree _ => mk_identity ty |
|
588 | Type (_, []) => mk_identity ty |
|
589 | Type ("fun" , [ty1, ty2]) => |
|
590 let |
|
591 val fs_ty1 = get_fun (negF flag) qenv lthy ty1 |
|
592 val fs_ty2 = get_fun flag qenv lthy ty2 |
|
593 in |
|
594 get_fun_aux "fun" [fs_ty1, fs_ty2] |
|
595 end |
|
596 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
|
597 | _ => error ("no type variables allowed")) |
|
598 end |
|
599 |
|
600 (* returns all subterms where two types differ *) |
|
601 fun diff (T, S) Ds = |
|
602 case (T, S) of |
|
603 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
|
604 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
|
605 | (Type (a, Ts), Type (b, Us)) => |
|
606 if a = b then diffs (Ts, Us) Ds else (T, S)::Ds |
|
607 | _ => (T, S)::Ds |
|
608 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
|
609 | diffs ([], []) Ds = Ds |
|
610 | diffs _ _ = error "Unequal length of type arguments" |
|
611 |
|
612 *} |
|
613 |
|
614 ML {* |
|
615 fun get_fun_OLD flag (rty, qty) lthy ty = |
561 let |
616 let |
562 val tys = find_matching_types rty ty; |
617 val tys = find_matching_types rty ty; |
563 val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; |
618 val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; |
564 val xchg_ty = exchange_ty lthy rty qty ty |
619 val xchg_ty = exchange_ty lthy rty qty ty |
565 in |
620 in |
655 val qty = Logic.varifyT qty; |
710 val qty = Logic.varifyT qty; |
656 |
711 |
657 fun mk_abs tm = |
712 fun mk_abs tm = |
658 let |
713 let |
659 val ty = fastype_of tm |
714 val ty = fastype_of tm |
660 in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end |
715 in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end |
661 fun mk_repabs tm = |
716 fun mk_repabs tm = |
662 let |
717 let |
663 val ty = fastype_of tm |
718 val ty = fastype_of tm |
664 in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end |
719 in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end |
665 |
720 |
666 fun is_lifted_const (Const (x, _)) = member (op =) consts x |
721 fun is_lifted_const (Const (x, _)) = member (op =) consts x |
667 | is_lifted_const _ = false; |
722 | is_lifted_const _ = false; |
668 |
723 |
669 fun build_aux lthy tm = |
724 fun build_aux lthy tm = |
1006 fun absty ty = |
1061 fun absty ty = |
1007 exchange_ty lthy rty qty ty |
1062 exchange_ty lthy rty qty ty |
1008 fun mk_rep tm = |
1063 fun mk_rep tm = |
1009 let |
1064 let |
1010 val ty = exchange_ty lthy qty rty (fastype_of tm) |
1065 val ty = exchange_ty lthy qty rty (fastype_of tm) |
1011 in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end; |
1066 in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end; |
1012 fun mk_abs tm = |
1067 fun mk_abs tm = |
1013 let |
1068 let |
1014 val ty = fastype_of tm |
1069 val ty = fastype_of tm |
1015 in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end |
1070 in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end |
1016 val (l, ltl) = Term.strip_type ty; |
1071 val (l, ltl) = Term.strip_type ty; |
1017 val nl = map absty l; |
1072 val nl = map absty l; |
1018 val vs = map (fn _ => "x") l; |
1073 val vs = map (fn _ => "x") l; |
1019 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
1074 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
1020 val args = map Free (vfs ~~ nl); |
1075 val args = map Free (vfs ~~ nl); |
1190 | _ => f trm1 trm2 |
1244 | _ => f trm1 trm2 |
1191 |
1245 |
1192 fun qnt_typ ty = domain_type (domain_type ty) |
1246 fun qnt_typ ty = domain_type (domain_type ty) |
1193 *} |
1247 *} |
1194 |
1248 |
1195 ML {* |
1249 (* |
1196 fun REGULARIZE_aux lthy rtrm qtrm = |
1250 Regularizing an rterm means: |
|
1251 - Quantifiers over a type that needs lifting are replaced by |
|
1252 bounded quantifiers, for example: |
|
1253 \<forall>x. P \<Longrightarrow> \<forall>x\<in>(Respects R). P |
|
1254 - Abstractions over a type that needs lifting are replaced |
|
1255 by bounded abstractions: |
|
1256 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
|
1257 |
|
1258 - Equalities over the type being lifted are replaced by |
|
1259 appropriate relations: |
|
1260 A = B \<Longrightarrow> A \<approx> B |
|
1261 Example with more complicated types of A, B: |
|
1262 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
|
1263 *) |
|
1264 |
|
1265 ML {* |
|
1266 fun REGULARIZE_trm lthy rtrm qtrm = |
1197 case (rtrm, qtrm) of |
1267 case (rtrm, qtrm) of |
1198 (Abs (x, T, t), Abs (x', T', t')) => |
1268 (Abs (x, T, t), Abs (x', T', t')) => |
1199 let |
1269 let |
1200 val subtrm = REGULARIZE_aux lthy t t' |
1270 val subtrm = REGULARIZE_trm lthy t t' |
1201 in |
1271 in |
1202 if T = T' |
1272 if T = T' |
1203 then Abs (x, T, subtrm) |
1273 then Abs (x, T, subtrm) |
1204 else mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm |
1274 else mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm |
1205 end |
1275 end |
1206 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1276 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1207 let |
1277 let |
1208 val subtrm = apply_subt (REGULARIZE_aux lthy) t t' |
1278 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1209 in |
1279 in |
1210 if ty = ty' |
1280 if ty = ty' |
1211 then Const (@{const_name "All"}, ty) $ subtrm |
1281 then Const (@{const_name "All"}, ty) $ subtrm |
1212 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1282 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1213 end |
1283 end |
1214 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1284 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1215 let |
1285 let |
1216 val subtrm = apply_subt (REGULARIZE_aux lthy) t t' |
1286 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1217 in |
1287 in |
1218 if ty = ty' |
1288 if ty = ty' |
1219 then Const (@{const_name "Ex"}, ty) $ subtrm |
1289 then Const (@{const_name "Ex"}, ty) $ subtrm |
1220 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1290 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1221 end |
1291 end |
1222 (* FIXME: why is there a case for equality? is it correct? *) |
1292 (* FIXME: why is there a case for equality? is it correct? *) |
1223 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1293 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1224 let |
1294 let |
1225 val subtrm = REGULARIZE_aux lthy t t' |
1295 val subtrm = REGULARIZE_trm lthy t t' |
1226 in |
1296 in |
1227 if ty = ty' |
1297 if ty = ty' |
1228 then Const (@{const_name "op ="}, ty) $ subtrm |
1298 then Const (@{const_name "op ="}, ty) $ subtrm |
1229 else mk_resp_arg lthy (ty, ty') $ subtrm |
1299 else mk_resp_arg lthy (ty, ty') $ subtrm |
1230 end |
1300 end |
1231 | (t1 $ t2, t1' $ t2') => |
1301 | (t1 $ t2, t1' $ t2') => |
1232 (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2') |
1302 (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2') |
1233 | (Free (x, ty), Free (x', ty')) => |
1303 | (Free (x, ty), Free (x', ty')) => |
1234 if x = x' |
1304 if x = x' |
1235 then rtrm |
1305 then rtrm |
1236 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
1306 else raise LIFT_MATCH "quotient and lifted theorem do not match" |
1237 | (Bound i, Bound i') => |
1307 | (Bound i, Bound i') => |
1244 else rtrm (* FIXME: check correspondence according to definitions *) |
1314 else rtrm (* FIXME: check correspondence according to definitions *) |
1245 | _ => raise LIFT_MATCH "quotient and lifted theorem do not match" |
1315 | _ => raise LIFT_MATCH "quotient and lifted theorem do not match" |
1246 *} |
1316 *} |
1247 |
1317 |
1248 ML {* |
1318 ML {* |
1249 fun REGULARIZE_trm lthy rtrm qtrm = |
1319 fun mk_REGULARIZE_goal lthy rtrm qtrm = |
1250 REGULARIZE_aux lthy rtrm qtrm |
1320 Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy) |
1251 |> Syntax.check_term lthy |
1321 *} |
1252 |
1322 |
1253 *} |
1323 (* |
1254 |
1324 To prove that the old theorem implies the new one, we first |
|
1325 atomize it and then try: |
|
1326 - Reflexivity of the relation |
|
1327 - Assumption |
|
1328 - Elimnating quantifiers on both sides of toplevel implication |
|
1329 - Simplifying implications on both sides of toplevel implication |
|
1330 - Ball (Respects ?E) ?P = All ?P |
|
1331 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
|
1332 |
|
1333 *) |
|
1334 |
|
1335 lemma my_equiv_res_forall2: |
|
1336 fixes P::"'a \<Rightarrow> bool" |
|
1337 fixes Q::"'b \<Rightarrow> bool" |
|
1338 assumes a: "(All Q) \<longrightarrow> (All P)" |
|
1339 shows "(All Q) \<longrightarrow> Ball (Respects E) P" |
|
1340 using a by auto |
|
1341 |
|
1342 lemma my_equiv_res_exists: |
|
1343 fixes P::"'a \<Rightarrow> bool" |
|
1344 fixes Q::"'b \<Rightarrow> bool" |
|
1345 assumes a: "EQUIV E" |
|
1346 and b: "(Ex Q) \<longrightarrow> (Ex P)" |
|
1347 shows "(Ex Q) \<longrightarrow> Bex (Respects E) P" |
|
1348 apply(subst equiv_res_exists) |
|
1349 apply(rule a) |
|
1350 apply(rule b) |
|
1351 done |
|
1352 |
|
1353 ML {* |
|
1354 fun REGULARIZE_tac lthy rel_refl rel_eqv = |
|
1355 ObjectLogic.full_atomize_tac THEN' |
|
1356 REPEAT_ALL_NEW (FIRST' |
|
1357 [rtac rel_refl, |
|
1358 atac, |
|
1359 rtac @{thm universal_twice}, |
|
1360 rtac @{thm impI} THEN' atac, |
|
1361 rtac @{thm implication_twice}, |
|
1362 rtac @{thm my_equiv_res_forall2}, |
|
1363 rtac (rel_eqv RS @{thm my_equiv_res_exists}), |
|
1364 (* For a = b \<longrightarrow> a \<approx> b *) |
|
1365 rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, |
|
1366 rtac @{thm RIGHT_RES_FORALL_REGULAR}]) |
|
1367 *} |
|
1368 |
|
1369 (* same version including debugging information *) |
|
1370 ML {* |
|
1371 fun my_print_tac ctxt s thm = |
|
1372 let |
|
1373 val prems_str = prems_of thm |
|
1374 |> map (Syntax.string_of_term ctxt) |
|
1375 |> cat_lines |
|
1376 val _ = tracing (s ^ "\n" ^ prems_str) |
|
1377 in |
|
1378 Seq.single thm |
1255 end |
1379 end |
1256 |
1380 |
|
1381 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
|
1382 *} |
|
1383 |
|
1384 ML {* |
|
1385 fun REGULARIZE_tac' lthy rel_refl rel_eqv = |
|
1386 (REPEAT1 o FIRST1) |
|
1387 [(K (print_tac "start")) THEN' (K no_tac), |
|
1388 DT lthy "1" (rtac rel_refl), |
|
1389 DT lthy "2" atac, |
|
1390 DT lthy "3" (rtac @{thm universal_twice}), |
|
1391 DT lthy "4" (rtac @{thm impI} THEN' atac), |
|
1392 DT lthy "5" (rtac @{thm implication_twice}), |
|
1393 DT lthy "6" (rtac @{thm my_equiv_res_forall2}), |
|
1394 DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), |
|
1395 (* For a = b \<longrightarrow> a \<approx> b *) |
|
1396 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
1397 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
|
1398 *} |
|
1399 |
|
1400 ML {* |
|
1401 fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy = |
|
1402 let |
|
1403 val goal = mk_REGULARIZE_goal lthy rtrm qtrm |
|
1404 val cthm = Goal.prove lthy [] [] goal |
|
1405 (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1) |
|
1406 in |
|
1407 cthm |
|
1408 end |
|
1409 *} |
|
1410 |
|
1411 |
|
1412 end |
|
1413 |