src/HOL/BNF/More_BNFs.thy
changeset 51836 4d6dcd51dd52
parent 51782 84e7225f5ab6
child 51893 596baae88a88
     1.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:23:52 2013 +0200
     1.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:34:31 2013 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  lemma option_rec_conv_option_case: "option_rec = option_case"
     1.5  by (simp add: fun_eq_iff split: option.split)
     1.6  
     1.7 -bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
     1.8 +bnf Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
     1.9  proof -
    1.10    show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
    1.11  next
    1.12 @@ -200,7 +200,7 @@
    1.13      (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
    1.14  qed
    1.15  
    1.16 -bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    1.17 +bnf map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    1.18  proof -
    1.19    show "map id = id" by (rule List.map.id)
    1.20  next
    1.21 @@ -327,7 +327,7 @@
    1.22       using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, simp)+
    1.23  qed
    1.24  
    1.25 -bnf_def fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
    1.26 +bnf fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
    1.27  apply -
    1.28            apply transfer' apply simp
    1.29           apply transfer' apply simp
    1.30 @@ -447,7 +447,7 @@
    1.31    by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range)
    1.32  qed
    1.33  
    1.34 -bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
    1.35 +bnf cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
    1.36  proof -
    1.37    show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
    1.38  next
    1.39 @@ -1075,7 +1075,7 @@
    1.40  definition multiset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    1.41  "multiset_map h = Abs_multiset \<circ> mmap h \<circ> count"
    1.42  
    1.43 -bnf_def multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    1.44 +bnf multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    1.45  unfolding multiset_map_def
    1.46  proof -
    1.47    show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)