# HG changeset patch
# User blanchet
# Date 1392190557 -3600
# Node ID 05f5fdb8d093bd108d0e50b40a1f319a10fc6db7
# Parent  eab03e9cee8aa04cfdfad69bf01c6df9843fb43c
renamed 'nat_{case,rec}' to '{case,rec}_nat'

diff -r eab03e9cee8a -r 05f5fdb8d093 src/Doc/Logics/document/HOL.tex
--- a/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:57 2014 +0100
@@ -1231,7 +1231,7 @@
 Note that Isabelle insists on precisely this format; you may not even change
 the order of the two cases.
 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
-\cdx{nat_rec}, which is available because \textit{nat} is represented as
+\cdx{rec_nat}, which is available because \textit{nat} is represented as
 a datatype.
 
 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
diff -r eab03e9cee8a -r 05f5fdb8d093 src/Doc/Tutorial/CTL/CTL.thy
--- a/src/Doc/Tutorial/CTL/CTL.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/Doc/Tutorial/CTL/CTL.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -258,9 +258,9 @@
 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
 that we could have given the witness without having to define a new function:
 the term
-@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
+@{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
 is extensionally equal to @{term"path s Q"},
-where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.
+where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.
 *};
 (*<*)
 lemma
@@ -270,7 +270,7 @@
  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
  apply(simp add: Paths_def);
  apply(blast);
-apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
+apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
 apply(simp);
 apply(intro strip);
 apply(induct_tac i);
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -34,13 +34,13 @@
 
 overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
 begin
-  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+  definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
 end
 
 overloading int_pow == "pow :: [_, 'a, int] => 'a"
 begin
   definition "int_pow G a z =
-   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
     in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
 end
 
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -266,10 +266,10 @@
 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
 unfolding Field_card_of csum_def by auto
 
-lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
+lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
 by auto
 
-lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
+lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
 by auto
 
 lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Datatype.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -56,7 +56,7 @@
   Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
   (*crude "lists" of nats -- needed for the constructions*)
-  Push_def:   "Push == (%b h. nat_case b h)"
+  Push_def:   "Push == (%b h. case_nat b h)"
 
   (** operations on S-expressions -- sets of nodes **)
 
@@ -133,7 +133,7 @@
 
 lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
 apply (simp add: Node_def Push_def) 
-apply (fast intro!: apfst_conv nat_case_Suc [THEN trans])
+apply (fast intro!: apfst_conv case_nat_Suc [THEN trans])
 done
 
 
@@ -251,7 +251,7 @@
 by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
 
 lemma ndepth_Push_Node_aux:
-     "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
+     "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
 apply (induct_tac "k", auto)
 apply (erule Least_le)
 done
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -198,7 +198,7 @@
   def b \<equiv> "\<lambda>i. LEAST j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i"
   def c \<equiv> "\<lambda>i j. LEAST k. enum k \<in> rep x \<and> enum i \<preceq> enum k \<and> enum j \<preceq> enum k"
   def P \<equiv> "\<lambda>i. \<exists>j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i"
-  def X \<equiv> "nat_rec a (\<lambda>n i. if P i then c i (b i) else i)"
+  def X \<equiv> "rec_nat a (\<lambda>n i. if P i then c i (b i) else i)"
   have X_0: "X 0 = a" unfolding X_def by simp
   have X_Suc: "\<And>n. X (Suc n) = (if P (X n) then c (X n) (b (X n)) else X n)"
     unfolding X_def by simp
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -289,7 +289,7 @@
   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
   -- {* Courtesy of Stephan Merz *}
 proof -
-  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
+  def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
   moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
@@ -534,8 +534,8 @@
  apply (erule exE)
  apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
 apply (erule contrapos_np, simp, clarify)
-apply (subgoal_tac "\<forall>n. nat_rec x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
- apply (rule_tac x = "nat_rec x (%i y. @z. z:Q & (z,y) :r)" in exI)
+apply (subgoal_tac "\<forall>n. rec_nat x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
+ apply (rule_tac x = "rec_nat x (%i y. @z. z:Q & (z,y) :r)" in exI)
  apply (rule allI, simp)
  apply (rule someI2_ex, blast, blast)
 apply (rule allI)
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -24,7 +24,7 @@
 *}
 
 lemma [code, code_unfold]:
-  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
+  "case_nat = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
 
 
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -145,9 +145,9 @@
   with that show thesis .
 qed
 
-lemma almost_everywhere_zero_nat_case:
+lemma almost_everywhere_zero_case_nat:
   assumes "almost_everywhere_zero f"
-  shows "almost_everywhere_zero (nat_case a f)"
+  shows "almost_everywhere_zero (case_nat a f)"
   using assms
   by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
     blast
@@ -258,8 +258,8 @@
 subsection {* List-style constructor for polynomials *}
 
 lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
-  is "\<lambda>a p. nat_case a (coeff p)"
-  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case)
+  is "\<lambda>a p. case_nat a (coeff p)"
+  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_case_nat)
 
 lemmas coeff_pCons = pCons.rep_eq
 
