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.32    by (simp add: zero_enat_def)
    1.33 @@ -88,13 +88,13 @@
    1.34  lemma enat_number: "enat (number_of k) = number_of k"
    1.35    by (simp add: number_of_enat_def)
    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.44    by (simp add: zero_enat_def)
    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.48    by (simp add: zero_enat_def)
    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.57    by (simp add: one_enat_def)
    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.61    by (simp add: one_enat_def)
    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.65    by (simp add: number_of_enat_def)
    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.69    by (simp add: number_of_enat_def)
    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.125 -by (simp_all add: iSuc_plus_1 add_ac)
   1.126 +lemma plus_1_eSuc:
   1.127 +  "1 + q = eSuc q"
   1.128 +  "q + 1 = eSuc q"
   1.129 +  by (simp_all add: eSuc_plus_1 add_ac)
   1.130  
   1.131 -lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   1.132 -by (simp_all add: iSuc_plus_1 add_ac)
   1.133 +lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
   1.134 +  by (simp_all add: eSuc_plus_1 add_ac)
   1.135  
   1.136 -lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   1.137 -by (simp only: add_commute[of m] iadd_Suc)
   1.138 +lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
   1.139 +  by (simp only: add_commute[of m] iadd_Suc)
   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.163    apply (simp add: enat_0)
   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.190 -by(simp add: diff_enat_def)
   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.195 -by(simp add: diff_enat_def)
   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.200 -by(simp add: diff_enat_def)
   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.318 -by(simp add: mono_def)
   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)
   1.348        apply (simp add: P_enat)
   1.349        done
   1.350    qed
   1.351 @@ -568,7 +568,7 @@
   1.352  
   1.353  subsection {* Traditional theorem names *}
   1.354  
   1.355 -lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   1.356 +lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def eSuc_def
   1.357    plus_enat_def less_eq_enat_def less_enat_def
   1.358  
   1.359  end