1 (* Title: HOL/Codatatype/Tools/bnf_comp.ML
2 Author: Dmitriy Traytel, TU Muenchen
3 Author: Jasmin Blanchette, TU Muenchen
6 Composition of bounded natural functors.
12 val empty_unfold: unfold_thms
13 val map_unfolds_of: unfold_thms -> thm list
14 val set_unfoldss_of: unfold_thms -> thm list list
15 val rel_unfolds_of: unfold_thms -> thm list
16 val pred_unfolds_of: unfold_thms -> thm list
18 val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
19 ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
20 (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
21 val default_comp_sort: (string * sort) list list -> (string * sort) list
22 val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
23 (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
24 (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
25 val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
26 (BNF_Def.BNF * typ list) * local_theory
29 structure BNF_Comp : BNF_COMP =
38 map_unfolds: thm list,
39 set_unfoldss: thm list list,
40 rel_unfolds: thm list,
41 pred_unfolds: thm list
44 fun add_to_thms thms NONE = thms
45 | add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms;
46 fun adds_to_thms thms NONE = thms
47 | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_refl news) thms;
49 fun mk_unfold_thms maps setss rels preds =
50 {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds};
52 val empty_unfold = mk_unfold_thms [] [] [] [];
54 fun add_to_unfold_opt map_opt sets_opt rel_opt pred_opt
55 {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds} = {
56 map_unfolds = add_to_thms maps map_opt,
57 set_unfoldss = adds_to_thms setss sets_opt,
58 rel_unfolds = add_to_thms rels rel_opt,
59 pred_unfolds = add_to_thms preds pred_opt};
61 fun add_to_unfold map sets rel pred =
62 add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred);
64 val map_unfolds_of = #map_unfolds;
65 val set_unfoldss_of = #set_unfoldss;
66 val rel_unfolds_of = #rel_unfolds;
67 val pred_unfolds_of = #pred_unfolds;
71 fun mk_killN n = "_kill" ^ string_of_int n;
72 fun mk_liftN n = "_lift" ^ string_of_int n;
73 fun mk_permuteN src dest =
74 "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
77 val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
78 val abs_pred_sym = sym RS @{thm abs_pred_def};
79 val abs_pred_sym_pred_abs = abs_pred_sym RS @{thm pred_def_abs};
81 (*copied from Envir.expand_term_free*)
82 fun expand_term_const defs =
84 val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
85 val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
86 in Envir.expand_term get end;
88 fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) =
90 val olive = live_of_bnf outer;
91 val onwits = nwits_of_bnf outer;
92 val odead = dead_of_bnf outer;
93 val inner = hd inners;
94 val ilive = live_of_bnf inner;
95 val ideads = map dead_of_bnf inners;
96 val inwitss = map nwits_of_bnf inners;
98 (* TODO: check olive = length inners > 0,
99 forall inner from inners. ilive = live,
100 forall inner from inners. idead = dead *)
102 val (oDs, lthy1) = apfst (map TFree)
103 (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
104 val (Dss, lthy2) = apfst (map (map TFree))
105 (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
106 val (Ass, lthy3) = apfst (replicate ilive o map TFree)
107 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
108 val As = if ilive > 0 then hd Ass else [];
109 val Ass_repl = replicate olive As;
110 val (Bs, _(*lthy4*)) = apfst (map TFree)
111 (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
112 val Bss_repl = replicate olive Bs;
114 val (((fs', Asets), xs), _(*names_lthy*)) = lthy
115 |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
116 ||>> mk_Frees "A" (map (HOLogic.mk_setT) As)
117 ||>> mk_Frees "x" As;
119 val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
120 val CCA = mk_T_of_bnf oDs CAs outer;
121 val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
122 val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
123 val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
124 val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
125 val outer_bd = mk_bd_of_bnf oDs CAs outer;
127 (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
128 val mapx = fold_rev Term.abs fs'
129 (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
130 map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
131 mk_map_of_bnf Ds As Bs) Dss inners));
133 (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
134 (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
137 val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
138 val outer_set = mk_collect
139 (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
140 (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
141 val inner_sets = map (fn sets => nth sets i) inner_setss;
142 val outer_map = mk_map_of_bnf oDs CAs setTs outer;
143 val map_inner_sets = Term.list_comb (outer_map, inner_sets);
144 val collect_image = mk_collect
145 (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
146 (CCA --> HOLogic.mk_setT T);
148 (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
149 HOLogic.mk_comp (mk_Union T, collect_image))
152 val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
154 (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
155 val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
157 fun map_id_tac {context = ctxt, ...} =
159 (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
161 val thms = (map map_id_of_bnf inners
162 |> map (`(Term.size_of_term o Thm.prop_of))
163 |> sort (rev_order o int_ord o pairself fst)
164 |> map snd) @ [map_id_of_bnf outer];
166 (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
170 mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
171 (map map_comp_of_bnf inners);
173 fun mk_single_set_natural_tac i _ =
174 mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
175 (collect_set_natural_of_bnf outer)
176 (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
178 val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1);
180 fun bd_card_order_tac _ =
181 mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
183 fun bd_cinfinite_tac _ =
184 mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
187 if ! quick_and_dirty then
188 replicate ilive no_thm
191 Skip_Proof.prove lthy [] [] goal
192 (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
193 |> Thm.close_derivation)
194 (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
197 mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
200 if ! quick_and_dirty then
201 replicate (length set_alt_thms) (K all_tac)
204 val outer_set_bds = set_bd_of_bnf outer;
205 val inner_set_bdss = map set_bd_of_bnf inners;
206 val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
207 fun single_set_bd_thm i j =
208 @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
210 val single_set_bd_thmss =
211 map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
213 map2 (fn set_alt => fn single_set_bds => fn {context, ...} =>
214 mk_comp_set_bd_tac context set_alt single_set_bds)
215 set_alt_thms single_set_bd_thmss
220 val inx = mk_in Asets sets CCA;
221 val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
222 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
224 Skip_Proof.prove lthy [] [] goal
225 (fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms)
226 |> Thm.close_derivation
230 mk_comp_in_bd_tac in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
231 (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
233 fun map_wpull_tac _ =
234 mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
236 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
237 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
239 val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
241 val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
242 (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
245 val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
247 val wits = (inner_witsss, (map (single o snd) outer_wits))
248 |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
250 |> map (`(fn t => Term.add_frees t []))
252 |> map (fn (frees, t) => fold absfree frees t);
254 fun wit_tac {context = ctxt, ...} =
255 mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
256 (maps wit_thms_of_bnf inners);
259 bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
260 ((((b, mapx), sets), bd), wits) lthy;
262 val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
263 val outer_rel_cong = rel_cong_of_bnf outer;
266 trans OF [rel_def_of_bnf bnf',
267 trans OF [in_alt_thm RS @{thm subst_rel_def},
268 trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
269 [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
270 rel_converse_of_bnf outer RS sym], outer_rel_Gr],
271 trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
272 (map (fn bnf => rel_def_of_bnf bnf RS sym) inners)]]]];
274 val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
275 pred_def_of_bnf bnf' RS abs_pred_sym,
276 trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners),
277 pred_def_of_bnf outer RS abs_pred_sym]];
279 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
280 pred_unfold_thm unfold;
282 (bnf', (unfold', lthy'))
285 (* Killing live variables *)
287 fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
289 val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
290 val live = live_of_bnf bnf;
291 val dead = dead_of_bnf bnf;
292 val nwits = nwits_of_bnf bnf;
294 (* TODO: check 0 < n <= live *)
296 val (Ds, lthy1) = apfst (map TFree)
297 (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
298 val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
299 (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
300 val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
301 (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
303 val ((Asets, lives), _(*names_lthy*)) = lthy
304 |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As))
305 ||>> mk_Frees "x" (drop n As);
306 val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
308 val T = mk_T_of_bnf Ds As bnf;
310 (*bnf.map id ... id*)
311 val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
313 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
314 val sets = drop n bnf_sets;
316 (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
317 val bnf_bd = mk_bd_of_bnf Ds As bnf;
319 (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
321 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
322 fun map_comp_tac {context, ...} =
323 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
325 fun map_cong_tac {context, ...} =
326 mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
327 val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
328 fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
329 fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
331 map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
332 (drop n (set_bd_of_bnf bnf));
336 val inx = mk_in Asets sets T;
337 val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
338 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
340 Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
344 mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
345 (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
346 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
348 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
349 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
351 val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
353 val wits = map (fn t => fold absfree (Term.add_frees t []) t)
354 (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
356 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
359 bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
360 ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
362 val rel_Gr = rel_Gr_of_bnf bnf RS sym;
365 trans OF [rel_def_of_bnf bnf',
366 trans OF [in_alt_thm RS @{thm subst_rel_def},
367 trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
368 [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym],
370 trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
371 (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
372 replicate (live - n) @{thm Gr_fst_snd})]]]];
374 val pred_unfold_thm = Collect_split_box_equals OF
375 [Local_Defs.unfold lthy' @{thms Id_def'} rel_unfold_thm, pred_def_of_bnf bnf' RS abs_pred_sym,
376 pred_def_of_bnf bnf RS abs_pred_sym];
378 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
379 pred_unfold_thm unfold;
381 (bnf', (unfold', lthy'))
384 (* Adding dummy live variables *)
386 fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
388 val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
389 val live = live_of_bnf bnf;
390 val dead = dead_of_bnf bnf;
391 val nwits = nwits_of_bnf bnf;
393 (* TODO: check 0 < n *)
395 val (Ds, lthy1) = apfst (map TFree)
396 (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
397 val ((newAs, As), lthy2) = apfst (chop n o map TFree)
398 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
399 val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
400 (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
402 val (Asets, _(*names_lthy*)) = lthy
403 |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As));
405 val T = mk_T_of_bnf Ds As bnf;
407 (*%f1 ... fn. bnf.map*)
409 fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
411 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
412 val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
414 val bd = mk_bd_of_bnf Ds As bnf;
416 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
417 fun map_comp_tac {context, ...} =
418 Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
420 fun map_cong_tac {context, ...} =
421 rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
422 val set_natural_tacs =
423 if ! quick_and_dirty then
424 replicate (n + live) (K all_tac)
426 replicate n (K empty_natural_tac) @
427 map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
428 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
429 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
431 if ! quick_and_dirty then
432 replicate (n + live) (K all_tac)
434 replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
435 (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
439 val inx = mk_in Asets sets T;
440 val in_alt = mk_in (drop n Asets) bnf_sets T;
441 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
443 Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
446 fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
447 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
449 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
450 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
452 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
454 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
457 bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
458 ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
461 trans OF [rel_def_of_bnf bnf',
462 trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
464 val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
465 pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
467 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
468 pred_unfold_thm unfold;
470 (bnf', (unfold', lthy'))
473 (* Changing the order of live variables *)
475 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
477 val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
478 val live = live_of_bnf bnf;
479 val dead = dead_of_bnf bnf;
480 val nwits = nwits_of_bnf bnf;
481 fun permute xs = mk_permute src dest xs;
482 fun permute_rev xs = mk_permute dest src xs;
484 val (Ds, lthy1) = apfst (map TFree)
485 (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
486 val (As, lthy2) = apfst (map TFree)
487 (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
488 val (Bs, _(*lthy3*)) = apfst (map TFree)
489 (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
491 val (Asets, _(*names_lthy*)) = lthy
492 |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As));
494 val T = mk_T_of_bnf Ds As bnf;
496 (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
497 val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
498 (Term.list_comb (mk_map_of_bnf Ds As Bs bnf,
499 permute_rev (map Bound ((live - 1) downto 0))));
501 val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
502 val sets = permute bnf_sets;
504 val bd = mk_bd_of_bnf Ds As bnf;
506 fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
507 fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
508 fun map_cong_tac {context, ...} =
509 rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
510 val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
511 fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
512 fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
513 val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
517 val inx = mk_in Asets sets T;
518 val in_alt = mk_in (permute_rev Asets) bnf_sets T;
519 val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
521 Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
522 |> Thm.close_derivation
526 mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
527 fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
529 val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
530 bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
532 val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
534 fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
537 bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
538 ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
541 trans OF [rel_def_of_bnf bnf',
542 trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
544 val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
545 pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
547 val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
548 pred_unfold_thm unfold;
550 (bnf', (unfold', lthy'))
553 (* Composition pipeline *)
555 fun permute_and_kill qualify n src dest bnf =
557 |> permute_bnf qualify src dest
558 #> uncurry (kill_bnf qualify n);
560 fun lift_and_permute qualify n src dest bnf =
562 |> lift_bnf qualify n
563 #> uncurry (permute_bnf qualify src dest);
565 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =
567 val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
568 val kill_poss = map (find_indices Ds) Ass;
569 val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
570 val before_kill_dest = map2 append kill_poss live_poss;
571 val kill_ns = map length kill_poss;
572 val (inners', (unfold', lthy')) =
573 fold_map5 (fn i => permute_and_kill (qualify i))
574 (if length bnfs = 1 then [0] else (1 upto length bnfs))
575 kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy);
577 val Ass' = map2 (map o nth) Ass live_poss;
579 val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
580 val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
581 val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
582 val after_lift_src = map2 append new_poss old_poss;
583 val lift_ns = map (fn xs => length As - length xs) Ass';
585 ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
586 (if length bnfs = 1 then [0] else (1 upto length bnfs))
587 lift_ns after_lift_src after_lift_dest inners' (unfold', lthy'))
590 fun default_comp_sort Ass =
591 Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
593 fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
595 val b = name_of_bnf outer;
597 val Ass = map (map Term.dest_TFree) tfreess;
598 val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
600 val ((kill_poss, As), (inners', (unfold', lthy'))) =
601 normalize_bnfs qualify Ass Ds sort inners unfold lthy;
603 val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
604 val As = map TFree As;
606 apfst (rpair (Ds, As))
607 (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
610 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
612 fun seal_bnf unfold b Ds bnf lthy =
614 val live = live_of_bnf bnf;
615 val nwits = nwits_of_bnf bnf;
617 val (As, lthy1) = apfst (map TFree)
618 (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
619 val (Bs, _) = apfst (map TFree)
620 (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
622 val map_unfolds = filter_refl (map_unfolds_of unfold);
623 val set_unfoldss = map filter_refl (set_unfoldss_of unfold);
625 val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
627 val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
629 val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
630 val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
631 val unfold_defs = unfold_sets o unfold_maps;
632 val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
633 val bnf_sets = map (expand_maps o expand_sets)
634 (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
635 val bnf_bd = mk_bd_of_bnf Ds As bnf;
636 val T = mk_T_of_bnf Ds As bnf;
638 (*bd should only depend on dead type variables!*)
639 val bd_repT = fst (dest_relT (fastype_of bnf_bd));
640 val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
641 val params = fold Term.add_tfreesT Ds [];
642 val deads = map TFree params;
644 val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
645 typedef false NONE (bdT_bind, params, NoSyn)
646 (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
648 val bnf_bd' = mk_dir_image bnf_bd
649 (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
651 val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
652 val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
654 val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
656 @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
658 (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
661 map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
663 @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
664 @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
665 @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
666 bd_Card_order_of_bnf bnf]];
668 fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
669 SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
671 map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @
672 set_natural_of_bnf bnf) @
673 map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @
674 map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]);
676 val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
678 fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
680 val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
681 ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
683 val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
684 val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
686 val rel_def = unfold_defs' (rel_def_of_bnf bnf');
687 val rel_unfold = Local_Defs.unfold lthy'
688 (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def;
690 val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']);
692 val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
693 val pred_unfold = Local_Defs.unfold lthy'
694 (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
697 [(rel_unfoldN, [rel_unfold]),
698 (pred_unfoldN, [pred_unfold])]
699 |> map (fn (thmN, thms) =>
700 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
702 ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
705 fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
706 ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
707 (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
708 | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
709 | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
711 val tfrees = Term.add_tfreesT T [];
712 val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
715 NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
717 if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
719 val T' = T_of_bnf bnf;
720 val deads = deads_of_bnf bnf;
721 val lives = lives_of_bnf bnf;
722 val tvars' = Term.add_tvarsT T' [];
724 pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
726 val rel_def = rel_def_of_bnf bnf;
727 val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_def RS sym))
728 (SOME (Local_Defs.unfold lthy [rel_def] (pred_def_of_bnf bnf) RS sym)) unfold;
729 in ((bnf, deads_lives), (unfold', lthy)) end
732 val name = Long_Name.base_name C;
734 let val namei = name ^ nonzero_string_of_int i;
735 in qualify' o Binding.qualify true namei end;
736 val odead = dead_of_bnf bnf;
737 val olive = live_of_bnf bnf;
738 val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
739 (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
740 val oDs = map (nth Ts) oDs_pos;
741 val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
742 val ((inners, (Dss, Ass)), (unfold', lthy')) =
743 apfst (apsnd split_list o split_list)
744 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
745 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
747 compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')