@@ -405,8 +405,8 @@
 proof -
   { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
     assume "\<forall>m\<in>set ms. m > 0"
-    then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
-      by (induct ms) (auto, metis Suc_pred' nat_case_Suc) }
+    then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
+      by (induct ms) (auto, metis Suc_pred' case_nat_Suc) }
   note * = this
   show ?thesis
     by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
@@ -452,7 +452,7 @@
 lemma coeff_Poly_eq:
   "coeff (Poly xs) n = nth_default 0 xs n"
   apply (induct xs arbitrary: n) apply simp_all
-  by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
+  by (metis case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
 
 lemma nth_default_coeffs_eq:
   "nth_default 0 (coeffs p) = coeff p"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Limits.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -1750,7 +1750,7 @@
   assumes local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b"
   shows "P a b"
 proof -
-  def bisect \<equiv> "nat_rec (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
+  def bisect \<equiv> "rec_nat (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
   def l \<equiv> "\<lambda>n. fst (bisect n)" and u \<equiv> "\<lambda>n. snd (bisect n)"
   have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
     and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -1648,10 +1648,10 @@
 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
 apply (induct xs, simp, simp)
 apply safe
-apply (metis nat_case_0 nth.simps zero_less_Suc)
+apply (metis case_nat_0 nth.simps zero_less_Suc)
 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
 apply (case_tac i, simp)
-apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc case_nat_Suc nth.simps zero_less_diff)
 done
 
 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -2776,7 +2776,7 @@
       unfolding s_def by (auto intro: someI2_ex)
   }
   note s = this
-  def r \<equiv> "nat_rec (s 0 0) s"
+  def r \<equiv> "rec_nat (s 0 0) s"
   have "subseq r"
     by (auto simp: r_def s subseq_Suc_iff)
   moreover
@@ -3376,7 +3376,7 @@
       unfolding s_def by (auto intro: someI2_ex)
   }
   note s = this
-  def r \<equiv> "nat_rec (s 0 0) s"
+  def r \<equiv> "rec_nat (s 0 0) s"
   have "subseq r"
     by (auto simp: r_def s subseq_Suc_iff)
   moreover
@@ -3953,7 +3953,7 @@
       }
       note B = this
 
