author  nipkow 
Sun, 21 Oct 2007 14:53:44 +0200  
changeset 25134  3d4953e88449 
parent 25111  d52a58b51f1f 
child 25140  273772abbea2 
permissions  rwrr 
923  1 
(* Title: HOL/Nat.thy 
2 
ID: $Id$ 

21243  3 
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel 
923  4 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

5 
Type "nat" is a linear order, and a datatype; arithmetic operators +  
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

6 
and * (for div, mod and dvd, see theory Divides). 
923  7 
*) 
8 

13449  9 
header {* Natural numbers *} 
10 

15131  11 
theory Nat 
15140  12 
imports Wellfounded_Recursion Ring_and_Field 
23263  13 
uses 
14 
"~~/src/Tools/rat.ML" 

15 
"~~/src/Provers/Arith/cancel_sums.ML" 

16 
("arith_data.ML") 

24091  17 
"~~/src/Provers/Arith/fast_lin_arith.ML" 
18 
("Tools/lin_arith.ML") 

24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24523
diff
changeset

19 
("Tools/function_package/size.ML") 
15131  20 
begin 
13449  21 

22 
subsection {* Type @{text ind} *} 

23 

24 
typedecl ind 

25 

19573  26 
axiomatization 
27 
Zero_Rep :: ind and 

28 
Suc_Rep :: "ind => ind" 

29 
where 

13449  30 
 {* the axiom of infinity in 2 parts *} 
19573  31 
inj_Suc_Rep: "inj Suc_Rep" and 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

32 
Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" 
19573  33 

13449  34 

35 
subsection {* Type nat *} 

36 

37 
text {* Type definition *} 

38 

23740  39 
inductive_set Nat :: "ind set" 
22262  40 
where 
23740  41 
Zero_RepI: "Zero_Rep : Nat" 
42 
 Suc_RepI: "i : Nat ==> Suc_Rep i : Nat" 

13449  43 

44 
global 

45 

46 
typedef (open Nat) 

23740  47 
nat = Nat 
21243  48 
proof 
23740  49 
show "Zero_Rep : Nat" by (rule Nat.Zero_RepI) 
21243  50 
qed 
13449  51 

52 
consts 

53 
Suc :: "nat => nat" 

54 

55 
local 

56 

24995  57 
instance nat :: zero 
58 
Zero_nat_def: "0 == Abs_Nat Zero_Rep" .. 

59 
lemmas [code func del] = Zero_nat_def 

60 

13449  61 
defs 
18648  62 
Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" 
22718  63 

13449  64 
theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" 
65 
apply (unfold Zero_nat_def Suc_def) 

66 
apply (rule Rep_Nat_inverse [THEN subst])  {* types force good instantiation *} 

23740  67 
apply (erule Rep_Nat [THEN Nat.induct]) 
68 
apply (iprover elim: Abs_Nat_inverse [THEN subst]) 

13449  69 
done 
70 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

71 
lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0" 
23740  72 
by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI 
22718  73 
Suc_Rep_not_Zero_Rep) 
13449  74 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

75 
lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m" 
13449  76 
by (rule not_sym, rule Suc_not_Zero not_sym) 
77 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset

78 
lemma inj_Suc[simp]: "inj_on Suc N" 
23740  79 
by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI 
22718  80 
inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) 
13449  81 

82 
lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)" 

15413  83 
by (rule inj_Suc [THEN inj_eq]) 
13449  84 

5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset

85 
rep_datatype nat 
13449  86 
distinct Suc_not_Zero Zero_not_Suc 
87 
inject Suc_Suc_eq 

21411  88 
induction nat_induct 
89 

90 
declare nat.induct [case_names 0 Suc, induct type: nat] 

91 
declare nat.exhaust [case_names 0 Suc, cases type: nat] 

13449  92 

21672  93 
lemmas nat_rec_0 = nat.recs(1) 
94 
and nat_rec_Suc = nat.recs(2) 

95 

96 
lemmas nat_case_0 = nat.cases(1) 

97 
and nat_case_Suc = nat.cases(2) 

98 

24995  99 

100 
text {* Injectiveness and distinctness lemmas *} 

101 

102 
lemma Suc_neq_Zero: "Suc m = 0 ==> R" 

103 
by (rule notE, rule Suc_not_Zero) 

104 

105 
lemma Zero_neq_Suc: "0 = Suc m ==> R" 

106 
by (rule Suc_neq_Zero, erule sym) 

107 

108 
lemma Suc_inject: "Suc x = Suc y ==> x = y" 

109 
by (rule inj_Suc [THEN injD]) 

110 

111 
lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" 

112 
by auto 

113 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

114 
lemma n_not_Suc_n: "n \<noteq> Suc n" 
13449  115 
by (induct n) simp_all 
116 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

117 
lemma Suc_n_not_n: "Suc t \<noteq> t" 
13449  118 
by (rule not_sym, rule n_not_Suc_n) 
119 

24995  120 

13449  121 
text {* A special form of induction for reasoning 
122 
about @{term "m < n"} and @{term "m  n"} *} 

123 

124 
theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> 

125 
(!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" 

14208  126 
apply (rule_tac x = m in spec) 
15251  127 
apply (induct n) 
13449  128 
prefer 2 
129 
apply (rule allI) 

17589  130 
apply (induct_tac x, iprover+) 
13449  131 
done 
132 

24995  133 

134 
subsection {* Arithmetic operators *} 

135 

136 
instance nat :: "{one, plus, minus, times}" 

137 
One_nat_def [simp]: "1 == Suc 0" .. 

138 

139 
primrec 

140 
add_0: "0 + n = n" 

141 
add_Suc: "Suc m + n = Suc (m + n)" 

142 

143 
primrec 

144 
diff_0: "m  0 = m" 

145 
diff_Suc: "m  Suc n = (case m  n of 0 => 0  Suc k => k)" 

146 

147 
primrec 

148 
mult_0: "0 * n = 0" 

149 
mult_Suc: "Suc m * n = n + (m * n)" 

150 

151 

152 
subsection {* Orders on @{typ nat} *} 

153 

154 
definition 

155 
pred_nat :: "(nat * nat) set" where 

156 
"pred_nat = {(m, n). n = Suc m}" 

157 

158 
instance nat :: ord 

159 
less_def: "m < n == (m, n) : pred_nat^+" 

160 
le_def: "m \<le> (n::nat) == ~ (n < m)" .. 

161 

162 
lemmas [code func del] = less_def le_def 

13449  163 

164 
lemma wf_pred_nat: "wf pred_nat" 

14208  165 
apply (unfold wf_def pred_nat_def, clarify) 
166 
apply (induct_tac x, blast+) 

13449  167 
done 
168 

169 
lemma wf_less: "wf {(x, y::nat). x < y}" 

170 
apply (unfold less_def) 

14208  171 
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast) 
13449  172 
done 
173 

174 
lemma less_eq: "((m, n) : pred_nat^+) = (m < n)" 

