author  huffman 
Mon, 18 Feb 2008 02:10:55 +0100  
changeset 26089  373221497340 
parent 25691  8f8d83af100a 
child 27110  194aa674c2a1 
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 
25691  9 
imports ATP_Linkup 
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 

28 
definition 

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

29 
iSuc :: "inat => inat" where 
19736  30 
"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

31 

25594  32 
instantiation inat :: "{ord, zero}" 
33 
begin 

34 

35 
definition 

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

36 
Zero_inat_def: "0 == Fin 0" 
25594  37 

38 
definition 

11355  39 
iless_def: "m < n == 
40 
case m of Fin m1 => (case n of Fin n1 => m1 < n1  \<infinity> => True) 

41 
 \<infinity> => False" 

25594  42 

43 
definition 

26089  44 
ile_def: "m \<le> n == 
45 
case n of Fin n1 => (case m of Fin m1 => m1 \<le> n1  \<infinity> => False) 

46 
 \<infinity> => True" 

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

47 

25594  48 
instance .. 
49 

50 
end 

51 

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

52 
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

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

54 

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

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

59 
the fly. 

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

60 
*} 
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 
subsection "Constructors" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

63 

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

64 
lemma Fin_0: "Fin 0 = 0" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

65 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

66 

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

67 
lemma Infty_ne_i0 [simp]: "\<infinity> \<noteq> 0" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

68 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

69 

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

70 
lemma i0_ne_Infty [simp]: "0 \<noteq> \<infinity>" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

71 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

72 

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

73 
lemma iSuc_Fin [simp]: "iSuc (Fin n) = Fin (Suc n)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

74 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

75 

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

76 
lemma iSuc_Infty [simp]: "iSuc \<infinity> = \<infinity>" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

77 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

78 

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

79 
lemma iSuc_ne_0 [simp]: "iSuc n \<noteq> 0" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

80 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

81 

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

82 
lemma iSuc_inject [simp]: "(iSuc x = iSuc y) = (x = y)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

83 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

84 

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 
subsection "Ordering relations" 
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

87 

26089  88 
instance inat :: linorder 
89 
proof 

90 
fix x :: inat 

91 
show "x \<le> x" 

92 
by (simp add: inat_defs split: inat_splits) 

93 
next 

94 
fix x y :: inat 

95 
assume "x \<le> y" and "y \<le> x" thus "x = y" 

96 
by (simp add: inat_defs split: inat_splits) 

97 
next 

98 
fix x y z :: inat 

99 
assume "x \<le> y" and "y \<le> z" thus "x \<le> z" 

100 
by (simp add: inat_defs split: inat_splits) 

101 
next 

102 
fix x y :: inat 

103 
show "(x < y) = (x \<le> y \<and> x \<noteq> y)" 

104 
by (simp add: inat_defs order_less_le split: inat_splits) 

105 
next 

106 
fix x y :: inat 

107 
show "x \<le> y \<or> y \<le> x" 

108 
by (simp add: inat_defs linorder_linear split: inat_splits) 

109 
qed 

110 

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

111 
lemma Infty_ilessE [elim!]: "\<infinity> < Fin m ==> R" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

112 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

113 

11355  114 
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" 
26089  115 
by (rule linorder_less_linear) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

116 

26089  117 
lemma iless_not_refl: "\<not> n < (n::inat)" 
118 
by (rule order_less_irrefl) 

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

119 

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

120 
lemma iless_trans: "i < j ==> j < k ==> i < (k::inat)" 
26089  121 
by (rule order_less_trans) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

122 

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

123 
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" 
26089  124 
by (rule order_less_not_sym) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

125 

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

126 
lemma Fin_iless_mono [simp]: "(Fin n < Fin m) = (n < m)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

127 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

128 

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

129 
lemma Fin_iless_Infty [simp]: "Fin n < \<infinity>" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

130 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

131 

11655  132 
lemma Infty_eq [simp]: "(n < \<infinity>) = (n \<noteq> \<infinity>)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

133 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

134 

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

135 
lemma i0_eq [simp]: "((0::inat) < n) = (n \<noteq> 0)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

