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