175 
apply (unfold less_def) 

176 
apply (rule refl) 

177 
done 

178 

179 
subsubsection {* Introduction properties *} 

180 

181 
lemma less_trans: "i < j ==> j < k ==> i < (k::nat)" 

182 
apply (unfold less_def) 

14208  183 
apply (rule trans_trancl [THEN transD], assumption+) 
13449  184 
done 
185 

186 
lemma lessI [iff]: "n < Suc n" 

187 
apply (unfold less_def pred_nat_def) 

188 
apply (simp add: r_into_trancl) 

189 
done 

190 

191 
lemma less_SucI: "i < j ==> i < Suc j" 

14208  192 
apply (rule less_trans, assumption) 
13449  193 
apply (rule lessI) 
194 
done 

195 

196 
lemma zero_less_Suc [iff]: "0 < Suc n" 

197 
apply (induct n) 

198 
apply (rule lessI) 

199 
apply (erule less_trans) 

200 
apply (rule lessI) 

201 
done 

202 

203 
subsubsection {* Elimination properties *} 

204 

205 
lemma less_not_sym: "n < m ==> ~ m < (n::nat)" 

206 
apply (unfold less_def) 

207 
apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym]) 

208 
done 

209 

210 
lemma less_asym: 

211 
assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P 

212 
apply (rule contrapos_np) 

213 
apply (rule less_not_sym) 

214 
apply (rule h1) 

215 
apply (erule h2) 

216 
done 

217 

218 
lemma less_not_refl: "~ n < (n::nat)" 

219 
apply (unfold less_def) 

220 
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl]) 

221 
done 

222 

223 
lemma less_irrefl [elim!]: "(n::nat) < n ==> R" 

224 
by (rule notE, rule less_not_refl) 

225 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

226 
lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast 
13449  227 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

228 
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t" 
13449  229 
by (rule not_sym, rule less_not_refl2) 
230 

231 
lemma lessE: 

232 
assumes major: "i < k" 

233 
and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P" 

234 
shows P 

14208  235 
apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all) 
13449  236 
apply (erule p1) 
237 
apply (rule p2) 

14208  238 
apply (simp add: less_def pred_nat_def, assumption) 
13449  239 
done 
240 

241 
lemma not_less0 [iff]: "~ n < (0::nat)" 

242 
by (blast elim: lessE) 

243 

244 
lemma less_zeroE: "(n::nat) < 0 ==> R" 

245 
by (rule notE, rule not_less0) 

246 

247 
lemma less_SucE: assumes major: "m < Suc n" 

248 
and less: "m < n ==> P" and eq: "m = n ==> P" shows P 

249 
apply (rule major [THEN lessE]) 

14208  250 
apply (rule eq, blast) 
251 
apply (rule less, blast) 

13449  252 
done 
253 

254 
lemma less_Suc_eq: "(m < Suc n) = (m < n  m = n)" 

255 
by (blast elim!: less_SucE intro: less_trans) 

256 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset

257 
lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)" 
13449  258 
by (simp add: less_Suc_eq) 
259 

260 
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)" 

261 
by (simp add: less_Suc_eq) 

262 

263 
lemma Suc_mono: "m < n ==> Suc m < Suc n" 

264 
by (induct n) (fast elim: less_trans lessE)+ 

265 

266 
text {* "Less than" is a linear ordering *} 

267 
lemma less_linear: "m < n  m = n  n < (m::nat)" 

15251  268 
apply (induct m) 
269 
apply (induct n) 

13449  270 
apply (rule refl [THEN disjI1, THEN disjI2]) 
271 
apply (rule zero_less_Suc [THEN disjI1]) 

272 
apply (blast intro: Suc_mono less_SucI elim: lessE) 

273 
done 

274 

14302  275 
text {* "Less than" is antisymmetric, sort of *} 
276 
lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n" 

22718  277 
apply(simp only:less_Suc_eq) 
278 
apply blast 

279 
done 

14302  280 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

281 
lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n  n < m)" 
13449  282 
using less_linear by blast 
283 

284 
lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m" 

285 
and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m" 

286 
shows "P n m" 

287 
apply (rule less_linear [THEN disjE]) 

288 
apply (erule_tac [2] disjE) 

289 
apply (erule lessCase) 

290 
apply (erule sym [THEN eqCase]) 

291 
apply (erule major) 

292 
done 

293 

294 

295 
subsubsection {* Inductive (?) properties *} 

296 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

297 
lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n" 
13449  298 
apply (simp add: nat_neq_iff) 
299 
apply (blast elim!: less_irrefl less_SucE elim: less_asym) 

300 
done 

301 

302 
lemma Suc_lessD: "Suc m < n ==> m < n" 

303 
apply (induct n) 

304 
apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+ 

305 
done 

306 

307 
lemma Suc_lessE: assumes major: "Suc i < k" 

308 
and minor: "!!j. i < j ==> k = Suc j ==> P" shows P 

309 
apply (rule major [THEN lessE]) 

310 
apply (erule lessI [THEN minor]) 

14208  311 
apply (erule Suc_lessD [THEN minor], assumption) 
13449  312 
done 
313 

314 
lemma Suc_less_SucD: "Suc m < Suc n ==> m < n" 

315 
by (blast elim: lessE dest: Suc_lessD) 

4104  316 

16635  317 
lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" 
13449  318 
apply (rule iffI) 
319 
apply (erule Suc_less_SucD) 

320 
apply (erule Suc_mono) 

321 
done 

322 

323 
lemma less_trans_Suc: 

324 
assumes le: "i < j" shows "j < k ==> Suc i < k" 

14208  325 
apply (induct k, simp_all) 
13449  326 
apply (insert le) 
327 
apply (simp add: less_Suc_eq) 

328 
apply (blast dest: Suc_lessD) 

329 
done 

330 

16635  331 
lemma [code]: "((n::nat) < 0) = False" by simp 
332 
lemma [code]: "(0 < Suc n) = True" by simp 

333 

13449  334 
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m  n < m"} *} 
335 
lemma not_less_eq: "(~ m < n) = (n < Suc m)" 

22718  336 
by (induct m n rule: diff_induct) simp_all 
13449  337 

338 
text {* Complete induction, aka courseofvalues induction *} 

339 
lemma nat_less_induct: 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

340 
assumes prem: "!!n. \<forall>m::nat. m < n > P m ==> P n" shows "P n" 
22718  341 
apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]]) 
13449  342 
apply (rule prem) 
14208  343 
apply (unfold less_def, assumption) 
13449  344 
done 
345 

14131  346 
lemmas less_induct = nat_less_induct [rule_format, case_names less] 
347 

21243  348 

24995  349 
text {* Properties of "less than or equal" *} 
13449  350 

351 
text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

352 
lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)" 
22718  353 
unfolding le_def by (rule not_less_eq [symmetric]) 
13449  354 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

355 
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n" 
13449  356 
by (rule less_Suc_eq_le [THEN iffD2]) 
357 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

