|
1 (* Title: HOL/BNF/Tools/bnf_fp_def_sugar.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012, 2013 |
|
4 |
|
5 Sugared datatype and codatatype constructions. |
|
6 *) |
|
7 |
|
8 signature BNF_FP_DEF_SUGAR = |
|
9 sig |
|
10 type fp_sugar = |
|
11 {T: typ, |
|
12 fp: BNF_FP_Util.fp_kind, |
|
13 index: int, |
|
14 pre_bnfs: BNF_Def.bnf list, |
|
15 nested_bnfs: BNF_Def.bnf list, |
|
16 nesting_bnfs: BNF_Def.bnf list, |
|
17 fp_res: BNF_FP_Util.fp_result, |
|
18 ctr_defss: thm list list, |
|
19 ctr_sugars: Ctr_Sugar.ctr_sugar list, |
|
20 co_iterss: term list list, |
|
21 mapss: thm list list, |
|
22 co_inducts: thm list, |
|
23 co_iter_thmsss: thm list list list, |
|
24 disc_co_itersss: thm list list list, |
|
25 sel_co_iterssss: thm list list list list}; |
|
26 |
|
27 val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a |
|
28 val eq_fp_sugar: fp_sugar * fp_sugar -> bool |
|
29 val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar |
|
30 val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar |
|
31 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
|
32 val fp_sugars_of: Proof.context -> fp_sugar list |
|
33 |
|
34 val co_induct_of: 'a list -> 'a |
|
35 val strong_co_induct_of: 'a list -> 'a |
|
36 |
|
37 val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list |
|
38 val exists_subtype_in: typ list -> typ -> bool |
|
39 val flat_rec_arg_args: 'a list list -> 'a list |
|
40 val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list -> |
|
41 'a list |
|
42 val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term |
|
43 val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list |
|
44 |
|
45 type lfp_sugar_thms = |
|
46 (thm list * thm * Args.src list) |
|
47 * (thm list list * thm list list * Args.src list) |
|
48 |
|
49 val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms |
|
50 val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms |
|
51 |
|
52 type gfp_sugar_thms = |
|
53 ((thm list * thm) list * Args.src list) |
|
54 * (thm list list * thm list list * Args.src list) |
|
55 * (thm list list * thm list list * Args.src list) |
|
56 * (thm list list * thm list list * Args.src list) |
|
57 * (thm list list list * thm list list list * Args.src list) |
|
58 |
|
59 val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms |
|
60 val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms |
|
61 |
|
62 val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list -> |
|
63 int list -> int list list -> term list list -> Proof.context -> |
|
64 (term list list |
|
65 * (typ list list * typ list list list list * term list list |
|
66 * term list list list list) list option |
|
67 * (string * term list * term list list |
|
68 * ((term list list * term list list list) * (typ list * typ list list)) list) option) |
|
69 * Proof.context |
|
70 val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term -> |
|
71 typ list list list list |
|
72 val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term -> |
|
73 typ list list |
|
74 * (typ list list list list * typ list list list * typ list list list list * typ list) |
|
75 val define_iters: string list -> |
|
76 (typ list list * typ list list list list * term list list * term list list list list) list -> |
|
77 (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> |
|
78 (term list * thm list) * Proof.context |
|
79 val define_coiters: string list -> string * term list * term list list |
|
80 * ((term list list * term list list list) * (typ list * typ list list)) list -> |
|
81 (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> |
|
82 (term list * thm list) * Proof.context |
|
83 val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> |
|
84 (typ list list * typ list list list list * term list list * term list list list list) list -> |
|
85 thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
|
86 typ list -> typ list list list -> term list list -> thm list list -> term list list -> |
|
87 thm list list -> local_theory -> lfp_sugar_thms |
|
88 val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> |
|
89 string * term list * term list list * ((term list list * term list list list) |
|
90 * (typ list * typ list list)) list -> |
|
91 thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> |
|
92 typ list -> typ list list list -> int list list -> int list list -> int list -> thm list list -> |
|
93 Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) -> |
|
94 local_theory -> gfp_sugar_thms |
|
95 val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> |
|
96 binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> |
|
97 BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> |
|
98 (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) |
|
99 * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) * |
|
100 mixfix) list) list -> |
|
101 local_theory -> local_theory |
|
102 val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> |
|
103 binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> |
|
104 BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> |
|
105 (local_theory -> local_theory) parser |
|
106 end; |
|
107 |
|
108 structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = |
|
109 struct |
|
110 |
|
111 open Ctr_Sugar |
|
112 open BNF_Util |
|
113 open BNF_Comp |
|
114 open BNF_Def |
|
115 open BNF_FP_Util |
|
116 open BNF_FP_Def_Sugar_Tactics |
|
117 |
|
118 val EqN = "Eq_"; |
|
119 |
|
120 type fp_sugar = |
|
121 {T: typ, |
|
122 fp: fp_kind, |
|
123 index: int, |
|
124 pre_bnfs: bnf list, |
|
125 nested_bnfs: bnf list, |
|
126 nesting_bnfs: bnf list, |
|
127 fp_res: fp_result, |
|
128 ctr_defss: thm list list, |
|
129 ctr_sugars: ctr_sugar list, |
|
130 co_iterss: term list list, |
|
131 mapss: thm list list, |
|
132 co_inducts: thm list, |
|
133 co_iter_thmsss: thm list list list, |
|
134 disc_co_itersss: thm list list list, |
|
135 sel_co_iterssss: thm list list list list}; |
|
136 |
|
137 fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index; |
|
138 |
|
139 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
|
140 {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
|
141 T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
|
142 |
|
143 fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss, |
|
144 ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} |
|
145 : fp_sugar) = |
|
146 {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
|
147 nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs, |
|
148 fp_res = morph_fp_result phi fp_res, |
|
149 ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
|
150 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, |
|
151 co_iterss = map (map (Morphism.term phi)) co_iterss, |
|
152 mapss = map (map (Morphism.thm phi)) mapss, |
|
153 co_inducts = map (Morphism.thm phi) co_inducts, |
|
154 co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss, |
|
155 disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss, |
|
156 sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss}; |
|
157 |
|
158 val transfer_fp_sugar = |
|
159 morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; |
|
160 |
|
161 structure Data = Generic_Data |
|
162 ( |
|
163 type T = fp_sugar Symtab.table; |
|
164 val empty = Symtab.empty; |
|
165 val extend = I; |
|
166 val merge = Symtab.merge eq_fp_sugar; |
|
167 ); |
|
168 |
|
169 fun fp_sugar_of ctxt = |
|
170 Symtab.lookup (Data.get (Context.Proof ctxt)) |
|
171 #> Option.map (transfer_fp_sugar ctxt); |
|
172 |
|
173 fun fp_sugars_of ctxt = |
|
174 Symtab.fold (cons o transfer_fp_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) []; |
|
175 |
|
176 fun co_induct_of (i :: _) = i; |
|
177 fun strong_co_induct_of [_, s] = s; |
|
178 |
|
179 (* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *) |
|
180 |
|
181 fun register_fp_sugar key fp_sugar = |
|
182 Local_Theory.declaration {syntax = false, pervasive = true} |
|
183 (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar))); |
|
184 |
|
185 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss |
|
186 ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = |
|
187 (0, lthy) |
|
188 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
|
189 register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, |
|
190 nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, |
|
191 ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, |
|
192 co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss, |
|
193 sel_co_iterssss = sel_co_iterssss} |
|
194 lthy)) Ts |
|
195 |> snd; |
|
196 |
|
197 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
|
198 fun quasi_unambiguous_case_names names = |
|
199 let |
|
200 val ps = map (`Long_Name.base_name) names; |
|
201 val dups = Library.duplicates (op =) (map fst ps); |
|
202 fun underscore s = |
|
203 let val ss = space_explode Long_Name.separator s in |
|
204 space_implode "_" (drop (length ss - 2) ss) |
|
205 end; |
|
206 in |
|
207 map (fn (base, full) => if member (op =) dups base then underscore full else base) ps |
|
208 end; |
|
209 |
|
210 val id_def = @{thm id_def}; |
|
211 val mp_conj = @{thm mp_conj}; |
|
212 |
|
213 val nitpicksimp_attrs = @{attributes [nitpick_simp]}; |
|
214 val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs; |
|
215 val simp_attrs = @{attributes [simp]}; |
|
216 |
|
217 fun tvar_subst thy Ts Us = |
|
218 Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; |
|
219 |
|
220 val exists_subtype_in = Term.exists_subtype o member (op =); |
|
221 |
|
222 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); |
|
223 |
|
224 fun flat_rec_arg_args xss = |
|
225 (* FIXME (once the old datatype package is phased out): The first line below gives the preferred |
|
226 order. The second line is for compatibility with the old datatype package. *) |
|
227 (* |
|
228 flat xss |
|
229 *) |
|
230 map hd xss @ maps tl xss; |
|
231 |
|
232 fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss); |
|
233 |
|
234 fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss |
|
235 | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) = |
|
236 p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss; |
|
237 |
|
238 fun mk_tupled_fun x f xs = |
|
239 if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
|
240 |
|
241 fun mk_uncurried2_fun f xss = |
|
242 mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss); |
|
243 |
|
244 fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) = |
|
245 Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1)); |
|
246 |
|
247 fun flip_rels lthy n thm = |
|
248 let |
|
249 val Rs = Term.add_vars (prop_of thm) []; |
|
250 val Rs' = rev (drop (length Rs - n) Rs); |
|
251 val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs'; |
|
252 in |
|
253 Drule.cterm_instantiate cRs thm |
|
254 end; |
|
255 |
|
256 fun mk_ctor_or_dtor get_T Ts t = |
|
257 let val Type (_, Ts0) = get_T (fastype_of t) in |
|
258 Term.subst_atomic_types (Ts0 ~~ Ts) t |
|
259 end; |
|
260 |
|
261 val mk_ctor = mk_ctor_or_dtor range_type; |
|
262 val mk_dtor = mk_ctor_or_dtor domain_type; |
|
263 |
|
264 fun mk_co_iter thy fp fpT Cs t = |
|
265 let |
|
266 val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t); |
|
267 val fpT0 = fp_case fp prebody body; |
|
268 val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs); |
|
269 val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); |
|
270 in |
|
271 Term.subst_TVars rho t |
|
272 end; |
|
273 |
|
274 fun mk_co_iters thy fp fpTs Cs ts0 = |
|
275 let |
|
276 val nn = length fpTs; |
|
277 val (fpTs0, Cs0) = |
|
278 map ((fp = Greatest_FP ? swap) o dest_funT o snd o strip_typeN nn o fastype_of) ts0 |
|
279 |> split_list; |
|
280 val rho = tvar_subst thy (fpTs0 @ Cs0) (fpTs @ Cs); |
|
281 in |
|
282 map (Term.subst_TVars rho) ts0 |
|
283 end; |
|
284 |
|
285 val mk_fp_iter_fun_types = binder_fun_types o fastype_of; |
|
286 |
|
287 fun unzip_recT (Type (@{type_name prod}, _)) T = [T] |
|
288 | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts |
|
289 | unzip_recT _ T = [T]; |
|
290 |
|
291 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] |
|
292 | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts |
|
293 | unzip_corecT _ T = [T]; |
|
294 |
|
295 fun liveness_of_fp_bnf n bnf = |
|
296 (case T_of_bnf bnf of |
|
297 Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts |
|
298 | _ => replicate n false); |
|
299 |
|
300 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters"; |
|
301 |
|
302 fun merge_type_arg T T' = if T = T' then T else cannot_merge_types (); |
|
303 |
|
304 fun merge_type_args (As, As') = |
|
305 if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); |
|
306 |
|
307 fun reassoc_conjs thm = |
|
308 reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]}) |
|
309 handle THM _ => thm; |
|
310 |
|
311 fun type_args_named_constrained_of ((((ncAs, _), _), _), _) = ncAs; |
|
312 fun type_binding_of ((((_, b), _), _), _) = b; |
|
313 fun map_binding_of (((_, (b, _)), _), _) = b; |
|
314 fun rel_binding_of (((_, (_, b)), _), _) = b; |
|
315 fun mixfix_of ((_, mx), _) = mx; |
|
316 fun ctr_specs_of (_, ctr_specs) = ctr_specs; |
|
317 |
|
318 fun disc_of ((((disc, _), _), _), _) = disc; |
|
319 fun ctr_of ((((_, ctr), _), _), _) = ctr; |
|
320 fun args_of (((_, args), _), _) = args; |
|
321 fun defaults_of ((_, ds), _) = ds; |
|
322 fun ctr_mixfix_of (_, mx) = mx; |
|
323 |
|
324 fun add_nesty_bnf_names Us = |
|
325 let |
|
326 fun add (Type (s, Ts)) ss = |
|
327 let val (needs, ss') = fold_map add Ts ss in |
|
328 if exists I needs then (true, insert (op =) s ss') else (false, ss') |
|
329 end |
|
330 | add T ss = (member (op =) Us T, ss); |
|
331 in snd oo add end; |
|
332 |
|
333 fun nesty_bnfs ctxt ctr_Tsss Us = |
|
334 map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []); |
|
335 |
|
336 fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p; |
|
337 |
|
338 type lfp_sugar_thms = |
|
339 (thm list * thm * Args.src list) |
|
340 * (thm list list * thm list list * Args.src list) |
|
341 |
|
342 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) = |
|
343 ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs), |
|
344 (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs)); |
|
345 |
|
346 val transfer_lfp_sugar_thms = |
|
347 morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; |
|
348 |
|
349 type gfp_sugar_thms = |
|
350 ((thm list * thm) list * Args.src list) |
|
351 * (thm list list * thm list list * Args.src list) |
|
352 * (thm list list * thm list list * Args.src list) |
|
353 * (thm list list * thm list list * Args.src list) |
|
354 * (thm list list list * thm list list list * Args.src list); |
|
355 |
|
356 fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs), |
|
357 (unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs), |
|
358 (disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs), |
|
359 (sel_unfoldsss, sel_corecsss, sel_iter_attrs)) = |
|
360 ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, |
|
361 coinduct_attrs), |
|
362 (map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs), |
|
363 (map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss, |
|
364 disc_iter_attrs), |
|
365 (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss, |
|
366 disc_iter_iff_attrs), |
|
367 (map (map (map (Morphism.thm phi))) sel_unfoldsss, |
|
368 map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)); |
|
369 |
|
370 val transfer_gfp_sugar_thms = |
|
371 morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; |
|
372 |
|
373 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; |
|
374 |
|
375 fun mk_iter_fun_arg_types ctr_Tsss ns mss = |
|
376 mk_fp_iter_fun_types |
|
377 #> map3 mk_iter_fun_arg_types0 ns mss |
|
378 #> map2 (map2 (map2 unzip_recT)) ctr_Tsss; |
|
379 |
|
380 fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy = |
|
381 let |
|
382 val Css = map2 replicate ns Cs; |
|
383 val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss); |
|
384 val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss; |
|
385 |
|
386 val ((gss, ysss), lthy) = |
|
387 lthy |
|
388 |> mk_Freess "f" g_Tss |
|
389 ||>> mk_Freesss "x" y_Tsss; |
|
390 |
|
391 val y_Tssss = map (map (map single)) y_Tsss; |
|
392 val yssss = map (map (map single)) ysss; |
|
393 |
|
394 val z_Tssss = |
|
395 map4 (fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts => |
|
396 map3 (fn m => fn ctr_Ts => fn ctor_iter_fun_T => |
|
397 map2 unzip_recT ctr_Ts (dest_tupleT m ctor_iter_fun_T)) |
|
398 ms ctr_Tss (dest_sumTN_balanced n (domain_type (co_rec_of ctor_iter_fun_Ts)))) |
|
399 ns mss ctr_Tsss ctor_iter_fun_Tss; |
|
400 |
|
401 val z_Tsss' = map (map flat_rec_arg_args) z_Tssss; |
|
402 val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css; |
|
403 |
|
404 val hss = map2 (map2 retype_free) h_Tss gss; |
|
405 val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss; |
|
406 val (zssss_tl, lthy) = |
|
407 lthy |
|
408 |> mk_Freessss "y" (map (map (map tl)) z_Tssss); |
|
409 val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl; |
|
410 in |
|
411 ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) |
|
412 end; |
|
413 |
|
414 fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts = |
|
415 let |
|
416 (*avoid "'a itself" arguments in coiterators*) |
|
417 fun repair_arity [[]] = [[@{typ unit}]] |
|
418 | repair_arity Tss = Tss; |
|
419 |
|
420 val ctr_Tsss' = map repair_arity ctr_Tsss; |
|
421 val f_sum_prod_Ts = map range_type fun_Ts; |
|
422 val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; |
|
423 val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss; |
|
424 val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT))) |
|
425 Cs ctr_Tsss' f_Tsss; |
|
426 val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss; |
|
427 in |
|
428 (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) |
|
429 end; |
|
430 |
|
431 fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs; |
|
432 |
|
433 fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter = |
|
434 (mk_coiter_p_pred_types Cs ns, |
|
435 mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 ctr_Tsss Cs ns); |
|
436 |
|
437 fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy = |
|
438 let |
|
439 val p_Tss = mk_coiter_p_pred_types Cs ns; |
|
440 |
|
441 fun mk_types get_Ts = |
|
442 let |
|
443 val fun_Ts = map get_Ts dtor_coiter_fun_Tss; |
|
444 val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts; |
|
445 val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; |
|
446 in |
|
447 (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) |
|
448 end; |
|
449 |
|
450 val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of; |
|
451 val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of; |
|
452 |
|
453 val ((((Free (z, _), cs), pss), gssss), lthy) = |
|
454 lthy |
|
455 |> yield_singleton (mk_Frees "z") dummyT |
|
456 ||>> mk_Frees "a" Cs |
|
457 ||>> mk_Freess "p" p_Tss |
|
458 ||>> mk_Freessss "g" g_Tssss; |
|
459 val rssss = map (map (map (fn [] => []))) r_Tssss; |
|
460 |
|
461 val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss; |
|
462 val ((sssss, hssss_tl), lthy) = |
|
463 lthy |
|
464 |> mk_Freessss "q" s_Tssss |
|
465 ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss); |
|
466 val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl; |
|
467 |
|
468 val cpss = map2 (map o rapp) cs pss; |
|
469 |
|
470 fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); |
|
471 |
|
472 fun build_dtor_coiter_arg _ [] [cf] = cf |
|
473 | build_dtor_coiter_arg T [cq] [cf, cf'] = |
|
474 mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf) |
|
475 (build_sum_inj Inr_const (fastype_of cf', T) $ cf'); |
|
476 |
|
477 fun mk_args qssss fssss f_Tsss = |
|
478 let |
|
479 val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss; |
|
480 val cqssss = map2 (map o map o map o rapp) cs qssss; |
|
481 val cfssss = map2 (map o map o map o rapp) cs fssss; |
|
482 val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss; |
|
483 in (pfss, cqfsss) end; |
|
484 |
|
485 val unfold_args = mk_args rssss gssss g_Tsss; |
|
486 val corec_args = mk_args sssss hssss h_Tsss; |
|
487 in |
|
488 ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) |
|
489 end; |
|
490 |
|
491 fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy = |
|
492 let |
|
493 val thy = Proof_Context.theory_of lthy; |
|
494 |
|
495 val (xtor_co_iter_fun_Tss, xtor_co_iterss) = |
|
496 map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) (transpose xtor_co_iterss0) |
|
497 |> apsnd transpose o apfst transpose o split_list; |
|
498 |
|
499 val ((iters_args_types, coiters_args_types), lthy') = |
|
500 if fp = Least_FP then |
|
501 mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME) |
|
502 else |
|
503 mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME) |
|
504 in |
|
505 ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') |
|
506 end; |
|
507 |
|
508 fun mk_preds_getterss_join c cps sum_prod_T cqfss = |
|
509 let val n = length cqfss in |
|
510 Term.lambda c (mk_IfN sum_prod_T cps |
|
511 (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n))) |
|
512 end; |
|
513 |
|
514 fun define_co_iters fp fpT Cs binding_specs lthy0 = |
|
515 let |
|
516 val thy = Proof_Context.theory_of lthy0; |
|
517 |
|
518 val maybe_conceal_def_binding = Thm.def_binding |
|
519 #> Config.get lthy0 bnf_note_all = false ? Binding.conceal; |
|
520 |
|
521 val ((csts, defs), (lthy', lthy)) = lthy0 |
|
522 |> apfst split_list o fold_map (fn (b, rhs) => |
|
523 Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) |
|
524 #>> apsnd snd) binding_specs |
|
525 ||> `Local_Theory.restore; |
|
526 |
|
527 val phi = Proof_Context.export_morphism lthy lthy'; |
|
528 |
|
529 val csts' = map (mk_co_iter thy fp fpT Cs o Morphism.term phi) csts; |
|
530 val defs' = map (Morphism.thm phi) defs; |
|
531 in |
|
532 ((csts', defs'), lthy') |
|
533 end; |
|
534 |
|
535 fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs ctor_iters lthy = |
|
536 let |
|
537 val nn = length fpTs; |
|
538 |
|
539 val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters))); |
|
540 |
|
541 fun generate_iter pre (_, _, fss, xssss) ctor_iter = |
|
542 (mk_binding pre, |
|
543 fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter, |
|
544 map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss))); |
|
545 in |
|
546 define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy |
|
547 end; |
|
548 |
|
549 fun define_coiters coiterNs (_, cs, cpss, coiter_args_typess') mk_binding fpTs Cs dtor_coiters |
|
550 lthy = |
|
551 let |
|
552 val nn = length fpTs; |
|
553 |
|
554 val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters))); |
|
555 |
|
556 fun generate_coiter pre ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter = |
|
557 (mk_binding pre, |
|
558 fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter, |
|
559 map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss))); |
|
560 in |
|
561 define_co_iters Greatest_FP fpT Cs |
|
562 (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy |
|
563 end; |
|
564 |
|
565 fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct |
|
566 ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss |
|
567 lthy = |
|
568 let |
|
569 val iterss' = transpose iterss; |
|
570 val iter_defss' = transpose iter_defss; |
|
571 |
|
572 val [folds, recs] = iterss'; |
|
573 val [fold_defs, rec_defs] = iter_defss'; |
|
574 |
|
575 val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; |
|
576 |
|
577 val nn = length pre_bnfs; |
|
578 val ns = map length ctr_Tsss; |
|
579 val mss = map (map length) ctr_Tsss; |
|
580 |
|
581 val pre_map_defs = map map_def_of_bnf pre_bnfs; |
|
582 val pre_set_defss = map set_defs_of_bnf pre_bnfs; |
|
583 val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; |
|
584 val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs; |
|
585 val nested_set_maps = maps set_map_of_bnf nested_bnfs; |
|
586 |
|
587 val fp_b_names = map base_name_of_typ fpTs; |
|
588 |
|
589 val ((((ps, ps'), xsss), us'), names_lthy) = |
|
590 lthy |
|
591 |> mk_Frees' "P" (map mk_pred1T fpTs) |
|
592 ||>> mk_Freesss "x" ctr_Tsss |
|
593 ||>> Variable.variant_fixes fp_b_names; |
|
594 |
|
595 val us = map2 (curry Free) us' fpTs; |
|
596 |
|
597 fun mk_sets_nested bnf = |
|
598 let |
|
599 val Type (T_name, Us) = T_of_bnf bnf; |
|
600 val lives = lives_of_bnf bnf; |
|
601 val sets = sets_of_bnf bnf; |
|
602 fun mk_set U = |
|
603 (case find_index (curry (op =) U) lives of |
|
604 ~1 => Term.dummy |
|
605 | i => nth sets i); |
|
606 in |
|
607 (T_name, map mk_set Us) |
|
608 end; |
|
609 |
|
610 val setss_nested = map mk_sets_nested nested_bnfs; |
|
611 |
|
612 val (induct_thms, induct_thm) = |
|
613 let |
|
614 fun mk_set Ts t = |
|
615 let val Type (_, Ts0) = domain_type (fastype_of t) in |
|
616 Term.subst_atomic_types (Ts0 ~~ Ts) t |
|
617 end; |
|
618 |
|
619 fun mk_raw_prem_prems _ (x as Free (_, Type _)) (X as TFree _) = |
|
620 [([], (find_index (curry (op =) X) Xs + 1, x))] |
|
621 | mk_raw_prem_prems names_lthy (x as Free (s, Type (T_name, Ts0))) (Type (_, Xs_Ts0)) = |
|
622 (case AList.lookup (op =) setss_nested T_name of |
|
623 NONE => [] |
|
624 | SOME raw_sets0 => |
|
625 let |
|
626 val (Xs_Ts, (Ts, raw_sets)) = |
|
627 filter (exists_subtype_in Xs o fst) (Xs_Ts0 ~~ (Ts0 ~~ raw_sets0)) |
|
628 |> split_list ||> split_list; |
|
629 val sets = map (mk_set Ts0) raw_sets; |
|
630 val (ys, names_lthy') = names_lthy |> mk_Frees s Ts; |
|
631 val xysets = map (pair x) (ys ~~ sets); |
|
632 val ppremss = map2 (mk_raw_prem_prems names_lthy') ys Xs_Ts; |
|
633 in |
|
634 flat (map2 (map o apfst o cons) xysets ppremss) |
|
635 end) |
|
636 | mk_raw_prem_prems _ _ _ = []; |
|
637 |
|
638 fun close_prem_prem xs t = |
|
639 fold_rev Logic.all (map Free (drop (nn + length xs) |
|
640 (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t; |
|
641 |
|
642 fun mk_prem_prem xs (xysets, (j, x)) = |
|
643 close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) => |
|
644 HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets, |
|
645 HOLogic.mk_Trueprop (nth ps (j - 1) $ x))); |
|
646 |
|
647 fun mk_raw_prem phi ctr ctr_Ts ctrXs_Ts = |
|
648 let |
|
649 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; |
|
650 val pprems = flat (map2 (mk_raw_prem_prems names_lthy') xs ctrXs_Ts); |
|
651 in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end; |
|
652 |
|
653 fun mk_prem (xs, raw_pprems, concl) = |
|
654 fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl)); |
|
655 |
|
656 val raw_premss = map4 (map3 o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss; |
|
657 |
|
658 val goal = |
|
659 Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss, |
|
660 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us))); |
|
661 |
|
662 val kksss = map (map (map (fst o snd) o #2)) raw_premss; |
|
663 |
|
664 val ctor_induct' = ctor_induct OF (map mk_sumEN_tupled_balanced mss); |
|
665 |
|
666 val thm = |
|
667 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => |
|
668 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_maps |
|
669 pre_set_defss) |
|
670 |> singleton (Proof_Context.export names_lthy lthy) |
|
671 |> Thm.close_derivation; |
|
672 in |
|
673 `(conj_dests nn) thm |
|
674 end; |
|
675 |
|
676 val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); |
|
677 val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); |
|
678 |
|
679 val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss; |
|
680 |
|
681 fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms = |
|
682 let |
|
683 val fiters = map (lists_bmoc fss) iters; |
|
684 |
|
685 fun mk_goal fss fiter xctr f xs fxs = |
|
686 fold_rev (fold_rev Logic.all) (xs :: fss) |
|
687 (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs))); |
|
688 |
|
689 fun maybe_tick (T, U) u f = |
|
690 if try (fst o HOLogic.dest_prodT) U = SOME T then |
|
691 Term.lambda u (HOLogic.mk_prod (u, f $ u)) |
|
692 else |
|
693 f; |
|
694 |
|
695 fun build_iter (x as Free (_, T)) U = |
|
696 if T = U then |
|
697 x |
|
698 else |
|
699 build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs |
|
700 (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x; |
|
701 |
|
702 val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss; |
|
703 |
|
704 val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss; |
|
705 |
|
706 val tacss = |
|
707 map2 (map o mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs) |
|
708 ctor_iter_thms ctr_defss; |
|
709 |
|
710 fun prove goal tac = |
|
711 Goal.prove_sorry lthy [] [] goal (tac o #context) |
|
712 |> Thm.close_derivation; |
|
713 in |
|
714 map2 (map2 prove) goalss tacss |
|
715 end; |
|
716 |
|
717 val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss); |
|
718 val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss); |
|
719 in |
|
720 ((induct_thms, induct_thm, [induct_case_names_attr]), |
|
721 (fold_thmss, rec_thmss, code_nitpicksimp_attrs @ simp_attrs)) |
|
722 end; |
|
723 |
|
724 fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, |
|
725 coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) |
|
726 dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss |
|
727 mss ns ctr_defss (ctr_sugars : ctr_sugar list) coiterss coiter_defss export_args lthy = |
|
728 let |
|
729 fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter = |
|
730 iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]]; |
|
731 |
|
732 val ctor_dtor_coiter_thmss = |
|
733 map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss; |
|
734 |
|
735 val coiterss' = transpose coiterss; |
|
736 val coiter_defss' = transpose coiter_defss; |
|
737 |
|
738 val [unfold_defs, corec_defs] = coiter_defss'; |
|
739 |
|
740 val nn = length pre_bnfs; |
|
741 |
|
742 val pre_map_defs = map map_def_of_bnf pre_bnfs; |
|
743 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; |
|
744 val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs; |
|
745 val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs; |
|
746 |
|
747 val fp_b_names = map base_name_of_typ fpTs; |
|
748 |
|
749 val ctrss = map #ctrs ctr_sugars; |
|
750 val discss = map #discs ctr_sugars; |
|
751 val selsss = map #selss ctr_sugars; |
|
752 val exhausts = map #exhaust ctr_sugars; |
|
753 val disc_thmsss = map #disc_thmss ctr_sugars; |
|
754 val discIss = map #discIs ctr_sugars; |
|
755 val sel_thmsss = map #sel_thmss ctr_sugars; |
|
756 |
|
757 val (((rs, us'), vs'), names_lthy) = |
|
758 lthy |
|
759 |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs) |
|
760 ||>> Variable.variant_fixes fp_b_names |
|
761 ||>> Variable.variant_fixes (map (suffix "'") fp_b_names); |
|
762 |
|
763 val us = map2 (curry Free) us' fpTs; |
|
764 val udiscss = map2 (map o rapp) us discss; |
|
765 val uselsss = map2 (map o map o rapp) us selsss; |
|
766 |
|
767 val vs = map2 (curry Free) vs' fpTs; |
|
768 val vdiscss = map2 (map o rapp) vs discss; |
|
769 val vselsss = map2 (map o map o rapp) vs selsss; |
|
770 |
|
771 val coinduct_thms_pairs = |
|
772 let |
|
773 val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs; |
|
774 val uv_eqs = map2 (curry HOLogic.mk_eq) us vs; |
|
775 val strong_rs = |
|
776 map4 (fn u => fn v => fn uvr => fn uv_eq => |
|
777 fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; |
|
778 |
|
779 fun build_the_rel rs' T Xs_T = |
|
780 build_rel lthy (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) |
|
781 |> Term.subst_atomic_types (Xs ~~ fpTs); |
|
782 |
|
783 fun build_rel_app rs' usel vsel Xs_T = |
|
784 fold rapp [usel, vsel] (build_the_rel rs' (fastype_of usel) Xs_T); |
|
785 |
|
786 fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels ctrXs_Ts = |
|
787 (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @ |
|
788 (if null usels then |
|
789 [] |
|
790 else |
|
791 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc], |
|
792 Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]); |
|
793 |
|
794 fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss = |
|
795 Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n) |
|
796 (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss)) |
|
797 handle List.Empty => @{term True}; |
|
798 |
|
799 fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss = |
|
800 fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr, |
|
801 HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss))); |
|
802 |
|
803 val concl = |
|
804 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
805 (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v))) |
|
806 uvrs us vs)); |
|
807 |
|
808 fun mk_goal rs' = |
|
809 Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss |
|
810 ctrXs_Tsss, concl); |
|
811 |
|
812 val goals = map mk_goal [rs, strong_rs]; |
|
813 |
|
814 fun prove dtor_coinduct' goal = |
|
815 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => |
|
816 mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors |
|
817 exhausts ctr_defss disc_thmsss sel_thmsss) |
|
818 |> singleton (Proof_Context.export names_lthy lthy) |
|
819 |> Thm.close_derivation; |
|
820 |
|
821 fun postproc nn thm = |
|
822 Thm.permute_prems 0 nn |
|
823 (if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm) |
|
824 |> Drule.zero_var_indexes |
|
825 |> `(conj_dests nn); |
|
826 |
|
827 val rel_eqs = map rel_eq_of_bnf pre_bnfs; |
|
828 val rel_monos = map rel_mono_of_bnf pre_bnfs; |
|
829 val dtor_coinducts = |
|
830 [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos lthy]; |
|
831 in |
|
832 map2 (postproc nn oo prove) dtor_coinducts goals |
|
833 end; |
|
834 |
|
835 fun mk_coinduct_concls ms discs ctrs = |
|
836 let |
|
837 fun mk_disc_concl disc = [name_of_disc disc]; |
|
838 fun mk_ctr_concl 0 _ = [] |
|
839 | mk_ctr_concl _ ctor = [name_of_ctr ctor]; |
|
840 val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]]; |
|
841 val ctr_concls = map2 mk_ctr_concl ms ctrs; |
|
842 in |
|
843 flat (map2 append disc_concls ctr_concls) |
|
844 end; |
|
845 |
|
846 val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names); |
|
847 val coinduct_conclss = |
|
848 map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; |
|
849 |
|
850 fun mk_maybe_not pos = not pos ? HOLogic.mk_not; |
|
851 |
|
852 val fcoiterss' as [gunfolds, hcorecs] = |
|
853 map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss'; |
|
854 |
|
855 val (unfold_thmss, corec_thmss) = |
|
856 let |
|
857 fun mk_goal pfss c cps fcoiter n k ctr m cfs' = |
|
858 fold_rev (fold_rev Logic.all) ([c] :: pfss) |
|
859 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps, |
|
860 mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs')))); |
|
861 |
|
862 fun mk_U maybe_mk_sumT = |
|
863 typ_subst_nonatomic (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs); |
|
864 |
|
865 fun tack z_name (c, u) f = |
|
866 let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in |
|
867 Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z) |
|
868 end; |
|
869 |
|
870 fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf = |
|
871 let val T = fastype_of cqf in |
|
872 if exists_subtype_in Cs T then |
|
873 let val U = mk_U maybe_mk_sumT T in |
|
874 build_map lthy (indexify snd fpTs (fn kk => fn _ => |
|
875 maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf |
|
876 end |
|
877 else |
|
878 cqf |
|
879 end; |
|
880 |
|
881 val crgsss' = map (map (map (build_coiter (un_fold_of fcoiterss') (K I) (K I)))) crgsss; |
|
882 val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z)))) |
|
883 cshsss; |
|
884 |
|
885 val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss'; |
|
886 val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; |
|
887 |
|
888 val unfold_tacss = |
|
889 map3 (map oo mk_coiter_tac unfold_defs nesting_map_idents) |
|
890 (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; |
|
891 val corec_tacss = |
|
892 map3 (map oo mk_coiter_tac corec_defs nesting_map_idents) |
|
893 (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss; |
|
894 |
|
895 fun prove goal tac = |
|
896 Goal.prove_sorry lthy [] [] goal (tac o #context) |
|
897 |> Thm.close_derivation; |
|
898 |
|
899 val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss; |
|
900 val corec_thmss = |
|
901 map2 (map2 prove) corec_goalss corec_tacss |
|
902 |> map (map (unfold_thms lthy @{thms sum_case_if})); |
|
903 in |
|
904 (unfold_thmss, corec_thmss) |
|
905 end; |
|
906 |
|
907 val (disc_unfold_iff_thmss, disc_corec_iff_thmss) = |
|
908 let |
|
909 fun mk_goal c cps fcoiter n k disc = |
|
910 mk_Trueprop_eq (disc $ (fcoiter $ c), |
|
911 if n = 1 then @{const True} |
|
912 else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps)); |
|
913 |
|
914 val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss; |
|
915 val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss; |
|
916 |
|
917 fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split}; |
|
918 |
|
919 val case_splitss' = map (map mk_case_split') cpss; |
|
920 |
|
921 val unfold_tacss = |
|
922 map3 (map oo mk_disc_coiter_iff_tac) case_splitss' unfold_thmss disc_thmsss; |
|
923 val corec_tacss = |
|
924 map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss; |
|
925 |
|
926 fun prove goal tac = |
|
927 Goal.prove_sorry lthy [] [] goal (tac o #context) |
|
928 |> singleton export_args |
|
929 |> singleton (Proof_Context.export names_lthy lthy) |
|
930 |> Thm.close_derivation; |
|
931 |
|
932 fun proves [_] [_] = [] |
|
933 | proves goals tacs = map2 prove goals tacs; |
|
934 in |
|
935 (map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss) |
|
936 end; |
|
937 |
|
938 fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs); |
|
939 |
|
940 val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss; |
|
941 val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss; |
|
942 |
|
943 fun mk_sel_coiter_thm coiter_thm sel sel_thm = |
|
944 let |
|
945 val (domT, ranT) = dest_funT (fastype_of sel); |
|
946 val arg_cong' = |
|
947 Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT]) |
|
948 [NONE, NONE, SOME (certify lthy sel)] arg_cong |
|
949 |> Thm.varifyT_global; |
|
950 val sel_thm' = sel_thm RSN (2, trans); |
|
951 in |
|
952 coiter_thm RS arg_cong' RS sel_thm' |
|
953 end; |
|
954 |
|
955 fun mk_sel_coiter_thms coiter_thmss = |
|
956 map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss; |
|
957 |
|
958 val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss; |
|
959 val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss; |
|
960 |
|
961 val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn)); |
|
962 val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); |
|
963 val coinduct_case_concl_attrs = |
|
964 map2 (fn casex => fn concls => |
|
965 Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) |
|
966 coinduct_cases coinduct_conclss; |
|
967 val coinduct_case_attrs = |
|
968 coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; |
|
969 in |
|
970 ((coinduct_thms_pairs, coinduct_case_attrs), |
|
971 (unfold_thmss, corec_thmss, code_nitpicksimp_attrs), |
|
972 (disc_unfold_thmss, disc_corec_thmss, []), |
|
973 (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), |
|
974 (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) |
|
975 end; |
|
976 |
|
977 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp |
|
978 (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 = |
|
979 let |
|
980 (* TODO: sanity checks on arguments *) |
|
981 |
|
982 val _ = if fp = Greatest_FP andalso no_discs_sels then |
|
983 error "Cannot define codatatypes without discriminators and selectors" |
|
984 else |
|
985 (); |
|
986 |
|
987 fun qualify mandatory fp_b_name = |
|
988 Binding.qualify mandatory fp_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix); |
|
989 |
|
990 val nn = length specs; |
|
991 val fp_bs = map type_binding_of specs; |
|
992 val fp_b_names = map Binding.name_of fp_bs; |
|
993 val fp_common_name = mk_common_name fp_b_names; |
|
994 val map_bs = map map_binding_of specs; |
|
995 val rel_bs = map rel_binding_of specs; |
|
996 |
|
997 fun prepare_type_arg (_, (ty, c)) = |
|
998 let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in |
|
999 TFree (s, prepare_constraint no_defs_lthy0 c) |
|
1000 end; |
|
1001 |
|
1002 val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of) specs; |
|
1003 val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0; |
|
1004 val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0; |
|
1005 val num_As = length unsorted_As; |
|
1006 val set_bss = map (map fst o type_args_named_constrained_of) specs; |
|
1007 |
|
1008 val (((Bs0, Cs), Xs), no_defs_lthy) = |
|
1009 no_defs_lthy0 |
|
1010 |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As |
|
1011 |> mk_TFrees num_As |
|
1012 ||>> mk_TFrees nn |
|
1013 ||>> variant_tfrees fp_b_names; |
|
1014 |
|
1015 fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec); |
|
1016 |
|
1017 val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; |
|
1018 |
|
1019 val qsoty = quote o Syntax.string_of_typ fake_lthy; |
|
1020 |
|
1021 val _ = (case Library.duplicates (op =) unsorted_As of [] => () |
|
1022 | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^ |
|
1023 "datatype specification")); |
|
1024 |
|
1025 val bad_args = |
|
1026 map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As |
|
1027 |> filter_out Term.is_TVar; |
|
1028 val _ = null bad_args orelse |
|
1029 error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^ |
|
1030 "datatype specification"); |
|
1031 |
|
1032 val mixfixes = map mixfix_of specs; |
|
1033 |
|
1034 val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => () |
|
1035 | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); |
|
1036 |
|
1037 val ctr_specss = map ctr_specs_of specs; |
|
1038 |
|
1039 val disc_bindingss = map (map disc_of) ctr_specss; |
|
1040 val ctr_bindingss = |
|
1041 map2 (fn fp_b_name => map (qualify false fp_b_name o ctr_of)) fp_b_names ctr_specss; |
|
1042 val ctr_argsss = map (map args_of) ctr_specss; |
|
1043 val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; |
|
1044 |
|
1045 val sel_bindingsss = map (map (map fst)) ctr_argsss; |
|
1046 val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; |
|
1047 val raw_sel_defaultsss = map (map defaults_of) ctr_specss; |
|
1048 |
|
1049 val (As :: _) :: fake_ctr_Tsss = |
|
1050 burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); |
|
1051 val As' = map dest_TFree As; |
|
1052 |
|
1053 val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss []; |
|
1054 val _ = (case subtract (op =) As' rhs_As' of [] => () |
|
1055 | extras => error ("Extra type variables on right-hand side: " ^ |
|
1056 commas (map (qsoty o TFree) extras))); |
|
1057 |
|
1058 val fake_Ts = map (fn s => Type (s, As)) fake_T_names; |
|
1059 |
|
1060 fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) = |
|
1061 s = s' andalso (Ts = Ts' orelse |
|
1062 error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^ |
|
1063 " (expected " ^ qsoty T' ^ ")")) |
|
1064 | eq_fpT_check _ _ = false; |
|
1065 |
|
1066 fun freeze_fp (T as Type (s, Ts)) = |
|
1067 (case find_index (eq_fpT_check T) fake_Ts of |
|
1068 ~1 => Type (s, map freeze_fp Ts) |
|
1069 | kk => nth Xs kk) |
|
1070 | freeze_fp T = T; |
|
1071 |
|
1072 val unfreeze_fp = Term.typ_subst_atomic (Xs ~~ fake_Ts); |
|
1073 |
|
1074 val ctrXs_Tsss = map (map (map freeze_fp)) fake_ctr_Tsss; |
|
1075 val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss; |
|
1076 |
|
1077 val fp_eqs = |
|
1078 map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; |
|
1079 |
|
1080 val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss []; |
|
1081 val _ = (case subtract (op =) rhsXs_As' As' of [] => () |
|
1082 | extras => List.app (fn extra => warning ("Unused type variable on right-hand side of " ^ |
|
1083 co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras); |
|
1084 |
|
1085 val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, |
|
1086 xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, |
|
1087 dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, |
|
1088 lthy)) = |
|
1089 fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs |
|
1090 no_defs_lthy0 |
|
1091 handle BAD_DEAD (X, X_backdrop) => |
|
1092 (case X_backdrop of |
|
1093 Type (bad_tc, _) => |
|
1094 let |
|
1095 val fake_T = qsoty (unfreeze_fp X); |
|
1096 val fake_T_backdrop = qsoty (unfreeze_fp X_backdrop); |
|
1097 fun register_hint () = |
|
1098 "\nUse the " ^ quote (fst (fst @{command_spec "bnf"})) ^ " command to register " ^ |
|
1099 quote bad_tc ^ " as a bounded natural functor to allow nested (co)recursion through \ |
|
1100 \it"; |
|
1101 in |
|
1102 if is_some (bnf_of no_defs_lthy bad_tc) orelse |
|
1103 is_some (fp_sugar_of no_defs_lthy bad_tc) then |
|
1104 error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ |
|
1105 " in type expression " ^ fake_T_backdrop) |
|
1106 else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy) |
|
1107 bad_tc) then |
|
1108 error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ |
|
1109 " via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^ |
|
1110 fake_T_backdrop ^ register_hint ()) |
|
1111 else |
|
1112 error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^ |
|
1113 " via type constructor " ^ quote bad_tc ^ " in type expression " ^ fake_T_backdrop ^ |
|
1114 register_hint ()) |
|
1115 end); |
|
1116 |
|
1117 val time = time lthy; |
|
1118 val timer = time (Timer.startRealTimer ()); |
|
1119 |
|
1120 val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As; |
|
1121 val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs; |
|
1122 |
|
1123 val pre_map_defs = map map_def_of_bnf pre_bnfs; |
|
1124 val pre_set_defss = map set_defs_of_bnf pre_bnfs; |
|
1125 val pre_rel_defs = map rel_def_of_bnf pre_bnfs; |
|
1126 val nesting_set_maps = maps set_map_of_bnf nesting_bnfs; |
|
1127 val nested_set_maps = maps set_map_of_bnf nested_bnfs; |
|
1128 |
|
1129 val live = live_of_bnf any_fp_bnf; |
|
1130 val _ = |
|
1131 if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs) then |
|
1132 warning "Map function and relator names ignored" |
|
1133 else |
|
1134 (); |
|
1135 |
|
1136 val Bs = |
|
1137 map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A) |
|
1138 (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0; |
|
1139 |
|
1140 val B_ify = Term.typ_subst_atomic (As ~~ Bs); |
|
1141 |
|
1142 val ctors = map (mk_ctor As) ctors0; |
|
1143 val dtors = map (mk_dtor As) dtors0; |
|
1144 |
|
1145 val fpTs = map (domain_type o fastype_of) dtors; |
|
1146 |
|
1147 fun massage_simple_notes base = |
|
1148 filter_out (null o #2) |
|
1149 #> map (fn (thmN, thms, attrs) => |
|
1150 ((qualify true base (Binding.name thmN), attrs), [(thms, [])])); |
|
1151 |
|
1152 val massage_multi_notes = |
|
1153 maps (fn (thmN, thmss, attrs) => |
|
1154 map3 (fn fp_b_name => fn Type (T_name, _) => fn thms => |
|
1155 ((qualify true fp_b_name (Binding.name thmN), attrs T_name), [(thms, [])])) |
|
1156 fp_b_names fpTs thmss) |
|
1157 #> filter_out (null o fst o hd o snd); |
|
1158 |
|
1159 val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss; |
|
1160 val ns = map length ctr_Tsss; |
|
1161 val kss = map (fn n => 1 upto n) ns; |
|
1162 val mss = map (map length) ctr_Tsss; |
|
1163 |
|
1164 val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') = |
|
1165 mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy; |
|
1166 |
|
1167 fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), |
|
1168 xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), |
|
1169 pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), |
|
1170 ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = |
|
1171 let |
|
1172 val fp_b_name = Binding.name_of fp_b; |
|
1173 |
|
1174 val dtorT = domain_type (fastype_of ctor); |
|
1175 val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; |
|
1176 val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; |
|
1177 |
|
1178 val ((((w, xss), yss), u'), names_lthy) = |
|
1179 no_defs_lthy |
|
1180 |> yield_singleton (mk_Frees "w") dtorT |
|
1181 ||>> mk_Freess "x" ctr_Tss |
|
1182 ||>> mk_Freess "y" (map (map B_ify) ctr_Tss) |
|
1183 ||>> yield_singleton Variable.variant_fixes fp_b_name; |
|
1184 |
|
1185 val u = Free (u', fpT); |
|
1186 |
|
1187 val tuple_xs = map HOLogic.mk_tuple xss; |
|
1188 val tuple_ys = map HOLogic.mk_tuple yss; |
|
1189 |
|
1190 val ctr_rhss = |
|
1191 map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $ |
|
1192 mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs; |
|
1193 |
|
1194 val maybe_conceal_def_binding = Thm.def_binding |
|
1195 #> Config.get no_defs_lthy bnf_note_all = false ? Binding.conceal; |
|
1196 |
|
1197 val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |
|
1198 |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => |
|
1199 Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) |
|
1200 ctr_bindings ctr_mixfixes ctr_rhss |
|
1201 ||> `Local_Theory.restore; |
|
1202 |
|
1203 val phi = Proof_Context.export_morphism lthy lthy'; |
|
1204 |
|
1205 val ctr_defs = map (Morphism.thm phi) raw_ctr_defs; |
|
1206 val ctr_defs' = |
|
1207 map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs; |
|
1208 |
|
1209 val ctrs0 = map (Morphism.term phi) raw_ctrs; |
|
1210 val ctrs = map (mk_ctr As) ctrs0; |
|
1211 |
|
1212 fun wrap_ctrs lthy = |
|
1213 let |
|
1214 fun exhaust_tac {context = ctxt, prems = _} = |
|
1215 let |
|
1216 val ctor_iff_dtor_thm = |
|
1217 let |
|
1218 val goal = |
|
1219 fold_rev Logic.all [w, u] |
|
1220 (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); |
|
1221 in |
|
1222 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => |
|
1223 mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT]) |
|
1224 (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor) |
|
1225 |> Thm.close_derivation |
|
1226 |> Morphism.thm phi |
|
1227 end; |
|
1228 |
|
1229 val sumEN_thm' = |
|
1230 unfold_thms lthy @{thms unit_all_eq1} |
|
1231 (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] |
|
1232 (mk_sumEN_balanced n)) |
|
1233 |> Morphism.thm phi; |
|
1234 in |
|
1235 mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm' |
|
1236 end; |
|
1237 |
|
1238 val inject_tacss = |
|
1239 map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} => |
|
1240 mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs; |
|
1241 |
|
1242 val half_distinct_tacss = |
|
1243 map (map (fn (def, def') => fn {context = ctxt, ...} => |
|
1244 mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs)); |
|
1245 |
|
1246 val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss; |
|
1247 |
|
1248 val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss |
|
1249 in |
|
1250 wrap_free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings, |
|
1251 (sel_bindingss, sel_defaultss))) lthy |
|
1252 end; |
|
1253 |
|
1254 fun derive_maps_sets_rels (ctr_sugar, lthy) = |
|
1255 if live = 0 then |
|
1256 ((([], [], [], []), ctr_sugar), lthy) |
|
1257 else |
|
1258 let |
|
1259 val rel_flip = rel_flip_of_bnf fp_bnf; |
|
1260 val nones = replicate live NONE; |
|
1261 |
|
1262 val ctor_cong = |
|
1263 if fp = Least_FP then |
|
1264 Drule.dummy_thm |
|
1265 else |
|
1266 let val ctor' = mk_ctor Bs ctor in |
|
1267 cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong |
|
1268 end; |
|
1269 |
|
1270 fun mk_cIn ify = |
|
1271 certify lthy o (fp = Greatest_FP ? curry (op $) (map_types ify ctor)) oo |
|
1272 mk_InN_balanced (ify ctr_sum_prod_T) n; |
|
1273 |
|
1274 val cxIns = map2 (mk_cIn I) tuple_xs ks; |
|
1275 val cyIns = map2 (mk_cIn B_ify) tuple_ys ks; |
|
1276 |
|
1277 fun mk_map_thm ctr_def' cxIn = |
|
1278 fold_thms lthy [ctr_def'] |
|
1279 (unfold_thms lthy (pre_map_def :: |
|
1280 (if fp = Least_FP then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map) |
|
1281 (cterm_instantiate_pos (nones @ [SOME cxIn]) |
|
1282 (if fp = Least_FP then fp_map_thm else fp_map_thm RS ctor_cong))) |
|
1283 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
|
1284 |
|
1285 fun mk_set_thm fp_set_thm ctr_def' cxIn = |
|
1286 fold_thms lthy [ctr_def'] |
|
1287 (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @ |
|
1288 (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_set) |
|
1289 (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) |
|
1290 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
|
1291 |
|
1292 fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns; |
|
1293 |
|
1294 val map_thms = map2 mk_map_thm ctr_defs' cxIns; |
|
1295 val set_thmss = map mk_set_thms fp_set_thms; |
|
1296 |
|
1297 val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); |
|
1298 |
|
1299 fun mk_rel_thm postproc ctr_defs' cxIn cyIn = |
|
1300 fold_thms lthy ctr_defs' |
|
1301 (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def :: |
|
1302 (if fp = Least_FP then [] else [dtor_ctor]) @ sum_prod_thms_rel) |
|
1303 (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) |
|
1304 |> postproc |
|
1305 |> singleton (Proof_Context.export names_lthy no_defs_lthy); |
|
1306 |
|
1307 fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = |
|
1308 mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; |
|
1309 |
|
1310 val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); |
|
1311 |
|
1312 fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = |
|
1313 mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] |
|
1314 cxIn cyIn; |
|
1315 |
|
1316 fun mk_other_half_rel_distinct_thm thm = |
|
1317 flip_rels lthy live thm |
|
1318 RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); |
|
1319 |
|
1320 val half_rel_distinct_thmss = |
|
1321 map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); |
|
1322 val other_half_rel_distinct_thmss = |
|
1323 map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; |
|
1324 val (rel_distinct_thms, _) = |
|
1325 join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; |
|
1326 |
|
1327 val anonymous_notes = |
|
1328 [(map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms, |
|
1329 code_nitpicksimp_attrs), |
|
1330 (map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th) |
|
1331 rel_inject_thms ms, code_nitpicksimp_attrs)] |
|
1332 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); |
|
1333 |
|
1334 val notes = |
|
1335 [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs), |
|
1336 (rel_distinctN, rel_distinct_thms, simp_attrs), |
|
1337 (rel_injectN, rel_inject_thms, simp_attrs), |
|
1338 (setN, flat set_thmss, code_nitpicksimp_attrs @ simp_attrs)] |
|
1339 |> massage_simple_notes fp_b_name; |
|
1340 in |
|
1341 (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), |
|
1342 lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd) |
|
1343 end; |
|
1344 |
|
1345 fun mk_binding pre = qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); |
|
1346 |
|
1347 fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) = |
|
1348 (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy); |
|
1349 in |
|
1350 (wrap_ctrs |
|
1351 #> derive_maps_sets_rels |
|
1352 ##>> |
|
1353 (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types) |
|
1354 else define_coiters [unfoldN, corecN] (the coiters_args_types)) |
|
1355 mk_binding fpTs Cs xtor_co_iters |
|
1356 #> massage_res, lthy') |
|
1357 end; |
|
1358 |
|
1359 fun wrap_types_etc (wrap_types_etcs, lthy) = |
|
1360 fold_map I wrap_types_etcs lthy |
|
1361 |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list) |
|
1362 o split_list; |
|
1363 |
|
1364 fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs |
|
1365 mapsx rel_injects rel_distincts setss = |
|
1366 injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts |
|
1367 @ flat setss; |
|
1368 |
|
1369 fun derive_note_induct_iters_thms_for_types |
|
1370 ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), |
|
1371 (iterss, iter_defss)), lthy) = |
|
1372 let |
|
1373 val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, iter_attrs)) = |
|
1374 derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct |
|
1375 xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss |
|
1376 iter_defss lthy; |
|
1377 |
|
1378 val induct_type_attr = Attrib.internal o K o Induct.induct_type; |
|
1379 |
|
1380 val simp_thmss = |
|
1381 map7 mk_simp_thms ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss; |
|
1382 |
|
1383 val common_notes = |
|
1384 (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
|
1385 |> massage_simple_notes fp_common_name; |
|
1386 |
|
1387 val notes = |
|
1388 [(foldN, fold_thmss, K iter_attrs), |
|
1389 (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), |
|
1390 (recN, rec_thmss, K iter_attrs), |
|
1391 (simpsN, simp_thmss, K [])] |
|
1392 |> massage_multi_notes; |
|
1393 in |
|
1394 lthy |
|
1395 |> Local_Theory.notes (common_notes @ notes) |> snd |
|
1396 |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars |
|
1397 iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] [] |
|
1398 end; |
|
1399 |
|
1400 fun derive_note_coinduct_coiters_thms_for_types |
|
1401 ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), |
|
1402 (coiterss, coiter_defss)), lthy) = |
|
1403 let |
|
1404 val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], |
|
1405 coinduct_attrs), |
|
1406 (unfold_thmss, corec_thmss, coiter_attrs), |
|
1407 (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), |
|
1408 (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), |
|
1409 (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) = |
|
1410 derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct |
|
1411 dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns |
|
1412 ctr_defss ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) |
|
1413 lthy; |
|
1414 |
|
1415 val sel_unfold_thmss = map flat sel_unfold_thmsss; |
|
1416 val sel_corec_thmss = map flat sel_corec_thmsss; |
|
1417 |
|
1418 val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; |
|
1419 |
|
1420 val flat_coiter_thms = append oo append; |
|
1421 |
|
1422 val simp_thmss = |
|
1423 map7 mk_simp_thms ctr_sugars |
|
1424 (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss) |
|
1425 (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) |
|
1426 mapss rel_injects rel_distincts setss; |
|
1427 |
|
1428 val common_notes = |
|
1429 (if nn > 1 then |
|
1430 [(coinductN, [coinduct_thm], coinduct_attrs), |
|
1431 (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)] |
|
1432 else |
|
1433 []) |
|
1434 |> massage_simple_notes fp_common_name; |
|
1435 |
|
1436 val notes = |
|
1437 [(coinductN, map single coinduct_thms, |
|
1438 fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]), |
|
1439 (corecN, corec_thmss, K coiter_attrs), |
|
1440 (disc_corecN, disc_corec_thmss, K disc_coiter_attrs), |
|
1441 (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs), |
|
1442 (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs), |
|
1443 (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs), |
|
1444 (sel_corecN, sel_corec_thmss, K sel_coiter_attrs), |
|
1445 (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs), |
|
1446 (simpsN, simp_thmss, K []), |
|
1447 (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs), |
|
1448 (unfoldN, unfold_thmss, K coiter_attrs)] |
|
1449 |> massage_multi_notes; |
|
1450 |
|
1451 fun is_codatatype (Type (s, _)) = |
|
1452 (case fp_sugar_of lthy s of SOME {fp = Greatest_FP, ...} => true | _ => false) |
|
1453 | is_codatatype _ = false; |
|
1454 |
|
1455 val nitpick_supported = forall (is_codatatype o T_of_bnf) nested_bnfs; |
|
1456 |
|
1457 fun register_nitpick fpT ({ctrs, casex, ...} : ctr_sugar) = |
|
1458 Nitpick_HOL.register_codatatype fpT (fst (dest_Const casex)) |
|
1459 (map (dest_Const o mk_ctr As) ctrs) |
|
1460 |> Generic_Target.theory_declaration; |
|
1461 in |
|
1462 lthy |
|
1463 |> Local_Theory.notes (common_notes @ notes) |> snd |
|
1464 |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss |
|
1465 ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] |
|
1466 (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) |
|
1467 (transpose [sel_unfold_thmsss, sel_corec_thmsss]) |
|
1468 |> nitpick_supported ? fold2 register_nitpick fpTs ctr_sugars |
|
1469 end; |
|
1470 |
|
1471 val lthy'' = lthy' |
|
1472 |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ |
|
1473 xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ |
|
1474 pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ |
|
1475 kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ |
|
1476 sel_bindingsss ~~ raw_sel_defaultsss) |
|
1477 |> wrap_types_etc |
|
1478 |> fp_case fp derive_note_induct_iters_thms_for_types |
|
1479 derive_note_coinduct_coiters_thms_for_types; |
|
1480 |
|
1481 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ |
|
1482 co_prefix fp ^ "datatype")); |
|
1483 in |
|
1484 timer; lthy'' |
|
1485 end; |
|
1486 |
|
1487 fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x; |
|
1488 |
|
1489 fun co_datatype_cmd x = |
|
1490 define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x; |
|
1491 |
|
1492 val parse_ctr_arg = |
|
1493 @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} || |
|
1494 (Parse.typ >> pair Binding.empty); |
|
1495 |
|
1496 val parse_defaults = |
|
1497 @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"}; |
|
1498 |
|
1499 val parse_type_arg_constrained = |
|
1500 Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); |
|
1501 |
|
1502 val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained; |
|
1503 |
|
1504 (*FIXME: use parse_type_args_named_constrained from BNF_Util and thus |
|
1505 allow users to kill certain arguments of a (co)datatype*) |
|
1506 val parse_type_args_named_constrained = |
|
1507 parse_type_arg_constrained >> (single o pair Binding.empty) || |
|
1508 @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) || |
|
1509 Scan.succeed []; |
|
1510 |
|
1511 val parse_ctr_spec = |
|
1512 parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg -- |
|
1513 Scan.optional parse_defaults [] -- Parse.opt_mixfix; |
|
1514 |
|
1515 val parse_spec = |
|
1516 parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- |
|
1517 Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec); |
|
1518 |
|
1519 val parse_co_datatype = parse_wrap_free_constructors_options -- Parse.and_list1 parse_spec; |
|
1520 |
|
1521 fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp; |
|
1522 |
|
1523 end; |