# HG changeset patch
# User blanchet
# Date 1367321671 -7200
# Node ID 4d6dcd51dd52378772b6b4024e320529979373a9
# Parent  56523caf372fcf480ca17b4f62c58dc370ce7136
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)

diff -r 56523caf372f -r 4d6dcd51dd52 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Apr 30 13:23:52 2013 +0200
+++ b/etc/isar-keywords.el	Tue Apr 30 13:34:31 2013 +0200
@@ -31,7 +31,7 @@
     "ax_specification"
     "axiomatization"
     "back"
-    "bnf_def"
+    "bnf"
     "boogie_end"
     "boogie_open"
     "boogie_status"
@@ -583,7 +583,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
-    "bnf_def"
+    "bnf"
     "boogie_vc"
     "code_pred"
     "corollary"
diff -r 56523caf372f -r 4d6dcd51dd52 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:23:52 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:34:31 2013 +0200
@@ -11,7 +11,7 @@
 imports BNF_Util
 keywords
   "print_bnfs" :: diag and
-  "bnf_def" :: thy_goal
+  "bnf" :: thy_goal
 begin
 
 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
diff -r 56523caf372f -r 4d6dcd51dd52 src/HOL/BNF/Basic_BNFs.thy
--- a/src/HOL/BNF/Basic_BNFs.thy	Tue Apr 30 13:23:52 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Apr 30 13:34:31 2013 +0200
@@ -27,7 +27,7 @@
 lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
   unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
 
-bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
+bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
   "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
 apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
@@ -45,7 +45,7 @@
 apply (rule natLeq_Card_order)
 done
 
-bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
+bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
   "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
 apply (auto simp add: wpull_Gr_def Gr_def
   card_order_csum natLeq_card_order card_of_card_order_on
@@ -74,7 +74,7 @@
  (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
           | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
 
-bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
+bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
 proof -
   show "sum_map id id = id" by (rule sum_map.id)
 next
@@ -213,7 +213,7 @@
 definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where
 "prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)"
 
-bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
+bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
 proof (unfold prod_set_defs)
   show "map_pair id id = id" by (rule map_pair.id)
 next
@@ -327,7 +327,7 @@
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
 
-bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
+bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
   "fun_rel op ="
 proof
   fix f show "id \<circ> f = id f" by simp
diff -r 56523caf372f -r 4d6dcd51dd52 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:23:52 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:34:31 2013 +0200
@@ -22,7 +22,7 @@
 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
@@ -200,7 +200,7 @@
     (\<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
@@ -327,7 +327,7 @@
      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
@@ -447,7 +447,7 @@
   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
@@ -1075,7 +1075,7 @@
 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)
diff -r 56523caf372f -r 4d6dcd51dd52 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:23:52 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:34:31 2013 +0200
@@ -1285,7 +1285,7 @@
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
   end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
 
-val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
+val bnf_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
   Proof.unfolding ([[(defs, [])]])
     (Proof.theorem NONE (snd o register_bnf key oo after_qed)
       (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
@@ -1318,14 +1318,16 @@
   end;
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_bnfs"} "print all BNFs"
+  Outer_Syntax.improper_command @{command_spec "print_bnfs"}
+    "print all BNFs (bounded natural functors)"
     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
+  Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
+    "register a type as a BNF (bounded natural functor)"
     ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
-       >> bnf_def_cmd);
+       >> bnf_cmd);
 
 end;