src/HOL/Codatatype/Tools/bnf_comp.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49236 632f68beff2a
child 49303 c87930fb5b90
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/Tools/bnf_comp.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     5 
     6 Composition of bounded natural functors.
     7 *)
     8 
     9 signature BNF_COMP =
    10 sig
    11   type unfold_thms
    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
    17 
    18   val bnf_of_typ: BNF_Def.const_policy -> binding -> (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
    27 end;
    28 
    29 structure BNF_Comp : BNF_COMP =
    30 struct
    31 
    32 open BNF_Def
    33 open BNF_Util
    34 open BNF_Tactics
    35 open BNF_Comp_Tactics
    36 
    37 type unfold_thms = {
    38   map_unfolds: thm list,
    39   set_unfoldss: thm list list,
    40   rel_unfolds: thm list,
    41   pred_unfolds: thm list
    42 };
    43 
    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;
    48 
    49 fun mk_unfold_thms maps setss rels preds =
    50   {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds};
    51 
    52 val empty_unfold = mk_unfold_thms [] [] [] [];
    53 
    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};
    60 
    61 fun add_to_unfold map sets rel pred =
    62   add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred);
    63 
    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;
    68 
    69 val bdTN = "bdT";
    70 
    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) ^ "_";
    75 
    76 val no_thm = refl;
    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};
    80 
    81 (*copied from Envir.expand_term_free*)
    82 fun expand_term_const defs =
    83   let
    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;
    87 
    88 fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) =
    89   let
    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;
    97 
    98     (* TODO: check olive = length inners > 0,
    99                    forall inner from inners. ilive = live,
   100                    forall inner from inners. idead = dead  *)
   101 
   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;
   113 
   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;
   118 
   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;
   126 
   127     (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
   128     val comp_map = 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));
   132 
   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}*)
   135     fun mk_comp_set i =
   136       let
   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);
   147       in
   148         (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
   149         HOLogic.mk_comp (mk_Union T, collect_image))
   150       end;
   151 
   152     val (comp_sets, comp_sets_alt) = map_split mk_comp_set (0 upto ilive - 1);
   153 
   154     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
   155     val comp_bd = Term.absdummy CCA (mk_cprod
   156       (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
   157 
   158     fun comp_map_id_tac {context = ctxt, ...} =
   159       let
   160         (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
   161           rules*)
   162         val thms = (map map_id_of_bnf inners
   163           |> map (`(Term.size_of_term o Thm.prop_of))
   164           |> sort (rev_order o int_ord o pairself fst)
   165           |> map snd) @ [map_id_of_bnf outer];
   166       in
   167         (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
   168       end;
   169 
   170     fun comp_map_comp_tac _ =
   171       mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
   172         (map map_comp_of_bnf inners);
   173 
   174     fun mk_single_comp_set_natural_tac i _ =
   175       mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
   176         (collect_set_natural_of_bnf outer)
   177         (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
   178 
   179     val comp_set_natural_tacs = map mk_single_comp_set_natural_tac (0 upto ilive - 1);
   180 
   181     fun comp_bd_card_order_tac _ =
   182       mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
   183 
   184     fun comp_bd_cinfinite_tac _ =
   185       mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
   186 
   187     val comp_set_alt_thms =
   188       if ! quick_and_dirty then
   189         replicate ilive no_thm
   190       else
   191         map (fn goal =>
   192           Skip_Proof.prove lthy [] [] goal
   193             (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
   194           |> Thm.close_derivation)
   195         (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) comp_sets comp_sets_alt);
   196 
   197     fun comp_map_cong_tac _ =
   198       mk_comp_map_cong_tac comp_set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
   199 
   200     val comp_set_bd_tacs =
   201       if ! quick_and_dirty then
   202         replicate (length comp_set_alt_thms) (K all_tac)
   203       else
   204         let
   205           val outer_set_bds = set_bd_of_bnf outer;
   206           val inner_set_bdss = map set_bd_of_bnf inners;
   207           val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
   208           fun comp_single_set_bd_thm i j =
   209             @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
   210               nth outer_set_bds j]
   211           val single_set_bd_thmss =
   212             map ((fn f => map f (0 upto olive - 1)) o comp_single_set_bd_thm) (0 upto ilive - 1);
   213         in
   214           map2 (fn comp_set_alt => fn single_set_bds => fn {context, ...} =>
   215             mk_comp_set_bd_tac context comp_set_alt single_set_bds)
   216           comp_set_alt_thms single_set_bd_thmss
   217         end;
   218 
   219     val comp_in_alt_thm =
   220       let
   221         val comp_in = mk_in Asets comp_sets CCA;
   222         val comp_in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
   223         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (comp_in, comp_in_alt));
   224       in
   225         Skip_Proof.prove lthy [] [] goal
   226           (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
   227         |> Thm.close_derivation
   228       end;
   229 
   230     fun comp_in_bd_tac _ =
   231       mk_comp_in_bd_tac comp_in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
   232         (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
   233 
   234     fun comp_map_wpull_tac _ =
   235       mk_map_wpull_tac comp_in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
   236 
   237     val tacs = [comp_map_id_tac, comp_map_comp_tac, comp_map_cong_tac] @ comp_set_natural_tacs @
   238       [comp_bd_card_order_tac, comp_bd_cinfinite_tac] @ comp_set_bd_tacs @
   239       [comp_in_bd_tac, comp_map_wpull_tac];
   240 
   241     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
   242 
   243     val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
   244       (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
   245         Dss inwitss inners);
   246 
   247     val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
   248 
   249     val comp_wits = (inner_witsss, (map (single o snd) outer_wits))
   250       |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
   251       |> flat
   252       |> map (`(fn t => Term.add_frees t []))
   253       |> minimize_wits
   254       |> map (fn (frees, t) => fold absfree frees t);
   255 
   256     fun wit_tac {context = ctxt, ...} =
   257       mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
   258         (maps wit_thms_of_bnf inners);
   259 
   260     val (bnf', lthy') =
   261       bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
   262         ((((b, comp_map), comp_sets), comp_bd), comp_wits) lthy;
   263 
   264     val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
   265     val outer_rel_cong = rel_cong_of_bnf outer;
   266 
   267     val comp_rel_unfold_thm =
   268       trans OF [rel_def_of_bnf bnf',
   269         trans OF [comp_in_alt_thm RS @{thm subst_rel_def},
   270           trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
   271             [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
   272               rel_converse_of_bnf outer RS sym], outer_rel_Gr],
   273             trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
   274               (map (fn bnf => rel_def_of_bnf bnf RS sym) inners)]]]];
   275 
   276     val comp_pred_unfold_thm = Collect_split_box_equals OF [comp_rel_unfold_thm,
   277       pred_def_of_bnf bnf' RS abs_pred_sym,
   278         trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners),
   279           pred_def_of_bnf outer RS abs_pred_sym]];
   280 
   281     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
   282       comp_rel_unfold_thm comp_pred_unfold_thm unfold;
   283   in
   284     (bnf', (unfold', lthy'))
   285   end;
   286 
   287 (* Killing live variables *)
   288 
   289 fun killN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   290   let
   291     val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
   292     val live = live_of_bnf bnf;
   293     val dead = dead_of_bnf bnf;
   294     val nwits = nwits_of_bnf bnf;
   295 
   296     (* TODO: check 0 < n <= live *)
   297 
   298     val (Ds, lthy1) = apfst (map TFree)
   299       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   300     val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
   301       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   302     val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
   303       (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
   304 
   305     val ((Asets, lives), _(*names_lthy*)) = lthy
   306       |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As))
   307       ||>> mk_Frees "x" (drop n As);
   308     val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
   309 
   310     val T = mk_T_of_bnf Ds As bnf;
   311 
   312     (*bnf.map id ... id*)
   313     val killN_map = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
   314 
   315     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   316     val killN_sets = drop n bnf_sets;
   317 
   318     (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
   319     val bnf_bd = mk_bd_of_bnf Ds As bnf;
   320     val killN_bd = mk_cprod
   321       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
   322 
   323     fun killN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   324     fun killN_map_comp_tac {context, ...} =
   325       Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   326       rtac refl 1;
   327     fun killN_map_cong_tac {context, ...} =
   328       mk_killN_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
   329     val killN_set_natural_tacs =
   330       map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
   331     fun killN_bd_card_order_tac _ = mk_killN_bd_card_order_tac n (bd_card_order_of_bnf bnf);
   332     fun killN_bd_cinfinite_tac _ = mk_killN_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
   333     val killN_set_bd_tacs =
   334       map (fn thm => fn _ => mk_killN_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
   335         (drop n (set_bd_of_bnf bnf));
   336 
   337     val killN_in_alt_thm =
   338       let
   339         val killN_in = mk_in Asets killN_sets T;
   340         val killN_in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
   341         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (killN_in, killN_in_alt));
   342       in
   343         Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
   344       end;
   345 
   346     fun killN_in_bd_tac _ =
   347       mk_killN_in_bd_tac n (live > n) killN_in_alt_thm (in_bd_of_bnf bnf)
   348          (bd_Card_order_of_bnf bnf) (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
   349     fun killN_map_wpull_tac _ =
   350       mk_map_wpull_tac killN_in_alt_thm [] (map_wpull_of_bnf bnf);
   351 
   352     val tacs = [killN_map_id_tac, killN_map_comp_tac, killN_map_cong_tac] @ killN_set_natural_tacs @
   353       [killN_bd_card_order_tac, killN_bd_cinfinite_tac] @ killN_set_bd_tacs @
   354       [killN_in_bd_tac, killN_map_wpull_tac];
   355 
   356     val wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
   357 
   358     val killN_wits = map (fn t => fold absfree (Term.add_frees t []) t)
   359       (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) wits);
   360 
   361     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   362 
   363     val (bnf', lthy') =
   364       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
   365         ((((b, killN_map), killN_sets), Term.absdummy T killN_bd), killN_wits) lthy;
   366 
   367     val rel_Gr = rel_Gr_of_bnf bnf RS sym;
   368 
   369     val killN_rel_unfold_thm =
   370       trans OF [rel_def_of_bnf bnf',
   371         trans OF [killN_in_alt_thm RS @{thm subst_rel_def},
   372           trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
   373             [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym],
   374               rel_Gr],
   375             trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
   376               (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
   377                replicate (live - n) @{thm Gr_fst_snd})]]]];
   378 
   379     val killN_pred_unfold_thm = Collect_split_box_equals OF
   380       [Local_Defs.unfold lthy' @{thms Id_def'} killN_rel_unfold_thm,
   381         pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
   382 
   383     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
   384       killN_rel_unfold_thm killN_pred_unfold_thm unfold;
   385   in
   386     (bnf', (unfold', lthy'))
   387   end;
   388 
   389 (* Adding dummy live variables *)
   390 
   391 fun liftN_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   392   let
   393     val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
   394     val live = live_of_bnf bnf;
   395     val dead = dead_of_bnf bnf;
   396     val nwits = nwits_of_bnf bnf;
   397 
   398     (* TODO: check 0 < n *)
   399 
   400     val (Ds, lthy1) = apfst (map TFree)
   401       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   402     val ((newAs, As), lthy2) = apfst (chop n o map TFree)
   403       (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
   404     val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
   405       (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
   406 
   407     val (Asets, _(*names_lthy*)) = lthy
   408       |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As));
   409 
   410     val T = mk_T_of_bnf Ds As bnf;
   411 
   412     (*%f1 ... fn. bnf.map*)
   413     val liftN_map =
   414       fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
   415 
   416     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   417     val liftN_sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
   418 
   419     val liftN_bd = mk_bd_of_bnf Ds As bnf;
   420 
   421     fun liftN_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   422     fun liftN_map_comp_tac {context, ...} =
   423       Local_Defs.unfold_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   424       rtac refl 1;
   425     fun liftN_map_cong_tac {context, ...} =
   426       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
   427     val liftN_set_natural_tacs =
   428       if ! quick_and_dirty then
   429         replicate (n + live) (K all_tac)
   430       else
   431         replicate n (K empty_natural_tac) @
   432         map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
   433     fun liftN_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   434     fun liftN_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   435     val liftN_set_bd_tacs =
   436       if ! quick_and_dirty then
   437         replicate (n + live) (K all_tac)
   438       else
   439         replicate n (K (mk_liftN_set_bd_tac (bd_Card_order_of_bnf bnf))) @
   440         (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   441 
   442     val liftN_in_alt_thm =
   443       let
   444         val liftN_in = mk_in Asets liftN_sets T;
   445         val liftN_in_alt = mk_in (drop n Asets) bnf_sets T;
   446         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (liftN_in, liftN_in_alt));
   447       in
   448         Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
   449       end;
   450 
   451     fun liftN_in_bd_tac _ =
   452       mk_liftN_in_bd_tac n liftN_in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
   453     fun liftN_map_wpull_tac _ =
   454       mk_map_wpull_tac liftN_in_alt_thm [] (map_wpull_of_bnf bnf);
   455 
   456     val tacs = [liftN_map_id_tac, liftN_map_comp_tac, liftN_map_cong_tac] @ liftN_set_natural_tacs @
   457       [liftN_bd_card_order_tac, liftN_bd_cinfinite_tac] @ liftN_set_bd_tacs @
   458       [liftN_in_bd_tac, liftN_map_wpull_tac];
   459 
   460     val liftN_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   461 
   462     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   463 
   464     val (bnf', lthy') =
   465       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
   466         ((((b, liftN_map), liftN_sets), Term.absdummy T liftN_bd), liftN_wits) lthy;
   467 
   468     val liftN_rel_unfold_thm =
   469       trans OF [rel_def_of_bnf bnf',
   470         trans OF [liftN_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
   471 
   472     val liftN_pred_unfold_thm = Collect_split_box_equals OF [liftN_rel_unfold_thm,
   473       pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
   474 
   475     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
   476       liftN_rel_unfold_thm liftN_pred_unfold_thm unfold;
   477   in
   478     (bnf', (unfold', lthy'))
   479   end;
   480 
   481 (* Changing the order of live variables *)
   482 
   483 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
   484   let
   485     val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
   486     val live = live_of_bnf bnf;
   487     val dead = dead_of_bnf bnf;
   488     val nwits = nwits_of_bnf bnf;
   489     fun permute xs = mk_permute src dest xs;
   490     fun permute_rev xs = mk_permute dest src xs;
   491 
   492     val (Ds, lthy1) = apfst (map TFree)
   493       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   494     val (As, lthy2) = apfst (map TFree)
   495       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   496     val (Bs, _(*lthy3*)) = apfst (map TFree)
   497       (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
   498 
   499     val (Asets, _(*names_lthy*)) = lthy
   500       |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As));
   501 
   502     val T = mk_T_of_bnf Ds As bnf;
   503 
   504     (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
   505     val permute_map = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
   506       (Term.list_comb (mk_map_of_bnf Ds As Bs bnf,
   507         permute_rev (map Bound ((live - 1) downto 0))));
   508 
   509     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   510     val permute_sets = permute bnf_sets;
   511 
   512     val permute_bd = mk_bd_of_bnf Ds As bnf;
   513 
   514     fun permute_map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   515     fun permute_map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
   516     fun permute_map_cong_tac {context, ...} =
   517       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
   518     val permute_set_natural_tacs =
   519       permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
   520     fun permute_bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   521     fun permute_bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   522     val permute_set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   523 
   524     val permute_in_alt_thm =
   525       let
   526         val permute_in = mk_in Asets permute_sets T;
   527         val permute_in_alt = mk_in (permute_rev Asets) bnf_sets T;
   528         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (permute_in, permute_in_alt));
   529       in
   530         Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
   531         |> Thm.close_derivation
   532       end;
   533 
   534     fun permute_in_bd_tac _ =
   535       mk_permute_in_bd_tac src dest permute_in_alt_thm (in_bd_of_bnf bnf)
   536         (bd_Card_order_of_bnf bnf);
   537     fun permute_map_wpull_tac _ =
   538       mk_map_wpull_tac permute_in_alt_thm [] (map_wpull_of_bnf bnf);
   539 
   540     val tacs = [permute_map_id_tac, permute_map_comp_tac, permute_map_cong_tac] @
   541       permute_set_natural_tacs @ [permute_bd_card_order_tac, permute_bd_cinfinite_tac] @
   542       permute_set_bd_tacs @ [permute_in_bd_tac, permute_map_wpull_tac];
   543 
   544     val permute_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   545 
   546     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   547 
   548     val (bnf', lthy') =
   549       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
   550         ((((b, permute_map), permute_sets), Term.absdummy T permute_bd), permute_wits) lthy;
   551 
   552     val permute_rel_unfold_thm =
   553       trans OF [rel_def_of_bnf bnf',
   554         trans OF [permute_in_alt_thm RS @{thm subst_rel_def}, rel_def_of_bnf bnf RS sym]];
   555 
   556     val permute_pred_unfold_thm = Collect_split_box_equals OF [permute_rel_unfold_thm,
   557       pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
   558 
   559     val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf')
   560       permute_rel_unfold_thm permute_pred_unfold_thm unfold;
   561   in
   562     (bnf', (unfold', lthy'))
   563   end;
   564 
   565 (* Composition pipeline *)
   566 
   567 fun permute_and_kill qualify n src dest bnf =
   568   bnf
   569   |> permute_bnf qualify src dest
   570   #> uncurry (killN_bnf qualify n);
   571 
   572 fun lift_and_permute qualify n src dest bnf =
   573   bnf
   574   |> liftN_bnf qualify n
   575   #> uncurry (permute_bnf qualify src dest);
   576 
   577 fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =
   578   let
   579     val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
   580     val kill_poss = map (find_indices Ds) Ass;
   581     val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
   582     val before_kill_dest = map2 append kill_poss live_poss;
   583     val kill_ns = map length kill_poss;
   584     val (inners', (unfold', lthy')) =
   585       fold_map5 (fn i => permute_and_kill (qualify i))
   586         (if length bnfs = 1 then [0] else (1 upto length bnfs))
   587         kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy);
   588 
   589     val Ass' = map2 (map o nth) Ass live_poss;
   590     val As = sort Ass';
   591     val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
   592     val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
   593     val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
   594     val after_lift_src = map2 append new_poss old_poss;
   595     val lift_ns = map (fn xs => length As - length xs) Ass';
   596   in
   597     ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
   598       (if length bnfs = 1 then [0] else (1 upto length bnfs))
   599       lift_ns after_lift_src after_lift_dest inners' (unfold', lthy'))
   600   end;
   601 
   602 fun default_comp_sort Ass =
   603   Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
   604 
   605 fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
   606   let
   607     val name = Binding.name_of b;
   608     fun qualify i bind =
   609       let val namei = if i > 0 then name ^ string_of_int i else name;
   610       in
   611         if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
   612         else qualify' (Binding.prefix_name namei bind)
   613       end;
   614 
   615     val Ass = map (map Term.dest_TFree) tfreess;
   616     val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
   617 
   618     val ((kill_poss, As), (inners', (unfold', lthy'))) =
   619       normalize_bnfs qualify Ass Ds sort inners unfold lthy;
   620 
   621     val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
   622     val As = map TFree As;
   623   in
   624     apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
   625   end;
   626 
   627 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
   628 
   629 fun seal_bnf unfold b Ds bnf lthy =
   630   let
   631     val live = live_of_bnf bnf;
   632     val nwits = nwits_of_bnf bnf;
   633 
   634     val (As, lthy1) = apfst (map TFree)
   635       (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
   636     val (Bs, _) = apfst (map TFree)
   637       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   638 
   639     val map_unfolds = filter_refl (map_unfolds_of unfold);
   640     val set_unfoldss = map filter_refl (set_unfoldss_of unfold);
   641 
   642     val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
   643       map_unfolds);
   644     val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
   645       set_unfoldss);
   646     val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
   647     val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
   648     val unfold_defs = unfold_sets o unfold_maps;
   649     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
   650     val bnf_sets = map (expand_maps o expand_sets)
   651       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
   652     val bnf_bd = mk_bd_of_bnf Ds As bnf;
   653     val T = mk_T_of_bnf Ds As bnf;
   654 
   655     (*bd should only depend on dead type variables!*)
   656     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
   657     val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
   658     val params = fold Term.add_tfreesT Ds [];
   659     val deads = map TFree params;
   660 
   661     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
   662       typedef false NONE (bdT_bind, params, NoSyn)
   663         (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   664 
   665     val bnf_bd' = mk_dir_image bnf_bd
   666       (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
   667 
   668     val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
   669     val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
   670 
   671     val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
   672     val bd_card_order =
   673       @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
   674     val bd_cinfinite =
   675       (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
   676 
   677     val set_bds =
   678       map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
   679     val in_bd =
   680       @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
   681         @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
   682           @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
   683             bd_Card_order_of_bnf bnf]];
   684 
   685     fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
   686       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   687     val tacs =
   688       map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @
   689         set_natural_of_bnf bnf) @
   690       map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @
   691       map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]);
   692 
   693     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   694 
   695     fun wit_tac _ = mk_simple_wit_tac (map unfold_defs (wit_thms_of_bnf bnf));
   696 
   697     val (bnf', lthy') = bnf_def Hardly_Inline (K Derive_All_Facts) I tacs wit_tac (SOME deads)
   698       ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
   699 
   700     val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
   701     val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
   702 
   703     val rel_def = unfold_defs' (rel_def_of_bnf bnf');
   704     val rel_unfold = Local_Defs.unfold lthy'
   705       (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_def;
   706 
   707     val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_def_of_bnf bnf']);
   708 
   709     val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
   710     val pred_unfold = Local_Defs.unfold lthy'
   711       (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
   712 
   713     val notes =
   714       [(rel_unfoldN, [rel_unfold]),
   715       (pred_unfoldN, [pred_unfold])]
   716       |> map (fn (thmN, thms) =>
   717         ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   718   in
   719     ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
   720   end;
   721 
   722 fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
   723     ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
   724       (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
   725   | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
   726   | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
   727     let
   728       val tfrees = Term.add_tfreesT T [];
   729       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
   730     in
   731       (case bnf_opt of
   732         NONE => ((Basic_BNFs.DEADID_bnf, ([T], [])), (unfold, lthy))
   733       | SOME bnf =>
   734         if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
   735           let
   736             val T' = T_of_bnf bnf;
   737             val deads = deads_of_bnf bnf;
   738             val lives = lives_of_bnf bnf;
   739             val tvars' = Term.add_tvarsT T' [];
   740             val deads_lives =
   741               pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
   742                 (deads, lives);
   743             val rel_def = rel_def_of_bnf bnf;
   744             val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_def RS sym))
   745               (SOME (Local_Defs.unfold lthy [rel_def] (pred_def_of_bnf bnf) RS sym)) unfold;
   746           in ((bnf, deads_lives), (unfold', lthy)) end
   747         else
   748           let
   749             val name = Binding.name_of b;
   750             fun qualify i bind =
   751               let val namei = if i > 0 then name ^ string_of_int i else name;
   752               in
   753                 if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
   754                 else qualify' (Binding.prefix_name namei bind)
   755               end;
   756             val odead = dead_of_bnf bnf;
   757             val olive = live_of_bnf bnf;
   758             val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
   759               (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
   760             val oDs = map (nth Ts) oDs_pos;
   761             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
   762             val ((inners, (Dss, Ass)), (unfold', lthy')) =
   763               apfst (apsnd split_list o split_list)
   764                 (fold_map2 (fn i =>
   765                   bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
   766                 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
   767           in
   768             compose_bnf const_policy (qualify 0) b sort bnf inners oDs Dss Ass (unfold', lthy')
   769           end)
   770     end;
   771 
   772 end;