src/HOL/BNF/More_BNFs.thy

 begin
 
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
-bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
+bnf Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
 proof -
   show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
 next
   fix f g
   show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"

   }
   thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
     (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
 qed
 
-bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
+bnf map [set] "\<lambda>_::'a list. natLeq" ["[]"]
 proof -
   show "map id = id" by (rule List.map.id)
 next
   fix f g
   show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])

   then obtain x where X'eq: "X' = fset x" by transfer (metis finite_list)
   show "\<exists>x. fset x \<subseteq> A \<and> fmap p1 x = y1 \<and> fmap p2 x = y2"
      using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, simp)+
 qed
 
-bnf_def fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
+bnf fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
 apply -
           apply transfer' apply simp
          apply transfer' apply simp
         apply transfer apply force
        apply transfer apply force

   apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing)
   apply (clarsimp)
   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
+bnf cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
 proof -
   show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
 next
   fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f"
   unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto

 qed
 
 definition multiset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
 "multiset_map h = Abs_multiset \<circ> mmap h \<circ> count"
 
-bnf_def multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
+bnf multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
 unfolding multiset_map_def
 proof -
   show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
 next
   fix f g