equal
deleted
inserted
replaced
61 case flag of |
61 case flag of |
62 AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 |
62 AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 |
63 | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 |
63 | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 |
64 |
64 |
65 fun get_mapfun ctxt s = |
65 fun get_mapfun ctxt s = |
66 case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of |
66 (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of |
67 SOME map_data => Const (#mapfun map_data, dummyT) |
67 SOME map_data => Const (#mapfun map_data, dummyT) |
68 | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
68 | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) |
69 |
69 |
70 (* makes a Free out of a TVar *) |
70 (* makes a Free out of a TVar *) |
71 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
71 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
72 |
72 |
73 (* produces an aggregate map function for the |
73 (* produces an aggregate map function for the |
94 |
94 |
95 (* looks up the (varified) rty and qty for |
95 (* looks up the (varified) rty and qty for |
96 a quotient definition |
96 a quotient definition |
97 *) |
97 *) |
98 fun get_rty_qty ctxt s = |
98 fun get_rty_qty ctxt s = |
99 case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of |
99 case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of |
100 SOME qdata => (#rtyp qdata, #qtyp qdata) |
100 SOME qdata => (#rtyp qdata, #qtyp qdata) |
101 | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."); |
101 | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."); |
102 |
102 |
103 (* takes two type-environments and looks |
103 (* takes two type-environments and looks |
104 up in both of them the variable v, which |
104 up in both of them the variable v, which |
269 |
269 |
270 fun mk_rel_compose (trm1, trm2) = |
270 fun mk_rel_compose (trm1, trm2) = |
271 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
271 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
272 |
272 |
273 fun get_relmap ctxt s = |
273 fun get_relmap ctxt s = |
274 case Quotient_Info.maps_lookup (Proof_Context.theory_of ctxt) s of |
274 (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of |
275 SOME map_data => Const (#relmap map_data, dummyT) |
275 SOME map_data => Const (#relmap map_data, dummyT) |
276 | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
276 | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) |
277 |
277 |
278 fun mk_relmap ctxt vs rty = |
278 fun mk_relmap ctxt vs rty = |
279 let |
279 let |
280 val vs' = map (mk_Free) vs |
280 val vs' = map (mk_Free) vs |
281 |
281 |
288 in |
288 in |
289 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
289 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
290 end |
290 end |
291 |
291 |
292 fun get_equiv_rel ctxt s = |
292 fun get_equiv_rel ctxt s = |
293 case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of |
293 (case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of |
294 SOME qdata => #equiv_rel qdata |
294 SOME qdata => #equiv_rel qdata |
295 | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
295 | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")) |
296 |
296 |
297 fun equiv_match_err ctxt ty_pat ty = |
297 fun equiv_match_err ctxt ty_pat ty = |
298 let |
298 let |
299 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
299 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
300 val ty_str = Syntax.string_of_typ ctxt ty |
300 val ty_str = Syntax.string_of_typ ctxt ty |
425 (Type (rs, rtys), Type (qs, qtys)) => |
425 (Type (rs, rtys), Type (qs, qtys)) => |
426 if rs = qs then |
426 if rs = qs then |
427 if length rtys <> length qtys then false |
427 if length rtys <> length qtys then false |
428 else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
428 else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
429 else |
429 else |
430 (case Quotient_Info.quotdata_lookup thy qs of |
430 (case Quotient_Info.lookup_quotients thy qs of |
431 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
431 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
432 | NONE => false) |
432 | NONE => false) |
433 | _ => false) |
433 | _ => false) |
434 |
434 |
435 |
435 |
551 | same_const _ _ = false |
551 | same_const _ _ = false |
552 in |
552 in |
553 if same_const rtrm qtrm then rtrm |
553 if same_const rtrm qtrm then rtrm |
554 else |
554 else |
555 let |
555 let |
556 val rtrm' = case Quotient_Info.qconsts_lookup thy qtrm of |
556 val rtrm' = |
557 SOME qconst_info => #rconst qconst_info |
557 (case Quotient_Info.lookup_quotconsts thy qtrm of |
558 | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm |
558 SOME qconst_info => #rconst qconst_info |
|
559 | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) |
559 in |
560 in |
560 if Pattern.matches thy (rtrm', rtrm) |
561 if Pattern.matches thy (rtrm', rtrm) |
561 then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
562 then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
562 end |
563 end |
563 end |
564 end |
741 *) |
742 *) |
742 fun mk_ty_subst qtys direction ctxt = |
743 fun mk_ty_subst qtys direction ctxt = |
743 let |
744 let |
744 val thy = Proof_Context.theory_of ctxt |
745 val thy = Proof_Context.theory_of ctxt |
745 in |
746 in |
746 Quotient_Info.quotdata_dest ctxt |
747 Quotient_Info.dest_quotients ctxt |
747 |> map (fn x => (#rtyp x, #qtyp x)) |
748 |> map (fn x => (#rtyp x, #qtyp x)) |
748 |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) |
749 |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) |
749 |> map (if direction then swap else I) |
750 |> map (if direction then swap else I) |
750 end |
751 end |
751 |
752 |
753 let |
754 let |
754 val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) |
755 val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) |
755 fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 |
756 fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 |
756 |
757 |
757 val const_substs = |
758 val const_substs = |
758 Quotient_Info.qconsts_dest ctxt |
759 Quotient_Info.dest_quotconsts ctxt |
759 |> map (fn x => (#rconst x, #qconst x)) |
760 |> map (fn x => (#rconst x, #qconst x)) |
760 |> map (if direction then swap else I) |
761 |> map (if direction then swap else I) |
761 |
762 |
762 val rel_substs = |
763 val rel_substs = |
763 Quotient_Info.quotdata_dest ctxt |
764 Quotient_Info.dest_quotients ctxt |
764 |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) |
765 |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) |
765 |> map (if direction then swap else I) |
766 |> map (if direction then swap else I) |
766 in |
767 in |
767 filter proper (const_substs @ rel_substs) |
768 filter proper (const_substs @ rel_substs) |
768 end |
769 end |
785 |
786 |
786 fun derive_rtrm ctxt qtys qtrm = |
787 fun derive_rtrm ctxt qtys qtrm = |
787 subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm |
788 subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm |
788 |
789 |
789 |
790 |
790 end; (* structure *) |
791 end; |