src/HOL/BNF/Tools/bnf_comp.ML
changeset 55058 4e700eb471d4
parent 55057 6b0fcbeebaba
child 55059 ef2e0fb783c6
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,704 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_comp.ML
     1.5 -    Author:     Dmitriy Traytel, TU Muenchen
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Copyright   2012
     1.8 -
     1.9 -Composition of bounded natural functors.
    1.10 -*)
    1.11 -
    1.12 -signature BNF_COMP =
    1.13 -sig
    1.14 -  val ID_bnf: BNF_Def.bnf
    1.15 -  val DEADID_bnf: BNF_Def.bnf
    1.16 -
    1.17 -  type unfold_set
    1.18 -  val empty_unfolds: unfold_set
    1.19 -
    1.20 -  exception BAD_DEAD of typ * typ
    1.21 -
    1.22 -  val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
    1.23 -    ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> typ ->
    1.24 -    unfold_set * Proof.context ->
    1.25 -    (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
    1.26 -  val default_comp_sort: (string * sort) list list -> (string * sort) list
    1.27 -  val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
    1.28 -    (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
    1.29 -    (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
    1.30 -  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf ->
    1.31 -    Proof.context -> (BNF_Def.bnf * typ list) * local_theory
    1.32 -end;
    1.33 -
    1.34 -structure BNF_Comp : BNF_COMP =
    1.35 -struct
    1.36 -
    1.37 -open BNF_Def
    1.38 -open BNF_Util
    1.39 -open BNF_Tactics
    1.40 -open BNF_Comp_Tactics
    1.41 -
    1.42 -val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
    1.43 -val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
    1.44 -
    1.45 -(* TODO: Replace by "BNF_Defs.defs list" *)
    1.46 -type unfold_set = {
    1.47 -  map_unfolds: thm list,
    1.48 -  set_unfoldss: thm list list,
    1.49 -  rel_unfolds: thm list
    1.50 -};
    1.51 -
    1.52 -val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
    1.53 -
    1.54 -fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
    1.55 -fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
    1.56 -
    1.57 -fun add_to_unfolds map sets rel
    1.58 -  {map_unfolds, set_unfoldss, rel_unfolds} =
    1.59 -  {map_unfolds = add_to_thms map_unfolds map,
    1.60 -    set_unfoldss = adds_to_thms set_unfoldss sets,
    1.61 -    rel_unfolds = add_to_thms rel_unfolds rel};
    1.62 -
    1.63 -fun add_bnf_to_unfolds bnf =
    1.64 -  add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf);
    1.65 -
    1.66 -val bdTN = "bdT";
    1.67 -
    1.68 -fun mk_killN n = "_kill" ^ string_of_int n;
    1.69 -fun mk_liftN n = "_lift" ^ string_of_int n;
    1.70 -fun mk_permuteN src dest =
    1.71 -  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
    1.72 -
    1.73 -(*copied from Envir.expand_term_free*)
    1.74 -fun expand_term_const defs =
    1.75 -  let
    1.76 -    val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
    1.77 -    val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
    1.78 -  in Envir.expand_term get end;
    1.79 -
    1.80 -fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
    1.81 -  let
    1.82 -    val olive = live_of_bnf outer;
    1.83 -    val onwits = nwits_of_bnf outer;
    1.84 -    val odead = dead_of_bnf outer;
    1.85 -    val inner = hd inners;
    1.86 -    val ilive = live_of_bnf inner;
    1.87 -    val ideads = map dead_of_bnf inners;
    1.88 -    val inwitss = map nwits_of_bnf inners;
    1.89 -
    1.90 -    (* TODO: check olive = length inners > 0,
    1.91 -                   forall inner from inners. ilive = live,
    1.92 -                   forall inner from inners. idead = dead  *)
    1.93 -
    1.94 -    val (oDs, lthy1) = apfst (map TFree)
    1.95 -      (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
    1.96 -    val (Dss, lthy2) = apfst (map (map TFree))
    1.97 -        (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
    1.98 -    val (Ass, lthy3) = apfst (replicate ilive o map TFree)
    1.99 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
   1.100 -    val As = if ilive > 0 then hd Ass else [];
   1.101 -    val Ass_repl = replicate olive As;
   1.102 -    val (Bs, _(*lthy4*)) = apfst (map TFree)
   1.103 -      (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
   1.104 -    val Bss_repl = replicate olive Bs;
   1.105 -
   1.106 -    val ((((fs', Qs'), Asets), xs), _(*names_lthy*)) = lthy
   1.107 -      |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs)
   1.108 -      ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs)
   1.109 -      ||>> mk_Frees "A" (map HOLogic.mk_setT As)
   1.110 -      ||>> mk_Frees "x" As;
   1.111 -
   1.112 -    val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
   1.113 -    val CCA = mk_T_of_bnf oDs CAs outer;
   1.114 -    val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
   1.115 -    val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
   1.116 -    val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
   1.117 -    val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
   1.118 -    val outer_bd = mk_bd_of_bnf oDs CAs outer;
   1.119 -
   1.120 -    (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
   1.121 -    val mapx = fold_rev Term.abs fs'
   1.122 -      (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
   1.123 -        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
   1.124 -          mk_map_of_bnf Ds As Bs) Dss inners));
   1.125 -    (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*)
   1.126 -    val rel = fold_rev Term.abs Qs'
   1.127 -      (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
   1.128 -        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o
   1.129 -          mk_rel_of_bnf Ds As Bs) Dss inners));
   1.130 -
   1.131 -    (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
   1.132 -    (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
   1.133 -    fun mk_set i =
   1.134 -      let
   1.135 -        val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i);
   1.136 -        val outer_set = mk_collect
   1.137 -          (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer)
   1.138 -          (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T);
   1.139 -        val inner_sets = map (fn sets => nth sets i) inner_setss;
   1.140 -        val outer_map = mk_map_of_bnf oDs CAs setTs outer;
   1.141 -        val map_inner_sets = Term.list_comb (outer_map, inner_sets);
   1.142 -        val collect_image = mk_collect
   1.143 -          (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets)
   1.144 -          (CCA --> HOLogic.mk_setT T);
   1.145 -      in
   1.146 -        (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets],
   1.147 -        HOLogic.mk_comp (mk_Union T, collect_image))
   1.148 -      end;
   1.149 -
   1.150 -    val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1);
   1.151 -
   1.152 -    (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
   1.153 -    val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
   1.154 -
   1.155 -    fun map_id0_tac _ =
   1.156 -      mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
   1.157 -        (map map_id0_of_bnf inners);
   1.158 -
   1.159 -    fun map_comp0_tac _ =
   1.160 -      mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
   1.161 -        (map map_comp0_of_bnf inners);
   1.162 -
   1.163 -    fun mk_single_set_map0_tac i _ =
   1.164 -      mk_comp_set_map0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
   1.165 -        (collect_set_map_of_bnf outer)
   1.166 -        (map ((fn thms => nth thms i) o set_map0_of_bnf) inners);
   1.167 -
   1.168 -    val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1);
   1.169 -
   1.170 -    fun bd_card_order_tac _ =
   1.171 -      mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
   1.172 -
   1.173 -    fun bd_cinfinite_tac _ =
   1.174 -      mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
   1.175 -
   1.176 -    val set_alt_thms =
   1.177 -      if Config.get lthy quick_and_dirty then
   1.178 -        []
   1.179 -      else
   1.180 -        map (fn goal =>
   1.181 -          Goal.prove_sorry lthy [] [] goal
   1.182 -            (fn {context = ctxt, prems = _} =>
   1.183 -              mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
   1.184 -          |> Thm.close_derivation)
   1.185 -        (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
   1.186 -
   1.187 -    fun map_cong0_tac _ =
   1.188 -      mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
   1.189 -
   1.190 -    val set_bd_tacs =
   1.191 -      if Config.get lthy quick_and_dirty then
   1.192 -        replicate ilive (K all_tac)
   1.193 -      else
   1.194 -        let
   1.195 -          val outer_set_bds = set_bd_of_bnf outer;
   1.196 -          val inner_set_bdss = map set_bd_of_bnf inners;
   1.197 -          val inner_bd_Card_orders = map bd_Card_order_of_bnf inners;
   1.198 -          fun single_set_bd_thm i j =
   1.199 -            @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i,
   1.200 -              nth outer_set_bds j]
   1.201 -          val single_set_bd_thmss =
   1.202 -            map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
   1.203 -        in
   1.204 -          map2 (fn set_alt => fn single_set_bds => fn {context = ctxt, prems = _} =>
   1.205 -            mk_comp_set_bd_tac ctxt set_alt single_set_bds)
   1.206 -          set_alt_thms single_set_bd_thmss
   1.207 -        end;
   1.208 -
   1.209 -    val in_alt_thm =
   1.210 -      let
   1.211 -        val inx = mk_in Asets sets CCA;
   1.212 -        val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
   1.213 -        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   1.214 -      in
   1.215 -        Goal.prove_sorry lthy [] [] goal
   1.216 -          (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
   1.217 -        |> Thm.close_derivation
   1.218 -      end;
   1.219 -
   1.220 -    fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
   1.221 -      (map le_rel_OO_of_bnf inners);
   1.222 -
   1.223 -    fun rel_OO_Grp_tac _ =
   1.224 -      let
   1.225 -        val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
   1.226 -        val outer_rel_cong = rel_cong_of_bnf outer;
   1.227 -        val thm =
   1.228 -          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
   1.229 -             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
   1.230 -               [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
   1.231 -                 rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
   1.232 -               trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
   1.233 -                 (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym)
   1.234 -          (*|> unfold_thms lthy (rel_def_of_bnf outer :: map rel_def_of_bnf inners)*);
   1.235 -      in
   1.236 -        rtac thm 1
   1.237 -      end;
   1.238 -
   1.239 -    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
   1.240 -      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
   1.241 -
   1.242 -    val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
   1.243 -
   1.244 -    val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
   1.245 -      (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
   1.246 -        Dss inwitss inners);
   1.247 -
   1.248 -    val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
   1.249 -
   1.250 -    val wits = (inner_witsss, (map (single o snd) outer_wits))
   1.251 -      |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit)))
   1.252 -      |> flat
   1.253 -      |> map (`(fn t => Term.add_frees t []))
   1.254 -      |> minimize_wits
   1.255 -      |> map (fn (frees, t) => fold absfree frees t);
   1.256 -
   1.257 -    fun wit_tac {context = ctxt, prems = _} =
   1.258 -      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
   1.259 -        (maps wit_thms_of_bnf inners);
   1.260 -
   1.261 -    val (bnf', lthy') =
   1.262 -      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
   1.263 -        Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
   1.264 -  in
   1.265 -    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   1.266 -  end;
   1.267 -
   1.268 -(* Killing live variables *)
   1.269 -
   1.270 -fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   1.271 -  let
   1.272 -    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
   1.273 -    val live = live_of_bnf bnf;
   1.274 -    val dead = dead_of_bnf bnf;
   1.275 -    val nwits = nwits_of_bnf bnf;
   1.276 -
   1.277 -    (* TODO: check 0 < n <= live *)
   1.278 -
   1.279 -    val (Ds, lthy1) = apfst (map TFree)
   1.280 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   1.281 -    val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
   1.282 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   1.283 -    val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
   1.284 -      (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
   1.285 -
   1.286 -    val ((Asets, lives), _(*names_lthy*)) = lthy
   1.287 -      |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
   1.288 -      ||>> mk_Frees "x" (drop n As);
   1.289 -    val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
   1.290 -
   1.291 -    val T = mk_T_of_bnf Ds As bnf;
   1.292 -
   1.293 -    (*bnf.map id ... id*)
   1.294 -    val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
   1.295 -    (*bnf.rel (op =) ... (op =)*)
   1.296 -    val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs);
   1.297 -
   1.298 -    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   1.299 -    val sets = drop n bnf_sets;
   1.300 -
   1.301 -    (*(|UNIV :: A1 set| +c ... +c |UNIV :: An set|) *c bnf.bd*)
   1.302 -    val bnf_bd = mk_bd_of_bnf Ds As bnf;
   1.303 -    val bd = mk_cprod
   1.304 -      (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
   1.305 -
   1.306 -    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
   1.307 -    fun map_comp0_tac {context = ctxt, prems = _} =
   1.308 -      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   1.309 -      rtac refl 1;
   1.310 -    fun map_cong0_tac {context = ctxt, prems = _} =
   1.311 -      mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
   1.312 -    val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
   1.313 -    fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
   1.314 -    fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
   1.315 -    val set_bd_tacs =
   1.316 -      map (fn thm => fn _ => mk_kill_set_bd_tac (bd_Card_order_of_bnf bnf) thm)
   1.317 -        (drop n (set_bd_of_bnf bnf));
   1.318 -
   1.319 -    val in_alt_thm =
   1.320 -      let
   1.321 -        val inx = mk_in Asets sets T;
   1.322 -        val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
   1.323 -        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   1.324 -      in
   1.325 -        Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
   1.326 -      end;
   1.327 -
   1.328 -    fun le_rel_OO_tac {context = ctxt, prems = _} =
   1.329 -      EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
   1.330 -      unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
   1.331 -
   1.332 -    fun rel_OO_Grp_tac _ =
   1.333 -      let
   1.334 -        val rel_Grp = rel_Grp_of_bnf bnf RS sym
   1.335 -        val thm =
   1.336 -          (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
   1.337 -            trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
   1.338 -              [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
   1.339 -                rel_conversep_of_bnf bnf RS sym], rel_Grp],
   1.340 -              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
   1.341 -                (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
   1.342 -                 replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
   1.343 -      in
   1.344 -        rtac thm 1
   1.345 -      end;
   1.346 -
   1.347 -    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
   1.348 -      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
   1.349 -
   1.350 -    val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
   1.351 -
   1.352 -    val wits = map (fn t => fold absfree (Term.add_frees t []) t)
   1.353 -      (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits);
   1.354 -
   1.355 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   1.356 -
   1.357 -    val (bnf', lthy') =
   1.358 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
   1.359 -        Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   1.360 -  in
   1.361 -    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   1.362 -  end;
   1.363 -
   1.364 -(* Adding dummy live variables *)
   1.365 -
   1.366 -fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   1.367 -  let
   1.368 -    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
   1.369 -    val live = live_of_bnf bnf;
   1.370 -    val dead = dead_of_bnf bnf;
   1.371 -    val nwits = nwits_of_bnf bnf;
   1.372 -
   1.373 -    (* TODO: check 0 < n *)
   1.374 -
   1.375 -    val (Ds, lthy1) = apfst (map TFree)
   1.376 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   1.377 -    val ((newAs, As), lthy2) = apfst (chop n o map TFree)
   1.378 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
   1.379 -    val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
   1.380 -      (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
   1.381 -
   1.382 -    val (Asets, _(*names_lthy*)) = lthy
   1.383 -      |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
   1.384 -
   1.385 -    val T = mk_T_of_bnf Ds As bnf;
   1.386 -
   1.387 -    (*%f1 ... fn. bnf.map*)
   1.388 -    val mapx =
   1.389 -      fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
   1.390 -    (*%Q1 ... Qn. bnf.rel*)
   1.391 -    val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
   1.392 -
   1.393 -    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   1.394 -    val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
   1.395 -
   1.396 -    val bd = mk_bd_of_bnf Ds As bnf;
   1.397 -
   1.398 -    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
   1.399 -    fun map_comp0_tac {context = ctxt, prems = _} =
   1.400 -      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
   1.401 -      rtac refl 1;
   1.402 -    fun map_cong0_tac {context = ctxt, prems = _} =
   1.403 -      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
   1.404 -    val set_map0_tacs =
   1.405 -      if Config.get lthy quick_and_dirty then
   1.406 -        replicate (n + live) (K all_tac)
   1.407 -      else
   1.408 -        replicate n (K empty_natural_tac) @
   1.409 -        map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf);
   1.410 -    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   1.411 -    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   1.412 -    val set_bd_tacs =
   1.413 -      if Config.get lthy quick_and_dirty then
   1.414 -        replicate (n + live) (K all_tac)
   1.415 -      else
   1.416 -        replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
   1.417 -        (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   1.418 -
   1.419 -    val in_alt_thm =
   1.420 -      let
   1.421 -        val inx = mk_in Asets sets T;
   1.422 -        val in_alt = mk_in (drop n Asets) bnf_sets T;
   1.423 -        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   1.424 -      in
   1.425 -        Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
   1.426 -      end;
   1.427 -
   1.428 -    fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
   1.429 -
   1.430 -    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
   1.431 -
   1.432 -    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
   1.433 -      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
   1.434 -
   1.435 -    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   1.436 -
   1.437 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   1.438 -
   1.439 -    val (bnf', lthy') =
   1.440 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
   1.441 -        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   1.442 -  in
   1.443 -    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   1.444 -  end;
   1.445 -
   1.446 -(* Changing the order of live variables *)
   1.447 -
   1.448 -fun permute_bnf qualify src dest bnf (unfold_set, lthy) =
   1.449 -  if src = dest then (bnf, (unfold_set, lthy)) else
   1.450 -  let
   1.451 -    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
   1.452 -    val live = live_of_bnf bnf;
   1.453 -    val dead = dead_of_bnf bnf;
   1.454 -    val nwits = nwits_of_bnf bnf;
   1.455 -    fun permute xs = permute_like (op =) src dest xs;
   1.456 -    fun unpermute xs = permute_like (op =) dest src xs;
   1.457 -
   1.458 -    val (Ds, lthy1) = apfst (map TFree)
   1.459 -      (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
   1.460 -    val (As, lthy2) = apfst (map TFree)
   1.461 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   1.462 -    val (Bs, _(*lthy3*)) = apfst (map TFree)
   1.463 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
   1.464 -
   1.465 -    val (Asets, _(*names_lthy*)) = lthy
   1.466 -      |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
   1.467 -
   1.468 -    val T = mk_T_of_bnf Ds As bnf;
   1.469 -
   1.470 -    (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
   1.471 -    val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
   1.472 -      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
   1.473 -    (*%Q(1) ... Q(n). bnf.rel Q\<sigma>(1) ... Q\<sigma>(n)*)
   1.474 -    val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs))
   1.475 -      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0))));
   1.476 -
   1.477 -    val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
   1.478 -    val sets = permute bnf_sets;
   1.479 -
   1.480 -    val bd = mk_bd_of_bnf Ds As bnf;
   1.481 -
   1.482 -    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
   1.483 -    fun map_comp0_tac _ = rtac (map_comp0_of_bnf bnf) 1;
   1.484 -    fun map_cong0_tac {context = ctxt, prems = _} =
   1.485 -      rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
   1.486 -    val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_of_bnf bnf));
   1.487 -    fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
   1.488 -    fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
   1.489 -    val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
   1.490 -
   1.491 -    val in_alt_thm =
   1.492 -      let
   1.493 -        val inx = mk_in Asets sets T;
   1.494 -        val in_alt = mk_in (unpermute Asets) bnf_sets T;
   1.495 -        val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
   1.496 -      in
   1.497 -        Goal.prove_sorry lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
   1.498 -        |> Thm.close_derivation
   1.499 -      end;
   1.500 -
   1.501 -    fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
   1.502 -
   1.503 -    fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
   1.504 -
   1.505 -    val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
   1.506 -      bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
   1.507 -
   1.508 -    val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   1.509 -
   1.510 -    fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
   1.511 -
   1.512 -    val (bnf', lthy') =
   1.513 -      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
   1.514 -        [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   1.515 -  in
   1.516 -    (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   1.517 -  end;
   1.518 -
   1.519 -(* Composition pipeline *)
   1.520 -
   1.521 -fun permute_and_kill qualify n src dest bnf =
   1.522 -  bnf
   1.523 -  |> permute_bnf qualify src dest
   1.524 -  #> uncurry (kill_bnf qualify n);
   1.525 -
   1.526 -fun lift_and_permute qualify n src dest bnf =
   1.527 -  bnf
   1.528 -  |> lift_bnf qualify n
   1.529 -  #> uncurry (permute_bnf qualify src dest);
   1.530 -
   1.531 -fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy =
   1.532 -  let
   1.533 -    val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
   1.534 -    val kill_poss = map (find_indices op = Ds) Ass;
   1.535 -    val live_poss = map2 (subtract op =) kill_poss before_kill_src;
   1.536 -    val before_kill_dest = map2 append kill_poss live_poss;
   1.537 -    val kill_ns = map length kill_poss;
   1.538 -    val (inners', (unfold_set', lthy')) =
   1.539 -      fold_map5 (fn i => permute_and_kill (qualify i))
   1.540 -        (if length bnfs = 1 then [0] else (1 upto length bnfs))
   1.541 -        kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy);
   1.542 -
   1.543 -    val Ass' = map2 (map o nth) Ass live_poss;
   1.544 -    val As = sort Ass';
   1.545 -    val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
   1.546 -    val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
   1.547 -    val new_poss = map2 (subtract op =) old_poss after_lift_dest;
   1.548 -    val after_lift_src = map2 append new_poss old_poss;
   1.549 -    val lift_ns = map (fn xs => length As - length xs) Ass';
   1.550 -  in
   1.551 -    ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
   1.552 -      (if length bnfs = 1 then [0] else (1 upto length bnfs))
   1.553 -      lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy'))
   1.554 -  end;
   1.555 -
   1.556 -fun default_comp_sort Ass =
   1.557 -  Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
   1.558 -
   1.559 -fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) =
   1.560 -  let
   1.561 -    val b = name_of_bnf outer;
   1.562 -
   1.563 -    val Ass = map (map Term.dest_TFree) tfreess;
   1.564 -    val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
   1.565 -
   1.566 -    val ((kill_poss, As), (inners', (unfold_set', lthy'))) =
   1.567 -      normalize_bnfs qualify Ass Ds sort inners unfold_set lthy;
   1.568 -
   1.569 -    val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
   1.570 -    val As = map TFree As;
   1.571 -  in
   1.572 -    apfst (rpair (Ds, As))
   1.573 -      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))
   1.574 -  end;
   1.575 -
   1.576 -(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
   1.577 -
   1.578 -fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
   1.579 -  let
   1.580 -    val live = live_of_bnf bnf;
   1.581 -    val nwits = nwits_of_bnf bnf;
   1.582 -
   1.583 -    val (As, lthy1) = apfst (map TFree)
   1.584 -      (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
   1.585 -    val (Bs, _) = apfst (map TFree)
   1.586 -      (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
   1.587 -
   1.588 -    val map_unfolds = #map_unfolds unfold_set;
   1.589 -    val set_unfoldss = #set_unfoldss unfold_set;
   1.590 -    val rel_unfolds = #rel_unfolds unfold_set;
   1.591 -
   1.592 -    val expand_maps =
   1.593 -      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
   1.594 -    val expand_sets =
   1.595 -      fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
   1.596 -    val expand_rels =
   1.597 -      fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
   1.598 -    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
   1.599 -    fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
   1.600 -    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
   1.601 -    fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
   1.602 -    val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
   1.603 -    val bnf_sets = map (expand_maps o expand_sets)
   1.604 -      (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
   1.605 -    val bnf_bd = mk_bd_of_bnf Ds As bnf;
   1.606 -    val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
   1.607 -    val T = mk_T_of_bnf Ds As bnf;
   1.608 -
   1.609 -    (*bd should only depend on dead type variables!*)
   1.610 -    val bd_repT = fst (dest_relT (fastype_of bnf_bd));
   1.611 -    val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
   1.612 -    val params = fold Term.add_tfreesT Ds [];
   1.613 -    val deads = map TFree params;
   1.614 -
   1.615 -    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
   1.616 -      typedef (bdT_bind, params, NoSyn)
   1.617 -        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   1.618 -
   1.619 -    val bnf_bd' = mk_dir_image bnf_bd
   1.620 -      (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
   1.621 -
   1.622 -    val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
   1.623 -    val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
   1.624 -
   1.625 -    val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
   1.626 -    val bd_card_order =
   1.627 -      @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf];
   1.628 -    val bd_cinfinite =
   1.629 -      (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
   1.630 -
   1.631 -    val set_bds =
   1.632 -      map (fn thm => @{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso]) (set_bd_of_bnf bnf);
   1.633 -
   1.634 -    fun mk_tac thm {context = ctxt, prems = _} =
   1.635 -      (rtac (unfold_all ctxt thm) THEN'
   1.636 -      SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   1.637 -
   1.638 -    val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
   1.639 -      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_of_bnf bnf))
   1.640 -      (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
   1.641 -      (mk_tac (le_rel_OO_of_bnf bnf))
   1.642 -      (mk_tac (rel_OO_Grp_of_bnf bnf));
   1.643 -
   1.644 -    val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   1.645 -
   1.646 -    fun wit_tac {context = ctxt, prems = _} =
   1.647 -      mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
   1.648 -
   1.649 -    val (bnf', lthy') =
   1.650 -      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
   1.651 -        Binding.empty Binding.empty []
   1.652 -        ((((((b, T), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   1.653 -  in
   1.654 -    ((bnf', deads), lthy')
   1.655 -  end;
   1.656 -
   1.657 -exception BAD_DEAD of typ * typ;
   1.658 -
   1.659 -fun bnf_of_typ _ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
   1.660 -  | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
   1.661 -  | bnf_of_typ const_policy qualify' sort Xs (T as Type (C, Ts)) (unfold_set, lthy) =
   1.662 -    let
   1.663 -      fun check_bad_dead ((_, (deads, _)), _) =
   1.664 -        let val Ds = fold Term.add_tfreesT deads [] in
   1.665 -          (case Library.inter (op =) Ds Xs of [] => ()
   1.666 -           | X :: _ => raise BAD_DEAD (TFree X, T))
   1.667 -        end;
   1.668 -
   1.669 -      val tfrees = Term.add_tfreesT T [];
   1.670 -      val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
   1.671 -    in
   1.672 -      (case bnf_opt of
   1.673 -        NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy))
   1.674 -      | SOME bnf =>
   1.675 -        if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
   1.676 -          let
   1.677 -            val T' = T_of_bnf bnf;
   1.678 -            val deads = deads_of_bnf bnf;
   1.679 -            val lives = lives_of_bnf bnf;
   1.680 -            val tvars' = Term.add_tvarsT T' [];
   1.681 -            val deads_lives =
   1.682 -              pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
   1.683 -                (deads, lives);
   1.684 -          in ((bnf, deads_lives), (unfold_set, lthy)) end
   1.685 -        else
   1.686 -          let
   1.687 -            val name = Long_Name.base_name C;
   1.688 -            fun qualify i =
   1.689 -              let val namei = name ^ nonzero_string_of_int i;
   1.690 -              in qualify' o Binding.qualify true namei end;
   1.691 -            val odead = dead_of_bnf bnf;
   1.692 -            val olive = live_of_bnf bnf;
   1.693 -            val oDs_pos = find_indices op = [TFree ("dead", [])] (snd (Term.dest_Type
   1.694 -              (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
   1.695 -            val oDs = map (nth Ts) oDs_pos;
   1.696 -            val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
   1.697 -            val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
   1.698 -              apfst (apsnd split_list o split_list)
   1.699 -                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs)
   1.700 -                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
   1.701 -          in
   1.702 -            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
   1.703 -          end)
   1.704 -      |> tap check_bad_dead
   1.705 -    end;
   1.706 -
   1.707 -end;