src/HOL/BNF/Tools/bnf_def.ML
author blanchet
Fri Jun 07 09:30:13 2013 +0200 (2013-06-07)
changeset 52334 705bc4f5fc70
parent 51930 52fd62618631
child 52635 4f84b730c489
permissions -rw-r--r--
tuning
     1 (*  Title:      HOL/BNF/Tools/bnf_def.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     5 
     6 Definition of bounded natural functors.
     7 *)
     8 
     9 signature BNF_DEF =
    10 sig
    11   type bnf
    12   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
    13 
    14   val morph_bnf: morphism -> bnf -> bnf
    15   val eq_bnf: bnf * bnf -> bool
    16   val bnf_of: Proof.context -> string -> bnf option
    17   val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
    18 
    19   val name_of_bnf: bnf -> binding
    20   val T_of_bnf: bnf -> typ
    21   val live_of_bnf: bnf -> int
    22   val lives_of_bnf: bnf -> typ list
    23   val dead_of_bnf: bnf -> int
    24   val deads_of_bnf: bnf -> typ list
    25   val nwits_of_bnf: bnf -> int
    26 
    27   val mapN: string
    28   val relN: string
    29   val setN: string
    30   val mk_setN: int -> string
    31 
    32   val map_of_bnf: bnf -> term
    33   val sets_of_bnf: bnf -> term list
    34   val rel_of_bnf: bnf -> term
    35 
    36   val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
    37   val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
    38   val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    39   val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    40   val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
    41   val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
    42 
    43   val bd_Card_order_of_bnf: bnf -> thm
    44   val bd_Cinfinite_of_bnf: bnf -> thm
    45   val bd_Cnotzero_of_bnf: bnf -> thm
    46   val bd_card_order_of_bnf: bnf -> thm
    47   val bd_cinfinite_of_bnf: bnf -> thm
    48   val collect_set_map_of_bnf: bnf -> thm
    49   val in_bd_of_bnf: bnf -> thm
    50   val in_cong_of_bnf: bnf -> thm
    51   val in_mono_of_bnf: bnf -> thm
    52   val in_rel_of_bnf: bnf -> thm
    53   val map_comp'_of_bnf: bnf -> thm
    54   val map_comp_of_bnf: bnf -> thm
    55   val map_cong0_of_bnf: bnf -> thm
    56   val map_cong_of_bnf: bnf -> thm
    57   val map_def_of_bnf: bnf -> thm
    58   val map_id'_of_bnf: bnf -> thm
    59   val map_id_of_bnf: bnf -> thm
    60   val map_wppull_of_bnf: bnf -> thm
    61   val map_wpull_of_bnf: bnf -> thm
    62   val rel_def_of_bnf: bnf -> thm
    63   val rel_Grp_of_bnf: bnf -> thm
    64   val rel_OO_of_bnf: bnf -> thm
    65   val rel_OO_Grp_of_bnf: bnf -> thm
    66   val rel_cong_of_bnf: bnf -> thm
    67   val rel_conversep_of_bnf: bnf -> thm
    68   val rel_mono_of_bnf: bnf -> thm
    69   val rel_mono_strong_of_bnf: bnf -> thm
    70   val rel_eq_of_bnf: bnf -> thm
    71   val rel_flip_of_bnf: bnf -> thm
    72   val set_bd_of_bnf: bnf -> thm list
    73   val set_defs_of_bnf: bnf -> thm list
    74   val set_map'_of_bnf: bnf -> thm list
    75   val set_map_of_bnf: bnf -> thm list
    76   val wit_thms_of_bnf: bnf -> thm list
    77   val wit_thmss_of_bnf: bnf -> thm list list
    78 
    79   val mk_witness: int list * term -> thm list -> nonemptiness_witness
    80   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
    81   val wits_of_bnf: bnf -> nonemptiness_witness list
    82 
    83   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
    84 
    85   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
    86   datatype fact_policy = Dont_Note | Note_Some | Note_All
    87 
    88   val bnf_note_all: bool Config.T
    89   val user_policy: fact_policy -> Proof.context -> fact_policy
    90 
    91   val print_bnfs: Proof.context -> unit
    92   val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
    93     ({prems: thm list, context: Proof.context} -> tactic) list ->
    94     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
    95     binding -> binding list ->
    96     ((((binding * term) * term list) * term) * term list) * term option ->
    97     local_theory -> bnf * local_theory
    98 end;
    99 
   100 structure BNF_Def : BNF_DEF =
   101 struct
   102 
   103 open BNF_Util
   104 open BNF_Tactics
   105 open BNF_Def_Tactics
   106 
   107 val fundef_cong_attrs = @{attributes [fundef_cong]};
   108 
   109 type axioms = {
   110   map_id: thm,
   111   map_comp: thm,
   112   map_cong0: thm,
   113   set_map: thm list,
   114   bd_card_order: thm,
   115   bd_cinfinite: thm,
   116   set_bd: thm list,
   117   in_bd: thm,
   118   map_wpull: thm,
   119   rel_OO_Grp: thm
   120 };
   121 
   122 fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), rel) =
   123   {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
   124    bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, rel_OO_Grp = rel};
   125 
   126 fun dest_cons [] = raise List.Empty
   127   | dest_cons (x :: xs) = (x, xs);
   128 
   129 fun mk_axioms n thms = thms
   130   |> map the_single
   131   |> dest_cons
   132   ||>> dest_cons
   133   ||>> dest_cons
   134   ||>> chop n
   135   ||>> dest_cons
   136   ||>> dest_cons
   137   ||>> chop n
   138   ||>> dest_cons
   139   ||>> dest_cons
   140   ||> the_single
   141   |> mk_axioms';
   142 
   143 fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
   144   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
   145 
   146 fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd,
   147   map_wpull, rel_OO_Grp} =
   148   zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull
   149     rel_OO_Grp;
   150 
   151 fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
   152   in_bd, map_wpull, rel_OO_Grp} =
   153   {map_id = f map_id,
   154     map_comp = f map_comp,
   155     map_cong0 = f map_cong0,
   156     set_map = map f set_map,
   157     bd_card_order = f bd_card_order,
   158     bd_cinfinite = f bd_cinfinite,
   159     set_bd = map f set_bd,
   160     in_bd = f in_bd,
   161     map_wpull = f map_wpull,
   162     rel_OO_Grp = f rel_OO_Grp};
   163 
   164 val morph_axioms = map_axioms o Morphism.thm;
   165 
   166 type defs = {
   167   map_def: thm,
   168   set_defs: thm list,
   169   rel_def: thm
   170 }
   171 
   172 fun mk_defs map sets rel = {map_def = map, set_defs = sets, rel_def = rel};
   173 
   174 fun map_defs f {map_def, set_defs, rel_def} =
   175   {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def};
   176 
   177 val morph_defs = map_defs o Morphism.thm;
   178 
   179 type facts = {
   180   bd_Card_order: thm,
   181   bd_Cinfinite: thm,
   182   bd_Cnotzero: thm,
   183   collect_set_map: thm lazy,
   184   in_cong: thm lazy,
   185   in_mono: thm lazy,
   186   in_rel: thm lazy,
   187   map_comp': thm lazy,
   188   map_cong: thm lazy,
   189   map_id': thm lazy,
   190   map_wppull: thm lazy,
   191   rel_eq: thm lazy,
   192   rel_flip: thm lazy,
   193   set_map': thm lazy list,
   194   rel_cong: thm lazy,
   195   rel_mono: thm lazy,
   196   rel_mono_strong: thm lazy,
   197   rel_Grp: thm lazy,
   198   rel_conversep: thm lazy,
   199   rel_OO: thm lazy
   200 };
   201 
   202 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_rel
   203     map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono rel_mono_strong
   204     rel_Grp rel_conversep rel_OO = {
   205   bd_Card_order = bd_Card_order,
   206   bd_Cinfinite = bd_Cinfinite,
   207   bd_Cnotzero = bd_Cnotzero,
   208   collect_set_map = collect_set_map,
   209   in_cong = in_cong,
   210   in_mono = in_mono,
   211   in_rel = in_rel,
   212   map_comp' = map_comp',
   213   map_cong = map_cong,
   214   map_id' = map_id',
   215   map_wppull = map_wppull,
   216   rel_eq = rel_eq,
   217   rel_flip = rel_flip,
   218   set_map' = set_map',
   219   rel_cong = rel_cong,
   220   rel_mono = rel_mono,
   221   rel_mono_strong = rel_mono_strong,
   222   rel_Grp = rel_Grp,
   223   rel_conversep = rel_conversep,
   224   rel_OO = rel_OO};
   225 
   226 fun map_facts f {
   227   bd_Card_order,
   228   bd_Cinfinite,
   229   bd_Cnotzero,
   230   collect_set_map,
   231   in_cong,
   232   in_mono,
   233   in_rel,
   234   map_comp',
   235   map_cong,
   236   map_id',
   237   map_wppull,
   238   rel_eq,
   239   rel_flip,
   240   set_map',
   241   rel_cong,
   242   rel_mono,
   243   rel_mono_strong,
   244   rel_Grp,
   245   rel_conversep,
   246   rel_OO} =
   247   {bd_Card_order = f bd_Card_order,
   248     bd_Cinfinite = f bd_Cinfinite,
   249     bd_Cnotzero = f bd_Cnotzero,
   250     collect_set_map = Lazy.map f collect_set_map,
   251     in_cong = Lazy.map f in_cong,
   252     in_mono = Lazy.map f in_mono,
   253     in_rel = Lazy.map f in_rel,
   254     map_comp' = Lazy.map f map_comp',
   255     map_cong = Lazy.map f map_cong,
   256     map_id' = Lazy.map f map_id',
   257     map_wppull = Lazy.map f map_wppull,
   258     rel_eq = Lazy.map f rel_eq,
   259     rel_flip = Lazy.map f rel_flip,
   260     set_map' = map (Lazy.map f) set_map',
   261     rel_cong = Lazy.map f rel_cong,
   262     rel_mono = Lazy.map f rel_mono,
   263     rel_mono_strong = Lazy.map f rel_mono_strong,
   264     rel_Grp = Lazy.map f rel_Grp,
   265     rel_conversep = Lazy.map f rel_conversep,
   266     rel_OO = Lazy.map f rel_OO};
   267 
   268 val morph_facts = map_facts o Morphism.thm;
   269 
   270 type nonemptiness_witness = {
   271   I: int list,
   272   wit: term,
   273   prop: thm list
   274 };
   275 
   276 fun mk_witness (I, wit) prop = {I = I, wit = wit, prop = prop};
   277 fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
   278 fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
   279 
   280 datatype bnf = BNF of {
   281   name: binding,
   282   T: typ,
   283   live: int,
   284   lives: typ list, (*source type variables of map, only for composition*)
   285   lives': typ list, (*target type variables of map, only for composition*)
   286   dead: int,
   287   deads: typ list, (*only for composition*)
   288   map: term,
   289   sets: term list,
   290   bd: term,
   291   axioms: axioms,
   292   defs: defs,
   293   facts: facts,
   294   nwits: int,
   295   wits: nonemptiness_witness list,
   296   rel: term
   297 };
   298 
   299 (* getters *)
   300 
   301 fun rep_bnf (BNF bnf) = bnf;
   302 val name_of_bnf = #name o rep_bnf;
   303 val T_of_bnf = #T o rep_bnf;
   304 fun mk_T_of_bnf Ds Ts bnf =
   305   let val bnf_rep = rep_bnf bnf
   306   in Term.typ_subst_atomic ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#T bnf_rep) end;
   307 val live_of_bnf = #live o rep_bnf;
   308 val lives_of_bnf = #lives o rep_bnf;
   309 val dead_of_bnf = #dead o rep_bnf;
   310 val deads_of_bnf = #deads o rep_bnf;
   311 val axioms_of_bnf = #axioms o rep_bnf;
   312 val facts_of_bnf = #facts o rep_bnf;
   313 val nwits_of_bnf = #nwits o rep_bnf;
   314 val wits_of_bnf = #wits o rep_bnf;
   315 
   316 (*terms*)
   317 val map_of_bnf = #map o rep_bnf;
   318 val sets_of_bnf = #sets o rep_bnf;
   319 fun mk_map_of_bnf Ds Ts Us bnf =
   320   let val bnf_rep = rep_bnf bnf;
   321   in
   322     Term.subst_atomic_types
   323       ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#map bnf_rep)
   324   end;
   325 fun mk_sets_of_bnf Dss Tss bnf =
   326   let val bnf_rep = rep_bnf bnf;
   327   in
   328     map2 (fn (Ds, Ts) => Term.subst_atomic_types
   329       ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts))) (Dss ~~ Tss) (#sets bnf_rep)
   330   end;
   331 val bd_of_bnf = #bd o rep_bnf;
   332 fun mk_bd_of_bnf Ds Ts bnf =
   333   let val bnf_rep = rep_bnf bnf;
   334   in Term.subst_atomic_types ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)) (#bd bnf_rep) end;
   335 fun mk_wits_of_bnf Dss Tss bnf =
   336   let
   337     val bnf_rep = rep_bnf bnf;
   338     val wits = map (fn x => (#I x, #wit x)) (#wits bnf_rep);
   339   in
   340     map2 (fn (Ds, Ts) => apsnd (Term.subst_atomic_types
   341       ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts)))) (Dss ~~ Tss) wits
   342   end;
   343 val rel_of_bnf = #rel o rep_bnf;
   344 fun mk_rel_of_bnf Ds Ts Us bnf =
   345   let val bnf_rep = rep_bnf bnf;
   346   in
   347     Term.subst_atomic_types
   348       ((#deads bnf_rep ~~ Ds) @ (#lives bnf_rep ~~ Ts) @ (#lives' bnf_rep ~~ Us)) (#rel bnf_rep)
   349   end;
   350 
   351 (*thms*)
   352 val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
   353 val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
   354 val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf;
   355 val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
   356 val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
   357 val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
   358 val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
   359 val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
   360 val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
   361 val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
   362 val map_def_of_bnf = #map_def o #defs o rep_bnf;
   363 val map_id_of_bnf = #map_id o #axioms o rep_bnf;
   364 val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
   365 val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
   366 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
   367 val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
   368 val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
   369 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
   370 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
   371 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
   372 val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
   373 val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
   374 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
   375 val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
   376 val set_map_of_bnf = #set_map o #axioms o rep_bnf;
   377 val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
   378 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
   379 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
   380 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
   381 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
   382 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
   383 val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
   384 val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
   385 val wit_thms_of_bnf = maps #prop o wits_of_bnf;
   386 val wit_thmss_of_bnf = map #prop o wits_of_bnf;
   387 
   388 fun mk_bnf name T live lives lives' dead deads map sets bd axioms defs facts wits rel =
   389   BNF {name = name, T = T,
   390        live = live, lives = lives, lives' = lives', dead = dead, deads = deads,
   391        map = map, sets = sets, bd = bd,
   392        axioms = axioms, defs = defs, facts = facts,
   393        nwits = length wits, wits = wits, rel = rel};
   394 
   395 fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives',
   396   dead = dead, deads = deads, map = map, sets = sets, bd = bd,
   397   axioms = axioms, defs = defs, facts = facts,
   398   nwits = nwits, wits = wits, rel = rel}) =
   399   BNF {name = Morphism.binding phi name, T = Morphism.typ phi T,
   400     live = live, lives = List.map (Morphism.typ phi) lives,
   401     lives' = List.map (Morphism.typ phi) lives',
   402     dead = dead, deads = List.map (Morphism.typ phi) deads,
   403     map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets,
   404     bd = Morphism.term phi bd,
   405     axioms = morph_axioms phi axioms,
   406     defs = morph_defs phi defs,
   407     facts = morph_facts phi facts,
   408     nwits = nwits,
   409     wits = List.map (morph_witness phi) wits,
   410     rel = Morphism.term phi rel};
   411 
   412 fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
   413   BNF {T = T2, live = live2, dead = dead2, ...}) =
   414   Type.could_unify (T1, T2) andalso live1 = live2 andalso dead1 = dead2;
   415 
   416 structure Data = Generic_Data
   417 (
   418   type T = bnf Symtab.table;
   419   val empty = Symtab.empty;
   420   val extend = I;
   421   val merge = Symtab.merge eq_bnf;
   422 );
   423 
   424 val bnf_of = Symtab.lookup o Data.get o Context.Proof;
   425 
   426 
   427 
   428 (* Utilities *)
   429 
   430 fun normalize_set insts instA set =
   431   let
   432     val (T, T') = dest_funT (fastype_of set);
   433     val A = fst (Term.dest_TVar (HOLogic.dest_setT T'));
   434     val params = Term.add_tvar_namesT T [];
   435   in Term.subst_TVars ((A :: params) ~~ (instA :: insts)) set end;
   436 
   437 fun normalize_rel ctxt instTs instA instB rel =
   438   let
   439     val thy = Proof_Context.theory_of ctxt;
   440     val tyenv =
   441       Sign.typ_match thy (fastype_of rel, Library.foldr (op -->) (instTs, mk_pred2T instA instB))
   442         Vartab.empty;
   443   in Envir.subst_term (tyenv, Vartab.empty) rel end
   444   handle Type.TYPE_MATCH => error "Bad relator";
   445 
   446 fun normalize_wit insts CA As wit =
   447   let
   448     fun strip_param (Ts, T as Type (@{type_name fun}, [T1, T2])) =
   449         if Type.raw_instance (CA, T) then (Ts, T) else strip_param (T1 :: Ts, T2)
   450       | strip_param x = x;
   451     val (Ts, T) = strip_param ([], fastype_of wit);
   452     val subst = Term.add_tvar_namesT T [] ~~ insts;
   453     fun find y = find_index (fn x => x = y) As;
   454   in
   455     (map (find o Term.typ_subst_TVars subst) (rev Ts), Term.subst_TVars subst wit)
   456   end;
   457 
   458 fun minimize_wits wits =
   459  let
   460    fun minimize done [] = done
   461      | minimize done ((I, wit) :: todo) =
   462        if exists (fn (J, _) => subset (op =) (J, I)) (done @ todo)
   463        then minimize done todo
   464        else minimize ((I, wit) :: done) todo;
   465  in minimize [] wits end;
   466 
   467 
   468 
   469 (* Names *)
   470 
   471 val mapN = "map";
   472 val setN = "set";
   473 fun mk_setN i = setN ^ nonzero_string_of_int i;
   474 val bdN = "bd";
   475 val witN = "wit";
   476 fun mk_witN i = witN ^ nonzero_string_of_int i;
   477 val relN = "rel";
   478 
   479 val bd_card_orderN = "bd_card_order";
   480 val bd_cinfiniteN = "bd_cinfinite";
   481 val bd_Card_orderN = "bd_Card_order";
   482 val bd_CinfiniteN = "bd_Cinfinite";
   483 val bd_CnotzeroN = "bd_Cnotzero";
   484 val collect_set_mapN = "collect_set_map";
   485 val in_bdN = "in_bd";
   486 val in_monoN = "in_mono";
   487 val in_relN = "in_rel";
   488 val map_idN = "map_id";
   489 val map_id'N = "map_id'";
   490 val map_compN = "map_comp";
   491 val map_comp'N = "map_comp'";
   492 val map_cong0N = "map_cong0";
   493 val map_congN = "map_cong";
   494 val map_wpullN = "map_wpull";
   495 val rel_eqN = "rel_eq";
   496 val rel_flipN = "rel_flip";
   497 val set_mapN = "set_map";
   498 val set_map'N = "set_map'";
   499 val set_bdN = "set_bd";
   500 val rel_GrpN = "rel_Grp";
   501 val rel_conversepN = "rel_conversep";
   502 val rel_monoN = "rel_mono"
   503 val rel_mono_strongN = "rel_mono_strong"
   504 val rel_OON = "rel_compp";
   505 val rel_OO_GrpN = "rel_compp_Grp";
   506 
   507 datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
   508 
   509 datatype fact_policy = Dont_Note | Note_Some | Note_All;
   510 
   511 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
   512 
   513 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
   514 
   515 val smart_max_inline_size = 25; (*FUDGE*)
   516 
   517 
   518 (* Define new BNFs *)
   519 
   520 fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
   521   (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
   522   let
   523     val fact_policy = mk_fact_policy no_defs_lthy;
   524     val b = qualify raw_b;
   525     val live = length raw_sets;
   526     val nwits = length raw_wits;
   527 
   528     val map_rhs = prep_term no_defs_lthy raw_map;
   529     val set_rhss = map (prep_term no_defs_lthy) raw_sets;
   530     val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of
   531       Abs (_, T, t) => (T, t)
   532     | _ => error "Bad bound constant");
   533     val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
   534 
   535     fun err T =
   536       error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
   537         " as unnamed BNF");
   538 
   539     val (b, key) =
   540       if Binding.eq_name (b, Binding.empty) then
   541         (case bd_rhsT of
   542           Type (C, Ts) => if forall (is_some o try dest_TFree) Ts
   543             then (Binding.qualified_name C, C) else err bd_rhsT
   544         | T => err T)
   545       else (b, Local_Theory.full_name no_defs_lthy b);
   546 
   547     fun maybe_define user_specified (b, rhs) lthy =
   548       let
   549         val inline =
   550           (user_specified orelse fact_policy = Dont_Note) andalso
   551           (case const_policy of
   552             Dont_Inline => false
   553           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
   554           | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
   555           | Do_Inline => true)
   556       in
   557         if inline then
   558           ((rhs, Drule.reflexive_thm), lthy)
   559         else
   560           let val b = b () in
   561             apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs))
   562               lthy)
   563           end
   564       end;
   565 
   566     fun maybe_restore lthy_old lthy =
   567       lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;
   568 
   569     val map_bind_def =
   570       (fn () => if Binding.is_empty map_b then Binding.suffix_name ("_" ^ mapN) b else map_b,
   571        map_rhs);
   572     val set_binds_defs =
   573       let
   574         fun set_name i get_b =
   575           (case try (nth set_bs) (i - 1) of
   576             SOME b => if Binding.is_empty b then get_b else K b
   577           | NONE => get_b);
   578         val bs =
   579           if live = 1 then
   580             [set_name 1 (fn () => Binding.suffix_name ("_" ^ setN) b)]
   581           else
   582             map (fn i => set_name i (fn () => Binding.suffix_name ("_" ^ mk_setN i) b))
   583               (1 upto live);
   584       in bs ~~ set_rhss end;
   585     val bd_bind_def = (fn () => Binding.suffix_name ("_" ^ bdN) b, bd_rhs);
   586     val wit_binds_defs =
   587       let
   588         val bs = if nwits = 1 then [fn () => Binding.suffix_name ("_" ^ witN) b]
   589           else map (fn i => fn () => Binding.suffix_name ("_" ^ mk_witN i) b) (1 upto nwits);
   590       in bs ~~ wit_rhss end;
   591 
   592     val (((((bnf_map_term, raw_map_def),
   593       (bnf_set_terms, raw_set_defs)),
   594       (bnf_bd_term, raw_bd_def)),
   595       (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
   596         no_defs_lthy
   597         |> maybe_define true map_bind_def
   598         ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
   599         ||>> maybe_define true bd_bind_def
   600         ||>> apfst split_list o fold_map (maybe_define true) wit_binds_defs
   601         ||> `(maybe_restore no_defs_lthy);
   602 
   603     val phi = Proof_Context.export_morphism lthy_old lthy;
   604 
   605     val bnf_map_def = Morphism.thm phi raw_map_def;
   606     val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
   607     val bnf_bd_def = Morphism.thm phi raw_bd_def;
   608     val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
   609 
   610     val bnf_map = Morphism.term phi bnf_map_term;
   611 
   612     (*TODO: handle errors*)
   613     (*simple shape analysis of a map function*)
   614     val ((alphas, betas), (CA, _)) =
   615       fastype_of bnf_map
   616       |> strip_typeN live
   617       |>> map_split dest_funT
   618       ||> dest_funT
   619       handle TYPE _ => error "Bad map function";
   620 
   621     val CA_params = map TVar (Term.add_tvarsT CA []);
   622 
   623     val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms);
   624     val bdT = Morphism.typ phi bd_rhsT;
   625     val bnf_bd =
   626       Term.subst_TVars (Term.add_tvar_namesT bdT [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
   627     val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms;
   628 
   629     (*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
   630     val deads = (case Ds_opt of
   631       NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map []))
   632     | SOME Ds => map (Morphism.typ phi) Ds);
   633     val dead = length deads;
   634 
   635     (*TODO: further checks of type of bnf_map*)
   636     (*TODO: check types of bnf_sets*)
   637     (*TODO: check type of bnf_bd*)
   638     (*TODO: check type of bnf_rel*)
   639 
   640     val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
   641       (Ts, T)) = lthy
   642       |> mk_TFrees live
   643       ||>> mk_TFrees live
   644       ||>> mk_TFrees live
   645       ||>> mk_TFrees dead
   646       ||>> mk_TFrees live
   647       ||>> mk_TFrees live
   648       ||>> mk_TFrees live
   649       ||>> mk_TFrees live
   650       ||>> mk_TFrees live
   651       ||>> mk_TFrees live
   652       ||> fst o mk_TFrees 1
   653       ||> the_single
   654       ||> `(replicate live);
   655 
   656     fun mk_bnf_map As' Bs' =
   657       Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map;
   658     fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
   659     fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
   660 
   661     val RTs = map HOLogic.mk_prodT (As' ~~ Bs');
   662     val pred2RTs = map2 mk_pred2T As' Bs';
   663     val pred2RTsAsCs = map2 mk_pred2T As' Cs;
   664     val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
   665     val pred2RT's = map2 mk_pred2T Bs' As';
   666     val self_pred2RTs = map2 mk_pred2T As' As';
   667 
   668     val CA' = mk_bnf_T As' CA;
   669     val CB' = mk_bnf_T Bs' CA;
   670     val CC' = mk_bnf_T Cs CA;
   671     val CRs' = mk_bnf_T RTs CA;
   672 
   673     val bnf_map_AsAs = mk_bnf_map As' As';
   674     val bnf_map_AsBs = mk_bnf_map As' Bs';
   675     val bnf_map_AsCs = mk_bnf_map As' Cs;
   676     val bnf_map_BsCs = mk_bnf_map Bs' Cs;
   677     val bnf_sets_As = map (mk_bnf_t As') bnf_sets;
   678     val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
   679     val bnf_bd_As = mk_bnf_t As' bnf_bd;
   680     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
   681 
   682     val pre_names_lthy = lthy;
   683     val (((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
   684       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
   685       names_lthy) = pre_names_lthy
   686       |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
   687       ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
   688       ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
   689       ||>> yield_singleton (mk_Frees "x") CA'
   690       ||>> yield_singleton (mk_Frees "y") CB'
   691       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
   692       ||>> mk_Frees "z" As'
   693       ||>> mk_Frees "y" Bs'
   694       ||>> mk_Frees "A" (map HOLogic.mk_setT As')
   695       ||>> mk_Frees "A" (map HOLogic.mk_setT As')
   696       ||>> mk_Frees "A" (map HOLogic.mk_setT domTs)
   697       ||>> mk_Frees "B1" (map HOLogic.mk_setT B1Ts)
   698       ||>> mk_Frees "B2" (map HOLogic.mk_setT B2Ts)
   699       ||>> mk_Frees "f1" (map2 (curry (op -->)) B1Ts ranTs)
   700       ||>> mk_Frees "f2" (map2 (curry (op -->)) B2Ts ranTs)
   701       ||>> mk_Frees "e1" (map2 (curry (op -->)) B1Ts ranTs')
   702       ||>> mk_Frees "e2" (map2 (curry (op -->)) B2Ts ranTs'')
   703       ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
   704       ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
   705       ||>> mk_Frees "b" As'
   706       ||>> mk_Frees' "R" pred2RTs
   707       ||>> mk_Frees "R" pred2RTs
   708       ||>> mk_Frees "S" pred2RTsBsCs;
   709 
   710     val fs_copy = map2 (retype_free o fastype_of) fs gs;
   711     val x_copy = retype_free CA' y;
   712 
   713     val setRs =
   714       map3 (fn R => fn T => fn U =>
   715           HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As' Bs';
   716 
   717     (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
   718       Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
   719     val OO_Grp =
   720       let
   721         val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
   722         val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
   723         val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
   724       in
   725         mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
   726       end;
   727 
   728     val rel_rhs = (case raw_rel_opt of
   729         NONE => fold_rev Term.absfree Rs' OO_Grp
   730       | SOME raw_rel => prep_term no_defs_lthy raw_rel);
   731 
   732     val rel_bind_def =
   733       (fn () => if Binding.is_empty rel_b then Binding.suffix_name ("_" ^ relN) b else rel_b,
   734        rel_rhs);
   735 
   736     val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
   737       lthy
   738       |> maybe_define (is_some raw_rel_opt) rel_bind_def
   739       ||> `(maybe_restore lthy);
   740 
   741     val phi = Proof_Context.export_morphism lthy_old lthy;
   742     val bnf_rel_def = Morphism.thm phi raw_rel_def;
   743     val bnf_rel = Morphism.term phi bnf_rel_term;
   744 
   745     fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel;
   746 
   747     val rel = mk_bnf_rel pred2RTs CA' CB';
   748 
   749     val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
   750         raw_wit_defs @ [raw_rel_def]) of
   751         [] => ()
   752       | defs => Proof_Display.print_consts true lthy_old (K false)
   753           (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
   754 
   755     val map_id_goal =
   756       let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
   757         mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
   758       end;
   759 
   760     val map_comp_goal =
   761       let
   762         val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
   763         val comp_bnf_map_app = HOLogic.mk_comp
   764           (Term.list_comb (bnf_map_BsCs, gs), Term.list_comb (bnf_map_AsBs, fs));
   765       in
   766         fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
   767       end;
   768 
   769     fun mk_map_cong_prem x z set f f_copy =
   770       Logic.all z (Logic.mk_implies
   771         (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set $ x)),
   772         mk_Trueprop_eq (f $ z, f_copy $ z)));
   773 
   774     val map_cong0_goal =
   775       let
   776         val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy;
   777         val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
   778           Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
   779       in
   780         fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
   781       end;
   782 
   783     val set_maps_goal =
   784       let
   785         fun mk_goal setA setB f =
   786           let
   787             val set_comp_map =
   788               HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));
   789             val image_comp_set = HOLogic.mk_comp (mk_image f, setA);
   790           in
   791             fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
   792           end;
   793       in
   794         map3 mk_goal bnf_sets_As bnf_sets_Bs fs
   795       end;
   796 
   797     val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
   798 
   799     val cinfinite_bd_goal = HOLogic.mk_Trueprop (mk_cinfinite bnf_bd_As);
   800 
   801     val set_bds_goal =
   802       let
   803         fun mk_goal set =
   804           Logic.all x (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (set $ x)) bnf_bd_As));
   805       in
   806         map mk_goal bnf_sets_As
   807       end;
   808 
   809     val in_bd_goal =
   810       let
   811         val bd = mk_cexp
   812           (if live = 0 then ctwo
   813             else mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo)
   814           bnf_bd_As;
   815       in
   816         fold_rev Logic.all As
   817           (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of (mk_in As bnf_sets_As CA')) bd))
   818       end;
   819 
   820     val map_wpull_goal =
   821       let
   822         val prems = map HOLogic.mk_Trueprop
   823           (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s);
   824         val CX = mk_bnf_T domTs CA;
   825         val CB1 = mk_bnf_T B1Ts CA;
   826         val CB2 = mk_bnf_T B2Ts CA;
   827         val bnf_sets_CX = map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
   828         val bnf_sets_CB1 = map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets;
   829         val bnf_sets_CB2 = map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets;
   830         val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s);
   831         val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s);
   832         val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s);
   833         val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s);
   834 
   835         val map_wpull = mk_wpull (mk_in Xs bnf_sets_CX CX)
   836           (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2)
   837           bnf_map_app_f1 bnf_map_app_f2 NONE bnf_map_app_p1 bnf_map_app_p2;
   838       in
   839         fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s)
   840           (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
   841       end;
   842 
   843     val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
   844 
   845     val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
   846       cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal rel_OO_Grp_goal;
   847 
   848     fun mk_wit_goals (I, wit) =
   849       let
   850         val xs = map (nth bs) I;
   851         fun wit_goal i =
   852           let
   853             val z = nth zs i;
   854             val set_wit = nth bnf_sets_As i $ Term.list_comb (wit, xs);
   855             val concl = HOLogic.mk_Trueprop
   856               (if member (op =) I i then HOLogic.mk_eq (z, nth bs i)
   857               else @{term False});
   858           in
   859             fold_rev Logic.all (z :: xs)
   860               (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (z, set_wit)), concl))
   861           end;
   862       in
   863         map wit_goal (0 upto live - 1)
   864       end;
   865 
   866     val wit_goalss = map mk_wit_goals bnf_wit_As;
   867 
   868     fun after_qed thms lthy =
   869       let
   870         val (axioms, wit_thms) = apfst (mk_axioms live) (chop (length goals) thms);
   871 
   872         val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
   873         val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
   874         val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   875 
   876         fun mk_collect_set_map () =
   877           let
   878             val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T;
   879             val collect_map = HOLogic.mk_comp
   880               (mk_collect (map (mk_bnf_t Ts) bnf_sets) defT,
   881               Term.list_comb (mk_bnf_map As' Ts, hs));
   882             val image_collect = mk_collect
   883               (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
   884               defT;
   885             (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
   886             val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
   887           in
   888             Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms)))
   889             |> Thm.close_derivation
   890           end;
   891 
   892         val collect_set_map = Lazy.lazy mk_collect_set_map;
   893 
   894         fun mk_in_mono () =
   895           let
   896             val prems_mono = map2 (HOLogic.mk_Trueprop oo mk_leq) As As_copy;
   897             val in_mono_goal =
   898               fold_rev Logic.all (As @ As_copy)
   899                 (Logic.list_implies (prems_mono, HOLogic.mk_Trueprop
   900                   (mk_leq (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
   901           in
   902             Goal.prove_sorry lthy [] [] in_mono_goal (K (mk_in_mono_tac live))
   903             |> Thm.close_derivation
   904           end;
   905 
   906         val in_mono = Lazy.lazy mk_in_mono;
   907 
   908         fun mk_in_cong () =
   909           let
   910             val prems_cong = map2 (curry mk_Trueprop_eq) As As_copy;
   911             val in_cong_goal =
   912               fold_rev Logic.all (As @ As_copy)
   913                 (Logic.list_implies (prems_cong,
   914                   mk_Trueprop_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA')));
   915           in
   916             Goal.prove_sorry lthy [] [] in_cong_goal
   917               (K ((TRY o hyp_subst_tac lthy THEN' rtac refl) 1))
   918             |> Thm.close_derivation
   919           end;
   920 
   921         val in_cong = Lazy.lazy mk_in_cong;
   922 
   923         val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id axioms));
   924         val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
   925 
   926         fun mk_map_cong () =
   927           let
   928             val prem0 = mk_Trueprop_eq (x, x_copy);
   929             val prems = map4 (mk_map_cong_prem x_copy) zs bnf_sets_As fs fs_copy;
   930             val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
   931               Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
   932             val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
   933               (Logic.list_implies (prem0 :: prems, eq));
   934           in
   935             Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
   936             |> Thm.close_derivation
   937           end;
   938 
   939         val map_cong = Lazy.lazy mk_map_cong;
   940 
   941         val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms);
   942 
   943         fun mk_map_wppull () =
   944           let
   945             val prems = if live = 0 then [] else
   946               [HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   947                 (map8 mk_wpull Xs B1s B2s f1s f2s (map SOME (e1s ~~ e2s)) p1s p2s))];
   948             val CX = mk_bnf_T domTs CA;
   949             val CB1 = mk_bnf_T B1Ts CA;
   950             val CB2 = mk_bnf_T B2Ts CA;
   951             val bnf_sets_CX =
   952               map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
   953             val bnf_sets_CB1 =
   954               map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets;
   955             val bnf_sets_CB2 =
   956               map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets;
   957             val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s);
   958             val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s);
   959             val bnf_map_app_e1 = Term.list_comb (mk_bnf_map B1Ts ranTs', e1s);
   960             val bnf_map_app_e2 = Term.list_comb (mk_bnf_map B2Ts ranTs'', e2s);
   961             val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s);
   962             val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s);
   963 
   964             val concl = mk_wpull (mk_in Xs bnf_sets_CX CX)
   965               (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2)
   966               bnf_map_app_f1 bnf_map_app_f2 (SOME (bnf_map_app_e1, bnf_map_app_e2))
   967               bnf_map_app_p1 bnf_map_app_p2;
   968 
   969             val goal =
   970               fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ e1s @ e2s @ p1s @ p2s)
   971                 (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
   972           in
   973             Goal.prove_sorry lthy [] [] goal
   974               (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
   975                 (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
   976             |> Thm.close_derivation
   977           end;
   978 
   979         val map_wppull = Lazy.lazy mk_map_wppull;
   980 
   981         val rel_OO_Grps = no_refl [#rel_OO_Grp axioms];
   982 
   983         fun mk_rel_Grp () =
   984           let
   985             val lhs = Term.list_comb (rel, map2 mk_Grp As fs);
   986             val rhs = mk_Grp (mk_in As bnf_sets_As CA') (Term.list_comb (bnf_map_AsBs, fs));
   987             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
   988           in
   989             Goal.prove_sorry lthy [] [] goal
   990               (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
   991                 (Lazy.force map_comp') (map Lazy.force set_map'))
   992             |> Thm.close_derivation
   993           end;
   994 
   995         val rel_Grp = Lazy.lazy mk_rel_Grp;
   996 
   997         fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
   998         fun mk_rel_concl f = HOLogic.mk_Trueprop
   999           (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
  1000 
  1001         fun mk_rel_mono () =
  1002           let
  1003             val mono_prems = mk_rel_prems mk_leq;
  1004             val mono_concl = mk_rel_concl (uncurry mk_leq);
  1005           in
  1006             Goal.prove_sorry lthy [] []
  1007               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
  1008               (mk_rel_mono_tac rel_OO_Grps (Lazy.force in_mono))
  1009             |> Thm.close_derivation
  1010           end;
  1011 
  1012         fun mk_rel_cong () =
  1013           let
  1014             val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
  1015             val cong_concl = mk_rel_concl HOLogic.mk_eq;
  1016           in
  1017             Goal.prove_sorry lthy [] []
  1018               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
  1019               (fn _ => (TRY o hyp_subst_tac lthy THEN' rtac refl) 1)
  1020             |> Thm.close_derivation
  1021           end;
  1022 
  1023         val rel_mono = Lazy.lazy mk_rel_mono;
  1024         val rel_cong = Lazy.lazy mk_rel_cong;
  1025 
  1026         fun mk_rel_eq () =
  1027           let val relAsAs = mk_bnf_rel self_pred2RTs CA' CA' in
  1028             Goal.prove_sorry lthy [] []
  1029               (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
  1030                 HOLogic.eq_const CA'))
  1031               (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
  1032             |> Thm.close_derivation
  1033           end;
  1034 
  1035         val rel_eq = Lazy.lazy mk_rel_eq;
  1036 
  1037         fun mk_rel_conversep () =
  1038           let
  1039             val relBsAs = mk_bnf_rel pred2RT's CB' CA';
  1040             val lhs = Term.list_comb (relBsAs, map mk_conversep Rs);
  1041             val rhs = mk_conversep (Term.list_comb (rel, Rs));
  1042             val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
  1043             val le_thm = Goal.prove_sorry lthy [] [] le_goal
  1044               (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
  1045                 (Lazy.force map_comp') (map Lazy.force set_map'))
  1046               |> Thm.close_derivation
  1047             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
  1048           in
  1049             Goal.prove_sorry lthy [] [] goal
  1050               (K (mk_rel_conversep_tac le_thm (Lazy.force rel_mono)))
  1051             |> Thm.close_derivation
  1052           end;
  1053 
  1054         val rel_conversep = Lazy.lazy mk_rel_conversep;
  1055 
  1056         fun mk_rel_OO () =
  1057           let
  1058             val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
  1059             val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
  1060             val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
  1061             val rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
  1062             val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
  1063           in
  1064             Goal.prove_sorry lthy [] [] goal
  1065               (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
  1066                 (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
  1067             |> Thm.close_derivation
  1068           end;
  1069 
  1070         val rel_OO = Lazy.lazy mk_rel_OO;
  1071 
  1072         fun mk_in_rel () =
  1073           let
  1074             val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
  1075             val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
  1076             val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
  1077             val map_fst_eq = HOLogic.mk_eq (map1 $ z, x);
  1078             val map_snd_eq = HOLogic.mk_eq (map2 $ z, y);
  1079             val lhs = Term.list_comb (rel, Rs) $ x $ y;
  1080             val rhs =
  1081               HOLogic.mk_exists (fst z', snd z', HOLogic.mk_conj (HOLogic.mk_mem (z, bnf_in),
  1082                 HOLogic.mk_conj (map_fst_eq, map_snd_eq)));
  1083             val goal =
  1084               fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
  1085           in
  1086             Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
  1087             |> Thm.close_derivation
  1088           end;
  1089 
  1090         val in_rel = Lazy.lazy mk_in_rel;
  1091 
  1092         fun mk_rel_flip () =
  1093           let
  1094             val rel_conversep_thm = Lazy.force rel_conversep;
  1095             val cts = map (SOME o certify lthy) Rs;
  1096             val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
  1097           in
  1098             unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
  1099             |> singleton (Proof_Context.export names_lthy pre_names_lthy)
  1100           end;
  1101 
  1102         val rel_flip = Lazy.lazy mk_rel_flip;
  1103 
  1104         fun mk_rel_mono_strong () =
  1105           let
  1106             fun mk_prem setA setB R S a b =
  1107               HOLogic.mk_Trueprop
  1108                 (mk_Ball (setA $ x) (Term.absfree (dest_Free a)
  1109                   (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
  1110                     (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
  1111             val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) :: 
  1112               map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
  1113             val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
  1114           in
  1115             Goal.prove_sorry lthy [] []
  1116               (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
  1117               (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map'))
  1118             |> Thm.close_derivation
  1119           end;
  1120 
  1121         val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
  1122 
  1123         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
  1124 
  1125         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono
  1126           in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
  1127           rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
  1128 
  1129         val wits = map2 mk_witness bnf_wits wit_thms;
  1130 
  1131         val bnf_rel =
  1132           Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
  1133 
  1134         val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
  1135           wits bnf_rel;
  1136       in
  1137         (bnf, lthy
  1138           |> (if fact_policy = Note_All then
  1139                 let
  1140                   val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
  1141                   val notes =
  1142                     [(bd_card_orderN, [#bd_card_order axioms]),
  1143                     (bd_cinfiniteN, [#bd_cinfinite axioms]),
  1144                     (bd_Card_orderN, [#bd_Card_order facts]),
  1145                     (bd_CinfiniteN, [#bd_Cinfinite facts]),
  1146                     (bd_CnotzeroN, [#bd_Cnotzero facts]),
  1147                     (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
  1148                     (in_bdN, [#in_bd axioms]),
  1149                     (in_monoN, [Lazy.force (#in_mono facts)]),
  1150                     (in_relN, [Lazy.force (#in_rel facts)]),
  1151                     (map_compN, [#map_comp axioms]),
  1152                     (map_idN, [#map_id axioms]),
  1153                     (map_wpullN, [#map_wpull axioms]),
  1154                     (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
  1155                     (set_mapN, #set_map axioms),
  1156                     (set_bdN, #set_bd axioms)] @
  1157                     (witNs ~~ wit_thms)
  1158                     |> map (fn (thmN, thms) =>
  1159                       ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
  1160                       [(thms, [])]));
  1161                 in
  1162                   Local_Theory.notes notes #> snd
  1163                 end
  1164               else
  1165                 I)
  1166           |> (if fact_policy <> Dont_Note then
  1167                 let
  1168                   val notes =
  1169                     [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
  1170                     (map_cong0N, [#map_cong0 axioms], []),
  1171                     (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
  1172                     (map_id'N, [Lazy.force (#map_id' facts)], []),
  1173                     (rel_eqN, [Lazy.force (#rel_eq facts)], []),
  1174                     (rel_flipN, [Lazy.force (#rel_flip facts)], []),
  1175                     (set_map'N, map Lazy.force (#set_map' facts), []),
  1176                     (rel_OO_GrpN, rel_OO_Grps, []),
  1177                     (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
  1178                     (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
  1179                     (rel_monoN, [Lazy.force (#rel_mono facts)], []),
  1180                     (rel_OON, [Lazy.force (#rel_OO facts)], [])]
  1181                     |> filter_out (null o #2)
  1182                     |> map (fn (thmN, thms, attrs) =>
  1183                       ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)),
  1184                         attrs), [(thms, [])]));
  1185                 in
  1186                   Local_Theory.notes notes #> snd
  1187                 end
  1188               else
  1189                 I))
  1190       end;
  1191 
  1192     val one_step_defs =
  1193       no_reflexive (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
  1194   in
  1195     (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
  1196   end;
  1197 
  1198 fun register_bnf key (bnf, lthy) =
  1199   (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
  1200     (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
  1201 
  1202 (* TODO: Once the invariant "nwits > 0" holds, remove "mk_conjunction_balanced'" and "rtac TrueI"
  1203    below *)
  1204 fun mk_conjunction_balanced' [] = @{prop True}
  1205   | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
  1206 
  1207 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
  1208   (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) =>
  1209   let
  1210     val wits_tac =
  1211       K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
  1212       mk_unfold_thms_then_tac lthy one_step_defs wit_tac;
  1213     val wit_goals = map mk_conjunction_balanced' wit_goalss;
  1214     val wit_thms =
  1215       Goal.prove_sorry lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
  1216       |> Conjunction.elim_balanced (length wit_goals)
  1217       |> map2 (Conjunction.elim_balanced o length) wit_goalss
  1218       |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
  1219   in
  1220     map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
  1221       goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
  1222     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
  1223   end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
  1224 
  1225 val bnf_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
  1226   Proof.unfolding ([[(defs, [])]])
  1227     (Proof.theorem NONE (snd o register_bnf key oo after_qed)
  1228       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
  1229   prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty Binding.empty
  1230     [];
  1231 
  1232 fun print_bnfs ctxt =
  1233   let
  1234     fun pretty_set sets i = Pretty.block
  1235       [Pretty.str (mk_setN (i + 1) ^ ":"), Pretty.brk 1,
  1236           Pretty.quote (Syntax.pretty_term ctxt (nth sets i))];
  1237 
  1238     fun pretty_bnf (key, BNF {T = T, map = map, sets = sets, bd = bd,
  1239       live = live, lives = lives, dead = dead, deads = deads, ...}) =
  1240       Pretty.big_list
  1241         (Pretty.string_of (Pretty.block [Pretty.str key, Pretty.str ":", Pretty.brk 1,
  1242           Pretty.quote (Syntax.pretty_typ ctxt T)]))
  1243         ([Pretty.block [Pretty.str "live:", Pretty.brk 1, Pretty.str (string_of_int live),
  1244             Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) lives)],
  1245           Pretty.block [Pretty.str "dead:", Pretty.brk 1, Pretty.str (string_of_int dead),
  1246             Pretty.brk 3, Pretty.list "[" "]" (List.map (Syntax.pretty_typ ctxt) deads)],
  1247           Pretty.block [Pretty.str (mapN ^ ":"), Pretty.brk 1,
  1248             Pretty.quote (Syntax.pretty_term ctxt map)]] @
  1249           List.map (pretty_set sets) (0 upto length sets - 1) @
  1250           [Pretty.block [Pretty.str (bdN ^ ":"), Pretty.brk 1,
  1251             Pretty.quote (Syntax.pretty_term ctxt bd)]]);
  1252   in
  1253     Pretty.big_list "BNFs:" (map pretty_bnf (Symtab.dest (Data.get (Context.Proof ctxt))))
  1254     |> Pretty.writeln
  1255   end;
  1256 
  1257 val _ =
  1258   Outer_Syntax.improper_command @{command_spec "print_bnfs"}
  1259     "print all BNFs (bounded natural functors)"
  1260     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
  1261 
  1262 val _ =
  1263   Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
  1264     "register a type as a BNF (bounded natural functor)"
  1265     ((parse_opt_binding_colon -- Parse.term --
  1266        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
  1267        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
  1268        >> bnf_cmd);
  1269 
  1270 end;