--- a/NEWS Tue Aug 02 07:36:58 2011 -0700
+++ b/NEWS Tue Aug 02 08:28:34 2011 -0700
@@ -65,7 +65,7 @@
* Class complete_lattice: generalized a couple of lemmas from sets;
generalized theorems INF_cong and SUP_cong. New type classes for complete
-boolean algebras and complete linear orderes. Lemmas Inf_less_iff,
+boolean algebras and complete linear orders. Lemmas Inf_less_iff,
less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
More consistent and less misunderstandable names:
INFI_def ~> INF_def
@@ -83,7 +83,7 @@
to UNION any longer; these have been moved to collection UN_ball_bex_simps.
INCOMPATIBILITY.
-* Archimedian_Field.thy:
+* Archimedean_Field.thy:
floor now is defined as parameter of a separate type class floor_ceiling.
* Finite_Set.thy: more coherent development of fold_set locales:
@@ -157,6 +157,16 @@
* Well-founded recursion combinator "wfrec" has been moved to
Library/Wfrec.thy. INCOMPATIBILITY.
+* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat.
+The names of the following types and constants have changed:
+ inat (type) ~> enat
+ Fin ~> enat
+ Infty ~> infinity (overloaded)
+ iSuc ~> eSuc
+ the_Fin ~> the_enat
+Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
+been renamed accordingly.
+
*** Document preparation ***
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Tue Aug 02 07:36:58 2011 -0700
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Tue Aug 02 08:28:34 2011 -0700
@@ -140,7 +140,7 @@
section "slen"
-lemma slen_fscons: "#(m~> s) = iSuc (#s)"
+lemma slen_fscons: "#(m~> s) = eSuc (#s)"
by (simp add: fscons_def)
lemma slen_fscons_eq:
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Aug 02 07:36:58 2011 -0700
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Aug 02 08:28:34 2011 -0700
@@ -57,12 +57,12 @@
lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
by (simp add: fsingleton_def2 enat_defs)
-lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
+lemma slen_fstreams[simp]: "#(<a> ooo s) = eSuc (#s)"
by (simp add: fsingleton_def2)
-lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
+lemma slen_fstreams2[simp]: "#(s ooo <a>) = eSuc (#s)"
apply (cases "#s")
-apply (auto simp add: iSuc_enat)
+apply (auto simp add: eSuc_enat)
apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
by (simp add: sconc_def)
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Tue Aug 02 07:36:58 2011 -0700
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Tue Aug 02 08:28:34 2011 -0700
@@ -132,8 +132,8 @@
apply (erule allE, erule allE, drule mp) (* stream_monoP *)
apply ( drule ileI1)
apply ( drule order_trans)
-apply ( rule ile_iSuc)
-apply ( drule iSuc_ile_mono [THEN iffD1])
+apply ( rule ile_eSuc)
+apply ( drule eSuc_ile_mono [THEN iffD1])
apply ( assumption)
apply (drule mp)
apply ( erule is_ub_thelub)
--- a/src/HOL/HOLCF/Library/Stream.thy Tue Aug 02 07:36:58 2011 -0700
+++ b/src/HOL/HOLCF/Library/Stream.thy Tue Aug 02 08:28:34 2011 -0700
@@ -329,10 +329,10 @@
lemma slen_empty [simp]: "#\<bottom> = 0"
by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
-lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
+lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = eSuc (#xs)"
apply (case_tac "stream_finite (x && xs)")
apply (simp add: slen_def, auto)
-apply (simp add: stream.finite_def, auto simp add: iSuc_enat)
+apply (simp add: stream.finite_def, auto simp add: eSuc_enat)
apply (rule Least_Suc2, auto)
(*apply (drule sym)*)
(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
@@ -341,7 +341,7 @@
by (drule stream_finite_lemma1,auto)
lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \<bottom>)"
-by (cases x, auto simp add: enat_0 iSuc_enat[THEN sym])
+by (cases x, auto simp add: enat_0 eSuc_enat[THEN sym])
lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
by (cases x, auto)
@@ -353,7 +353,7 @@
apply (case_tac "#y") apply simp_all
done
-lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
+lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)"
by (cases x, auto)
lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
@@ -362,15 +362,15 @@
lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < enat (Suc n))"
apply (cases x, auto)
apply (simp add: zero_enat_def)
- apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
- apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
+ apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
+ apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
done
lemma slen_take_lemma4 [rule_format]:
"!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n"
apply (induct n, auto simp add: enat_0)
apply (case_tac "s=UU", simp)
-by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_enat)
+by (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat)
(*
lemma stream_take_idempotent [simp]:
@@ -398,7 +398,7 @@
apply (case_tac "x=UU", simp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply (erule_tac x="y" in allE, auto)
-apply (simp_all add: not_less iSuc_enat)
+apply (simp_all add: not_less eSuc_enat)
apply (case_tac "#y") apply simp_all
apply (case_tac "x=UU", simp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
@@ -448,7 +448,7 @@
apply (case_tac "x=UU", auto simp add: zero_enat_def)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (erule_tac x="y" in allE, auto)
-apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_enat)
+apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat)
by (simp add: iterate_lemma)
lemma slen_take_lemma3 [rule_format]:
@@ -478,7 +478,7 @@
apply (subgoal_tac "stream_take n$s ~=s")
apply (insert slen_take_lemma4 [of n s],auto)
apply (cases s, simp)
-by (simp add: slen_take_lemma4 iSuc_enat)
+by (simp add: slen_take_lemma4 eSuc_enat)
(* ----------------------------------------------------------------------- *)
(* theorems about smap *)
@@ -593,12 +593,12 @@
apply (erule_tac x="k" in allE)
apply (erule_tac x="y" in allE,auto)
apply (erule_tac x="THE p. Suc p = t" in allE,auto)
- apply (simp add: iSuc_def split: enat.splits)
- apply (simp add: iSuc_def split: enat.splits)
+ apply (simp add: eSuc_def split: enat.splits)
+ apply (simp add: eSuc_def split: enat.splits)
apply (simp only: the_equality)
- apply (simp add: iSuc_def split: enat.splits)
+ apply (simp add: eSuc_def split: enat.splits)
apply force
-apply (simp add: iSuc_def split: enat.splits)
+apply (simp add: eSuc_def split: enat.splits)
done
lemma take_i_rt_len:
@@ -696,7 +696,7 @@
by auto
lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
-apply (simp add: sconc_def zero_enat_def iSuc_def split: enat.splits, auto)
+apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto)
apply (rule someI2_ex,auto)
apply (rule_tac x="x && y" in exI,auto)
apply (simp add: i_rt_Suc_forw)
@@ -709,7 +709,7 @@
apply (rule stream_finite_ind [of x],auto)
apply (simp add: stream.finite_def)
apply (drule slen_take_lemma1,blast)
- apply (simp_all add: zero_enat_def iSuc_def split: enat.splits)
+ apply (simp_all add: zero_enat_def eSuc_def split: enat.splits)
apply (erule_tac x="y" in allE,auto)
by (rule_tac x="a && w" in exI,auto)
@@ -743,7 +743,7 @@
lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
apply (cases "#x",auto)
- apply (simp add: sconc_def iSuc_enat)
+ apply (simp add: sconc_def eSuc_enat)
apply (rule someI2_ex)
apply (drule ex_sconc, simp)
apply (rule someI2_ex, auto)
@@ -870,9 +870,9 @@
lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
apply auto
- apply (metis not_Infty_eq slen_sconc_finite1)
- apply (metis not_Infty_eq slen_sconc_infinite1)
-apply (metis not_Infty_eq slen_sconc_infinite2)
+ apply (metis not_infinity_eq slen_sconc_finite1)
+ apply (metis not_infinity_eq slen_sconc_infinite1)
+apply (metis not_infinity_eq slen_sconc_infinite2)
done
(* ----------------------------------------------------------------------- *)
@@ -956,7 +956,7 @@
defer 1
apply (simp add: constr_sconc_def del: scons_sconc)
apply (case_tac "#s")
- apply (simp add: iSuc_enat)
+ apply (simp add: eSuc_enat)
apply (case_tac "a=UU",auto simp del: scons_sconc)
apply (simp)
apply (simp add: sconc_def)
--- a/src/HOL/Library/Extended_Nat.thy Tue Aug 02 07:36:58 2011 -0700
+++ b/src/HOL/Library/Extended_Nat.thy Tue Aug 02 08:28:34 2011 -0700
@@ -49,14 +49,14 @@
declare [[coercion "enat::nat\<Rightarrow>enat"]]
-lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
-by (cases x) auto
+lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
+ by (cases x) auto
lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
-by (cases x) auto
+ by (cases x) auto
primrec the_enat :: "enat \<Rightarrow> nat"
-where "the_enat (enat n) = n"
+ where "the_enat (enat n) = n"
subsection {* Constructors and numbers *}
@@ -76,8 +76,8 @@
end
-definition iSuc :: "enat \<Rightarrow> enat" where
- "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
+definition eSuc :: "enat \<Rightarrow> enat" where
+ "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
lemma enat_0: "enat 0 = 0"
by (simp add: zero_enat_def)
@@ -88,13 +88,13 @@
lemma enat_number: "enat (number_of k) = number_of k"
by (simp add: number_of_enat_def)
-lemma one_iSuc: "1 = iSuc 0"
- by (simp add: zero_enat_def one_enat_def iSuc_def)
+lemma one_eSuc: "1 = eSuc 0"
+ by (simp add: zero_enat_def one_enat_def eSuc_def)
-lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
+lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
by (simp add: zero_enat_def)
-lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
+lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
by (simp add: zero_enat_def)
lemma zero_enat_eq [simp]:
@@ -112,35 +112,35 @@
"\<not> 1 = (0\<Colon>enat)"
unfolding zero_enat_def one_enat_def by simp_all
-lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
+lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
by (simp add: one_enat_def)
-lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
+lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)"
by (simp add: one_enat_def)
-lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
+lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
by (simp add: number_of_enat_def)
-lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
+lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::enat)"
by (simp add: number_of_enat_def)
-lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
- by (simp add: iSuc_def)
+lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)"
+ by (simp add: eSuc_def)
-lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
- by (simp add: iSuc_enat number_of_enat_def)
+lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))"
+ by (simp add: eSuc_enat number_of_enat_def)
-lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
- by (simp add: iSuc_def)
+lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>"
+ by (simp add: eSuc_def)
-lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
- by (simp add: iSuc_def zero_enat_def split: enat.splits)
+lemma eSuc_ne_0 [simp]: "eSuc n \<noteq> 0"
+ by (simp add: eSuc_def zero_enat_def split: enat.splits)
-lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
- by (rule iSuc_ne_0 [symmetric])
+lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n"
+ by (rule eSuc_ne_0 [symmetric])
-lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
- by (simp add: iSuc_def split: enat.splits)
+lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
+ by (simp add: eSuc_def split: enat.splits)
lemma number_of_enat_inject [simp]:
"(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
@@ -184,28 +184,28 @@
else if l < Int.Pls then number_of k else number_of (k + l))"
unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
-lemma iSuc_number [simp]:
- "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
- unfolding iSuc_number_of
+lemma eSuc_number [simp]:
+ "eSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
+ unfolding eSuc_number_of
unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
-lemma iSuc_plus_1:
- "iSuc n = n + 1"
- by (cases n) (simp_all add: iSuc_enat one_enat_def)
+lemma eSuc_plus_1:
+ "eSuc n = n + 1"
+ by (cases n) (simp_all add: eSuc_enat one_enat_def)
-lemma plus_1_iSuc:
- "1 + q = iSuc q"
- "q + 1 = iSuc q"
-by (simp_all add: iSuc_plus_1 add_ac)
+lemma plus_1_eSuc:
+ "1 + q = eSuc q"
+ "q + 1 = eSuc q"
+ by (simp_all add: eSuc_plus_1 add_ac)
-lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
-by (simp_all add: iSuc_plus_1 add_ac)
+lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
+ by (simp_all add: eSuc_plus_1 add_ac)
-lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
-by (simp only: add_commute[of m] iadd_Suc)
+lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
+ by (simp only: add_commute[of m] iadd_Suc)
lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
-by (cases m, cases n, simp_all add: zero_enat_def)
+ by (cases m, cases n, simp_all add: zero_enat_def)
subsection {* Multiplication *}
@@ -251,16 +251,16 @@
end
-lemma mult_iSuc: "iSuc m * n = n + m * n"
- unfolding iSuc_plus_1 by (simp add: algebra_simps)
+lemma mult_eSuc: "eSuc m * n = n + m * n"
+ unfolding eSuc_plus_1 by (simp add: algebra_simps)
-lemma mult_iSuc_right: "m * iSuc n = m + m * n"
- unfolding iSuc_plus_1 by (simp add: algebra_simps)
+lemma mult_eSuc_right: "m * eSuc n = m + m * n"
+ unfolding eSuc_plus_1 by (simp add: algebra_simps)
lemma of_nat_eq_enat: "of_nat n = enat n"
apply (induct n)
apply (simp add: enat_0)
- apply (simp add: plus_1_iSuc iSuc_enat)
+ apply (simp add: plus_1_eSuc eSuc_enat)
done
instance enat :: number_semiring
@@ -274,11 +274,11 @@
then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
qed
-lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
-by(auto simp add: times_enat_def zero_enat_def split: enat.split)
+lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
+ by (auto simp add: times_enat_def zero_enat_def split: enat.split)
-lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
-by(auto simp add: times_enat_def zero_enat_def split: enat.split)
+lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
+ by (auto simp add: times_enat_def zero_enat_def split: enat.split)
subsection {* Subtraction *}
@@ -294,33 +294,33 @@
end
-lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
-by(simp add: diff_enat_def)
+lemma idiff_enat_enat [simp,code]: "enat a - enat b = enat (a - b)"
+ by (simp add: diff_enat_def)
-lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
-by(simp add: diff_enat_def)
+lemma idiff_infinity [simp,code]: "\<infinity> - n = (\<infinity>::enat)"
+ by (simp add: diff_enat_def)
-lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
-by(simp add: diff_enat_def)
+lemma idiff_infinity_right [simp,code]: "enat a - \<infinity> = 0"
+ by (simp add: diff_enat_def)
-lemma idiff_0[simp]: "(0::enat) - n = 0"
-by (cases n, simp_all add: zero_enat_def)
+lemma idiff_0 [simp]: "(0::enat) - n = 0"
+ by (cases n, simp_all add: zero_enat_def)
-lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
+lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def]
-lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
-by (cases n) (simp_all add: zero_enat_def)
+lemma idiff_0_right [simp]: "(n::enat) - 0 = n"
+ by (cases n) (simp_all add: zero_enat_def)
-lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
+lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def]
-lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
-by(auto simp: zero_enat_def)
+lemma idiff_self [simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
+ by (auto simp: zero_enat_def)
-lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
-by(simp add: iSuc_def split: enat.split)
+lemma eSuc_minus_eSuc [simp]: "eSuc n - eSuc m = n - m"
+ by (simp add: eSuc_def split: enat.split)
-lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
-by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
+lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
+ by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
@@ -378,58 +378,58 @@
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
-by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-
-lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
-lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
+lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
+ by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
+
+lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
by simp
lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
by (simp add: zero_enat_def less_enat_def split: enat.splits)
lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
-by (simp add: zero_enat_def less_enat_def split: enat.splits)
+ by (simp add: zero_enat_def less_enat_def split: enat.splits)
-lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
- by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
+lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
+ by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
-lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
- by (simp add: iSuc_def less_enat_def split: enat.splits)
+lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
+ by (simp add: eSuc_def less_enat_def split: enat.splits)
-lemma ile_iSuc [simp]: "n \<le> iSuc n"
- by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
+lemma ile_eSuc [simp]: "n \<le> eSuc n"
+ by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
-lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
- by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
+lemma not_eSuc_ilei0 [simp]: "\<not> eSuc n \<le> 0"
+ by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits)
-lemma i0_iless_iSuc [simp]: "0 < iSuc n"
- by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
+lemma i0_iless_eSuc [simp]: "0 < eSuc n"
+ by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits)
-lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
-by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
+lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)"
+ by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split)
-lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
- by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
+lemma ileI1: "m < n \<Longrightarrow> eSuc m \<le> n"
+ by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits)
lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
by (cases n) auto
-lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
- by (auto simp add: iSuc_def less_enat_def split: enat.splits)
+lemma iless_Suc_eq [simp]: "enat m < eSuc n \<longleftrightarrow> enat m \<le> n"
+ by (auto simp add: eSuc_def less_enat_def split: enat.splits)
-lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
-by (simp add: zero_enat_def less_enat_def split: enat.splits)
+lemma imult_infinity: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
+ by (simp add: zero_enat_def less_enat_def split: enat.splits)
-lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
-by (simp add: zero_enat_def less_enat_def split: enat.splits)
+lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
+ by (simp add: zero_enat_def less_enat_def split: enat.splits)
lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
-by (simp only: i0_less imult_is_0, simp)
+ by (simp only: i0_less imult_is_0, simp)
-lemma mono_iSuc: "mono iSuc"
-by(simp add: mono_def)
+lemma mono_eSuc: "mono eSuc"
+ by (simp add: mono_def)
lemma min_enat_simps [simp]:
@@ -462,7 +462,7 @@
apply (drule spec)
apply (erule exE)
apply (drule ileI1)
-apply (rule iSuc_enat [THEN subst])
+apply (rule eSuc_enat [THEN subst])
apply (rule exI)
apply (erule (1) le_less_trans)
done
@@ -500,7 +500,7 @@
"[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
by (induct n) auto
-lemma less_InftyE:
+lemma less_infinityE:
"[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
by (induct n) auto
@@ -519,7 +519,7 @@
next
show "P \<infinity>"
apply (rule prem, clarify)
- apply (erule less_InftyE)
+ apply (erule less_infinityE)
apply (simp add: P_enat)
done
qed
@@ -568,7 +568,7 @@
subsection {* Traditional theorem names *}
-lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
+lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def
plus_enat_def less_eq_enat_def less_enat_def
end