Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
authorhuffman
Tue Aug 02 08:28:34 2011 -0700 (2011-08-02)
changeset 44019ee784502aed5
parent 44018 d34f0cd62164
child 44020 376c1e7b320c
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
NEWS
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/NEWS	Tue Aug 02 07:36:58 2011 -0700
     1.2 +++ b/NEWS	Tue Aug 02 08:28:34 2011 -0700
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5  * Class complete_lattice: generalized a couple of lemmas from sets;
     1.6  generalized theorems INF_cong and SUP_cong.  New type classes for complete
     1.7 -boolean algebras and complete linear orderes.  Lemmas Inf_less_iff,
     1.8 +boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
     1.9  less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
    1.10  More consistent and less misunderstandable names:
    1.11    INFI_def ~> INF_def
    1.12 @@ -83,7 +83,7 @@
    1.13  to UNION any longer;  these have been moved to collection UN_ball_bex_simps.
    1.14  INCOMPATIBILITY.
    1.15  
    1.16 -* Archimedian_Field.thy:
    1.17 +* Archimedean_Field.thy:
    1.18      floor now is defined as parameter of a separate type class floor_ceiling.
    1.19   
    1.20  * Finite_Set.thy: more coherent development of fold_set locales:
    1.21 @@ -157,6 +157,16 @@
    1.22  * Well-founded recursion combinator "wfrec" has been moved to
    1.23  Library/Wfrec.thy. INCOMPATIBILITY.
    1.24  
    1.25 +* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat.
    1.26 +The names of the following types and constants have changed:
    1.27 +  inat (type) ~> enat
    1.28 +  Fin         ~> enat
    1.29 +  Infty       ~> infinity (overloaded)
    1.30 +  iSuc        ~> eSuc
    1.31 +  the_Fin     ~> the_enat
    1.32 +Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
    1.33 +been renamed accordingly.
    1.34 +
    1.35  
    1.36  *** Document preparation ***
    1.37  
     2.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Aug 02 07:36:58 2011 -0700
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Tue Aug 02 08:28:34 2011 -0700
     2.3 @@ -140,7 +140,7 @@
     2.4  
     2.5  section "slen"
     2.6  
     2.7 -lemma slen_fscons: "#(m~> s) = iSuc (#s)"
     2.8 +lemma slen_fscons: "#(m~> s) = eSuc (#s)"
     2.9  by (simp add: fscons_def)
    2.10  
    2.11  lemma slen_fscons_eq:
     3.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Aug 02 07:36:58 2011 -0700
     3.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Aug 02 08:28:34 2011 -0700
     3.3 @@ -57,12 +57,12 @@
     3.4  lemma slen_fsingleton[simp]: "#(<a>) = enat 1"
     3.5  by (simp add: fsingleton_def2 enat_defs)
     3.6  
     3.7 -lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
     3.8 +lemma slen_fstreams[simp]: "#(<a> ooo s) = eSuc (#s)"
     3.9  by (simp add: fsingleton_def2)
    3.10  
    3.11 -lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
    3.12 +lemma slen_fstreams2[simp]: "#(s ooo <a>) = eSuc (#s)"
    3.13  apply (cases "#s")
    3.14 -apply (auto simp add: iSuc_enat)
    3.15 +apply (auto simp add: eSuc_enat)
    3.16  apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
    3.17  by (simp add: sconc_def)
    3.18  
     4.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Aug 02 07:36:58 2011 -0700
     4.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Aug 02 08:28:34 2011 -0700
     4.3 @@ -132,8 +132,8 @@
     4.4  apply (erule allE, erule allE, drule mp) (* stream_monoP *)
     4.5  apply ( drule ileI1)
     4.6  apply ( drule order_trans)
     4.7 -apply (  rule ile_iSuc)
     4.8 -apply ( drule iSuc_ile_mono [THEN iffD1])
     4.9 +apply (  rule ile_eSuc)
    4.10 +apply ( drule eSuc_ile_mono [THEN iffD1])
    4.11  apply ( assumption)
    4.12  apply (drule mp)
    4.13  apply ( erule is_ub_thelub)
     5.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Aug 02 07:36:58 2011 -0700
     5.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Aug 02 08:28:34 2011 -0700
     5.3 @@ -329,10 +329,10 @@
     5.4  lemma slen_empty [simp]: "#\<bottom> = 0"
     5.5  by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
     5.6  
     5.7 -lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
     5.8 +lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = eSuc (#xs)"
     5.9  apply (case_tac "stream_finite (x && xs)")
    5.10  apply (simp add: slen_def, auto)
    5.11 -apply (simp add: stream.finite_def, auto simp add: iSuc_enat)
    5.12 +apply (simp add: stream.finite_def, auto simp add: eSuc_enat)
    5.13  apply (rule Least_Suc2, auto)
    5.14  (*apply (drule sym)*)
    5.15  (*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
    5.16 @@ -341,7 +341,7 @@
    5.17  by (drule stream_finite_lemma1,auto)
    5.18  
    5.19  lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \<bottom>)"
    5.20 -by (cases x, auto simp add: enat_0 iSuc_enat[THEN sym])
    5.21 +by (cases x, auto simp add: enat_0 eSuc_enat[THEN sym])
    5.22  
    5.23  lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
    5.24  by (cases x, auto)
    5.25 @@ -353,7 +353,7 @@
    5.26  apply (case_tac "#y") apply simp_all
    5.27  done
    5.28  
    5.29 -lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y &  a ~= \<bottom> &  #y = n)"
    5.30 +lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y &  a ~= \<bottom> &  #y = n)"
    5.31  by (cases x, auto)
    5.32  
    5.33  lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
    5.34 @@ -362,15 +362,15 @@
    5.35  lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < enat (Suc n))"
    5.36   apply (cases x, auto)
    5.37     apply (simp add: zero_enat_def)
    5.38 -  apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
    5.39 - apply (case_tac "#stream") apply (simp_all add: iSuc_enat)
    5.40 +  apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
    5.41 + apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
    5.42  done
    5.43  
    5.44  lemma slen_take_lemma4 [rule_format]:
    5.45    "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n"
    5.46  apply (induct n, auto simp add: enat_0)
    5.47  apply (case_tac "s=UU", simp)
    5.48 -by (drule stream_exhaust_eq [THEN iffD1], auto simp add: iSuc_enat)
    5.49 +by (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat)
    5.50  
    5.51  (*
    5.52  lemma stream_take_idempotent [simp]:
    5.53 @@ -398,7 +398,7 @@
    5.54  apply (case_tac "x=UU", simp)
    5.55  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
    5.56  apply (erule_tac x="y" in allE, auto)
    5.57 -apply (simp_all add: not_less iSuc_enat)
    5.58 +apply (simp_all add: not_less eSuc_enat)
    5.59  apply (case_tac "#y") apply simp_all
    5.60  apply (case_tac "x=UU", simp)
    5.61  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
    5.62 @@ -448,7 +448,7 @@
    5.63  apply (case_tac "x=UU", auto simp add: zero_enat_def)
    5.64  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    5.65  apply (erule_tac x="y" in allE, auto)
    5.66 -apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_enat)
    5.67 +apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat)
    5.68  by (simp add: iterate_lemma)
    5.69  
    5.70  lemma slen_take_lemma3 [rule_format]:
    5.71 @@ -478,7 +478,7 @@
    5.72  apply (subgoal_tac "stream_take n$s ~=s")
    5.73   apply (insert slen_take_lemma4 [of n s],auto)
    5.74  apply (cases s, simp)
    5.75 -by (simp add: slen_take_lemma4 iSuc_enat)
    5.76 +by (simp add: slen_take_lemma4 eSuc_enat)
    5.77  
    5.78  (* ----------------------------------------------------------------------- *)
    5.79  (* theorems about smap                                                     *)
    5.80 @@ -593,12 +593,12 @@
    5.81   apply (erule_tac x="k" in allE)
    5.82   apply (erule_tac x="y" in allE,auto)
    5.83   apply (erule_tac x="THE p. Suc p = t" in allE,auto)
    5.84 -   apply (simp add: iSuc_def split: enat.splits)
    5.85 -  apply (simp add: iSuc_def split: enat.splits)
    5.86 +   apply (simp add: eSuc_def split: enat.splits)
    5.87 +  apply (simp add: eSuc_def split: enat.splits)
    5.88    apply (simp only: the_equality)
    5.89 - apply (simp add: iSuc_def split: enat.splits)
    5.90 + apply (simp add: eSuc_def split: enat.splits)
    5.91   apply force
    5.92 -apply (simp add: iSuc_def split: enat.splits)
    5.93 +apply (simp add: eSuc_def split: enat.splits)
    5.94  done
    5.95  
    5.96  lemma take_i_rt_len:
    5.97 @@ -696,7 +696,7 @@
    5.98  by auto
    5.99  
   5.100  lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
   5.101 -apply (simp add: sconc_def zero_enat_def iSuc_def split: enat.splits, auto)
   5.102 +apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto)
   5.103  apply (rule someI2_ex,auto)
   5.104   apply (rule_tac x="x && y" in exI,auto)
   5.105  apply (simp add: i_rt_Suc_forw)
   5.106 @@ -709,7 +709,7 @@
   5.107   apply (rule stream_finite_ind [of x],auto)
   5.108    apply (simp add: stream.finite_def)
   5.109    apply (drule slen_take_lemma1,blast)
   5.110 - apply (simp_all add: zero_enat_def iSuc_def split: enat.splits)
   5.111 + apply (simp_all add: zero_enat_def eSuc_def split: enat.splits)
   5.112  apply (erule_tac x="y" in allE,auto)
   5.113  by (rule_tac x="a && w" in exI,auto)
   5.114  
   5.115 @@ -743,7 +743,7 @@
   5.116  
   5.117  lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
   5.118  apply (cases "#x",auto)
   5.119 - apply (simp add: sconc_def iSuc_enat)
   5.120 + apply (simp add: sconc_def eSuc_enat)
   5.121   apply (rule someI2_ex)
   5.122    apply (drule ex_sconc, simp)
   5.123   apply (rule someI2_ex, auto)
   5.124 @@ -870,9 +870,9 @@
   5.125  
   5.126  lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
   5.127  apply auto
   5.128 -  apply (metis not_Infty_eq slen_sconc_finite1)
   5.129 - apply (metis not_Infty_eq slen_sconc_infinite1)
   5.130 -apply (metis not_Infty_eq slen_sconc_infinite2)
   5.131 +  apply (metis not_infinity_eq slen_sconc_finite1)
   5.132 + apply (metis not_infinity_eq slen_sconc_infinite1)
   5.133 +apply (metis not_infinity_eq slen_sconc_infinite2)
   5.134  done
   5.135  
   5.136  (* ----------------------------------------------------------------------- *)
   5.137 @@ -956,7 +956,7 @@
   5.138    defer 1
   5.139    apply (simp add: constr_sconc_def del: scons_sconc)
   5.140    apply (case_tac "#s")
   5.141 -   apply (simp add: iSuc_enat)
   5.142 +   apply (simp add: eSuc_enat)
   5.143     apply (case_tac "a=UU",auto simp del: scons_sconc)
   5.144     apply (simp)
   5.145    apply (simp add: sconc_def)
     6.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Aug 02 07:36:58 2011 -0700
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Aug 02 08:28:34 2011 -0700
     6.3 @@ -49,14 +49,14 @@
     6.4  
     6.5  declare [[coercion "enat::nat\<Rightarrow>enat"]]
     6.6  
     6.7 -lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
     6.8 -by (cases x) auto
     6.9 +lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
    6.10 +  by (cases x) auto
    6.11  
    6.12  lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
    6.13 -by (cases x) auto
    6.14 +  by (cases x) auto
    6.15  
    6.16  primrec the_enat :: "enat \<Rightarrow> nat"
    6.17 -where "the_enat (enat n) = n"
    6.18 +  where "the_enat (enat n) = n"
    6.19  
    6.20  subsection {* Constructors and numbers *}
    6.21  
    6.22 @@ -76,8 +76,8 @@
    6.23  
    6.24  end
    6.25  
    6.26 -definition iSuc :: "enat \<Rightarrow> enat" where
    6.27 -  "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    6.28 +definition eSuc :: "enat \<Rightarrow> enat" where
    6.29 +  "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    6.30  
    6.31  lemma enat_0: "enat 0 = 0"
    6.32    by (simp add: zero_enat_def)
    6.33 @@ -88,13 +88,13 @@
    6.34  lemma enat_number: "enat (number_of k) = number_of k"
    6.35    by (simp add: number_of_enat_def)
    6.36  
    6.37 -lemma one_iSuc: "1 = iSuc 0"
    6.38 -  by (simp add: zero_enat_def one_enat_def iSuc_def)
    6.39 +lemma one_eSuc: "1 = eSuc 0"
    6.40 +  by (simp add: zero_enat_def one_enat_def eSuc_def)
    6.41  
    6.42 -lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
    6.43 +lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
    6.44    by (simp add: zero_enat_def)
    6.45  
    6.46 -lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
    6.47 +lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
    6.48    by (simp add: zero_enat_def)
    6.49  
    6.50  lemma zero_enat_eq [simp]:
    6.51 @@ -112,35 +112,35 @@
    6.52    "\<not> 1 = (0\<Colon>enat)"
    6.53    unfolding zero_enat_def one_enat_def by simp_all
    6.54  
    6.55 -lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
    6.56 +lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
    6.57    by (simp add: one_enat_def)
    6.58  
    6.59 -lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
    6.60 +lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)"
    6.61    by (simp add: one_enat_def)
    6.62  
    6.63 -lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
    6.64 +lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
    6.65    by (simp add: number_of_enat_def)
    6.66  
    6.67 -lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
    6.68 +lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::enat)"
    6.69    by (simp add: number_of_enat_def)
    6.70  
    6.71 -lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
    6.72 -  by (simp add: iSuc_def)
    6.73 +lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)"
    6.74 +  by (simp add: eSuc_def)
    6.75  
    6.76 -lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
    6.77 -  by (simp add: iSuc_enat number_of_enat_def)
    6.78 +lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))"
    6.79 +  by (simp add: eSuc_enat number_of_enat_def)
    6.80  
    6.81 -lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    6.82 -  by (simp add: iSuc_def)
    6.83 +lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>"
    6.84 +  by (simp add: eSuc_def)
    6.85  
    6.86 -lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    6.87 -  by (simp add: iSuc_def zero_enat_def split: enat.splits)
    6.88 +lemma eSuc_ne_0 [simp]: "eSuc n \<noteq> 0"
    6.89 +  by (simp add: eSuc_def zero_enat_def split: enat.splits)
    6.90  
    6.91 -lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
    6.92 -  by (rule iSuc_ne_0 [symmetric])
    6.93 +lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n"
    6.94 +  by (rule eSuc_ne_0 [symmetric])
    6.95  
    6.96 -lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
    6.97 -  by (simp add: iSuc_def split: enat.splits)
    6.98 +lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
    6.99 +  by (simp add: eSuc_def split: enat.splits)
   6.100  
   6.101  lemma number_of_enat_inject [simp]:
   6.102    "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
   6.103 @@ -184,28 +184,28 @@
   6.104      else if l < Int.Pls then number_of k else number_of (k + l))"
   6.105    unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
   6.106  
   6.107 -lemma iSuc_number [simp]:
   6.108 -  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   6.109 -  unfolding iSuc_number_of
   6.110 +lemma eSuc_number [simp]:
   6.111 +  "eSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   6.112 +  unfolding eSuc_number_of
   6.113    unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
   6.114  
   6.115 -lemma iSuc_plus_1:
   6.116 -  "iSuc n = n + 1"
   6.117 -  by (cases n) (simp_all add: iSuc_enat one_enat_def)
   6.118 +lemma eSuc_plus_1:
   6.119 +  "eSuc n = n + 1"
   6.120 +  by (cases n) (simp_all add: eSuc_enat one_enat_def)
   6.121    
   6.122 -lemma plus_1_iSuc:
   6.123 -  "1 + q = iSuc q"
   6.124 -  "q + 1 = iSuc q"
   6.125 -by (simp_all add: iSuc_plus_1 add_ac)
   6.126 +lemma plus_1_eSuc:
   6.127 +  "1 + q = eSuc q"
   6.128 +  "q + 1 = eSuc q"
   6.129 +  by (simp_all add: eSuc_plus_1 add_ac)
   6.130  
   6.131 -lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   6.132 -by (simp_all add: iSuc_plus_1 add_ac)
   6.133 +lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
   6.134 +  by (simp_all add: eSuc_plus_1 add_ac)
   6.135  
   6.136 -lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   6.137 -by (simp only: add_commute[of m] iadd_Suc)
   6.138 +lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
   6.139 +  by (simp only: add_commute[of m] iadd_Suc)
   6.140  
   6.141  lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
   6.142 -by (cases m, cases n, simp_all add: zero_enat_def)
   6.143 +  by (cases m, cases n, simp_all add: zero_enat_def)
   6.144  
   6.145  subsection {* Multiplication *}
   6.146  
   6.147 @@ -251,16 +251,16 @@
   6.148  
   6.149  end
   6.150  
   6.151 -lemma mult_iSuc: "iSuc m * n = n + m * n"
   6.152 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   6.153 +lemma mult_eSuc: "eSuc m * n = n + m * n"
   6.154 +  unfolding eSuc_plus_1 by (simp add: algebra_simps)
   6.155  
   6.156 -lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   6.157 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   6.158 +lemma mult_eSuc_right: "m * eSuc n = m + m * n"
   6.159 +  unfolding eSuc_plus_1 by (simp add: algebra_simps)
   6.160  
   6.161  lemma of_nat_eq_enat: "of_nat n = enat n"
   6.162    apply (induct n)
   6.163    apply (simp add: enat_0)
   6.164 -  apply (simp add: plus_1_iSuc iSuc_enat)
   6.165 +  apply (simp add: plus_1_eSuc eSuc_enat)
   6.166    done
   6.167  
   6.168  instance enat :: number_semiring
   6.169 @@ -274,11 +274,11 @@
   6.170    then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
   6.171  qed
   6.172  
   6.173 -lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   6.174 -by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.175 +lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   6.176 +  by (auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.177  
   6.178 -lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   6.179 -by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.180 +lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   6.181 +  by (auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.182  
   6.183  
   6.184  subsection {* Subtraction *}
   6.185 @@ -294,33 +294,33 @@
   6.186  
   6.187  end
   6.188  
   6.189 -lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
   6.190 -by(simp add: diff_enat_def)
   6.191 +lemma idiff_enat_enat [simp,code]: "enat a - enat b = enat (a - b)"
   6.192 +  by (simp add: diff_enat_def)
   6.193  
   6.194 -lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   6.195 -by(simp add: diff_enat_def)
   6.196 +lemma idiff_infinity [simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   6.197 +  by (simp add: diff_enat_def)
   6.198  
   6.199 -lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
   6.200 -by(simp add: diff_enat_def)
   6.201 +lemma idiff_infinity_right [simp,code]: "enat a - \<infinity> = 0"
   6.202 +  by (simp add: diff_enat_def)
   6.203  
   6.204 -lemma idiff_0[simp]: "(0::enat) - n = 0"
   6.205 -by (cases n, simp_all add: zero_enat_def)
   6.206 +lemma idiff_0 [simp]: "(0::enat) - n = 0"
   6.207 +  by (cases n, simp_all add: zero_enat_def)
   6.208  
   6.209 -lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
   6.210 +lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def]
   6.211  
   6.212 -lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   6.213 -by (cases n) (simp_all add: zero_enat_def)
   6.214 +lemma idiff_0_right [simp]: "(n::enat) - 0 = n"
   6.215 +  by (cases n) (simp_all add: zero_enat_def)
   6.216  
   6.217 -lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   6.218 +lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def]
   6.219  
   6.220 -lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   6.221 -by(auto simp: zero_enat_def)
   6.222 +lemma idiff_self [simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   6.223 +  by (auto simp: zero_enat_def)
   6.224  
   6.225 -lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
   6.226 -by(simp add: iSuc_def split: enat.split)
   6.227 +lemma eSuc_minus_eSuc [simp]: "eSuc n - eSuc m = n - m"
   6.228 +  by (simp add: eSuc_def split: enat.split)
   6.229  
   6.230 -lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   6.231 -by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
   6.232 +lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
   6.233 +  by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
   6.234  
   6.235  (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
   6.236  
   6.237 @@ -378,58 +378,58 @@
   6.238    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.239  
   6.240  lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   6.241 -by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.242 -
   6.243 -lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   6.244    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.245  
   6.246 -lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   6.247 +lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   6.248 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.249 +
   6.250 +lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   6.251    by simp
   6.252  
   6.253  lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   6.254    by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.255  
   6.256  lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
   6.257 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.258 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.259  
   6.260 -lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
   6.261 -  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   6.262 +lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
   6.263 +  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
   6.264   
   6.265 -lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
   6.266 -  by (simp add: iSuc_def less_enat_def split: enat.splits)
   6.267 +lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
   6.268 +  by (simp add: eSuc_def less_enat_def split: enat.splits)
   6.269  
   6.270 -lemma ile_iSuc [simp]: "n \<le> iSuc n"
   6.271 -  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   6.272 +lemma ile_eSuc [simp]: "n \<le> eSuc n"
   6.273 +  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
   6.274  
   6.275 -lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   6.276 -  by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
   6.277 +lemma not_eSuc_ilei0 [simp]: "\<not> eSuc n \<le> 0"
   6.278 +  by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits)
   6.279  
   6.280 -lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   6.281 -  by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
   6.282 +lemma i0_iless_eSuc [simp]: "0 < eSuc n"
   6.283 +  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits)
   6.284  
   6.285 -lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
   6.286 -by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
   6.287 +lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)"
   6.288 +  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split)
   6.289  
   6.290 -lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   6.291 -  by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   6.292 +lemma ileI1: "m < n \<Longrightarrow> eSuc m \<le> n"
   6.293 +  by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   6.294  
   6.295  lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
   6.296    by (cases n) auto
   6.297  
   6.298 -lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
   6.299 -  by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   6.300 +lemma iless_Suc_eq [simp]: "enat m < eSuc n \<longleftrightarrow> enat m \<le> n"
   6.301 +  by (auto simp add: eSuc_def less_enat_def split: enat.splits)
   6.302  
   6.303 -lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   6.304 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.305 +lemma imult_infinity: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   6.306 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.307  
   6.308 -lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   6.309 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.310 +lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   6.311 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.312  
   6.313  lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
   6.314 -by (simp only: i0_less imult_is_0, simp)
   6.315 +  by (simp only: i0_less imult_is_0, simp)
   6.316  
   6.317 -lemma mono_iSuc: "mono iSuc"
   6.318 -by(simp add: mono_def)
   6.319 +lemma mono_eSuc: "mono eSuc"
   6.320 +  by (simp add: mono_def)
   6.321  
   6.322  
   6.323  lemma min_enat_simps [simp]:
   6.324 @@ -462,7 +462,7 @@
   6.325  apply (drule spec)
   6.326  apply (erule exE)
   6.327  apply (drule ileI1)
   6.328 -apply (rule iSuc_enat [THEN subst])
   6.329 +apply (rule eSuc_enat [THEN subst])
   6.330  apply (rule exI)
   6.331  apply (erule (1) le_less_trans)
   6.332  done
   6.333 @@ -500,7 +500,7 @@
   6.334    "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
   6.335  by (induct n) auto
   6.336  
   6.337 -lemma less_InftyE:
   6.338 +lemma less_infinityE:
   6.339    "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
   6.340  by (induct n) auto
   6.341  
   6.342 @@ -519,7 +519,7 @@
   6.343    next
   6.344      show "P \<infinity>"
   6.345        apply (rule prem, clarify)
   6.346 -      apply (erule less_InftyE)
   6.347 +      apply (erule less_infinityE)
   6.348        apply (simp add: P_enat)
   6.349        done
   6.350    qed
   6.351 @@ -568,7 +568,7 @@
   6.352  
   6.353  subsection {* Traditional theorem names *}
   6.354  
   6.355 -lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   6.356 +lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def
   6.357    plus_enat_def less_eq_enat_def less_enat_def
   6.358  
   6.359  end