src/HOL/Library/Nat_Infinity.thy
author haftmann
Sat Jan 03 08:36:46 2009 +0100 (2009-01-03)
changeset 29337 450805a4a91f
parent 29023 ef3adebc6d98
child 29652 f4c6e546b7fe
child 29667 53103fc8ffa3
permissions -rw-r--r--
added instance for bot, top
wenzelm@11355
     1
(*  Title:      HOL/Library/Nat_Infinity.thy
haftmann@27110
     2
    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
oheimb@11351
     3
*)
oheimb@11351
     4
wenzelm@14706
     5
header {* Natural numbers with infinity *}
oheimb@11351
     6
nipkow@15131
     7
theory Nat_Infinity
haftmann@27487
     8
imports Plain "~~/src/HOL/Presburger"
nipkow@15131
     9
begin
oheimb@11351
    10
haftmann@29337
    11
text {* FIXME: move to Nat.thy *}
haftmann@29337
    12
haftmann@29337
    13
instantiation nat :: bot
haftmann@29337
    14
begin
haftmann@29337
    15
haftmann@29337
    16
definition bot_nat :: nat where
haftmann@29337
    17
  "bot_nat = 0"
haftmann@29337
    18
haftmann@29337
    19
instance proof
haftmann@29337
    20
qed (simp add: bot_nat_def)
haftmann@29337
    21
haftmann@27110
    22
subsection {* Type definition *}
oheimb@11351
    23
oheimb@11351
    24
text {*
wenzelm@11355
    25
  We extend the standard natural numbers by a special value indicating
haftmann@27110
    26
  infinity.
oheimb@11351
    27
*}
oheimb@11351
    28
haftmann@29337
    29
end
haftmann@29337
    30
oheimb@11351
    31
datatype inat = Fin nat | Infty
oheimb@11351
    32
wenzelm@21210
    33
notation (xsymbols)
wenzelm@19736
    34
  Infty  ("\<infinity>")
wenzelm@19736
    35
wenzelm@21210
    36
notation (HTML output)
wenzelm@19736
    37
  Infty  ("\<infinity>")
wenzelm@19736
    38
oheimb@11351
    39
haftmann@27110
    40
subsection {* Constructors and numbers *}
haftmann@27110
    41
haftmann@27110
    42
instantiation inat :: "{zero, one, number}"
haftmann@25594
    43
begin
haftmann@25594
    44
haftmann@25594
    45
definition
haftmann@27110
    46
  "0 = Fin 0"
haftmann@25594
    47
haftmann@25594
    48
definition
haftmann@27110
    49
  [code inline]: "1 = Fin 1"
haftmann@25594
    50
haftmann@25594
    51
definition
haftmann@28562
    52
  [code inline, code del]: "number_of k = Fin (number_of k)"
oheimb@11351
    53
haftmann@25594
    54
instance ..
haftmann@25594
    55
haftmann@25594
    56
end
haftmann@25594
    57
haftmann@27110
    58
definition iSuc :: "inat \<Rightarrow> inat" where
haftmann@27110
    59
  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
oheimb@11351
    60
oheimb@11351
    61
lemma Fin_0: "Fin 0 = 0"
haftmann@27110
    62
  by (simp add: zero_inat_def)
haftmann@27110
    63
haftmann@27110
    64
lemma Fin_1: "Fin 1 = 1"
haftmann@27110
    65
  by (simp add: one_inat_def)
haftmann@27110
    66
haftmann@27110
    67
lemma Fin_number: "Fin (number_of k) = number_of k"
haftmann@27110
    68
  by (simp add: number_of_inat_def)
haftmann@27110
    69
haftmann@27110
    70
lemma one_iSuc: "1 = iSuc 0"
haftmann@27110
    71
  by (simp add: zero_inat_def one_inat_def iSuc_def)
oheimb@11351
    72
oheimb@11351
    73
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
haftmann@27110
    74
  by (simp add: zero_inat_def)
oheimb@11351
    75
oheimb@11351
    76
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
haftmann@27110
    77
  by (simp add: zero_inat_def)
haftmann@27110
    78
haftmann@27110
    79
lemma zero_inat_eq [simp]:
haftmann@27110
    80
  "number_of k = (0\<Colon>inat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
haftmann@27110
    81
  "(0\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
haftmann@27110
    82
  unfolding zero_inat_def number_of_inat_def by simp_all
haftmann@27110
    83
haftmann@27110
    84
lemma one_inat_eq [simp]:
haftmann@27110
    85
  "number_of k = (1\<Colon>inat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
haftmann@27110
    86
  "(1\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