-      def F \<equiv> "nat_rec (B 0 UNIV) B"
+      def F \<equiv> "rec_nat (B 0 UNIV) B"
       {
         fix n
         have "infinite {i. f i \<in> F n}"
@@ -3974,7 +3974,7 @@
           by (simp add: set_eq_iff not_le conj_commute)
       qed
 
-      def t \<equiv> "nat_rec (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
+      def t \<equiv> "rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
       have "subseq t"
         unfolding subseq_Suc_iff by (simp add: t_def sel)
       moreover have "\<forall>i. (f \<circ> t) i \<in> s"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -95,8 +95,8 @@
 lemmas nat_rec_0 = nat.recs(1)
   and nat_rec_Suc = nat.recs(2)
 
-lemmas nat_case_0 = nat.cases(1)
-  and nat_case_Suc = nat.cases(2)
+lemmas case_nat_0 = nat.cases(1)
+  and case_nat_Suc = nat.cases(2)
    
 
 text {* Injectiveness and distinctness lemmas *}
@@ -634,10 +634,10 @@
 
 text {* These two rules ease the use of primitive recursion.
 NOTE USE OF @{text "=="} *}
-lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
+lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
 by simp
 
-lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
+lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
 by simp
 
 lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -104,8 +104,8 @@
 
 declare unit.cases [nitpick_simp del]
 
-lemma nat_case_unfold [nitpick_unfold]:
-"nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
+lemma case_nat_unfold [nitpick_unfold]:
+"case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
 apply (rule eq_reflection)
 by (cases n) auto
 
@@ -241,7 +241,7 @@
 hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
     prod_def refl'_def wf'_def card'_def setsum'_def
-    fold_graph'_def The_psimp Eps_psimp case_unit_unfold nat_case_unfold
+    fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
     list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
     zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
     plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -746,17 +746,17 @@
 nitpick [card = 1\<emdash>7, expect = none]
 oops
 
-lemma "nat_rec zero suc 0 = zero"
+lemma "rec_nat zero suc 0 = zero"
 nitpick [expect = none]
 apply simp
 done
 
-lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
+lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
 nitpick [expect = none]
 apply simp
 done
 
-lemma "P (nat_rec zero suc x)"
+lemma "P (rec_nat zero suc x)"
 nitpick [expect = genuine]
 oops
 
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -1050,24 +1050,24 @@
   "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
   by (simp add: numeral_eq_Suc)
 
-text {* For @{term nat_case} and @{term nat_rec}. *}
+text {* For @{term case_nat} and @{term rec_nat}. *}
 
-lemma nat_case_numeral [simp]:
-  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
+lemma case_nat_numeral [simp]:
+  "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
   by (simp add: numeral_eq_Suc)
 
-lemma nat_case_add_eq_if [simp]:
-  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
+lemma case_nat_add_eq_if [simp]:
+  "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
   by (simp add: numeral_eq_Suc)
 
-lemma nat_rec_numeral [simp]:
-  "nat_rec a f (numeral v) =
-    (let pv = pred_numeral v in f pv (nat_rec a f pv))"
+lemma rec_nat_numeral [simp]:
+  "rec_nat a f (numeral v) =
+    (let pv = pred_numeral v in f pv (rec_nat a f pv))"
   by (simp add: numeral_eq_Suc Let_def)
 
-lemma nat_rec_add_eq_if [simp]:
-  "nat_rec a f (numeral v + n) =
-    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
+lemma rec_nat_add_eq_if [simp]:
+  "rec_nat a f (numeral v + n) =
+    (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
   by (simp add: numeral_eq_Suc Let_def)
 
 text {* Case analysis on @{term "n < 2"} *}
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -442,15 +442,15 @@
   "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
   by simp
 
-lemma measurable_nat_case[measurable (raw)]:
+lemma measurable_case_nat[measurable (raw)]:
   assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
     "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
-  shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
+  shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
   by (cases i) simp_all
 
-lemma measurable_nat_case'[measurable (raw)]:
+lemma measurable_case_nat'[measurable (raw)]:
   assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
-  shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
+  shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   using fg[THEN measurable_space]
   by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
 
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -190,13 +190,13 @@
       let ?P =
         "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
           (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
-      def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
+      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
 
       { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
           (\<forall>n. ?a / 2 ^ (k + 1) \<le> ?q k n (w k)) \<and> (k \<noteq> 0 \<longrightarrow> restrict (w k) (J (k - 1)) = w (k - 1))"
         proof (induct k)
           case 0 with w0 show ?case
-            unfolding w_def nat_rec_0 by auto
+            unfolding w_def rec_nat_0 by auto
         next
           case (Suc k)
           then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
@@ -241,7 +241,7 @@
                  (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
           qed
           then have "?P k (w k) (w (Suc k))"
-            unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
+            unfolding w_def rec_nat_Suc unfolding w_def[symmetric]
             by (rule someI_ex)
           then show ?case by auto
         qed
@@ -480,10 +480,10 @@
 lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
   by (auto simp add: comb_seq_def)
 
-lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
+lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (case_nat (\<omega> n) \<omega>')"
   by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
 
-lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
+lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = case_nat (\<omega> 0)"
   by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
 
 lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
@@ -492,11 +492,11 @@
 lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
   by (auto split: nat.split split_comb_seq)
 
-lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
+lemma case_nat_comb_seq: "case_nat s' (comb_seq n \<omega> \<omega>') (i + n) = case_nat (case_nat s' \<omega> n) \<omega>' i"
   by (auto split: nat.split split_comb_seq)
 
-lemma nat_case_comb_seq':
-  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
+lemma case_nat_comb_seq':
+  "case_nat s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (case_nat s \<omega>) \<omega>'"
   by (auto split: split_comb_seq nat.split)
 
 locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
@@ -570,7 +570,7 @@
 qed simp_all
 
 lemma PiM_iter:
-  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). nat_case s \<omega>) = S" (is "?D = _")
+  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). case_nat s \<omega>) = S" (is "?D = _")
 proof (rule PiM_eq)
   let ?I = "UNIV::nat set" and ?M = "\<lambda>n. M"
   let "distr _ _ ?f" = "?D"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -244,13 +244,13 @@
       by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
     hence "\<exists>A. ?P A S n" .. }
   note Ex_P = this
-  def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
+  def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
   have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
   have A_0[simp]: "A 0 = space M" unfolding A_def by simp
   { fix i have "A i \<in> sets M" unfolding A_def
     proof (induct i)
       case (Suc i)
-      from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
+      from Ex_P[OF this, of i] show ?case unfolding rec_nat_Suc
         by (rule someI2_ex) simp
     qed simp }
   note A_in_sets = this
@@ -281,7 +281,7 @@
       from ex_inverse_of_nat_Suc_less[OF this]
       obtain n where *: "?d B < - 1 / real (Suc n)"
         by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
-      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
+      have "B \<subseteq> A (Suc n)" using B by (auto simp del: rec_nat_Suc)
       from epsilon[OF B(1) this] *
       show False by auto
     qed
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
@@ -525,7 +525,7 @@
         val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
           (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
 
-        val rhs = mk_nat_rec Zero Suc;
+        val rhs = mk_rec_nat Zero Suc;
       in
         fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
@@ -555,8 +555,8 @@
         mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
       end;
 
-    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0_imp} hset_rec_defs;
-    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc_imp} hset_rec_defs;
+    val hset_rec_0ss = mk_rec_simps n @{thm rec_nat_0_imp} hset_rec_defs;
+    val hset_rec_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} hset_rec_defs;
     val hset_rec_0ss' = transpose hset_rec_0ss;
     val hset_rec_Sucss' = transpose hset_rec_Sucss;
 
