13 val boolN: string |
13 val boolN: string |
14 val boolT: typ |
14 val boolT: typ |
15 val Trueprop: term |
15 val Trueprop: term |
16 val mk_Trueprop: term -> term |
16 val mk_Trueprop: term -> term |
17 val dest_Trueprop: term -> term |
17 val dest_Trueprop: term -> term |
|
18 val Trueprop_conv: conv -> conv |
18 val mk_induct_forall: typ -> term |
19 val mk_induct_forall: typ -> term |
19 val mk_setT: typ -> typ |
20 val mk_setT: typ -> typ |
20 val dest_setT: typ -> typ |
21 val dest_setT: typ -> typ |
21 val Collect_const: typ -> term |
22 val Collect_const: typ -> term |
22 val mk_Collect: string * typ * term -> term |
23 val mk_Collect: string * typ * term -> term |
193 | dest_mem t = raise TERM ("dest_mem", [t]); |
194 | dest_mem t = raise TERM ("dest_mem", [t]); |
194 |
195 |
195 |
196 |
196 (* logic *) |
197 (* logic *) |
197 |
198 |
198 val Trueprop = Const ("HOL.Trueprop", boolT --> propT); |
199 val Trueprop = Const (@{const_name Trueprop}, boolT --> propT); |
199 |
200 |
200 fun mk_Trueprop P = Trueprop $ P; |
201 fun mk_Trueprop P = Trueprop $ P; |
201 |
202 |
202 fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P |
203 fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P |
203 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
204 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
|
205 |
|
206 fun Trueprop_conv cv ct = |
|
207 (case Thm.term_of ct of |
|
208 Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
|
209 | _ => raise CTERM ("Trueprop_conv", [ct])) |
|
210 |
204 |
211 |
205 fun conj_intr thP thQ = |
212 fun conj_intr thP thQ = |
206 let |
213 let |
207 val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ) |
214 val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ) |
208 handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); |
215 handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); |