358 
lemma le0 [iff]: "(0::nat) \<le> n" 
22718  359 
unfolding le_def by (rule not_less0) 
13449  360 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

361 
lemma Suc_n_not_le_n: "~ Suc n \<le> n" 
13449  362 
by (simp add: le_def) 
363 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

364 
lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)" 
13449  365 
by (induct i) (simp_all add: le_def) 
366 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

367 
lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n  m = Suc n)" 
13449  368 
by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq) 
369 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

370 
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R" 
17589  371 
by (drule le_Suc_eq [THEN iffD1], iprover+) 
13449  372 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

373 
lemma Suc_leI: "m < n ==> Suc(m) \<le> n" 
13449  374 
apply (simp add: le_def less_Suc_eq) 
375 
apply (blast elim!: less_irrefl less_asym) 

376 
done  {* formerly called lessD *} 

377 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

378 
lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n" 
13449  379 
by (simp add: le_def less_Suc_eq) 
380 

381 
text {* Stronger version of @{text Suc_leD} *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

382 
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n" 
13449  383 
apply (simp add: le_def less_Suc_eq) 
384 
using less_linear 

385 
apply blast 

386 
done 

387 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

388 
lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)" 
13449  389 
by (blast intro: Suc_leI Suc_le_lessD) 
390 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

391 
lemma le_SucI: "m \<le> n ==> m \<le> Suc n" 
13449  392 
by (unfold le_def) (blast dest: Suc_lessD) 
393 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

394 
lemma less_imp_le: "m < n ==> m \<le> (n::nat)" 
13449  395 
by (unfold le_def) (blast elim: less_asym) 
396 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

397 
text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *} 
13449  398 
lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq 
399 

400 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

401 
text {* Equivalence of @{term "m \<le> n"} and @{term "m < n  m = n"} *} 
13449  402 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

403 
lemma le_imp_less_or_eq: "m \<le> n ==> m < n  m = (n::nat)" 
22718  404 
unfolding le_def 
13449  405 
using less_linear 
22718  406 
by (blast elim: less_irrefl less_asym) 
13449  407 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

408 
lemma less_or_eq_imp_le: "m < n  m = n ==> m \<le> (n::nat)" 
22718  409 
unfolding le_def 
13449  410 
using less_linear 
22718  411 
by (blast elim!: less_irrefl elim: less_asym) 
13449  412 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

413 
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n  m=n)" 
17589  414 
by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq) 
13449  415 

22718  416 
text {* Useful with @{text blast}. *} 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

417 
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n" 
22718  418 
by (rule less_or_eq_imp_le) (rule disjI2) 
13449  419 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

420 
lemma le_refl: "n \<le> (n::nat)" 
13449  421 
by (simp add: le_eq_less_or_eq) 
422 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

423 
lemma le_less_trans: "[ i \<le> j; j < k ] ==> i < (k::nat)" 
13449  424 
by (blast dest!: le_imp_less_or_eq intro: less_trans) 
425 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

426 
lemma less_le_trans: "[ i < j; j \<le> k ] ==> i < (k::nat)" 
13449  427 
by (blast dest!: le_imp_less_or_eq intro: less_trans) 
428 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

429 
lemma le_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> (k::nat)" 
13449  430 
by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) 
431 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

432 
lemma le_anti_sym: "[ m \<le> n; n \<le> m ] ==> m = (n::nat)" 
13449  433 
by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) 
434 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

435 
lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)" 
13449  436 
by (simp add: le_simps) 
437 

438 
text {* Axiom @{text order_less_le} of class @{text order}: *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

439 
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)" 
13449  440 
by (simp add: le_def nat_neq_iff) (blast elim!: less_asym) 
441 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

442 
lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n" 
13449  443 
by (rule iffD2, rule nat_less_le, rule conjI) 
444 

445 
text {* Axiom @{text linorder_linear} of class @{text linorder}: *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

446 
lemma nat_le_linear: "(m::nat) \<le> n  n \<le> m" 
13449  447 
apply (simp add: le_eq_less_or_eq) 
22718  448 
using less_linear by blast 
13449  449 

24995  450 
text {* Type @{typ nat} is a wellfounded linear order *} 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

451 

22318  452 
instance nat :: wellorder 
14691  453 
by intro_classes 
454 
(assumption  

455 
rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+ 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

456 

22718  457 
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 
15921  458 

13449  459 
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)" 
460 
by (blast elim!: less_SucE) 

461 

462 
text {* 

463 
Rewrite @{term "n < Suc m"} to @{term "n = m"} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

464 
if @{term "~ n < m"} or @{term "m \<le> n"} hold. 
13449  465 
Not suitable as default simprules because they often lead to looping 
466 
*} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

467 
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)" 
13449  468 
by (rule not_less_less_Suc_eq, rule leD) 
469 

470 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

471 

472 

473 
text {* 

22718  474 
Reorientation of the equations @{text "0 = x"} and @{text "1 = x"}. 
475 
No longer added as simprules (they loop) 

13449  476 
but via @{text reorient_simproc} in Bin 
477 
*} 

478 

479 
text {* Polymorphic, not just for @{typ nat} *} 

480 
lemma zero_reorient: "(0 = x) = (x = 0)" 

481 
by auto 

482 

483 
lemma one_reorient: "(1 = x) = (x = 1)" 

484 
by auto 

485 

22718  486 
text {* These two rules ease the use of primitive recursion. 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

487 
NOTE USE OF @{text "=="} *} 
13449  488 
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c" 
489 
by simp 

490 

491 
lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)" 

492 
by simp 

493 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

494 
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m" 
22718  495 
by (cases n) simp_all 
13449  496 

22718  497 
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0" 
498 
by (cases n) simp_all 

13449  499 

25111
d52a58b51f1f
neq0_conv removed from [iff]  causes problems by simple goals with blast, auto etc...
chaieb
parents:
25076
diff
changeset

500 
lemma neq0_conv: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)" 
22718  501 
by (cases n) simp_all 
13449  502 

503 
text {* This theorem is useful with @{text blast} *} 

504 
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n" 

17589  505 
by (rule iffD1, rule neq0_conv, iprover) 
13449  506 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

507 
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" 
13449  508 
by (fast intro: not0_implies_Suc) 
509 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset

510 
lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

511 
using neq0_conv by blast 
13449  512 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

