src/HOL/BNF/Tools/bnf_def.ML

   val rel_mono_strong_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
   val rel_flip_of_bnf: bnf -> thm
   val set_bd_of_bnf: bnf -> thm list
   val set_defs_of_bnf: bnf -> thm list
+  val set_map0_of_bnf: bnf -> thm list
   val set_map'_of_bnf: bnf -> thm list
-  val set_map_of_bnf: bnf -> thm list
   val wit_thms_of_bnf: bnf -> thm list
   val wit_thmss_of_bnf: bnf -> thm list list
 
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list

 
 type axioms = {
   map_id0: thm,
   map_comp0: thm,
   map_cong0: thm,
-  set_map: thm list,
+  set_map0: thm list,
   bd_card_order: thm,
   bd_cinfinite: thm,
   set_bd: thm list,
   map_wpull: thm,
   rel_OO_Grp: thm
 };
 
-fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
-  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) =
+  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
    bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
 
 fun dest_cons [] = raise List.Empty
   | dest_cons (x :: xs) = (x, xs);
 

   ||>> chop n
   ||>> dest_cons
   ||> the_single
   |> mk_axioms';
 
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
-  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
-
-fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel =
+  [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel];
+
+fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
-  zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+  zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull
     rel_OO_Grp;
 
-fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
   {map_id0 = f map_id0,
     map_comp0 = f map_comp0,
     map_cong0 = f map_cong0,
-    set_map = map f set_map,
+    set_map0 = map f set_map0,
     bd_card_order = f bd_card_order,
     bd_cinfinite = f bd_cinfinite,
     set_bd = map f set_bd,
     map_wpull = f map_wpull,
     rel_OO_Grp = f rel_OO_Grp};

 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
 val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
 val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
 val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
-val set_map_of_bnf = #set_map o #axioms o rep_bnf;
+val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
 val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;

 val map_congN = "map_cong";
 val map_transferN = "map_transfer";
 val map_wpullN = "map_wpull";
 val rel_eqN = "rel_eq";
 val rel_flipN = "rel_flip";
-val set_mapN = "set_map";
+val set_map0N = "set_map0";
 val set_map'N = "set_map'";
 val set_bdN = "set_bd";
 val rel_GrpN = "rel_Grp";
 val rel_conversepN = "rel_conversep";
 val rel_monoN = "rel_mono"

             (map_comp0N, [#map_comp0 axioms]),
             (map_id0N, [#map_id0 axioms]),
             (map_transferN, [Lazy.force (#map_transfer facts)]),
             (map_wpullN, [#map_wpull axioms]),
             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
-            (set_mapN, #set_map axioms),
+            (set_map0N, #set_map0 axioms),
             (set_bdN, #set_bd axioms)] @
             (witNs ~~ wit_thmss_of_bnf bnf)
             |> map (fn (thmN, thms) =>
               ((qualify (Binding.qualify true (Binding.name_of bnf_b) (Binding.name thmN)), []),
               [(thms, [])]));

           Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
       in
         fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
       end;
 
-    val set_maps_goal =
+    val set_map0s_goal =
       let
         fun mk_goal setA setB f =
           let
             val set_comp_map =
               HOLogic.mk_comp (setB, Term.list_comb (bnf_map_AsBs, fs));

           (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
       end;
 
     val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
 
-    val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_maps_goal
+    val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
       card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
 
     fun mk_wit_goals (I, wit) =
       let
         val xs = map (nth bs) I;

               (map2 (fn h => fn set => HOLogic.mk_comp (mk_image h, set)) hs bnf_sets_As)
               defT;
             (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
             val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
           in
-            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms)))
+            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms)))
             |> Thm.close_derivation
           end;
 
         val collect_set_map = Lazy.lazy mk_collect_set_map;
 

             |> Thm.close_derivation
           end;
 
         val map_cong = Lazy.lazy mk_map_cong;
 
-        val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms);
+        val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map0 axioms);
 
         fun mk_in_bd () =
           let
             val bdT = fst (dest_relT (fastype_of bnf_bd_As));
             val bdTs = replicate live bdT;

     |> Pretty.writeln
   end;
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bnfs"}
-    "print all BNFs (bounded natural functors)"
+    "print all bounded natural functors"
     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
-    "register a type as a BNF (bounded natural functor)"
+    "register a type as a bounded natural functor"
     ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
        >> bnf_cmd);