49 Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T) |
49 Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T) |
50 |
50 |
51 fun mk_inv_of ctxt ct = |
51 fun mk_inv_of ctxt ct = |
52 let |
52 let |
53 val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) |
53 val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) |
54 val inv = Proof_Context.cterm_of ctxt (mk_inv_into dT rT) |
54 val inv = Thm.cterm_of ctxt (mk_inv_into dT rT) |
55 val univ = Proof_Context.cterm_of ctxt (mk_univ dT) |
55 val univ = Thm.cterm_of ctxt (mk_univ dT) |
56 in Thm.mk_binop inv univ ct end |
56 in Thm.mk_binop inv univ ct end |
57 |
57 |
58 fun mk_inj_prop ctxt ct = |
58 fun mk_inj_prop ctxt ct = |
59 let |
59 let |
60 val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) |
60 val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) |
61 val inj = Proof_Context.cterm_of ctxt (mk_inj_on dT rT) |
61 val inj = Thm.cterm_of ctxt (mk_inj_on dT rT) |
62 val univ = Proof_Context.cterm_of ctxt (mk_univ dT) |
62 val univ = Thm.cterm_of ctxt (mk_univ dT) |
63 in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end |
63 in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end |
64 |
64 |
65 |
65 |
66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
67 |
67 |