renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
--- 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> {}"
--- 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 *}
--- 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 {*
--- 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 *}
--- 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
-
--- 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:
--- 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));
--- 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"