src/HOL/Library/Nat_Infinity.thy
author huffman
Sat Dec 06 19:39:53 2008 -0800 (2008-12-06)
changeset 29012 9140227dc8c5
parent 28562 4e74209f113e
child 29014 e515f42d1db7
permissions -rw-r--r--
change lemmas to avoid using neg
wenzelm@11355
     1
(*  Title:      HOL/Library/Nat_Infinity.thy
wenzelm@11355
     2
    ID:         $Id$
haftmann@27110
     3
    Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, 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@27487
     9
imports Plain "~~/src/HOL/Presburger"
nipkow@15131
    10
begin
oheimb@11351
    11
haftmann@27110
    12
subsection {* Type definition *}
oheimb@11351
    13
oheimb@11351
    14
text {*
wenzelm@11355
    15
  We extend the standard natural numbers by a special value indicating
haftmann@27110
    16
  infinity.
oheimb@11351
    17
*}
oheimb@11351
    18
oheimb@11351
    19
datatype inat = Fin nat | Infty
oheimb@11351
    20
wenzelm@21210
    21
notation (xsymbols)
wenzelm@19736
    22
  Infty  ("\<infinity>")
wenzelm@19736
    23
wenzelm@21210
    24
notation (HTML output)
wenzelm@19736
    25
  Infty  ("\<infinity>")
wenzelm@19736
    26
oheimb@11351
    27
haftmann@27110
    28
subsection {* Constructors and numbers *}
haftmann@27110
    29
haftmann@27110
    30
instantiation inat :: "{zero, one, number}"
haftmann@25594
    31
begin
haftmann@25594
    32
haftmann@25594
    33
definition
haftmann@27110
    34
  "0 = Fin 0"
haftmann@25594
    35
haftmann@25594
    36
definition
haftmann@27110
    37
  [code inline]: "1 = Fin 1"
haftmann@25594
    38
haftmann@25594
    39
definition
haftmann@28562
    40
  [code inline, code del]: "number_of k = Fin (number_of k)"
oheimb@11351
    41
haftmann@25594
    42
instance ..
haftmann@25594
    43
haftmann@25594
    44
end
haftmann@25594
    45
haftmann@27110
    46
definition iSuc :: "inat \<Rightarrow> inat" where
haftmann@27110
    47
  "iSuc i = (case i of Fin n \<Rightarrow> Fin (Suc n) | \<infinity> \<Rightarrow> \<infinity>)"
oheimb@11351
    48
oheimb@11351
    49
lemma Fin_0: "Fin 0 = 0"
haftmann@27110
    50
  by (simp add: zero_inat_def)
haftmann@27110
    51
haftmann@27110
    52
lemma Fin_1: "Fin 1 = 1"
haftmann@27110
    53
  by (simp add: one_inat_def)
haftmann@27110
    54
haftmann@27110
    55
lemma Fin_number: "Fin (number_of k) = number_of k"
haftmann@27110
    56
  by (simp add: number_of_inat_def)
haftmann@27110
    57
haftmann@27110
    58
lemma one_iSuc: "1 = iSuc 0"
haftmann@27110
    59
  by (simp add: zero_inat_def one_inat_def iSuc_def)
oheimb@11351
    60
oheimb@11351
    61
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0"
haftmann@27110
    62
  by (simp add: zero_inat_def)
oheimb@11351
    63
oheimb@11351
    64
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>"
haftmann@27110
    65
  by (simp add: zero_inat_def)
haftmann@27110
    66
haftmann@27110
    67
lemma zero_inat_eq [simp]:
haftmann@27110
    68
  "number_of k = (0\<Colon>inat) \<longleftrightarrow> number_of k = (0\<Colon>nat)"
haftmann@27110
    69
  "(0\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (0\<Colon>nat)"
haftmann@27110
    70
  unfolding zero_inat_def number_of_inat_def by simp_all
haftmann@27110
    71
haftmann@27110
    72
lemma one_inat_eq [simp]:
haftmann@27110
    73
  "number_of k = (1\<Colon>inat) \<longleftrightarrow> number_of k = (1\<Colon>nat)"
haftmann@27110
    74
  "(1\<Colon>inat) = number_of k \<longleftrightarrow> number_of k = (1\<Colon>nat)"
haftmann@27110
    75
  unfolding one_inat_def number_of_inat_def by simp_all
haftmann@27110
    76
haftmann@27110
    77
lemma zero_one_inat_neq [simp]:
haftmann@27110
    78
  "\<not> 0 = (1\<Colon>inat)"
haftmann@27110
    79
  "\<not> 1 = (0\<Colon>inat)"
haftmann@27110
    80
  unfolding zero_inat_def one_inat_def by simp_all
oheimb@11351
    81
haftmann@27110
    82
lemma Infty_ne_i1 [simp]: "\<infinity> \<noteq> 1"
haftmann@27110
    83
  by (simp add: one_inat_def)
haftmann@27110
    84
haftmann@27110
    85
lemma i1_ne_Infty [simp]: "1 \<noteq> \<infinity>"
haftmann@27110
    86
  by (simp add: one_inat_def)
haftmann@27110
    87
haftmann@27110
    88
lemma Infty_ne_number [simp]: "\<infinity> \<noteq> number_of k"
haftmann@27110
    89
  by (simp add: number_of_inat_def)
haftmann@27110
    90
haftmann@27110
    91
lemma number_ne_Infty [simp]: "number_of k \<noteq> \<infinity>"
haftmann@27110
    92
  by (simp add: number_of_inat_def)
haftmann@27110
    93
haftmann@27110
    94
lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)"
haftmann@27110
    95
  by (simp add: iSuc_def)
