# HG changeset patch
# User huffman
# Date 1312298914 25200
# Node ID ee784502aed5c0186ec7b53919d660d7ac2a357a
# Parent  d34f0cd621648cab9dcbe598c8f8e70dd016eec2
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names

diff -r d34f0cd62164 -r ee784502aed5 NEWS
--- 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 ***
 
diff -r d34f0cd62164 -r ee784502aed5 src/HOL/HOLCF/FOCUS/Fstream.thy
--- 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:
diff -r d34f0cd62164 -r ee784502aed5 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- 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)
 
diff -r d34f0cd62164 -r ee784502aed5 src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- 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)
diff -r d34f0cd62164 -r ee784502aed5 src/HOL/HOLCF/Library/Stream.thy
--- 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)
diff -r d34f0cd62164 -r ee784502aed5 src/HOL/Library/Extended_Nat.thy
--- 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