author  haftmann 
Tue, 18 Dec 2007 14:37:00 +0100  
changeset 25691  8f8d83af100a 
parent 25594  43c718438f9f 
child 26089  373221497340 
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 

11355  44 
ile_def: "(m::inat) \<le> n == \<not> (n < m)" 
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset

45 

25594  46 
instance .. 
47 

48 
end 

49 

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

50 
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

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

52 

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

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

57 
the fly. 

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 

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

60 
subsection "Constructors" 
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 Fin_0: "Fin 0 = 0" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 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

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 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

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_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

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 
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

75 
by (simp add: inat_defs split:inat_splits) 
11351
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 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

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 

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

80 
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

81 
by (simp add: inat_defs split:inat_splits) 
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 

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

84 
subsection "Ordering relations" 
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 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

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 

11355  89 
lemma iless_linear: "m < n \<or> m = n \<or> n < (m::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

90 
by (simp add: inat_defs split:inat_splits, arith) 
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 iless_not_refl [simp]: "\<not> n < (n::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 iless_trans: "i < j ==> j < k ==> i < (k::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 

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

98 
lemma iless_not_sym: "n < m ==> \<not> m < (n::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 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

102 
by (simp add: 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 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

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 

11655  107 
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

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 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

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

112 

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

113 
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

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 
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

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

118 

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

119 
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

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

121 

11655  122 
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

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

124 

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 

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

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

129 

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

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 ile_trans: "i \<le> j ==> j \<le> k ==> i \<le> (k::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 ile_iless_trans: "i \<le> j ==> j < k ==> i < (k::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 iless_ile_trans: "i < j ==> j \<le> k ==> i < (k::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 Infty_ub [simp]: "n \<le> \<infinity>" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

144 

11355  145 
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

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 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

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 

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

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 

11355  154 
lemma ilessI1: "n \<le> m ==> n \<noteq> m ==> n < (m::inat)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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 

11355  157 
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

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

159 

11655  160 
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

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

162 

11655  163 
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

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 

11655  166 
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

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

168 

11355  169 
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

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

171 

11355  172 
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

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

174 

11355  175 
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

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

177 

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

178 
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

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

180 
apply (simp (no_asm) only: Fin_0) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

181 
apply (fast intro: ile_iless_trans i0_lb) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

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

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

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

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

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

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

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

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

190 

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

191 
end 