513 
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" 
13449  514 
by (induct m') simp_all 
515 

516 
text {* Useful in certain inductive arguments *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

517 
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0  (\<exists>j. m = Suc j & j < n))" 
22718  518 
by (cases m) simp_all 
13449  519 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

520 
lemma nat_induct2: "[P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))] ==> P n" 
13449  521 
apply (rule nat_less_induct) 
522 
apply (case_tac n) 

523 
apply (case_tac [2] nat) 

524 
apply (blast intro: less_trans)+ 

525 
done 

526 

21243  527 

15341
254f6f00b60e
converted to Isar script, simplifying some results
paulson
parents:
15281
diff
changeset

528 
subsection {* @{text LEAST} theorems for type @{typ nat}*} 
13449  529 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

530 
lemma Least_Suc: 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

531 
"[ P n; ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" 
14208  532 
apply (case_tac "n", auto) 
13449  533 
apply (frule LeastI) 
534 
apply (drule_tac P = "%x. P (Suc x) " in LeastI) 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

535 
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 
13449  536 
apply (erule_tac [2] Least_le) 
14208  537 
apply (case_tac "LEAST x. P x", auto) 
13449  538 
apply (drule_tac P = "%x. P (Suc x) " in Least_le) 
539 
apply (blast intro: order_antisym) 

540 
done 

541 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

542 
lemma Least_Suc2: 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

543 
"[P n; Q m; ~P 0; !k. P (Suc k) = Q k] ==> Least P = Suc (Least Q)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

544 
by (erule (1) Least_Suc [THEN ssubst], simp) 
13449  545 

546 

547 
subsection {* @{term min} and @{term max} *} 

548 

25076  549 
lemma mono_Suc: "mono Suc" 
550 
by (rule monoI) simp 

551 

13449  552 
lemma min_0L [simp]: "min 0 n = (0::nat)" 
553 
by (rule min_leastL) simp 

554 

555 
lemma min_0R [simp]: "min n 0 = (0::nat)" 

556 
by (rule min_leastR) simp 

557 

558 
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" 

25076  559 
by (simp add: mono_Suc min_of_mono) 
13449  560 

22191  561 
lemma min_Suc1: 
562 
"min (Suc n) m = (case m of 0 => 0  Suc m' => Suc(min n m'))" 

22718  563 
by (simp split: nat.split) 
22191  564 

565 
lemma min_Suc2: 

566 
"min m (Suc n) = (case m of 0 => 0  Suc m' => Suc(min m' n))" 

567 
by (simp split: nat.split) 

568 

13449  569 
lemma max_0L [simp]: "max 0 n = (n::nat)" 
570 
by (rule max_leastL) simp 

571 

572 
lemma max_0R [simp]: "max n 0 = (n::nat)" 

573 
by (rule max_leastR) simp 

574 

575 
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)" 

25076  576 
by (simp add: mono_Suc max_of_mono) 
13449  577 

22191  578 
lemma max_Suc1: 
579 
"max (Suc n) m = (case m of 0 => Suc n  Suc m' => Suc(max n m'))" 

22718  580 
by (simp split: nat.split) 
22191  581 

582 
lemma max_Suc2: 

583 
"max m (Suc n) = (case m of 0 => Suc n  Suc m' => Suc(max m' n))" 

584 
by (simp split: nat.split) 

585 

13449  586 

587 
subsection {* Basic rewrite rules for the arithmetic operators *} 

588 

589 
text {* Difference *} 

590 

14193
30e41f63712e
Improved efficiency of code generated for + and 
berghofe
parents:
14131
diff
changeset

591 
lemma diff_0_eq_0 [simp, code]: "0  n = (0::nat)" 
15251  592 
by (induct n) simp_all 
13449  593 

14193
30e41f63712e
Improved efficiency of code generated for + and 
berghofe
parents:
14131
diff
changeset

594 
lemma diff_Suc_Suc [simp, code]: "Suc(m)  Suc(n) = m  n" 
15251  595 
by (induct n) simp_all 
13449  596 

597 

598 
text {* 

599 
Could be (and is, below) generalized in various ways 

600 
However, none of the generalizations are currently in the simpset, 

601 
and I dread to think what happens if I put them in 

602 
*} 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

603 
lemma Suc_pred [simp]: "0 \<noteq> n ==> Suc (n  Suc 0) = n" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

604 
by (simp split add: nat.split) 
13449  605 

14193
30e41f63712e
Improved efficiency of code generated for + and 
berghofe
parents:
14131
diff
changeset

606 
declare diff_Suc [simp del, code del] 
13449  607 

608 

609 
subsection {* Addition *} 

610 

611 
lemma add_0_right [simp]: "m + 0 = (m::nat)" 

612 
by (induct m) simp_all 

613 

614 
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)" 

615 
by (induct m) simp_all 

616 

19890  617 
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" 
618 
by simp 

14193
30e41f63712e
Improved efficiency of code generated for + and 
berghofe
parents:
14131
diff
changeset

619 

13449  620 

621 
text {* Associative law for addition *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

622 
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" 
13449  623 
by (induct m) simp_all 
624 

625 
text {* Commutative law for addition *} 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

626 
lemma nat_add_commute: "m + n = n + (m::nat)" 
13449  627 
by (induct m) simp_all 
628 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

629 
lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)" 
13449  630 
apply (rule mk_left_commute [of "op +"]) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

631 
apply (rule nat_add_assoc) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

632 
apply (rule nat_add_commute) 
13449  633 
done 
634 

14331  635 
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" 
13449  636 
by (induct k) simp_all 
637 

14331  638 
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" 
13449  639 
by (induct k) simp_all 
640 

14331  641 
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))" 
13449  642 
by (induct k) simp_all 
643 

14331  644 
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" 
13449  645 
by (induct k) simp_all 
646 

647 
text {* Reasoning about @{text "m + 0 = 0"}, etc. *} 

648 

22718  649 
lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)" 
650 
by (cases m) simp_all 

13449  651 

652 
lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0  m=0 & n= Suc 0)" 

22718  653 
by (cases m) simp_all 
13449  654 

655 
lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0  m = 0 & n = Suc 0)" 

656 
by (rule trans, rule eq_commute, rule add_is_1) 

657 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

658 
lemma add_gr_0 [iff]: "!!m::nat. (m + n \<noteq> 0) = (m\<noteq>0  n\<noteq>0)" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

659 
by simp 
13449  660 

661 
lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0" 

662 
apply (drule add_0_right [THEN ssubst]) 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

663 
apply (simp add: nat_add_assoc del: add_0_right) 
13449  664 
done 
665 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset

666 
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" 
22718  667 
apply (induct k) 
668 
apply simp 

669 
apply(drule comp_inj_on[OF _ inj_Suc]) 

670 
apply (simp add:o_def) 

671 
done 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset

672 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset

673 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

