renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
1 (* Title: HOL/BNF/Tools/bnf_gfp_util.ML
2 Author: Dmitriy Traytel, TU Muenchen
5 Library for the codatatype construction.
8 signature BNF_GFP_UTIL =
10 val mk_rec_simps: int -> thm -> thm list -> thm list list
12 val dest_listT: typ -> typ
14 val mk_Cons: term -> term -> term
15 val mk_Shift: term -> term -> term
16 val mk_Succ: term -> term -> term
17 val mk_Times: term * term -> term
18 val mk_append: term * term -> term
19 val mk_congruent: term -> term -> term
20 val mk_clists: term -> term
21 val mk_diag: term -> term
22 val mk_equiv: term -> term -> term
23 val mk_fromCard: term -> term -> term
24 val mk_list_rec: term -> term -> term
25 val mk_nat_rec: term -> term -> term
26 val mk_pickWP: term -> term -> term -> term -> term -> term
27 val mk_prefCl: term -> term
28 val mk_proj: term -> term
29 val mk_quotient: term -> term -> term
30 val mk_shift: term -> term -> term
31 val mk_size: term -> term
32 val mk_thePull: term -> term -> term -> term -> term
33 val mk_toCard: term -> term -> term
34 val mk_undefined: typ -> term
35 val mk_univ: term -> term
37 val mk_specN: int -> thm -> thm
39 val mk_InN_Field: int -> int -> thm
40 val mk_InN_inject: int -> int -> thm
41 val mk_InN_not_InM: int -> int -> thm
44 structure BNF_GFP_Util : BNF_GFP_UTIL =
49 val mk_append = HOLogic.mk_binop @{const_name append};
52 Const (@{const_name equiv}, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R;
56 val AT = fastype_of A;
57 val BT = fastype_of B;
58 val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT));
59 in Const (@{const_name Sigma}, AT --> BT --> ABT) $ A $ B end;
63 val AT = fastype_of A;
64 val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
65 in Const (@{const_name diag}, AT --> AAT) $ A end;
68 let val AT = HOLogic.dest_setT (fastype_of A);
69 in mk_Sigma (A, Term.absdummy AT B) end;
71 fun dest_listT (Type (@{type_name list}, [T])) = T
72 | dest_listT T = raise TYPE ("dest_setT: set type expected", [T], []);
75 let val T = fastype_of kl;
77 Const (@{const_name Succ},
78 HOLogic.mk_setT T --> T --> HOLogic.mk_setT (dest_listT T)) $ Kl $ kl
82 let val T = fastype_of Kl;
84 Const (@{const_name Shift}, T --> dest_listT (HOLogic.dest_setT T) --> T) $ Kl $ k
88 let val T = fastype_of lab;
90 Const (@{const_name shift}, T --> dest_listT (Term.domain_type T) --> T) $ lab $ k
94 Const (@{const_name prefCl}, fastype_of A --> HOLogic.boolT) $ A;
97 let val T = fastype_of r;
98 in Const (@{const_name clists}, T --> mk_relT (`I (HOLogic.listT (fst (dest_relT T))))) $ r end;
102 val AT = fastype_of A;
103 val rT = fastype_of r;
105 Const (@{const_name toCard},
106 AT --> rT --> HOLogic.dest_setT AT --> fst (dest_relT rT)) $ A $ r
109 fun mk_fromCard A r =
111 val AT = fastype_of A;
112 val rT = fastype_of r;
114 Const (@{const_name fromCard},
115 AT --> rT --> fst (dest_relT rT) --> HOLogic.dest_setT AT) $ A $ r
119 let val T = fastype_of xs;
120 in Const (@{const_name Cons}, dest_listT T --> T --> T) $ x $ xs end;
122 fun mk_size t = HOLogic.size_const (fastype_of t) $ t;
124 fun mk_quotient A R =
125 let val T = fastype_of A;
126 in Const (@{const_name quotient}, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end;
129 let val ((AT, BT), T) = `dest_relT (fastype_of R);
130 in Const (@{const_name proj}, T --> AT --> HOLogic.mk_setT BT) $ R end;
133 let val ((AT, BT), T) = `dest_funT (fastype_of f);
134 in Const (@{const_name univ}, T --> HOLogic.mk_setT AT --> BT) $ f end;
136 fun mk_congruent R f =
137 Const (@{const_name congruent}, fastype_of R --> fastype_of f --> HOLogic.boolT) $ R $ f;
139 fun mk_undefined T = Const (@{const_name undefined}, T);
141 fun mk_nat_rec Zero Suc =
142 let val T = fastype_of Zero;
143 in Const (@{const_name nat_rec}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
145 fun mk_list_rec Nil Cons =
147 val T = fastype_of Nil;
148 val (U, consT) = `(Term.domain_type) (fastype_of Cons);
150 Const (@{const_name list_rec}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons
153 fun mk_thePull B1 B2 f1 f2 =
155 val fT1 = fastype_of f1;
156 val fT2 = fastype_of f2;
157 val BT1 = domain_type fT1;
158 val BT2 = domain_type fT2;
160 Const (@{const_name thePull}, HOLogic.mk_setT BT1 --> HOLogic.mk_setT BT2 --> fT1 --> fT2 -->
161 mk_relT (BT1, BT2)) $ B1 $ B2 $ f1 $ f2
164 fun mk_pickWP A f1 f2 b1 b2 =
166 val fT1 = fastype_of f1;
167 val fT2 = fastype_of f2;
168 val AT = domain_type fT1;
169 val BT1 = range_type fT1;
170 val BT2 = range_type fT2;
172 Const (@{const_name pickWP}, HOLogic.mk_setT AT --> fT1 --> fT2 --> BT1 --> BT2 --> AT) $
173 A $ f1 $ f2 $ b1 $ b2
176 fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr}
177 | mk_InN_not_InM n m =
178 if n > m then mk_InN_not_InM m n RS @{thm not_sym}
179 else mk_InN_not_InM (n - 1) (m - 1) RS @{thm not_arg_cong_Inr};
181 fun mk_InN_Field 1 1 = @{thm TrueE[OF TrueI]}
182 | mk_InN_Field _ 1 = @{thm Inl_Field_csum}
183 | mk_InN_Field 2 2 = @{thm Inr_Field_csum}
184 | mk_InN_Field n m = mk_InN_Field (n - 1) (m - 1) RS @{thm Inr_Field_csum};
186 fun mk_InN_inject 1 _ = @{thm TrueE[OF TrueI]}
187 | mk_InN_inject _ 1 = @{thm Inl_inject}
188 | mk_InN_inject 2 2 = @{thm Inr_inject}
189 | mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1);
191 fun mk_specN 0 thm = thm
192 | mk_specN n thm = mk_specN (n - 1) (thm RS spec);
194 fun mk_rec_simps n rec_thm defs = map (fn i =>
195 map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);