185 | dest_mem t = raise TERM ("dest_mem", [t]); |
185 | dest_mem t = raise TERM ("dest_mem", [t]); |
186 |
186 |
187 |
187 |
188 (* logic *) |
188 (* logic *) |
189 |
189 |
190 val Trueprop = Const (@{const_name Trueprop}, boolT --> propT); |
190 val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT); |
191 |
191 |
192 fun mk_Trueprop P = Trueprop $ P; |
192 fun mk_Trueprop P = Trueprop $ P; |
193 |
193 |
194 fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P |
194 fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P |
195 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
195 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); |
196 |
196 |
197 fun Trueprop_conv cv ct = |
197 fun Trueprop_conv cv ct = |
198 (case Thm.term_of ct of |
198 (case Thm.term_of ct of |
199 Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
199 Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => Conv.arg_conv cv ct |
200 | _ => raise CTERM ("Trueprop_conv", [ct])) |
200 | _ => raise CTERM ("Trueprop_conv", [ct])) |
201 |
201 |
202 |
202 |
203 fun conj_intr ctxt thP thQ = |
203 fun conj_intr ctxt thP thQ = |
204 let |
204 let |
218 |
218 |
219 fun conj_elims ctxt th = |
219 fun conj_elims ctxt th = |
220 let val (th1, th2) = conj_elim ctxt th |
220 let val (th1, th2) = conj_elim ctxt th |
221 in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th]; |
221 in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th]; |
222 |
222 |
223 val conj = @{term HOL.conj} |
223 val conj = \<^term>\<open>HOL.conj\<close> |
224 and disj = @{term HOL.disj} |
224 and disj = \<^term>\<open>HOL.disj\<close> |
225 and imp = @{term implies} |
225 and imp = \<^term>\<open>implies\<close> |
226 and Not = @{term Not}; |
226 and Not = \<^term>\<open>Not\<close>; |
227 |
227 |
228 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
228 fun mk_conj (t1, t2) = conj $ t1 $ t2 |
229 and mk_disj (t1, t2) = disj $ t1 $ t2 |
229 and mk_disj (t1, t2) = disj $ t1 $ t2 |
230 and mk_imp (t1, t2) = imp $ t1 $ t2 |
230 and mk_imp (t1, t2) = imp $ t1 $ t2 |
231 and mk_not t = Not $ t; |
231 and mk_not t = Not $ t; |
255 | dest_not t = raise TERM ("dest_not", [t]); |
255 | dest_not t = raise TERM ("dest_not", [t]); |
256 |
256 |
257 |
257 |
258 fun conj_conv cv1 cv2 ct = |
258 fun conj_conv cv1 cv2 ct = |
259 (case Thm.term_of ct of |
259 (case Thm.term_of ct of |
260 Const (@{const_name HOL.conj}, _) $ _ $ _ => |
260 Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => |
261 Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
261 Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
262 | _ => raise CTERM ("conj_conv", [ct])); |
262 | _ => raise CTERM ("conj_conv", [ct])); |
263 |
263 |
264 |
264 |
265 fun eq_const T = Const (@{const_name HOL.eq}, T --> T --> boolT); |
265 fun eq_const T = Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> boolT); |
266 |
266 |
267 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
267 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u; |
268 |
268 |
269 fun dest_eq (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (lhs, rhs) |
269 fun dest_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = (lhs, rhs) |
270 | dest_eq t = raise TERM ("dest_eq", [t]) |
270 | dest_eq t = raise TERM ("dest_eq", [t]) |
271 |
271 |
272 fun eq_conv cv1 cv2 ct = |
272 fun eq_conv cv1 cv2 ct = |
273 (case Thm.term_of ct of |
273 (case Thm.term_of ct of |
274 Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
274 Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
275 | _ => raise CTERM ("eq_conv", [ct])); |
275 | _ => raise CTERM ("eq_conv", [ct])); |
276 |
276 |
277 |
277 |
278 fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT); |
278 fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT); |
279 fun mk_all (x, T, P) = all_const T $ absfree (x, T) P; |
279 fun mk_all (x, T, P) = all_const T $ absfree (x, T) P; |