src/HOL/Library/Nat_Infinity.thy
changeset 11355 778c369559d9
parent 11351 c5c403d30c77
child 11357 908b761cdfb0
equal deleted inserted replaced
11354:9b80fe19407f 11355:778c369559d9
     1 (*  Title: 	HOL/Library/Nat_Infinity.thy
     1 (*  Title:      HOL/Library/Nat_Infinity.thy
     2     ID:         $ $
     2     ID:         $Id$
     3     Author: 	David von Oheimb, TU Muenchen
     3     Author:     David von Oheimb, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
       
     6 *)
     5 *)
     7 
     6 
     8 header {*
     7 header {*
     9   \title{Natural numbers with infinity}
     8   \title{Natural numbers with infinity}
    10   \author{David von Oheimb}
     9   \author{David von Oheimb}
    11 *}
    10 *}
    12 
    11 
    13 theory Nat_Infinity = Datatype:
    12 theory Nat_Infinity = Main:
    14 
    13 
    15 subsection "Definitions"
    14 subsection "Definitions"
    16 
    15 
    17 text {*
    16 text {*
    18  We extend the standard natural numbers by a special value indicating infinity.
    17   We extend the standard natural numbers by a special value indicating
    19  This includes extending the ordering relations @{term "op <"} and 
    18   infinity.  This includes extending the ordering relations @{term "op
    20  @{term "op <="}.
    19   <"} and @{term "op \<le>"}.
    21 *}
    20 *}
    22 
    21 
    23 datatype inat = Fin nat | Infty
    22 datatype inat = Fin nat | Infty
    24 
    23 
    25 instance inat :: ord ..
    24 instance inat :: ord ..
    26 instance inat :: zero ..
    25 instance inat :: zero ..
    27 
    26 
    28 consts
    27 consts
    29 
    28   iSuc :: "inat => inat"
    30   iSuc	:: "inat => inat"
       
    31 
    29 
    32 syntax (xsymbols)
    30 syntax (xsymbols)
    33 
    31   Infty :: inat    ("\<infinity>")
    34   Infty		:: inat					("\<infinity>")
       
    35 
    32 
    36 defs
    33 defs
    37 
    34   iZero_def: "0 == Fin 0"
    38   iZero_def:	"0      == Fin 0"
    35   iSuc_def: "iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    39   iSuc_def:	"iSuc i == case i of Fin n  => Fin (Suc n) | \<infinity> => \<infinity>"
    36   iless_def: "m < n ==
    40   iless_def:	"m < n  == case m of Fin m1 => (case n of Fin n1 => m1 < n1 
    37     case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
    41 						             | \<infinity> => True)
    38     | \<infinity>  => False"
    42 				   | \<infinity>  => False "
    39   ile_def: "(m::inat) \<le> n == \<not> (n < m)"
    43   ile_def:	"(m::inat) <= n == \<not>(n<m)"
       
    44 
    40 
    45 lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
    41 lemmas inat_defs = iZero_def iSuc_def iless_def ile_def
    46 lemmas inat_splits = inat.split inat.split_asm
    42 lemmas inat_splits = inat.split inat.split_asm
    47 
    43 
    48 
    44 text {*
    49 text {* Below is a not quite complete set of theorems. Use
    45   Below is a not quite complete set of theorems.  Use method @{text
    50 @{text "apply(simp add:inat_defs split:inat_splits, arith?)"}
    46   "(simp add: inat_defs split:inat_splits, arith?)"} to prove new
    51 to prove new theorems or solve arithmetic subgoals involving @{typ inat} 
    47   theorems or solve arithmetic subgoals involving @{typ inat} on the
    52 on the fly.
    48   fly.
    53 *}
    49 *}
    54 
    50 
    55 subsection "Constructors"
    51 subsection "Constructors"
    56 
    52 
    57 lemma Fin_0: "Fin 0 = 0"
    53 lemma Fin_0: "Fin 0 = 0"
    58 by(simp add:inat_defs split:inat_splits, arith?)
    54   by (simp add:inat_defs split:inat_splits, arith?)
    59 
    55 
    60 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    56 lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
    61 by(simp add:inat_defs split:inat_splits, arith?)
    57   by (simp add:inat_defs split:inat_splits, arith?)
    62 
    58 
    63 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    59 lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
    64 by(simp add:inat_defs split:inat_splits, arith?)
    60   by (simp add:inat_defs split:inat_splits, arith?)
    65 
    61 
    66 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    62 lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
    67 by(simp add:inat_defs split:inat_splits, arith?)
    63   by (simp add:inat_defs split:inat_splits, arith?)
    68 
    64 
    69 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    65 lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
    70 by(simp add:inat_defs split:inat_splits, arith?)
    66   by (simp add:inat_defs split:inat_splits, arith?)
    71 
    67 
    72 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    68 lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
    73 by(simp add:inat_defs split:inat_splits, arith?)
    69   by (simp add:inat_defs split:inat_splits, arith?)
    74 
    70 
    75 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
    71 lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
    76 by(simp add:inat_defs split:inat_splits, arith?)
    72   by (simp add:inat_defs split:inat_splits, arith?)
    77 
    73 
    78 
    74 
    79 subsection "Ordering relations"
    75 subsection "Ordering relations"
    80 
    76 
    81 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    77 lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
    82 by(simp add:inat_defs split:inat_splits, arith?)
    78   by (simp add:inat_defs split:inat_splits, arith?)
    83 
    79 
    84 lemma iless_linear: "m < n | m = n | n < (m::inat)"
    80 lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
    85 by(simp add:inat_defs split:inat_splits, arith?)
    81   by (simp add:inat_defs split:inat_splits, arith?)
    86 
    82 
    87 lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    83 lemma iless_not_refl [simp]: "\<not> n < (n::inat)"
    88 by(simp add:inat_defs split:inat_splits, arith?)
    84   by (simp add:inat_defs split:inat_splits, arith?)
    89 
    85 
    90 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    86 lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
    91 by(simp add:inat_defs split:inat_splits, arith?)
    87   by (simp add:inat_defs split:inat_splits, arith?)
    92 
    88 
    93 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    89 lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
    94 by(simp add:inat_defs split:inat_splits, arith?)
    90   by (simp add:inat_defs split:inat_splits, arith?)
    95 
    91 
    96 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
    92 lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
    97 by(simp add:inat_defs split:inat_splits, arith?)
    93   by (simp add:inat_defs split:inat_splits, arith?)
    98 
    94 
    99 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
    95 lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
   100 by(simp add:inat_defs split:inat_splits, arith?)
    96   by (simp add:inat_defs split:inat_splits, arith?)
   101 
    97 
   102 lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
    98 lemma Infty_eq [simp]: "n < \<infinity> = (n \<noteq> \<infinity>)"
   103 by(simp add:inat_defs split:inat_splits, arith?)
    99   by (simp add:inat_defs split:inat_splits, arith?)
   104 
   100 
   105 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   101 lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
   106 by(simp add:inat_defs split:inat_splits, arith?)
   102   by (simp add:inat_defs split:inat_splits, arith?)
   107 
   103 
   108 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   104 lemma i0_iless_iSuc [simp]: "0 < iSuc n"
   109 by(simp add:inat_defs split:inat_splits, arith?)
   105   by (simp add:inat_defs split:inat_splits, arith?)
   110 
   106 
   111 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
   107 lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
   112 by(simp add:inat_defs split:inat_splits, arith?)
   108   by (simp add:inat_defs split:inat_splits, arith?)
   113 
   109 
   114 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   110 lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
   115 by(simp add:inat_defs split:inat_splits, arith?)
   111   by (simp add:inat_defs split:inat_splits, arith?)
   116 
   112 
   117 lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
   113 lemma iSuc_mono [simp]: "iSuc n < iSuc m = (n < m)"
   118 by(simp add:inat_defs split:inat_splits, arith?)
   114   by (simp add:inat_defs split:inat_splits, arith?)
   119 
   115 
   120 
   116 
   121 (* ----------------------------------------------------------------------- *)
   117 (* ----------------------------------------------------------------------- *)
   122 
   118 
   123 lemma ile_def2: "m <= n = (m < n | m = (n::inat))"
   119 lemma ile_def2: "m \<le> n = (m < n \<or> m = (n::inat))"
   124 by(simp add:inat_defs split:inat_splits, arith?)
   120   by (simp add:inat_defs split:inat_splits, arith?)
   125 
   121 
   126 lemma ile_refl [simp]: "n <= (n::inat)"
   122 lemma ile_refl [simp]: "n \<le> (n::inat)"
   127 by(simp add:inat_defs split:inat_splits, arith?)
   123   by (simp add:inat_defs split:inat_splits, arith?)
   128 
   124 
   129 lemma ile_trans: "i <= j ==> j <= k ==> i <= (k::inat)"
   125 lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
   130 by(simp add:inat_defs split:inat_splits, arith?)
   126   by (simp add:inat_defs split:inat_splits, arith?)
   131 
   127 
   132 lemma ile_iless_trans: "i <= j ==> j < k ==> i < (k::inat)"
   128 lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
   133 by(simp add:inat_defs split:inat_splits, arith?)
   129   by (simp add:inat_defs split:inat_splits, arith?)
   134 
   130 
   135 lemma iless_ile_trans: "i < j ==> j <= k ==> i < (k::inat)"
   131 lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
   136 by(simp add:inat_defs split:inat_splits, arith?)
   132   by (simp add:inat_defs split:inat_splits, arith?)
   137 
   133 
   138 lemma Infty_ub [simp]: "n <= \<infinity>"
   134 lemma Infty_ub [simp]: "n \<le> \<infinity>"
   139 by(simp add:inat_defs split:inat_splits, arith?)
   135   by (simp add:inat_defs split:inat_splits, arith?)
   140 
   136 
   141 lemma i0_lb [simp]: "(0::inat) <= n"
   137 lemma i0_lb [simp]: "(0::inat) \<le> n"
   142 by(simp add:inat_defs split:inat_splits, arith?)
   138   by (simp add:inat_defs split:inat_splits, arith?)
   143 
   139 
   144 lemma Infty_ileE [elim!]: "\<infinity> <= Fin m ==> R"
   140 lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
   145 by(simp add:inat_defs split:inat_splits, arith?)
   141   by (simp add:inat_defs split:inat_splits, arith?)
   146 
   142 
   147 lemma Fin_ile_mono [simp]: "(Fin n <= Fin m) = (n <= m)"
   143 lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
   148 by(simp add:inat_defs split:inat_splits, arith?)
   144   by (simp add:inat_defs split:inat_splits, arith?)
   149 
   145 
   150 lemma ilessI1: "n <= m ==> n \<noteq> m ==> n < (m::inat)"
   146 lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
   151 by(simp add:inat_defs split:inat_splits, arith?)
   147   by (simp add:inat_defs split:inat_splits, arith?)
   152 
   148 
   153 lemma ileI1: "m < n ==> iSuc m <= n"
   149 lemma ileI1: "m < n ==> iSuc m \<le> n"
   154 by(simp add:inat_defs split:inat_splits, arith?)
   150   by (simp add:inat_defs split:inat_splits, arith?)
   155 
   151 
   156 lemma Suc_ile_eq: "Fin (Suc m) <= n = (Fin m < n)"
   152 lemma Suc_ile_eq: "Fin (Suc m) \<le> n = (Fin m < n)"
   157 by(simp add:inat_defs split:inat_splits, arith?)
   153   by (simp add:inat_defs split:inat_splits, arith?)
   158 
   154 
   159 lemma iSuc_ile_mono [simp]: "iSuc n <= iSuc m = (n <= m)"
   155 lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m = (n \<le> m)"
   160 by(simp add:inat_defs split:inat_splits, arith?)
   156   by (simp add:inat_defs split:inat_splits, arith?)
   161 
   157 
   162 lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m <= n)"
   158 lemma iless_Suc_eq [simp]: "Fin m < iSuc n = (Fin m \<le> n)"
   163 by(simp add:inat_defs split:inat_splits, arith?)
   159   by (simp add:inat_defs split:inat_splits, arith?)
   164 
   160 
   165 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n <= 0"
   161 lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
   166 by(simp add:inat_defs split:inat_splits, arith?)
   162   by (simp add:inat_defs split:inat_splits, arith?)
   167 
   163 
   168 lemma ile_iSuc [simp]: "n <= iSuc n"
   164 lemma ile_iSuc [simp]: "n \<le> iSuc n"
   169 by(simp add:inat_defs split:inat_splits, arith?)
   165   by (simp add:inat_defs split:inat_splits, arith?)
   170 
   166 
   171 lemma Fin_ile: "n <= Fin m ==> \<exists>k. n = Fin k"
   167 lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
   172 by(simp add:inat_defs split:inat_splits, arith?)
   168   by (simp add:inat_defs split:inat_splits, arith?)
   173 
   169 
   174 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   170 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
   175 apply (induct_tac "k")
   171   apply (induct_tac k)
   176 apply  (simp (no_asm) only: Fin_0)
   172    apply (simp (no_asm) only: Fin_0)
   177 apply  (fast intro: ile_iless_trans i0_lb)
   173    apply (fast intro: ile_iless_trans i0_lb)
   178 apply (erule exE)
   174   apply (erule exE)
   179 apply (drule spec)
   175   apply (drule spec)
   180 apply (erule exE)
   176   apply (erule exE)
   181 apply (drule ileI1)
   177   apply (drule ileI1)
   182 apply (rule iSuc_Fin [THEN subst])
   178   apply (rule iSuc_Fin [THEN subst])
   183 apply (rule exI)
   179   apply (rule exI)
   184 apply (erule (1) ile_iless_trans)
   180   apply (erule (1) ile_iless_trans)
   185 done
   181   done
   186 
       
   187 ML {*
       
   188 val Fin_0 = thm "Fin_0";
       
   189 val Suc_ile_eq = thm "Suc_ile_eq";
       
   190 val iSuc_Fin = thm "iSuc_Fin";
       
   191 val iSuc_Infty = thm "iSuc_Infty";
       
   192 val iSuc_mono = thm "iSuc_mono";
       
   193 val iSuc_ile_mono = thm "iSuc_ile_mono";
       
   194 val not_iSuc_ilei0=thm "not_iSuc_ilei0";
       
   195 val iSuc_inject = thm "iSuc_inject";
       
   196 val i0_iless_iSuc = thm "i0_iless_iSuc";
       
   197 val i0_eq = thm "i0_eq";
       
   198 val i0_lb = thm "i0_lb";
       
   199 val ile_def = thm "ile_def";
       
   200 val ile_refl = thm "ile_refl";
       
   201 val Infty_ub = thm "Infty_ub";
       
   202 val ilessI1 = thm "ilessI1";
       
   203 val ile_iless_trans = thm "ile_iless_trans";
       
   204 val ile_trans = thm "ile_trans";
       
   205 val ileI1 = thm "ileI1";
       
   206 val ile_iSuc = thm "ile_iSuc";
       
   207 val Fin_iless_Infty = thm "Fin_iless_Infty";
       
   208 val Fin_ile_mono = thm "Fin_ile_mono";
       
   209 val chain_incr = thm "chain_incr";
       
   210 val Infty_eq = thm "Infty_eq";
       
   211 *}
       
   212 
   182 
   213 end
   183 end
   214 
       
   215 
       
   216