--- 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.
--- 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);
--- 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
--- 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"
--- 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
--- 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
--- 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)
--- 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)
--- 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"
--- 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)"
--- 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)"
--- 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"
--- 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"
--- 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
--- 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
--- 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"} *}
--- 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)
--- 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"
--- 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
--- 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;
--- 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
--- 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)"
--- 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]:
--- 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)
--- 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
--- 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