674 
subsection {* Multiplication *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

675 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

676 
text {* right annihilation in product *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

677 
lemma mult_0_right [simp]: "(m::nat) * 0 = 0" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

678 
by (induct m) simp_all 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

679 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

680 
text {* right successor law for multiplication *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

681 
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

682 
by (induct m) (simp_all add: nat_add_left_commute) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

683 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

684 
text {* Commutative law for multiplication *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

685 
lemma nat_mult_commute: "m * n = n * (m::nat)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

686 
by (induct m) simp_all 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

687 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

688 
text {* addition distributes over multiplication *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

689 
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

690 
by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

691 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

692 
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

693 
by (induct m) (simp_all add: nat_add_assoc) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

694 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

695 
text {* Associative law for multiplication *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

696 
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

697 
by (induct m) (simp_all add: add_mult_distrib) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

698 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

699 

14740  700 
text{*The naturals form a @{text comm_semiring_1_cancel}*} 
14738  701 
instance nat :: comm_semiring_1_cancel 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

702 
proof 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

703 
fix i j k :: nat 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

704 
show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

705 
show "i + j = j + i" by (rule nat_add_commute) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

706 
show "0 + i = i" by simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

707 
show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

708 
show "i * j = j * i" by (rule nat_mult_commute) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

709 
show "1 * i = i" by simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

710 
show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

711 
show "0 \<noteq> (1::nat)" by simp 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

712 
assume "k+i = k+j" thus "i=j" by simp 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

713 
qed 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

714 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

715 
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0  n=0)" 
15251  716 
apply (induct m) 
22718  717 
apply (induct_tac [2] n) 
718 
apply simp_all 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

719 
done 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

720 

21243  721 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

722 
subsection {* Monotonicity of Addition *} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

723 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

724 
text {* strict, in 1st argument *} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

725 
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

726 
by (induct k) simp_all 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

727 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

728 
text {* strict, in both arguments *} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

729 
lemma add_less_mono: "[i < j; k < l] ==> i + k < j + (l::nat)" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

730 
apply (rule add_less_mono1 [THEN less_trans], assumption+) 
15251  731 
apply (induct j, simp_all) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

732 
done 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

733 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

734 
text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

735 
lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

736 
apply (induct n) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

737 
apply (simp_all add: order_le_less) 
22718  738 
apply (blast elim!: less_SucE 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

739 
intro!: add_0_right [symmetric] add_Suc_right [symmetric]) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

740 
done 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

741 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

742 
text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

743 
lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j" 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

744 
apply(auto simp: gr0_conv_Suc) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

745 
apply (induct_tac m) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

746 
apply (simp_all add: add_less_mono) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

747 
done 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

748 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

749 

14740  750 
text{*The naturals form an ordered @{text comm_semiring_1_cancel}*} 
14738  751 
instance nat :: ordered_semidom 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

752 
proof 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

753 
fix i j k :: nat 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

754 
show "0 < (1::nat)" by simp 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

755 
show "i \<le> j ==> k + i \<le> k + j" by simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

756 
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

757 
qed 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

758 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

759 
lemma nat_mult_1: "(1::nat) * n = n" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

760 
by simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

761 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

762 
lemma nat_mult_1_right: "n * (1::nat) = n" 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

763 
by simp 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

764 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

765 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

766 
subsection {* Additional theorems about "less than" *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

767 

19870  768 
text{*An induction rule for estabilishing binary relations*} 
22718  769 
lemma less_Suc_induct: 
19870  770 
assumes less: "i < j" 
771 
and step: "!!i. P i (Suc i)" 

772 
and trans: "!!i j k. P i j ==> P j k ==> P i k" 

773 
shows "P i j" 

774 
proof  

22718  775 
from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add) 
776 
have "P i (Suc (i + k))" 

19870  777 
proof (induct k) 
22718  778 
case 0 
779 
show ?case by (simp add: step) 

19870  780 
next 
781 
case (Suc k) 

22718  782 
thus ?case by (auto intro: assms) 
19870  783 
qed 
22718  784 
thus "P i j" by (simp add: j) 
19870  785 
qed 
786 

24438  787 
text {* The method of infinite descent, frequently used in number theory. 
788 
Provided by Roelof Oosterhuis. 

789 
$P(n)$ is true for all $n\in\mathbb{N}$ if 

790 
\begin{itemize} 

791 
\item case ``0'': given $n=0$ prove $P(n)$, 

792 
\item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists 

793 
a smaller integer $m$ such that $\neg P(m)$. 

794 
\end{itemize} *} 

795 

24523  796 
lemma infinite_descent0[case_names 0 smaller]: 
24438  797 
"\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n" 
798 
by (induct n rule: less_induct, case_tac "n>0", auto) 

799 

24523  800 
text{* A compact version without explicit base case: *} 
801 
lemma infinite_descent: 

802 
"\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m \<rbrakk> \<Longrightarrow> P n" 

803 
by (induct n rule: less_induct, auto) 

804 

24438  805 

806 
text {* Infinite descent using a mapping to $\mathbb{N}$: 

807 
$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and 

808 
\begin{itemize} 

809 
\item case ``0'': given $V(x)=0$ prove $P(x)$, 

810 
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$. 

811 
\end{itemize} 

812 
NB: the proof also shows how to use the previous lemma. *} 

24523  813 
corollary infinite_descent0_measure[case_names 0 smaller]: 
814 
assumes 0: "!!x. V x = (0::nat) \<Longrightarrow> P x" 

815 
and 1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)" 

24438  816 
shows "P x" 
817 
proof  

818 
obtain n where "n = V x" by auto 

24523  819 
moreover have "!!x. V x = n \<Longrightarrow> P x" 
820 
proof (induct n rule: infinite_descent0) 

24438  821 
case 0  "i.e. $V(x) = 0$" 
822 
with 0 show "P x" by auto 

823 
next  "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" 

824 
case (smaller n) 

825 
then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto 

826 
with 1 obtain y where "V y < V x \<and> \<not> P y" by auto 

827 
with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto 

828 
thus ?case by auto 

829 
qed 

830 
ultimately show "P x" by auto 

831 
qed 

19870  832 

24523  833 
text{* Again, without explicit base case: *} 
834 
lemma infinite_descent_measure: 

835 
assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x" 

836 
proof  

837 
from assms obtain n where "n = V x" by auto 

838 
moreover have "!!x. V x = n \<Longrightarrow> P x" 

839 
proof (induct n rule: infinite_descent, auto) 

840 
fix x assume "\<not> P x" 

841 
with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto 

842 
qed 

843 
ultimately show "P x" by auto 

844 
qed 

845 

846 

847 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

848 
text {* A [clumsy] way of lifting @{text "<"} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

849 
monotonicity to @{text "\<le>"} monotonicity *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

850 
lemma less_mono_imp_le_mono: 
24438  851 
"\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)" 
852 
by (simp add: order_le_less) (blast) 

853 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

854 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

855 
text {* nonstrict, in 1st argument *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

856 
lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)" 
24438  857 
by (rule add_right_mono) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

858 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

859 
text {* nonstrict, in both arguments *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

860 
lemma add_le_mono: "[ i \<le> j; k \<le> l ] ==> i + k \<le> j + (l::nat)" 
24438  861 
by (rule add_mono) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

862 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

863 
lemma le_add2: "n \<le> ((m + n)::nat)" 
24438  864 
by (insert add_right_mono [of 0 m n], simp) 
13449  865 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

866 
lemma le_add1: "n \<le> ((n + m)::nat)" 
24438  867 
by (simp add: add_commute, rule le_add2) 
13449  868 

869 
lemma less_add_Suc1: "i < Suc (i + m)" 

24438  870 
by (rule le_less_trans, rule le_add1, rule lessI) 
13449  871 

872 
lemma less_add_Suc2: "i < Suc (m + i)" 

24438  873 
by (rule le_less_trans, rule le_add2, rule lessI) 
13449  874 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

875 
lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))" 
24438  876 
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) 
13449  877 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

878 
lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m" 
24438  879 
by (rule le_trans, assumption, rule le_add1) 
13449  880 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

881 
lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j" 
24438  882 
by (rule le_trans, assumption, rule le_add2) 
13449  883 

884 
lemma trans_less_add1: "(i::nat) < j ==> i < j + m" 

24438  885 
by (rule less_le_trans, assumption, rule le_add1) 
13449  886 

887 
lemma trans_less_add2: "(i::nat) < j ==> i < m + j" 

24438  888 
by (rule less_le_trans, assumption, rule le_add2) 
13449  889 

890 
lemma add_lessD1: "i + j < (k::nat) ==> i < k" 

24438  891 
apply (rule le_less_trans [of _ "i+j"]) 
892 
apply (simp_all add: le_add1) 

893 
done 

13449  894 

895 
lemma not_add_less1 [iff]: "~ (i + j < (i::nat))" 

24438  896 
apply (rule notI) 
897 
apply (erule add_lessD1 [THEN less_irrefl]) 

898 
done 

13449  899 

900 
lemma not_add_less2 [iff]: "~ (j + i < (i::nat))" 

24438  901 
by (simp add: add_commute not_add_less1) 
13449  902 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

903 
lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)" 
24438  904 
apply (rule order_trans [of _ "m+k"]) 
905 
apply (simp_all add: le_add1) 

906 
done 

13449  907 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

908 
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" 
24438  909 
apply (simp add: add_commute) 
910 
apply (erule add_leD1) 

911 
done 

13449  912 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

913 
lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R" 
24438  914 
by (blast dest: add_leD1 add_leD2) 
13449  915 

916 
text {* needs @{text "!!k"} for @{text add_ac} to work *} 

917 
lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n" 

24438  918 
by (force simp del: add_Suc_right 
13449  919 
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) 
920 

921 

922 
subsection {* Difference *} 

923 

924 
lemma diff_self_eq_0 [simp]: "(m::nat)  m = 0" 

24438  925 
by (induct m) simp_all 
13449  926 

927 
text {* Addition is the inverse of subtraction: 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

928 
if @{term "n \<le> m"} then @{term "n + (m  n) = m"}. *} 
13449  929 
lemma add_diff_inverse: "~ m < n ==> n + (m  n) = (m::nat)" 
24438  930 
by (induct m n rule: diff_induct) simp_all 
13449  931 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

932 
lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m  n) = (m::nat)" 
24438  933 
by (simp add: add_diff_inverse linorder_not_less) 
13449  934 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

935 
lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m  n) + n = (m::nat)" 
24438  936 
by (simp add: le_add_diff_inverse add_commute) 
13449  937 

