author  chaieb 
Sat, 20 Oct 2007 12:09:33 +0200  
changeset 25112  98824cc791c0 
parent 23315  df3a7e9ebadb 
child 25134  3d4953e88449 
permissions  rwrr 
11355  1 
(* Title: HOL/Library/Nat_Infinity.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb, TU Muenchen 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

4 
*) 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

5 

14706  6 
header {* Natural numbers with infinity *} 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

7 

15131  8 
theory Nat_Infinity 
15140  9 
imports Main 
15131  10 
begin 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

11 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

12 
subsection "Definitions" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

13 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

14 
text {* 
11355  15 
We extend the standard natural numbers by a special value indicating 
16 
infinity. This includes extending the ordering relations @{term "op 

17 
<"} and @{term "op \<le>"}. 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

18 
*} 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

19 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

20 
datatype inat = Fin nat  Infty 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

21 

21210  22 
notation (xsymbols) 
19736  23 
Infty ("\<infinity>") 
24 

21210  25 
notation (HTML output) 
19736  26 
Infty ("\<infinity>") 
27 

14691  28 
instance inat :: "{ord, zero}" .. 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

29 

19736  30 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

31 
iSuc :: "inat => inat" where 
19736  32 
"iSuc i = (case i of Fin n => Fin (Suc n)  \<infinity> => \<infinity>)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

33 

19736  34 
defs (overloaded) 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

35 
Zero_inat_def: "0 == Fin 0" 
11355  36 
iless_def: "m < n == 
37 
case m of Fin m1 => (case n of Fin n1 => m1 < n1  \<infinity> => True) 

38 
 \<infinity> => False" 

39 
ile_def: "(m::inat) \<le> n == \<not> (n < m)" 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

40 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

41 
lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

42 
lemmas inat_splits = inat.split inat.split_asm 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

43 

11355  44 
text {* 
11357  45 
Below is a not quite complete set of theorems. Use the method 
46 
@{text "(simp add: inat_defs split:inat_splits, arith?)"} to prove 

47 
new theorems or solve arithmetic subgoals involving @{typ inat} on 

48 
the fly. 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

49 
*} 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

50 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

51 
subsection "Constructors" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

52 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

53 
lemma Fin_0: "Fin 0 = 0" 
23315  54 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

55 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

56 
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" 
23315  57 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

58 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

59 
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" 
23315  60 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

61 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

62 
lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)" 
23315  63 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

64 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

65 
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" 
23315  66 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

67 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

68 
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" 
23315  69 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

70 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

71 
lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)" 
23315  72 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

73 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

74 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

75 
subsection "Ordering relations" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

76 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

77 
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R" 
23315  78 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

79 

11355  80 
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" 
23315  81 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

82 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

83 
lemma iless_not_refl [simp]: "\<not> n < (n::inat)" 
23315  84 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

85 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

86 
lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)" 
23315  87 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

88 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

89 
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" 
23315  90 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

91 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

92 
lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)" 
23315  93 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

94 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

95 
lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>" 
23315  96 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

97 

11655  98 
lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)" 
23315  99 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

100 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

101 
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)" 
25112  102 
by (simp add: neq0_conv inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

103 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

104 
lemma i0_iless_iSuc [simp]: "0 < iSuc n" 
23315  105 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

106 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

107 
lemma not_ilessi0 [simp]: "\<not> n < (0::inat)" 
23315  108 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

109 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

110 
lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k" 
23315  111 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

112 

11655  113 
lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)" 
23315  114 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

115 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

116 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

117 

11655  118 
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" 
23315  119 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

120 

11355  121 
lemma ile_refl [simp]: "n \<le> (n::inat)" 
23315  122 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

123 

11355  124 
lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" 
23315  125 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

126 

11355  127 
lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" 
23315  128 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

129 

11355  130 
lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" 
23315  131 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

132 

11355  133 
lemma Infty_ub [simp]: "n \<le> \<infinity>" 
23315  134 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

135 

11355  136 
lemma i0_lb [simp]: "(0::inat) \<le> n" 
23315  137 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

138 

11355  139 
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R" 
23315  140 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

141 

11355  142 
lemma Fin_ile_mono [simp]: "(Fin n \<le> Fin m) = (n \<le> m)" 
23315  143 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

144 

11355  145 
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" 
23315  146 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

147 

11355  148 
lemma ileI1: "m < n ==> iSuc m \<le> n" 
23315  149 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

150 

11655  151 
lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" 
23315  152 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

153 

11655  154 
lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" 
23315  155 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

156 

11655  157 
lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" 
23315  158 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

159 

11355  160 
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" 
23315  161 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

162 

11355  163 
lemma ile_iSuc [simp]: "n \<le> iSuc n" 
23315  164 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

165 

11355  166 
lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k" 
23315  167 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

168 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

169 
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" 
11355  170 
apply (induct_tac k) 
171 
apply (simp (no_asm) only: Fin_0) 

172 
apply (fast intro: ile_iless_trans i0_lb) 

173 
apply (erule exE) 

174 
apply (drule spec) 

175 
apply (erule exE) 

176 
apply (drule ileI1) 

177 
apply (rule iSuc_Fin [THEN subst]) 

178 
apply (rule exI) 

179 
apply (erule (1) ile_iless_trans) 

180 
done 

11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

181 

c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

182 
end 