haftmann@27110
    87
  unfolding one_inat_def number_of_inat_def by simp_all
haftmann@27110
    88
haftmann@27110
    89
lemma zero_one_inat_neq [simp]:
haftmann@27110
    90
  "\<not> 0 = (1\<Colon>inat)"
haftmann@27110
    91
  "\<not> 1 = (0\<Colon>inat)"
haftmann@27110
    92
  unfolding zero_inat_def one_inat_def by simp_all
oheimb@11351
    93
haftmann@27110
    94
lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
haftmann@27110
    95
  by (simp add: one_inat_def)
haftmann@27110
    96
haftmann@27110
    97
lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
haftmann@27110
    98
  by (simp add: one_inat_def)
haftmann@27110
    99
haftmann@27110
   100
lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
haftmann@27110
   101
  by (simp add: number_of_inat_def)
haftmann@27110
   102
haftmann@27110
   103
lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
haftmann@27110
   104
  by (simp add: number_of_inat_def)
haftmann@27110
   105
haftmann@27110
   106
lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
haftmann@27110
   107
  by (simp add: iSuc_def)
haftmann@27110
   108
haftmann@27110
   109
lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
haftmann@27110
   110
  by (simp add: iSuc_Fin number_of_inat_def)
oheimb@11351
   111
oheimb@11351
   112
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
haftmann@27110
   113
  by (simp add: iSuc_def)
oheimb@11351
   114
oheimb@11351
   115
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
haftmann@27110
   116
  by (simp add: iSuc_def zero_inat_def split: inat.splits)
haftmann@27110
   117
haftmann@27110
   118
lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
haftmann@27110
   119
  by (rule iSuc_ne_0 [symmetric])
oheimb@11351
   120
haftmann@27110
   121
lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
haftmann@27110
   122
  by (simp add: iSuc_def split: inat.splits)
haftmann@27110
   123
haftmann@27110
   124
lemma number_of_inat_inject [simp]:
haftmann@27110
   125
  "(number_of k \<Colon> inat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
haftmann@27110
   126
  by (simp add: number_of_inat_def)
oheimb@11351
   127
oheimb@11351
   128
haftmann@27110
   129
subsection {* Addition *}
haftmann@27110
   130
haftmann@27110
   131
instantiation inat :: comm_monoid_add
haftmann@27110
   132
begin
haftmann@27110
   133
haftmann@27110
   134
definition
haftmann@27110
   135
  [code del]: "m + n = (case m of \<infinity> \<Rightarrow> \<infinity> | Fin m \<Rightarrow> (case n of \<infinity> \<Rightarrow> \<infinity> | Fin n \<Rightarrow> Fin (m + n)))"
oheimb@11351
   136
haftmann@27110
   137
lemma plus_inat_simps [simp, code]:
haftmann@27110
   138
  "Fin m + Fin n = Fin (m + n)"
haftmann@27110
   139
  "\<infinity> + q = \<infinity>"
haftmann@27110
   140
  "q + \<infinity> = \<infinity>"
haftmann@27110
   141
  by (simp_all add: plus_inat_def split: inat.splits)
haftmann@27110
   142
haftmann@27110
   143
instance proof
haftmann@27110
   144
  fix n m q :: inat
haftmann@27110
   145
  show "n + m + q = n + (m + q)"
haftmann@27110
   146
    by (cases n, auto, cases m, auto, cases q, auto)
haftmann@27110
   147
  show "n + m = m + n"
haftmann@27110
   148
    by (cases n, auto, cases m, auto)
haftmann@27110
   149
  show "0 + n = n"
haftmann@27110
   150
    by (cases n) (simp_all add: zero_inat_def)
huffman@26089
   151
qed
huffman@26089
   152
haftmann@27110
   153
end
oheimb@11351
   154
haftmann@27110
   155
lemma plus_inat_0 [simp]:
haftmann@27110
   156
  "0 + (q\<Colon>inat) = q"
haftmann@27110
   157
  "(q\<Colon>inat) + 0 = q"
haftmann@27110
   158
  by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
oheimb@11351
   159
haftmann@27110
   160
lemma plus_inat_number [simp]:
huffman@29012
   161
  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
huffman@29012
   162
    else if l < Int.Pls then number_of k else number_of (k + l))"
haftmann@27110
   163
  unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
oheimb@11351
   164
haftmann@27110
   165
lemma iSuc_number [simp]:
haftmann@27110
   166
  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
haftmann@27110
   167
  unfolding iSuc_number_of
haftmann@27110
   168
  unfolding one_inat_def number_of_inat_def Suc_nat_number_of if_distrib [symmetric] ..