136 
by (fastsimp simp: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

137 

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

138 
lemma i0_iless_iSuc [simp]: "0 < iSuc n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

139 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

140 

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

141 
lemma not_ilessi0 [simp]: "\<not> n < (0::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

142 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

143 

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

144 
lemma Fin_iless: "n < Fin m ==> \<exists>k. n = Fin k" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

145 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

146 

11655  147 
lemma iSuc_mono [simp]: "(iSuc n < iSuc m) = (n < m)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

148 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

149 

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

150 

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

151 

11655  152 
lemma ile_def2: "(m \<le> n) = (m < n \<or> m = (n::inat))" 
26089  153 
by (rule order_le_less) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

154 

11355  155 
lemma ile_refl [simp]: "n \<le> (n::inat)" 
26089  156 
by (rule order_refl) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

157 

11355  158 
lemma ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" 
26089  159 
by (rule order_trans) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

160 

11355  161 
lemma ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" 
26089  162 
by (rule order_le_less_trans) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

163 

11355  164 
lemma iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" 
26089  165 
by (rule order_less_le_trans) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

166 

11355  167 
lemma Infty_ub [simp]: "n \<le> \<infinity>" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

168 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

169 

11355  170 
lemma i0_lb [simp]: "(0::inat) \<le> n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

171 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

172 

11355  173 
lemma Infty_ileE [elim!]: "\<infinity> \<le> Fin m ==> R" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

174 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

175 

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

178 

11355  179 
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" 
26089  180 
by (rule order_le_neq_trans) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

181 

11355  182 
lemma ileI1: "m < n ==> iSuc m \<le> n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

183 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

184 

11655  185 
lemma Suc_ile_eq: "(Fin (Suc m) \<le> n) = (Fin m < n)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

186 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

187 

11655  188 
lemma iSuc_ile_mono [simp]: "(iSuc n \<le> iSuc m) = (n \<le> m)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

189 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

190 

11655  191 
lemma iless_Suc_eq [simp]: "(Fin m < iSuc n) = (Fin m \<le> n)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

192 
by (simp add: inat_defs split:inat_splits, arith) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

193 

11355  194 
lemma not_iSuc_ilei0 [simp]: "\<not> iSuc n \<le> 0" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

195 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

196 

11355  197 
lemma ile_iSuc [simp]: "n \<le> iSuc n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

198 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

199 

11355  200 
lemma Fin_ile: "n \<le> Fin m ==> \<exists>k. n = Fin k" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

201 
by (simp add: inat_defs split:inat_splits) 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

202 

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

203 
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. Fin k < Y j" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

204 
apply (induct_tac k) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

205 
apply (simp (no_asm) only: Fin_0) 
26089  206 
apply (fast intro: ile_iless_trans [OF i0_lb]) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

207 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

208 
apply (drule spec) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

209 
apply (erule exE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

210 
apply (drule ileI1) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

211 
apply (rule iSuc_Fin [THEN subst]) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

212 
apply (rule exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

213 
apply (erule (1) ile_iless_trans) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

215 

26089  216 

217 
subsection "Wellordering" 

218 

219 
lemma less_FinE: 

220 
"[ n < Fin m; !!k. n = Fin k ==> k < m ==> P ] ==> P" 

221 
by (induct n) auto 

222 

223 
lemma less_InftyE: 

224 
"[ n < Infty; !!k. n = Fin k ==> P ] ==> P" 

225 
by (induct n) auto 

226 

227 
lemma inat_less_induct: 

228 
assumes prem: "!!n. \<forall>m::inat. m < n > P m ==> P n" shows "P n" 

229 
proof  

230 
have P_Fin: "!!k. P (Fin k)" 

231 
apply (rule nat_less_induct) 

232 
apply (rule prem, clarify) 

233 
apply (erule less_FinE, simp) 

234 
done 

235 
show ?thesis 

236 
proof (induct n) 

237 
fix nat 

238 
show "P (Fin nat)" by (rule P_Fin) 

239 
next 

240 
show "P Infty" 

241 
apply (rule prem, clarify) 

242 
apply (erule less_InftyE) 

243 
apply (simp add: P_Fin) 

244 
done 

245 
qed 

246 
qed 

247 

248 
instance inat :: wellorder 

249 
proof 

250 
show "wf {(x::inat, y::inat). x < y}" 

251 
proof (rule wfUNIVI) 

252 
fix P and x :: inat 

253 
assume "\<forall>x::inat. (\<forall>y. (y, x) \<in> {(x, y). x < y} \<longrightarrow> P y) \<longrightarrow> P x" 

254 
hence 1: "!!x::inat. ALL y. y < x > P y ==> P x" by fast 

255 
thus "P x" by (rule inat_less_induct) 

256 
qed 

257 
qed 

258 

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

259 
end 