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