haftmann@27110
    96
haftmann@27110
    97
lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))"
haftmann@27110
    98
  by (simp add: iSuc_Fin number_of_inat_def)
oheimb@11351
    99
oheimb@11351
   100
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>"
haftmann@27110
   101
  by (simp add: iSuc_def)
oheimb@11351
   102
oheimb@11351
   103
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0"
haftmann@27110
   104
  by (simp add: iSuc_def zero_inat_def split: inat.splits)
haftmann@27110
   105
haftmann@27110
   106
lemma zero_ne_iSuc [simp]: "0 \<noteq> iSuc n"
haftmann@27110
   107
  by (rule iSuc_ne_0 [symmetric])
oheimb@11351
   108
haftmann@27110
   109
lemma iSuc_inject [simp]: "iSuc m = iSuc n \<longleftrightarrow> m = n"
haftmann@27110
   110
  by (simp add: iSuc_def split: inat.splits)
haftmann@27110
   111
haftmann@27110
   112
lemma number_of_inat_inject [simp]:
haftmann@27110
   113
  "(number_of k \<Colon> inat) = number_of l \<longleftrightarrow> (number_of k \<Colon> nat) = number_of l"
haftmann@27110
   114
  by (simp add: number_of_inat_def)
oheimb@11351
   115
oheimb@11351
   116
haftmann@27110
   117
subsection {* Addition *}
haftmann@27110
   118
haftmann@27110
   119
instantiation inat :: comm_monoid_add
haftmann@27110
   120
begin
haftmann@27110
   121
haftmann@27110
   122
definition
haftmann@27110
   123
  [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
   124
haftmann@27110
   125
lemma plus_inat_simps [simp, code]:
haftmann@27110
   126
  "Fin m + Fin n = Fin (m + n)"
haftmann@27110
   127
  "\<infinity> + q = \<infinity>"
haftmann@27110
   128
  "q + \<infinity> = \<infinity>"
haftmann@27110
   129
  by (simp_all add: plus_inat_def split: inat.splits)
haftmann@27110
   130
haftmann@27110
   131
instance proof
haftmann@27110
   132
  fix n m q :: inat
haftmann@27110
   133
  show "n + m + q = n + (m + q)"
haftmann@27110
   134
    by (cases n, auto, cases m, auto, cases q, auto)
haftmann@27110
   135
  show "n + m = m + n"
haftmann@27110
   136
    by (cases n, auto, cases m, auto)
haftmann@27110
   137
  show "0 + n = n"
haftmann@27110
   138
    by (cases n) (simp_all add: zero_inat_def)
huffman@26089
   139
qed
huffman@26089
   140
haftmann@27110
   141
end
oheimb@11351
   142
haftmann@27110
   143
lemma plus_inat_0 [simp]:
haftmann@27110
   144
  "0 + (q\<Colon>inat) = q"
haftmann@27110
   145
  "(q\<Colon>inat) + 0 = q"
haftmann@27110
   146
  by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
oheimb@11351
   147
haftmann@27110
   148
lemma plus_inat_number [simp]:
huffman@29012
   149
  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
huffman@29012
   150
    else if l < Int.Pls then number_of k else number_of (k + l))"
