equal
deleted
inserted
replaced
1 (* Title: quotient_term.thy |
1 (* Title: HOL/Tools/Quotient/quotient_term.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Constructs terms corresponding to goals from |
4 Constructs terms corresponding to goals from lifting theorems to |
5 lifting theorems to quotient types. |
5 quotient types. |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TERM = |
8 signature QUOTIENT_TERM = |
9 sig |
9 sig |
10 exception LIFT_MATCH of string |
10 exception LIFT_MATCH of string |
263 |
263 |
264 fun is_eq (Const (@{const_name "op ="}, _)) = true |
264 fun is_eq (Const (@{const_name "op ="}, _)) = true |
265 | is_eq _ = false |
265 | is_eq _ = false |
266 |
266 |
267 fun mk_rel_compose (trm1, trm2) = |
267 fun mk_rel_compose (trm1, trm2) = |
268 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 |
268 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
269 |
269 |
270 fun get_relmap ctxt s = |
270 fun get_relmap ctxt s = |
271 let |
271 let |
272 val thy = ProofContext.theory_of ctxt |
272 val thy = ProofContext.theory_of ctxt |
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
777 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |
777 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |
778 in |
778 in |
779 lift_aux t |
779 lift_aux t |
780 end |
780 end |
781 |
781 |
782 |
|
783 end; (* structure *) |
782 end; (* structure *) |
784 |
|
785 |
|
786 |
|