src/HOL/Library/Extended_Nat.thy
changeset 43924 1165fe965da8
parent 43923 ab93d0190a5d
child 43978 da7d04d4023c
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:48 2011 +0200
     1.3 @@ -27,8 +27,8 @@
     1.4  
     1.5  typedef (open) enat = "UNIV :: nat option set" ..
     1.6   
     1.7 -definition Fin :: "nat \<Rightarrow> enat" where
     1.8 -  "Fin n = Abs_enat (Some n)"
     1.9 +definition enat :: "nat \<Rightarrow> enat" where
    1.10 +  "enat n = Abs_enat (Some n)"
    1.11   
    1.12  instantiation enat :: infinity
    1.13  begin
    1.14 @@ -36,27 +36,27 @@
    1.15    instance proof qed
    1.16  end
    1.17   
    1.18 -rep_datatype Fin "\<infinity> :: enat"
    1.19 +rep_datatype enat "\<infinity> :: enat"
    1.20  proof -
    1.21 -  fix P i assume "\<And>j. P (Fin j)" "P \<infinity>"
    1.22 +  fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    1.23    then show "P i"
    1.24    proof induct
    1.25      case (Abs_enat y) then show ?case
    1.26        by (cases y rule: option.exhaust)
    1.27 -         (auto simp: Fin_def infinity_enat_def)
    1.28 +         (auto simp: enat_def infinity_enat_def)
    1.29    qed
    1.30 -qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
    1.31 +qed (auto simp add: enat_def infinity_enat_def Abs_enat_inject)
    1.32  
    1.33 -declare [[coercion "Fin::nat\<Rightarrow>enat"]]
    1.34 +declare [[coercion "enat::nat\<Rightarrow>enat"]]
    1.35  
    1.36 -lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
    1.37 +lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = enat i)"
    1.38  by (cases x) auto
    1.39  
    1.40 -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = \<infinity>)"
    1.41 +lemma not_enat_eq [iff]: "(ALL y. x ~= enat y) = (x = \<infinity>)"
    1.42  by (cases x) auto
    1.43  
    1.44 -primrec the_Fin :: "enat \<Rightarrow> nat"
    1.45 -where "the_Fin (Fin n) = n"
    1.46 +primrec the_enat :: "enat \<Rightarrow> nat"
    1.47 +where "the_enat (enat n) = n"
    1.48  
    1.49  subsection {* Constructors and numbers *}
    1.50  
    1.51 @@ -64,28 +64,28 @@
    1.52  begin
    1.53  
    1.54  definition
    1.55 -  "0 = Fin 0"
    1.56 +  "0 = enat 0"
    1.57  
    1.58  definition
    1.59 -  [code_unfold]: "1 = Fin 1"
    1.60 +  [code_unfold]: "1 = enat 1"
    1.61  
    1.62  definition
    1.63 -  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    1.64 +  [code_unfold, code del]: "number_of k = enat (number_of k)"
    1.65  
    1.66  instance ..
    1.67  
    1.68  end
    1.69  
    1.70  definition iSuc :: "enat \<Rightarrow> enat" where
    1.71 -  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    1.72 +  "iSuc i = (case i of enat n \<Rightarrow> enat (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    1.73  
    1.74 -lemma Fin_0: "Fin 0 = 0"
    1.75 +lemma enat_0: "enat 0 = 0"
    1.76    by (simp add: zero_enat_def)
    1.77  
    1.78 -lemma Fin_1: "Fin 1 = 1"
    1.79 +lemma enat_1: "enat 1 = 1"
    1.80    by (simp add: one_enat_def)
    1.81  
    1.82 -lemma Fin_number: "Fin (number_of k) = number_of k"
    1.83 +lemma enat_number: "enat (number_of k) = number_of k"
    1.84    by (simp add: number_of_enat_def)
    1.85  
    1.86  lemma one_iSuc: "1 = iSuc 0"
    1.87 @@ -124,11 +124,11 @@
    1.88  lemma number_ne_Infty [simp]: "number_of k \<noteq> (\<infinity>::enat)"
    1.89    by (simp add: number_of_enat_def)
    1.90  
    1.91 -lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
    1.92 +lemma iSuc_enat: "iSuc (enat n) = enat (Suc n)"
    1.93    by (simp add: iSuc_def)
    1.94  
    1.95 -lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
    1.96 -  by (simp add: iSuc_Fin number_of_enat_def)
    1.97 +lemma iSuc_number_of: "iSuc (number_of k) = enat (Suc (number_of k))"
    1.98 +  by (simp add: iSuc_enat number_of_enat_def)
    1.99  
   1.100  lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   1.101    by (simp add: iSuc_def)
   1.102 @@ -153,11 +153,11 @@
   1.103  begin
   1.104  
   1.105  definition [nitpick_simp]:
   1.106 -  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   1.107 +  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | enat m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | enat n \<Rightarrow> enat (m + n)))"
   1.108  
   1.109  lemma plus_enat_simps [simp, code]:
   1.110    fixes q :: enat
   1.111 -  shows "Fin m + Fin n = Fin (m + n)"
   1.112 +  shows "enat m + enat n = enat (m + n)"
   1.113      and "\<infinity> + q = \<infinity>"
   1.114      and "q + \<infinity> = \<infinity>"
   1.115    by (simp_all add: plus_enat_def split: enat.splits)
   1.116 @@ -182,7 +182,7 @@
   1.117  lemma plus_enat_number [simp]:
   1.118    "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
   1.119      else if l < Int.Pls then number_of k else number_of (k + l))"
   1.120 -  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   1.121 +  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ enat] ..
   1.122  
   1.123  lemma iSuc_number [simp]:
   1.124    "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   1.125 @@ -191,7 +191,7 @@
   1.126  
   1.127  lemma iSuc_plus_1:
   1.128    "iSuc n = n + 1"
   1.129 -  by (cases n) (simp_all add: iSuc_Fin one_enat_def)
   1.130 +  by (cases n) (simp_all add: iSuc_enat one_enat_def)
   1.131    
   1.132  lemma plus_1_iSuc:
   1.133    "1 + q = iSuc q"
   1.134 @@ -213,14 +213,14 @@
   1.135  begin
   1.136  
   1.137  definition times_enat_def [nitpick_simp]:
   1.138 -  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   1.139 -    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   1.140 +  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | enat m \<Rightarrow>
   1.141 +    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | enat n \<Rightarrow> enat (m * n)))"
   1.142  
   1.143  lemma times_enat_simps [simp, code]:
   1.144 -  "Fin m * Fin n = Fin (m * n)"
   1.145 +  "enat m * enat n = enat (m * n)"
   1.146    "\<infinity> * \<infinity> = (\<infinity>::enat)"
   1.147 -  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   1.148 -  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   1.149 +  "\<infinity> * enat n = (if n = 0 then 0 else \<infinity>)"
   1.150 +  "enat m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   1.151    unfolding times_enat_def zero_enat_def
   1.152    by (simp_all split: enat.split)
   1.153  
   1.154 @@ -257,21 +257,21 @@
   1.155  lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   1.156    unfolding iSuc_plus_1 by (simp add: algebra_simps)
   1.157  
   1.158 -lemma of_nat_eq_Fin: "of_nat n = Fin n"
   1.159 +lemma of_nat_eq_enat: "of_nat n = enat n"
   1.160    apply (induct n)
   1.161 -  apply (simp add: Fin_0)
   1.162 -  apply (simp add: plus_1_iSuc iSuc_Fin)
   1.163 +  apply (simp add: enat_0)
   1.164 +  apply (simp add: plus_1_iSuc iSuc_enat)
   1.165    done
   1.166  
   1.167  instance enat :: number_semiring
   1.168  proof
   1.169    fix n show "number_of (int n) = (of_nat n :: enat)"
   1.170 -    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
   1.171 +    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_enat ..
   1.172  qed
   1.173  
   1.174  instance enat :: semiring_char_0 proof
   1.175 -  have "inj Fin" by (rule injI) simp
   1.176 -  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
   1.177 +  have "inj enat" by (rule injI) simp
   1.178 +  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
   1.179  qed
   1.180  
   1.181  lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   1.182 @@ -287,31 +287,31 @@
   1.183  begin
   1.184  
   1.185  definition diff_enat_def:
   1.186 -"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   1.187 +"a - b = (case a of (enat x) \<Rightarrow> (case b of (enat y) \<Rightarrow> enat (x - y) | \<infinity> \<Rightarrow> 0)
   1.188            | \<infinity> \<Rightarrow> \<infinity>)"
   1.189  
   1.190  instance ..
   1.191  
   1.192  end
   1.193  
   1.194 -lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   1.195 +lemma idiff_enat_enat[simp,code]: "enat a - enat b = enat (a - b)"
   1.196  by(simp add: diff_enat_def)
   1.197  
   1.198  lemma idiff_Infty[simp,code]: "\<infinity> - n = (\<infinity>::enat)"
   1.199  by(simp add: diff_enat_def)
   1.200  
   1.201 -lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   1.202 +lemma idiff_Infty_right[simp,code]: "enat a - \<infinity> = 0"
   1.203  by(simp add: diff_enat_def)
   1.204  
   1.205  lemma idiff_0[simp]: "(0::enat) - n = 0"
   1.206  by (cases n, simp_all add: zero_enat_def)
   1.207  
   1.208 -lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
   1.209 +lemmas idiff_enat_0[simp] = idiff_0[unfolded zero_enat_def]
   1.210  
   1.211  lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   1.212  by (cases n) (simp_all add: zero_enat_def)
   1.213  
   1.214 -lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   1.215 +lemmas idiff_enat_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   1.216  
   1.217  lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   1.218  by(auto simp: zero_enat_def)
   1.219 @@ -320,9 +320,9 @@
   1.220  by(simp add: iSuc_def split: enat.split)
   1.221  
   1.222  lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   1.223 -by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
   1.224 +by(simp add: one_enat_def iSuc_enat[symmetric] zero_enat_def[symmetric])
   1.225  
   1.226 -(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   1.227 +(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
   1.228  
   1.229  subsection {* Ordering *}
   1.230  
   1.231 @@ -330,16 +330,16 @@
   1.232  begin
   1.233  
   1.234  definition [nitpick_simp]:
   1.235 -  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   1.236 +  "m \<le> n = (case n of enat n1 \<Rightarrow> (case m of enat m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   1.237      | \<infinity> \<Rightarrow> True)"
   1.238  
   1.239  definition [nitpick_simp]:
   1.240 -  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   1.241 +  "m < n = (case m of enat m1 \<Rightarrow> (case n of enat n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   1.242      | \<infinity> \<Rightarrow> False)"
   1.243  
   1.244  lemma enat_ord_simps [simp]:
   1.245 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   1.246 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   1.247 +  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
   1.248 +  "enat m < enat n \<longleftrightarrow> m < n"
   1.249    "q \<le> (\<infinity>::enat)"
   1.250    "q < (\<infinity>::enat) \<longleftrightarrow> q \<noteq> \<infinity>"
   1.251    "(\<infinity>::enat) \<le> q \<longleftrightarrow> q = \<infinity>"
   1.252 @@ -347,11 +347,11 @@
   1.253    by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   1.254  
   1.255  lemma enat_ord_code [code]:
   1.256 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   1.257 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   1.258 +  "enat m \<le> enat n \<longleftrightarrow> m \<le> n"
   1.259 +  "enat m < enat n \<longleftrightarrow> m < n"
   1.260    "q \<le> (\<infinity>::enat) \<longleftrightarrow> True"
   1.261 -  "Fin m < \<infinity> \<longleftrightarrow> True"
   1.262 -  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   1.263 +  "enat m < \<infinity> \<longleftrightarrow> True"
   1.264 +  "\<infinity> \<le> enat n \<longleftrightarrow> False"
   1.265    "(\<infinity>::enat) < q \<longleftrightarrow> False"
   1.266    by simp_all
   1.267  
   1.268 @@ -380,10 +380,10 @@
   1.269  lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   1.270  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   1.271  
   1.272 -lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   1.273 +lemma Infty_ileE [elim!]: "\<infinity> \<le> enat m \<Longrightarrow> R"
   1.274    by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   1.275  
   1.276 -lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   1.277 +lemma Infty_ilessE [elim!]: "\<infinity> < enat m \<Longrightarrow> R"
   1.278    by simp
   1.279  
   1.280  lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   1.281 @@ -413,10 +413,10 @@
   1.282  lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   1.283    by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   1.284  
   1.285 -lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   1.286 +lemma Suc_ile_eq: "enat (Suc m) \<le> n \<longleftrightarrow> enat m < n"
   1.287    by (cases n) auto
   1.288  
   1.289 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   1.290 +lemma iless_Suc_eq [simp]: "enat m < iSuc n \<longleftrightarrow> enat m \<le> n"
   1.291    by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   1.292  
   1.293  lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   1.294 @@ -433,7 +433,7 @@
   1.295  
   1.296  
   1.297  lemma min_enat_simps [simp]:
   1.298 -  "min (Fin m) (Fin n) = Fin (min m n)"
   1.299 +  "min (enat m) (enat n) = enat (min m n)"
   1.300    "min q 0 = 0"
   1.301    "min 0 q = 0"
   1.302    "min q (\<infinity>::enat) = q"
   1.303 @@ -441,28 +441,28 @@
   1.304    by (auto simp add: min_def)
   1.305  
   1.306  lemma max_enat_simps [simp]:
   1.307 -  "max (Fin m) (Fin n) = Fin (max m n)"
   1.308 +  "max (enat m) (enat n) = enat (max m n)"
   1.309    "max q 0 = q"
   1.310    "max 0 q = q"
   1.311    "max q \<infinity> = (\<infinity>::enat)"
   1.312    "max \<infinity> q = (\<infinity>::enat)"
   1.313    by (simp_all add: max_def)
   1.314  
   1.315 -lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   1.316 +lemma enat_ile: "n \<le> enat m \<Longrightarrow> \<exists>k. n = enat k"
   1.317    by (cases n) simp_all
   1.318  
   1.319 -lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   1.320 +lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k"
   1.321    by (cases n) simp_all
   1.322  
   1.323 -lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   1.324 +lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j"
   1.325  apply (induct_tac k)
   1.326 - apply (simp (no_asm) only: Fin_0)
   1.327 + apply (simp (no_asm) only: enat_0)
   1.328   apply (fast intro: le_less_trans [OF i0_lb])
   1.329  apply (erule exE)
   1.330  apply (drule spec)
   1.331  apply (erule exE)
   1.332  apply (drule ileI1)
   1.333 -apply (rule iSuc_Fin [THEN subst])
   1.334 +apply (rule iSuc_enat [THEN subst])
   1.335  apply (rule exI)
   1.336  apply (erule (1) le_less_trans)
   1.337  done
   1.338 @@ -481,46 +481,46 @@
   1.339  
   1.340  end
   1.341  
   1.342 -lemma finite_Fin_bounded:
   1.343 -  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   1.344 +lemma finite_enat_bounded:
   1.345 +  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> enat n"
   1.346    shows "finite A"
   1.347  proof (rule finite_subset)
   1.348 -  show "finite (Fin ` {..n})" by blast
   1.349 +  show "finite (enat ` {..n})" by blast
   1.350  
   1.351 -  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   1.352 -  also have "\<dots> \<subseteq> Fin ` {..n}"
   1.353 +  have "A \<subseteq> {..enat n}" using le_fin by fastsimp
   1.354 +  also have "\<dots> \<subseteq> enat ` {..n}"
   1.355      by (rule subsetI) (case_tac x, auto)
   1.356 -  finally show "A \<subseteq> Fin ` {..n}" .
   1.357 +  finally show "A \<subseteq> enat ` {..n}" .
   1.358  qed
   1.359  
   1.360  
   1.361  subsection {* Well-ordering *}
   1.362  
   1.363 -lemma less_FinE:
   1.364 -  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   1.365 +lemma less_enatE:
   1.366 +  "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
   1.367  by (induct n) auto
   1.368  
   1.369  lemma less_InftyE:
   1.370 -  "[| n < \<infinity>; !!k. n = Fin k ==> P |] ==> P"
   1.371 +  "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
   1.372  by (induct n) auto
   1.373  
   1.374  lemma enat_less_induct:
   1.375    assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
   1.376  proof -
   1.377 -  have P_Fin: "!!k. P (Fin k)"
   1.378 +  have P_enat: "!!k. P (enat k)"
   1.379      apply (rule nat_less_induct)
   1.380      apply (rule prem, clarify)
   1.381 -    apply (erule less_FinE, simp)
   1.382 +    apply (erule less_enatE, simp)
   1.383      done
   1.384    show ?thesis
   1.385    proof (induct n)
   1.386      fix nat
   1.387 -    show "P (Fin nat)" by (rule P_Fin)
   1.388 +    show "P (enat nat)" by (rule P_enat)
   1.389    next
   1.390      show "P \<infinity>"
   1.391        apply (rule prem, clarify)
   1.392        apply (erule less_InftyE)
   1.393 -      apply (simp add: P_Fin)
   1.394 +      apply (simp add: P_enat)
   1.395        done
   1.396    qed
   1.397  qed
   1.398 @@ -560,7 +560,7 @@
   1.399    { assume "x \<in> A" then show "x \<le> Sup A"
   1.400        unfolding Sup_enat_def by (cases "finite A") auto }
   1.401    { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   1.402 -      unfolding Sup_enat_def using finite_Fin_bounded by auto }
   1.403 +      unfolding Sup_enat_def using finite_enat_bounded by auto }
   1.404  qed (simp_all add: inf_enat_def sup_enat_def)
   1.405  end
   1.406