haftmann@27110
   151
  unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
oheimb@11351
   152
haftmann@27110
   153
lemma iSuc_number [simp]:
haftmann@27110
   154
  "iSuc (number_of k) = (if neg (number_of k \<Colon> int) then 1 else number_of (Int.succ k))"
haftmann@27110
   155
  unfolding iSuc_number_of
haftmann@27110
   156
  unfolding one_inat_def number_of_inat_def Suc_nat_number_of if_distrib [symmetric] ..
oheimb@11351
   157
haftmann@27110
   158
lemma iSuc_plus_1:
haftmann@27110
   159
  "iSuc n = n + 1"
haftmann@27110
   160
  by (cases n) (simp_all add: iSuc_Fin one_inat_def)
haftmann@27110
   161
  
haftmann@27110
   162
lemma plus_1_iSuc:
haftmann@27110
   163
  "1 + q = iSuc q"
haftmann@27110
   164
  "q + 1 = iSuc q"
haftmann@27110
   165
  unfolding iSuc_plus_1 by (simp_all add: add_ac)
oheimb@11351
   166
oheimb@11351
   167
haftmann@27110
   168
subsection {* Ordering *}
haftmann@27110
   169
haftmann@27110
   170
instantiation inat :: ordered_ab_semigroup_add
haftmann@27110
   171
begin
oheimb@11351
   172
haftmann@27110
   173
definition
haftmann@27110
   174
  [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
   175
    | \<infinity> \<Rightarrow> True)"
oheimb@11351
   176
haftmann@27110
   177
definition
haftmann@27110
   178
  [code del]: "m < n = (case m of Fin m1 \<Rightarrow> (case n of Fin n1 \<Rightarrow> m1 < n1 | \<infinity> \<Rightarrow> True)
haftmann@27110
   179
    | \<infinity> \<Rightarrow> False)"
oheimb@11351
   180
haftmann@27110
   181
lemma inat_ord_simps [simp]:
haftmann@27110
   182
  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
haftmann@27110
   183
  "Fin m < Fin n \<longleftrightarrow> m < n"
haftmann@27110
   184
  "q \<le> \<infinity>"
haftmann@27110
   185
  "q < \<infinity> \<longleftrightarrow> q \<noteq> \<infinity>"
haftmann@27110
   186
  "\<infinity> \<le> q \<longleftrightarrow> q = \<infinity>"
haftmann@27110
   187
  "\<infinity> < q \<longleftrightarrow> False"
haftmann@27110
   188
  by (simp_all add: less_eq_inat_def less_inat_def split: inat.splits)
oheimb@11351
   189
haftmann@27110
   190
lemma inat_ord_code [code]:
haftmann@27110
   191
  "Fin m \<le> Fin n \<longleftrightarrow> m \<le> n"
haftmann@27110
   192
  "Fin m < Fin n \<longleftrightarrow> m < n"
haftmann@27110
   193
  "q \<le> \<infinity> \<longleftrightarrow> True"
haftmann@27110
   194
  "Fin m < \<infinity> \<longleftrightarrow> True"
haftmann@27110
   195
  "\<infinity> \<le> Fin n \<longleftrightarrow> False"
haftmann@27110
   196
  "\<infinity> < q \<longleftrightarrow> False"
haftmann@27110
   197
  by simp_all
