src/HOL/Library/Extended_Nat.thy
 changeset 44019 ee784502aed5 parent 43978 da7d04d4023c child 44890 22f665a2e91c
```     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Aug 02 07:36:58 2011 -0700
1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Aug 02 08:28:34 2011 -0700
1.3 @@ -49,14 +49,14 @@
1.4
1.5  declare [[coercion "enat::nat\<Rightarrow>enat"]]
1.6
1.7 -lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
1.8 -by (cases x) auto
1.9 +lemma not_infinity_eq [iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
1.10 +  by (cases x) auto
1.11
1.12  lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
1.13 -by (cases x) auto
1.14 +  by (cases x) auto
1.15
1.16  primrec the_enat :: "enat \<Rightarrow> nat"
1.17 -where "the_enat (enat n) = n"
1.18 +  where "the_enat (enat n) = n"
1.19
1.20  subsection {* Constructors and numbers *}
1.21
1.22 @@ -76,8 +76,8 @@
1.23
1.24  end
1.25
1.26 -definition iSuc :: "enat \<Rightarrow> enat" where
1.27 -  "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
1.28 +definition eSuc :: "enat \<Rightarrow> enat" where
1.29 +  "eSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
1.30
1.31  lemma enat_0: "enat 0 = 0"
1.33 @@ -88,13 +88,13 @@
1.34  lemma enat_number: "enat (number_of k) = number_of k"
1.36
1.37 -lemma one_iSuc: "1 = iSuc 0"
1.38 -  by (simp add: zero_enat_def one_enat_def iSuc_def)
1.39 +lemma one_eSuc: "1 = eSuc 0"
1.40 +  by (simp add: zero_enat_def one_enat_def eSuc_def)
1.41
1.42 -lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
1.43 +lemma infinity_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
1.45
1.46 -lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
1.47 +lemma i0_ne_infinity [simp]: "0 \<noteq> (\<infinity>::enat)"
1.49
1.50  lemma zero_enat_eq [simp]:
1.51 @@ -112,35 +112,35 @@
1.52    "\<not> 1 = (0\<Colon>enat)"
1.53    unfolding zero_enat_def one_enat_def by simp_all
1.54
1.55 -lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
1.56 +lemma infinity_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
1.58
1.59 -lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
1.60 +lemma i1_ne_infinity [simp]: "1 \<noteq> (\<infinity>::enat)"
1.62
1.63 -lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
1.64 +lemma infinity_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
1.66
1.67 -lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
1.68 +lemma number_ne_infinity [simp]: "number_of k \<noteq> (\<infinity>::enat)"
1.70
1.71 -lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
1.72 -  by (simp add: iSuc_def)
1.73 +lemma eSuc_enat: "eSuc (enat n) = enat (Suc n)"
1.74 +  by (simp add: eSuc_def)
1.75
1.76 -lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
1.77 -  by (simp add: iSuc_enat number_of_enat_def)
1.78 +lemma eSuc_number_of: "eSuc (number_of k) = enat (Suc (number_of k))"
1.79 +  by (simp add: eSuc_enat number_of_enat_def)
1.80
1.81 -lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
1.82 -  by (simp add: iSuc_def)
1.83 +lemma eSuc_infinity [simp]: "eSuc \<infinity> = \<infinity>"
1.84 +  by (simp add: eSuc_def)
1.85
1.86 -lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
1.87 -  by (simp add: iSuc_def zero_enat_def split: enat.splits)
1.88 +lemma eSuc_ne_0 [simp]: "eSuc n \<noteq> 0"
1.89 +  by (simp add: eSuc_def zero_enat_def split: enat.splits)
1.90
1.91 -lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
1.92 -  by (rule iSuc_ne_0 [symmetric])
1.93 +lemma zero_ne_eSuc [simp]: "0 \<noteq> eSuc n"
1.94 +  by (rule eSuc_ne_0 [symmetric])
1.95
1.96 -lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
1.97 -  by (simp add: iSuc_def split: enat.splits)
1.98 +lemma eSuc_inject [simp]: "eSuc m = eSuc n \<longleftrightarrow> m = n"
1.99 +  by (simp add: eSuc_def split: enat.splits)
1.100
1.101  lemma number_of_enat_inject [simp]:
1.102    "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
1.103 @@ -184,28 +184,28 @@
1.104      else if l < Int.Pls then number_of k else number_of (k + l))"
1.105    unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
1.106
1.107 -lemma iSuc_number [simp]:
1.108 -  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
1.109 -  unfolding iSuc_number_of
1.110 +lemma eSuc_number [simp]:
1.111 +  "eSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
1.112 +  unfolding eSuc_number_of
1.113    unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
1.114
1.115 -lemma iSuc_plus_1:
1.116 -  "iSuc n = n + 1"
1.117 -  by (cases n) (simp_all add: iSuc_enat one_enat_def)
1.118 +lemma eSuc_plus_1:
1.119 +  "eSuc n = n + 1"
1.120 +  by (cases n) (simp_all add: eSuc_enat one_enat_def)
1.121
1.122 -lemma plus_1_iSuc:
1.123 -  "1 + q = iSuc q"
1.124 -  "q + 1 = iSuc q"
1.126 +lemma plus_1_eSuc:
1.127 +  "1 + q = eSuc q"
1.128 +  "q + 1 = eSuc q"
1.130
1.131 -lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
1.133 +lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
1.135
1.136 -lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
1.138 +lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
1.140
1.141  lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
1.142 -by (cases m, cases n, simp_all add: zero_enat_def)
1.143 +  by (cases m, cases n, simp_all add: zero_enat_def)
1.144
1.145  subsection {* Multiplication *}
1.146
1.147 @@ -251,16 +251,16 @@
1.148
1.149  end
1.150
1.151 -lemma mult_iSuc: "iSuc m * n = n + m * n"
1.152 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
1.153 +lemma mult_eSuc: "eSuc m * n = n + m * n"
1.154 +  unfolding eSuc_plus_1 by (simp add: algebra_simps)
1.155
1.156 -lemma mult_iSuc_right: "m * iSuc n = m + m * n"
1.157 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
1.158 +lemma mult_eSuc_right: "m * eSuc n = m + m * n"
1.159 +  unfolding eSuc_plus_1 by (simp add: algebra_simps)
1.160
1.161  lemma of_nat_eq_enat: "of_nat n = enat n"
1.162    apply (induct n)
1.164 -  apply (simp add: plus_1_iSuc iSuc_enat)
1.165 +  apply (simp add: plus_1_eSuc eSuc_enat)
1.166    done
1.167
1.168  instance enat :: number_semiring
1.169 @@ -274,11 +274,11 @@
1.170    then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
1.171  qed
1.172
1.173 -lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
1.174 -by(auto simp add: times_enat_def zero_enat_def split: enat.split)
1.175 +lemma imult_is_0 [simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
1.176 +  by (auto simp add: times_enat_def zero_enat_def split: enat.split)
1.177
1.178 -lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
1.179 -by(auto simp add: times_enat_def zero_enat_def split: enat.split)
1.180 +lemma imult_is_infinity: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
1.181 +  by (auto simp add: times_enat_def zero_enat_def split: enat.split)
1.182
1.183
1.184  subsection {* Subtraction *}
1.185 @@ -294,33 +294,33 @@
1.186
1.187  end
1.188
1.189 -lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
1.191 +lemma idiff_enat_enat [simp,code]: "enat a - enat b = enat (a - b)"
1.192 +  by (simp add: diff_enat_def)
1.193
1.194 -lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
1.196 +lemma idiff_infinity [simp,code]: "\<infinity> - n = (\<infinity>::enat)"
1.197 +  by (simp add: diff_enat_def)
1.198
1.199 -lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
1.201 +lemma idiff_infinity_right [simp,code]: "enat a - \<infinity> = 0"
1.202 +  by (simp add: diff_enat_def)
1.203
1.204 -lemma idiff_0[simp]: "(0::enat) - n = 0"
1.205 -by (cases n, simp_all add: zero_enat_def)
1.206 +lemma idiff_0 [simp]: "(0::enat) - n = 0"
1.207 +  by (cases n, simp_all add: zero_enat_def)
1.208
1.209 -lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
1.210 +lemmas idiff_enat_0 [simp] = idiff_0 [unfolded zero_enat_def]
1.211
1.212 -lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
1.213 -by (cases n) (simp_all add: zero_enat_def)
1.214 +lemma idiff_0_right [simp]: "(n::enat) - 0 = n"
1.215 +  by (cases n) (simp_all add: zero_enat_def)
1.216
1.217 -lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
1.218 +lemmas idiff_enat_0_right [simp] = idiff_0_right [unfolded zero_enat_def]
1.219
1.220 -lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
1.221 -by(auto simp: zero_enat_def)
1.222 +lemma idiff_self [simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
1.223 +  by (auto simp: zero_enat_def)
1.224
1.225 -lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
1.226 -by(simp add: iSuc_def split: enat.split)
1.227 +lemma eSuc_minus_eSuc [simp]: "eSuc n - eSuc m = n - m"
1.228 +  by (simp add: eSuc_def split: enat.split)
1.229
1.230 -lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
1.231 -by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
1.232 +lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
1.233 +  by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
1.234
1.235  (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
1.236
1.237 @@ -378,58 +378,58 @@
1.238    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
1.239
1.240  lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
1.241 -by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
1.242 -
1.243 -lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
1.244    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
1.245
1.246 -lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
1.247 +lemma infinity_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
1.248 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
1.249 +
1.250 +lemma infinity_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
1.251    by simp
1.252
1.253  lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
1.254    by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.255
1.256  lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
1.257 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.258 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.259
1.260 -lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
1.261 -  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
1.262 +lemma eSuc_ile_mono [simp]: "eSuc n \<le> eSuc m \<longleftrightarrow> n \<le> m"
1.263 +  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
1.264
1.265 -lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
1.266 -  by (simp add: iSuc_def less_enat_def split: enat.splits)
1.267 +lemma eSuc_mono [simp]: "eSuc n < eSuc m \<longleftrightarrow> n < m"
1.268 +  by (simp add: eSuc_def less_enat_def split: enat.splits)
1.269
1.270 -lemma ile_iSuc [simp]: "n \<le> iSuc n"
1.271 -  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
1.272 +lemma ile_eSuc [simp]: "n \<le> eSuc n"
1.273 +  by (simp add: eSuc_def less_eq_enat_def split: enat.splits)
1.274
1.275 -lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
1.276 -  by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
1.277 +lemma not_eSuc_ilei0 [simp]: "\<not> eSuc n \<le> 0"
1.278 +  by (simp add: zero_enat_def eSuc_def less_eq_enat_def split: enat.splits)
1.279
1.280 -lemma i0_iless_iSuc [simp]: "0 < iSuc n"
1.281 -  by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
1.282 +lemma i0_iless_eSuc [simp]: "0 < eSuc n"
1.283 +  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.splits)
1.284
1.285 -lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
1.286 -by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
1.287 +lemma iless_eSuc0[simp]: "(n < eSuc 0) = (n = 0)"
1.288 +  by (simp add: zero_enat_def eSuc_def less_enat_def split: enat.split)
1.289
1.290 -lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
1.291 -  by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
1.292 +lemma ileI1: "m < n \<Longrightarrow> eSuc m \<le> n"
1.293 +  by (simp add: eSuc_def less_eq_enat_def less_enat_def split: enat.splits)
1.294
1.295  lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
1.296    by (cases n) auto
1.297
1.298 -lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
1.299 -  by (auto simp add: iSuc_def less_enat_def split: enat.splits)
1.300 +lemma iless_Suc_eq [simp]: "enat m < eSuc n \<longleftrightarrow> enat m \<le> n"
1.301 +  by (auto simp add: eSuc_def less_enat_def split: enat.splits)
1.302
1.303 -lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
1.304 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.305 +lemma imult_infinity: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
1.306 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.307
1.308 -lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
1.309 -by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.310 +lemma imult_infinity_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
1.311 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
1.312
1.313  lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
1.314 -by (simp only: i0_less imult_is_0, simp)
1.315 +  by (simp only: i0_less imult_is_0, simp)
1.316
1.317 -lemma mono_iSuc: "mono iSuc"
1.319 +lemma mono_eSuc: "mono eSuc"
1.320 +  by (simp add: mono_def)
1.321
1.322
1.323  lemma min_enat_simps [simp]:
1.324 @@ -462,7 +462,7 @@
1.325  apply (drule spec)
1.326  apply (erule exE)
1.327  apply (drule ileI1)
1.328 -apply (rule iSuc_enat [THEN subst])
1.329 +apply (rule eSuc_enat [THEN subst])
1.330  apply (rule exI)
1.331  apply (erule (1) le_less_trans)
1.332  done
1.333 @@ -500,7 +500,7 @@
1.334    "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
1.335  by (induct n) auto
1.336
1.337 -lemma less_InftyE:
1.338 +lemma less_infinityE:
1.339    "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
1.340  by (induct n) auto
1.341
1.342 @@ -519,7 +519,7 @@
1.343    next
1.344      show "P \<infinity>"
1.345        apply (rule prem, clarify)
1.346 -      apply (erule less_InftyE)
1.347 +      apply (erule less_infinityE)