oheimb@11351
   169
haftmann@27110
   170
lemma iSuc_plus_1:
haftmann@27110
   171
  "iSuc n = n + 1"
haftmann@27110
   172
  by (cases n) (simp_all add: iSuc_Fin one_inat_def)
haftmann@27110
   173
  
haftmann@27110
   174
lemma plus_1_iSuc:
haftmann@27110
   175
  "1 + q = iSuc q"
haftmann@27110
   176
  "q + 1 = iSuc q"
haftmann@27110
   177
  unfolding iSuc_plus_1 by (simp_all add: add_ac)
oheimb@11351
   178
oheimb@11351
   179
huffman@29014
   180
subsection {* Multiplication *}
huffman@29014
   181
huffman@29014
   182
instantiation inat :: comm_semiring_1
huffman@29014
   183
begin
huffman@29014
   184
huffman@29014
   185
definition
huffman@29014
   186
  times_inat_def [code del]:
huffman@29014
   187
  "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
huffman@29014
   188
    (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
huffman@29014
   189
huffman@29014
   190
lemma times_inat_simps [simp, code]:
huffman@29014
   191
  "Fin m * Fin n = Fin (m * n)"
huffman@29014
   192
  "\<infinity> * \<infinity> = \<infinity>"
huffman@29014
   193
  "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
huffman@29014
   194
  "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
huffman@29014
   195
  unfolding times_inat_def zero_inat_def
huffman@29014
   196
  by (simp_all split: inat.split)
huffman@29014
   197
huffman@29014
   198
instance proof
huffman@29014
   199
  fix a b c :: inat
huffman@29014
   200
  show "(a * b) * c = a * (b * c)"
huffman@29014
   201
    unfolding times_inat_def zero_inat_def
huffman@29014
   202
    by (simp split: inat.split)
huffman@29014
   203
  show "a * b = b * a"
huffman@29014
   204
    unfolding times_inat_def zero_inat_def
huffman@29014
   205
    by (simp split: inat.split)
huffman@29014
   206
  show "1 * a = a"
huffman@29014
   207
    unfolding times_inat_def zero_inat_def one_inat_def
huffman@29014
   208
    by (simp split: inat.split)
huffman@29014
   209
  show "(a + b) * c = a * c + b * c"
huffman@29014
   210
    unfolding times_inat_def zero_inat_def
huffman@29014
   211
    by (simp split: inat.split add: left_distrib)
huffman@29014
   212
  show "0 * a = 0"
huffman@29014
   213
    unfolding times_inat_def zero_inat_def
huffman@29014
   214
    by (simp split: inat.split)
huffman@29014
   215
  show "a * 0 = 0"
huffman@29014
   216
    unfolding times_inat_def zero_inat_def
huffman@29014
   217
    by (simp split: inat.split)
huffman@29014
   218
  show "(0::inat) \<noteq> 1"
huffman@29014
   219
    unfolding zero_inat_def one_inat_def
huffman@29014
   220
    by simp
huffman@29014
   221
qed
huffman@29014
   222
huffman@29014
   223
end
huffman@29014
   224
huffman@29014
   225
lemma mult_iSuc: "iSuc m * n = n + m * n"
huffman@29014
   226
  unfolding iSuc_plus_1 by (simp add: ring_simps)
huffman@29014
   227
huffman@29014
   228
lemma mult_iSuc_right: "m * iSuc n = m + m * n"
huffman@29014
   229
  unfolding iSuc_plus_1 by (simp add: ring_simps)
huffman@29014
   230
huffman@29023
   231
lemma of_nat_eq_Fin: "of_nat n = Fin n"
huffman@29023
   232
  apply (induct n)
huffman@29023
   233
  apply (simp add: Fin_0)
huffman@29023
   234
  apply (simp add: plus_1_iSuc iSuc_Fin)
huffman@29023
   235
  done
huffman@29023
   236
huffman@29023
   237
instance inat :: semiring_char_0
huffman@29023
   238
  by default (simp add: of_nat_eq_Fin)
huffman@29023
   239
huffman@29014
   240
haftmann@27110
   241
subsection {* Ordering *}
haftmann@27110
   242
haftmann@27110
   243
instantiation inat :: ordered_ab_semigroup_add
haftmann@27110
   244
begin
oheimb@11351
   245
haftmann@27110
   246
definition
haftmann@27110
   247
  [code del]: "m \<le> n = (case n of Fin n1 \<Rightarrow> (case m of Fin m1 \<Rightarrow> m1 \<le> n1 | \<infinity> \<Rightarrow> False)
haftmann@27110
   248
    | \<infinity> \<Rightarrow> True)"