oheimb@11351
   198
haftmann@27110
   199
instance by default
haftmann@27110
   200
  (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits)
oheimb@11351
   201
haftmann@27110
   202
end
haftmann@27110
   203
haftmann@27110
   204
lemma inat_ord_number [simp]:
haftmann@27110
   205
  "(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
haftmann@27110
   206
  "(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
haftmann@27110
   207
  by (simp_all add: number_of_inat_def)
oheimb@11351
   208
haftmann@27110
   209
lemma i0_lb [simp]: "(0\<Colon>inat) \<le> n"
haftmann@27110
   210
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
oheimb@11351
   211
haftmann@27110
   212
lemma i0_neq [simp]: "n \<le> (0\<Colon>inat) \<longleftrightarrow> n = 0"
haftmann@27110
   213
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
haftmann@27110
   214
haftmann@27110
   215
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m \<Longrightarrow> R"
haftmann@27110
   216
  by (simp add: zero_inat_def less_eq_inat_def split: inat.splits)
oheimb@11351
   217
haftmann@27110
   218
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m \<Longrightarrow> R"
haftmann@27110
   219
  by simp
oheimb@11351
   220
haftmann@27110
   221
lemma not_ilessi0 [simp]: "\<not> n < (0\<Colon>inat)"
haftmann@27110
   222
  by (simp add: zero_inat_def less_inat_def split: inat.splits)
haftmann@27110
   223
haftmann@27110
   224
lemma i0_eq [simp]: "(0\<Colon>inat) < n \<longleftrightarrow> n \<noteq> 0"
haftmann@27110
   225
  by (simp add: zero_inat_def less_inat_def split: inat.splits)
oheimb@11351
   226
haftmann@27110
   227
lemma iSuc_ile_mono [simp]: "iSuc n \<le> iSuc m \<longleftrightarrow> n \<le> m"
haftmann@27110
   228
  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
haftmann@27110
   229
 
haftmann@27110
   230
lemma iSuc_mono [simp]: "iSuc n < iSuc m \<longleftrightarrow> n < m"
haftmann@27110
   231
  by (simp add: iSuc_def less_inat_def split: inat.splits)
oheimb@11351
   232
haftmann@27110
   233
lemma ile_iSuc [simp]: "n \<le> iSuc n"
haftmann@27110
   234
  by (simp add: iSuc_def less_eq_inat_def split: inat.splits)
oheimb@11351
   235
wenzelm@11355
   236
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0"
haftmann@27110
   237
  by (simp add: zero_inat_def iSuc_def less_eq_inat_def split: inat.splits)
haftmann@27110
   238
haftmann@27110
   239
lemma i0_iless_iSuc [simp]: "0 < iSuc n"
haftmann@27110
   240
  by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits)
haftmann@27110
   241
haftmann@27110
   242
lemma ileI1: "m < n \<Longrightarrow> iSuc m \<le> n"
haftmann@27110
   243
  by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits)
haftmann@27110
   244
haftmann@27110
   245
lemma Suc_ile_eq: "Fin (Suc m) \<le> n \<longleftrightarrow> Fin m < n"
haftmann@27110
   246
  by (cases n) auto
haftmann@27110
   247
haftmann@27110
   248
lemma iless_Suc_eq [simp]: "Fin m < iSuc n \<longleftrightarrow> Fin m \<le> n"
haftmann@27110
   249
  by (auto simp add: iSuc_def less_inat_def split: inat.splits)
oheimb@11351
   250
haftmann@27110
   251
lemma min_inat_simps [simp]:
haftmann@27110
   252
  "min (Fin m) (Fin n) = Fin (min m n)"
haftmann@27110
   253
  "min q 0 = 0"
haftmann@27110
   254
  "min 0 q = 0"
haftmann@27110
   255
  "min q \<infinity> = q"
haftmann@27110
   256
  "min \<infinity> q = q"
haftmann@27110
   257
  by (auto simp add: min_def)
oheimb@11351
   258
haftmann@27110
   259
