|
1 (* Title: HOL/BNF/Tools/bnf_lfp_util.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Library for the datatype construction. |
|
7 *) |
|
8 |
|
9 signature BNF_LFP_UTIL = |
|
10 sig |
|
11 val HOL_arg_cong: cterm -> thm |
|
12 |
|
13 val mk_bij_betw: term -> term -> term -> term |
|
14 val mk_cardSuc: term -> term |
|
15 val mk_convol: term * term -> term |
|
16 val mk_cpow: term -> term |
|
17 val mk_inver: term -> term -> term -> term |
|
18 val mk_not_empty: term -> term |
|
19 val mk_not_eq: term -> term -> term |
|
20 val mk_rapp: term -> typ -> term |
|
21 val mk_relChain: term -> term -> term |
|
22 val mk_underS: term -> term |
|
23 val mk_worec: term -> term -> term |
|
24 end; |
|
25 |
|
26 structure BNF_LFP_Util : BNF_LFP_UTIL = |
|
27 struct |
|
28 |
|
29 open BNF_Util |
|
30 |
|
31 fun HOL_arg_cong ct = Drule.instantiate' |
|
32 (map SOME (Thm.dest_ctyp (Thm.ctyp_of_term ct))) [NONE, NONE, SOME ct] arg_cong; |
|
33 |
|
34 (*reverse application*) |
|
35 fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg); |
|
36 |
|
37 fun mk_underS r = |
|
38 let val T = fst (dest_relT (fastype_of r)); |
|
39 in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end; |
|
40 |
|
41 fun mk_worec r f = |
|
42 let val (A, AB) = apfst domain_type (dest_funT (fastype_of f)); |
|
43 in Const (@{const_name wo_rel.worec}, mk_relT (A, A) --> (AB --> AB) --> AB) $ r $ f end; |
|
44 |
|
45 fun mk_relChain r f = |
|
46 let val (A, AB) = `domain_type (fastype_of f); |
|
47 in Const (@{const_name relChain}, mk_relT (A, A) --> AB --> HOLogic.boolT) $ r $ f end; |
|
48 |
|
49 fun mk_cardSuc r = |
|
50 let val T = fst (dest_relT (fastype_of r)); |
|
51 in Const (@{const_name cardSuc}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end; |
|
52 |
|
53 fun mk_cpow r = |
|
54 let val T = fst (dest_relT (fastype_of r)); |
|
55 in Const (@{const_name cpow}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end; |
|
56 |
|
57 fun mk_bij_betw f A B = |
|
58 Const (@{const_name bij_betw}, |
|
59 fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B; |
|
60 |
|
61 fun mk_inver f g A = |
|
62 Const (@{const_name inver}, fastype_of f --> fastype_of g --> fastype_of A --> HOLogic.boolT) $ |
|
63 f $ g $ A; |
|
64 |
|
65 fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y)); |
|
66 |
|
67 fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []); |
|
68 |
|
69 fun mk_convol (f, g) = |
|
70 let |
|
71 val (fU, fTU) = `range_type (fastype_of f); |
|
72 val ((gT, gU), gTU) = `dest_funT (fastype_of g); |
|
73 val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU); |
|
74 in Const (@{const_name convol}, convolT) $ f $ g end; |
|
75 |
|
76 end; |