938 

939 
subsection {* More results about difference *} 

940 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

941 
lemma Suc_diff_le: "n \<le> m ==> Suc m  n = Suc (m  n)" 
24438  942 
by (induct m n rule: diff_induct) simp_all 
13449  943 

944 
lemma diff_less_Suc: "m  n < Suc m" 

24438  945 
apply (induct m n rule: diff_induct) 
946 
apply (erule_tac [3] less_SucE) 

947 
apply (simp_all add: less_Suc_eq) 

948 
done 

13449  949 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

950 
lemma diff_le_self [simp]: "m  n \<le> (m::nat)" 
24438  951 
by (induct m n rule: diff_induct) (simp_all add: le_SucI) 
13449  952 

953 
lemma less_imp_diff_less: "(j::nat) < k ==> j  n < k" 

24438  954 
by (rule le_less_trans, rule diff_le_self) 
13449  955 

956 
lemma diff_diff_left: "(i::nat)  j  k = i  (j + k)" 

24438  957 
by (induct i j rule: diff_induct) simp_all 
13449  958 

959 
lemma Suc_diff_diff [simp]: "(Suc m  n)  Suc k = m  n  k" 

24438  960 
by (simp add: diff_diff_left) 
13449  961 

962 
lemma diff_Suc_less [simp]: "0<n ==> n  Suc i < n" 

24438  963 
by (cases n) (auto simp add: le_simps) 
13449  964 

965 
text {* This and the next few suggested by Florian Kammueller *} 

966 
lemma diff_commute: "(i::nat)  j  k = i  k  j" 

24438  967 
by (simp add: diff_diff_left add_commute) 
13449  968 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

969 
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j)  k = i + (j  k)" 
24438  970 
by (induct j k rule: diff_induct) simp_all 
13449  971 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

972 
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i)  k = (j  k) + i" 
24438  973 
by (simp add: add_commute diff_add_assoc) 
13449  974 

975 
lemma diff_add_inverse: "(n + m)  n = (m::nat)" 

24438  976 
by (induct n) simp_all 
13449  977 

978 
lemma diff_add_inverse2: "(m + n)  n = (m::nat)" 

24438  979 
by (simp add: diff_add_assoc) 
13449  980 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

981 
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j  i = k) = (j = k + i)" 
24438  982 
by (auto simp add: diff_add_inverse2) 
13449  983 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

984 
lemma diff_is_0_eq [simp]: "((m::nat)  n = 0) = (m \<le> n)" 
24438  985 
by (induct m n rule: diff_induct) simp_all 
13449  986 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

987 
lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat)  n = 0" 
24438  988 
by (rule iffD2, rule diff_is_0_eq) 
13449  989 

990 
lemma zero_less_diff [simp]: "(0 < n  (m::nat)) = (m < n)" 

24438  991 
by (induct m n rule: diff_induct) simp_all 
13449  992 

22718  993 
lemma less_imp_add_positive: 
994 
assumes "i < j" 

995 
shows "\<exists>k::nat. 0 < k & i + k = j" 

996 
proof 

997 
from assms show "0 < j  i & i + (j  i) = j" 

23476  998 
by (simp add: order_less_imp_le) 
22718  999 
qed 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

1000 

13449  1001 
lemma diff_cancel: "(k + m)  (k + n) = m  (n::nat)" 
24438  1002 
by (induct k) simp_all 
13449  1003 

1004 
lemma diff_cancel2: "(m + k)  (n + k) = m  (n::nat)" 

24438  1005 
by (simp add: diff_cancel add_commute) 
13449  1006 

1007 
lemma diff_add_0: "n  (n + m) = (0::nat)" 

24438  1008 
by (induct n) simp_all 
13449  1009 

1010 

1011 
text {* Difference distributes over multiplication *} 

1012 

1013 
lemma diff_mult_distrib: "((m::nat)  n) * k = (m * k)  (n * k)" 

24438  1014 
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) 
13449  1015 

1016 
lemma diff_mult_distrib2: "k * ((m::nat)  n) = (k * m)  (k * n)" 

