rename Nat_Infinity (inat) to Extended_Nat (enat)
authorhoelzl
Tue Jul 19 14:35:44 2011 +0200 (2011-07-19)
changeset 43919a7e4fb1a0502
parent 43903 1e2aa420c660
child 43920 cedb5cb948fd
rename Nat_Infinity (inat) to Extended_Nat (enat)
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/IsaMakefile
src/HOL/HOLCF/Library/Stream.thy
src/HOL/IsaMakefile
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Library.thy
src/HOL/Library/Nat_Infinity.thy
     1.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Tue Jul 19 14:35:44 2011 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  by (simp add: fsingleton_def2)
     1.5  
     1.6  lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
     1.7 -by (simp add: fsingleton_def2 inat_defs)
     1.8 +by (simp add: fsingleton_def2 enat_defs)
     1.9  
    1.10  lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
    1.11  by (simp add: fsingleton_def2)
    1.12 @@ -83,11 +83,11 @@
    1.13  lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    1.14  apply (simp add: jth_def, auto)
    1.15  apply (simp add: i_th_def rt_sconc1)
    1.16 -by (simp add: inat_defs split: inat.splits)
    1.17 +by (simp add: enat_defs split: enat.splits)
    1.18  
    1.19  lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    1.20  apply (simp add: last_def)
    1.21 -apply (simp add: inat_defs split:inat.splits)
    1.22 +apply (simp add: enat_defs split:enat.splits)
    1.23  by (drule sym, auto)
    1.24  
    1.25  lemma last_fsingleton[simp]: "last (<a>) = a"
    1.26 @@ -97,13 +97,13 @@
    1.27  by (simp add: first_def jth_def)
    1.28  
    1.29  lemma last_UU[simp]:"last UU = undefined"
    1.30 -by (simp add: last_def jth_def inat_defs)
    1.31 +by (simp add: last_def jth_def enat_defs)
    1.32  
    1.33  lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
    1.34  by (simp add: last_def)
    1.35  
    1.36  lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
    1.37 -by (simp add: jth_def inat_defs split:inat.splits, auto)
    1.38 +by (simp add: jth_def enat_defs split:enat.splits, auto)
    1.39  
    1.40  lemma jth_UU[simp]:"jth n UU = undefined" 
    1.41  by (simp add: jth_def)
     2.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 11:15:38 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Tue Jul 19 14:35:44 2011 +0200
     2.3 @@ -74,7 +74,7 @@
     2.4  apply (   erule spec)
     2.5  apply (  assumption)
     2.6  apply ( assumption)
     2.7 -apply (metis inat_ord_code(4) slen_infinite)
     2.8 +apply (metis enat_ord_code(4) slen_infinite)
     2.9  done
    2.10  
    2.11  (* should be without reference to stream length? *)
     3.1 --- a/src/HOL/HOLCF/IsaMakefile	Tue Jul 19 11:15:38 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/IsaMakefile	Tue Jul 19 14:35:44 2011 +0200
     3.3 @@ -134,7 +134,7 @@
     3.4  HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
     3.5  
     3.6  $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
     3.7 -  ../Library/Nat_Infinity.thy \
     3.8 +  ../Library/Extended_Nat.thy \
     3.9    ex/Concurrency_Monad.thy \
    3.10    ex/Dagstuhl.thy \
    3.11    ex/Dnat.thy \
     4.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 11:15:38 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Tue Jul 19 14:35:44 2011 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* General Stream domain *}
     4.5  
     4.6  theory Stream
     4.7 -imports HOLCF "~~/src/HOL/Library/Nat_Infinity"
     4.8 +imports HOLCF "~~/src/HOL/Library/Extended_Nat"
     4.9  begin
    4.10  
    4.11  default_sort pcpo
    4.12 @@ -22,7 +22,7 @@
    4.13                                       If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
    4.14  
    4.15  definition
    4.16 -  slen :: "'a stream \<Rightarrow> inat"  ("#_" [1000] 1000) where
    4.17 +  slen :: "'a stream \<Rightarrow> enat"  ("#_" [1000] 1000) where
    4.18    "#s = (if stream_finite s then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
    4.19  
    4.20  
    4.21 @@ -327,7 +327,7 @@
    4.22  section "slen"
    4.23  
    4.24  lemma slen_empty [simp]: "#\<bottom> = 0"
    4.25 -by (simp add: slen_def stream.finite_def zero_inat_def Least_equality)
    4.26 +by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
    4.27  
    4.28  lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
    4.29  apply (case_tac "stream_finite (x && xs)")
    4.30 @@ -361,7 +361,7 @@
    4.31  
    4.32  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
    4.33   apply (cases x, auto)
    4.34 -   apply (simp add: zero_inat_def)
    4.35 +   apply (simp add: zero_enat_def)
    4.36    apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    4.37   apply (case_tac "#stream") apply (simp_all add: iSuc_Fin)
    4.38  done
    4.39 @@ -445,7 +445,7 @@
    4.40  
    4.41  lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i$rt$x)"
    4.42  apply (induct i, auto)
    4.43 -apply (case_tac "x=UU", auto simp add: zero_inat_def)
    4.44 +apply (case_tac "x=UU", auto simp add: zero_enat_def)
    4.45  apply (drule stream_exhaust_eq [THEN iffD1], auto)
    4.46  apply (erule_tac x="y" in allE, auto)
    4.47  apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
    4.48 @@ -455,7 +455,7 @@
    4.49    "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
    4.50  apply (induct_tac n, auto)
    4.51  apply (case_tac "x=UU", auto)
    4.52 -apply (simp add: zero_inat_def)
    4.53 +apply (simp add: zero_enat_def)
    4.54  apply (simp add: Suc_ile_eq)
    4.55  apply (case_tac "y=UU", clarsimp)
    4.56  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
    4.57 @@ -566,11 +566,11 @@
    4.58   apply (subgoal_tac "#(i_rt n s)=0")
    4.59    apply (case_tac "stream_take n$s = s",simp+)
    4.60    apply (insert slen_take_eq [rule_format,of n s],simp)
    4.61 -  apply (cases "#s") apply (simp_all add: zero_inat_def)
    4.62 +  apply (cases "#s") apply (simp_all add: zero_enat_def)
    4.63    apply (simp add: slen_take_eq)
    4.64    apply (cases "#s")
    4.65    using i_rt_take_lemma1 [of n s]
    4.66 -  apply (simp_all add: zero_inat_def)
    4.67 +  apply (simp_all add: zero_enat_def)
    4.68    done
    4.69  
    4.70  lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
    4.71 @@ -585,20 +585,20 @@
    4.72                              #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j
    4.73                                                --> Fin (j + t) = #x"
    4.74  apply (induct n, auto)
    4.75 - apply (simp add: zero_inat_def)
    4.76 + apply (simp add: zero_enat_def)
    4.77  apply (case_tac "x=UU",auto)
    4.78 - apply (simp add: zero_inat_def)
    4.79 + apply (simp add: zero_enat_def)
    4.80  apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
    4.81  apply (subgoal_tac "EX k. Fin k = #y",clarify)
    4.82   apply (erule_tac x="k" in allE)
    4.83   apply (erule_tac x="y" in allE,auto)
    4.84   apply (erule_tac x="THE p. Suc p = t" in allE,auto)
    4.85 -   apply (simp add: iSuc_def split: inat.splits)
    4.86 -  apply (simp add: iSuc_def split: inat.splits)
    4.87 +   apply (simp add: iSuc_def split: enat.splits)
    4.88 +  apply (simp add: iSuc_def split: enat.splits)
    4.89    apply (simp only: the_equality)
    4.90 - apply (simp add: iSuc_def split: inat.splits)
    4.91 + apply (simp add: iSuc_def split: enat.splits)
    4.92   apply force
    4.93 -apply (simp add: iSuc_def split: inat.splits)
    4.94 +apply (simp add: iSuc_def split: enat.splits)
    4.95  done
    4.96  
    4.97  lemma take_i_rt_len:
    4.98 @@ -690,13 +690,13 @@
    4.99  (* ----------------------------------------------------------------------- *)
   4.100  
   4.101  lemma UU_sconc [simp]: " UU ooo s = s "
   4.102 -by (simp add: sconc_def zero_inat_def)
   4.103 +by (simp add: sconc_def zero_enat_def)
   4.104  
   4.105  lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
   4.106  by auto
   4.107  
   4.108  lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
   4.109 -apply (simp add: sconc_def zero_inat_def iSuc_def split: inat.splits, auto)
   4.110 +apply (simp add: sconc_def zero_enat_def iSuc_def split: enat.splits, auto)
   4.111  apply (rule someI2_ex,auto)
   4.112   apply (rule_tac x="x && y" in exI,auto)
   4.113  apply (simp add: i_rt_Suc_forw)
   4.114 @@ -709,12 +709,12 @@
   4.115   apply (rule stream_finite_ind [of x],auto)
   4.116    apply (simp add: stream.finite_def)
   4.117    apply (drule slen_take_lemma1,blast)
   4.118 - apply (simp_all add: zero_inat_def iSuc_def split: inat.splits)
   4.119 + apply (simp_all add: zero_enat_def iSuc_def split: enat.splits)
   4.120  apply (erule_tac x="y" in allE,auto)
   4.121  by (rule_tac x="a && w" in exI,auto)
   4.122  
   4.123  lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"
   4.124 -apply (simp add: sconc_def split: inat.splits, arith?,auto)
   4.125 +apply (simp add: sconc_def split: enat.splits, arith?,auto)
   4.126  apply (rule someI2_ex,auto)
   4.127  by (drule ex_sconc,simp)
   4.128  
   4.129 @@ -948,7 +948,7 @@
   4.130  (* ----------------------------------------------------------------------- *)
   4.131  
   4.132  lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
   4.133 -by (simp add: constr_sconc_def zero_inat_def)
   4.134 +by (simp add: constr_sconc_def zero_enat_def)
   4.135  
   4.136  lemma "x ooo y = constr_sconc x y"
   4.137  apply (case_tac "#x")
     5.1 --- a/src/HOL/IsaMakefile	Tue Jul 19 11:15:38 2011 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Tue Jul 19 14:35:44 2011 +0200
     5.3 @@ -444,25 +444,25 @@
     5.4    Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
     5.5    Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
     5.6    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
     5.7 -  Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy			\
     5.8 -  Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
     5.9 -  Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
    5.10 -  Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
    5.11 -  Library/Dlist_Cset.thy 						\
    5.12 +  Library/Code_Char_ord.thy Library/Code_Integer.thy			\
    5.13 +  Library/Code_Natural.thy Library/Code_Prolog.thy			\
    5.14 +  Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
    5.15 +  Library/Continuity.thy Library/Convex.thy Library/Countable.thy	\
    5.16 +  Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy 	\
    5.17    Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
    5.18    Library/Executable_Set.thy Library/Extended_Reals.thy			\
    5.19 -  Library/Float.thy Library/Formal_Power_Series.thy			\
    5.20 -  Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy	\
    5.21 -  Library/FuncSet.thy Library/Function_Algebras.thy			\
    5.22 -  Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
    5.23 -  Library/Indicator_Function.thy Library/Infinite_Set.thy		\
    5.24 -  Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
    5.25 -  Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
    5.26 -  Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy 	\
    5.27 -  Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
    5.28 -  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
    5.29 -  Library/Multiset.thy Library/Nat_Bijection.thy			\
    5.30 -  Library/Nat_Infinity.thy Library/Nested_Environment.thy		\
    5.31 +  Library/Extended_Nat.thy Library/Float.thy				\
    5.32 +  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    5.33 +  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
    5.34 +  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
    5.35 +  Library/Glbs.thy Library/Indicator_Function.thy			\
    5.36 +  Library/Infinite_Set.thy Library/Inner_Product.thy			\
    5.37 +  Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\
    5.38 +  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
    5.39 +  Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy	\
    5.40 +  Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
    5.41 +  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
    5.42 +  Library/Nat_Bijection.thy Library/Nested_Environment.thy		\
    5.43    Library/Numeral_Type.thy Library/OptionalSugar.thy			\
    5.44    Library/Order_Relation.thy Library/Permutation.thy			\
    5.45    Library/Permutations.thy Library/Poly_Deriv.thy			\
    5.46 @@ -481,7 +481,7 @@
    5.47    Library/Sum_of_Squares/sos_wrapper.ML					\
    5.48    Library/Sum_of_Squares/sum_of_squares.ML				\
    5.49    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    5.50 -  Library/While_Combinator.thy Library/Zorn.thy	\
    5.51 +  Library/While_Combinator.thy Library/Zorn.thy				\
    5.52    $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    5.53    Library/reflection.ML Library/reify_data.ML				\
    5.54    Library/document/root.bib Library/document/root.tex
    5.55 @@ -1576,7 +1576,7 @@
    5.56  HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
    5.57  
    5.58  $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
    5.59 -  Library/Nat_Infinity.thy \
    5.60 +  Library/Extended_Nat.thy \
    5.61    HOLCF/Library/Defl_Bifinite.thy \
    5.62    HOLCF/Library/Bool_Discrete.thy \
    5.63    HOLCF/Library/Char_Discrete.thy \
    5.64 @@ -1630,7 +1630,7 @@
    5.65  HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
    5.66  
    5.67  $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
    5.68 -  Library/Nat_Infinity.thy \
    5.69 +  Library/Extended_Nat.thy \
    5.70    HOLCF/Library/Stream.thy \
    5.71    HOLCF/FOCUS/Fstreams.thy \
    5.72    HOLCF/FOCUS/Fstream.thy \
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:35:44 2011 +0200
     6.3 @@ -0,0 +1,551 @@
     6.4 +(*  Title:      HOL/Library/Extended_Nat.thy
     6.5 +    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
     6.6 +    Contributions: David Trachtenherz, TU Muenchen
     6.7 +*)
     6.8 +
     6.9 +header {* Extended natural numbers (i.e. with infinity) *}
    6.10 +
    6.11 +theory Extended_Nat
    6.12 +imports Main
    6.13 +begin
    6.14 +
    6.15 +subsection {* Type definition *}
    6.16 +
    6.17 +text {*
    6.18 +  We extend the standard natural numbers by a special value indicating
    6.19 +  infinity.
    6.20 +*}
    6.21 +
    6.22 +datatype enat = Fin nat | Infty
    6.23 +
    6.24 +notation (xsymbols)
    6.25 +  Infty  ("\<infinity>")
    6.26 +
    6.27 +notation (HTML output)
    6.28 +  Infty  ("\<infinity>")
    6.29 +
    6.30 +
    6.31 +lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
    6.32 +by (cases x) auto
    6.33 +
    6.34 +lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
    6.35 +by (cases x) auto
    6.36 +
    6.37 +
    6.38 +primrec the_Fin :: "enat \<Rightarrow> nat"
    6.39 +where "the_Fin (Fin n) = n"
    6.40 +
    6.41 +
    6.42 +subsection {* Constructors and numbers *}
    6.43 +
    6.44 +instantiation enat :: "{zero, one, number}"
    6.45 +begin
    6.46 +
    6.47 +definition
    6.48 +  "0 = Fin 0"
    6.49 +
    6.50 +definition
    6.51 +  [code_unfold]: "1 = Fin 1"
    6.52 +
    6.53 +definition
    6.54 +  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    6.55 +
    6.56 +instance ..
    6.57 +
    6.58 +end
    6.59 +
    6.60 +definition iSuc :: "enat \<Rightarrow> enat" where
    6.61 +  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    6.62 +
    6.63 +lemma Fin_0: "Fin 0 = 0"
    6.64 +  by (simp add: zero_enat_def)
    6.65 +
    6.66 +lemma Fin_1: "Fin 1 = 1"
    6.67 +  by (simp add: one_enat_def)
    6.68 +
    6.69 +lemma Fin_number: "Fin (number_of k) = number_of k"
    6.70 +  by (simp add: number_of_enat_def)
    6.71 +
    6.72 +lemma one_iSuc: "1 = iSuc 0"
    6.73 +  by (simp add: zero_enat_def one_enat_def iSuc_def)
    6.74 +
    6.75 +lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    6.76 +  by (simp add: zero_enat_def)
    6.77 +
    6.78 +lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    6.79 +  by (simp add: zero_enat_def)
    6.80 +
    6.81 +lemma zero_enat_eq [simp]:
    6.82 +  "number_of k = (0\<Colon>enat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    6.83 +  "(0\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    6.84 +  unfolding zero_enat_def number_of_enat_def by simp_all
    6.85 +
    6.86 +lemma one_enat_eq [simp]:
    6.87 +  "number_of k = (1\<Colon>enat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    6.88 +  "(1\<Colon>enat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    6.89 +  unfolding one_enat_def number_of_enat_def by simp_all
    6.90 +
    6.91 +lemma zero_one_enat_neq [simp]:
    6.92 +  "\<not> 0 = (1\<Colon>enat)"
    6.93 +  "\<not> 1 = (0\<Colon>enat)"
    6.94 +  unfolding zero_enat_def one_enat_def by simp_all
    6.95 +
    6.96 +lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
    6.97 +  by (simp add: one_enat_def)
    6.98 +
    6.99 +lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
   6.100 +  by (simp add: one_enat_def)
   6.101 +
   6.102 +lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
   6.103 +  by (simp add: number_of_enat_def)
   6.104 +
   6.105 +lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
   6.106 +  by (simp add: number_of_enat_def)
   6.107 +
   6.108 +lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
   6.109 +  by (simp add: iSuc_def)
   6.110 +
   6.111 +lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
   6.112 +  by (simp add: iSuc_Fin number_of_enat_def)
   6.113 +
   6.114 +lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   6.115 +  by (simp add: iSuc_def)
   6.116 +
   6.117 +lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   6.118 +  by (simp add: iSuc_def zero_enat_def split: enat.splits)
   6.119 +
   6.120 +lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
   6.121 +  by (rule iSuc_ne_0 [symmetric])
   6.122 +
   6.123 +lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
   6.124 +  by (simp add: iSuc_def split: enat.splits)
   6.125 +
   6.126 +lemma number_of_enat_inject [simp]:
   6.127 +  "(number_of k \<Colon> enat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
   6.128 +  by (simp add: number_of_enat_def)
   6.129 +
   6.130 +
   6.131 +subsection {* Addition *}
   6.132 +
   6.133 +instantiation enat :: comm_monoid_add
   6.134 +begin
   6.135 +
   6.136 +definition [nitpick_simp]:
   6.137 +  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   6.138 +
   6.139 +lemma plus_enat_simps [simp, code]:
   6.140 +  "Fin m + Fin n = Fin (m + n)"
   6.141 +  "\<infinity> + q = \<infinity>"
   6.142 +  "q + \<infinity> = \<infinity>"
   6.143 +  by (simp_all add: plus_enat_def split: enat.splits)
   6.144 +
   6.145 +instance proof
   6.146 +  fix n m q :: enat
   6.147 +  show "n + m + q = n + (m + q)"
   6.148 +    by (cases n, auto, cases m, auto, cases q, auto)
   6.149 +  show "n + m = m + n"
   6.150 +    by (cases n, auto, cases m, auto)
   6.151 +  show "0 + n = n"
   6.152 +    by (cases n) (simp_all add: zero_enat_def)
   6.153 +qed
   6.154 +
   6.155 +end
   6.156 +
   6.157 +lemma plus_enat_0 [simp]:
   6.158 +  "0 + (q\<Colon>enat) = q"
   6.159 +  "(q\<Colon>enat) + 0 = q"
   6.160 +  by (simp_all add: plus_enat_def zero_enat_def split: enat.splits)
   6.161 +
   6.162 +lemma plus_enat_number [simp]:
   6.163 +  "(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
   6.164 +    else if l < Int.Pls then number_of k else number_of (k + l))"
   6.165 +  unfolding number_of_enat_def plus_enat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   6.166 +
   6.167 +lemma iSuc_number [simp]:
   6.168 +  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   6.169 +  unfolding iSuc_number_of
   6.170 +  unfolding one_enat_def number_of_enat_def Suc_nat_number_of if_distrib [symmetric] ..
   6.171 +
   6.172 +lemma iSuc_plus_1:
   6.173 +  "iSuc n = n + 1"
   6.174 +  by (cases n) (simp_all add: iSuc_Fin one_enat_def)
   6.175 +  
   6.176 +lemma plus_1_iSuc:
   6.177 +  "1 + q = iSuc q"
   6.178 +  "q + 1 = iSuc q"
   6.179 +by (simp_all add: iSuc_plus_1 add_ac)
   6.180 +
   6.181 +lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   6.182 +by (simp_all add: iSuc_plus_1 add_ac)
   6.183 +
   6.184 +lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   6.185 +by (simp only: add_commute[of m] iadd_Suc)
   6.186 +
   6.187 +lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
   6.188 +by (cases m, cases n, simp_all add: zero_enat_def)
   6.189 +
   6.190 +subsection {* Multiplication *}
   6.191 +
   6.192 +instantiation enat :: comm_semiring_1
   6.193 +begin
   6.194 +
   6.195 +definition times_enat_def [nitpick_simp]:
   6.196 +  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   6.197 +    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   6.198 +
   6.199 +lemma times_enat_simps [simp, code]:
   6.200 +  "Fin m * Fin n = Fin (m * n)"
   6.201 +  "\<infinity> * \<infinity> = \<infinity>"
   6.202 +  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   6.203 +  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   6.204 +  unfolding times_enat_def zero_enat_def
   6.205 +  by (simp_all split: enat.split)
   6.206 +
   6.207 +instance proof
   6.208 +  fix a b c :: enat
   6.209 +  show "(a * b) * c = a * (b * c)"
   6.210 +    unfolding times_enat_def zero_enat_def
   6.211 +    by (simp split: enat.split)
   6.212 +  show "a * b = b * a"
   6.213 +    unfolding times_enat_def zero_enat_def
   6.214 +    by (simp split: enat.split)
   6.215 +  show "1 * a = a"
   6.216 +    unfolding times_enat_def zero_enat_def one_enat_def
   6.217 +    by (simp split: enat.split)
   6.218 +  show "(a + b) * c = a * c + b * c"
   6.219 +    unfolding times_enat_def zero_enat_def
   6.220 +    by (simp split: enat.split add: left_distrib)
   6.221 +  show "0 * a = 0"
   6.222 +    unfolding times_enat_def zero_enat_def
   6.223 +    by (simp split: enat.split)
   6.224 +  show "a * 0 = 0"
   6.225 +    unfolding times_enat_def zero_enat_def
   6.226 +    by (simp split: enat.split)
   6.227 +  show "(0::enat) \<noteq> 1"
   6.228 +    unfolding zero_enat_def one_enat_def
   6.229 +    by simp
   6.230 +qed
   6.231 +
   6.232 +end
   6.233 +
   6.234 +lemma mult_iSuc: "iSuc m * n = n + m * n"
   6.235 +  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   6.236 +
   6.237 +lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   6.238 +  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   6.239 +
   6.240 +lemma of_nat_eq_Fin: "of_nat n = Fin n"
   6.241 +  apply (induct n)
   6.242 +  apply (simp add: Fin_0)
   6.243 +  apply (simp add: plus_1_iSuc iSuc_Fin)
   6.244 +  done
   6.245 +
   6.246 +instance enat :: number_semiring
   6.247 +proof
   6.248 +  fix n show "number_of (int n) = (of_nat n :: enat)"
   6.249 +    unfolding number_of_enat_def number_of_int of_nat_id of_nat_eq_Fin ..
   6.250 +qed
   6.251 +
   6.252 +instance enat :: semiring_char_0 proof
   6.253 +  have "inj Fin" by (rule injI) simp
   6.254 +  then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_Fin)
   6.255 +qed
   6.256 +
   6.257 +lemma imult_is_0[simp]: "((m::enat) * n = 0) = (m = 0 \<or> n = 0)"
   6.258 +by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.259 +
   6.260 +lemma imult_is_Infty: "((a::enat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   6.261 +by(auto simp add: times_enat_def zero_enat_def split: enat.split)
   6.262 +
   6.263 +
   6.264 +subsection {* Subtraction *}
   6.265 +
   6.266 +instantiation enat :: minus
   6.267 +begin
   6.268 +
   6.269 +definition diff_enat_def:
   6.270 +"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   6.271 +          | \<infinity> \<Rightarrow> \<infinity>)"
   6.272 +
   6.273 +instance ..
   6.274 +
   6.275 +end
   6.276 +
   6.277 +lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   6.278 +by(simp add: diff_enat_def)
   6.279 +
   6.280 +lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
   6.281 +by(simp add: diff_enat_def)
   6.282 +
   6.283 +lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   6.284 +by(simp add: diff_enat_def)
   6.285 +
   6.286 +lemma idiff_0[simp]: "(0::enat) - n = 0"
   6.287 +by (cases n, simp_all add: zero_enat_def)
   6.288 +
   6.289 +lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_enat_def]
   6.290 +
   6.291 +lemma idiff_0_right[simp]: "(n::enat) - 0 = n"
   6.292 +by (cases n) (simp_all add: zero_enat_def)
   6.293 +
   6.294 +lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_enat_def]
   6.295 +
   6.296 +lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::enat) - n = 0"
   6.297 +by(auto simp: zero_enat_def)
   6.298 +
   6.299 +lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
   6.300 +by(simp add: iSuc_def split: enat.split)
   6.301 +
   6.302 +lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   6.303 +by(simp add: one_enat_def iSuc_Fin[symmetric] zero_enat_def[symmetric])
   6.304 +
   6.305 +(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_enat_def]*)
   6.306 +
   6.307 +
   6.308 +subsection {* Ordering *}
   6.309 +
   6.310 +instantiation enat :: linordered_ab_semigroup_add
   6.311 +begin
   6.312 +
   6.313 +definition [nitpick_simp]:
   6.314 +  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   6.315 +    | \<infinity> \<Rightarrow> True)"
   6.316 +
   6.317 +definition [nitpick_simp]:
   6.318 +  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   6.319 +    | \<infinity> \<Rightarrow> False)"
   6.320 +
   6.321 +lemma enat_ord_simps [simp]:
   6.322 +  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   6.323 +  "Fin m < Fin n \<longleftrightarrow> m < n"
   6.324 +  "q \<le> \<infinity>"
   6.325 +  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
   6.326 +  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
   6.327 +  "\<infinity> < q \<longleftrightarrow> False"
   6.328 +  by (simp_all add: less_eq_enat_def less_enat_def split: enat.splits)
   6.329 +
   6.330 +lemma enat_ord_code [code]:
   6.331 +  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   6.332 +  "Fin m < Fin n \<longleftrightarrow> m < n"
   6.333 +  "q \<le> \<infinity> \<longleftrightarrow> True"
   6.334 +  "Fin m < \<infinity> \<longleftrightarrow> True"
   6.335 +  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   6.336 +  "\<infinity> < q \<longleftrightarrow> False"
   6.337 +  by simp_all
   6.338 +
   6.339 +instance by default
   6.340 +  (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
   6.341 +
   6.342 +end
   6.343 +
   6.344 +instance enat :: ordered_comm_semiring
   6.345 +proof
   6.346 +  fix a b c :: enat
   6.347 +  assume "a \<le> b" and "0 \<le> c"
   6.348 +  thus "c * a \<le> c * b"
   6.349 +    unfolding times_enat_def less_eq_enat_def zero_enat_def
   6.350 +    by (simp split: enat.splits)
   6.351 +qed
   6.352 +
   6.353 +lemma enat_ord_number [simp]:
   6.354 +  "(number_of m \<Colon> enat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   6.355 +  "(number_of m \<Colon> enat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   6.356 +  by (simp_all add: number_of_enat_def)
   6.357 +
   6.358 +lemma i0_lb [simp]: "(0\<Colon>enat) \<le> n"
   6.359 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.360 +
   6.361 +lemma ile0_eq [simp]: "n \<le> (0\<Colon>enat) \<longleftrightarrow> n = 0"
   6.362 +by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.363 +
   6.364 +lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   6.365 +  by (simp add: zero_enat_def less_eq_enat_def split: enat.splits)
   6.366 +
   6.367 +lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   6.368 +  by simp
   6.369 +
   6.370 +lemma not_iless0 [simp]: "\<not> n < (0\<Colon>enat)"
   6.371 +  by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.372 +
   6.373 +lemma i0_less [simp]: "(0\<Colon>enat) < n \<longleftrightarrow> n \<noteq> 0"
   6.374 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.375 +
   6.376 +lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
   6.377 +  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   6.378 + 
   6.379 +lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
   6.380 +  by (simp add: iSuc_def less_enat_def split: enat.splits)
   6.381 +
   6.382 +lemma ile_iSuc [simp]: "n \<le> iSuc n"
   6.383 +  by (simp add: iSuc_def less_eq_enat_def split: enat.splits)
   6.384 +
   6.385 +lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   6.386 +  by (simp add: zero_enat_def iSuc_def less_eq_enat_def split: enat.splits)
   6.387 +
   6.388 +lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   6.389 +  by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.splits)
   6.390 +
   6.391 +lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
   6.392 +by (simp add: zero_enat_def iSuc_def less_enat_def split: enat.split)
   6.393 +
   6.394 +lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   6.395 +  by (simp add: iSuc_def less_eq_enat_def less_enat_def split: enat.splits)
   6.396 +
   6.397 +lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   6.398 +  by (cases n) auto
   6.399 +
   6.400 +lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   6.401 +  by (auto simp add: iSuc_def less_enat_def split: enat.splits)
   6.402 +
   6.403 +lemma imult_Infty: "(0::enat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   6.404 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.405 +
   6.406 +lemma imult_Infty_right: "(0::enat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   6.407 +by (simp add: zero_enat_def less_enat_def split: enat.splits)
   6.408 +
   6.409 +lemma enat_0_less_mult_iff: "(0 < (m::enat) * n) = (0 < m \<and> 0 < n)"
   6.410 +by (simp only: i0_less imult_is_0, simp)
   6.411 +
   6.412 +lemma mono_iSuc: "mono iSuc"
   6.413 +by(simp add: mono_def)
   6.414 +
   6.415 +
   6.416 +lemma min_enat_simps [simp]:
   6.417 +  "min (Fin m) (Fin n) = Fin (min m n)"
   6.418 +  "min q 0 = 0"
   6.419 +  "min 0 q = 0"
   6.420 +  "min q \<infinity> = q"
   6.421 +  "min \<infinity> q = q"
   6.422 +  by (auto simp add: min_def)
   6.423 +
   6.424 +lemma max_enat_simps [simp]:
   6.425 +  "max (Fin m) (Fin n) = Fin (max m n)"
   6.426 +  "max q 0 = q"
   6.427 +  "max 0 q = q"
   6.428 +  "max q \<infinity> = \<infinity>"
   6.429 +  "max \<infinity> q = \<infinity>"
   6.430 +  by (simp_all add: max_def)
   6.431 +
   6.432 +lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   6.433 +  by (cases n) simp_all
   6.434 +
   6.435 +lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   6.436 +  by (cases n) simp_all
   6.437 +
   6.438 +lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   6.439 +apply (induct_tac k)
   6.440 + apply (simp (no_asm) only: Fin_0)
   6.441 + apply (fast intro: le_less_trans [OF i0_lb])
   6.442 +apply (erule exE)
   6.443 +apply (drule spec)
   6.444 +apply (erule exE)
   6.445 +apply (drule ileI1)
   6.446 +apply (rule iSuc_Fin [THEN subst])
   6.447 +apply (rule exI)
   6.448 +apply (erule (1) le_less_trans)
   6.449 +done
   6.450 +
   6.451 +instantiation enat :: "{bot, top}"
   6.452 +begin
   6.453 +
   6.454 +definition bot_enat :: enat where
   6.455 +  "bot_enat = 0"
   6.456 +
   6.457 +definition top_enat :: enat where
   6.458 +  "top_enat = \<infinity>"
   6.459 +
   6.460 +instance proof
   6.461 +qed (simp_all add: bot_enat_def top_enat_def)
   6.462 +
   6.463 +end
   6.464 +
   6.465 +lemma finite_Fin_bounded:
   6.466 +  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   6.467 +  shows "finite A"
   6.468 +proof (rule finite_subset)
   6.469 +  show "finite (Fin ` {..n})" by blast
   6.470 +
   6.471 +  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   6.472 +  also have "\<dots> \<subseteq> Fin ` {..n}"
   6.473 +    by (rule subsetI) (case_tac x, auto)
   6.474 +  finally show "A \<subseteq> Fin ` {..n}" .
   6.475 +qed
   6.476 +
   6.477 +
   6.478 +subsection {* Well-ordering *}
   6.479 +
   6.480 +lemma less_FinE:
   6.481 +  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   6.482 +by (induct n) auto
   6.483 +
   6.484 +lemma less_InftyE:
   6.485 +  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
   6.486 +by (induct n) auto
   6.487 +
   6.488 +lemma enat_less_induct:
   6.489 +  assumes prem: "!!n. \<forall>m::enat. m < n --> P m ==> P n" shows "P n"
   6.490 +proof -
   6.491 +  have P_Fin: "!!k. P (Fin k)"
   6.492 +    apply (rule nat_less_induct)
   6.493 +    apply (rule prem, clarify)
   6.494 +    apply (erule less_FinE, simp)
   6.495 +    done
   6.496 +  show ?thesis
   6.497 +  proof (induct n)
   6.498 +    fix nat
   6.499 +    show "P (Fin nat)" by (rule P_Fin)
   6.500 +  next
   6.501 +    show "P Infty"
   6.502 +      apply (rule prem, clarify)
   6.503 +      apply (erule less_InftyE)
   6.504 +      apply (simp add: P_Fin)
   6.505 +      done
   6.506 +  qed
   6.507 +qed
   6.508 +
   6.509 +instance enat :: wellorder
   6.510 +proof
   6.511 +  fix P and n
   6.512 +  assume hyp: "(\<And>n\<Colon>enat. (\<And>m\<Colon>enat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
   6.513 +  show "P n" by (blast intro: enat_less_induct hyp)
   6.514 +qed
   6.515 +
   6.516 +subsection {* Complete Lattice *}
   6.517 +
   6.518 +instantiation enat :: complete_lattice
   6.519 +begin
   6.520 +
   6.521 +definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   6.522 +  "inf_enat \<equiv> min"
   6.523 +
   6.524 +definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
   6.525 +  "sup_enat \<equiv> max"
   6.526 +
   6.527 +definition Inf_enat :: "enat set \<Rightarrow> enat" where
   6.528 +  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
   6.529 +
   6.530 +definition Sup_enat :: "enat set \<Rightarrow> enat" where
   6.531 +  "Sup_enat A \<equiv> if A = {} then 0
   6.532 +    else if finite A then Max A
   6.533 +                     else \<infinity>"
   6.534 +instance proof
   6.535 +  fix x :: "enat" and A :: "enat set"
   6.536 +  { assume "x \<in> A" then show "Inf A \<le> x"
   6.537 +      unfolding Inf_enat_def by (auto intro: Least_le) }
   6.538 +  { assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A"
   6.539 +      unfolding Inf_enat_def
   6.540 +      by (cases "A = {}") (auto intro: LeastI2_ex) }
   6.541 +  { assume "x \<in> A" then show "x \<le> Sup A"
   6.542 +      unfolding Sup_enat_def by (cases "finite A") auto }
   6.543 +  { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   6.544 +      unfolding Sup_enat_def using finite_Fin_bounded by auto }
   6.545 +qed (simp_all add: inf_enat_def sup_enat_def)
   6.546 +end
   6.547 +
   6.548 +
   6.549 +subsection {* Traditional theorem names *}
   6.550 +
   6.551 +lemmas enat_defs = zero_enat_def one_enat_def number_of_enat_def iSuc_def
   6.552 +  plus_enat_def less_eq_enat_def less_enat_def
   6.553 +
   6.554 +end
     7.1 --- a/src/HOL/Library/Library.thy	Tue Jul 19 11:15:38 2011 +0200
     7.2 +++ b/src/HOL/Library/Library.thy	Tue Jul 19 14:35:44 2011 +0200
     7.3 @@ -15,6 +15,7 @@
     7.4    Diagonalize
     7.5    Dlist_Cset
     7.6    Eval_Witness
     7.7 +  Extended_Nat
     7.8    Float
     7.9    Formal_Power_Series
    7.10    Fraction_Field
    7.11 @@ -35,7 +36,6 @@
    7.12    Monad_Syntax
    7.13    More_List
    7.14    Multiset
    7.15 -  Nat_Infinity
    7.16    Nested_Environment
    7.17    Numeral_Type
    7.18    OptionalSugar
     8.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Jul 19 11:15:38 2011 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,551 +0,0 @@
     8.4 -(*  Title:      HOL/Library/Nat_Infinity.thy
     8.5 -    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
     8.6 -    Contributions: David Trachtenherz, TU Muenchen
     8.7 -*)
     8.8 -
     8.9 -header {* Natural numbers with infinity *}
    8.10 -
    8.11 -theory Nat_Infinity
    8.12 -imports Main
    8.13 -begin
    8.14 -
    8.15 -subsection {* Type definition *}
    8.16 -
    8.17 -text {*
    8.18 -  We extend the standard natural numbers by a special value indicating
    8.19 -  infinity.
    8.20 -*}
    8.21 -
    8.22 -datatype inat = Fin nat | Infty
    8.23 -
    8.24 -notation (xsymbols)
    8.25 -  Infty  ("\<infinity>")
    8.26 -
    8.27 -notation (HTML output)
    8.28 -  Infty  ("\<infinity>")
    8.29 -
    8.30 -
    8.31 -lemma not_Infty_eq[iff]: "(x ~= Infty) = (EX i. x = Fin i)"
    8.32 -by (cases x) auto
    8.33 -
    8.34 -lemma not_Fin_eq [iff]: "(ALL y. x ~= Fin y) = (x = Infty)"
    8.35 -by (cases x) auto
    8.36 -
    8.37 -
    8.38 -primrec the_Fin :: "inat \<Rightarrow> nat"
    8.39 -where "the_Fin (Fin n) = n"
    8.40 -
    8.41 -
    8.42 -subsection {* Constructors and numbers *}
    8.43 -
    8.44 -instantiation inat :: "{zero, one, number}"
    8.45 -begin
    8.46 -
    8.47 -definition
    8.48 -  "0 = Fin 0"
    8.49 -
    8.50 -definition
    8.51 -  [code_unfold]: "1 = Fin 1"
    8.52 -
    8.53 -definition
    8.54 -  [code_unfold, code del]: "number_of k = Fin (number_of k)"
    8.55 -
    8.56 -instance ..
    8.57 -
    8.58 -end
    8.59 -
    8.60 -definition iSuc :: "inat \<Rightarrow> inat" where
    8.61 -  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
    8.62 -
    8.63 -lemma Fin_0: "Fin 0 = 0"
    8.64 -  by (simp add: zero_inat_def)
    8.65 -
    8.66 -lemma Fin_1: "Fin 1 = 1"
    8.67 -  by (simp add: one_inat_def)
    8.68 -
    8.69 -lemma Fin_number: "Fin (number_of k) = number_of k"
    8.70 -  by (simp add: number_of_inat_def)
    8.71 -
    8.72 -lemma one_iSuc: "1 = iSuc 0"
    8.73 -  by (simp add: zero_inat_def one_inat_def iSuc_def)
    8.74 -
    8.75 -lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    8.76 -  by (simp add: zero_inat_def)
    8.77 -
    8.78 -lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    8.79 -  by (simp add: zero_inat_def)
    8.80 -
    8.81 -lemma zero_inat_eq [simp]:
    8.82 -  "number_of k = (0\<Colon>inat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    8.83 -  "(0\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
    8.84 -  unfolding zero_inat_def number_of_inat_def by simp_all
    8.85 -
    8.86 -lemma one_inat_eq [simp]:
    8.87 -  "number_of k = (1\<Colon>inat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    8.88 -  "(1\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
    8.89 -  unfolding one_inat_def number_of_inat_def by simp_all
    8.90 -
    8.91 -lemma zero_one_inat_neq [simp]:
    8.92 -  "\<not> 0 = (1\<Colon>inat)"
    8.93 -  "\<not> 1 = (0\<Colon>inat)"
    8.94 -  unfolding zero_inat_def one_inat_def by simp_all
    8.95 -
    8.96 -lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
    8.97 -  by (simp add: one_inat_def)
    8.98 -
    8.99 -lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
   8.100 -  by (simp add: one_inat_def)
   8.101 -
   8.102 -lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
   8.103 -  by (simp add: number_of_inat_def)
   8.104 -
   8.105 -lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
   8.106 -  by (simp add: number_of_inat_def)
   8.107 -
   8.108 -lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
   8.109 -  by (simp add: iSuc_def)
   8.110 -
   8.111 -lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
   8.112 -  by (simp add: iSuc_Fin number_of_inat_def)
   8.113 -
   8.114 -lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
   8.115 -  by (simp add: iSuc_def)
   8.116 -
   8.117 -lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
   8.118 -  by (simp add: iSuc_def zero_inat_def split: inat.splits)
   8.119 -
   8.120 -lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
   8.121 -  by (rule iSuc_ne_0 [symmetric])
   8.122 -
   8.123 -lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
   8.124 -  by (simp add: iSuc_def split: inat.splits)
   8.125 -
   8.126 -lemma number_of_inat_inject [simp]:
   8.127 -  "(number_of k \<Colon> inat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
   8.128 -  by (simp add: number_of_inat_def)
   8.129 -
   8.130 -
   8.131 -subsection {* Addition *}
   8.132 -
   8.133 -instantiation inat :: comm_monoid_add
   8.134 -begin
   8.135 -
   8.136 -definition [nitpick_simp]:
   8.137 -  "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
   8.138 -
   8.139 -lemma plus_inat_simps [simp, code]:
   8.140 -  "Fin m + Fin n = Fin (m + n)"
   8.141 -  "\<infinity> + q = \<infinity>"
   8.142 -  "q + \<infinity> = \<infinity>"
   8.143 -  by (simp_all add: plus_inat_def split: inat.splits)
   8.144 -
   8.145 -instance proof
   8.146 -  fix n m q :: inat
   8.147 -  show "n + m + q = n + (m + q)"
   8.148 -    by (cases n, auto, cases m, auto, cases q, auto)
   8.149 -  show "n + m = m + n"
   8.150 -    by (cases n, auto, cases m, auto)
   8.151 -  show "0 + n = n"
   8.152 -    by (cases n) (simp_all add: zero_inat_def)
   8.153 -qed
   8.154 -
   8.155 -end
   8.156 -
   8.157 -lemma plus_inat_0 [simp]:
   8.158 -  "0 + (q\<Colon>inat) = q"
   8.159 -  "(q\<Colon>inat) + 0 = q"
   8.160 -  by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
   8.161 -
   8.162 -lemma plus_inat_number [simp]:
   8.163 -  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
   8.164 -    else if l < Int.Pls then number_of k else number_of (k + l))"
   8.165 -  unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
   8.166 -
   8.167 -lemma iSuc_number [simp]:
   8.168 -  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
   8.169 -  unfolding iSuc_number_of
   8.170 -  unfolding one_inat_def number_of_inat_def Suc_nat_number_of if_distrib [symmetric] ..
   8.171 -
   8.172 -lemma iSuc_plus_1:
   8.173 -  "iSuc n = n + 1"
   8.174 -  by (cases n) (simp_all add: iSuc_Fin one_inat_def)
   8.175 -  
   8.176 -lemma plus_1_iSuc:
   8.177 -  "1 + q = iSuc q"
   8.178 -  "q + 1 = iSuc q"
   8.179 -by (simp_all add: iSuc_plus_1 add_ac)
   8.180 -
   8.181 -lemma iadd_Suc: "iSuc m + n = iSuc (m + n)"
   8.182 -by (simp_all add: iSuc_plus_1 add_ac)
   8.183 -
   8.184 -lemma iadd_Suc_right: "m + iSuc n = iSuc (m + n)"
   8.185 -by (simp only: add_commute[of m] iadd_Suc)
   8.186 -
   8.187 -lemma iadd_is_0: "(m + n = (0::inat)) = (m = 0 \<and> n = 0)"
   8.188 -by (cases m, cases n, simp_all add: zero_inat_def)
   8.189 -
   8.190 -subsection {* Multiplication *}
   8.191 -
   8.192 -instantiation inat :: comm_semiring_1
   8.193 -begin
   8.194 -
   8.195 -definition times_inat_def [nitpick_simp]:
   8.196 -  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
   8.197 -    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
   8.198 -
   8.199 -lemma times_inat_simps [simp, code]:
   8.200 -  "Fin m * Fin n = Fin (m * n)"
   8.201 -  "\<infinity> * \<infinity> = \<infinity>"
   8.202 -  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
   8.203 -  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
   8.204 -  unfolding times_inat_def zero_inat_def
   8.205 -  by (simp_all split: inat.split)
   8.206 -
   8.207 -instance proof
   8.208 -  fix a b c :: inat
   8.209 -  show "(a * b) * c = a * (b * c)"
   8.210 -    unfolding times_inat_def zero_inat_def
   8.211 -    by (simp split: inat.split)
   8.212 -  show "a * b = b * a"
   8.213 -    unfolding times_inat_def zero_inat_def
   8.214 -    by (simp split: inat.split)
   8.215 -  show "1 * a = a"
   8.216 -    unfolding times_inat_def zero_inat_def one_inat_def
   8.217 -    by (simp split: inat.split)
   8.218 -  show "(a + b) * c = a * c + b * c"
   8.219 -    unfolding times_inat_def zero_inat_def
   8.220 -    by (simp split: inat.split add: left_distrib)
   8.221 -  show "0 * a = 0"
   8.222 -    unfolding times_inat_def zero_inat_def
   8.223 -    by (simp split: inat.split)
   8.224 -  show "a * 0 = 0"
   8.225 -    unfolding times_inat_def zero_inat_def
   8.226 -    by (simp split: inat.split)
   8.227 -  show "(0::inat) \<noteq> 1"
   8.228 -    unfolding zero_inat_def one_inat_def
   8.229 -    by simp
   8.230 -qed
   8.231 -
   8.232 -end
   8.233 -
   8.234 -lemma mult_iSuc: "iSuc m * n = n + m * n"
   8.235 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   8.236 -
   8.237 -lemma mult_iSuc_right: "m * iSuc n = m + m * n"
   8.238 -  unfolding iSuc_plus_1 by (simp add: algebra_simps)
   8.239 -
   8.240 -lemma of_nat_eq_Fin: "of_nat n = Fin n"
   8.241 -  apply (induct n)
   8.242 -  apply (simp add: Fin_0)
   8.243 -  apply (simp add: plus_1_iSuc iSuc_Fin)
   8.244 -  done
   8.245 -
   8.246 -instance inat :: number_semiring
   8.247 -proof
   8.248 -  fix n show "number_of (int n) = (of_nat n :: inat)"
   8.249 -    unfolding number_of_inat_def number_of_int of_nat_id of_nat_eq_Fin ..
   8.250 -qed
   8.251 -
   8.252 -instance inat :: semiring_char_0 proof
   8.253 -  have "inj Fin" by (rule injI) simp
   8.254 -  then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
   8.255 -qed
   8.256 -
   8.257 -lemma imult_is_0[simp]: "((m::inat) * n = 0) = (m = 0 \<or> n = 0)"
   8.258 -by(auto simp add: times_inat_def zero_inat_def split: inat.split)
   8.259 -
   8.260 -lemma imult_is_Infty: "((a::inat) * b = \<infinity>) = (a = \<infinity> \<and> b \<noteq> 0 \<or> b = \<infinity> \<and> a \<noteq> 0)"
   8.261 -by(auto simp add: times_inat_def zero_inat_def split: inat.split)
   8.262 -
   8.263 -
   8.264 -subsection {* Subtraction *}
   8.265 -
   8.266 -instantiation inat :: minus
   8.267 -begin
   8.268 -
   8.269 -definition diff_inat_def:
   8.270 -"a - b = (case a of (Fin x) \<Rightarrow> (case b of (Fin y) \<Rightarrow> Fin (x - y) | \<infinity> \<Rightarrow> 0)
   8.271 -          | \<infinity> \<Rightarrow> \<infinity>)"
   8.272 -
   8.273 -instance ..
   8.274 -
   8.275 -end
   8.276 -
   8.277 -lemma idiff_Fin_Fin[simp,code]: "Fin a - Fin b = Fin (a - b)"
   8.278 -by(simp add: diff_inat_def)
   8.279 -
   8.280 -lemma idiff_Infty[simp,code]: "\<infinity> - n = \<infinity>"
   8.281 -by(simp add: diff_inat_def)
   8.282 -
   8.283 -lemma idiff_Infty_right[simp,code]: "Fin a - \<infinity> = 0"
   8.284 -by(simp add: diff_inat_def)
   8.285 -
   8.286 -lemma idiff_0[simp]: "(0::inat) - n = 0"
   8.287 -by (cases n, simp_all add: zero_inat_def)
   8.288 -
   8.289 -lemmas idiff_Fin_0[simp] = idiff_0[unfolded zero_inat_def]
   8.290 -
   8.291 -lemma idiff_0_right[simp]: "(n::inat) - 0 = n"
   8.292 -by (cases n) (simp_all add: zero_inat_def)
   8.293 -
   8.294 -lemmas idiff_Fin_0_right[simp] = idiff_0_right[unfolded zero_inat_def]
   8.295 -
   8.296 -lemma idiff_self[simp]: "n \<noteq> \<infinity> \<Longrightarrow> (n::inat) - n = 0"
   8.297 -by(auto simp: zero_inat_def)
   8.298 -
   8.299 -lemma iSuc_minus_iSuc [simp]: "iSuc n - iSuc m = n - m"
   8.300 -by(simp add: iSuc_def split: inat.split)
   8.301 -
   8.302 -lemma iSuc_minus_1 [simp]: "iSuc n - 1 = n"
   8.303 -by(simp add: one_inat_def iSuc_Fin[symmetric] zero_inat_def[symmetric])
   8.304 -
   8.305 -(*lemmas idiff_self_eq_0_Fin = idiff_self_eq_0[unfolded zero_inat_def]*)
   8.306 -
   8.307 -
   8.308 -subsection {* Ordering *}
   8.309 -
   8.310 -instantiation inat :: linordered_ab_semigroup_add
   8.311 -begin
   8.312 -
   8.313 -definition [nitpick_simp]:
   8.314 -  "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
   8.315 -    | \<infinity> \<Rightarrow> True)"
   8.316 -
   8.317 -definition [nitpick_simp]:
   8.318 -  "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
   8.319 -    | \<infinity> \<Rightarrow> False)"
   8.320 -
   8.321 -lemma inat_ord_simps [simp]:
   8.322 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   8.323 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   8.324 -  "q \<le> \<infinity>"
   8.325 -  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
   8.326 -  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
   8.327 -  "\<infinity> < q \<longleftrightarrow> False"
   8.328 -  by (simp_all add: less_eq_inat_def less_inat_def split: inat.splits)
   8.329 -
   8.330 -lemma inat_ord_code [code]:
   8.331 -  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
   8.332 -  "Fin m < Fin n \<longleftrightarrow> m < n"
   8.333 -  "q \<le> \<infinity> \<longleftrightarrow> True"
   8.334 -  "Fin m < \<infinity> \<longleftrightarrow> True"
   8.335 -  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
   8.336 -  "\<infinity> < q \<longleftrightarrow> False"
   8.337 -  by simp_all
   8.338 -
   8.339 -instance by default
   8.340 -  (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
   8.341 -
   8.342 -end
   8.343 -
   8.344 -instance inat :: ordered_comm_semiring
   8.345 -proof
   8.346 -  fix a b c :: inat
   8.347 -  assume "a \<le> b" and "0 \<le> c"
   8.348 -  thus "c * a \<le> c * b"
   8.349 -    unfolding times_inat_def less_eq_inat_def zero_inat_def
   8.350 -    by (simp split: inat.splits)
   8.351 -qed
   8.352 -
   8.353 -lemma inat_ord_number [simp]:
   8.354 -  "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
   8.355 -  "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
   8.356 -  by (simp_all add: number_of_inat_def)
   8.357 -
   8.358 -lemma i0_lb [simp]: "(0\<Colon>inat) \<le> n"
   8.359 -  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
   8.360 -
   8.361 -lemma ile0_eq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0"
   8.362 -by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
   8.363 -
   8.364 -lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
   8.365 -  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
   8.366 -
   8.367 -lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
   8.368 -  by simp
   8.369 -
   8.370 -lemma not_iless0 [simp]: "\<not> n < (0\<Colon>inat)"
   8.371 -  by (simp add: zero_inat_def less_inat_def split: inat.splits)
   8.372 -
   8.373 -lemma i0_less [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0"
   8.374 -by (simp add: zero_inat_def less_inat_def split: inat.splits)
   8.375 -
   8.376 -lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
   8.377 -  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
   8.378 - 
   8.379 -lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
   8.380 -  by (simp add: iSuc_def less_inat_def split: inat.splits)
   8.381 -
   8.382 -lemma ile_iSuc [simp]: "n \<le> iSuc n"
   8.383 -  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
   8.384 -
   8.385 -lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   8.386 -  by (simp add: zero_inat_def iSuc_def less_eq_inat_def split: inat.splits)
   8.387 -
   8.388 -lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   8.389 -  by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits)
   8.390 -
   8.391 -lemma iless_iSuc0[simp]: "(n < iSuc 0) = (n = 0)"
   8.392 -by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.split)
   8.393 -
   8.394 -lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
   8.395 -  by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits)
   8.396 -
   8.397 -lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
   8.398 -  by (cases n) auto
   8.399 -
   8.400 -lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
   8.401 -  by (auto simp add: iSuc_def less_inat_def split: inat.splits)
   8.402 -
   8.403 -lemma imult_Infty: "(0::inat) < n \<Longrightarrow> \<infinity> * n = \<infinity>"
   8.404 -by (simp add: zero_inat_def less_inat_def split: inat.splits)
   8.405 -
   8.406 -lemma imult_Infty_right: "(0::inat) < n \<Longrightarrow> n * \<infinity> = \<infinity>"
   8.407 -by (simp add: zero_inat_def less_inat_def split: inat.splits)
   8.408 -
   8.409 -lemma inat_0_less_mult_iff: "(0 < (m::inat) * n) = (0 < m \<and> 0 < n)"
   8.410 -by (simp only: i0_less imult_is_0, simp)
   8.411 -
   8.412 -lemma mono_iSuc: "mono iSuc"
   8.413 -by(simp add: mono_def)
   8.414 -
   8.415 -
   8.416 -lemma min_inat_simps [simp]:
   8.417 -  "min (Fin m) (Fin n) = Fin (min m n)"
   8.418 -  "min q 0 = 0"
   8.419 -  "min 0 q = 0"
   8.420 -  "min q \<infinity> = q"
   8.421 -  "min \<infinity> q = q"
   8.422 -  by (auto simp add: min_def)
   8.423 -
   8.424 -lemma max_inat_simps [simp]:
   8.425 -  "max (Fin m) (Fin n) = Fin (max m n)"
   8.426 -  "max q 0 = q"
   8.427 -  "max 0 q = q"
   8.428 -  "max q \<infinity> = \<infinity>"
   8.429 -  "max \<infinity> q = \<infinity>"
   8.430 -  by (simp_all add: max_def)
   8.431 -
   8.432 -lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   8.433 -  by (cases n) simp_all
   8.434 -
   8.435 -lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
   8.436 -  by (cases n) simp_all
   8.437 -
   8.438 -lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   8.439 -apply (induct_tac k)
   8.440 - apply (simp (no_asm) only: Fin_0)
   8.441 - apply (fast intro: le_less_trans [OF i0_lb])
   8.442 -apply (erule exE)
   8.443 -apply (drule spec)
   8.444 -apply (erule exE)
   8.445 -apply (drule ileI1)
   8.446 -apply (rule iSuc_Fin [THEN subst])
   8.447 -apply (rule exI)
   8.448 -apply (erule (1) le_less_trans)
   8.449 -done
   8.450 -
   8.451 -instantiation inat :: "{bot, top}"
   8.452 -begin
   8.453 -
   8.454 -definition bot_inat :: inat where
   8.455 -  "bot_inat = 0"
   8.456 -
   8.457 -definition top_inat :: inat where
   8.458 -  "top_inat = \<infinity>"
   8.459 -
   8.460 -instance proof
   8.461 -qed (simp_all add: bot_inat_def top_inat_def)
   8.462 -
   8.463 -end
   8.464 -
   8.465 -lemma finite_Fin_bounded:
   8.466 -  assumes le_fin: "\<And>y. y \<in> A \<Longrightarrow> y \<le> Fin n"
   8.467 -  shows "finite A"
   8.468 -proof (rule finite_subset)
   8.469 -  show "finite (Fin ` {..n})" by blast
   8.470 -
   8.471 -  have "A \<subseteq> {..Fin n}" using le_fin by fastsimp
   8.472 -  also have "\<dots> \<subseteq> Fin ` {..n}"
   8.473 -    by (rule subsetI) (case_tac x, auto)
   8.474 -  finally show "A \<subseteq> Fin ` {..n}" .
   8.475 -qed
   8.476 -
   8.477 -
   8.478 -subsection {* Well-ordering *}
   8.479 -
   8.480 -lemma less_FinE:
   8.481 -  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
   8.482 -by (induct n) auto
   8.483 -
   8.484 -lemma less_InftyE:
   8.485 -  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
   8.486 -by (induct n) auto
   8.487 -
   8.488 -lemma inat_less_induct:
   8.489 -  assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n"
   8.490 -proof -
   8.491 -  have P_Fin: "!!k. P (Fin k)"
   8.492 -    apply (rule nat_less_induct)
   8.493 -    apply (rule prem, clarify)
   8.494 -    apply (erule less_FinE, simp)
   8.495 -    done
   8.496 -  show ?thesis
   8.497 -  proof (induct n)
   8.498 -    fix nat
   8.499 -    show "P (Fin nat)" by (rule P_Fin)
   8.500 -  next
   8.501 -    show "P Infty"
   8.502 -      apply (rule prem, clarify)
   8.503 -      apply (erule less_InftyE)
   8.504 -      apply (simp add: P_Fin)
   8.505 -      done
   8.506 -  qed
   8.507 -qed
   8.508 -
   8.509 -instance inat :: wellorder
   8.510 -proof
   8.511 -  fix P and n
   8.512 -  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
   8.513 -  show "P n" by (blast intro: inat_less_induct hyp)
   8.514 -qed
   8.515 -
   8.516 -subsection {* Complete Lattice *}
   8.517 -
   8.518 -instantiation inat :: complete_lattice
   8.519 -begin
   8.520 -
   8.521 -definition inf_inat :: "inat \<Rightarrow> inat \<Rightarrow> inat" where
   8.522 -  "inf_inat \<equiv> min"
   8.523 -
   8.524 -definition sup_inat :: "inat \<Rightarrow> inat \<Rightarrow> inat" where
   8.525 -  "sup_inat \<equiv> max"
   8.526 -
   8.527 -definition Inf_inat :: "inat set \<Rightarrow> inat" where
   8.528 -  "Inf_inat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
   8.529 -
   8.530 -definition Sup_inat :: "inat set \<Rightarrow> inat" where
   8.531 -  "Sup_inat A \<equiv> if A = {} then 0
   8.532 -    else if finite A then Max A
   8.533 -                     else \<infinity>"
   8.534 -instance proof
   8.535 -  fix x :: "inat" and A :: "inat set"
   8.536 -  { assume "x \<in> A" then show "Inf A \<le> x"
   8.537 -      unfolding Inf_inat_def by (auto intro: Least_le) }
   8.538 -  { assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" then show "x \<le> Inf A"
   8.539 -      unfolding Inf_inat_def
   8.540 -      by (cases "A = {}") (auto intro: LeastI2_ex) }
   8.541 -  { assume "x \<in> A" then show "x \<le> Sup A"
   8.542 -      unfolding Sup_inat_def by (cases "finite A") auto }
   8.543 -  { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
   8.544 -      unfolding Sup_inat_def using finite_Fin_bounded by auto }
   8.545 -qed (simp_all add: inf_inat_def sup_inat_def)
   8.546 -end
   8.547 -
   8.548 -
   8.549 -subsection {* Traditional theorem names *}
   8.550 -
   8.551 -lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def
   8.552 -  plus_inat_def less_eq_inat_def less_inat_def
   8.553 -
   8.554 -end