src/HOL/Library/Extended_Nat.thy
changeset 43919 a7e4fb1a0502
parent 43532 d32d72ea3215
child 43921 e8511be08ddd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -0,0 +1,551 @@
     1.4 +(*  Title:      HOL/Library/Extended_Nat.thy
     1.5 +    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
     1.6 +    Contributions: David Trachtenherz, TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Extended natural numbers (i.e. with infinity) *}
    1.10 +
    1.11 +theory Extended_Nat
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +subsection {* Type definition *}
    1.16 +
    1.17 +text {*
    1.18 +  We extend the standard natural numbers by a special value indicating
    1.19 +  infinity.
    1.20 +*}
    1.21 +
    1.22 +datatype enat = Fin nat | Infty
    1.23 +
    1.24 +notation (xsymbols)
    1.25 +  Infty  ("\<infinity>")
    1.26 +
    1.27 +notation (HTML output)
    1.28 +  Infty  ("\<infinity>")
    1.29 +
    1.30 +
    1.31 +lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
    1.32 +by (cases x) auto
    1.33 +
    1.34 +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
    1.35 +by (cases x) auto
    1.36 +
    1.37 +
    1.38 +primrec the_Fin :: "enat \<Rightarrow> nat"
    1.39 +where "the_Fin (Fin n) = n"
    1.40 +
    1.41 +
    1.42 +subsection {* Constructors and numbers *}
    1.43 +
    1.44 +instantiation enat :: "{zero, one, number}"
    1.45 +begin
    1.46 +
    1.47 +definition
    1.48 +  "0 = Fin 0"
    1.49 +
    1.50 +definition
    1.51 +  [code_unfold]: "1 = Fin 1"
    1.52 +
    1.53 +definition
    1.54 +  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    1.55 +
    1.56 +instance ..
    1.57 +
    1.58 +end
    1.59 +
    1.60 +definition iSuc :: "enat \<Rightarrow> enat" where
    1.61 +  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    1.62 +
    1.63 +lemma Fin_0: "Fin 0 = 0"
    1.64 +  by (simp add: zero_enat_def)
    1.65 +
    1.66 +lemma Fin_1: "Fin 1 = 1"
    1.67 +  by (simp add: one_enat_def)
    1.68 +
    1.69 +lemma Fin_number: "Fin (number_of k) = number_of k"
    1.70 +  by (simp add: number_of_enat_def)
    1.71 +
    1.72 +lemma one_iSuc: "1 = iSuc 0"
    1.73 +  by (simp add: zero_enat_def one_enat_def iSuc_def)
    1.74 +
    1.75 +lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    1.76 +  by (simp add: zero_enat_def)
    1.77 +
    1.78 +lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    1.79 +  by (simp add: zero_enat_def)
    1.80 +
    1.81 +lemma zero_enat_eq [simp]:
    1.82 +  "number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    1.83 +  "(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    1.84 +  unfolding zero_enat_def number_of_enat_def by simp_all
    1.85 +
    1.86 +lemma one_enat_eq [simp]:
    1.87 +  "number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    1.88 +  "(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    1.89 +  unfolding one_enat_def number_of_enat_def by simp_all
    1.90 +
    1.91 +lemma zero_one_enat_neq [simp]:
    1.92 +  "\<not> 0 = (1\<Colon>enat)"
    1.93 +  "\<not> 1 = (0\<Colon>enat)"
    1.94 +  unfolding zero_enat_def one_enat_def by simp_all
    1.95 +
    1.96 +lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
    1.97 +  by (simp add: one_enat_def)
    1.98 +
    1.99 +lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
   1.100 +  by (simp add: one_enat_def)
   1.101 +
   1.102 +lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
   1.103 +  by (simp add: number_of_enat_def)
   1.104 +
   1.105 +lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
   1.106 +  by (simp add: number_of_enat_def)
   1.107 +
   1.108 +lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
   1.109 +  by (simp add: iSuc_def)
   1.110 +
   1.111 +lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
   1.112 +  by (simp add: iSuc_Fin number_of_enat_def)
   1.113 +
   1.114 +lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   1.115 +  by (simp add: iSuc_def)
   1.116 +
   1.117 +lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   1.118 +  by (simp add: iSuc_def zero_enat_def split: enat.splits)
   1.119 +
   1.120 +lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
   1.121 +  by (rule iSuc_ne_0 [symmetric])
   1.122 +
   1.123 +lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
   1.124 +  by (simp add: iSuc_def split: enat.splits)
   1.125 +
   1.126 +lemma number_of_enat_inject [simp]:
   1.127 +  "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
   1.128 +  by (simp add: number_of_enat_def)
   1.129 +
   1.130 +
   1.131 +subsection {* Addition *}
   1.132 +
   1.133 +instantiation enat :: comm_monoid_add
   1.134 +begin
   1.135 +
   1.136 +definition [nitpick_simp]:
   1.137 +  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   1.138 +
   1.139 +lemma plus_enat_simps [simp, code]:
   1.140 +  "Fin m + Fin n = Fin (m + n)"
   1.141 +  "\<infinity> + q = \<infinity>"
   1.142 +  "q + \<infinity> = \<infinity>"
   1.143 +  by (simp_all add: plus_enat_def split: enat.splits)
   1.144 +
   1.145 +instance proof
   1.146 +  fix n m q :: enat
   1.147 +  show "n + m + q = n + (m + q)"
   1.148 +    by (cases n, auto, cases m, auto, cases q, auto)
   1.149 +  show "n + m = m + n"
   1.150 +    by (cases n, auto, cases m, auto)
   1.151 +  show "0 + n = n"
   1.152 +    by (cases n) (simp_all add: zero_enat_def)
   1.153 +qed
   1.154 +
   1.155 +end
   1.156 +
   1.157 +lemma plus_enat_0 [simp]:
   1.158 +  "0 + (q\<Colon>enat) = q"
   1.159 +  "(q\<Colon>enat) + 0 = q"
   1.160 +  by (simp_all add: plus_enat_def zero_enat_def split: enat.splits)
   1.161 +
   1.162 +lemma plus_enat_number [simp]:
   1.163 +  "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
   1.164 +    else if l < Int.Pls then number_of k else number_of (k + l))"
   1.165 +  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   1.166 +
   1.167 +lemma iSuc_number [simp]:
   1.168 +  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   1.169 +  unfolding iSuc_number_of
   1.170 +  unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
   1.171 +
   1.172 +lemma iSuc_plus_1:
   1.173 +  "iSuc n = n + 1"
   1.174 +  by (cases n) (simp_all add: iSuc_Fin one_enat_def)
   1.175 +  
   1.176 +lemma plus_1_iSuc:
   1.177 +  "1 + q = iSuc q"
   1.178 +  "q + 1 = iSuc q"
   1.179 +by (simp_all add: iSuc_plus_1 add_ac)
   1.180 +
   1.181 +lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   1.182 +by (simp_all add: iSuc_plus_1 add_ac)
   1.183 +
   1.184 +lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   1.185 +by (simp only: add_commute[of m] iadd_Suc)
   1.186 +
   1.187 +lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
   1.188 +by (cases m, cases n, simp_all add: zero_enat_def)
   1.189 +
   1.190 +subsection {* Multiplication *}
   1.191 +
   1.192 +instantiation enat :: comm_semiring_1
   1.193 +begin
   1.194 +
   1.195 +definition times_enat_def [nitpick_simp]:
   1.196 +  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   1.197 +    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   1.198 +
   1.199 +lemma times_enat_simps [simp, code]:
   1.200 +  "Fin m * Fin n = Fin (m * n)"
   1.201 +  "\<infinity> * \<infinity> = \<infinity>"
   1.202 +  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   1.203 +  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   1.204 +  unfolding times_enat_def zero_enat_def
   1.205 +  by (simp_all split: enat.split)
   1.206 +
   1.207 +instance proof
   1.208 +  fix a b c :: enat
   1.209 +  show "(a * b) * c = a * (b * c)"
   1.210 +    unfolding times_enat_def zero_enat_def
   1.211 +    by (simp split: enat.split)
   1.212 +  show "a * b = b * a"
   1.213 +    unfolding times_enat_def zero_enat_def
   1.214 +    by (simp split: enat.split)
   1.215 +  show "1 * a = a"
   1.216 +    unfolding times_enat_def zero_enat_def one_enat_def
   1.217 +    by (simp split: enat.split)
   1.218 +  show "(a + b) * c = a * c + b * c"
   1.219 +    unfolding times_enat_def zero_enat_def
   1.220 +    by (simp split: enat.split add: left_distrib)
   1.221 +  show "0 * a = 0"
   1.222 +    unfolding times_enat_def zero_enat_def
   1.223 +    by (simp split: enat.split)
   1.224 +  show "a * 0 = 0"
   1.225 +    unfolding times_enat_def zero_enat_def
   1.226 +    by (simp split: enat.split)
   1.227 +  show "(0::enat) \<noteq> 1"
   1.228 +    unfolding zero_enat_def one_enat_def
   1.229 +    by simp
   1.230 +qed
   1.231 +
   1.232 +end
   1.233 +
   1.234 +lemma mult_iSuc: "iSuc m * n = n + m * n"
   1.235 +  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   1.236 +
   1.237 +lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   1.238 +  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   1.239 +
   1.240 +lemma of_nat_eq_Fin: "of_nat n = Fin n"
   1.241 +  apply (induct n)
   1.242 +  apply (simp add: Fin_0)
   1.243 +  apply (simp add: plus_1_iSuc iSuc_Fin)
   1.244 +  done
   1.245 +
   1.246 +instance enat :: number_semiring
   1.247 +proof
   1.248 +  fix n show "number_of (int n) = (of_nat n :: enat)"
   1.249 +    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
   1.250 +qed
   1.251 +
   1.252 +instance enat :: semiring_char_0 proof
   1.253 +  have "inj Fin" by (rule injI) simp
   1.254 +  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
   1.255 +qed
   1.256 +
   1.257 +lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   1.258 +by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   1.259 +
   1.260 +lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   1.261 +by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   1.262 +
   1.263 +
   1.264 +subsection {* Subtraction *}
   1.265 +
   1.266 +instantiation enat :: minus
   1.267 +begin
   1.268 +
   1.269 +definition diff_enat_def:
   1.270 +"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   1.271 +          | \<infinity> \<Rightarrow> \<infinity>)"
   1.272 +
   1.273 +instance ..
   1.274 +
   1.275 +end
   1.276 +
   1.277 +lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   1.278 +by(simp add: diff_enat_def)
   1.279 +
   1.280 +lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
   1.281 +by(simp add: diff_enat_def)
   1.282 +
   1.283 +lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   1.284 +by(simp add: diff_enat_def)
   1.285 +
   1.286 +lemma idiff_0[simp]: "(0::enat) - n = 0"
   1.287 +by (cases n, simp_all add: zero_enat_def)
   1.288 +
   1.289 +lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
   1.290 +
   1.291 +lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   1.292 +by (cases n) (simp_all add: zero_enat_def)
   1.293 +
   1.294 +lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   1.295 +
   1.296 +lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   1.297 +by(auto simp: zero_enat_def)
   1.298 +
   1.299 +lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
   1.300 +by(simp add: iSuc_def split: enat.split)
   1.301 +
   1.302 +lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   1.303 +by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
   1.304 +
   1.305 +(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   1.306 +
   1.307 +
   1.308 +subsection {* Ordering *}
   1.309 +
   1.310 +instantiation enat :: linordered_ab_semigroup_add
   1.311 +begin
   1.312 +
   1.313 +definition [nitpick_simp]:
   1.314 +  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   1.315 +    | \<infinity> \<Rightarrow> True)"
   1.316 +
   1.317 +definition [nitpick_simp]:
   1.318 +  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   1.319 +    | \<infinity> \<Rightarrow> False)"
   1.320 +
   1.321 +lemma enat_ord_simps [simp]:
   1.322 +  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   1.323 +  "Fin m < Fin n \<longleftrightarrow> m < n"
   1.324 +  "q \<le> \<infinity>"
   1.325 +  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
   1.326 +  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
   1.327 +  "\<infinity> < q \<longleftrightarrow> False"
   1.328 +  by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   1.329 +
   1.330 +lemma enat_ord_code [code]:
   1.331 +  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   1.332 +  "Fin m < Fin n \<longleftrightarrow> m < n"
   1.333 +  "q \<le> \<infinity> \<longleftrightarrow> True"
   1.334 +  "Fin m < \<infinity> \<longleftrightarrow> True"
   1.335 +  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   1.336 +  "\<infinity> < q \<longleftrightarrow> False"
   1.337 +  by simp_all
   1.338 +
   1.339 +instance by default
   1.340 +  (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
   1.341 +
   1.342 +end
   1.343 +
   1.344 +instance enat :: ordered_comm_semiring
   1.345 +proof
   1.346 +  fix a b c :: enat
   1.347 +  assume "a \<le> b" and "0 \<le> c"
   1.348 +  thus "c * a \<le> c * b"
   1.349 +    unfolding times_enat_def less_eq_enat_def zero_enat_def
   1.350 +    by (simp split: enat.splits)
   1.351 +qed
   1.352 +
   1.353 +lemma enat_ord_number [simp]:
   1.354 +  "(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   1.355 +  "(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   1.356 +  by (simp_all add: number_of_enat_def)
   1.357 +
   1.358 +lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n"
   1.359 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   1.360 +
   1.361 +lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   1.362 +by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   1.363 +
   1.364 +lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   1.365 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   1.366 +
   1.367 +lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   1.368 +  by simp
   1.369 +
   1.370 +lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   1.371 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
   1.372 +
   1.373 +lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
   1.374 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   1.375 +
   1.376 +lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
   1.377 +  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   1.378 + 
   1.379 +lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
   1.380 +  by (simp add: iSuc_def less_enat_def split: enat.splits)
   1.381 +
   1.382 +lemma ile_iSuc [simp]: "n \<le> iSuc n"
   1.383 +  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   1.384 +
   1.385 +lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   1.386 +  by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
   1.387 +
   1.388 +lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   1.389 +  by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
   1.390 +
   1.391 +lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
   1.392 +by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
   1.393 +
   1.394 +lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   1.395 +  by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   1.396 +
   1.397 +lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   1.398 +  by (cases n) auto
   1.399 +
   1.400 +lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   1.401 +  by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   1.402 +
   1.403 +lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   1.404 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   1.405 +
   1.406 +lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   1.407 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   1.408 +
   1.409 +lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
   1.410 +by (simp only: i0_less imult_is_0, simp)
   1.411 +
   1.412 +lemma mono_iSuc: "mono iSuc"
   1.413 +by(simp add: mono_def)
   1.414 +
   1.415 +
   1.416 +lemma min_enat_simps [simp]:
   1.417 +  "min (Fin m) (Fin n) = Fin (min m n)"
   1.418 +  "min q 0 = 0"
   1.419 +  "min 0 q = 0"
   1.420 +  "min q \<infinity> = q"
   1.421 +  "min \<infinity> q = q"
   1.422 +  by (auto simp add: min_def)
   1.423 +
   1.424 +lemma max_enat_simps [simp]:
   1.425 +  "max (Fin m) (Fin n) = Fin (max m n)"
   1.426 +  "max q 0 = q"
   1.427 +  "max 0 q = q"
   1.428 +  "max q \<infinity> = \<infinity>"
   1.429 +  "max \<infinity> q = \<infinity>"
   1.430 +  by (simp_all add: max_def)
   1.431 +
   1.432 +lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   1.433 +  by (cases n) simp_all
   1.434 +
   1.435 +lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   1.436 +  by (cases n) simp_all
   1.437 +
   1.438 +lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   1.439 +apply (induct_tac k)
   1.440 + apply (simp (no_asm) only: Fin_0)
   1.441 + apply (fast intro: le_less_trans [OF i0_lb])
   1.442 +apply (erule exE)
   1.443 +apply (drule spec)
   1.444 +apply (erule exE)
   1.445 +apply (drule ileI1)
   1.446 +apply (rule iSuc_Fin [THEN subst])
   1.447 +apply (rule exI)
   1.448 +apply (erule (1) le_less_trans)
   1.449 +done
   1.450 +
   1.451 +instantiation enat :: "{bot, top}"
   1.452 +begin
   1.453 +
   1.454 +definition bot_enat :: enat where
   1.455 +  "bot_enat = 0"
   1.456 +
   1.457 +definition top_enat :: enat where
   1.458 +  "top_enat = \<infinity>"
   1.459 +
   1.460 +instance proof
   1.461 +qed (simp_all add: bot_enat_def top_enat_def)
   1.462 +
   1.463 +end
   1.464 +
   1.465 +lemma finite_Fin_bounded:
   1.466 +  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   1.467 +  shows "finite A"
   1.468 +proof (rule finite_subset)
   1.469 +  show "finite (Fin ` {..n})" by blast
   1.470 +
   1.471 +  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   1.472 +  also have "\<dots> \<subseteq> Fin ` {..n}"
   1.473 +    by (rule subsetI) (case_tac x, auto)
   1.474 +  finally show "A \<subseteq> Fin ` {..n}" .
   1.475 +qed
   1.476 +
   1.477 +
   1.478 +subsection {* Well-ordering *}
   1.479 +
   1.480 +lemma less_FinE:
   1.481 +  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   1.482 +by (induct n) auto
   1.483 +
   1.484 +lemma less_InftyE:
   1.485 +  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
   1.486 +by (induct n) auto
   1.487 +
   1.488 +lemma enat_less_induct:
   1.489 +  assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
   1.490 +proof -
   1.491 +  have P_Fin: "!!k. P (Fin k)"
   1.492 +    apply (rule nat_less_induct)
   1.493 +    apply (rule prem, clarify)
   1.494 +    apply (erule less_FinE, simp)
   1.495 +    done
   1.496 +  show ?thesis
   1.497 +  proof (induct n)
   1.498 +    fix nat
   1.499 +    show "P (Fin nat)" by (rule P_Fin)
   1.500 +  next
   1.501 +    show "P Infty"
   1.502 +      apply (rule prem, clarify)
   1.503 +      apply (erule less_InftyE)
   1.504 +      apply (simp add: P_Fin)
   1.505 +      done
   1.506 +  qed
   1.507 +qed
   1.508 +
   1.509 +instance enat :: wellorder
   1.510 +proof
   1.511 +  fix P and n
   1.512 +  assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
   1.513 +  show "P n" by (blast intro: enat_less_induct hyp)
   1.514 +qed
   1.515 +
   1.516 +subsection {* Complete Lattice *}
   1.517 +
   1.518 +instantiation enat :: complete_lattice
   1.519 +begin
   1.520 +
   1.521 +definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   1.522 +  "inf_enat \<equiv> min"
   1.523 +
   1.524 +definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   1.525 +  "sup_enat \<equiv> max"
   1.526 +
   1.527 +definition Inf_enat :: "enat set \<Rightarrow> enat" where
   1.528 +  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
   1.529 +
   1.530 +definition Sup_enat :: "enat set \<Rightarrow> enat" where
   1.531 +  "Sup_enat A \<equiv> if A = {} then 0
   1.532 +    else if finite A then Max A
   1.533 +                     else \<infinity>"
   1.534 +instance proof
   1.535 +  fix x :: "enat" and A :: "enat set"
   1.536 +  { assume "x \<in> A" then show "Inf A \<le> x"
   1.537 +      unfolding Inf_enat_def by (auto intro: Least_le) }
   1.538 +  { assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A"
   1.539 +      unfolding Inf_enat_def
   1.540 +      by (cases "A = {}") (auto intro: LeastI2_ex) }
   1.541 +  { assume "x \<in> A" then show "x \<le> Sup A"
   1.542 +      unfolding Sup_enat_def by (cases "finite A") auto }
   1.543 +  { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   1.544 +      unfolding Sup_enat_def using finite_Fin_bounded by auto }
   1.545 +qed (simp_all add: inf_enat_def sup_enat_def)
   1.546 +end
   1.547 +
   1.548 +
   1.549 +subsection {* Traditional theorem names *}
   1.550 +
   1.551 +lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   1.552 +  plus_enat_def less_eq_enat_def less_enat_def
   1.553 +
   1.554 +end