src/HOL/BNF/Tools/bnf_comp.ML
author blanchet
Fri Sep 21 16:45:06 2012 +0200 (2012-09-21)
changeset 49510 ba50d204095e
parent 49509 src/HOL/Codatatype/Tools/bnf_comp.ML@163914705f8d
child 49512 82d99fe04018
permissions -rw-r--r--
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
     1 (*  Title:      HOL/BNF/Tools/bnf_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_set
    12   val empty_unfolds: unfold_set
    13   val map_unfolds_of: unfold_set -> thm list
    14   val rel_unfolds_of: unfold_set -> thm list
    15   val set_unfoldss_of: unfold_set -> thm list list
    16   val srel_unfolds_of: unfold_set -> thm list
    17 
    18   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
    19     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
    20     (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * 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_set -> Proof.context ->
    24     (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
    25   val seal_bnf: unfold_set -> 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_set = {
    38   map_unfolds: thm list,
    39   set_unfoldss: thm list list,
    40   rel_unfolds: thm list,
    41   srel_unfolds: thm list
    42 };
    43 
    44 val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], srel_unfolds = []};
    45 
    46 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
    47 fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
    48 
    49 fun add_to_unfolds map sets rel srel
    50   {map_unfolds, set_unfoldss, rel_unfolds, srel_unfolds} =
    51   {map_unfolds = add_to_thms map_unfolds map,
    52     set_unfoldss = adds_to_thms set_unfoldss sets,
    53     rel_unfolds = add_to_thms rel_unfolds rel,
    54     srel_unfolds = add_to_thms srel_unfolds srel};
    55 
    56 fun add_bnf_to_unfolds bnf =
    57   add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf)
    58     (srel_def_of_bnf bnf);
    59 
    60 val map_unfolds_of = #map_unfolds;
    61 val set_unfoldss_of = #set_unfoldss;
    62 val rel_unfolds_of = #rel_unfolds;
    63 val srel_unfolds_of = #srel_unfolds;
    64 
    65 val bdTN = "bdT";
    66 
    67 fun mk_killN n = "_kill" ^ string_of_int n;
    68 fun mk_liftN n = "_lift" ^ string_of_int n;
    69 fun mk_permuteN src dest =
    70   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
    71 
    72 (*copied from Envir.expand_term_free*)
    73 fun expand_term_const defs =
    74   let
    75     val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
    76     val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
    77   in Envir.expand_term get end;
    78 
    79 fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
    80   let
    81     val olive = live_of_bnf outer;
    82     val onwits = nwits_of_bnf outer;
    83     val odead = dead_of_bnf outer;
    84     val inner = hd inners;
    85     val ilive = live_of_bnf inner;
    86     val ideads = map dead_of_bnf inners;
    87     val inwitss = map nwits_of_bnf inners;
    88 
    89     (* TODO: check olive = length inners > 0,
    90                    forall inner from inners. ilive = live,
    91                    forall inner from inners. idead = dead  *)
    92 
    93     val (oDs, lthy1) = apfst (map TFree)
    94       (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
    95     val (Dss, lthy2) = apfst (map (map TFree))
    96         (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
    97     val (Ass, lthy3) = apfst (replicate ilive o map TFree)
    98       (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
    99     val As = if ilive > 0 then hd Ass else [];
   100     val Ass_repl = replicate olive As;
   101     val (Bs, _(*lthy4*)) = apfst (map TFree)
   102       (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
   103     val Bss_repl = replicate olive Bs;
   104 
   105     val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
   106       |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
   107       ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
   108       ||>> mk_Frees "A" (map HOLogic.mk_setT As)
   109       ||>> mk_Frees "x" As;
   110 
   111     val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
   112     val CCA = mk_T_of_bnf oDs CAs outer;
   113     val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
   114     val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
   115     val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
   116     val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
   117     val outer_bd = mk_bd_of_bnf oDs CAs outer;
   118 
   119     (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
   120     val mapx = fold_rev Term.abs fs'
   121       (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
   122         map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
   123           mk_map_of_bnf Ds As Bs) Dss inners));
   124     (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*)
   125     val rel = fold_rev Term.abs Qs'
   126       (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
   127         map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
   128           mk_rel_of_bnf Ds As Bs) Dss inners));
   129 
   130     (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
   131     (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
   132     fun mk_set i =
   133       let
   134         val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
   135         val outer_set = mk_collect
   136           (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
   137           (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
   138         val inner_sets = map (fn sets => nth sets i) inner_setss;
   139         val outer_map = mk_map_of_bnf oDs CAs setTs outer;
   140         val map_inner_sets = Term.list_comb (outer_map, inner_sets);
   141         val collect_image = mk_collect
   142           (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
   143           (CCA --> HOLogic.mk_setT T);
   144       in
   145         (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
   146         HOLogic.mk_comp (mk_Union T, collect_image))
   147       end;
   148 
   149     val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
   150 
   151     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
   152     val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
   153 
   154     fun map_id_tac {context = ctxt, ...} =
   155       let
   156         (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
   157           rules*)
   158         val thms = (map map_id_of_bnf inners
   159           |> map (`(Term.size_of_term o Thm.prop_of))
   160           |> sort (rev_order o int_ord o pairself fst)
   161           |> map snd) @ [map_id_of_bnf outer];
   162       in
   163         (EVERY' (map (fn thm => subst_tac ctxt [thm]) thms) THEN' rtac refl) 1
   164       end;
   165 
   166     fun map_comp_tac _ =
   167       mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
   168         (map map_comp_of_bnf inners);
   169 
   170     fun mk_single_set_natural_tac i _ =
   171       mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
   172         (collect_set_natural_of_bnf outer)
   173         (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
   174 
   175     val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1);
   176 
   177     fun bd_card_order_tac _ =
   178       mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
   179 
   180     fun bd_cinfinite_tac _ =
   181       mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
   182 
   183     val set_alt_thms =
   184       if ! quick_and_dirty then
   185         []
   186       else
   187         map (fn goal =>
   188           Skip_Proof.prove lthy [] [] goal
   189             (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
   190           |> Thm.close_derivation)
   191         (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
   192 
   193     fun map_cong_tac _ =
   194       mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
   195 
   196     val set_bd_tacs =
   197       if ! quick_and_dirty then
   198         replicate (length set_alt_thms) (K all_tac)
   199       else
   200         let
   201           val outer_set_bds = set_bd_of_bnf outer;
   202           val inner_set_bdss = map set_bd_of_bnf inners;
   203           val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
   204           fun single_set_bd_thm i j =
   205             @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
   206               nth outer_set_bds j]
   207           val single_set_bd_thmss =
   208             map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
   209         in
   210           map2 (fn set_alt => fn single_set_bds => fn {context, ...} =>
   211             mk_comp_set_bd_tac context set_alt single_set_bds)
   212           set_alt_thms single_set_bd_thmss
   213         end;
   214 
   215     val in_alt_thm =
   216       let
   217         val inx = mk_in Asets sets CCA;
   218         val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
   219         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   220       in
   221         Skip_Proof.prove lthy [] [] goal
   222           (fn {context, ...} => mk_comp_in_alt_tac context set_alt_thms)
   223         |> Thm.close_derivation
   224       end;
   225 
   226     fun in_bd_tac _ =
   227       mk_comp_in_bd_tac in_alt_thm (map in_bd_of_bnf inners) (in_bd_of_bnf outer)
   228         (map bd_Cinfinite_of_bnf inners) (bd_Card_order_of_bnf outer);
   229 
   230     fun map_wpull_tac _ =
   231       mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
   232 
   233     fun srel_O_Gr_tac _ =
   234       let
   235         val basic_thms = @{thms mem_Collect_eq fst_conv snd_conv}; (*TODO: tune*)
   236         val outer_srel_Gr = srel_Gr_of_bnf outer RS sym;
   237         val outer_srel_cong = srel_cong_of_bnf outer;
   238         val thm =
   239           (trans OF [in_alt_thm RS @{thm subst_rel_def},
   240              trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
   241                [trans OF [outer_srel_Gr RS @{thm arg_cong[of _ _ converse]},
   242                  srel_converse_of_bnf outer RS sym], outer_srel_Gr],
   243                trans OF [srel_O_of_bnf outer RS sym, outer_srel_cong OF
   244                  (map (fn bnf => srel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
   245           |> unfold_thms lthy (basic_thms @ srel_def_of_bnf outer :: map srel_def_of_bnf inners);
   246       in
   247         unfold_thms_tac lthy basic_thms THEN rtac thm 1
   248       end;
   249 
   250     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
   251       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   252 
   253     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
   254 
   255     val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
   256       (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
   257         Dss inwitss inners);
   258 
   259     val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
   260 
   261     val wits = (inner_witsss, (map (single o snd) outer_wits))
   262       |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
   263       |> flat
   264       |> map (`(fn t => Term.add_frees t []))
   265       |> minimize_wits
   266       |> map (fn (frees, t) => fold absfree frees t);
   267 
   268     fun wit_tac {context = ctxt, ...} =
   269       mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
   270         (maps wit_thms_of_bnf inners);
   271 
   272     val (bnf', lthy') =
   273       bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
   274         (((((b, mapx), sets), bd), wits), SOME rel) lthy;
   275   in
   276     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   277   end;
   278 
   279 (* Killing live variables *)
   280 
   281 fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   282   let
   283     val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
   284     val live = live_of_bnf bnf;
   285     val dead = dead_of_bnf bnf;
   286     val nwits = nwits_of_bnf bnf;
   287 
   288     (* TODO: check 0 < n <= live *)
   289 
   290     val (Ds, lthy1) = apfst (map TFree)
   291       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   292     val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
   293       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   294     val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
   295       (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
   296 
   297     val ((Asets, lives), _(*names_lthy*)) = lthy
   298       |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
   299       ||>> mk_Frees "x" (drop n As);
   300     val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
   301 
   302     val T = mk_T_of_bnf Ds As bnf;
   303 
   304     (*bnf.map id ... id*)
   305     val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
   306     (*bnf.rel (op =) ... (op =)*)
   307     val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
   308 
   309     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   310     val sets = drop n bnf_sets;
   311 
   312     (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
   313     val bnf_bd = mk_bd_of_bnf Ds As bnf;
   314     val bd = mk_cprod
   315       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
   316 
   317     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   318     fun map_comp_tac {context, ...} =
   319       unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   320       rtac refl 1;
   321     fun map_cong_tac {context, ...} =
   322       mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
   323     val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
   324     fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
   325     fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
   326     val set_bd_tacs =
   327       map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
   328         (drop n (set_bd_of_bnf bnf));
   329 
   330     val in_alt_thm =
   331       let
   332         val inx = mk_in Asets sets T;
   333         val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
   334         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   335       in
   336         Skip_Proof.prove lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
   337       end;
   338 
   339     fun in_bd_tac _ =
   340       mk_kill_in_bd_tac n (live > n) in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf)
   341         (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
   342     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
   343 
   344     fun srel_O_Gr_tac _ =
   345       let
   346         val srel_Gr = srel_Gr_of_bnf bnf RS sym
   347         val thm =
   348           (trans OF [in_alt_thm RS @{thm subst_rel_def},
   349             trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
   350               [trans OF [srel_Gr RS @{thm arg_cong[of _ _ converse]},
   351                 srel_converse_of_bnf bnf RS sym], srel_Gr],
   352               trans OF [srel_O_of_bnf bnf RS sym, srel_cong_of_bnf bnf OF
   353                 (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
   354                  replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
   355           |> unfold_thms lthy (srel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
   356       in
   357         rtac thm 1
   358       end;
   359 
   360     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
   361       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   362 
   363     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
   364 
   365     val wits = map (fn t => fold absfree (Term.add_frees t []) t)
   366       (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
   367 
   368     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   369 
   370     val (bnf', lthy') =
   371       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
   372         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   373   in
   374     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   375   end;
   376 
   377 (* Adding dummy live variables *)
   378 
   379 fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   380   let
   381     val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
   382     val live = live_of_bnf bnf;
   383     val dead = dead_of_bnf bnf;
   384     val nwits = nwits_of_bnf bnf;
   385 
   386     (* TODO: check 0 < n *)
   387 
   388     val (Ds, lthy1) = apfst (map TFree)
   389       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   390     val ((newAs, As), lthy2) = apfst (chop n o map TFree)
   391       (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
   392     val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
   393       (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
   394 
   395     val (Asets, _(*names_lthy*)) = lthy
   396       |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
   397 
   398     val T = mk_T_of_bnf Ds As bnf;
   399 
   400     (*%f1 ... fn. bnf.map*)
   401     val mapx =
   402       fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
   403     (*%Q1 ... Qn. bnf.rel*)
   404     val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
   405 
   406     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   407     val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
   408 
   409     val bd = mk_bd_of_bnf Ds As bnf;
   410 
   411     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   412     fun map_comp_tac {context, ...} =
   413       unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   414       rtac refl 1;
   415     fun map_cong_tac {context, ...} =
   416       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
   417     val set_natural_tacs =
   418       if ! quick_and_dirty then
   419         replicate (n + live) (K all_tac)
   420       else
   421         replicate n (K empty_natural_tac) @
   422         map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
   423     fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   424     fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   425     val set_bd_tacs =
   426       if ! quick_and_dirty then
   427         replicate (n + live) (K all_tac)
   428       else
   429         replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
   430         (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   431 
   432     val in_alt_thm =
   433       let
   434         val inx = mk_in Asets sets T;
   435         val in_alt = mk_in (drop n Asets) bnf_sets T;
   436         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   437       in
   438         Skip_Proof.prove lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
   439       end;
   440 
   441     fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
   442     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
   443 
   444     fun srel_O_Gr_tac _ =
   445       mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   446 
   447     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
   448       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   449 
   450     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   451 
   452     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   453 
   454     val (bnf', lthy') =
   455       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
   456         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   457 
   458   in
   459     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   460   end;
   461 
   462 (* Changing the order of live variables *)
   463 
   464 fun permute_bnf qualify src dest bnf (unfold_set, lthy) =
   465   if src = dest then (bnf, (unfold_set, lthy)) else
   466   let
   467     val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
   468     val live = live_of_bnf bnf;
   469     val dead = dead_of_bnf bnf;
   470     val nwits = nwits_of_bnf bnf;
   471     fun permute xs = mk_permute src dest xs;
   472     fun permute_rev xs = mk_permute dest src xs;
   473 
   474     val (Ds, lthy1) = apfst (map TFree)
   475       (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   476     val (As, lthy2) = apfst (map TFree)
   477       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   478     val (Bs, _(*lthy3*)) = apfst (map TFree)
   479       (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
   480 
   481     val (Asets, _(*names_lthy*)) = lthy
   482       |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
   483 
   484     val T = mk_T_of_bnf Ds As bnf;
   485 
   486     (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
   487     val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
   488       (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
   489     (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
   490     val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
   491       (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound (live - 1 downto 0))));
   492 
   493     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   494     val sets = permute bnf_sets;
   495 
   496     val bd = mk_bd_of_bnf Ds As bnf;
   497 
   498     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
   499     fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
   500     fun map_cong_tac {context, ...} =
   501       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
   502     val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
   503     fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   504     fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   505     val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   506 
   507     val in_alt_thm =
   508       let
   509         val inx = mk_in Asets sets T;
   510         val in_alt = mk_in (permute_rev Asets) bnf_sets T;
   511         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   512       in
   513         Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
   514         |> Thm.close_derivation
   515       end;
   516 
   517     fun in_bd_tac _ =
   518       mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
   519     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
   520 
   521     fun srel_O_Gr_tac _ =
   522       mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   523 
   524     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
   525       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   526 
   527     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   528 
   529     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   530 
   531     val (bnf', lthy') =
   532       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
   533         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   534   in
   535     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   536   end;
   537 
   538 (* Composition pipeline *)
   539 
   540 fun permute_and_kill qualify n src dest bnf =
   541   bnf
   542   |> permute_bnf qualify src dest
   543   #> uncurry (kill_bnf qualify n);
   544 
   545 fun lift_and_permute qualify n src dest bnf =
   546   bnf
   547   |> lift_bnf qualify n
   548   #> uncurry (permute_bnf qualify src dest);
   549 
   550 fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy =
   551   let
   552     val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
   553     val kill_poss = map (find_indices Ds) Ass;
   554     val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
   555     val before_kill_dest = map2 append kill_poss live_poss;
   556     val kill_ns = map length kill_poss;
   557     val (inners', (unfold_set', lthy')) =
   558       fold_map5 (fn i => permute_and_kill (qualify i))
   559         (if length bnfs = 1 then [0] else (1 upto length bnfs))
   560         kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy);
   561 
   562     val Ass' = map2 (map o nth) Ass live_poss;
   563     val As = sort Ass';
   564     val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
   565     val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
   566     val new_poss = map2 (subtract (op =)) old_poss after_lift_dest;
   567     val after_lift_src = map2 append new_poss old_poss;
   568     val lift_ns = map (fn xs => length As - length xs) Ass';
   569   in
   570     ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
   571       (if length bnfs = 1 then [0] else (1 upto length bnfs))
   572       lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy'))
   573   end;
   574 
   575 fun default_comp_sort Ass =
   576   Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
   577 
   578 fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) =
   579   let
   580     val b = name_of_bnf outer;
   581 
   582     val Ass = map (map Term.dest_TFree) tfreess;
   583     val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
   584 
   585     val ((kill_poss, As), (inners', (unfold_set', lthy'))) =
   586       normalize_bnfs qualify Ass Ds sort inners unfold_set lthy;
   587 
   588     val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
   589     val As = map TFree As;
   590   in
   591     apfst (rpair (Ds, As))
   592       (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))
   593   end;
   594 
   595 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
   596 
   597 fun seal_bnf unfold_set b Ds bnf lthy =
   598   let
   599     val live = live_of_bnf bnf;
   600     val nwits = nwits_of_bnf bnf;
   601 
   602     val (As, lthy1) = apfst (map TFree)
   603       (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
   604     val (Bs, _) = apfst (map TFree)
   605       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   606 
   607     val map_unfolds = map_unfolds_of unfold_set;
   608     val set_unfoldss = set_unfoldss_of unfold_set;
   609     val rel_unfolds = rel_unfolds_of unfold_set;
   610     val srel_unfolds = srel_unfolds_of unfold_set;
   611 
   612     val expand_maps =
   613       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
   614     val expand_sets =
   615       fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
   616     val expand_rels =
   617       fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
   618     val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
   619     val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
   620     val unfold_rels = unfold_thms lthy rel_unfolds;
   621     val unfold_srels = unfold_thms lthy srel_unfolds;
   622     val unfold_all = unfold_sets o unfold_maps o unfold_rels o unfold_srels;
   623     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
   624     val bnf_sets = map (expand_maps o expand_sets)
   625       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
   626     val bnf_bd = mk_bd_of_bnf Ds As bnf;
   627     val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
   628     val T = mk_T_of_bnf Ds As bnf;
   629 
   630     (*bd should only depend on dead type variables!*)
   631     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
   632     val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
   633     val params = fold Term.add_tfreesT Ds [];
   634     val deads = map TFree params;
   635 
   636     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
   637       typedef false NONE (bdT_bind, params, NoSyn)
   638         (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   639 
   640     val bnf_bd' = mk_dir_image bnf_bd
   641       (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
   642 
   643     val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
   644     val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
   645 
   646     val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
   647     val bd_card_order =
   648       @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
   649     val bd_cinfinite =
   650       (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
   651 
   652     val set_bds =
   653       map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
   654     val in_bd =
   655       @{thm ordLeq_ordIso_trans} OF [in_bd_of_bnf bnf,
   656         @{thm cexp_cong2_Cnotzero} OF [bd_ordIso, if live = 0 then
   657           @{thm ctwo_Cnotzero} else @{thm ctwo_Cnotzero} RS @{thm csum_Cnotzero2},
   658             bd_Card_order_of_bnf bnf]];
   659 
   660     fun mk_tac thm {context = ctxt, prems = _} =
   661       (rtac (unfold_all thm) THEN'
   662       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   663 
   664     val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
   665       (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
   666       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
   667       (mk_tac (map_wpull_of_bnf bnf))
   668       (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
   669 
   670     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   671 
   672     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
   673 
   674     val policy = user_policy Derive_All_Facts;
   675 
   676     val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
   677       (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   678   in
   679     ((bnf', deads), lthy')
   680   end;
   681 
   682 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
   683 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
   684 
   685 fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
   686   | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
   687   | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
   688     let
   689       val tfrees = Term.add_tfreesT T [];
   690       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
   691     in
   692       (case bnf_opt of
   693         NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy))
   694       | SOME bnf =>
   695         if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
   696           let
   697             val T' = T_of_bnf bnf;
   698             val deads = deads_of_bnf bnf;
   699             val lives = lives_of_bnf bnf;
   700             val tvars' = Term.add_tvarsT T' [];
   701             val deads_lives =
   702               pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
   703                 (deads, lives);
   704           in ((bnf, deads_lives), (unfold_set, lthy)) end
   705         else
   706           let
   707             val name = Long_Name.base_name C;
   708             fun qualify i =
   709               let val namei = name ^ nonzero_string_of_int i;
   710               in qualify' o Binding.qualify true namei end;
   711             val odead = dead_of_bnf bnf;
   712             val olive = live_of_bnf bnf;
   713             val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
   714               (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
   715             val oDs = map (nth Ts) oDs_pos;
   716             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
   717             val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
   718               apfst (apsnd split_list o split_list)
   719                 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
   720                 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
   721           in
   722             compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
   723           end)
   724     end;
   725 
   726 end;