oheimb@11351
   249
haftmann@27110
   250
definition
haftmann@27110
   251
  [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
haftmann@27110
   252
    | \<infinity> \<Rightarrow> False)"
oheimb@11351
   253
haftmann@27110
   254
lemma inat_ord_simps [simp]:
haftmann@27110
   255
  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
haftmann@27110
   256
  "Fin m < Fin n \<longleftrightarrow> m < n"
haftmann@27110
   257
  "q \<le> \<infinity>"
haftmann@27110
   258
  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
haftmann@27110
   259
  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
haftmann@27110
   260
  "\<infinity> < q \<longleftrightarrow> False"
haftmann@27110
   261
  by (simp_all add: less_eq_inat_def less_inat_def split: inat.splits)
oheimb@11351
   262
haftmann@27110
   263
lemma inat_ord_code [code]:
haftmann@27110
   264
  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
haftmann@27110
   265
  "Fin m < Fin n \<longleftrightarrow> m < n"
haftmann@27110
   266
  "q \<le> \<infinity> \<longleftrightarrow> True"
haftmann@27110
   267
  "Fin m < \<infinity> \<longleftrightarrow> True"
haftmann@27110
   268
  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
haftmann@27110
   269
  "\<infinity> < q \<longleftrightarrow> False"
haftmann@27110
   270
  by simp_all
oheimb@11351
   271
haftmann@27110
   272
instance by default
haftmann@27110
   273
  (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
oheimb@11351
   274
haftmann@27110
   275
end
haftmann@27110
   276
huffman@29014
   277
instance inat :: pordered_comm_semiring
huffman@29014
   278
proof
huffman@29014
   279
  fix a b c :: inat
huffman@29014
   280
  assume "a \<le> b" and "0 \<le> c"
huffman@29014
   281
  thus "c * a \<le> c * b"
huffman@29014
   282
    unfolding times_inat_def less_eq_inat_def zero_inat_def
huffman@29014
   283
    by (simp split: inat.splits)
huffman@29014
   284
qed
huffman@29014
   285
haftmann@27110
   286
lemma inat_ord_number [simp]:
haftmann@27110
   287
  "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
haftmann@27110
   288
  "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
haftmann@27110
   289
  by (simp_all add: number_of_inat_def)
oheimb@11351
   290
haftmann@27110
   291
lemma i0_lb [simp]: "(0\<Colon>inat) \<le> n"
haftmann@27110
   292
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
oheimb@11351
   293
haftmann@27110
   294
lemma i0_neq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0"
haftmann@27110
   295
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
haftmann@27110
   296
haftmann@27110
   297
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
haftmann@27110
   298
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
oheimb@11351
   299
haftmann@27110
   300
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
haftmann@27110
   301
  by simp
oheimb@11351
   302
haftmann@27110
   303
lemma not_ilessi0 [simp]: "\<not> n < (0\<Colon>inat)"
haftmann@27110
   304
  by (simp add: zero_inat_def less_inat_def split: inat.splits)
haftmann@27110
   305
haftmann@27110
   306
lemma i0_eq [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0"
haftmann@27110
   307
  by (simp add: zero_inat_def less_inat_def split: inat.splits)
oheimb@11351
   308
haftmann@27110
   309
lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
haftmann@27110
   310
  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
haftmann@27110
   311
 
haftmann@27110
   312
lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
haftmann@27110
   313
  by (simp add: iSuc_def less_inat_def split: inat.splits)
oheimb@11351
   314
haftmann@27110
   315
lemma ile_iSuc [simp]: "n \<le> iSuc n"
haftmann@27110
   316
  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
oheimb@11351
   317
wenzelm@11355
   318
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
haftmann@27110
   319
  by (simp add: zero_inat_def iSuc_def less_eq_inat_def split: inat.splits)
haftmann@27110
   320
haftmann@27110
   321
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
haftmann@27110
   322
  by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits)
haftmann@27110
   323
haftmann@27110
   324
lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
haftmann@27110
   325
  by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits)
haftmann@27110
   326
haftmann@27110
   327
lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
haftmann@27110
   328
  by (cases n) auto
haftmann@27110
   329
haftmann@27110
   330
lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
haftmann@27110
   331
  by (auto simp add: iSuc_def less_inat_def split: inat.splits)
oheimb@11351
   332
haftmann@27110
   333
lemma min_inat_simps [simp]:
haftmann@27110
   334
  "min (Fin m) (Fin n) = Fin (min m n)"
haftmann@27110
   335
  "min q 0 = 0"
