renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
authorblanchet
Wed Apr 24 17:47:22 2013 +0200 (2013-04-24)
changeset 51766f19a4d0ab1bf
parent 51765 224b6eb2313a
child 51767 bbcdd8519253
renamed "set_natural" to "set_map", reflecting {Bl,Po,Tr} concensus
src/HOL/BNF/Examples/Stream.thy
src/HOL/BNF/Examples/TreeFI.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
     1.1 --- a/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 17:03:43 2013 +0200
     1.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 17:47:22 2013 +0200
     1.3 @@ -442,12 +442,12 @@
     1.4  proof (cases "n \<le> m")
     1.5    case False thus ?thesis unfolding smerge_def
     1.6      by (subst stream_set_flat)
     1.7 -      (auto simp: stream.set_natural' in_set_conv_nth simp del: stake.simps
     1.8 +      (auto simp: stream.set_map' in_set_conv_nth simp del: stake.simps
     1.9          intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp])
    1.10  next
    1.11    case True thus ?thesis unfolding smerge_def
    1.12      by (subst stream_set_flat)
    1.13 -      (auto simp: stream.set_natural' in_set_conv_nth image_iff simp del: stake.simps snth.simps
    1.14 +      (auto simp: stream.set_map' in_set_conv_nth image_iff simp del: stake.simps snth.simps
    1.15          intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
    1.16  qed
    1.17  
    1.18 @@ -456,7 +456,7 @@
    1.19    fix x assume "x \<in> stream_set (smerge ss)"
    1.20    thus "x \<in> UNION (stream_set ss) stream_set"
    1.21      unfolding smerge_def by (subst (asm) stream_set_flat)
    1.22 -      (auto simp: stream.set_natural' in_set_conv_nth stream_set_range simp del: stake.simps, fast+)
    1.23 +      (auto simp: stream.set_map' in_set_conv_nth stream_set_range simp del: stake.simps, fast+)
    1.24  next
    1.25    fix s x assume "s \<in> stream_set ss" "x \<in> stream_set s"
    1.26    thus "x \<in> stream_set (smerge ss)" using snth_stream_set_smerge by (auto simp: stream_set_range)
    1.27 @@ -469,7 +469,7 @@
    1.28    "sproduct s1 s2 = smerge (stream_map (\<lambda>x. stream_map (Pair x) s2) s1)"
    1.29  
    1.30  lemma stream_set_sproduct: "stream_set (sproduct s1 s2) = stream_set s1 \<times> stream_set s2"
    1.31 -  unfolding sproduct_def stream_set_smerge by (auto simp: stream.set_natural')
    1.32 +  unfolding sproduct_def stream_set_smerge by (auto simp: stream.set_map')
    1.33  
    1.34  
    1.35  subsection {* interleave two streams *}
     2.1 --- a/src/HOL/BNF/Examples/TreeFI.thy	Wed Apr 24 17:03:43 2013 +0200
     2.2 +++ b/src/HOL/BNF/Examples/TreeFI.thy	Wed Apr 24 17:47:22 2013 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5  lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
     2.6  unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
     2.7 -by (auto simp add: listF.set_natural')
     2.8 +by (auto simp add: listF.set_map')
     2.9  
    2.10  lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
    2.11  unfolding lab_def sub_def treeFI_case_def
     3.1 --- a/src/HOL/BNF/More_BNFs.thy	Wed Apr 24 17:03:43 2013 +0200
     3.2 +++ b/src/HOL/BNF/More_BNFs.thy	Wed Apr 24 17:47:22 2013 +0200
     3.3 @@ -353,7 +353,7 @@
     3.4  apply transfer apply simp
     3.5  done
     3.6  
     3.7 -lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
     3.8 +lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map'
     3.9  
    3.10  lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
    3.11    unfolding fset_rel_def set_rel_def by auto 
    3.12 @@ -422,7 +422,7 @@
    3.13  "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
    3.14  by auto
    3.15  
    3.16 -lemma rcset_natural': "rcset (cIm f x) = f ` rcset x"
    3.17 +lemma rcset_map': "rcset (cIm f x) = f ` rcset x"
    3.18  unfolding cIm_def[abs_def] by simp
    3.19  
    3.20  definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
    3.21 @@ -455,9 +455,9 @@
    3.22    assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
    3.23    apply (simp add: subset_eq Ball_def)
    3.24    apply (rule conjI)
    3.25 -  apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing)
    3.26 +  apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing)
    3.27    apply (clarsimp)
    3.28 -  by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range)
    3.29 +  by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range)
    3.30  qed
    3.31  
    3.32  bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
    3.33 @@ -1151,7 +1151,7 @@
    3.34  Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
    3.35  
    3.36  lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \<longleftrightarrow> M = {#}"
    3.37 -by (metis image_is_empty multiset.set_natural' set_of_eq_empty_iff)
    3.38 +by (metis image_is_empty multiset.set_map' set_of_eq_empty_iff)
    3.39  
    3.40  lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp
    3.41  
    3.42 @@ -1287,7 +1287,7 @@
    3.43  shows "\<exists> N1. N = N1 + {#f a#} \<and> multiset_map f M = N1"
    3.44  proof-
    3.45    have "f a \<in># N"
    3.46 -  using assms multiset.set_natural'[of f "M + {#a#}"] by auto
    3.47 +  using assms multiset.set_map'[of f "M + {#a#}"] by auto
    3.48    then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
    3.49    have "multiset_map f M = N1" using assms unfolding N by simp
    3.50    thus ?thesis using N by blast
    3.51 @@ -1298,7 +1298,7 @@
    3.52  shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> multiset_map f M1 = N"
    3.53  proof-
    3.54    obtain a where a: "a \<in># M" and fa: "f a = b"
    3.55 -  using multiset.set_natural'[of f M] unfolding assms
    3.56 +  using multiset.set_map'[of f M] unfolding assms
    3.57    by (metis image_iff mem_set_of_iff union_single_eq_member)
    3.58    then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
    3.59    have "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp
     4.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:03:43 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 17:47:22 2013 +0200
     4.3 @@ -157,12 +157,12 @@
     4.4        mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
     4.5          (map map_comp_of_bnf inners);
     4.6  
     4.7 -    fun mk_single_set_natural_tac i _ =
     4.8 -      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
     4.9 -        (collect_set_natural_of_bnf outer)
    4.10 -        (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
    4.11 +    fun mk_single_set_map_tac i _ =
    4.12 +      mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
    4.13 +        (collect_set_map_of_bnf outer)
    4.14 +        (map ((fn thms => nth thms i) o set_map_of_bnf) inners);
    4.15  
    4.16 -    val set_natural_tacs = map mk_single_set_natural_tac (0 upto ilive - 1);
    4.17 +    val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1);
    4.18  
    4.19      fun bd_card_order_tac _ =
    4.20        mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
    4.21 @@ -177,7 +177,7 @@
    4.22          map (fn goal =>
    4.23            Goal.prove_sorry lthy [] [] goal
    4.24              (fn {context = ctxt, prems = _} =>
    4.25 -              mk_comp_set_alt_tac ctxt (collect_set_natural_of_bnf outer))
    4.26 +              mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
    4.27            |> Thm.close_derivation)
    4.28          (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
    4.29  
    4.30 @@ -238,7 +238,7 @@
    4.31          unfold_thms_tac lthy basic_thms THEN rtac thm 1
    4.32        end;
    4.33  
    4.34 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    4.35 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    4.36        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    4.37  
    4.38      val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
    4.39 @@ -257,7 +257,7 @@
    4.40        |> map (fn (frees, t) => fold absfree frees t);
    4.41  
    4.42      fun wit_tac {context = ctxt, prems = _} =
    4.43 -      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_natural_of_bnf outer)
    4.44 +      mk_comp_wit_tac ctxt (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer)
    4.45          (maps wit_thms_of_bnf inners);
    4.46  
    4.47      val (bnf', lthy') =
    4.48 @@ -311,7 +311,7 @@
    4.49        rtac refl 1;
    4.50      fun map_cong0_tac {context = ctxt, prems = _} =
    4.51        mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
    4.52 -    val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
    4.53 +    val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf));
    4.54      fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
    4.55      fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
    4.56      val set_bd_tacs =
    4.57 @@ -348,7 +348,7 @@
    4.58          rtac thm 1
    4.59        end;
    4.60  
    4.61 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    4.62 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    4.63        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    4.64  
    4.65      val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
    4.66 @@ -405,12 +405,12 @@
    4.67        rtac refl 1;
    4.68      fun map_cong0_tac {context = ctxt, prems = _} =
    4.69        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    4.70 -    val set_natural_tacs =
    4.71 +    val set_map_tacs =
    4.72        if ! quick_and_dirty then
    4.73          replicate (n + live) (K all_tac)
    4.74        else
    4.75          replicate n (K empty_natural_tac) @
    4.76 -        map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf);
    4.77 +        map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf);
    4.78      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    4.79      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    4.80      val set_bd_tacs =
    4.81 @@ -435,7 +435,7 @@
    4.82      fun srel_O_Gr_tac _ =
    4.83        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
    4.84  
    4.85 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
    4.86 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
    4.87        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
    4.88  
    4.89      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    4.90 @@ -490,7 +490,7 @@
    4.91      fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
    4.92      fun map_cong0_tac {context = ctxt, prems = _} =
    4.93        rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
    4.94 -    val set_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
    4.95 +    val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf));
    4.96      fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
    4.97      fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
    4.98      val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_of_bnf bnf));
    4.99 @@ -512,7 +512,7 @@
   4.100      fun srel_O_Gr_tac _ =
   4.101        mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
   4.102  
   4.103 -    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
   4.104 +    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
   4.105        bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
   4.106  
   4.107      val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
   4.108 @@ -653,7 +653,7 @@
   4.109        SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
   4.110  
   4.111      val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
   4.112 -      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
   4.113 +      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
   4.114        (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
   4.115        (mk_tac (map_wpull_of_bnf bnf))
   4.116        (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
     5.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4    val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
     5.5    val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
     5.6    val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
     5.7 -  val mk_comp_set_natural_tac: thm -> thm -> thm -> thm list -> tactic
     5.8 +  val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
     5.9    val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
    5.10  
    5.11    val mk_kill_bd_card_order_tac: int -> thm -> tactic
    5.12 @@ -64,9 +64,9 @@
    5.13  
    5.14  (* Composition *)
    5.15  
    5.16 -fun mk_comp_set_alt_tac ctxt collect_set_natural =
    5.17 +fun mk_comp_set_alt_tac ctxt collect_set_map =
    5.18    unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
    5.19 -  unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
    5.20 +  unfold_thms_tac ctxt [collect_set_map RS sym] THEN
    5.21    rtac refl 1;
    5.22  
    5.23  fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
    5.24 @@ -78,21 +78,21 @@
    5.25      rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    5.26      map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
    5.27  
    5.28 -fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals =
    5.29 +fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
    5.30    EVERY' ([rtac ext] @
    5.31      replicate 3 (rtac trans_o_apply) @
    5.32      [rtac (arg_cong_Union RS trans),
    5.33       rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
    5.34       rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
    5.35       rtac Gmap_cong0] @
    5.36 -     map (fn thm => rtac (thm RS fun_cong)) set_naturals @
    5.37 -     [rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    5.38 +     map (fn thm => rtac (thm RS fun_cong)) set_maps @
    5.39 +     [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    5.40       rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
    5.41 -     rtac (@{thm image_cong} OF [Gset_natural RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    5.42 +     rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    5.43       rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
    5.44       rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    5.45       rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
    5.46 -     [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]},
    5.47 +     [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
    5.48          rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
    5.49          rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
    5.50          rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
    5.51 @@ -217,9 +217,9 @@
    5.52  val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
    5.53    Union_image_insert Union_image_empty};
    5.54  
    5.55 -fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
    5.56 +fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
    5.57    ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
    5.58 -  unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
    5.59 +  unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
    5.60    REPEAT_DETERM (
    5.61      atac 1 ORELSE
    5.62      REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
     6.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:03:43 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:47:22 2013 +0200
     6.3 @@ -45,7 +45,7 @@
     6.4    val bd_Cnotzero_of_bnf: BNF -> thm
     6.5    val bd_card_order_of_bnf: BNF -> thm
     6.6    val bd_cinfinite_of_bnf: BNF -> thm
     6.7 -  val collect_set_natural_of_bnf: BNF -> thm
     6.8 +  val collect_set_map_of_bnf: BNF -> thm
     6.9    val in_bd_of_bnf: BNF -> thm
    6.10    val in_cong_of_bnf: BNF -> thm
    6.11    val in_mono_of_bnf: BNF -> thm
    6.12 @@ -65,8 +65,8 @@
    6.13    val rel_srel_of_bnf: BNF -> thm
    6.14    val set_bd_of_bnf: BNF -> thm list
    6.15    val set_defs_of_bnf: BNF -> thm list
    6.16 -  val set_natural'_of_bnf: BNF -> thm list
    6.17 -  val set_natural_of_bnf: BNF -> thm list
    6.18 +  val set_map'_of_bnf: BNF -> thm list
    6.19 +  val set_map_of_bnf: BNF -> thm list
    6.20    val srel_def_of_bnf: BNF -> thm
    6.21    val srel_Gr_of_bnf: BNF -> thm
    6.22    val srel_Id_of_bnf: BNF -> thm
    6.23 @@ -111,7 +111,7 @@
    6.24    map_id: thm,
    6.25    map_comp: thm,
    6.26    map_cong0: thm,
    6.27 -  set_natural: thm list,
    6.28 +  set_map: thm list,
    6.29    bd_card_order: thm,
    6.30    bd_cinfinite: thm,
    6.31    set_bd: thm list,
    6.32 @@ -121,7 +121,7 @@
    6.33  };
    6.34  
    6.35  fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
    6.36 -  {map_id = id, map_comp = comp, map_cong0 = cong, set_natural = nat, bd_card_order = c_o,
    6.37 +  {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
    6.38     bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
    6.39  
    6.40  fun dest_cons [] = raise Empty
    6.41 @@ -144,17 +144,17 @@
    6.42  fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
    6.43    [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
    6.44  
    6.45 -fun dest_axioms {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
    6.46 -  in_bd, map_wpull, srel_O_Gr} =
    6.47 -  zip_axioms map_id map_comp map_cong0 set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
    6.48 +fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd, in_bd,
    6.49 +  map_wpull, srel_O_Gr} =
    6.50 +  zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd in_bd map_wpull
    6.51      srel_O_Gr;
    6.52  
    6.53 -fun map_axioms f {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
    6.54 +fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
    6.55    in_bd, map_wpull, srel_O_Gr} =
    6.56    {map_id = f map_id,
    6.57      map_comp = f map_comp,
    6.58      map_cong0 = f map_cong0,
    6.59 -    set_natural = map f set_natural,
    6.60 +    set_map = map f set_map,
    6.61      bd_card_order = f bd_card_order,
    6.62      bd_cinfinite = f bd_cinfinite,
    6.63      set_bd = map f set_bd,
    6.64 @@ -182,7 +182,7 @@
    6.65    bd_Card_order: thm,
    6.66    bd_Cinfinite: thm,
    6.67    bd_Cnotzero: thm,
    6.68 -  collect_set_natural: thm lazy,
    6.69 +  collect_set_map: thm lazy,
    6.70    in_cong: thm lazy,
    6.71    in_mono: thm lazy,
    6.72    in_srel: thm lazy,
    6.73 @@ -193,7 +193,7 @@
    6.74    rel_eq: thm lazy,
    6.75    rel_flip: thm lazy,
    6.76    rel_srel: thm lazy,
    6.77 -  set_natural': thm lazy list,
    6.78 +  set_map': thm lazy list,
    6.79    srel_cong: thm lazy,
    6.80    srel_mono: thm lazy,
    6.81    srel_Id: thm lazy,
    6.82 @@ -202,13 +202,13 @@
    6.83    srel_O: thm lazy
    6.84  };
    6.85  
    6.86 -fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
    6.87 -    map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_natural' srel_cong srel_mono
    6.88 +fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_srel
    6.89 +    map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map' srel_cong srel_mono
    6.90      srel_Id srel_Gr srel_converse srel_O = {
    6.91    bd_Card_order = bd_Card_order,
    6.92    bd_Cinfinite = bd_Cinfinite,
    6.93    bd_Cnotzero = bd_Cnotzero,
    6.94 -  collect_set_natural = collect_set_natural,
    6.95 +  collect_set_map = collect_set_map,
    6.96    in_cong = in_cong,
    6.97    in_mono = in_mono,
    6.98    in_srel = in_srel,
    6.99 @@ -219,7 +219,7 @@
   6.100    rel_eq = rel_eq,
   6.101    rel_flip = rel_flip,
   6.102    rel_srel = rel_srel,
   6.103 -  set_natural' = set_natural',
   6.104 +  set_map' = set_map',
   6.105    srel_cong = srel_cong,
   6.106    srel_mono = srel_mono,
   6.107    srel_Id = srel_Id,
   6.108 @@ -231,7 +231,7 @@
   6.109    bd_Card_order,
   6.110    bd_Cinfinite,
   6.111    bd_Cnotzero,
   6.112 -  collect_set_natural,
   6.113 +  collect_set_map,
   6.114    in_cong,
   6.115    in_mono,
   6.116    in_srel,
   6.117 @@ -242,7 +242,7 @@
   6.118    rel_eq,
   6.119    rel_flip,
   6.120    rel_srel,
   6.121 -  set_natural',
   6.122 +  set_map',
   6.123    srel_cong,
   6.124    srel_mono,
   6.125    srel_Id,
   6.126 @@ -252,7 +252,7 @@
   6.127    {bd_Card_order = f bd_Card_order,
   6.128      bd_Cinfinite = f bd_Cinfinite,
   6.129      bd_Cnotzero = f bd_Cnotzero,
   6.130 -    collect_set_natural = Lazy.map f collect_set_natural,
   6.131 +    collect_set_map = Lazy.map f collect_set_map,
   6.132      in_cong = Lazy.map f in_cong,
   6.133      in_mono = Lazy.map f in_mono,
   6.134      in_srel = Lazy.map f in_srel,
   6.135 @@ -263,7 +263,7 @@
   6.136      rel_eq = Lazy.map f rel_eq,
   6.137      rel_flip = Lazy.map f rel_flip,
   6.138      rel_srel = Lazy.map f rel_srel,
   6.139 -    set_natural' = map (Lazy.map f) set_natural',
   6.140 +    set_map' = map (Lazy.map f) set_map',
   6.141      srel_cong = Lazy.map f srel_cong,
   6.142      srel_mono = Lazy.map f srel_mono,
   6.143      srel_Id = Lazy.map f srel_Id,
   6.144 @@ -368,7 +368,7 @@
   6.145  val bd_Card_order_of_bnf = #bd_Card_order o #facts o rep_bnf;
   6.146  val bd_Cinfinite_of_bnf = #bd_Cinfinite o #facts o rep_bnf;
   6.147  val bd_Cnotzero_of_bnf = #bd_Cnotzero o #facts o rep_bnf;
   6.148 -val collect_set_natural_of_bnf = Lazy.force o #collect_set_natural o #facts o rep_bnf;
   6.149 +val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
   6.150  val in_bd_of_bnf = #in_bd o #axioms o rep_bnf;
   6.151  val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
   6.152  val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
   6.153 @@ -388,8 +388,8 @@
   6.154  val rel_srel_of_bnf = Lazy.force o #rel_srel o #facts o rep_bnf;
   6.155  val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
   6.156  val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
   6.157 -val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
   6.158 -val set_natural'_of_bnf = map Lazy.force o #set_natural' o #facts o rep_bnf;
   6.159 +val set_map_of_bnf = #set_map o #axioms o rep_bnf;
   6.160 +val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
   6.161  val srel_cong_of_bnf = Lazy.force o #srel_cong o #facts o rep_bnf;
   6.162  val srel_mono_of_bnf = Lazy.force o #srel_mono o #facts o rep_bnf;
   6.163  val srel_def_of_bnf = #srel_def o #defs o rep_bnf;
   6.164 @@ -507,7 +507,7 @@
   6.165  val bd_Card_orderN = "bd_Card_order";
   6.166  val bd_CinfiniteN = "bd_Cinfinite";
   6.167  val bd_CnotzeroN = "bd_Cnotzero";
   6.168 -val collect_set_naturalN = "collect_set_natural";
   6.169 +val collect_set_mapN = "collect_set_map";
   6.170  val in_bdN = "in_bd";
   6.171  val in_monoN = "in_mono";
   6.172  val in_srelN = "in_srel";
   6.173 @@ -521,8 +521,8 @@
   6.174  val rel_eqN = "rel_eq";
   6.175  val rel_flipN = "rel_flip";
   6.176  val rel_srelN = "rel_srel";
   6.177 -val set_naturalN = "set_natural";
   6.178 -val set_natural'N = "set_natural'";
   6.179 +val set_mapN = "set_map";
   6.180 +val set_map'N = "set_map'";
   6.181  val set_bdN = "set_bd";
   6.182  val srel_IdN = "srel_Id";
   6.183  val srel_GrN = "srel_Gr";
   6.184 @@ -835,7 +835,7 @@
   6.185          fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
   6.186        end;
   6.187  
   6.188 -    val set_naturals_goal =
   6.189 +    val set_maps_goal =
   6.190        let
   6.191          fun mk_goal setA setB f =
   6.192            let
   6.193 @@ -897,8 +897,8 @@
   6.194  
   6.195      val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
   6.196  
   6.197 -    val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_naturals_goal
   6.198 -      card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
   6.199 +    val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
   6.200 +      cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
   6.201  
   6.202      fun mk_wit_goals (I, wit) =
   6.203        let
   6.204 @@ -928,7 +928,7 @@
   6.205          val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
   6.206          val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
   6.207  
   6.208 -        fun mk_collect_set_natural () =
   6.209 +        fun mk_collect_set_map () =
   6.210            let
   6.211              val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T;
   6.212              val collect_map = HOLogic.mk_comp
   6.213 @@ -940,11 +940,11 @@
   6.214              (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
   6.215              val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
   6.216            in
   6.217 -            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
   6.218 +            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms)))
   6.219              |> Thm.close_derivation
   6.220            end;
   6.221  
   6.222 -        val collect_set_natural = Lazy.lazy mk_collect_set_natural;
   6.223 +        val collect_set_map = Lazy.lazy mk_collect_set_map;
   6.224  
   6.225          fun mk_in_mono () =
   6.226            let
   6.227 @@ -992,8 +992,7 @@
   6.228  
   6.229          val map_cong = Lazy.lazy mk_map_cong;
   6.230  
   6.231 -        val set_natural' =
   6.232 -          map (fn thm => Lazy.lazy (fn () => mk_set_natural' thm)) (#set_natural axioms);
   6.233 +        val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms);
   6.234  
   6.235          fun mk_map_wppull () =
   6.236            let
   6.237 @@ -1027,7 +1026,7 @@
   6.238            in
   6.239              Goal.prove_sorry lthy [] [] goal
   6.240                (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
   6.241 -                (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
   6.242 +                (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
   6.243              |> Thm.close_derivation
   6.244            end;
   6.245  
   6.246 @@ -1043,7 +1042,7 @@
   6.247            in
   6.248              Goal.prove_sorry lthy [] [] goal
   6.249                (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
   6.250 -                (Lazy.force map_comp') (map Lazy.force set_natural'))
   6.251 +                (Lazy.force map_comp') (map Lazy.force set_map'))
   6.252              |> Thm.close_derivation
   6.253            end;
   6.254  
   6.255 @@ -1096,7 +1095,7 @@
   6.256              val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
   6.257              val le_thm = Goal.prove_sorry lthy [] [] le_goal
   6.258                (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   6.259 -                (Lazy.force map_comp') (map Lazy.force set_natural'))
   6.260 +                (Lazy.force map_comp') (map Lazy.force set_map'))
   6.261                |> Thm.close_derivation
   6.262              val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
   6.263            in
   6.264 @@ -1116,7 +1115,7 @@
   6.265            in
   6.266              Goal.prove_sorry lthy [] [] goal
   6.267                (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
   6.268 -                (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
   6.269 +                (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
   6.270              |> Thm.close_derivation
   6.271            end;
   6.272  
   6.273 @@ -1176,9 +1175,9 @@
   6.274  
   6.275          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
   6.276  
   6.277 -        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
   6.278 -          in_mono in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel
   6.279 -          set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
   6.280 +        val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono
   6.281 +          in_srel map_comp' map_cong map_id' map_wppull rel_eq rel_flip rel_srel set_map'
   6.282 +          srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
   6.283  
   6.284          val wits = map2 mk_witness bnf_wits wit_thms;
   6.285  
   6.286 @@ -1200,14 +1199,14 @@
   6.287                      (bd_Card_orderN, [#bd_Card_order facts]),
   6.288                      (bd_CinfiniteN, [#bd_Cinfinite facts]),
   6.289                      (bd_CnotzeroN, [#bd_Cnotzero facts]),
   6.290 -                    (collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]),
   6.291 +                    (collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
   6.292                      (in_bdN, [#in_bd axioms]),
   6.293                      (in_monoN, [Lazy.force (#in_mono facts)]),
   6.294                      (in_srelN, [Lazy.force (#in_srel facts)]),
   6.295                      (map_compN, [#map_comp axioms]),
   6.296                      (map_idN, [#map_id axioms]),
   6.297                      (map_wpullN, [#map_wpull axioms]),
   6.298 -                    (set_naturalN, #set_natural axioms),
   6.299 +                    (set_mapN, #set_map axioms),
   6.300                      (set_bdN, #set_bd axioms)] @
   6.301                      (witNs ~~ wit_thms)
   6.302                      |> map (fn (thmN, thms) =>
   6.303 @@ -1228,7 +1227,7 @@
   6.304                      (rel_eqN, [Lazy.force (#rel_eq facts)], []),
   6.305                      (rel_flipN, [Lazy.force (#rel_flip facts)], []),
   6.306                      (rel_srelN, [Lazy.force (#rel_srel facts)], []),
   6.307 -                    (set_natural'N, map Lazy.force (#set_natural' facts), []),
   6.308 +                    (set_map'N, map Lazy.force (#set_map' facts), []),
   6.309                      (srel_O_GrN, srel_O_Grs, []),
   6.310                      (srel_IdN, [Lazy.force (#srel_Id facts)], []),
   6.311                      (srel_GrN, [Lazy.force (#srel_Gr facts)], []),
     7.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
     7.3 @@ -8,13 +8,13 @@
     7.4  
     7.5  signature BNF_DEF_TACTICS =
     7.6  sig
     7.7 -  val mk_collect_set_natural_tac: thm list -> tactic
     7.8 +  val mk_collect_set_map_tac: thm list -> tactic
     7.9    val mk_map_id': thm -> thm
    7.10    val mk_map_comp': thm -> thm
    7.11    val mk_map_cong_tac: thm -> tactic
    7.12    val mk_in_mono_tac: int -> tactic
    7.13    val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    7.14 -  val mk_set_natural': thm -> thm
    7.15 +  val mk_set_map': thm -> thm
    7.16  
    7.17    val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
    7.18      {prems: thm list, context: Proof.context} -> tactic
    7.19 @@ -39,7 +39,7 @@
    7.20  fun mk_map_cong_tac cong0 =
    7.21    (hyp_subst_tac THEN' rtac cong0 THEN'
    7.22     REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
    7.23 -fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
    7.24 +fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
    7.25  fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
    7.26    else (rtac subsetI THEN'
    7.27    rtac CollectI) 1 THEN
    7.28 @@ -48,15 +48,15 @@
    7.29      ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
    7.30    (etac subset_trans THEN' atac) 1;
    7.31  
    7.32 -fun mk_collect_set_natural_tac set_naturals =
    7.33 +fun mk_collect_set_map_tac set_maps =
    7.34    (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
    7.35 -  EVERY' (map (fn set_natural =>
    7.36 +  EVERY' (map (fn set_map =>
    7.37      rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
    7.38 -    rtac set_natural) set_naturals) THEN'
    7.39 +    rtac set_map) set_maps) THEN'
    7.40    rtac @{thm image_empty}) 1;
    7.41  
    7.42 -fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals =
    7.43 -  if null set_naturals then
    7.44 +fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps =
    7.45 +  if null set_maps then
    7.46      EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
    7.47    else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
    7.48      REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
    7.49 @@ -64,19 +64,19 @@
    7.50      REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
    7.51      CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    7.52        rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
    7.53 -      set_naturals,
    7.54 +      set_maps,
    7.55      CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
    7.56        rtac (map_comp RS trans RS sym), rtac map_cong0,
    7.57 -      REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
    7.58 +      REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
    7.59          rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
    7.60          rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
    7.61  
    7.62 -fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals
    7.63 +fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_maps
    7.64    {context = ctxt, prems = _} =
    7.65    let
    7.66 -    val n = length set_naturals;
    7.67 +    val n = length set_maps;
    7.68    in
    7.69 -    if null set_naturals then
    7.70 +    if null set_maps then
    7.71        unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
    7.72      else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
    7.73        EVERY' [rtac equalityI, rtac subsetI,
    7.74 @@ -93,7 +93,7 @@
    7.75          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    7.76            rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
    7.77            REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    7.78 -          stac @{thm fst_conv}, atac]) set_naturals,
    7.79 +          stac @{thm fst_conv}, atac]) set_maps,
    7.80          rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
    7.81          REPEAT_DETERM o dtac Pair_eqD,
    7.82          REPEAT_DETERM o etac conjE, hyp_subst_tac,
    7.83 @@ -108,7 +108,7 @@
    7.84              CONJ_WRAP' (fn thm =>
    7.85                EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
    7.86                  rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
    7.87 -            set_naturals])
    7.88 +            set_maps])
    7.89            @{thms fst_convol snd_convol} [map_id', refl])] 1
    7.90    end;
    7.91  
    7.92 @@ -125,12 +125,12 @@
    7.93        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
    7.94        rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
    7.95  
    7.96 -fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals
    7.97 +fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_maps
    7.98    {context = ctxt, prems = _} =
    7.99    let
   7.100 -    val n = length set_naturals;
   7.101 +    val n = length set_maps;
   7.102    in
   7.103 -    if null set_naturals then
   7.104 +    if null set_maps then
   7.105        unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
   7.106      else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
   7.107        EVERY' [rtac @{thm subrelI},
   7.108 @@ -143,22 +143,22 @@
   7.109            rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
   7.110            rtac (map_comp RS sym), rtac CollectI,
   7.111            CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   7.112 -            etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   7.113 +            etac @{thm flip_rel}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   7.114    end;
   7.115  
   7.116  fun mk_srel_converse_tac le_converse =
   7.117    EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
   7.118      rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
   7.119  
   7.120 -fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals
   7.121 +fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_maps
   7.122    {context = ctxt, prems = _} =
   7.123    let
   7.124 -    val n = length set_naturals;
   7.125 +    val n = length set_maps;
   7.126      fun in_tac nthO_in = rtac CollectI THEN'
   7.127          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   7.128 -          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
   7.129 +          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
   7.130    in
   7.131 -    if null set_naturals then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
   7.132 +    if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
   7.133      else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
   7.134        EVERY' [rtac equalityI, rtac @{thm subrelI},
   7.135          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   7.136 @@ -190,7 +190,7 @@
   7.137          REPEAT_DETERM o dtac Pair_eqD,
   7.138          REPEAT_DETERM o etac conjE, hyp_subst_tac,
   7.139          rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
   7.140 -        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
   7.141 +        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
   7.142          etac allE, etac impE, etac conjI, etac conjI, atac,
   7.143          REPEAT_DETERM o eresolve_tac [bexE, conjE],
   7.144          rtac @{thm relcompI}, rtac @{thm converseI},
     8.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:03:43 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 17:47:22 2013 +0200
     8.3 @@ -287,8 +287,8 @@
     8.4      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
     8.5      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
     8.6      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
     8.7 -    val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
     8.8 -    val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
     8.9 +    val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    8.10 +    val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
    8.11  
    8.12      val live = live_of_bnf any_fp_bnf;
    8.13  
    8.14 @@ -548,7 +548,7 @@
    8.15  
    8.16              fun mk_set_thm fp_set_thm ctr_def' cxIn =
    8.17                fold_thms lthy [ctr_def']
    8.18 -                (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
    8.19 +                (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @
    8.20                       (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
    8.21                     (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
    8.22                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
    8.23 @@ -814,8 +814,8 @@
    8.24  
    8.25              val thm =
    8.26                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    8.27 -                mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
    8.28 -                  nested_set_natural's pre_set_defss)
    8.29 +                mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' nested_set_map's
    8.30 +                  pre_set_defss)
    8.31                |> singleton (Proof_Context.export names_lthy lthy)
    8.32                |> Thm.close_derivation;
    8.33            in
     9.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
     9.3 @@ -133,26 +133,26 @@
     9.4      hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
     9.5    (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
     9.6  
     9.7 -fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
     9.8 +fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs =
     9.9    EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    9.10 -     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ sum_prod_thms_set0)),
    9.11 +     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_map's @ sum_prod_thms_set0)),
    9.12       solve_prem_prem_tac]) (rev kks)) 1;
    9.13  
    9.14 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
    9.15 +fun mk_induct_discharge_prem_tac ctxt nn n set_map's pre_set_defs m k kks =
    9.16    let val r = length kks in
    9.17      EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
    9.18        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
    9.19      EVERY [REPEAT_DETERM_N r
    9.20          (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
    9.21        if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
    9.22 -      mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs]
    9.23 +      mk_induct_leverage_prem_prems_tac ctxt nn kks set_map's pre_set_defs]
    9.24    end;
    9.25  
    9.26 -fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_natural's pre_set_defss =
    9.27 +fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' set_map's pre_set_defss =
    9.28    let val n = Integer.sum ns in
    9.29      unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_as_projs_tac ctxt 1 THEN
    9.30 -    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
    9.31 -      pre_set_defss mss (unflat mss (1 upto n)) kkss)
    9.32 +    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_map's) pre_set_defss
    9.33 +      mss (unflat mss (1 upto n)) kkss)
    9.34    end;
    9.35  
    9.36  fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
    10.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 17:03:43 2013 +0200
    10.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 17:47:22 2013 +0200
    10.3 @@ -227,7 +227,7 @@
    10.4      val map_id's = map map_id'_of_bnf bnfs;
    10.5      val map_wpulls = map map_wpull_of_bnf bnfs;
    10.6      val set_bdss = map set_bd_of_bnf bnfs;
    10.7 -    val set_natural'ss = map set_natural'_of_bnf bnfs;
    10.8 +    val set_map'ss = map set_map'_of_bnf bnfs;
    10.9      val srel_congs = map srel_cong_of_bnf bnfs;
   10.10      val srel_converses = map srel_converse_of_bnf bnfs;
   10.11      val srel_defs = map srel_def_of_bnf bnfs;
   10.12 @@ -762,7 +762,7 @@
   10.13                singleton (Proof_Context.export names_lthy lthy)
   10.14                  (Goal.prove_sorry lthy [] [] goal
   10.15                    (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs
   10.16 -                    morE_thms set_natural'ss coalg_set_thmss)))
   10.17 +                    morE_thms set_map'ss coalg_set_thmss)))
   10.18                |> Thm.close_derivation)
   10.19              ls goals ctss hset_rec_0ss' hset_rec_Sucss'
   10.20            end;
   10.21 @@ -866,7 +866,7 @@
   10.22          Goal.prove_sorry lthy [] []
   10.23            (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
   10.24              (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
   10.25 -          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_natural'ss))
   10.26 +          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_map'ss))
   10.27          |> Thm.close_derivation
   10.28        end;
   10.29  
   10.30 @@ -1284,7 +1284,7 @@
   10.31      val coalgT_thm =
   10.32        Goal.prove_sorry lthy [] []
   10.33          (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
   10.34 -        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss)
   10.35 +        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_map'ss)
   10.36        |> Thm.close_derivation;
   10.37  
   10.38      val card_of_carT_thms =
   10.39 @@ -1323,14 +1323,13 @@
   10.40          val goalss = map3 (fn carT => fn strT => fn sets =>
   10.41            map3 (mk_goal carT strT) (drop m sets) kks ks) carTAs strTAs tree_setss;
   10.42        in
   10.43 -        map6 (fn i => fn goals =>
   10.44 -            fn carT_def => fn strT_def => fn isNode_def => fn set_naturals =>
   10.45 -          map2 (fn goal => fn set_natural =>
   10.46 +        map6 (fn i => fn goals => fn carT_def => fn strT_def => fn isNode_def => fn set_maps =>
   10.47 +          map2 (fn goal => fn set_map =>
   10.48              Goal.prove_sorry lthy [] [] goal
   10.49 -              (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural)
   10.50 +              (mk_carT_set_tac n i carT_def strT_def isNode_def set_map)
   10.51              |> Thm.close_derivation)
   10.52 -          goals (drop m set_naturals))
   10.53 -        ks goalss carT_defs strT_defs isNode_defs set_natural'ss
   10.54 +          goals (drop m set_maps))
   10.55 +        ks goalss carT_defs strT_defs isNode_defs set_map'ss
   10.56        end;
   10.57  
   10.58      val carT_set_thmss' = transpose carT_set_thmss;
   10.59 @@ -1372,7 +1371,7 @@
   10.60                        (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
   10.61                          carT_defs strT_defs isNode_defs
   10.62                          set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
   10.63 -                        coalgT_thm set_natural'ss)))
   10.64 +                        coalgT_thm set_map'ss)))
   10.65                    |> Thm.close_derivation)
   10.66                  ls goals ctss set_incl_hset_thmss' set_hset_incl_hset_thmsss''
   10.67                end;
   10.68 @@ -1770,7 +1769,7 @@
   10.69            to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
   10.70            length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
   10.71            set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
   10.72 -          set_natural'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
   10.73 +          set_map'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
   10.74        |> Thm.close_derivation;
   10.75  
   10.76      val timer = time (timer "Behavioral morphism");
   10.77 @@ -1809,7 +1808,7 @@
   10.78      val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
   10.79        (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
   10.80        (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
   10.81 -        set_natural'ss coalgT_set_thmss))
   10.82 +        set_map'ss coalgT_set_thmss))
   10.83        |> Thm.close_derivation;
   10.84  
   10.85      val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
   10.86 @@ -2517,7 +2516,7 @@
   10.87                map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
   10.88                  singleton (Proof_Context.export names_lthy lthy)
   10.89                    (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
   10.90 -                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_natural'ss))
   10.91 +                    (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_map'ss))
   10.92                  |> Thm.close_derivation)
   10.93                goals ctss hset_rec_0ss' hset_rec_Sucss';
   10.94            in
   10.95 @@ -2585,7 +2584,7 @@
   10.96  
   10.97              val thm = singleton (Proof_Context.export names_lthy lthy)
   10.98                (Goal.prove_sorry lthy [] [] goal
   10.99 -              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_natural'ss
  10.100 +              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
  10.101                set_hset_thmss set_hset_hset_thmsss)))
  10.102                |> Thm.close_derivation
  10.103            in
  10.104 @@ -2621,7 +2620,7 @@
  10.105                (Logic.mk_implies (wpull_prem, coalg));
  10.106            in
  10.107              Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
  10.108 -              set_natural'ss pickWP_assms_tacs)
  10.109 +              set_map'ss pickWP_assms_tacs)
  10.110              |> Thm.close_derivation
  10.111            end;
  10.112  
  10.113 @@ -2672,7 +2671,7 @@
  10.114              val thms =
  10.115                map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  10.116                  singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal
  10.117 -                  (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss
  10.118 +                  (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_map'ss
  10.119                      map_wpull_thms pickWP_assms_tacs))
  10.120                  |> Thm.close_derivation)
  10.121                ls goals ctss hset_rec_0ss' hset_rec_Sucss';
  10.122 @@ -2687,7 +2686,7 @@
  10.123          val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
  10.124          val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
  10.125          val set_nat_tacss =
  10.126 -          map2 (map2 (K oo mk_set_natural_tac)) hset_defss (transpose col_natural_thmss);
  10.127 +          map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss);
  10.128  
  10.129          val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order));
  10.130          val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite));
  10.131 @@ -2866,7 +2865,7 @@
  10.132            in
  10.133              map2 (fn goal => fn induct =>
  10.134                Goal.prove_sorry lthy [] [] goal
  10.135 -                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
  10.136 +                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_map'ss) wit_thms)
  10.137                |> Thm.close_derivation)
  10.138              goals dtor_hset_induct_thms
  10.139              |> map split_conj_thm
  10.140 @@ -2943,13 +2942,13 @@
  10.141            in
  10.142              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
  10.143                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
  10.144 -              fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
  10.145 +              fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
  10.146                Goal.prove_sorry lthy [] [] goal
  10.147                  (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
  10.148 -                  dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
  10.149 +                  dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
  10.150                |> Thm.close_derivation)
  10.151              ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
  10.152 -              dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
  10.153 +              dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss
  10.154                dtor_set_set_incl_thmsss
  10.155            end;
  10.156  
    11.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
    11.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
    11.3 @@ -110,7 +110,7 @@
    11.4    val mk_set_incl_hin_tac: thm list -> tactic
    11.5    val mk_set_incl_hset_tac: thm -> thm -> tactic
    11.6    val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
    11.7 -  val mk_set_natural_tac: thm -> thm -> tactic
    11.8 +  val mk_set_map_tac: thm -> thm -> tactic
    11.9    val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
   11.10      thm list list -> thm list list -> tactic
   11.11    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
   11.12 @@ -230,38 +230,38 @@
   11.13      EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
   11.14      REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
   11.15  
   11.16 -fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =
   11.17 +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss =
   11.18    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   11.19      REPEAT_DETERM o rtac allI,
   11.20      CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
   11.21      REPEAT_DETERM o rtac allI,
   11.22      CONJ_WRAP'
   11.23 -      (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) =>
   11.24 +      (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
   11.25          EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
   11.26            if m = 0 then K all_tac
   11.27            else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
   11.28 -            rtac (nth passive_set_naturals (j - 1) RS sym),
   11.29 +            rtac (nth passive_set_maps (j - 1) RS sym),
   11.30              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
   11.31            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   11.32 -            (fn (i, (set_natural, coalg_set)) =>
   11.33 +            (fn (i, (set_map, coalg_set)) =>
   11.34                EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
   11.35 -                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,
   11.36 +                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
   11.37                  rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
   11.38                  ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
   11.39                  REPEAT_DETERM o etac allE, atac, atac])
   11.40 -            (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])
   11.41 -      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;
   11.42 +            (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
   11.43 +      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
   11.44  
   11.45  fun mk_mor_hset_tac hset_def mor_hset_rec =
   11.46    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
   11.47      atac, atac, rtac (hset_def RS sym)] 1
   11.48  
   11.49 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss =
   11.50 +fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
   11.51    let
   11.52      val n = length srel_O_Grs;
   11.53 -    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs);
   11.54 +    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
   11.55  
   11.56 -    fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
   11.57 +    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
   11.58        EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
   11.59          etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
   11.60          rtac (srel_O_Gr RS equalityD2 RS set_mp),
   11.61 @@ -275,12 +275,12 @@
   11.62                  etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
   11.63                else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
   11.64                  rtac trans_fun_cong_image_id_id_apply, atac])
   11.65 -            (1 upto (m + n) ~~ set_naturals),
   11.66 +            (1 upto (m + n) ~~ set_maps),
   11.67              rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
   11.68              REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
   11.69            @{thms fst_diag_id snd_diag_id})];
   11.70  
   11.71 -    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
   11.72 +    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
   11.73        EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
   11.74          etac allE, etac allE, etac impE, atac,
   11.75          dtac (srel_O_Gr RS equalityD1 RS set_mp),
   11.76 @@ -306,7 +306,7 @@
   11.77              rtac @{thm Id_on_fst}, etac set_mp, atac]
   11.78            else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
   11.79              rtac trans_fun_cong_image_id_id_apply, atac])
   11.80 -        (1 upto (m + n) ~~ set_naturals)];
   11.81 +        (1 upto (m + n) ~~ set_maps)];
   11.82    in
   11.83      EVERY' [rtac (bis_def RS trans),
   11.84        rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
   11.85 @@ -401,7 +401,7 @@
   11.86      rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
   11.87      etac @{thm relcompI}, atac] 1;
   11.88  
   11.89 -fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =
   11.90 +fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} =
   11.91    let
   11.92      val n = length strT_defs;
   11.93      val ks = 1 upto n;
   11.94 @@ -446,7 +446,7 @@
   11.95              rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   11.96    in
   11.97      unfold_thms_tac ctxt defs THEN
   11.98 -    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
   11.99 +    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
  11.100    end;
  11.101  
  11.102  fun mk_card_of_carT_tac m isNode_defs sbd_sbd
  11.103 @@ -539,7 +539,7 @@
  11.104        atac] 1
  11.105    end;
  11.106  
  11.107 -fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
  11.108 +fun mk_carT_set_tac n i carT_def strT_def isNode_def set_map {context = ctxt, prems = _}=
  11.109    EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
  11.110      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
  11.111      dtac Pair_eqD,
  11.112 @@ -550,20 +550,20 @@
  11.113      rtac (strT_def RS arg_cong RS trans),
  11.114      etac (arg_cong RS trans),
  11.115      fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
  11.116 -    rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
  11.117 +    rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
  11.118      etac @{thm prefCl_Succ}, atac] 1;
  11.119  
  11.120  fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
  11.121 -  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss =
  11.122 +  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
  11.123    let
  11.124 -    val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss;
  11.125 +    val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
  11.126      val ks = 1 upto n;
  11.127 -    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) =
  11.128 +    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_map)))) =
  11.129        CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
  11.130          (if i = i'
  11.131          then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
  11.132            rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
  11.133 -          rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
  11.134 +          rtac (Thm.permute_prems 0 1 (set_map RS box_equals)),
  11.135            rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
  11.136            rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
  11.137          else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
  11.138 @@ -585,7 +585,7 @@
  11.139      EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
  11.140        REPEAT_DETERM o rtac allI, rtac impI,
  11.141        CONJ_WRAP' base_tac
  11.142 -        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))),
  11.143 +        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_maps)))),
  11.144        REPEAT_DETERM o rtac allI, rtac impI,
  11.145        REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
  11.146        CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
  11.147 @@ -840,14 +840,14 @@
  11.148  
  11.149  fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
  11.150    to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
  11.151 -  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
  11.152 +  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_mapss coalg_setss
  11.153    map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
  11.154    let
  11.155      val n = length beh_defs;
  11.156      val ks = 1 upto n;
  11.157  
  11.158      fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
  11.159 -      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,
  11.160 +      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps,
  11.161          (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
  11.162        EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
  11.163          rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
  11.164 @@ -863,29 +863,29 @@
  11.165          rtac conjI,
  11.166            rtac ballI, etac @{thm UN_E}, rtac conjI,
  11.167            if n = 1 then K all_tac else rtac (mk_sumEN n),
  11.168 -          EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
  11.169 +          EVERY' (map6 (fn i => fn isNode_def => fn set_maps =>
  11.170              fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
  11.171              EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
  11.172                rtac exI, rtac conjI,
  11.173                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
  11.174                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
  11.175                  etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
  11.176 -              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
  11.177 -                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
  11.178 +              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
  11.179 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
  11.180                    rtac trans_fun_cong_image_id_id_apply,
  11.181                    etac set_rv_Lev, TRY o atac, etac conjI, atac])
  11.182 -              (take m set_naturals) set_rv_Levs),
  11.183 -              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
  11.184 -                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.185 +              (take m set_maps) set_rv_Levs),
  11.186 +              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
  11.187 +                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.188                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
  11.189                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
  11.190                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
  11.191                    rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
  11.192                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
  11.193                    if n = 1 then rtac refl else atac])
  11.194 -              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
  11.195 -          ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss),
  11.196 -          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals,
  11.197 +              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
  11.198 +          ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss),
  11.199 +          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps,
  11.200              (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
  11.201              EVERY' [rtac ballI,
  11.202                REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
  11.203 @@ -894,13 +894,13 @@
  11.204                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
  11.205                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
  11.206                  etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
  11.207 -              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
  11.208 -                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
  11.209 +              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
  11.210 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
  11.211                    rtac trans_fun_cong_image_id_id_apply,
  11.212                    etac set_rv_Lev, TRY o atac, etac conjI, atac])
  11.213 -              (take m set_naturals) set_rv_Levs),
  11.214 -              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
  11.215 -                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.216 +              (take m set_maps) set_rv_Levs),
  11.217 +              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
  11.218 +                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.219                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
  11.220                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
  11.221                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
  11.222 @@ -909,8 +909,8 @@
  11.223                    atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
  11.224                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
  11.225                    if n = 1 then rtac refl else atac])
  11.226 -              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
  11.227 -          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~
  11.228 +              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
  11.229 +          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~
  11.230              (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
  11.231          (**)
  11.232            rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
  11.233 @@ -921,12 +921,12 @@
  11.234            CONVERSION (Conv.top_conv
  11.235              (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
  11.236            if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
  11.237 -          EVERY' (map2 (fn set_natural => fn coalg_set =>
  11.238 -            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
  11.239 +          EVERY' (map2 (fn set_map => fn coalg_set =>
  11.240 +            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
  11.241                rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
  11.242 -            (take m set_naturals) (take m coalg_sets)),
  11.243 -          CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
  11.244 -            EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.245 +            (take m set_maps) (take m coalg_sets)),
  11.246 +          CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
  11.247 +            EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
  11.248                rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
  11.249                rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
  11.250                atac, rtac subsetI,
  11.251 @@ -936,7 +936,7 @@
  11.252                etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
  11.253                  trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
  11.254                rtac rv_Nil])
  11.255 -          (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
  11.256 +          (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
  11.257  
  11.258      fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
  11.259        ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
  11.260 @@ -997,7 +997,7 @@
  11.261      CONJ_WRAP' fbetw_tac
  11.262        (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
  11.263          ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
  11.264 -          (set_naturalss ~~ (coalg_setss ~~
  11.265 +          (set_mapss ~~ (coalg_setss ~~
  11.266              (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
  11.267      CONJ_WRAP' mor_tac
  11.268        (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
  11.269 @@ -1015,22 +1015,22 @@
  11.270      equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
  11.271      etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
  11.272  
  11.273 -fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss =
  11.274 +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss =
  11.275    EVERY' [stac coalg_def,
  11.276 -    CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
  11.277 +    CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
  11.278        EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
  11.279          rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
  11.280 -        EVERY' (map2 (fn set_natural => fn coalgT_set =>
  11.281 -          EVERY' [rtac conjI, rtac (set_natural RS ord_eq_le_trans),
  11.282 +        EVERY' (map2 (fn set_map => fn coalgT_set =>
  11.283 +          EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans),
  11.284              rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
  11.285              etac coalgT_set])
  11.286 -        (take m set_naturals) (take m coalgT_sets)),
  11.287 -        CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) =>
  11.288 -          EVERY' [rtac (set_natural RS ord_eq_le_trans),
  11.289 +        (take m set_maps) (take m coalgT_sets)),
  11.290 +        CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) =>
  11.291 +          EVERY' [rtac (set_map RS ord_eq_le_trans),
  11.292              rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
  11.293              rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
  11.294 -        (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))])
  11.295 -    ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
  11.296 +        (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))])
  11.297 +    ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
  11.298  
  11.299  fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
  11.300    EVERY' [stac mor_def, rtac conjI,
  11.301 @@ -1225,7 +1225,7 @@
  11.302          replicate n (@{thm o_id} RS fun_cong))))
  11.303      maps map_comps map_cong0s)] 1;
  11.304  
  11.305 -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss
  11.306 +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
  11.307    set_hset_hsetsss =
  11.308    let
  11.309      val n = length map_comp's;
  11.310 @@ -1233,7 +1233,7 @@
  11.311    in
  11.312      EVERY' ([rtac rev_mp,
  11.313        coinduct_tac] @
  11.314 -      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets),
  11.315 +      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
  11.316          set_hset_hsetss) =>
  11.317          [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
  11.318           rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
  11.319 @@ -1244,16 +1244,16 @@
  11.320             [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
  11.321             REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
  11.322           REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
  11.323 -         CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
  11.324 +         CONJ_WRAP' (fn (set_map, set_hset_hsets) =>
  11.325             EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
  11.326 -             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural,
  11.327 +             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map,
  11.328               rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
  11.329               REPEAT_DETERM o etac conjE,
  11.330               CONJ_WRAP' (fn set_hset_hset =>
  11.331                 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
  11.332 -           (drop m set_naturals ~~ set_hset_hsetss)])
  11.333 +           (drop m set_maps ~~ set_hset_hsetss)])
  11.334          (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
  11.335 -          map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
  11.336 +          map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @
  11.337        [rtac impI,
  11.338         CONJ_WRAP' (fn k =>
  11.339           EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
  11.340 @@ -1265,7 +1265,7 @@
  11.341    unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
  11.342    ALLGOALS (etac sym);
  11.343  
  11.344 -fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss
  11.345 +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
  11.346    {context = ctxt, prems = _} =
  11.347    let
  11.348      val n = length dtor_maps;
  11.349 @@ -1281,10 +1281,10 @@
  11.350          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
  11.351            (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
  11.352              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
  11.353 -      (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1
  11.354 +      (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
  11.355    end;
  11.356  
  11.357 -fun mk_set_natural_tac hset_def col_natural =
  11.358 +fun mk_set_map_tac hset_def col_natural =
  11.359    EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
  11.360      (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
  11.361      (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
  11.362 @@ -1370,10 +1370,10 @@
  11.363        REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
  11.364    end;
  11.365  
  11.366 -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
  11.367 +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs
  11.368    {context = ctxt, prems = _} =
  11.369    unfold_thms_tac ctxt [coalg_def] THEN
  11.370 -  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
  11.371 +  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
  11.372      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  11.373        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  11.374        hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  11.375 @@ -1383,11 +1383,11 @@
  11.376        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  11.377        rtac CollectI,
  11.378        REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
  11.379 -      CONJ_WRAP' (fn set_natural =>
  11.380 -        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
  11.381 +      CONJ_WRAP' (fn set_map =>
  11.382 +        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map,
  11.383            rtac trans_fun_cong_image_id_id_apply, atac])
  11.384 -      (drop m set_naturals)])
  11.385 -  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
  11.386 +      (drop m set_maps)])
  11.387 +  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
  11.388  
  11.389  fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
  11.390    {context = ctxt, prems = _: thm list} =
  11.391 @@ -1422,7 +1422,7 @@
  11.392        rtac refl])
  11.393    (unfolds ~~ map_comps) 1;
  11.394  
  11.395 -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
  11.396 +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
  11.397    {context = ctxt, prems = _} =
  11.398    let
  11.399      val n = length rec_0s;
  11.400 @@ -1433,7 +1433,7 @@
  11.401        CONJ_WRAP' (fn thm => EVERY'
  11.402          [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
  11.403        REPEAT_DETERM o rtac allI,
  11.404 -      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
  11.405 +      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
  11.406          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
  11.407            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
  11.408            hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
  11.409 @@ -1442,16 +1442,16 @@
  11.410            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
  11.411            rtac ord_eq_le_trans, rtac rec_Suc,
  11.412            rtac @{thm Un_least},
  11.413 -          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
  11.414 +          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1),
  11.415              @{thm prod.cases}]),
  11.416            etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
  11.417 -          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
  11.418 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
  11.419              EVERY' [rtac @{thm UN_least},
  11.420 -              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
  11.421 +              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
  11.422                etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
  11.423                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
  11.424 -          (ks ~~ rev (drop m set_naturals))])
  11.425 -      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
  11.426 +          (ks ~~ rev (drop m set_maps))])
  11.427 +      (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
  11.428    end;
  11.429  
  11.430  fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
  11.431 @@ -1500,26 +1500,26 @@
  11.432      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
  11.433  
  11.434  fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
  11.435 -  set_naturals dtor_set_incls dtor_set_set_inclss =
  11.436 +  set_maps dtor_set_incls dtor_set_set_inclss =
  11.437    let
  11.438      val m = length dtor_set_incls;
  11.439      val n = length dtor_set_set_inclss;
  11.440 -    val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
  11.441 +    val (passive_set_maps, active_set_maps) = chop m set_maps;
  11.442      val in_Jsrel = nth in_Jsrels (i - 1);
  11.443      val if_tac =
  11.444        EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  11.445          rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  11.446 -        EVERY' (map2 (fn set_natural => fn set_incl =>
  11.447 -          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
  11.448 +        EVERY' (map2 (fn set_map => fn set_incl =>
  11.449 +          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
  11.450              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
  11.451              etac (set_incl RS @{thm subset_trans})])
  11.452 -        passive_set_naturals dtor_set_incls),
  11.453 -        CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) =>
  11.454 -          EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
  11.455 +        passive_set_maps dtor_set_incls),
  11.456 +        CONJ_WRAP' (fn (in_Jsrel, (set_map, dtor_set_set_incls)) =>
  11.457 +          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
  11.458              rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  11.459              CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
  11.460              rtac conjI, rtac refl, rtac refl])
  11.461 -        (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
  11.462 +        (in_Jsrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
  11.463          CONJ_WRAP' (fn conv =>
  11.464            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
  11.465            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  11.466 @@ -1529,21 +1529,21 @@
  11.467      val only_if_tac =
  11.468        EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  11.469          rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  11.470 -        CONJ_WRAP' (fn (dtor_set, passive_set_natural) =>
  11.471 +        CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
  11.472            EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
  11.473 -            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
  11.474 +            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
  11.475              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
  11.476              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  11.477 -              (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
  11.478 +              (fn (active_set_map, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
  11.479                  rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
  11.480 -                rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
  11.481 +                rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
  11.482                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
  11.483                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
  11.484                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  11.485                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  11.486                  hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  11.487 -            (rev (active_set_naturals ~~ in_Jsrels))])
  11.488 -        (dtor_sets ~~ passive_set_naturals),
  11.489 +            (rev (active_set_maps ~~ in_Jsrels))])
  11.490 +        (dtor_sets ~~ passive_set_maps),
  11.491          rtac conjI,
  11.492          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
  11.493            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    12.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 17:03:43 2013 +0200
    12.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 17:47:22 2013 +0200
    12.3 @@ -149,7 +149,7 @@
    12.4      val map_id's = map map_id'_of_bnf bnfs;
    12.5      val map_wpulls = map map_wpull_of_bnf bnfs;
    12.6      val set_bdss = map set_bd_of_bnf bnfs;
    12.7 -    val set_natural'ss = map set_natural'_of_bnf bnfs;
    12.8 +    val set_map'ss = map set_map'_of_bnf bnfs;
    12.9  
   12.10      val timer = time (timer "Extracted terms & thms");
   12.11  
   12.12 @@ -388,7 +388,7 @@
   12.13          Goal.prove_sorry lthy [] []
   12.14            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
   12.15               (Logic.list_implies (prems, concl)))
   12.16 -          (K (mk_mor_comp_tac mor_def set_natural'ss map_comp_id_thms))
   12.17 +          (K (mk_mor_comp_tac mor_def set_map'ss map_comp_id_thms))
   12.18          |> Thm.close_derivation
   12.19        end;
   12.20  
   12.21 @@ -407,7 +407,7 @@
   12.22            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
   12.23              (Logic.list_implies (prems, concl)))
   12.24            (K (mk_mor_inv_tac alg_def mor_def
   12.25 -            set_natural'ss morE_thms map_comp_id_thms map_cong0L_thms))
   12.26 +            set_map'ss morE_thms map_comp_id_thms map_cong0L_thms))
   12.27          |> Thm.close_derivation
   12.28        end;
   12.29  
   12.30 @@ -512,7 +512,7 @@
   12.31          val copy_str_thm = Goal.prove_sorry lthy [] []
   12.32            (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   12.33              (Logic.list_implies (all_prems, alg)))
   12.34 -          (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms))
   12.35 +          (K (mk_copy_str_tac set_map'ss alg_def alg_set_thms))
   12.36            |> Thm.close_derivation;
   12.37  
   12.38          val iso = HOLogic.mk_Trueprop
   12.39 @@ -520,7 +520,7 @@
   12.40          val copy_alg_thm = Goal.prove_sorry lthy [] []
   12.41            (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   12.42              (Logic.list_implies (all_prems, iso)))
   12.43 -          (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm))
   12.44 +          (K (mk_copy_alg_tac set_map'ss alg_set_thms mor_def iso_alt_thm copy_str_thm))
   12.45            |> Thm.close_derivation;
   12.46  
   12.47          val ex = HOLogic.mk_Trueprop
   12.48 @@ -871,7 +871,7 @@
   12.49          Goal.prove_sorry lthy [] []
   12.50            (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
   12.51            (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
   12.52 -            alg_select_thm alg_set_thms set_natural'ss str_init_defs))
   12.53 +            alg_select_thm alg_set_thms set_map'ss str_init_defs))
   12.54          |> Thm.close_derivation
   12.55        end;
   12.56  
   12.57 @@ -1318,7 +1318,7 @@
   12.58        in
   12.59          (Goal.prove_sorry lthy [] []
   12.60            (fold_rev Logic.all (phis @ Izs) goal)
   12.61 -          (K (mk_ctor_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
   12.62 +          (K (mk_ctor_induct_tac m set_map'ss init_induct_thm morE_thms mor_Abs_thm
   12.63              Rep_inverses Abs_inverses Reps))
   12.64          |> Thm.close_derivation,
   12.65          rev (Term.add_tfrees goal []))
   12.66 @@ -1509,7 +1509,7 @@
   12.67                  Goal.prove_sorry lthy [] [] goal
   12.68                    (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
   12.69                  |> Thm.close_derivation)
   12.70 -              set_natural'ss) ls simp_goalss setss;
   12.71 +              set_map'ss) ls simp_goalss setss;
   12.72            in
   12.73              ctor_setss
   12.74            end;
   12.75 @@ -1528,13 +1528,13 @@
   12.76            map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf;
   12.77          val setss_by_range' = transpose setss_by_bnf';
   12.78  
   12.79 -        val set_natural_thmss =
   12.80 +        val set_map_thmss =
   12.81            let
   12.82 -            fun mk_set_natural f map z set set' =
   12.83 +            fun mk_set_map f map z set set' =
   12.84                HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
   12.85  
   12.86              fun mk_cphi f map z set set' = certify lthy
   12.87 -              (Term.absfree (dest_Free z) (mk_set_natural f map z set set'));
   12.88 +              (Term.absfree (dest_Free z) (mk_set_map f map z set set'));
   12.89  
   12.90              val csetss = map (map (certify lthy)) setss_by_range';
   12.91  
   12.92 @@ -1547,10 +1547,10 @@
   12.93              val goals =
   12.94                map3 (fn f => fn sets => fn sets' =>
   12.95                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   12.96 -                  (map4 (mk_set_natural f) fs_maps Izs sets sets')))
   12.97 +                  (map4 (mk_set_map f) fs_maps Izs sets sets')))
   12.98                    fs setss_by_range setss_by_range';
   12.99  
  12.100 -            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss ctor_map_thms;
  12.101 +            fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_map'ss ctor_map_thms;
  12.102              val thms =
  12.103                map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
  12.104                  singleton (Proof_Context.export names_lthy lthy)
  12.105 @@ -1693,7 +1693,7 @@
  12.106          val map_comp_tacs =
  12.107            map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
  12.108          val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
  12.109 -        val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
  12.110 +        val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss);
  12.111          val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
  12.112          val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
  12.113          val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
  12.114 @@ -1780,13 +1780,13 @@
  12.115            in
  12.116              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
  12.117                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
  12.118 -              fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
  12.119 +              fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
  12.120                Goal.prove_sorry lthy [] [] goal
  12.121                 (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
  12.122 -                 ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
  12.123 +                 ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
  12.124                |> Thm.close_derivation)
  12.125              ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
  12.126 -              ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
  12.127 +              ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
  12.128                ctor_set_set_incl_thmsss
  12.129            end;
  12.130  
    13.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
    13.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
    13.3 @@ -71,7 +71,7 @@
    13.4      {prems: 'a, context: Proof.context} -> tactic
    13.5    val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
    13.6      thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
    13.7 -  val mk_set_natural_tac: thm -> tactic
    13.8 +  val mk_set_map_tac: thm -> tactic
    13.9    val mk_set_tac: thm -> tactic
   13.10    val mk_wit_tac: int -> thm list -> thm list -> tactic
   13.11    val mk_wpull_tac: thm -> tactic
   13.12 @@ -119,39 +119,39 @@
   13.13    CONJ_WRAP' (fn thm =>
   13.14     (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_id's) 1;
   13.15  
   13.16 -fun mk_mor_comp_tac mor_def set_natural's map_comp_ids =
   13.17 +fun mk_mor_comp_tac mor_def set_map's map_comp_ids =
   13.18    let
   13.19      val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
   13.20 -    fun mor_tac (set_natural', map_comp_id) =
   13.21 +    fun mor_tac (set_map', map_comp_id) =
   13.22        EVERY' [rtac ballI, stac o_apply, rtac trans,
   13.23          rtac trans, dtac @{thm rev_bspec}, atac, etac arg_cong,
   13.24           REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
   13.25        CONJ_WRAP' (fn thm =>
   13.26          FIRST' [rtac subset_UNIV,
   13.27            (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
   13.28 -            etac bspec, etac set_mp, atac])]) set_natural' THEN'
   13.29 +            etac bspec, etac set_mp, atac])]) set_map' THEN'
   13.30        rtac (map_comp_id RS arg_cong);
   13.31    in
   13.32      (dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN'
   13.33      REPEAT o etac conjE THEN'
   13.34      rtac conjI THEN'
   13.35 -    CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
   13.36 -    CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1
   13.37 +    CONJ_WRAP' (K fbetw_tac) set_map's THEN'
   13.38 +    CONJ_WRAP' mor_tac (set_map's ~~ map_comp_ids)) 1
   13.39    end;
   13.40  
   13.41 -fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_cong0Ls =
   13.42 +fun mk_mor_inv_tac alg_def mor_def set_map's morEs map_comp_ids map_cong0Ls =
   13.43    let
   13.44      val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
   13.45 -    fun Collect_tac set_natural' =
   13.46 +    fun Collect_tac set_map' =
   13.47        CONJ_WRAP' (fn thm =>
   13.48          FIRST' [rtac subset_UNIV,
   13.49            (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
   13.50 -            etac @{thm image_mono}, atac])]) set_natural';
   13.51 -    fun mor_tac (set_natural', ((morE, map_comp_id), map_cong0L)) =
   13.52 +            etac @{thm image_mono}, atac])]) set_map';
   13.53 +    fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) =
   13.54        EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
   13.55           REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
   13.56 -         etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_natural',
   13.57 -         rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural',
   13.58 +         etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map',
   13.59 +         rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map',
   13.60           rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
   13.61           REPEAT_DETERM_N (length morEs) o
   13.62             (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
   13.63 @@ -161,8 +161,8 @@
   13.64      dtac (alg_def RS iffD1) THEN'
   13.65      REPEAT o etac conjE THEN'
   13.66      rtac conjI THEN'
   13.67 -    CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
   13.68 -    CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
   13.69 +    CONJ_WRAP' (K fbetw_tac) set_map's THEN'
   13.70 +    CONJ_WRAP' mor_tac (set_map's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
   13.71    end;
   13.72  
   13.73  fun mk_mor_str_tac ks mor_def =
   13.74 @@ -208,7 +208,7 @@
   13.75      (rtac iffI THEN' if_tac THEN' only_if_tac) 1
   13.76    end;
   13.77  
   13.78 -fun mk_copy_str_tac set_natural's alg_def alg_sets =
   13.79 +fun mk_copy_str_tac set_map's alg_def alg_sets =
   13.80    let
   13.81      val n = length alg_sets;
   13.82      val bij_betw_inv_tac =
   13.83 @@ -222,13 +222,13 @@
   13.84          EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
   13.85            rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
   13.86            REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
   13.87 -      (set_natural's ~~ alg_sets);
   13.88 +      (set_map's ~~ alg_sets);
   13.89    in
   13.90      (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
   13.91      stac alg_def THEN' copy_str_tac) 1
   13.92    end;
   13.93  
   13.94 -fun mk_copy_alg_tac set_natural's alg_sets mor_def iso_alt copy_str =
   13.95 +fun mk_copy_alg_tac set_map's alg_sets mor_def iso_alt copy_str =
   13.96    let
   13.97      val n = length alg_sets;
   13.98      val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
   13.99 @@ -240,7 +240,7 @@
  13.100        CONJ_WRAP' (fn (thms, thm) =>
  13.101          EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
  13.102            REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
  13.103 -      (set_natural's ~~ alg_sets);
  13.104 +      (set_map's ~~ alg_sets);
  13.105    in
  13.106      (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) THEN'
  13.107      etac copy_str THEN' REPEAT_DETERM o atac THEN'
  13.108 @@ -389,24 +389,24 @@
  13.109    unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
  13.110  
  13.111  fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
  13.112 -    alg_sets set_natural's str_init_defs =
  13.113 +    alg_sets set_map's str_init_defs =
  13.114    let
  13.115      val n = length alg_sets;
  13.116      val fbetw_tac =
  13.117        CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm rev_bspec}, etac CollectE, atac])) alg_sets;
  13.118      val mor_tac =
  13.119        CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
  13.120 -    fun alg_epi_tac ((alg_set, str_init_def), set_natural') =
  13.121 +    fun alg_epi_tac ((alg_set, str_init_def), set_map') =
  13.122        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
  13.123          rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
  13.124          REPEAT_DETERM o FIRST' [rtac subset_UNIV,
  13.125 -          EVERY' [rtac ord_eq_le_trans, resolve_tac set_natural', rtac subset_trans,
  13.126 +          EVERY' [rtac ord_eq_le_trans, resolve_tac set_map', rtac subset_trans,
  13.127              etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
  13.128    in
  13.129      (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN'
  13.130      rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
  13.131      stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
  13.132 -    stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_natural's)) 1
  13.133 +    stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_map's)) 1
  13.134    end;
  13.135  
  13.136  fun mk_init_ex_mor_tac Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
  13.137 @@ -532,21 +532,21 @@
  13.138      (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
  13.139    etac fold_unique_mor 1;
  13.140  
  13.141 -fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
  13.142 +fun mk_ctor_induct_tac m set_map'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
  13.143    let
  13.144 -    val n = length set_natural'ss;
  13.145 +    val n = length set_map'ss;
  13.146      val ks = 1 upto n;
  13.147  
  13.148 -    fun mk_IH_tac Rep_inv Abs_inv set_natural' =
  13.149 +    fun mk_IH_tac Rep_inv Abs_inv set_map' =
  13.150        DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
  13.151 -        dtac set_rev_mp, rtac equalityD1, rtac set_natural', etac imageE,
  13.152 +        dtac set_rev_mp, rtac equalityD1, rtac set_map', etac imageE,
  13.153          hyp_subst_tac, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
  13.154  
  13.155 -    fun mk_closed_tac (k, (morE, set_natural's)) =
  13.156 +    fun mk_closed_tac (k, (morE, set_map's)) =
  13.157        EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
  13.158          rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac,
  13.159          REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
  13.160 -        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's)), atac];
  13.161 +        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_map's)), atac];
  13.162  
  13.163      fun mk_induct_tac (Rep, Rep_inv) =
  13.164        EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))];
  13.165 @@ -554,7 +554,7 @@
  13.166      (rtac mp THEN' rtac impI THEN'
  13.167      DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
  13.168      rtac init_induct THEN'
  13.169 -    DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_natural'ss))) 1
  13.170 +    DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_map'ss))) 1
  13.171    end;
  13.172  
  13.173  fun mk_ctor_induct2_tac cTs cts ctor_induct weak_ctor_inducts {context = ctxt, prems = _} =
  13.174 @@ -599,19 +599,19 @@
  13.175  fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
  13.176    rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
  13.177  
  13.178 -fun mk_ctor_set_tac set set_natural' set_natural's =
  13.179 +fun mk_ctor_set_tac set set_map' set_map's =
  13.180    let
  13.181 -    val n = length set_natural's;
  13.182 +    val n = length set_map's;
  13.183      fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
  13.184        rtac @{thm Union_image_eq};
  13.185    in
  13.186      EVERY' [rtac (set RS @{thm pointfreeE} RS trans), rtac @{thm Un_cong},
  13.187 -      rtac (trans OF [set_natural', trans_fun_cong_image_id_id_apply]),
  13.188 +      rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]),
  13.189        REPEAT_DETERM_N (n - 1) o rtac @{thm Un_cong},
  13.190 -      EVERY' (map mk_UN set_natural's)] 1
  13.191 +      EVERY' (map mk_UN set_map's)] 1
  13.192    end;
  13.193  
  13.194 -fun mk_set_nat_tac m induct_tac set_natural'ss
  13.195 +fun mk_set_nat_tac m induct_tac set_map'ss
  13.196      ctor_maps csets ctor_sets i {context = ctxt, prems = _} =
  13.197    let
  13.198      val n = length ctor_maps;
  13.199 @@ -628,7 +628,7 @@
  13.200          REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
  13.201          EVERY' (map useIH (drop m set_nats))];
  13.202    in
  13.203 -    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_natural'ss)) 1
  13.204 +    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1
  13.205    end;
  13.206  
  13.207  fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} =
  13.208 @@ -747,7 +747,7 @@
  13.209      (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1
  13.210    end;
  13.211  
  13.212 -fun mk_set_natural_tac set_nat =
  13.213 +fun mk_set_map_tac set_nat =
  13.214    EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
  13.215  
  13.216  fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg =
  13.217 @@ -776,31 +776,31 @@
  13.218              REPEAT_DETERM_N n o etac UnE]))))] 1);
  13.219  
  13.220  fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
  13.221 -  ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
  13.222 +  ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
  13.223    let
  13.224      val m = length ctor_set_incls;
  13.225      val n = length ctor_set_set_inclss;
  13.226  
  13.227 -    val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
  13.228 +    val (passive_set_maps, active_set_maps) = chop m set_maps;
  13.229      val in_Isrel = nth in_Isrels (i - 1);
  13.230      val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
  13.231      val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
  13.232      val if_tac =
  13.233        EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  13.234          rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  13.235 -        EVERY' (map2 (fn set_natural => fn ctor_set_incl =>
  13.236 -          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
  13.237 +        EVERY' (map2 (fn set_map => fn ctor_set_incl =>
  13.238 +          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
  13.239              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
  13.240              rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
  13.241 -        passive_set_naturals ctor_set_incls),
  13.242 -        CONJ_WRAP' (fn (in_Isrel, (set_natural, ctor_set_set_incls)) =>
  13.243 -          EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
  13.244 +        passive_set_maps ctor_set_incls),
  13.245 +        CONJ_WRAP' (fn (in_Isrel, (set_map, ctor_set_set_incls)) =>
  13.246 +          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
  13.247              rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  13.248              CONJ_WRAP' (fn thm =>
  13.249                EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
  13.250              ctor_set_set_incls,
  13.251              rtac conjI, rtac refl, rtac refl])
  13.252 -        (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
  13.253 +        (in_Isrels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
  13.254          CONJ_WRAP' (fn conv =>
  13.255            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
  13.256            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
  13.257 @@ -811,20 +811,20 @@
  13.258      val only_if_tac =
  13.259        EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
  13.260          rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
  13.261 -        CONJ_WRAP' (fn (ctor_set, passive_set_natural) =>
  13.262 +        CONJ_WRAP' (fn (ctor_set, passive_set_map) =>
  13.263            EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
  13.264              rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
  13.265 -            rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
  13.266 +            rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac,
  13.267              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
  13.268 -              (fn (active_set_natural, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
  13.269 -                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
  13.270 +              (fn (active_set_map, in_Isrel) => EVERY' [rtac ord_eq_le_trans,
  13.271 +                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least},
  13.272                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
  13.273                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
  13.274                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
  13.275                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
  13.276                  hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
  13.277 -            (rev (active_set_naturals ~~ in_Isrels))])
  13.278 -        (ctor_sets ~~ passive_set_naturals),
  13.279 +            (rev (active_set_maps ~~ in_Isrels))])
  13.280 +        (ctor_sets ~~ passive_set_maps),
  13.281          rtac conjI,
  13.282          REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
  13.283            rtac trans, rtac map_comp, rtac trans, rtac map_cong0,