src/HOL/Library/Nat_Infinity.thy
author huffman
Mon Feb 18 02:10:55 2008 +0100 (2008-02-18)
changeset 26089 373221497340
parent 25691 8f8d83af100a
child 27110 194aa674c2a1
permissions -rw-r--r--
proved linorder and wellorder class instances
wenzelm@11355
     1
(*  Title:      HOL/Library/Nat_Infinity.thy
wenzelm@11355
     2
    ID:         $Id$
wenzelm@11355
     3
    Author:     David von Oheimb, TU Muenchen
oheimb@11351
     4
*)
oheimb@11351
     5
wenzelm@14706
     6
header {* Natural numbers with infinity *}
oheimb@11351
     7
nipkow@15131
     8
theory Nat_Infinity
haftmann@25691
     9
imports ATP_Linkup
nipkow@15131
    10
begin
oheimb@11351
    11
oheimb@11351
    12
subsection "Definitions"
oheimb@11351
    13
oheimb@11351
    14
text {*
wenzelm@11355
    15
  We extend the standard natural numbers by a special value indicating
wenzelm@11355
    16
  infinity.  This includes extending the ordering relations @{term "op
wenzelm@11355
    17
  <"} and @{term "op \<le>"}.
oheimb@11351
    18
*}
oheimb@11351
    19
oheimb@11351
    20
datatype inat = Fin nat | Infty
oheimb@11351
    21
wenzelm@21210
    22
notation (xsymbols)
wenzelm@19736
    23
  Infty  ("\<infinity>")
wenzelm@19736
    24
wenzelm@21210
    25
notation (HTML output)
wenzelm@19736
    26
  Infty  ("\<infinity>")
wenzelm@19736
    27
wenzelm@19736
    28
definition
wenzelm@21404
    29
  iSuc :: "inat => inat" where
wenzelm@19736
    30
  "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
oheimb@11351
    31
haftmann@25594
    32
instantiation inat :: "{ord, zero}"
haftmann@25594
    33
begin
haftmann@25594
    34
haftmann@25594
    35
definition
wenzelm@11701
    36
  Zero_inat_def: "0 == Fin 0"
haftmann@25594
    37
haftmann@25594
    38
definition
wenzelm@11355
    39
  iless_def: "m < n ==
wenzelm@11355
    40
    case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
wenzelm@11355
    41
    | \<infinity>  => False"
haftmann@25594
    42
haftmann@25594
    43
definition
huffman@26089
    44
  ile_def: "m \<le> n ==
huffman@26089
    45
    case n of Fin n1 => (case m of Fin m1 => m1 \<le> n1 | \<infinity> => False)
huffman@26089
    46
    | \<infinity>  => True"
oheimb@11351
    47
haftmann@25594
    48
instance ..
haftmann@25594
    49
haftmann@25594
    50
end
haftmann@25594
    51
wenzelm@11701
    52
lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def
oheimb@11351
    53
lemmas inat_splits = inat.split inat.split_asm
oheimb@11351
    54
wenzelm@11355
    55
text {*
wenzelm@11357
    56
  Below is a not quite complete set of theorems.  Use the method
wenzelm@11357
    57
  @{text "(simp add: inat_defs split:inat_splits, arith?)"} to prove
wenzelm@11357
    58
  new theorems or solve arithmetic subgoals involving @{typ inat} on
wenzelm@11357
    59
  the fly.
oheimb@11351
    60
*}
oheimb@11351
    61
oheimb@11351
    62
subsection "Constructors"
oheimb@11351
    63
oheimb@11351
    64
lemma Fin_0: "Fin 0 = 0"
nipkow@25134
    65
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    66
oheimb@11351
    67
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
nipkow@25134
    68
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    69
oheimb@11351
    70
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
nipkow@25134
    71
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    72
oheimb@11351
    73
lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)"
nipkow@25134
    74
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    75
oheimb@11351
    76
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
nipkow@25134
    77
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    78
oheimb@11351
    79
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
nipkow@25134
    80
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    81
oheimb@11351
    82
lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)"
nipkow@25134
    83
by (simp add: inat_defs split:inat_splits)
oheimb@11351
    84
oheimb@11351
    85
oheimb@11351
    86
subsection "Ordering relations"
oheimb@11351
    87
huffman@26089
    88
instance inat :: linorder
huffman@26089
    89
proof
huffman@26089
    90
  fix x :: inat
huffman@26089
    91
  show "x \<le> x"
huffman@26089
    92
    by (simp add: inat_defs split: inat_splits)
huffman@26089
    93
next
huffman@26089
    94
  fix x y :: inat
huffman@26089
    95
  assume "x \<le> y" and "y \<le> x" thus "x = y"
huffman@26089
    96
    by (simp add: inat_defs split: inat_splits)
huffman@26089
    97
next
huffman@26089
    98
  fix x y z :: inat
huffman@26089
    99
  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
huffman@26089
   100
    by (simp add: inat_defs split: inat_splits)
huffman@26089
   101
next
huffman@26089
   102
  fix x y :: inat
huffman@26089
   103
  show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
huffman@26089
   104
    by (simp add: inat_defs order_less_le split: inat_splits)
huffman@26089
   105
next
huffman@26089
   106
  fix x y :: inat
huffman@26089
   107
  show "x \<le> y \<or> y \<le> x"
huffman@26089
   108
    by (simp add: inat_defs linorder_linear split: inat_splits)
huffman@26089
   109
qed
huffman@26089
   110
oheimb@11351
   111
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R"
nipkow@25134
   112
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   113
wenzelm@11355
   114
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)"
huffman@26089
   115
by (rule linorder_less_linear)
oheimb@11351
   116
huffman@26089
   117
lemma iless_not_refl: "\<not> n < (n::inat)"
huffman@26089
   118
by (rule order_less_irrefl)
oheimb@11351
   119
oheimb@11351
   120
lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)"
huffman@26089
   121
by (rule order_less_trans)
oheimb@11351
   122
oheimb@11351
   123
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)"
huffman@26089
   124
by (rule order_less_not_sym)
oheimb@11351
   125
oheimb@11351
   126
lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)"
nipkow@25134
   127
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   128
oheimb@11351
   129
lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>"
nipkow@25134
   130
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   131
wenzelm@11655
   132
lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)"
nipkow@25134
   133
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   134
oheimb@11351
   135
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)"
nipkow@25134
   136
by (fastsimp simp: inat_defs split:inat_splits)
oheimb@11351
   137
oheimb@11351
   138
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
nipkow@25134
   139
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   140
oheimb@11351
   141
lemma not_ilessi0 [simp]: "\<not> n < (0::inat)"
nipkow@25134
   142
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   143
oheimb@11351
   144
lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k"
nipkow@25134
   145
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   146
wenzelm@11655
   147
lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)"
nipkow@25134
   148
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   149
oheimb@11351
   150
oheimb@11351
   151
wenzelm@11655
   152
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))"
huffman@26089
   153
by (rule order_le_less)
oheimb@11351
   154
wenzelm@11355
   155
lemma ile_refl [simp]: "n \<le> (n::inat)"
huffman@26089
   156
by (rule order_refl)
oheimb@11351
   157
wenzelm@11355
   158
lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)"
huffman@26089
   159
by (rule order_trans)
oheimb@11351
   160
wenzelm@11355
   161
lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)"
huffman@26089
   162
by (rule order_le_less_trans)
oheimb@11351
   163
wenzelm@11355
   164
lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)"
huffman@26089
   165
by (rule order_less_le_trans)
oheimb@11351
   166
wenzelm@11355
   167
lemma Infty_ub [simp]: "n \<le> \<infinity>"
nipkow@25134
   168
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   169
wenzelm@11355
   170
lemma i0_lb [simp]: "(0::inat) \<le> n"
nipkow@25134
   171
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   172
wenzelm@11355
   173
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R"
nipkow@25134
   174
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   175
wenzelm@11355
   176
lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)"
huffman@26089
   177
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   178
wenzelm@11355
   179
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)"
huffman@26089
   180
by (rule order_le_neq_trans)
oheimb@11351
   181
wenzelm@11355
   182
lemma ileI1: "m < n ==> iSuc m \<le> n"
nipkow@25134
   183
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   184
wenzelm@11655
   185
lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)"
nipkow@25134
   186
by (simp add: inat_defs split:inat_splits, arith)
oheimb@11351
   187
wenzelm@11655
   188
lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)"
nipkow@25134
   189
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   190
wenzelm@11655
   191
lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)"
nipkow@25134
   192
by (simp add: inat_defs split:inat_splits, arith)
oheimb@11351
   193
wenzelm@11355
   194
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
nipkow@25134
   195
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   196
wenzelm@11355
   197
lemma ile_iSuc [simp]: "n \<le> iSuc n"
nipkow@25134
   198
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   199
wenzelm@11355
   200
lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k"
nipkow@25134
   201
by (simp add: inat_defs split:inat_splits)
oheimb@11351
   202
oheimb@11351
   203
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
nipkow@25134
   204
apply (induct_tac k)
nipkow@25134
   205
 apply (simp (no_asm) only: Fin_0)
huffman@26089
   206
 apply (fast intro: ile_iless_trans [OF i0_lb])
nipkow@25134
   207
apply (erule exE)
nipkow@25134
   208
apply (drule spec)
nipkow@25134
   209
apply (erule exE)
nipkow@25134
   210
apply (drule ileI1)
nipkow@25134
   211
apply (rule iSuc_Fin [THEN subst])
nipkow@25134
   212
apply (rule exI)
nipkow@25134
   213
apply (erule (1) ile_iless_trans)
nipkow@25134
   214
done
oheimb@11351
   215
huffman@26089
   216
huffman@26089
   217
subsection "Well-ordering"
huffman@26089
   218
huffman@26089
   219
lemma less_FinE:
huffman@26089
   220
  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
huffman@26089
   221
by (induct n) auto
huffman@26089
   222
huffman@26089
   223
lemma less_InftyE:
huffman@26089
   224
  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
huffman@26089
   225
by (induct n) auto
huffman@26089
   226
huffman@26089
   227
lemma inat_less_induct:
huffman@26089
   228
  assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n"
huffman@26089
   229
proof -
huffman@26089
   230
  have P_Fin: "!!k. P (Fin k)"
huffman@26089
   231
    apply (rule nat_less_induct)
huffman@26089
   232
    apply (rule prem, clarify)
huffman@26089
   233
    apply (erule less_FinE, simp)
huffman@26089
   234
    done
huffman@26089
   235
  show ?thesis
huffman@26089
   236
  proof (induct n)
huffman@26089
   237
    fix nat
huffman@26089
   238
    show "P (Fin nat)" by (rule P_Fin)
huffman@26089
   239
  next
huffman@26089
   240
    show "P Infty"
huffman@26089
   241
      apply (rule prem, clarify)
huffman@26089
   242
      apply (erule less_InftyE)
huffman@26089
   243
      apply (simp add: P_Fin)
huffman@26089
   244
      done
huffman@26089
   245
  qed
huffman@26089
   246
qed
huffman@26089
   247
huffman@26089
   248
instance inat :: wellorder
huffman@26089
   249
proof
huffman@26089
   250
  show "wf {(x::inat, y::inat). x < y}"
huffman@26089
   251
  proof (rule wfUNIVI)
huffman@26089
   252
    fix P and x :: inat
huffman@26089
   253
    assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x"
huffman@26089
   254
    hence 1: "!!x::inat. ALL y. y < x --> P y ==> P x" by fast
huffman@26089
   255
    thus "P x" by (rule inat_less_induct)
huffman@26089
   256
  qed
huffman@26089
   257
qed
huffman@26089
   258
oheimb@11351
   259
end