@@ -1202,7 +1202,7 @@
         val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
           (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
 
-        val rhs = mk_nat_rec Zero Suc;
+        val rhs = mk_rec_nat Zero Suc;
       in
         fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Tools/BNF/bnf_gfp_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 12 08:35:57 2014 +0100
@@ -22,12 +22,12 @@
   val mk_in_rel: term -> term
   val mk_equiv: term -> term -> term
   val mk_fromCard: term -> term -> term
-  val mk_nat_rec: term -> term -> term
   val mk_prefCl: term -> term
   val mk_prefixeq: term -> term -> term
   val mk_proj: term -> term
   val mk_quotient: term -> term -> term
   val mk_rec_list: term -> term -> term
+  val mk_rec_nat: term -> term -> term
   val mk_shift: term -> term -> term
   val mk_size: term -> term
   val mk_toCard: term -> term -> term
@@ -146,9 +146,9 @@
 
 fun mk_undefined T = Const (@{const_name undefined}, T);
 
-fun mk_nat_rec Zero Suc =
+fun mk_rec_nat Zero Suc =
   let val T = fastype_of Zero;
-  in Const (@{const_name nat_rec}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
+  in Const (@{const_name rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
 
 fun mk_rec_list Nil Cons =
   let
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -1296,7 +1296,7 @@
 proof cases
   let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
   assume *: "\<forall>n. \<exists>p. ?P p n"
-  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
+  def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
   have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
   have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
   have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
@@ -1318,7 +1318,7 @@
   let "?P p m" = "m < p \<and> s m < s p"
   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
-  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
+  def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
   have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
   have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
   have P_0: "?P (f 0) (Suc N)"
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -358,12 +358,12 @@
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   unfolding fun_upd_def [abs_def] by transfer_prover
 
-lemma nat_case_transfer [transfer_rule]:
-  "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
+lemma case_nat_transfer [transfer_rule]:
+  "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
   unfolding fun_rel_def by (simp split: nat.split)
 
-lemma nat_rec_transfer [transfer_rule]:
-  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
+lemma rec_nat_transfer [transfer_rule]:
+  "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
   unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
 
 lemma funpow_transfer [transfer_rule]:
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Word/Word.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -4578,7 +4578,7 @@
 
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
 where
-  "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
+  "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
 
 lemma word_rec_0: "word_rec z s 0 = z"
   by (simp add: word_rec_def)
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/ex/Primrec.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -191,7 +191,7 @@
   "PREC f g l =
     (case l of
       [] => 0
-    | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
+    | x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)"
   -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
 
 inductive PRIMREC :: "(nat list => nat) => bool" where
diff -r eab03e9cee8a -r 05f5fdb8d093 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
@@ -734,15 +734,15 @@
       model will be found *}
 oops
 
-lemma "nat_rec zero suc 0 = zero"
+lemma "rec_nat zero suc 0 = zero"
 refute [expect = none]
 by simp
 
-lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
+lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
 refute [maxsize = 2, expect = none]
 by simp
 
-lemma "P (nat_rec zero suc x)"
+lemma "P (rec_nat zero suc x)"
 refute [expect = potential]
 oops