haftmann@27110
   336
  "min 0 q = 0"
haftmann@27110
   337
  "min q \<infinity> = q"
haftmann@27110
   338
  "min \<infinity> q = q"
haftmann@27110
   339
  by (auto simp add: min_def)
oheimb@11351
   340
haftmann@27110
   341
lemma max_inat_simps [simp]:
haftmann@27110
   342
  "max (Fin m) (Fin n) = Fin (max m n)"
haftmann@27110
   343
  "max q 0 = q"
haftmann@27110
   344
  "max 0 q = q"
haftmann@27110
   345
  "max q \<infinity> = \<infinity>"
haftmann@27110
   346
  "max \<infinity> q = \<infinity>"
haftmann@27110
   347
  by (simp_all add: max_def)
haftmann@27110
   348
haftmann@27110
   349
lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
haftmann@27110
   350
  by (cases n) simp_all
haftmann@27110
   351
haftmann@27110
   352
lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
haftmann@27110
   353
  by (cases n) simp_all
oheimb@11351
   354
oheimb@11351
   355
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
nipkow@25134
   356
apply (induct_tac k)
nipkow@25134
   357
 apply (simp (no_asm) only: Fin_0)
haftmann@27110
   358
 apply (fast intro: le_less_trans [OF i0_lb])
nipkow@25134
   359
apply (erule exE)
nipkow@25134
   360
apply (drule spec)
nipkow@25134
   361
apply (erule exE)
nipkow@25134
   362
apply (drule ileI1)
nipkow@25134
   363
apply (rule iSuc_Fin [THEN subst])
nipkow@25134
   364
apply (rule exI)
haftmann@27110
   365
apply (erule (1) le_less_trans)
nipkow@25134
   366
done
oheimb@11351
   367
haftmann@29337
   368
instantiation inat :: "{bot, top}"
haftmann@29337
   369
begin
haftmann@29337
   370
haftmann@29337
   371
definition bot_inat :: inat where
haftmann@29337
   372
  "bot_inat = 0"
haftmann@29337
   373
haftmann@29337
   374
definition top_inat :: inat where
haftmann@29337
   375
  "top_inat = \<infinity>"
haftmann@29337
   376
haftmann@29337
   377
instance proof
haftmann@29337
   378
qed (simp_all add: bot_inat_def top_inat_def)
haftmann@29337
   379
haftmann@29337
   380
end
haftmann@29337
   381
huffman@26089
   382
haftmann@27110
   383
subsection {* Well-ordering *}
huffman@26089
   384
huffman@26089
   385
lemma less_FinE:
huffman@26089
   386
  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
huffman@26089
   387
by (induct n) auto
huffman@26089
   388
huffman@26089
   389
lemma less_InftyE:
huffman@26089
   390
  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
huffman@26089
   391
by (induct n) auto
huffman@26089
   392
huffman@26089
   393
lemma inat_less_induct:
huffman@26089
   394
  assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n"
huffman@26089
   395
proof -
huffman@26089
   396
  have P_Fin: "!!k. P (Fin k)"
huffman@26089
   397
    apply (rule nat_less_induct)
huffman@26089
   398
    apply (rule prem, clarify)
huffman@26089
   399
    apply (erule less_FinE, simp)
huffman@26089
   400
    done
huffman@26089
   401
  show ?thesis
huffman@26089
   402
  proof (induct n)
huffman@26089
   403
    fix nat
huffman@26089
   404
    show "P (Fin nat)" by (rule P_Fin)
huffman@26089
   405
  next
huffman@26089
   406
    show "P Infty"
huffman@26089
   407
      apply (rule prem, clarify)
huffman@26089
   408
      apply (erule less_InftyE)
huffman@26089
   409
      apply (simp add: P_Fin)
huffman@26089
   410
      done
huffman@26089
   411
  qed
huffman@26089
   412
qed
huffman@26089
   413
huffman@26089
   414
instance inat :: wellorder
huffman@26089
   415
proof
haftmann@27823
   416
  fix P and n
haftmann@27823
   417
  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
haftmann@27823
   418
  show "P n" by (blast intro: inat_less_induct hyp)
huffman@26089
   419
qed
huffman@26089
   420
haftmann@27110
   421
haftmann@27110
   422
subsection {* Traditional theorem names *}
haftmann@27110
   423
haftmann@27110
   424
lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def
haftmann@27110
   425
  plus_inat_def less_eq_inat_def less_inat_def
haftmann@27110
   426
haftmann@27110
   427
lemmas inat_splits = inat.splits
haftmann@27110
   428
oheimb@11351
   429
end