24438  1017 
by (simp add: diff_mult_distrib mult_commute [of k]) 
13449  1018 
 {* NOT added as rewrites, since sometimes they are used from righttoleft *} 
1019 

1020 
lemmas nat_distrib = 

1021 
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 

1022 

1023 

1024 
subsection {* Monotonicity of Multiplication *} 

1025 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1026 
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k" 
24438  1027 
by (simp add: mult_right_mono) 
13449  1028 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1029 
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" 
24438  1030 
by (simp add: mult_left_mono) 
13449  1031 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1032 
text {* @{text "\<le>"} monotonicity, BOTH arguments *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1033 
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" 
24438  1034 
by (simp add: mult_mono) 
13449  1035 

1036 
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" 

24438  1037 
by (simp add: mult_strict_right_mono) 
13449  1038 

14266  1039 
text{*Differs from the standard @{text zero_less_mult_iff} in that 
1040 
there are no negative numbers.*} 

1041 
lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" 

13449  1042 
apply (induct m) 
22718  1043 
apply simp 
1044 
apply (case_tac n) 

1045 
apply simp_all 

13449  1046 
done 
1047 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1048 
lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)" 
13449  1049 
apply (induct m) 
22718  1050 
apply simp 
1051 
apply (case_tac n) 

1052 
apply simp_all 

13449  1053 
done 
1054 

1055 
lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)" 

22718  1056 
apply (induct m) 
1057 
apply simp 

1058 
apply (induct n) 

1059 
apply auto 

13449  1060 
done 
1061 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset

1062 
lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" 
13449  1063 
apply (rule trans) 
14208  1064 
apply (rule_tac [2] mult_eq_1_iff, fastsimp) 
13449  1065 
done 
1066 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

1067 
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)" 
13449  1068 
apply (safe intro!: mult_less_mono1) 
14208  1069 
apply (case_tac k, auto) 
13449  1070 
apply (simp del: le_0_eq add: linorder_not_le [symmetric]) 
1071 
apply (blast intro: mult_le_mono1) 

1072 
done 

1073 

1074 
lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)" 

24438  1075 
by (simp add: mult_commute [of k]) 
13449  1076 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1077 
lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k > m \<le> n)" 
24438  1078 
by (simp add: linorder_not_less [symmetric], auto) 
13449  1079 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1080 
lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k > m \<le> n)" 
24438  1081 
by (simp add: linorder_not_less [symmetric], auto) 
13449  1082 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

1083 
lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n  (k = (0::nat)))" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

1084 
apply (cut_tac less_linear, safe, auto simp add: neq0_conv) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

1085 
apply (drule mult_less_mono1, assumption, simp)+ 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

1086 
done 
13449  1087 

1088 
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n  (k = (0::nat)))" 

24438  1089 
by (simp add: mult_commute [of k]) 
13449  1090 

1091 
lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)" 

24438  1092 
by (subst mult_less_cancel1) simp 
13449  1093 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1094 
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" 
24438  1095 
by (subst mult_le_cancel1) simp 
13449  1096 

1097 
lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)" 

24438  1098 
by (subst mult_cancel1) simp 
13449  1099 

1100 
text {* Lemma for @{text gcd} *} 

1101 
lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1  m = 0" 

1102 
apply (drule sym) 

1103 
apply (rule disjCI) 

1104 
apply (rule nat_less_cases, erule_tac [2] _) 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

1105 
apply (fastsimp elim!: less_SucE) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset

1106 
apply (auto simp add: neq0_conv dest: mult_less_mono2) 
13449  1107 
done 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

1108 

20588  1109 

24995  1110 
subsection {* size of a datatype value *} 
1111 

1112 
class size = type + 

1113 
fixes size :: "'a \<Rightarrow> nat" 

1114 

1115 
use "Tools/function_package/size.ML" 

1116 

1117 
setup Size.setup 

1118 

1119 
lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n" 

1120 
by (induct n) simp_all 

1121 

1122 
lemma size_bool [code func]: 

1123 
"size (b\<Colon>bool) = 0" by (cases b) auto 

1124 

1125 
declare "*.size" [noatp] 

1126 

1127 

18702  1128 
subsection {* Code generator setup *} 
1129 

22718  1130 
lemma one_is_Suc_zero [code inline]: "1 = Suc 0" 
24438  1131 
by simp 
20355  1132 

20588  1133 
instance nat :: eq .. 
1134 

1135 
lemma [code func]: 

22718  1136 
"(0\<Colon>nat) = 0 \<longleftrightarrow> True" 
1137 
"Suc n = Suc m \<longleftrightarrow> n = m" 

1138 
"Suc n = 0 \<longleftrightarrow> False" 

1139 
"0 = Suc m \<longleftrightarrow> False" 

24438  1140 
by auto 
20588  1141 

1142 
lemma [code func]: 

22718  1143 
"(0\<Colon>nat) \<le> m \<longleftrightarrow> True" 
1144 
"Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" 

1145 
"(n\<Colon>nat) < 0 \<longleftrightarrow> False" 

1146 
"(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m" 

22348  1147 
using Suc_le_eq less_Suc_eq_le by simp_all 
20588  1148 

21243  1149 

24196  1150 
subsection{*Embedding of the Naturals into any 
1151 
@{text semiring_1}: @{term of_nat}*} 

1152 

1153 
context semiring_1 

1154 
begin 

1155 

1156 
definition 

25062  1157 
of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)" 
24196  1158 

1159 
end 

1160 

21243  1161 
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} 
1162 

22845  1163 
lemma subst_equals: 
1164 
assumes 1: "t = s" and 2: "u = t" 

1165 
shows "u = s" 

1166 
using 2 1 by (rule trans) 

1167 

24196  1168 

21243  1169 
use "arith_data.ML" 
24091  1170 
declaration {* K arith_data_setup *} 
1171 

1172 
use "Tools/lin_arith.ML" 

1173 
declaration {* K LinArith.setup *} 

1174 

21243  1175 

1176 
text{*The following proofs may rely on the arithmetic proof procedures.*} 

1177 

1178 
lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)" 

24438  1179 
by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) 
21243  1180 

1181 
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)" 

24438  1182 
by (simp add: less_eq reflcl_trancl [symmetric] del: reflcl_trancl, arith) 
21243  1183 

1184 
lemma nat_diff_split: 

22718  1185 
"P(a  b::nat) = ((a<b > P 0) & (ALL d. a = b + d > P d))" 
21243  1186 
 {* elimination of @{text } on @{text nat} *} 
24438  1187 
by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2]) 
21243  1188 

1189 
lemma nat_diff_split_asm: 

1190 
"P(a  b::nat) = (~ (a < b & ~ P 0  (EX d. a = b + d & ~ P d)))" 

1191 
 {* elimination of @{text } on @{text nat} in assumptions *} 

24438  1192 
by (simp split: nat_diff_split) 
21243  1193 

1194 
lemmas [arith_split] = nat_diff_split split_min split_max 

1195 

