src/HOL/Codatatype/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 = Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
+bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
 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"

       apply (rule ordLeq_csum2)
       by (rule Card_order_ctwo)
   qed
 qed
 
-bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
+bnf_def 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])

 qed
 
 lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
 by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
 
-bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
+bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
 proof -
   show "map_fset id = id"
   unfolding map_fset_def2 map_id o_id afset_rfset_id ..
 next
   fix f g

     using csum_Cnotzero2 ctwo_Cnotzero apply blast
     by (rule natLeq_Card_order)
   finally show ?thesis .
 qed
 
-bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
+bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
 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 mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
 "mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
 
-bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
+bnf_def mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
 unfolding mset_map_def
 proof -
   show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
 next
   fix f g