src/HOL/Library/Extended_Nat.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43921 e8511be08ddd
child 43923 ab93d0190a5d
permissions -rw-r--r--
add nat => enat coercion
     1 (*  Title:      HOL/Library/Extended_Nat.thy
     2     Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
     3     Contributions: David Trachtenherz, TU Muenchen
     4 *)
     5 
     6 header {* Extended natural numbers (i.e. with infinity) *}
     7 
     8 theory Extended_Nat
     9 imports Main
    10 begin
    11 
    12 class infinity =
    13   fixes infinity :: "'a"
    14 
    15 notation (xsymbols)
    16   infinity  ("\<infinity>")
    17 
    18 notation (HTML output)
    19   infinity  ("\<infinity>")
    20 
    21 subsection {* Type definition *}
    22 
    23 text {*
    24   We extend the standard natural numbers by a special value indicating
    25   infinity.
    26 *}
    27 
    28 typedef (open) enat = "UNIV :: nat option set" ..
    29  
    30 definition Fin :: "nat \<Rightarrow> enat" where
    31   "Fin n = Abs_enat (Some n)"
    32  
    33 instantiation enat :: infinity
    34 begin
    35   definition "\<infinity> = Abs_enat None"
    36   instance proof qed
    37 end
    38  
    39 rep_datatype Fin "\<infinity> :: enat"
    40 proof -
    41   fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
    42   then show "P i"
    43   proof induct
    44     case (Abs_enat y) then show ?case
    45       by (cases y rule: option.exhaust)
    46          (auto simp: Fin_def infinity_enat_def)
    47   qed
    48 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
    49 
    50 declare [[coercion_enabled]]
    51 declare [[coercion "Fin::nat\<Rightarrow>enat"]]
    52 
    53 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
    54 by (cases x) auto
    55 
    56 lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
    57 by (cases x) auto
    58 
    59 primrec the_Fin :: "enat \<Rightarrow> nat"
    60 where "the_Fin (Fin n) = n"
    61 
    62 subsection {* Constructors and numbers *}
    63 
    64 instantiation enat :: "{zero, one, number}"
    65 begin
    66 
    67 definition
    68   "0 = Fin 0"
    69 
    70 definition
    71   [code_unfold]: "1 = Fin 1"
    72 
    73 definition
    74   [code_unfold, code del]: "number_of k = Fin (number_of k)"
    75 
    76 instance ..
    77 
    78 end
    79 
    80 definition iSuc :: "enat \<Rightarrow> enat" where
    81   "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    82 
    83 lemma Fin_0: "Fin 0 = 0"
    84   by (simp add: zero_enat_def)
    85 
    86 lemma Fin_1: "Fin 1 = 1"
    87   by (simp add: one_enat_def)
    88 
    89 lemma Fin_number: "Fin (number_of k) = number_of k"
    90   by (simp add: number_of_enat_def)
    91 
    92 lemma one_iSuc: "1 = iSuc 0"
    93   by (simp add: zero_enat_def one_enat_def iSuc_def)
    94 
    95 lemma Infty_ne_i0 [simp]: "(\<infinity>::enat) \<noteq> 0"
    96   by (simp add: zero_enat_def)
    97 
    98 lemma i0_ne_Infty [simp]: "0 \<noteq> (\<infinity>::enat)"
    99   by (simp add: zero_enat_def)
   100 
   101 lemma zero_enat_eq [simp]:
   102   "number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
   103   "(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
   104   unfolding zero_enat_def number_of_enat_def by simp_all
   105 
   106 lemma one_enat_eq [simp]:
   107   "number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
   108   "(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
   109   unfolding one_enat_def number_of_enat_def by simp_all
   110 
   111 lemma zero_one_enat_neq [simp]:
   112   "\<not> 0 = (1\<Colon>enat)"
   113   "\<not> 1 = (0\<Colon>enat)"
   114   unfolding zero_enat_def one_enat_def by simp_all
   115 
   116 lemma Infty_ne_i1 [simp]: "(\<infinity>::enat) \<noteq> 1"
   117   by (simp add: one_enat_def)
   118 
   119 lemma i1_ne_Infty [simp]: "1 \<noteq> (\<infinity>::enat)"
   120   by (simp add: one_enat_def)
   121 
   122 lemma Infty_ne_number [simp]: "(\<infinity>::enat) \<noteq> number_of k"
   123   by (simp add: number_of_enat_def)
   124 
   125 lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
   126   by (simp add: number_of_enat_def)
   127 
   128 lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
   129   by (simp add: iSuc_def)
   130 
   131 lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
   132   by (simp add: iSuc_Fin number_of_enat_def)
   133 
   134 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   135   by (simp add: iSuc_def)
   136 
   137 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   138   by (simp add: iSuc_def zero_enat_def split: enat.splits)
   139 
   140 lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
   141   by (rule iSuc_ne_0 [symmetric])
   142 
   143 lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
   144   by (simp add: iSuc_def split: enat.splits)
   145 
   146 lemma number_of_enat_inject [simp]:
   147   "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
   148   by (simp add: number_of_enat_def)
   149 
   150 
   151 subsection {* Addition *}
   152 
   153 instantiation enat :: comm_monoid_add
   154 begin
   155 
   156 definition [nitpick_simp]:
   157   "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   158 
   159 lemma plus_enat_simps [simp, code]:
   160   fixes q :: enat
   161   shows "Fin m + Fin n = Fin (m + n)"
   162     and "\<infinity> + q = \<infinity>"
   163     and "q + \<infinity> = \<infinity>"
   164   by (simp_all add: plus_enat_def split: enat.splits)
   165 
   166 instance proof
   167   fix n m q :: enat
   168   show "n + m + q = n + (m + q)"
   169     by (cases n, auto, cases m, auto, cases q, auto)
   170   show "n + m = m + n"
   171     by (cases n, auto, cases m, auto)
   172   show "0 + n = n"
   173     by (cases n) (simp_all add: zero_enat_def)
   174 qed
   175 
   176 end
   177 
   178 lemma plus_enat_0 [simp]:
   179   "0 + (q\<Colon>enat) = q"
   180   "(q\<Colon>enat) + 0 = q"
   181   by (simp_all add: plus_enat_def zero_enat_def split: enat.splits)
   182 
   183 lemma plus_enat_number [simp]:
   184   "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
   185     else if l < Int.Pls then number_of k else number_of (k + l))"
   186   unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   187 
   188 lemma iSuc_number [simp]:
   189   "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   190   unfolding iSuc_number_of
   191   unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
   192 
   193 lemma iSuc_plus_1:
   194   "iSuc n = n + 1"
   195   by (cases n) (simp_all add: iSuc_Fin one_enat_def)
   196   
   197 lemma plus_1_iSuc:
   198   "1 + q = iSuc q"
   199   "q + 1 = iSuc q"
   200 by (simp_all add: iSuc_plus_1 add_ac)
   201 
   202 lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   203 by (simp_all add: iSuc_plus_1 add_ac)
   204 
   205 lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   206 by (simp only: add_commute[of m] iadd_Suc)
   207 
   208 lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
   209 by (cases m, cases n, simp_all add: zero_enat_def)
   210 
   211 subsection {* Multiplication *}
   212 
   213 instantiation enat :: comm_semiring_1
   214 begin
   215 
   216 definition times_enat_def [nitpick_simp]:
   217   "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   218     (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   219 
   220 lemma times_enat_simps [simp, code]:
   221   "Fin m * Fin n = Fin (m * n)"
   222   "\<infinity> * \<infinity> = (\<infinity>::enat)"
   223   "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   224   "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   225   unfolding times_enat_def zero_enat_def
   226   by (simp_all split: enat.split)
   227 
   228 instance proof
   229   fix a b c :: enat
   230   show "(a * b) * c = a * (b * c)"
   231     unfolding times_enat_def zero_enat_def
   232     by (simp split: enat.split)
   233   show "a * b = b * a"
   234     unfolding times_enat_def zero_enat_def
   235     by (simp split: enat.split)
   236   show "1 * a = a"
   237     unfolding times_enat_def zero_enat_def one_enat_def
   238     by (simp split: enat.split)
   239   show "(a + b) * c = a * c + b * c"
   240     unfolding times_enat_def zero_enat_def
   241     by (simp split: enat.split add: left_distrib)
   242   show "0 * a = 0"
   243     unfolding times_enat_def zero_enat_def
   244     by (simp split: enat.split)
   245   show "a * 0 = 0"
   246     unfolding times_enat_def zero_enat_def
   247     by (simp split: enat.split)
   248   show "(0::enat) \<noteq> 1"
   249     unfolding zero_enat_def one_enat_def
   250     by simp
   251 qed
   252 
   253 end
   254 
   255 lemma mult_iSuc: "iSuc m * n = n + m * n"
   256   unfolding iSuc_plus_1 by (simp add: algebra_simps)
   257 
   258 lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   259   unfolding iSuc_plus_1 by (simp add: algebra_simps)
   260 
   261 lemma of_nat_eq_Fin: "of_nat n = Fin n"
   262   apply (induct n)
   263   apply (simp add: Fin_0)
   264   apply (simp add: plus_1_iSuc iSuc_Fin)
   265   done
   266 
   267 instance enat :: number_semiring
   268 proof
   269   fix n show "number_of (int n) = (of_nat n :: enat)"
   270     unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
   271 qed
   272 
   273 instance enat :: semiring_char_0 proof
   274   have "inj Fin" by (rule injI) simp
   275   then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
   276 qed
   277 
   278 lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   279 by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   280 
   281 lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   282 by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   283 
   284 
   285 subsection {* Subtraction *}
   286 
   287 instantiation enat :: minus
   288 begin
   289 
   290 definition diff_enat_def:
   291 "a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   292           | \<infinity> \<Rightarrow> \<infinity>)"
   293 
   294 instance ..
   295 
   296 end
   297 
   298 lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   299 by(simp add: diff_enat_def)
   300 
   301 lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   302 by(simp add: diff_enat_def)
   303 
   304 lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   305 by(simp add: diff_enat_def)
   306 
   307 lemma idiff_0[simp]: "(0::enat) - n = 0"
   308 by (cases n, simp_all add: zero_enat_def)
   309 
   310 lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
   311 
   312 lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   313 by (cases n) (simp_all add: zero_enat_def)
   314 
   315 lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   316 
   317 lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   318 by(auto simp: zero_enat_def)
   319 
   320 lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
   321 by(simp add: iSuc_def split: enat.split)
   322 
   323 lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   324 by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
   325 
   326 (*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   327 
   328 subsection {* Ordering *}
   329 
   330 instantiation enat :: linordered_ab_semigroup_add
   331 begin
   332 
   333 definition [nitpick_simp]:
   334   "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   335     | \<infinity> \<Rightarrow> True)"
   336 
   337 definition [nitpick_simp]:
   338   "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   339     | \<infinity> \<Rightarrow> False)"
   340 
   341 lemma enat_ord_simps [simp]:
   342   "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   343   "Fin m < Fin n \<longleftrightarrow> m < n"
   344   "q \<le> (\<infinity>::enat)"
   345   "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
   346   "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
   347   "(\<infinity>::enat) < q \<longleftrightarrow> False"
   348   by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   349 
   350 lemma enat_ord_code [code]:
   351   "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   352   "Fin m < Fin n \<longleftrightarrow> m < n"
   353   "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
   354   "Fin m < \<infinity> \<longleftrightarrow> True"
   355   "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   356   "(\<infinity>::enat) < q \<longleftrightarrow> False"
   357   by simp_all
   358 
   359 instance by default
   360   (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
   361 
   362 end
   363 
   364 instance enat :: ordered_comm_semiring
   365 proof
   366   fix a b c :: enat
   367   assume "a \<le> b" and "0 \<le> c"
   368   thus "c * a \<le> c * b"
   369     unfolding times_enat_def less_eq_enat_def zero_enat_def
   370     by (simp split: enat.splits)
   371 qed
   372 
   373 lemma enat_ord_number [simp]:
   374   "(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   375   "(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   376   by (simp_all add: number_of_enat_def)
   377 
   378 lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n"
   379   by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   380 
   381 lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   382 by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   383 
   384 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   385   by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   386 
   387 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   388   by simp
   389 
   390 lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   391   by (simp add: zero_enat_def less_enat_def split: enat.splits)
   392 
   393 lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
   394 by (simp add: zero_enat_def less_enat_def split: enat.splits)
   395 
   396 lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
   397   by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   398  
   399 lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
   400   by (simp add: iSuc_def less_enat_def split: enat.splits)
   401 
   402 lemma ile_iSuc [simp]: "n \<le> iSuc n"
   403   by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   404 
   405 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   406   by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
   407 
   408 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   409   by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
   410 
   411 lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
   412 by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
   413 
   414 lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   415   by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   416 
   417 lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   418   by (cases n) auto
   419 
   420 lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   421   by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   422 
   423 lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   424 by (simp add: zero_enat_def less_enat_def split: enat.splits)
   425 
   426 lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   427 by (simp add: zero_enat_def less_enat_def split: enat.splits)
   428 
   429 lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
   430 by (simp only: i0_less imult_is_0, simp)
   431 
   432 lemma mono_iSuc: "mono iSuc"
   433 by(simp add: mono_def)
   434 
   435 
   436 lemma min_enat_simps [simp]:
   437   "min (Fin m) (Fin n) = Fin (min m n)"
   438   "min q 0 = 0"
   439   "min 0 q = 0"
   440   "min q (\<infinity>::enat) = q"
   441   "min (\<infinity>::enat) q = q"
   442   by (auto simp add: min_def)
   443 
   444 lemma max_enat_simps [simp]:
   445   "max (Fin m) (Fin n) = Fin (max m n)"
   446   "max q 0 = q"
   447   "max 0 q = q"
   448   "max q \<infinity> = (\<infinity>::enat)"
   449   "max \<infinity> q = (\<infinity>::enat)"
   450   by (simp_all add: max_def)
   451 
   452 lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   453   by (cases n) simp_all
   454 
   455 lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   456   by (cases n) simp_all
   457 
   458 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   459 apply (induct_tac k)
   460  apply (simp (no_asm) only: Fin_0)
   461  apply (fast intro: le_less_trans [OF i0_lb])
   462 apply (erule exE)
   463 apply (drule spec)
   464 apply (erule exE)
   465 apply (drule ileI1)
   466 apply (rule iSuc_Fin [THEN subst])
   467 apply (rule exI)
   468 apply (erule (1) le_less_trans)
   469 done
   470 
   471 instantiation enat :: "{bot, top}"
   472 begin
   473 
   474 definition bot_enat :: enat where
   475   "bot_enat = 0"
   476 
   477 definition top_enat :: enat where
   478   "top_enat = \<infinity>"
   479 
   480 instance proof
   481 qed (simp_all add: bot_enat_def top_enat_def)
   482 
   483 end
   484 
   485 lemma finite_Fin_bounded:
   486   assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   487   shows "finite A"
   488 proof (rule finite_subset)
   489   show "finite (Fin ` {..n})" by blast
   490 
   491   have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   492   also have "\<dots> \<subseteq> Fin ` {..n}"
   493     by (rule subsetI) (case_tac x, auto)
   494   finally show "A \<subseteq> Fin ` {..n}" .
   495 qed
   496 
   497 
   498 subsection {* Well-ordering *}
   499 
   500 lemma less_FinE:
   501   "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   502 by (induct n) auto
   503 
   504 lemma less_InftyE:
   505   "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
   506 by (induct n) auto
   507 
   508 lemma enat_less_induct:
   509   assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
   510 proof -
   511   have P_Fin: "!!k. P (Fin k)"
   512     apply (rule nat_less_induct)
   513     apply (rule prem, clarify)
   514     apply (erule less_FinE, simp)
   515     done
   516   show ?thesis
   517   proof (induct n)
   518     fix nat
   519     show "P (Fin nat)" by (rule P_Fin)
   520   next
   521     show "P \<infinity>"
   522       apply (rule prem, clarify)
   523       apply (erule less_InftyE)
   524       apply (simp add: P_Fin)
   525       done
   526   qed
   527 qed
   528 
   529 instance enat :: wellorder
   530 proof
   531   fix P and n
   532   assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
   533   show "P n" by (blast intro: enat_less_induct hyp)
   534 qed
   535 
   536 subsection {* Complete Lattice *}
   537 
   538 instantiation enat :: complete_lattice
   539 begin
   540 
   541 definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   542   "inf_enat \<equiv> min"
   543 
   544 definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   545   "sup_enat \<equiv> max"
   546 
   547 definition Inf_enat :: "enat set \<Rightarrow> enat" where
   548   "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
   549 
   550 definition Sup_enat :: "enat set \<Rightarrow> enat" where
   551   "Sup_enat A \<equiv> if A = {} then 0
   552     else if finite A then Max A
   553                      else \<infinity>"
   554 instance proof
   555   fix x :: "enat" and A :: "enat set"
   556   { assume "x \<in> A" then show "Inf A \<le> x"
   557       unfolding Inf_enat_def by (auto intro: Least_le) }
   558   { assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A"
   559       unfolding Inf_enat_def
   560       by (cases "A = {}") (auto intro: LeastI2_ex) }
   561   { assume "x \<in> A" then show "x \<le> Sup A"
   562       unfolding Sup_enat_def by (cases "finite A") auto }
   563   { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   564       unfolding Sup_enat_def using finite_Fin_bounded by auto }
   565 qed (simp_all add: inf_enat_def sup_enat_def)
   566 end
   567 
   568 
   569 subsection {* Traditional theorem names *}
   570 
   571 lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   572   plus_enat_def less_eq_enat_def less_enat_def
   573 
   574 end