renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
authorblanchet
Tue Apr 30 13:34:31 2013 +0200 (2013-04-30)
changeset 518364d6dcd51dd52
parent 51835 56523caf372f
child 51837 087498724486
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
etc/isar-keywords.el
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/Basic_BNFs.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/BNF/Tools/bnf_def.ML
     1.1 --- a/etc/isar-keywords.el	Tue Apr 30 13:23:52 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Tue Apr 30 13:34:31 2013 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4      "ax_specification"
     1.5      "axiomatization"
     1.6      "back"
     1.7 -    "bnf_def"
     1.8 +    "bnf"
     1.9      "boogie_end"
    1.10      "boogie_open"
    1.11      "boogie_status"
    1.12 @@ -583,7 +583,7 @@
    1.13  
    1.14  (defconst isar-keywords-theory-goal
    1.15    '("ax_specification"
    1.16 -    "bnf_def"
    1.17 +    "bnf"
    1.18      "boogie_vc"
    1.19      "code_pred"
    1.20      "corollary"
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:23:52 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Tue Apr 30 13:34:31 2013 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  imports BNF_Util
     2.5  keywords
     2.6    "print_bnfs" :: diag and
     2.7 -  "bnf_def" :: thy_goal
     2.8 +  "bnf" :: thy_goal
     2.9  begin
    2.10  
    2.11  lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
     3.1 --- a/src/HOL/BNF/Basic_BNFs.thy	Tue Apr 30 13:23:52 2013 +0200
     3.2 +++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Apr 30 13:34:31 2013 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4  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"
     3.5    unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
     3.6  
     3.7 -bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
     3.8 +bnf ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
     3.9    "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x"
    3.10  apply (auto simp: Gr_def fun_eq_iff natLeq_card_order natLeq_cinfinite)
    3.11  apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    3.12 @@ -45,7 +45,7 @@
    3.13  apply (rule natLeq_Card_order)
    3.14  done
    3.15  
    3.16 -bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    3.17 +bnf DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
    3.18    "op =::'a \<Rightarrow> 'a \<Rightarrow> bool"
    3.19  apply (auto simp add: wpull_Gr_def Gr_def
    3.20    card_order_csum natLeq_card_order card_of_card_order_on
    3.21 @@ -74,7 +74,7 @@
    3.22   (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
    3.23            | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
    3.24  
    3.25 -bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
    3.26 +bnf sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel
    3.27  proof -
    3.28    show "sum_map id id = id" by (rule sum_map.id)
    3.29  next
    3.30 @@ -213,7 +213,7 @@
    3.31  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
    3.32  "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)"
    3.33  
    3.34 -bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
    3.35 +bnf map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel
    3.36  proof (unfold prod_set_defs)
    3.37    show "map_pair id id = id" by (rule map_pair.id)
    3.38  next
    3.39 @@ -327,7 +327,7 @@
    3.40    ultimately show ?thesis using card_of_ordLeq by fast
    3.41  qed
    3.42  
    3.43 -bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
    3.44 +bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"]
    3.45    "fun_rel op ="
    3.46  proof
    3.47    fix f show "id \<circ> f = id f" by simp
     4.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:23:52 2013 +0200
     4.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Apr 30 13:34:31 2013 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  lemma option_rec_conv_option_case: "option_rec = option_case"
     4.5  by (simp add: fun_eq_iff split: option.split)
     4.6  
     4.7 -bnf_def Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
     4.8 +bnf Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"] option_rel
     4.9  proof -
    4.10    show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
    4.11  next
    4.12 @@ -200,7 +200,7 @@
    4.13      (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
    4.14  qed
    4.15  
    4.16 -bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    4.17 +bnf map [set] "\<lambda>_::'a list. natLeq" ["[]"]
    4.18  proof -
    4.19    show "map id = id" by (rule List.map.id)
    4.20  next
    4.21 @@ -327,7 +327,7 @@
    4.22       using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, simp)+
    4.23  qed
    4.24  
    4.25 -bnf_def fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
    4.26 +bnf fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
    4.27  apply -
    4.28            apply transfer' apply simp
    4.29           apply transfer' apply simp
    4.30 @@ -447,7 +447,7 @@
    4.31    by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range)
    4.32  qed
    4.33  
    4.34 -bnf_def cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
    4.35 +bnf cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] cset_rel
    4.36  proof -
    4.37    show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
    4.38  next
    4.39 @@ -1075,7 +1075,7 @@
    4.40  definition multiset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
    4.41  "multiset_map h = Abs_multiset \<circ> mmap h \<circ> count"
    4.42  
    4.43 -bnf_def multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    4.44 +bnf multiset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
    4.45  unfolding multiset_map_def
    4.46  proof -
    4.47    show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
     5.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:23:52 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:34:31 2013 +0200
     5.3 @@ -1285,7 +1285,7 @@
     5.4      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
     5.5    end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
     5.6  
     5.7 -val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
     5.8 +val bnf_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
     5.9    Proof.unfolding ([[(defs, [])]])
    5.10      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    5.11        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    5.12 @@ -1318,14 +1318,16 @@
    5.13    end;
    5.14  
    5.15  val _ =
    5.16 -  Outer_Syntax.improper_command @{command_spec "print_bnfs"} "print all BNFs"
    5.17 +  Outer_Syntax.improper_command @{command_spec "print_bnfs"}
    5.18 +    "print all BNFs (bounded natural functors)"
    5.19      (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
    5.20  
    5.21  val _ =
    5.22 -  Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
    5.23 +  Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
    5.24 +    "register a type as a BNF (bounded natural functor)"
    5.25      ((parse_opt_binding_colon -- Parse.term --
    5.26         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
    5.27         (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)
    5.28 -       >> bnf_def_cmd);
    5.29 +       >> bnf_cmd);
    5.30  
    5.31  end;