src/HOL/BNF/More_BNFs.thy

   apply (erule wpull_fmap)
  apply (simp add: Gr_def relcomp_unfold converse_unfold fset_rel_def fset_rel_aux) 
 apply transfer apply simp
 done
 
-lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
+lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map'
 
 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   unfolding fset_rel_def set_rel_def by auto 
 
 (* Countable sets *)

 
 lemma Collect_Int_Times:
 "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
 by auto
 
-lemma rcset_natural': "rcset (cIm f x) = f ` rcset x"
+lemma rcset_map': "rcset (cIm f x) = f ` rcset x"
 unfolding cIm_def[abs_def] by simp
 
 definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
 "cset_rel R a b \<longleftrightarrow>
  (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>

   qed (auto simp add: *)
 next
   assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
   apply (simp add: subset_eq Ball_def)
   apply (rule conjI)
-  apply (clarsimp, metis (lifting, no_types) rcset_natural' image_iff surjective_pairing)
+  apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing)
   apply (clarsimp)
-  by (metis Domain.intros Range.simps rcset_natural' fst_eq_Domain snd_eq_Range)
+  by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range)
 qed
 
 bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
 proof -
   show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto

 Zero: "multiset_rel' R {#} {#}"
 |
 Plus: "\<lbrakk>R a b; multiset_rel' R M N\<rbrakk> \<Longrightarrow> multiset_rel' R (M + {#a#}) (N + {#b#})"
 
 lemma multiset_map_Zero_iff[simp]: "multiset_map f M = {#} \<longleftrightarrow> M = {#}"
-by (metis image_is_empty multiset.set_natural' set_of_eq_empty_iff)
+by (metis image_is_empty multiset.set_map' set_of_eq_empty_iff)
 
 lemma multiset_map_Zero[simp]: "multiset_map f {#} = {#}" by simp
 
 lemma multiset_rel_Zero: "multiset_rel R {#} {#}"
 unfolding multiset_rel_def Gr_def relcomp_unfold by auto

 lemma msed_map_invL:
 assumes "multiset_map f (M + {#a#}) = N"
 shows "\<exists> N1. N = N1 + {#f a#} \<and> multiset_map f M = N1"
 proof-
   have "f a \<in># N"
-  using assms multiset.set_natural'[of f "M + {#a#}"] by auto
+  using assms multiset.set_map'[of f "M + {#a#}"] by auto
   then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
   have "multiset_map f M = N1" using assms unfolding N by simp
   thus ?thesis using N by blast
 qed
 
 lemma msed_map_invR:
 assumes "multiset_map f M = N + {#b#}"
 shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> multiset_map f M1 = N"
 proof-
   obtain a where a: "a \<in># M" and fa: "f a = b"
-  using multiset.set_natural'[of f M] unfolding assms
+  using multiset.set_map'[of f M] unfolding assms
   by (metis image_iff mem_set_of_iff union_single_eq_member)
   then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
   have "multiset_map f M1 = N" using assms unfolding M fa[symmetric] by simp
   thus ?thesis using M fa by blast
 qed