# HG changeset patch
# User blanchet
# Date 1392640302 -3600
# Node ID b18bdcbda41b8f5de7396ce7d63c9f205244e74f
# Parent  6260caf1d6126452c2a1d39dd70addb1a58dca77
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)

diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -13,7 +13,8 @@
 imports BNF_FP_Base
 keywords
   "datatype_new" :: thy_decl and
-  "datatype_compat" :: thy_decl
+  "datatype_compat" :: thy_decl and
+  "primrec" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Inductive.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -11,7 +11,7 @@
   "inductive_cases" "inductive_simps" :: thy_script and "monos" and
   "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
-  "primrec" :: thy_decl
+  "old_primrec" :: thy_decl
 begin
 
 subsection {* Least and greatest fixed points *}
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Main.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_LFP BNF_GFP
+imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_GFP
 begin
 
 text {*
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -187,7 +187,7 @@
 instantiation nat :: comm_monoid_diff
 begin
 
-primrec plus_nat where
+old_primrec plus_nat where
   add_0:      "0 + n = (n\<Colon>nat)"
 | add_Suc:  "Suc m + n = Suc (m + n)"
 
@@ -202,7 +202,7 @@
 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   by simp
 
-primrec minus_nat where
+old_primrec minus_nat where
   diff_0 [code]: "m - 0 = (m\<Colon>nat)"
 | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
 
@@ -235,7 +235,7 @@
 definition
   One_nat_def [simp]: "1 = Suc 0"
 
-primrec times_nat where
+old_primrec times_nat where
   mult_0:     "0 * n = (0\<Colon>nat)"
 | mult_Suc: "Suc m * n = n + (m * n)"
 
@@ -414,7 +414,7 @@
 instantiation nat :: linorder
 begin
 
-primrec less_eq_nat where
+old_primrec less_eq_nat where
   "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
 | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
 
@@ -1303,7 +1303,7 @@
   funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
 begin
 
-primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+old_primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   "funpow 0 f = id"
 | "funpow (Suc n) f = f o funpow n f"
 
@@ -1410,7 +1410,7 @@
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: add_ac distrib_right)
 
-primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+old_primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   "of_nat_aux inc 0 i = i"
 | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
 
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Num.thy
--- a/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -6,7 +6,7 @@
 header {* Binary Numerals *}
 
 theory Num
-imports Datatype
+imports Datatype BNF_LFP
 begin
 
 subsection {* The @{text num} type *}
@@ -1249,4 +1249,3 @@
   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -120,7 +120,7 @@
 
 setup {* Sign.parent_path *}
 
-primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+old_primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
@@ -177,10 +177,10 @@
   qed
 qed
 
-primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+old_primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   "Suml f (Inl x) = f x"
 
-primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+old_primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   "Sumr f (Inr x) = f x"
 
 lemma Suml_inject:
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Tools/Datatype/primrec.ML
--- a/src/HOL/Tools/Datatype/primrec.ML	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/Datatype/primrec.ML	Mon Feb 17 13:31:42 2014 +0100
@@ -312,7 +312,7 @@
 (* outer syntax *)
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "primrec"}
+  Outer_Syntax.local_theory @{command_spec "old_primrec"}
     "define primitive recursive functions on datatypes"
     (Parse.fixes -- Parse_Spec.where_alt_specs
       >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));
diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -716,11 +716,11 @@
   relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
 begin
 
-primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+old_primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     "relpow 0 R = Id"
   | "relpow (Suc n) R = (R ^^ n) O R"
 
-primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
+old_primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
     "relpowp 0 R = HOL.eq"
   | "relpowp (Suc n) R = (R ^^ n) OO R"