lemma max_inat_simps [simp]:
haftmann@27110
   260
  "max (Fin m) (Fin n) = Fin (max m n)"
haftmann@27110
   261
  "max q 0 = q"
haftmann@27110
   262
  "max 0 q = q"
haftmann@27110
   263
  "max q \<infinity> = \<infinity>"
haftmann@27110
   264
  "max \<infinity> q = \<infinity>"
haftmann@27110
   265
  by (simp_all add: max_def)
haftmann@27110
   266
haftmann@27110
   267
lemma Fin_ile: "n \<le> Fin m \<Longrightarrow> \<exists>k. n = Fin k"
haftmann@27110
   268
  by (cases n) simp_all
haftmann@27110
   269
haftmann@27110
   270
lemma Fin_iless: "n < Fin m \<Longrightarrow> \<exists>k. n = Fin k"
haftmann@27110
   271
  by (cases n) simp_all
oheimb@11351
   272
oheimb@11351
   273
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j"
nipkow@25134
   274
apply (induct_tac k)
nipkow@25134
   275
 apply (simp (no_asm) only: Fin_0)
haftmann@27110
   276
 apply (fast intro: le_less_trans [OF i0_lb])
nipkow@25134
   277
apply (erule exE)
nipkow@25134
   278
apply (drule spec)
nipkow@25134
   279
apply (erule exE)
nipkow@25134
   280
apply (drule ileI1)
nipkow@25134
   281
apply (rule iSuc_Fin [THEN subst])
nipkow@25134
   282
apply (rule exI)
haftmann@27110
   283
apply (erule (1) le_less_trans)
nipkow@25134
   284
done
oheimb@11351
   285
huffman@26089
   286
haftmann@27110
   287
subsection {* Well-ordering *}
huffman@26089
   288
huffman@26089
   289
lemma less_FinE:
huffman@26089
   290
  "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P"
huffman@26089
   291
by (induct n) auto
huffman@26089
   292
huffman@26089
   293
lemma less_InftyE:
huffman@26089
   294
  "[| n < Infty; !!k. n = Fin k ==> P |] ==> P"
huffman@26089
   295
by (induct n) auto
huffman@26089
   296
huffman@26089
   297
lemma inat_less_induct:
huffman@26089
   298
  assumes prem: "!!n. \<forall>m::inat. m < n --> P m ==> P n" shows "P n"
huffman@26089
   299
proof -
huffman@26089
   300
  have P_Fin: "!!k. P (Fin k)"
huffman@26089
   301
    apply (rule nat_less_induct)
huffman@26089
   302
    apply (rule prem, clarify)
huffman@26089
   303
    apply (erule less_FinE, simp)
huffman@26089
   304
    done
huffman@26089
   305
  show ?thesis
huffman@26089
   306
  proof (induct n)
huffman@26089
   307
    fix nat
huffman@26089
   308
    show "P (Fin nat)" by (rule P_Fin)
huffman@26089
   309
  next
huffman@26089
   310
    show "P Infty"
huffman@26089
   311
      apply (rule prem, clarify)
huffman@26089
   312
      apply (erule less_InftyE)
huffman@26089
   313
      apply (simp add: P_Fin)
huffman@26089
   314
      done
huffman@26089
   315
  qed
huffman@26089
   316
qed
huffman@26089
   317
huffman@26089
   318
instance inat :: wellorder
huffman@26089
   319
proof
haftmann@27823
   320
  fix P and n
haftmann@27823
   321
  assume hyp: "(\<And>n\<Colon>inat. (\<And>m\<Colon>inat. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
haftmann@27823
   322
  show "P n" by (blast intro: inat_less_induct hyp)
huffman@26089
   323
qed
huffman@26089
   324
haftmann@27110
   325
haftmann@27110
   326
subsection {* Traditional theorem names *}
haftmann@27110
   327
haftmann@27110
   328
lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def
haftmann@27110
   329
  plus_inat_def less_eq_inat_def less_inat_def
haftmann@27110
   330
haftmann@27110
   331
lemmas inat_splits = inat.splits
haftmann@27110
   332
oheimb@11351
   333
end