renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
authorblanchet
Mon Feb 17 13:31:42 2014 +0100 (2014-02-17)
changeset 55534b18bdcbda41b
parent 55533 6260caf1d612
child 55535 10194808430d
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
src/HOL/BNF_LFP.thy
src/HOL/Inductive.thy
src/HOL/Main.thy
src/HOL/Nat.thy
src/HOL/Num.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Datatype/primrec.ML
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -13,7 +13,8 @@
     1.4  imports BNF_FP_Base
     1.5  keywords
     1.6    "datatype_new" :: thy_decl and
     1.7 -  "datatype_compat" :: thy_decl
     1.8 +  "datatype_compat" :: thy_decl and
     1.9 +  "primrec" :: thy_decl
    1.10  begin
    1.11  
    1.12  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
     2.1 --- a/src/HOL/Inductive.thy	Mon Feb 17 13:31:42 2014 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Mon Feb 17 13:31:42 2014 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
     2.5    "print_inductives" :: diag and
     2.6    "rep_datatype" :: thy_goal and
     2.7 -  "primrec" :: thy_decl
     2.8 +  "old_primrec" :: thy_decl
     2.9  begin
    2.10  
    2.11  subsection {* Least and greatest fixed points *}
     3.1 --- a/src/HOL/Main.thy	Mon Feb 17 13:31:42 2014 +0100
     3.2 +++ b/src/HOL/Main.thy	Mon Feb 17 13:31:42 2014 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  header {* Main HOL *}
     3.5  
     3.6  theory Main
     3.7 -imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_LFP BNF_GFP
     3.8 +imports Predicate_Compile Extraction Lifting_Sum List_Prefix Coinduction Nitpick BNF_GFP
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
     4.2 +++ b/src/HOL/Nat.thy	Mon Feb 17 13:31:42 2014 +0100
     4.3 @@ -187,7 +187,7 @@
     4.4  instantiation nat :: comm_monoid_diff
     4.5  begin
     4.6  
     4.7 -primrec plus_nat where
     4.8 +old_primrec plus_nat where
     4.9    add_0:      "0 + n = (n\<Colon>nat)"
    4.10  | add_Suc:  "Suc m + n = Suc (m + n)"
    4.11  
    4.12 @@ -202,7 +202,7 @@
    4.13  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
    4.14    by simp
    4.15  
    4.16 -primrec minus_nat where
    4.17 +old_primrec minus_nat where
    4.18    diff_0 [code]: "m - 0 = (m\<Colon>nat)"
    4.19  | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    4.20  
    4.21 @@ -235,7 +235,7 @@
    4.22  definition
    4.23    One_nat_def [simp]: "1 = Suc 0"
    4.24  
    4.25 -primrec times_nat where
    4.26 +old_primrec times_nat where
    4.27    mult_0:     "0 * n = (0\<Colon>nat)"
    4.28  | mult_Suc: "Suc m * n = n + (m * n)"
    4.29  
    4.30 @@ -414,7 +414,7 @@
    4.31  instantiation nat :: linorder
    4.32  begin
    4.33  
    4.34 -primrec less_eq_nat where
    4.35 +old_primrec less_eq_nat where
    4.36    "(0\<Colon>nat) \<le> n \<longleftrightarrow> True"
    4.37  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
    4.38  
    4.39 @@ -1303,7 +1303,7 @@
    4.40    funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
    4.41  begin
    4.42  
    4.43 -primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.44 +old_primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.45    "funpow 0 f = id"
    4.46  | "funpow (Suc n) f = f o funpow n f"
    4.47  
    4.48 @@ -1410,7 +1410,7 @@
    4.49  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    4.50    by (induct m) (simp_all add: add_ac distrib_right)
    4.51  
    4.52 -primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.53 +old_primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.54    "of_nat_aux inc 0 i = i"
    4.55  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
    4.56  
     5.1 --- a/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
     5.2 +++ b/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Binary Numerals *}
     5.5  
     5.6  theory Num
     5.7 -imports Datatype
     5.8 +imports Datatype BNF_LFP
     5.9  begin
    5.10  
    5.11  subsection {* The @{text num} type *}
    5.12 @@ -1249,4 +1249,3 @@
    5.13    code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    5.14  
    5.15  end
    5.16 -
     6.1 --- a/src/HOL/Sum_Type.thy	Mon Feb 17 13:31:42 2014 +0100
     6.2 +++ b/src/HOL/Sum_Type.thy	Mon Feb 17 13:31:42 2014 +0100
     6.3 @@ -120,7 +120,7 @@
     6.4  
     6.5  setup {* Sign.parent_path *}
     6.6  
     6.7 -primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
     6.8 +old_primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
     6.9    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    6.10  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    6.11  
    6.12 @@ -177,10 +177,10 @@
    6.13    qed
    6.14  qed
    6.15  
    6.16 -primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
    6.17 +old_primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
    6.18    "Suml f (Inl x) = f x"
    6.19  
    6.20 -primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
    6.21 +old_primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
    6.22    "Sumr f (Inr x) = f x"
    6.23  
    6.24  lemma Suml_inject:
     7.1 --- a/src/HOL/Tools/Datatype/primrec.ML	Mon Feb 17 13:31:42 2014 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/primrec.ML	Mon Feb 17 13:31:42 2014 +0100
     7.3 @@ -312,7 +312,7 @@
     7.4  (* outer syntax *)
     7.5  
     7.6  val _ =
     7.7 -  Outer_Syntax.local_theory @{command_spec "primrec"}
     7.8 +  Outer_Syntax.local_theory @{command_spec "old_primrec"}
     7.9      "define primitive recursive functions on datatypes"
    7.10      (Parse.fixes -- Parse_Spec.where_alt_specs
    7.11        >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));
     8.1 --- a/src/HOL/Transitive_Closure.thy	Mon Feb 17 13:31:42 2014 +0100
     8.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 17 13:31:42 2014 +0100
     8.3 @@ -716,11 +716,11 @@
     8.4    relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
     8.5  begin
     8.6  
     8.7 -primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     8.8 +old_primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     8.9      "relpow 0 R = Id"
    8.10    | "relpow (Suc n) R = (R ^^ n) O R"
    8.11  
    8.12 -primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
    8.13 +old_primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
    8.14      "relpowp 0 R = HOL.eq"
    8.15    | "relpowp (Suc n) R = (R ^^ n) OO R"
    8.16