renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
authorblanchet
Mon Feb 17 13:31:42 2014 +0100 (2014-02-17)
changeset 555303dfb724db099
parent 55529 51998cb9d6b8
child 55531 601ca8efa000
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Examples/Lambda_Term.thy
src/HOL/BNF_Examples/ListF.thy
src/HOL/BNF_Examples/Misc_Primrec.thy
src/HOL/BNF_Examples/Stream_Processor.thy
src/HOL/BNF_LFP.thy
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
     1.6  Functions,'' describes how to specify recursive functions using
     1.7 -@{command primrec_new}, \keyw{fun}, and \keyw{function}.
     1.8 +@{command primrec}, \keyw{fun}, and \keyw{function}.
     1.9  
    1.10  \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
    1.11  describes how to specify codatatypes using the @{command codatatype} command.
    1.12 @@ -147,10 +147,9 @@
    1.13  \newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
    1.14  in.\allowbreak tum.\allowbreak de}}
    1.15  
    1.16 -The commands @{command datatype_new} and @{command primrec_new} are expected to
    1.17 -replace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
    1.18 -theories are encouraged to use the new commands, and maintainers of older
    1.19 -theories may want to consider upgrading.
    1.20 +The command @{command datatype_new} is expected to replace \keyw{datatype} in a
    1.21 +future release. Authors of new theories are encouraged to use the new commands,
    1.22 +and maintainers of older theories may want to consider upgrading.
    1.23  
    1.24  Comments and bug reports concerning either the tool or this tutorial should be
    1.25  directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
    1.26 @@ -979,13 +978,13 @@
    1.27  type of the recursor, used by \keyw{primrec}. Recursion through functions was
    1.28  handled specially. In the new package, nested recursion (for functions and
    1.29  non-functions) is handled in a more modular fashion. The old-style recursor can
    1.30 -be generated on demand using @{command primrec_new}, as explained in
    1.31 +be generated on demand using @{command primrec}, as explained in
    1.32  Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
    1.33  new-style datatypes.
    1.34  
    1.35  \item \emph{Accordingly, the induction rule is different for nested recursive
    1.36  datatypes.} Again, the old-style induction rule can be generated on demand using
    1.37 -@{command primrec_new}, as explained in
    1.38 +@{command primrec}, as explained in
    1.39  Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
    1.40  new-style datatypes.
    1.41  
    1.42 @@ -1025,11 +1024,11 @@
    1.43    \label{sec:defining-recursive-functions} *}
    1.44  
    1.45  text {*
    1.46 -Recursive functions over datatypes can be specified using the @{command
    1.47 -primrec_new} command, which supports primitive recursion, or using the more
    1.48 -general \keyw{fun} and \keyw{function} commands. Here, the focus is on @{command
    1.49 -primrec_new}; the other two commands are described in a separate tutorial
    1.50 -\cite{isabelle-function}.
    1.51 +Recursive functions over datatypes can be specified using the @{command primrec}
    1.52 +command, which supports primitive recursion, or using the more general
    1.53 +\keyw{fun} and \keyw{function} commands. Here, the focus is on
    1.54 +@{command primrec}; the other two commands are described in a separate
    1.55 +tutorial \cite{isabelle-function}.
    1.56  
    1.57  %%% TODO: partial_function
    1.58  *}
    1.59 @@ -1053,25 +1052,25 @@
    1.60  each equation. For example:
    1.61  *}
    1.62  
    1.63 -    primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
    1.64 +    primrec bool_of_trool :: "trool \<Rightarrow> bool" where
    1.65        "bool_of_trool Faalse \<longleftrightarrow> False" |
    1.66        "bool_of_trool Truue \<longleftrightarrow> True"
    1.67  
    1.68  text {* \blankline *}
    1.69  
    1.70 -    primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
    1.71 +    primrec the_list :: "'a option \<Rightarrow> 'a list" where
    1.72        "the_list None = []" |
    1.73        "the_list (Some a) = [a]"
    1.74  
    1.75  text {* \blankline *}
    1.76  
    1.77 -    primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
    1.78 +    primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
    1.79        "the_default d None = d" |
    1.80        "the_default _ (Some a) = a"
    1.81  
    1.82  text {* \blankline *}
    1.83  
    1.84 -    primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
    1.85 +    primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
    1.86        "mirrror (Triple a b c) = Triple c b a"
    1.87  
    1.88  text {*
    1.89 @@ -1091,13 +1090,13 @@
    1.90  allowed on the right-hand side:
    1.91  *}
    1.92  
    1.93 -    primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
    1.94 +    primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
    1.95        "replicate Zero _ = []" |
    1.96        "replicate (Suc n) x = x # replicate n x"
    1.97  
    1.98  text {* \blankline *}
    1.99  
   1.100 -    primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
   1.101 +    primrec at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
   1.102        "at (x # xs) j =
   1.103           (case j of
   1.104              Zero \<Rightarrow> x
   1.105 @@ -1105,7 +1104,7 @@
   1.106  
   1.107  text {* \blankline *}
   1.108  
   1.109 -    primrec_new (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
   1.110 +    primrec (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
   1.111        "tfold _ (TNil y) = y" |
   1.112        "tfold f (TCons x xs) = f x (tfold f xs)"
   1.113  
   1.114 @@ -1149,7 +1148,7 @@
   1.115  is straightforward:
   1.116  *}
   1.117  
   1.118 -    primrec_new
   1.119 +    primrec
   1.120        nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
   1.121        nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
   1.122      where
   1.123 @@ -1159,7 +1158,7 @@
   1.124  
   1.125  text {* \blankline *}
   1.126  
   1.127 -    primrec_new
   1.128 +    primrec
   1.129        eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
   1.130        eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
   1.131        eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
   1.132 @@ -1199,7 +1198,7 @@
   1.133  (*<*)
   1.134      datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
   1.135  (*>*)
   1.136 -    primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
   1.137 +    primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
   1.138        "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
   1.139           (case js of
   1.140              [] \<Rightarrow> a
   1.141 @@ -1212,7 +1211,7 @@
   1.142  map function @{const map_option}:
   1.143  *}
   1.144  
   1.145 -    primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
   1.146 +    primrec (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
   1.147        "sum_btree (BNode a lt rt) =
   1.148           a + the_default 0 (map_option sum_btree lt) +
   1.149             the_default 0 (map_option sum_btree rt)"
   1.150 @@ -1224,7 +1223,7 @@
   1.151  (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
   1.152  *}
   1.153  
   1.154 -    primrec_new (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.155 +    primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.156        "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
   1.157        "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
   1.158  
   1.159 @@ -1235,13 +1234,13 @@
   1.160  For example:
   1.161  *}
   1.162  
   1.163 -    primrec_new relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.164 +    primrec relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.165        "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
   1.166        "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
   1.167  
   1.168  text {* \blankline *}
   1.169  
   1.170 -    primrec_new subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.171 +    primrec subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   1.172        "subtree_ft x (FTNode g) = g x"
   1.173  
   1.174  text {*
   1.175 @@ -1255,19 +1254,19 @@
   1.176  
   1.177  text {* \blankline *}
   1.178  
   1.179 -    primrec_new (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.180 +    primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.181        "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
   1.182        "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
   1.183  
   1.184  text {* \blankline *}
   1.185  
   1.186 -    primrec_new relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.187 +    primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.188        "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
   1.189        "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
   1.190  
   1.191  text {* \blankline *}
   1.192  
   1.193 -    primrec_new subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.194 +    primrec subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
   1.195        "subtree_ft2 x y (FTNode2 g) = g x y"
   1.196  
   1.197  
   1.198 @@ -1285,7 +1284,7 @@
   1.199  datatypes. For example:
   1.200  *}
   1.201  
   1.202 -    primrec_new
   1.203 +    primrec
   1.204        at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
   1.205        ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
   1.206      where
   1.207 @@ -1310,7 +1309,7 @@
   1.208  Here is a second example:
   1.209  *}
   1.210  
   1.211 -    primrec_new
   1.212 +    primrec
   1.213        sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
   1.214        sum_btree_option :: "'a btree option \<Rightarrow> 'a"
   1.215      where
   1.216 @@ -1330,7 +1329,7 @@
   1.217  %
   1.218  %  * there's no hard-and-fast rule of when to use one or the other,
   1.219  %    just like there's no rule when to use fold and when to use
   1.220 -%    primrec_new
   1.221 +%    primrec
   1.222  %
   1.223  %  * higher-order approach, considering nesting as nesting, is more
   1.224  %    compositional -- e.g. we saw how we could reuse an existing polymorphic
   1.225 @@ -1361,11 +1360,11 @@
   1.226  
   1.227  text {*
   1.228  \begin{matharray}{rcl}
   1.229 -  @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
   1.230 +  @{command_def "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"}
   1.231  \end{matharray}
   1.232  
   1.233  @{rail \<open>
   1.234 -  @@{command primrec_new} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
   1.235 +  @@{command primrec} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
   1.236    ;
   1.237    @{syntax_def pr_equation}: thmdecl? prop
   1.238  \<close>}
   1.239 @@ -1373,8 +1372,8 @@
   1.240  \medskip
   1.241  
   1.242  \noindent
   1.243 -The @{command primrec_new} command introduces a set of mutually recursive
   1.244 -functions over datatypes.
   1.245 +The @{command primrec} command introduces a set of mutually recursive functions
   1.246 +over datatypes.
   1.247  
   1.248  The syntactic entity \synt{target} can be used to specify a local context,
   1.249  \synt{fixes} denotes a list of names with optional type signatures,
   1.250 @@ -1455,7 +1454,7 @@
   1.251      overloading
   1.252        termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
   1.253      begin
   1.254 -    primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
   1.255 +    primrec termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
   1.256        "termi\<^sub>0 (TNil y) = y" |
   1.257        "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
   1.258      end
   1.259 @@ -1470,9 +1469,10 @@
   1.260    \label{ssec:primrec-compatibility-issues} *}
   1.261  
   1.262  text {*
   1.263 -The command @{command primrec_new} has been designed to be highly compatible
   1.264 -with the old \keyw{primrec}, to ease migration. There is nonetheless at least
   1.265 -one incompatibility that may arise when porting to the new package:
   1.266 +The command @{command primrec}'s behavior on new-style datatypes has been
   1.267 +designed to be highly compatible with that for old-style datatypes, to ease
   1.268 +migration. There is nonetheless at least one incompatibility that may arise when
   1.269 +porting to the new package:
   1.270  
   1.271  \begin{itemize}
   1.272  \setlength{\itemsep}{0pt}
     2.1 --- a/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Feb 17 13:31:42 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Feb 17 13:31:42 2014 +0100
     2.3 @@ -23,13 +23,13 @@
     2.4  
     2.5  subsection {* Example: The set of all variables varsOf and free variables fvarsOf of a term *}
     2.6  
     2.7 -primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where
     2.8 +primrec varsOf :: "'a trm \<Rightarrow> 'a set" where
     2.9    "varsOf (Var a) = {a}"
    2.10  | "varsOf (App f x) = varsOf f \<union> varsOf x"
    2.11  | "varsOf (Lam x b) = {x} \<union> varsOf b"
    2.12  | "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})"
    2.13  
    2.14 -primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where
    2.15 +primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
    2.16    "fvarsOf (Var x) = {x}"
    2.17  | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
    2.18  | "fvarsOf (Lam x t) = fvarsOf t - {x}"
     3.1 --- a/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
     3.3 @@ -19,11 +19,11 @@
     3.4  definition Singll ("[[_]]") where
     3.5    [simp]: "Singll a \<equiv> Conss a NilF"
     3.6  
     3.7 -primrec_new appendd (infixr "@@" 65) where
     3.8 +primrec appendd (infixr "@@" 65) where
     3.9    "NilF @@ ys = ys"
    3.10  | "Conss x xs @@ ys = Conss x (xs @@ ys)"
    3.11  
    3.12 -primrec_new lrev where
    3.13 +primrec lrev where
    3.14    "lrev NilF = NilF"
    3.15  | "lrev (Conss y ys) = lrev ys @@ [[y]]"
    3.16  
    3.17 @@ -46,7 +46,7 @@
    3.18  lemma lrev_lrev[simp]: "lrev (lrev xs) = xs"
    3.19    by (induct xs) auto
    3.20  
    3.21 -primrec_new lengthh where
    3.22 +primrec lengthh where
    3.23    "lengthh NilF = 0"
    3.24  | "lengthh (Conss x xs) = Suc (lengthh xs)"
    3.25  
     4.1 --- a/src/HOL/BNF_Examples/Misc_Primrec.thy	Mon Feb 17 13:31:42 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Misc_Primrec.thy	Mon Feb 17 13:31:42 2014 +0100
     4.3 @@ -11,49 +11,49 @@
     4.4  imports Misc_Datatype
     4.5  begin
     4.6  
     4.7 -primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
     4.8 +primrec nat_of_simple :: "simple \<Rightarrow> nat" where
     4.9    "nat_of_simple X1 = 1" |
    4.10    "nat_of_simple X2 = 2" |
    4.11    "nat_of_simple X3 = 3" |
    4.12    "nat_of_simple X4 = 4"
    4.13  
    4.14 -primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where
    4.15 +primrec simple_of_simple' :: "simple' \<Rightarrow> simple" where
    4.16    "simple_of_simple' (X1' _) = X1" |
    4.17    "simple_of_simple' (X2' _) = X2" |
    4.18    "simple_of_simple' (X3' _) = X3" |
    4.19    "simple_of_simple' (X4' _) = X4"
    4.20  
    4.21 -primrec_new inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
    4.22 +primrec inc_simple'' :: "nat \<Rightarrow> simple'' \<Rightarrow> simple''" where
    4.23    "inc_simple'' k (X1'' n i) = X1'' (n + k) (i + int k)" |
    4.24    "inc_simple'' _ X2'' = X2''"
    4.25  
    4.26 -primrec_new myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
    4.27 +primrec myapp :: "'a mylist \<Rightarrow> 'a mylist \<Rightarrow> 'a mylist" where
    4.28    "myapp MyNil ys = ys" |
    4.29    "myapp (MyCons x xs) ys = MyCons x (myapp xs ys)"
    4.30  
    4.31 -primrec_new myrev :: "'a mylist \<Rightarrow> 'a mylist" where
    4.32 +primrec myrev :: "'a mylist \<Rightarrow> 'a mylist" where
    4.33    "myrev MyNil = MyNil" |
    4.34    "myrev (MyCons x xs) = myapp (myrev xs) (MyCons x MyNil)"
    4.35  
    4.36 -primrec_new shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
    4.37 +primrec shuffle_sp :: "('a, 'b, 'c, 'd) some_passive \<Rightarrow> ('d, 'a, 'b, 'c) some_passive" where
    4.38    "shuffle_sp (SP1 sp) = SP1 (shuffle_sp sp)" |
    4.39    "shuffle_sp (SP2 a) = SP3 a" |
    4.40    "shuffle_sp (SP3 b) = SP4 b" |
    4.41    "shuffle_sp (SP4 c) = SP5 c" |
    4.42    "shuffle_sp (SP5 d) = SP2 d"
    4.43  
    4.44 -primrec_new
    4.45 +primrec
    4.46    hf_size :: "hfset \<Rightarrow> nat"
    4.47  where
    4.48    "hf_size (HFset X) = 1 + setsum id (fset (fimage hf_size X))"
    4.49  
    4.50 -primrec_new rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
    4.51 +primrec rename_lam :: "(string \<Rightarrow> string) \<Rightarrow> lambda \<Rightarrow> lambda" where
    4.52    "rename_lam f (Var s) = Var (f s)" |
    4.53    "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
    4.54    "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
    4.55    "rename_lam f (Let SL l) = Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l)"
    4.56  
    4.57 -primrec_new
    4.58 +primrec
    4.59    sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
    4.60    sum_i2 :: "'a I2 \<Rightarrow> 'a"
    4.61  where
    4.62 @@ -62,18 +62,18 @@
    4.63    "sum_i2 I21 = 0" |
    4.64    "sum_i2 (I22 i j) = sum_i1 i + sum_i2 j"
    4.65  
    4.66 -primrec_new forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
    4.67 +primrec forest_of_mylist :: "'a tree mylist \<Rightarrow> 'a forest" where
    4.68    "forest_of_mylist MyNil = FNil" |
    4.69    "forest_of_mylist (MyCons t ts) = FCons t (forest_of_mylist ts)"
    4.70  
    4.71 -primrec_new mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
    4.72 +primrec mylist_of_forest :: "'a forest \<Rightarrow> 'a tree mylist" where
    4.73    "mylist_of_forest FNil = MyNil" |
    4.74    "mylist_of_forest (FCons t ts) = MyCons t (mylist_of_forest ts)"
    4.75  
    4.76  definition frev :: "'a forest \<Rightarrow> 'a forest" where
    4.77    "frev = forest_of_mylist \<circ> myrev \<circ> mylist_of_forest"
    4.78  
    4.79 -primrec_new
    4.80 +primrec
    4.81    mirror_tree :: "'a tree \<Rightarrow> 'a tree" and
    4.82    mirror_forest :: "'a forest \<Rightarrow> 'a forest"
    4.83  where
    4.84 @@ -82,7 +82,7 @@
    4.85    "mirror_forest FNil = FNil" |
    4.86    "mirror_forest (FCons t ts) = frev (FCons (mirror_tree t) (mirror_forest ts))"
    4.87  
    4.88 -primrec_new
    4.89 +primrec
    4.90    mylist_of_tree' :: "'a tree' \<Rightarrow> 'a mylist" and
    4.91    mylist_of_branch :: "'a branch \<Rightarrow> 'a mylist"
    4.92  where
    4.93 @@ -90,7 +90,7 @@
    4.94    "mylist_of_tree' (TNode' b b') = myapp (mylist_of_branch b) (mylist_of_branch b')" |
    4.95    "mylist_of_branch (Branch x t) = MyCons x (mylist_of_tree' t)"
    4.96  
    4.97 -primrec_new
    4.98 +primrec
    4.99    id_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
   4.100    id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
   4.101    id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
   4.102 @@ -101,7 +101,7 @@
   4.103    "id_trees2 MyNil = MyNil" |
   4.104    "id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)"
   4.105  
   4.106 -primrec_new
   4.107 +primrec
   4.108    is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
   4.109    is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
   4.110    is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"
   4.111 @@ -114,11 +114,11 @@
   4.112    "is_ground_factor (V _) \<longleftrightarrow> False" |
   4.113    "is_ground_factor (Paren e) \<longleftrightarrow> is_ground_exp e"
   4.114  
   4.115 -primrec_new map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   4.116 +primrec map_ftreeA :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
   4.117    "map_ftreeA f (FTLeaf x) = FTLeaf (f x)" |
   4.118    "map_ftreeA f (FTNode g) = FTNode (map_ftreeA f \<circ> g)"
   4.119  
   4.120 -primrec_new map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
   4.121 +primrec map_ftreeB :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ftree \<Rightarrow> 'b ftree" where
   4.122    "map_ftreeB f (FTLeaf x) = FTLeaf (f x)" |
   4.123    "map_ftreeB f (FTNode g) = FTNode (map_ftreeB f \<circ> g \<circ> the_inv f)"
   4.124  
     5.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Feb 17 13:31:42 2014 +0100
     5.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Feb 17 13:31:42 2014 +0100
     5.3 @@ -17,7 +17,7 @@
     5.4  datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
     5.5  codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
     5.6  
     5.7 -primrec_new run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
     5.8 +primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
     5.9    "run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
    5.10  | "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)"
    5.11  
    5.12 @@ -81,13 +81,13 @@
    5.13    qed
    5.14  qed
    5.15  
    5.16 -text {* Alternative definition of composition using primrec_new instead of function *}
    5.17 +text {* Alternative definition of composition using primrec instead of function *}
    5.18  
    5.19 -primrec_new sp\<^sub>\<mu>_comp2R  where
    5.20 +primrec sp\<^sub>\<mu>_comp2R  where
    5.21    "sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)"
    5.22  | "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)"
    5.23  
    5.24 -primrec_new sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
    5.25 +primrec sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
    5.26    "Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)"
    5.27  | "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp"
    5.28  
    5.29 @@ -177,7 +177,7 @@
    5.30  
    5.31  (* Definition of run for an arbitrary final coalgebra as codomain: *)
    5.32  
    5.33 -primrec_new
    5.34 +primrec
    5.35    runF\<^sub>\<mu> :: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> (('b, ('a, 'b) spF\<^sub>\<nu>) F) \<times> 'a stream" 
    5.36  where
    5.37    "runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)"
     6.1 --- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     6.2 +++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     6.3 @@ -13,8 +13,7 @@
     6.4  imports BNF_FP_Base
     6.5  keywords
     6.6    "datatype_new" :: thy_decl and
     6.7 -  "datatype_new_compat" :: thy_decl and
     6.8 -  "primrec_new" :: thy_decl
     6.9 +  "datatype_new_compat" :: thy_decl
    6.10  begin
    6.11  
    6.12  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
     7.3 @@ -355,7 +355,7 @@
     7.4        end;
     7.5  
     7.6      (* These results are half broken. This is deliberate. We care only about those fields that are
     7.7 -       used by "primrec_new", "primcorecursive", and "datatype_new_compat". *)
     7.8 +       used by "primrec", "primcorecursive", and "datatype_new_compat". *)
     7.9      val fp_res =
    7.10        ({Ts = fpTs,
    7.11          bnfs = steal #bnfs,
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     8.3 @@ -560,9 +560,9 @@
     8.4    end
     8.5    handle PRIMREC (str, eqns) =>
     8.6           if null eqns then
     8.7 -           error ("primrec_new error:\n  " ^ str)
     8.8 +           error ("primrec error:\n  " ^ str)
     8.9           else
    8.10 -           error ("primrec_new error:\n  " ^ str ^ "\nin\n  " ^
    8.11 +           error ("primrec error:\n  " ^ str ^ "\nin\n  " ^
    8.12               space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
    8.13  
    8.14  fun gen_primrec old_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec
    8.15 @@ -612,7 +612,7 @@
    8.16      val simpss' = burrow (Proof_Context.export lthy' lthy) simpss;
    8.17    in ((ts, simpss'), Local_Theory.exit_global lthy') end;
    8.18  
    8.19 -val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"}
    8.20 +val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
    8.21    "define primitive recursive functions"
    8.22    (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd));
    8.23