1196 

1197 
lemma le_square: "m \<le> m * (m::nat)" 

24438  1198 
by (induct m) auto 
21243  1199 

1200 
lemma le_cube: "(m::nat) \<le> m * (m * m)" 

24438  1201 
by (induct m) auto 
21243  1202 

1203 

1204 
text{*Subtraction laws, mostly by Clemens Ballarin*} 

1205 

1206 
lemma diff_less_mono: "[ a < (b::nat); c \<le> a ] ==> ac < bc" 

24438  1207 
by arith 
21243  1208 

1209 
lemma less_diff_conv: "(i < jk) = (i+k < (j::nat))" 

24438  1210 
by arith 
21243  1211 

1212 
lemma le_diff_conv: "(jk \<le> (i::nat)) = (j \<le> i+k)" 

24438  1213 
by arith 
21243  1214 

1215 
lemma le_diff_conv2: "k \<le> j ==> (i \<le> jk) = (i+k \<le> (j::nat))" 

24438  1216 
by arith 
21243  1217 

1218 
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n  (n  i) = i" 

24438  1219 
by arith 
21243  1220 

1221 
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m  k" 

24438  1222 
by arith 
21243  1223 

1224 
(*Replaces the previous diff_less and le_diff_less, which had the stronger 

1225 
second premise n\<le>m*) 

1226 
lemma diff_less[simp]: "!!m::nat. [ 0<n; 0<m ] ==> m  n < m" 

24438  1227 
by arith 
21243  1228 

1229 

1230 
(** Simplification of relational expressions involving subtraction **) 

1231 

1232 
lemma diff_diff_eq: "[ k \<le> m; k \<le> (n::nat) ] ==> ((mk)  (nk)) = (mn)" 

24438  1233 
by (simp split add: nat_diff_split) 
21243  1234 

1235 
lemma eq_diff_iff: "[ k \<le> m; k \<le> (n::nat) ] ==> (mk = nk) = (m=n)" 

24438  1236 
by (auto split add: nat_diff_split) 
21243  1237 

1238 
lemma less_diff_iff: "[ k \<le> m; k \<le> (n::nat) ] ==> (mk < nk) = (m<n)" 

24438  1239 
by (auto split add: nat_diff_split) 
21243  1240 

1241 
lemma le_diff_iff: "[ k \<le> m; k \<le> (n::nat) ] ==> (mk \<le> nk) = (m\<le>n)" 

24438  1242 
by (auto split add: nat_diff_split) 
21243  1243 

1244 

1245 
text{*(Anti)Monotonicity of subtraction  by Stephan Merz*} 

1246 

1247 
(* Monotonicity of subtraction in first argument *) 

1248 
lemma diff_le_mono: "m \<le> (n::nat) ==> (ml) \<le> (nl)" 

24438  1249 
by (simp split add: nat_diff_split) 
21243  1250 

1251 
lemma diff_le_mono2: "m \<le> (n::nat) ==> (ln) \<le> (lm)" 

24438  1252 
by (simp split add: nat_diff_split) 
21243  1253 

1254 
lemma diff_less_mono2: "[ m < (n::nat); m<l ] ==> (ln) < (lm)" 

24438  1255 
by (simp split add: nat_diff_split) 
21243  1256 

1257 
lemma diffs0_imp_equal: "!!m::nat. [ mn = 0; nm = 0 ] ==> m=n" 

24438  1258 
by (simp split add: nat_diff_split) 
21243  1259 

1260 
text{*Lemmas for ex/Factorization*} 

1261 

1262 
lemma one_less_mult: "[ Suc 0 < n; Suc 0 < m ] ==> Suc 0 < m*n" 

24438  1263 
by (cases m) auto 
21243  1264 

1265 
lemma n_less_m_mult_n: "[ Suc 0 < n; Suc 0 < m ] ==> n<m*n" 

24438  1266 
by (cases m) auto 
21243  1267 

1268 
lemma n_less_n_mult_m: "[ Suc 0 < n; Suc 0 < m ] ==> n<n*m" 

24438  1269 
by (cases m) auto 
21243  1270 

23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1271 
text {* Specialized induction principles that work "backwards": *} 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1272 

3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1273 
lemma inc_induct[consumes 1, case_names base step]: 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1274 
assumes less: "i <= j" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1275 
assumes base: "P j" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1276 
assumes step: "!!i. [ i < j; P (Suc i) ] ==> P i" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1277 
shows "P i" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1278 
using less 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1279 
proof (induct d=="j  i" arbitrary: i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1280 
case (0 i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1281 
hence "i = j" by simp 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1282 
with base show ?case by simp 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1283 
next 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1284 
case (Suc d i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1285 
hence "i < j" "P (Suc i)" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1286 
by simp_all 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1287 
thus "P i" by (rule step) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1288 
qed 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1289 

3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1290 
lemma strict_inc_induct[consumes 1, case_names base step]: 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1291 
assumes less: "i < j" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1292 
assumes base: "!!i. j = Suc i ==> P i" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1293 
assumes step: "!!i. [ i < j; P (Suc i) ] ==> P i" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1294 
shows "P i" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1295 
using less 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1296 
proof (induct d=="j  i  1" arbitrary: i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1297 
case (0 i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1298 
with `i < j` have "j = Suc i" by simp 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1299 
with base show ?case by simp 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1300 
next 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1301 
case (Suc d i) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1302 
hence "i < j" "P (Suc i)" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1303 
by simp_all 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1304 
thus "P i" by (rule step) 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1305 
qed 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1306 

3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1307 
lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k  i)" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1308 
using inc_induct[of "k  i" k P, simplified] by blast 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1309 

3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1310 
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" 
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset

1311 
using inc_induct[of 0 k P] by blast 
21243  1312 

1313 
text{*Rewriting to pull differences out*} 

1314 

1315 
lemma diff_diff_right [simp]: "k\<le>j > i  (j  k) = i + (k::nat)  j" 

24438  1316 
by arith 
21243  1317 

1318 
lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m  Suc (j  k) = m + k  Suc j" 

24438  1319 
by arith 
21243  1320 

1321 
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j  k)  m = Suc j  (k + m)" 

24438  1322 
by arith 
21243  1323 

1324 
(*The others are 

1325 
i  j  k = i  (j + k), 

1326 
k \<le> j ==> j  k + i = j + i  k, 

1327 
k \<le> j ==> i + (j  k) = i + j  k *) 

1328 
lemmas add_diff_assoc = diff_add_assoc [symmetric] 

1329 
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] 

1330 
declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp] 

1331 

1332 
text{*At present we prove no analogue of @{text not_less_Least} or @{text 

1333 
Least_Suc}, since there appears to be no need.*} 

1334 

22718  1335 

1336 
subsection{*Embedding of the Naturals into any 

23276
a70934b63910
generalize of_nat and related constants to class semiring_1
huffman
parents:
23263
diff
changeset

1337 
@{text semiring_1}: @{term of_nat}*} 
21243
