equal
deleted
inserted
replaced
33 |
33 |
34 val ctwo: term |
34 val ctwo: term |
35 val fst_const: typ -> term |
35 val fst_const: typ -> term |
36 val snd_const: typ -> term |
36 val snd_const: typ -> term |
37 val Id_const: typ -> term |
37 val Id_const: typ -> term |
|
38 |
|
39 val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term |
38 |
40 |
39 val mk_Ball: term -> term -> term |
41 val mk_Ball: term -> term -> term |
40 val mk_Bex: term -> term -> term |
42 val mk_Bex: term -> term -> term |
41 val mk_Card_order: term -> term |
43 val mk_Card_order: term -> term |
42 val mk_Field: term -> term |
44 val mk_Field: term -> term |
219 fun Id_const T = Const (@{const_name Id}, mk_relT (T, T)); |
221 fun Id_const T = Const (@{const_name Id}, mk_relT (T, T)); |
220 |
222 |
221 |
223 |
222 (** Operators **) |
224 (** Operators **) |
223 |
225 |
|
226 fun enforce_type ctxt get_T T t = |
|
227 Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t; |
|
228 |
224 fun mk_converse R = |
229 fun mk_converse R = |
225 let |
230 let |
226 val RT = dest_relT (fastype_of R); |
231 val RT = dest_relT (fastype_of R); |
227 val RST = mk_relT (snd RT, fst RT); |
232 val RST = mk_relT (snd RT, fst RT); |
228 in Const (@{const_name converse}, fastype_of R --> RST) $ R end; |
233 in Const (@{const_name converse}, fastype_of R --> RST) $ R end; |