renamed 'nat_{case,rec}' to '{case,rec}_nat'
authorblanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 5541505f5fdb8d093
parent 55414 eab03e9cee8a
child 55416 dd7992d4a61a
renamed 'nat_{case,rec}' to '{case,rec}_nat'
src/Doc/Logics/document/HOL.tex
src/Doc/Tutorial/CTL/CTL.thy
src/HOL/Algebra/Group.thy
src/HOL/BNF_GFP.thy
src/HOL/Datatype.thy
src/HOL/HOLCF/Completion.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Code_Abstract_Nat.thy
src/HOL/Library/Polynomial.thy
src/HOL/Limits.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nat.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Num.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_util.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transfer.thy
src/HOL/Word/Word.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/Doc/Logics/document/HOL.tex	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -1231,7 +1231,7 @@
     1.4  Note that Isabelle insists on precisely this format; you may not even change
     1.5  the order of the two cases.
     1.6  Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
     1.7 -\cdx{nat_rec}, which is available because \textit{nat} is represented as
     1.8 +\cdx{rec_nat}, which is available because \textit{nat} is represented as
     1.9  a datatype.
    1.10  
    1.11  %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
     2.1 --- a/src/Doc/Tutorial/CTL/CTL.thy	Wed Feb 12 08:35:57 2014 +0100
     2.2 +++ b/src/Doc/Tutorial/CTL/CTL.thy	Wed Feb 12 08:35:57 2014 +0100
     2.3 @@ -258,9 +258,9 @@
     2.4  @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
     2.5  that we could have given the witness without having to define a new function:
     2.6  the term
     2.7 -@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
     2.8 +@{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
     2.9  is extensionally equal to @{term"path s Q"},
    2.10 -where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.
    2.11 +where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.
    2.12  *};
    2.13  (*<*)
    2.14  lemma
    2.15 @@ -270,7 +270,7 @@
    2.16   "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
    2.17   apply(simp add: Paths_def);
    2.18   apply(blast);
    2.19 -apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
    2.20 +apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
    2.21  apply(simp);
    2.22  apply(intro strip);
    2.23  apply(induct_tac i);
     3.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
     3.2 +++ b/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
     3.3 @@ -34,13 +34,13 @@
     3.4  
     3.5  overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
     3.6  begin
     3.7 -  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
     3.8 +  definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
     3.9  end
    3.10  
    3.11  overloading int_pow == "pow :: [_, 'a, int] => 'a"
    3.12  begin
    3.13    definition "int_pow G a z =
    3.14 -   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    3.15 +   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    3.16      in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
    3.17  end
    3.18  
     4.1 --- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     4.2 +++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     4.3 @@ -266,10 +266,10 @@
     4.4  lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
     4.5  unfolding Field_card_of csum_def by auto
     4.6  
     4.7 -lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
     4.8 +lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
     4.9  by auto
    4.10  
    4.11 -lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    4.12 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    4.13  by auto
    4.14  
    4.15  lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
     5.1 --- a/src/HOL/Datatype.thy	Wed Feb 12 08:35:57 2014 +0100
     5.2 +++ b/src/HOL/Datatype.thy	Wed Feb 12 08:35:57 2014 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4    Push_Node_def:  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
     5.5  
     5.6    (*crude "lists" of nats -- needed for the constructions*)
     5.7 -  Push_def:   "Push == (%b h. nat_case b h)"
     5.8 +  Push_def:   "Push == (%b h. case_nat b h)"
     5.9  
    5.10    (** operations on S-expressions -- sets of nodes **)
    5.11  
    5.12 @@ -133,7 +133,7 @@
    5.13  
    5.14  lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
    5.15  apply (simp add: Node_def Push_def) 
    5.16 -apply (fast intro!: apfst_conv nat_case_Suc [THEN trans])
    5.17 +apply (fast intro!: apfst_conv case_nat_Suc [THEN trans])
    5.18  done
    5.19  
    5.20  
    5.21 @@ -251,7 +251,7 @@
    5.22  by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
    5.23  
    5.24  lemma ndepth_Push_Node_aux:
    5.25 -     "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
    5.26 +     "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
    5.27  apply (induct_tac "k", auto)
    5.28  apply (erule Least_le)
    5.29  done
     6.1 --- a/src/HOL/HOLCF/Completion.thy	Wed Feb 12 08:35:57 2014 +0100
     6.2 +++ b/src/HOL/HOLCF/Completion.thy	Wed Feb 12 08:35:57 2014 +0100
     6.3 @@ -198,7 +198,7 @@
     6.4    def b \<equiv> "\<lambda>i. LEAST j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i"
     6.5    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"
     6.6    def P \<equiv> "\<lambda>i. \<exists>j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i"
     6.7 -  def X \<equiv> "nat_rec a (\<lambda>n i. if P i then c i (b i) else i)"
     6.8 +  def X \<equiv> "rec_nat a (\<lambda>n i. if P i then c i (b i) else i)"
     6.9    have X_0: "X 0 = a" unfolding X_def by simp
    6.10    have X_Suc: "\<And>n. X (Suc n) = (if P (X n) then c (X n) (b (X n)) else X n)"
    6.11      unfolding X_def by simp
     7.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
     7.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Feb 12 08:35:57 2014 +0100
     7.3 @@ -289,7 +289,7 @@
     7.4    shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
     7.5    -- {* Courtesy of Stephan Merz *}
     7.6  proof -
     7.7 -  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
     7.8 +  def Sseq \<equiv> "rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
     7.9    def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
    7.10    { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
    7.11    moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
    7.12 @@ -534,8 +534,8 @@
    7.13   apply (erule exE)
    7.14   apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
    7.15  apply (erule contrapos_np, simp, clarify)
    7.16 -apply (subgoal_tac "\<forall>n. nat_rec x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
    7.17 - apply (rule_tac x = "nat_rec x (%i y. @z. z:Q & (z,y) :r)" in exI)
    7.18 +apply (subgoal_tac "\<forall>n. rec_nat x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
    7.19 + apply (rule_tac x = "rec_nat x (%i y. @z. z:Q & (z,y) :r)" in exI)
    7.20   apply (rule allI, simp)
    7.21   apply (rule someI2_ex, blast, blast)
    7.22  apply (rule allI)
     8.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
     8.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 12 08:35:57 2014 +0100
     8.3 @@ -24,7 +24,7 @@
     8.4  *}
     8.5  
     8.6  lemma [code, code_unfold]:
     8.7 -  "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
     8.8 +  "case_nat = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
     8.9    by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
    8.10  
    8.11  
     9.1 --- a/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
     9.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Feb 12 08:35:57 2014 +0100
     9.3 @@ -145,9 +145,9 @@
     9.4    with that show thesis .
     9.5  qed
     9.6  
     9.7 -lemma almost_everywhere_zero_nat_case:
     9.8 +lemma almost_everywhere_zero_case_nat:
     9.9    assumes "almost_everywhere_zero f"
    9.10 -  shows "almost_everywhere_zero (nat_case a f)"
    9.11 +  shows "almost_everywhere_zero (case_nat a f)"
    9.12    using assms
    9.13    by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split)
    9.14      blast
    9.15 @@ -258,8 +258,8 @@
    9.16  subsection {* List-style constructor for polynomials *}
    9.17  
    9.18  lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    9.19 -  is "\<lambda>a p. nat_case a (coeff p)"
    9.20 -  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case)
    9.21 +  is "\<lambda>a p. case_nat a (coeff p)"
    9.22 +  using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_case_nat)
    9.23  
    9.24  lemmas coeff_pCons = pCons.rep_eq
    9.25  
    9.26 @@ -405,8 +405,8 @@
    9.27  proof -
    9.28    { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a"
    9.29      assume "\<forall>m\<in>set ms. m > 0"
    9.30 -    then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)"
    9.31 -      by (induct ms) (auto, metis Suc_pred' nat_case_Suc) }
    9.32 +    then have "map (case_nat x f) ms = map f (map (\<lambda>n. n - 1) ms)"
    9.33 +      by (induct ms) (auto, metis Suc_pred' case_nat_Suc) }
    9.34    note * = this
    9.35    show ?thesis
    9.36      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
    9.37 @@ -452,7 +452,7 @@
    9.38  lemma coeff_Poly_eq:
    9.39    "coeff (Poly xs) n = nth_default 0 xs n"
    9.40    apply (induct xs arbitrary: n) apply simp_all
    9.41 -  by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
    9.42 +  by (metis case_nat_0 case_nat_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq)
    9.43  
    9.44  lemma nth_default_coeffs_eq:
    9.45    "nth_default 0 (coeffs p) = coeff p"
    10.1 --- a/src/HOL/Limits.thy	Wed Feb 12 08:35:57 2014 +0100
    10.2 +++ b/src/HOL/Limits.thy	Wed Feb 12 08:35:57 2014 +0100
    10.3 @@ -1750,7 +1750,7 @@
    10.4    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"
    10.5    shows "P a b"
    10.6  proof -
    10.7 -  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))"
    10.8 +  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))"
    10.9    def l \<equiv> "\<lambda>n. fst (bisect n)" and u \<equiv> "\<lambda>n. snd (bisect n)"
   10.10    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)"
   10.11      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)"
    11.1 --- a/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
    11.2 +++ b/src/HOL/List.thy	Wed Feb 12 08:35:57 2014 +0100
    11.3 @@ -1648,10 +1648,10 @@
    11.4  lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
    11.5  apply (induct xs, simp, simp)
    11.6  apply safe
    11.7 -apply (metis nat_case_0 nth.simps zero_less_Suc)
    11.8 +apply (metis case_nat_0 nth.simps zero_less_Suc)
    11.9  apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
   11.10  apply (case_tac i, simp)
   11.11 -apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
   11.12 +apply (metis diff_Suc_Suc case_nat_Suc nth.simps zero_less_diff)
   11.13  done
   11.14  
   11.15  lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
    12.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 12 08:35:57 2014 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 12 08:35:57 2014 +0100
    12.3 @@ -2776,7 +2776,7 @@
    12.4        unfolding s_def by (auto intro: someI2_ex)
    12.5    }
    12.6    note s = this
    12.7 -  def r \<equiv> "nat_rec (s 0 0) s"
    12.8 +  def r \<equiv> "rec_nat (s 0 0) s"
    12.9    have "subseq r"
   12.10      by (auto simp: r_def s subseq_Suc_iff)
   12.11    moreover
   12.12 @@ -3376,7 +3376,7 @@
   12.13        unfolding s_def by (auto intro: someI2_ex)
   12.14    }
   12.15    note s = this
   12.16 -  def r \<equiv> "nat_rec (s 0 0) s"
   12.17 +  def r \<equiv> "rec_nat (s 0 0) s"
   12.18    have "subseq r"
   12.19      by (auto simp: r_def s subseq_Suc_iff)
   12.20    moreover
   12.21 @@ -3953,7 +3953,7 @@
   12.22        }
   12.23        note B = this
   12.24  
   12.25 -      def F \<equiv> "nat_rec (B 0 UNIV) B"
   12.26 +      def F \<equiv> "rec_nat (B 0 UNIV) B"
   12.27        {
   12.28          fix n
   12.29          have "infinite {i. f i \<in> F n}"
   12.30 @@ -3974,7 +3974,7 @@
   12.31            by (simp add: set_eq_iff not_le conj_commute)
   12.32        qed
   12.33  
   12.34 -      def t \<equiv> "nat_rec (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
   12.35 +      def t \<equiv> "rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
   12.36        have "subseq t"
   12.37          unfolding subseq_Suc_iff by (simp add: t_def sel)
   12.38        moreover have "\<forall>i. (f \<circ> t) i \<in> s"
    13.1 --- a/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
    13.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
    13.3 @@ -95,8 +95,8 @@
    13.4  lemmas nat_rec_0 = nat.recs(1)
    13.5    and nat_rec_Suc = nat.recs(2)
    13.6  
    13.7 -lemmas nat_case_0 = nat.cases(1)
    13.8 -  and nat_case_Suc = nat.cases(2)
    13.9 +lemmas case_nat_0 = nat.cases(1)
   13.10 +  and case_nat_Suc = nat.cases(2)
   13.11     
   13.12  
   13.13  text {* Injectiveness and distinctness lemmas *}
   13.14 @@ -634,10 +634,10 @@
   13.15  
   13.16  text {* These two rules ease the use of primitive recursion.
   13.17  NOTE USE OF @{text "=="} *}
   13.18 -lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
   13.19 +lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
   13.20  by simp
   13.21  
   13.22 -lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
   13.23 +lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
   13.24  by simp
   13.25  
   13.26  lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
    14.1 --- a/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
    14.2 +++ b/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
    14.3 @@ -104,8 +104,8 @@
    14.4  
    14.5  declare unit.cases [nitpick_simp del]
    14.6  
    14.7 -lemma nat_case_unfold [nitpick_unfold]:
    14.8 -"nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    14.9 +lemma case_nat_unfold [nitpick_unfold]:
   14.10 +"case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
   14.11  apply (rule eq_reflection)
   14.12  by (cases n) auto
   14.13  
   14.14 @@ -241,7 +241,7 @@
   14.15  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
   14.16  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
   14.17      prod_def refl'_def wf'_def card'_def setsum'_def
   14.18 -    fold_graph'_def The_psimp Eps_psimp case_unit_unfold nat_case_unfold
   14.19 +    fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
   14.20      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
   14.21      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
   14.22      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    15.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:57 2014 +0100
    15.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 12 08:35:57 2014 +0100
    15.3 @@ -746,17 +746,17 @@
    15.4  nitpick [card = 1\<emdash>7, expect = none]
    15.5  oops
    15.6  
    15.7 -lemma "nat_rec zero suc 0 = zero"
    15.8 +lemma "rec_nat zero suc 0 = zero"
    15.9  nitpick [expect = none]
   15.10  apply simp
   15.11  done
   15.12  
   15.13 -lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
   15.14 +lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
   15.15  nitpick [expect = none]
   15.16  apply simp
   15.17  done
   15.18  
   15.19 -lemma "P (nat_rec zero suc x)"
   15.20 +lemma "P (rec_nat zero suc x)"
   15.21  nitpick [expect = genuine]
   15.22  oops
   15.23  
    16.1 --- a/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
    16.2 +++ b/src/HOL/Num.thy	Wed Feb 12 08:35:57 2014 +0100
    16.3 @@ -1050,24 +1050,24 @@
    16.4    "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
    16.5    by (simp add: numeral_eq_Suc)
    16.6  
    16.7 -text {* For @{term nat_case} and @{term nat_rec}. *}
    16.8 +text {* For @{term case_nat} and @{term rec_nat}. *}
    16.9  
   16.10 -lemma nat_case_numeral [simp]:
   16.11 -  "nat_case a f (numeral v) = (let pv = pred_numeral v in f pv)"
   16.12 +lemma case_nat_numeral [simp]:
   16.13 +  "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)"
   16.14    by (simp add: numeral_eq_Suc)
   16.15  
   16.16 -lemma nat_case_add_eq_if [simp]:
   16.17 -  "nat_case a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
   16.18 +lemma case_nat_add_eq_if [simp]:
   16.19 +  "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))"
   16.20    by (simp add: numeral_eq_Suc)
   16.21  
   16.22 -lemma nat_rec_numeral [simp]:
   16.23 -  "nat_rec a f (numeral v) =
   16.24 -    (let pv = pred_numeral v in f pv (nat_rec a f pv))"
   16.25 +lemma rec_nat_numeral [simp]:
   16.26 +  "rec_nat a f (numeral v) =
   16.27 +    (let pv = pred_numeral v in f pv (rec_nat a f pv))"
   16.28    by (simp add: numeral_eq_Suc Let_def)
   16.29  
   16.30 -lemma nat_rec_add_eq_if [simp]:
   16.31 -  "nat_rec a f (numeral v + n) =
   16.32 -    (let pv = pred_numeral v in f (pv + n) (nat_rec a f (pv + n)))"
   16.33 +lemma rec_nat_add_eq_if [simp]:
   16.34 +  "rec_nat a f (numeral v + n) =
   16.35 +    (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))"
   16.36    by (simp add: numeral_eq_Suc Let_def)
   16.37  
   16.38  text {* Case analysis on @{term "n < 2"} *}
    17.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    17.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    17.3 @@ -442,15 +442,15 @@
    17.4    "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
    17.5    by simp
    17.6  
    17.7 -lemma measurable_nat_case[measurable (raw)]:
    17.8 +lemma measurable_case_nat[measurable (raw)]:
    17.9    assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
   17.10      "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
   17.11 -  shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
   17.12 +  shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
   17.13    by (cases i) simp_all
   17.14  
   17.15 -lemma measurable_nat_case'[measurable (raw)]:
   17.16 +lemma measurable_case_nat'[measurable (raw)]:
   17.17    assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   17.18 -  shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   17.19 +  shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
   17.20    using fg[THEN measurable_space]
   17.21    by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
   17.22  
    18.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    18.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Feb 12 08:35:57 2014 +0100
    18.3 @@ -190,13 +190,13 @@
    18.4        let ?P =
    18.5          "\<lambda>k wk w. w \<in> space (Pi\<^sub>M (J (Suc k)) M) \<and> restrict w (J k) = wk \<and>
    18.6            (\<forall>n. ?a / 2 ^ (Suc k + 1) \<le> ?q (Suc k) n w)"
    18.7 -      def w \<equiv> "nat_rec w0 (\<lambda>k wk. Eps (?P k wk))"
    18.8 +      def w \<equiv> "rec_nat w0 (\<lambda>k wk. Eps (?P k wk))"
    18.9  
   18.10        { fix k have w: "w k \<in> space (Pi\<^sub>M (J k) M) \<and>
   18.11            (\<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))"
   18.12          proof (induct k)
   18.13            case 0 with w0 show ?case
   18.14 -            unfolding w_def nat_rec_0 by auto
   18.15 +            unfolding w_def rec_nat_0 by auto
   18.16          next
   18.17            case (Suc k)
   18.18            then have wk: "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
   18.19 @@ -241,7 +241,7 @@
   18.20                   (auto split: split_merge intro!: extensional_merge_sub ext simp: space_PiM PiE_iff)
   18.21            qed
   18.22            then have "?P k (w k) (w (Suc k))"
   18.23 -            unfolding w_def nat_rec_Suc unfolding w_def[symmetric]
   18.24 +            unfolding w_def rec_nat_Suc unfolding w_def[symmetric]
   18.25              by (rule someI_ex)
   18.26            then show ?case by auto
   18.27          qed
   18.28 @@ -480,10 +480,10 @@
   18.29  lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
   18.30    by (auto simp add: comb_seq_def)
   18.31  
   18.32 -lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
   18.33 +lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (case_nat (\<omega> n) \<omega>')"
   18.34    by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
   18.35  
   18.36 -lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
   18.37 +lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = case_nat (\<omega> 0)"
   18.38    by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
   18.39  
   18.40  lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
   18.41 @@ -492,11 +492,11 @@
   18.42  lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
   18.43    by (auto split: nat.split split_comb_seq)
   18.44  
   18.45 -lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
   18.46 +lemma case_nat_comb_seq: "case_nat s' (comb_seq n \<omega> \<omega>') (i + n) = case_nat (case_nat s' \<omega> n) \<omega>' i"
   18.47    by (auto split: nat.split split_comb_seq)
   18.48  
   18.49 -lemma nat_case_comb_seq':
   18.50 -  "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
   18.51 +lemma case_nat_comb_seq':
   18.52 +  "case_nat s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (case_nat s \<omega>) \<omega>'"
   18.53    by (auto split: split_comb_seq nat.split)
   18.54  
   18.55  locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
   18.56 @@ -570,7 +570,7 @@
   18.57  qed simp_all
   18.58  
   18.59  lemma PiM_iter:
   18.60 -  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). nat_case s \<omega>) = S" (is "?D = _")
   18.61 +  "distr (M \<Otimes>\<^sub>M S) S (\<lambda>(s, \<omega>). case_nat s \<omega>) = S" (is "?D = _")
   18.62  proof (rule PiM_eq)
   18.63    let ?I = "UNIV::nat set" and ?M = "\<lambda>n. M"
   18.64    let "distr _ _ ?f" = "?D"
    19.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 12 08:35:57 2014 +0100
    19.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 12 08:35:57 2014 +0100
    19.3 @@ -244,13 +244,13 @@
    19.4        by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
    19.5      hence "\<exists>A. ?P A S n" .. }
    19.6    note Ex_P = this
    19.7 -  def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
    19.8 +  def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
    19.9    have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
   19.10    have A_0[simp]: "A 0 = space M" unfolding A_def by simp
   19.11    { fix i have "A i \<in> sets M" unfolding A_def
   19.12      proof (induct i)
   19.13        case (Suc i)
   19.14 -      from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
   19.15 +      from Ex_P[OF this, of i] show ?case unfolding rec_nat_Suc
   19.16          by (rule someI2_ex) simp
   19.17      qed simp }
   19.18    note A_in_sets = this
   19.19 @@ -281,7 +281,7 @@
   19.20        from ex_inverse_of_nat_Suc_less[OF this]
   19.21        obtain n where *: "?d B < - 1 / real (Suc n)"
   19.22          by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
   19.23 -      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
   19.24 +      have "B \<subseteq> A (Suc n)" using B by (auto simp del: rec_nat_Suc)
   19.25        from epsilon[OF B(1) this] *
   19.26        show False by auto
   19.27      qed
    20.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
    20.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 12 08:35:57 2014 +0100
    20.3 @@ -525,7 +525,7 @@
    20.4          val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
    20.5            (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs')));
    20.6  
    20.7 -        val rhs = mk_nat_rec Zero Suc;
    20.8 +        val rhs = mk_rec_nat Zero Suc;
    20.9        in
   20.10          fold_rev (Term.absfree o Term.dest_Free) ss rhs
   20.11        end;
   20.12 @@ -555,8 +555,8 @@
   20.13          mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i
   20.14        end;
   20.15  
   20.16 -    val hset_rec_0ss = mk_rec_simps n @{thm nat_rec_0_imp} hset_rec_defs;
   20.17 -    val hset_rec_Sucss = mk_rec_simps n @{thm nat_rec_Suc_imp} hset_rec_defs;
   20.18 +    val hset_rec_0ss = mk_rec_simps n @{thm rec_nat_0_imp} hset_rec_defs;
   20.19 +    val hset_rec_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} hset_rec_defs;
   20.20      val hset_rec_0ss' = transpose hset_rec_0ss;
   20.21      val hset_rec_Sucss' = transpose hset_rec_Sucss;
   20.22  
   20.23 @@ -1202,7 +1202,7 @@
   20.24          val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
   20.25            (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
   20.26  
   20.27 -        val rhs = mk_nat_rec Zero Suc;
   20.28 +        val rhs = mk_rec_nat Zero Suc;
   20.29        in
   20.30          fold_rev (Term.absfree o Term.dest_Free) ss rhs
   20.31        end;
    21.1 --- a/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 12 08:35:57 2014 +0100
    21.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 12 08:35:57 2014 +0100
    21.3 @@ -22,12 +22,12 @@
    21.4    val mk_in_rel: term -> term
    21.5    val mk_equiv: term -> term -> term
    21.6    val mk_fromCard: term -> term -> term
    21.7 -  val mk_nat_rec: term -> term -> term
    21.8    val mk_prefCl: term -> term
    21.9    val mk_prefixeq: term -> term -> term
   21.10    val mk_proj: term -> term
   21.11    val mk_quotient: term -> term -> term
   21.12    val mk_rec_list: term -> term -> term
   21.13 +  val mk_rec_nat: term -> term -> term
   21.14    val mk_shift: term -> term -> term
   21.15    val mk_size: term -> term
   21.16    val mk_toCard: term -> term -> term
   21.17 @@ -146,9 +146,9 @@
   21.18  
   21.19  fun mk_undefined T = Const (@{const_name undefined}, T);
   21.20  
   21.21 -fun mk_nat_rec Zero Suc =
   21.22 +fun mk_rec_nat Zero Suc =
   21.23    let val T = fastype_of Zero;
   21.24 -  in Const (@{const_name nat_rec}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
   21.25 +  in Const (@{const_name rec_nat}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
   21.26  
   21.27  fun mk_rec_list Nil Cons =
   21.28    let
    22.1 --- a/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
    22.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Feb 12 08:35:57 2014 +0100
    22.3 @@ -1296,7 +1296,7 @@
    22.4  proof cases
    22.5    let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
    22.6    assume *: "\<forall>n. \<exists>p. ?P p n"
    22.7 -  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
    22.8 +  def f \<equiv> "rec_nat (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
    22.9    have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
   22.10    have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
   22.11    have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
   22.12 @@ -1318,7 +1318,7 @@
   22.13    let "?P p m" = "m < p \<and> s m < s p"
   22.14    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
   22.15    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
   22.16 -  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
   22.17 +  def f \<equiv> "rec_nat (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
   22.18    have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
   22.19    have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
   22.20    have P_0: "?P (f 0) (Suc N)"
    23.1 --- a/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
    23.2 +++ b/src/HOL/Transfer.thy	Wed Feb 12 08:35:57 2014 +0100
    23.3 @@ -358,12 +358,12 @@
    23.4    shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
    23.5    unfolding fun_upd_def [abs_def] by transfer_prover
    23.6  
    23.7 -lemma nat_case_transfer [transfer_rule]:
    23.8 -  "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
    23.9 +lemma case_nat_transfer [transfer_rule]:
   23.10 +  "(A ===> (op = ===> A) ===> op = ===> A) case_nat case_nat"
   23.11    unfolding fun_rel_def by (simp split: nat.split)
   23.12  
   23.13 -lemma nat_rec_transfer [transfer_rule]:
   23.14 -  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
   23.15 +lemma rec_nat_transfer [transfer_rule]:
   23.16 +  "(A ===> (op = ===> A ===> A) ===> op = ===> A) rec_nat rec_nat"
   23.17    unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
   23.18  
   23.19  lemma funpow_transfer [transfer_rule]:
    24.1 --- a/src/HOL/Word/Word.thy	Wed Feb 12 08:35:57 2014 +0100
    24.2 +++ b/src/HOL/Word/Word.thy	Wed Feb 12 08:35:57 2014 +0100
    24.3 @@ -4578,7 +4578,7 @@
    24.4  
    24.5  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
    24.6  where
    24.7 -  "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
    24.8 +  "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
    24.9  
   24.10  lemma word_rec_0: "word_rec z s 0 = z"
   24.11    by (simp add: word_rec_def)
    25.1 --- a/src/HOL/ex/Primrec.thy	Wed Feb 12 08:35:57 2014 +0100
    25.2 +++ b/src/HOL/ex/Primrec.thy	Wed Feb 12 08:35:57 2014 +0100
    25.3 @@ -191,7 +191,7 @@
    25.4    "PREC f g l =
    25.5      (case l of
    25.6        [] => 0
    25.7 -    | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)"
    25.8 +    | x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)"
    25.9    -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *}
   25.10  
   25.11  inductive PRIMREC :: "(nat list => nat) => bool" where
    26.1 --- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
    26.2 +++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 12 08:35:57 2014 +0100
    26.3 @@ -734,15 +734,15 @@
    26.4        model will be found *}
    26.5  oops
    26.6  
    26.7 -lemma "nat_rec zero suc 0 = zero"
    26.8 +lemma "rec_nat zero suc 0 = zero"
    26.9  refute [expect = none]
   26.10  by simp
   26.11  
   26.12 -lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
   26.13 +lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
   26.14  refute [maxsize = 2, expect = none]
   26.15  by simp
   26.16  
   26.17 -lemma "P (nat_rec zero suc x)"
   26.18 +lemma "P (rec_nat zero suc x)"
   26.19  refute [expect = potential]
   26.20  oops
   26.21