author  haftmann 
Mon, 21 Jan 2008 08:43:27 +0100  
changeset 25928  042e877d9841 
parent 25690  5226396bf261 
child 26072  f65a7fa2da6c 
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 

25510  57 
instantiation nat :: zero 
58 
begin 

59 

60 
definition Zero_nat_def [code func del]: 

61 
"0 = Abs_Nat Zero_Rep" 

62 

63 
instance .. 

64 

65 
end 

24995  66 

13449  67 
defs 
18648  68 
Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" 
22718  69 

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

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

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

13449  75 
done 
76 

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

77 
lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0" 
23740  78 
by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI 
22718  79 
Suc_Rep_not_Zero_Rep) 
13449  80 

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

81 
lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m" 
13449  82 
by (rule not_sym, rule Suc_not_Zero not_sym) 
83 

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

84 
lemma inj_Suc[simp]: "inj_on Suc N" 
23740  85 
by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI 
22718  86 
inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) 
13449  87 

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

15413  89 
by (rule inj_Suc [THEN inj_eq]) 
13449  90 

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

91 
rep_datatype nat 
13449  92 
distinct Suc_not_Zero Zero_not_Suc 
93 
inject Suc_Suc_eq 

21411  94 
induction nat_induct 
95 

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

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

13449  98 

21672  99 
lemmas nat_rec_0 = nat.recs(1) 
100 
and nat_rec_Suc = nat.recs(2) 

101 

102 
lemmas nat_case_0 = nat.cases(1) 

103 
and nat_case_Suc = nat.cases(2) 

104 

24995  105 

106 
text {* Injectiveness and distinctness lemmas *} 

107 

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

25162  109 
by (rule notE, rule Suc_not_Zero) 
24995  110 

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

25162  112 
by (rule Suc_neq_Zero, erule sym) 
24995  113 

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

25162  115 
by (rule inj_Suc [THEN injD]) 
24995  116 

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

25162  118 
by auto 
24995  119 

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

120 
lemma n_not_Suc_n: "n \<noteq> Suc n" 
25162  121 
by (induct n) simp_all 
13449  122 

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

123 
lemma Suc_n_not_n: "Suc t \<noteq> t" 
25162  124 
by (rule not_sym, rule n_not_Suc_n) 
13449  125 

24995  126 

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

129 

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

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

14208  132 
apply (rule_tac x = m in spec) 
15251  133 
apply (induct n) 
13449  134 
prefer 2 
135 
apply (rule allI) 

17589  136 
apply (induct_tac x, iprover+) 
13449  137 
done 
138 

24995  139 

140 
subsection {* Arithmetic operators *} 

141 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

142 
instantiation nat :: "{one, plus, minus, times}" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

143 
begin 
24995  144 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

145 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

146 
One_nat_def [simp]: "1 = Suc 0" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

147 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

148 
primrec plus_nat 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

149 
where 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

150 
add_0: "0 + n = (n\<Colon>nat)" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

151 
 add_Suc: "Suc m + n = Suc (m + n)" 
24995  152 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

153 
primrec minus_nat 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

154 
where 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

155 
diff_0: "m  0 = (m\<Colon>nat)" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

156 
 diff_Suc: "m  Suc n = (case m  n of 0 => 0  Suc k => k)" 
24995  157 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

158 
primrec times_nat 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

159 
where 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

160 
mult_0: "0 * n = (0\<Colon>nat)" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

161 
 mult_Suc: "Suc m * n = n + (m * n)" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

162 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

163 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

164 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

165 
end 
24995  166 

167 

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

169 

170 
definition 

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

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

173 

25510  174 
instantiation nat :: ord 
175 
begin 

176 

177 
definition 

178 
less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+" 

24995  179 

25510  180 
definition 
181 
le_def [code func del]: "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m" 

182 

183 
instance .. 

184 

185 
end 

13449  186 

187 
lemma wf_pred_nat: "wf pred_nat" 

14208  188 
apply (unfold wf_def pred_nat_def, clarify) 
189 
apply (induct_tac x, blast+) 

13449  190 
done 
191 

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

193 
apply (unfold less_def) 

14208  194 
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast) 
13449  195 
done 
196 

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

198 
apply (unfold less_def) 

199 
apply (rule refl) 

200 
done 

201 

202 
subsubsection {* Introduction properties *} 

203 

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

205 
apply (unfold less_def) 

14208  206 
apply (rule trans_trancl [THEN transD], assumption+) 
13449  207 
done 
208 

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

210 
apply (unfold less_def pred_nat_def) 

211 
apply (simp add: r_into_trancl) 

212 
done 

213 

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

14208  215 
apply (rule less_trans, assumption) 
13449  216 
apply (rule lessI) 
217 
done 

218 

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

220 
apply (induct n) 

221 
apply (rule lessI) 

222 
apply (erule less_trans) 

223 
apply (rule lessI) 

224 
done 

225 

226 
subsubsection {* Elimination properties *} 

227 

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

229 
apply (unfold less_def) 

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

231 
done 

232 

233 
lemma less_asym: 

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

235 
apply (rule contrapos_np) 

236 
apply (rule less_not_sym) 

237 
apply (rule h1) 

238 
apply (erule h2) 

239 
done 

240 

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

242 
apply (unfold less_def) 

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

244 
done 

245 

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

25162  247 
by (rule notE, rule less_not_refl) 
13449  248 

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

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

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

251 
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t" 
25162  252 
by (rule not_sym, rule less_not_refl2) 
13449  253 

254 
lemma lessE: 

255 
assumes major: "i < k" 

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

257 
shows P 

14208  258 
apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all) 
13449  259 
apply (erule p1) 
260 
apply (rule p2) 

14208  261 
apply (simp add: less_def pred_nat_def, assumption) 
13449  262 
done 
263 

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

25162  265 
by (blast elim: lessE) 
13449  266 

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

25162  268 
by (rule notE, rule not_less0) 
13449  269 

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

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

272 
apply (rule major [THEN lessE]) 

14208  273 
apply (rule eq, blast) 
274 
apply (rule less, blast) 

13449  275 
done 
276 

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

25162  278 
by (blast elim!: less_SucE intro: less_trans) 
13449  279 

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

280 
lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)" 
25162  281 
by (simp add: less_Suc_eq) 
13449  282 

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

25162  284 
by (simp add: less_Suc_eq) 
13449  285 

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

25162  287 
by (induct n) (fast elim: less_trans lessE)+ 
13449  288 

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

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

15251  291 
apply (induct m) 
292 
apply (induct n) 

13449  293 
apply (rule refl [THEN disjI1, THEN disjI2]) 
294 
apply (rule zero_less_Suc [THEN disjI1]) 

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

296 
done 

297 

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

22718  300 
apply(simp only:less_Suc_eq) 
301 
apply blast 

302 
done 

14302  303 

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

304 
lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n  n < m)" 
13449  305 
using less_linear by blast 
306 

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

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

309 
shows "P n m" 

310 
apply (rule less_linear [THEN disjE]) 

311 
apply (erule_tac [2] disjE) 

312 
apply (erule lessCase) 

313 
apply (erule sym [THEN eqCase]) 

314 
apply (erule major) 

315 
done 

316 

317 

318 
subsubsection {* Inductive (?) properties *} 

319 

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

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

323 
done 

324 

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

326 
apply (induct n) 

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

328 
done 

329 

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

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

332 
apply (rule major [THEN lessE]) 

333 
apply (erule lessI [THEN minor]) 

14208  334 
apply (erule Suc_lessD [THEN minor], assumption) 
13449  335 
done 
336 

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

25162  338 
by (blast elim: lessE dest: Suc_lessD) 
4104  339 

16635  340 
lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" 
13449  341 
apply (rule iffI) 
342 
apply (erule Suc_less_SucD) 

343 
apply (erule Suc_mono) 

344 
done 

345 

346 
lemma less_trans_Suc: 

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

14208  348 
apply (induct k, simp_all) 
13449  349 
apply (insert le) 
350 
apply (simp add: less_Suc_eq) 

351 
apply (blast dest: Suc_lessD) 

352 
done 

353 

354 
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m  n < m"} *} 

355 
lemma not_less_eq: "(~ m < n) = (n < Suc m)" 

25162  356 
by (induct m n rule: diff_induct) simp_all 
13449  357 

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

359 
lemma nat_less_induct: 

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

360 
assumes prem: "!!n. \<forall>m::nat. m < n > P m ==> P n" shows "P n" 
22718  361 
apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]]) 
13449  362 
apply (rule prem) 
14208  363 
apply (unfold less_def, assumption) 
13449  364 
done 
365 

14131  366 
lemmas less_induct = nat_less_induct [rule_format, case_names less] 
367 

21243  368 

24995  369 
text {* Properties of "less than or equal" *} 
13449  370 

371 
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

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

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

375 
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n" 
25162  376 
by (rule less_Suc_eq_le [THEN iffD2]) 
13449  377 

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

378 
lemma le0 [iff]: "(0::nat) \<le> n" 
22718  379 
unfolding le_def by (rule not_less0) 
13449  380 

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

381 
lemma Suc_n_not_le_n: "~ Suc n \<le> n" 
25162  382 
by (simp add: le_def) 
13449  383 

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

384 
lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)" 
25162  385 
by (induct i) (simp_all add: le_def) 
13449  386 

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

387 
lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n  m = Suc n)" 
25162  388 
by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq) 
13449  389 

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

390 
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R" 
25162  391 
by (drule le_Suc_eq [THEN iffD1], iprover+) 
13449  392 

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

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

396 
done  {* formerly called lessD *} 

397 

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

398 
lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n" 
25162  399 
by (simp add: le_def less_Suc_eq) 
13449  400 

401 
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

402 
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n" 
13449  403 
apply (simp add: le_def less_Suc_eq) 
404 
using less_linear 

405 
apply blast 

406 
done 

407 

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

408 
lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)" 
25162  409 
by (blast intro: Suc_leI Suc_le_lessD) 
13449  410 

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

411 
lemma le_SucI: "m \<le> n ==> m \<le> Suc n" 
25162  412 
by (unfold le_def) (blast dest: Suc_lessD) 
13449  413 

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

414 
lemma less_imp_le: "m < n ==> m \<le> (n::nat)" 
25162  415 
by (unfold le_def) (blast elim: less_asym) 
13449  416 

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

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

420 

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

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

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

423 
lemma le_imp_less_or_eq: "m \<le> n ==> m < n  m = (n::nat)" 
22718  424 
unfolding le_def 
13449  425 
using less_linear 
22718  426 
by (blast elim: less_irrefl less_asym) 
13449  427 

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

428 
lemma less_or_eq_imp_le: "m < n  m = n ==> m \<le> (n::nat)" 
22718  429 
unfolding le_def 
13449  430 
using less_linear 
22718  431 
by (blast elim!: less_irrefl elim: less_asym) 
13449  432 

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

433 
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n  m=n)" 
25162  434 
by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq) 
13449  435 

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

437 
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n" 
25162  438 
by (rule less_or_eq_imp_le) (rule disjI2) 
13449  439 

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

440 
lemma le_refl: "n \<le> (n::nat)" 
25162  441 
by (simp add: le_eq_less_or_eq) 
13449  442 

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

443 
lemma le_less_trans: "[ i \<le> j; j < k ] ==> i < (k::nat)" 
25162  444 
by (blast dest!: le_imp_less_or_eq intro: less_trans) 
13449  445 

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

446 
lemma less_le_trans: "[ i < j; j \<le> k ] ==> i < (k::nat)" 
25162  447 
by (blast dest!: le_imp_less_or_eq intro: less_trans) 
13449  448 

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

449 
lemma le_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> (k::nat)" 
25162  450 
by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) 
13449  451 

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

452 
lemma le_anti_sym: "[ m \<le> n; n \<le> m ] ==> m = (n::nat)" 
25162  453 
by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) 
13449  454 

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

455 
lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)" 
25162  456 
by (simp add: le_simps) 
13449  457 

458 
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

459 
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)" 
25162  460 
by (simp add: le_def nat_neq_iff) (blast elim!: less_asym) 
13449  461 

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

462 
lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n" 
25162  463 
by (rule iffD2, rule nat_less_le, rule conjI) 
13449  464 

465 
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

466 
lemma nat_le_linear: "(m::nat) \<le> n  n \<le> m" 
13449  467 
apply (simp add: le_eq_less_or_eq) 
22718  468 
using less_linear by blast 
13449  469 

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

471 

22318  472 
instance nat :: wellorder 
14691  473 
by intro_classes 
474 
(assumption  

475 
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

476 

22718  477 
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 
15921  478 

13449  479 
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)" 
25162  480 
by (blast elim!: less_SucE) 
13449  481 

482 
text {* 

483 
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

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

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

487 
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)" 
25162  488 
by (rule not_less_less_Suc_eq, rule leD) 
13449  489 

490 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

491 

492 

493 
text {* 

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

13449  496 
but via @{text reorient_simproc} in Bin 
497 
*} 

498 

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

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

25162  501 
by auto 
13449  502 

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

25162  504 
by auto 
13449  505 

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

507 
NOTE USE OF @{text "=="} *} 
13449  508 
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c" 
25162  509 
by simp 
13449  510 

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

25162  512 
by simp 
13449  513 

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

514 
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m" 
25162  515 
by (cases n) simp_all 
516 

517 
lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m" 

518 
by (cases n) simp_all 

13449  519 

22718  520 
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0" 
25162  521 
by (cases n) simp_all 
13449  522 

25162  523 
lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)" 
524 
by (cases n) simp_all 

25140  525 

13449  526 
text {* This theorem is useful with @{text blast} *} 
527 
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n" 

25162  528 
by (rule neq0_conv[THEN iffD1], iprover) 
13449  529 

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

530 
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" 
25162  531 
by (fast intro: not0_implies_Suc) 
13449  532 

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

533 
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

534 
using neq0_conv by blast 
13449  535 

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

536 
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" 
25162  537 
by (induct m') simp_all 
13449  538 

539 
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

540 
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0  (\<exists>j. m = Suc j & j < n))" 
25162  541 
by (cases m) simp_all 
13449  542 

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

543 
lemma nat_induct2: "[P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))] ==> P n" 
13449  544 
apply (rule nat_less_induct) 
545 
apply (case_tac n) 

546 
apply (case_tac [2] nat) 

547 
apply (blast intro: less_trans)+ 

548 
done 

549 

21243  550 

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

551 
subsection {* @{text LEAST} theorems for type @{typ nat}*} 
13449  552 

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

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

554 
"[ P n; ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" 
14208  555 
apply (case_tac "n", auto) 
13449  556 
apply (frule LeastI) 
557 
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

558 
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 
13449  559 
apply (erule_tac [2] Least_le) 
14208  560 
apply (case_tac "LEAST x. P x", auto) 
13449  561 
apply (drule_tac P = "%x. P (Suc x) " in Least_le) 
562 
apply (blast intro: order_antisym) 

563 
done 

564 

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

565 
lemma Least_Suc2: 
25162  566 
"[P n; Q m; ~P 0; !k. P (Suc k) = Q k] ==> Least P = Suc (Least Q)" 
567 
by (erule (1) Least_Suc [THEN ssubst], simp) 

13449  568 

569 

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

571 

25076  572 
lemma mono_Suc: "mono Suc" 
25162  573 
by (rule monoI) simp 
25076  574 

13449  575 
lemma min_0L [simp]: "min 0 n = (0::nat)" 
25162  576 
by (rule min_leastL) simp 
13449  577 

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

25162  579 
by (rule min_leastR) simp 
13449  580 

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

25162  582 
by (simp add: mono_Suc min_of_mono) 
13449  583 

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

25162  586 
by (simp split: nat.split) 
22191  587 

588 
lemma min_Suc2: 

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

25162  590 
by (simp split: nat.split) 
22191  591 

13449  592 
lemma max_0L [simp]: "max 0 n = (n::nat)" 
25162  593 
by (rule max_leastL) simp 
13449  594 

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

25162  596 
by (rule max_leastR) simp 
13449  597 

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

25162  599 
by (simp add: mono_Suc max_of_mono) 
13449  600 

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

25162  603 
by (simp split: nat.split) 
22191  604 

605 
lemma max_Suc2: 

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

25162  607 
by (simp split: nat.split) 
22191  608 

13449  609 

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

611 

612 
text {* Difference *} 

613 

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

614 
lemma diff_0_eq_0 [simp, code]: "0  n = (0::nat)" 
25162  615 
by (induct n) simp_all 
13449  616 

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

617 
lemma diff_Suc_Suc [simp, code]: "Suc(m)  Suc(n) = m  n" 
25162  618 
by (induct n) simp_all 
13449  619 

620 

621 
text {* 

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

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

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

625 
*} 

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

627 
by (simp split add: nat.split) 
13449  628 

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

629 
declare diff_Suc [simp del, code del] 
13449  630 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

631 
lemma [code]: 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

632 
"(0\<Colon>nat) \<le> m \<longleftrightarrow> True" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

633 
"Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

634 
"(n\<Colon>nat) < 0 \<longleftrightarrow> False" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

635 
"(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

636 
using Suc_le_eq less_Suc_eq_le by simp_all 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

637 

13449  638 

639 
subsection {* Addition *} 

640 

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

25162  642 
by (induct m) simp_all 
13449  643 

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

25162  645 
by (induct m) simp_all 
13449  646 

19890  647 
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" 
25162  648 
by simp 
14193
30e41f63712e
Improved efficiency of code generated for + and 
berghofe
parents:
14131
diff
changeset

649 

13449  650 

651 
text {* Associative law for addition *} 

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

652 
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" 
25162  653 
by (induct m) simp_all 
13449  654 

655 
text {* Commutative law for addition *} 

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

656 
lemma nat_add_commute: "m + n = n + (m::nat)" 
25162  657 
by (induct m) simp_all 
13449  658 

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

659 
lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)" 
13449  660 
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

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

662 
apply (rule nat_add_commute) 
13449  663 
done 
664 

14331  665 
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" 
25162  666 
by (induct k) simp_all 
13449  667 

14331  668 
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" 
25162  669 
by (induct k) simp_all 
13449  670 

14331  671 
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))" 
25162  672 
by (induct k) simp_all 
13449  673 

14331  674 
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" 
25162  675 
by (induct k) simp_all 
13449  676 

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

678 

22718  679 
lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)" 
25162  680 
by (cases m) simp_all 
13449  681 

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

25162  683 
by (cases m) simp_all 
13449  684 

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

25162  686 
by (rule trans, rule eq_commute, rule add_is_1) 
13449  687 

25162  688 
lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0  n>0)" 
689 
by(auto dest:gr0_implies_Suc) 

13449  690 

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

692 
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

693 
apply (simp add: nat_add_assoc del: add_0_right) 
13449  694 
done 
695 

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

696 
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" 
22718  697 
apply (induct k) 
698 
apply simp 

699 
apply(drule comp_inj_on[OF _ inj_Suc]) 

700 
apply (simp add:o_def) 

701 
done 

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

702 

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

703 

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

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

705 

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

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

707 
lemma mult_0_right [simp]: "(m::nat) * 0 = 0" 
25162  708 
by (induct m) simp_all 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

709 

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

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

711 
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" 
25162  712 
by (induct m) (simp_all add: nat_add_left_commute) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

713 

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

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

715 
lemma nat_mult_commute: "m * n = n * (m::nat)" 
25162  716 
by (induct m) simp_all 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

717 

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

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

719 
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)" 
25162  720 
by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

721 

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

722 
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)" 
25162  723 
by (induct m) (simp_all add: nat_add_assoc) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

724 

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

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

726 
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" 
25162  727 
by (induct m) (simp_all add: add_mult_distrib) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

728 

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

729 

14740  730 
text{*The naturals form a @{text comm_semiring_1_cancel}*} 
14738  731 
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

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

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

734 
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

735 
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

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

737 
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

738 
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

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

740 
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

741 
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

742 
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

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

744 

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

745 
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0  n=0)" 
15251  746 
apply (induct m) 
22718  747 
apply (induct_tac [2] n) 
748 
apply simp_all 

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

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

750 

21243  751 

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

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

753 

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

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

755 
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)" 
25162  756 
by (induct k) simp_all 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

757 

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

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

759 
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

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

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

763 

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

764 
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

765 
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

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

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

769 
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

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

771 

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

772 
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

773 
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

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

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

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

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

778 

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

779 

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

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

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

784 
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

785 
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

786 
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

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

788 

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

789 
lemma nat_mult_1: "(1::nat) * n = n" 
25162  790 
by simp 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

791 

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

792 
lemma nat_mult_1_right: "n * (1::nat) = n" 
25162  793 
by simp 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

794 

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

795 

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

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

797 

19870  798 
text{*An induction rule for estabilishing binary relations*} 
22718  799 
lemma less_Suc_induct: 
19870  800 
assumes less: "i < j" 
801 
and step: "!!i. P i (Suc i)" 

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

803 
shows "P i j" 

804 
proof  

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

19870  807 
proof (induct k) 
22718  808 
case 0 
809 
show ?case by (simp add: step) 

19870  810 
next 
811 
case (Suc k) 

22718  812 
thus ?case by (auto intro: assms) 
19870  813 
qed 
22718  814 
thus "P i j" by (simp add: j) 
19870  815 
qed 
816 

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

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

820 
\begin{itemize} 

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

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

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

824 
\end{itemize} *} 

825 

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

829 

24523  830 
text{* A compact version without explicit base case: *} 
831 
lemma infinite_descent: 

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

833 
by (induct n rule: less_induct, auto) 

834 

24438  835 

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

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

838 
\begin{itemize} 

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

840 
\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)$. 

841 
\end{itemize} 

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

25482  843 
corollary infinite_descent0_measure [case_names 0 smaller]: 
844 
assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x" 

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

846 
shows "P x" 

24438  847 
proof  
848 
obtain n where "n = V x" by auto 

25482  849 
moreover have "\<And>x. V x = n \<Longrightarrow> P x" 
24523  850 
proof (induct n rule: infinite_descent0) 
24438  851 
case 0  "i.e. $V(x) = 0$" 
25482  852 
with A0 show "P x" by auto 
24438  853 
next  "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" 
854 
case (smaller n) 

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

25482  856 
with A1 obtain y where "V y < V x \<and> \<not> P y" by auto 
24438  857 
with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto 
858 
thus ?case by auto 

859 
qed 

860 
ultimately show "P x" by auto 

861 
qed 

19870  862 

24523  863 
text{* Again, without explicit base case: *} 
864 
lemma infinite_descent_measure: 

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

866 
proof  

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

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

869 
proof (induct n rule: infinite_descent, auto) 

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

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

872 
qed 

873 
ultimately show "P x" by auto 

874 
qed 

875 

876 

877 

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

878 
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

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

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

883 

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

884 

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

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

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

888 

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

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

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

892 

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

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

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

896 
lemma le_add1: "n \<le> ((n + m)::nat)" 
24438  897 
by (simp add: add_commute, rule le_add2) 
13449  898 

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

24438  900 
by (rule le_less_trans, rule le_add1, rule lessI) 
13449  901 

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

24438  903 
by (rule le_less_trans, rule le_add2, rule lessI) 
13449  904 

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

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

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

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

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

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

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

24438  915 
by (rule less_le_trans, assumption, rule le_add1) 
13449  916 

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

24438  918 
by (rule less_le_trans, assumption, rule le_add2) 
13449  919 

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

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

923 
done 

13449  924 

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

24438  926 
apply (rule notI) 
927 
apply (erule add_lessD1 [THEN less_irrefl]) 

928 
done 

13449  929 

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

24438  931 
by (simp add: add_commute not_add_less1) 
13449  932 

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

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

936 
done 

13449  937 

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

938 
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" 
24438  939 
apply (simp add: add_commute) 
940 
apply (erule add_leD1) 

941 
done 

13449  942 

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

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

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

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

24438  948 
by (force simp del: add_Suc_right 
13449  949 
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) 
950 

951 

952 
subsection {* Difference *} 

953 

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

24438  955 
by (induct m) simp_all 
13449  956 

957 
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

958 
if @{term "n \<le> m"} then @{term "n + (m  n) = m"}. *} 
13449  959 
lemma add_diff_inverse: "~ m < n ==> n + (m  n) = (m::nat)" 
24438  960 
by (induct m n rule: diff_induct) simp_all 
13449  961 

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

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

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

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

968 

969 
subsection {* More results about difference *} 

970 

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

971 
lemma Suc_diff_le: "n \<le> m ==> Suc m  n = Suc (m  n)" 
24438  972 
by (induct m n rule: diff_induct) simp_all 
13449  973 

974 
lemma diff_less_Suc: "m  n < Suc m" 

24438  975 
apply (induct m n rule: diff_induct) 
976 
apply (erule_tac [3] less_SucE) 

977 
apply (simp_all add: less_Suc_eq) 

978 
done 

13449  979 

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

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

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

24438  984 
by (rule le_less_trans, rule diff_le_self) 
13449  985 

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

24438  987 
by (induct i j rule: diff_induct) simp_all 
13449  988 

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

24438  990 
by (simp add: diff_diff_left) 
13449  991 

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

24438  993 
by (cases n) (auto simp add: le_simps) 
13449  994 

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

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

24438  997 
by (simp add: diff_diff_left add_commute) 
13449  998 

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

999 
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j)  k = i + (j  k)" 
24438  1000 
by (induct j k rule: diff_induct) simp_all 
13449  1001 

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

1002 
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i)  k = (j  k) + i" 
24438  1003 
by (simp add: add_commute diff_add_assoc) 
13449  1004 

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

24438  1006 
by (induct n) simp_all 
13449  1007 

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

24438  1009 
by (simp add: diff_add_assoc) 
13449  1010 

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

1011 
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j  i = k) = (j = k + i)" 
24438  1012 
by (auto simp add: diff_add_inverse2) 
13449  1013 

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

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

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

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

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

24438  1021 
by (induct m n rule: diff_induct) simp_all 
13449  1022 

22718  1023 
lemma less_imp_add_positive: 
1024 
assumes "i < j" 

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

1026 
proof 

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

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

1030 

13449  1031 
lemma diff_cancel: "(k + m)  (k + n) = m  (n::nat)" 
24438  1032 
by (induct k) simp_all 
13449  1033 

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

24438  1035 
by (simp add: diff_cancel add_commute) 
13449  1036 

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

24438  1038 
by (induct n) simp_all 
13449  1039 

1040 

1041 
text {* Difference distributes over multiplication *} 

1042 

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

24438  1044 
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) 
13449  1045 

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

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

1050 
lemmas nat_distrib = 

1051 
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 

1052 

1053 

1054 
subsection {* Monotonicity of Multiplication *} 

1055 

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

1056 
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k" 
24438  1057 
by (simp add: mult_right_mono) 
13449  1058 

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

1059 
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" 
24438  1060 
by (simp add: mult_left_mono) 
13449  1061 

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

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

1063 
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" 
24438  1064 
by (simp add: mult_mono) 
13449  1065 

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

24438  1067 
by (simp add: mult_strict_right_mono) 
13449  1068 

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

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

13449  1072 
apply (induct m) 
22718  1073 
apply simp 
1074 
apply (case_tac n) 

1075 
apply simp_all 

13449  1076 
done 
1077 

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

1078 
lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)" 
13449  1079 
apply (induct m) 
22718  1080 
apply simp 
1081 
apply (case_tac n) 

1082 
apply simp_all 

13449  1083 
done 
1084 

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

22718  1086 
apply (induct m) 
1087 
apply simp 

1088 
apply (induct n) 

1089 
apply auto 

13449  1090 
done 
1091 

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

1092 
lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" 
13449  1093 
apply (rule trans) 
14208  1094 
apply (rule_tac [2] mult_eq_1_iff, fastsimp) 
13449  1095 
done 
1096 

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

1097 
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)" 
13449  1098 
apply (safe intro!: mult_less_mono1) 
14208  1099 
apply (case_tac k, auto) 
13449  1100 
apply (simp del: le_0_eq add: linorder_not_le [symmetric]) 
1101 
apply (blast intro: mult_le_mono1) 

1102 
done 

1103 

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

24438  1105 
by (simp add: mult_commute [of k]) 
13449  1106 

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

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

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

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

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

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

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

1116 
done 
13449  1117 

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

24438  1119 
by (simp add: mult_commute [of k]) 
13449  1120 

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

24438  1122 
by (subst mult_less_cancel1) simp 
13449  1123 

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

1124 
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" 
24438  1125 
by (subst mult_le_cancel1) simp 
13449  1126 

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

24438  1128 
by (subst mult_cancel1) simp 
13449  1129 

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

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

1132 
apply (drule sym) 

1133 
apply (rule disjCI) 

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

25157  1135 
apply (drule_tac [2] mult_less_mono2) 
25162  1136 
apply (auto) 
13449  1137 
done 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

1138 

20588  1139 

24995  1140 
subsection {* size of a datatype value *} 
1141 

1142 
class size = type + 

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

1144 

1145 
use "Tools/function_package/size.ML" 

1146 

1147 
setup Size.setup 

1148 

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

25162  1150 
by (induct n) simp_all 
24995  1151 

1152 
lemma size_bool [code func]: 

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

1154 

25690  1155 
declare "prod.size" [noatp] 
24995  1156 

1157 

25193  1158 
subsection {* Embedding of the Naturals into any 
1159 
@{text semiring_1}: @{term of_nat} *} 

24196  1160 

1161 
context semiring_1 

1162 
begin 

1163 

25559  1164 
primrec 
1165 
of_nat :: "nat \<Rightarrow> 'a" 

1166 
where 

1167 
of_nat_0: "of_nat 0 = 0" 

1168 
 of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" 

25193  1169 

1170 
lemma of_nat_1 [simp]: "of_nat 1 = 1" 

1171 
by simp 

1172 

1173 
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" 

1174 
by (induct m) (simp_all add: add_ac) 

1175 

1176 
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" 

1177 
by (induct m) (simp_all add: add_ac left_distrib) 

1178 

25928  1179 
definition 
1180 
of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 

1181 
where 

1182 
[code func del]: "of_nat_aux n i = of_nat n + i" 

1183 

1184 
lemma of_nat_aux_code [code]: 

1185 
"of_nat_aux 0 i = i" 

1186 
"of_nat_aux (Suc n) i = of_nat_aux n (i + 1)"  {* tail recursive *} 

1187 
by (simp_all add: of_nat_aux_def add_ac) 

1188 

1189 
lemma of_nat_code [code]: 

1190 
"of_nat n = of_nat_aux n 0" 

1191 
by (simp add: of_nat_aux_def) 

1192 

24196  1193 
end 
1194 

25193  1195 
context ordered_semidom 
1196 
begin 

1197 

1198 
lemma zero_le_imp_of_nat: "0 \<le> of_nat m" 

1199 
apply (induct m, simp_all) 

1200 
apply (erule order_trans) 

1201 
apply (rule ord_le_eq_trans [OF _ add_commute]) 

1202 
apply (rule less_add_one [THEN less_imp_le]) 

1203 
done 

1204 

1205 
lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n" 

1206 
apply (induct m n rule: diff_induct, simp_all) 

1207 
apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force) 

1208 
done 

1209 

1210 
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n" 

1211 
apply (induct m n rule: diff_induct, simp_all) 

1212 
apply (insert zero_le_imp_of_nat) 

1213 
apply (force simp add: not_less [symmetric]) 

1214 
done 

1215 

1216 
lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n" 

1217 
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less) 

1218 

1219 
text{*Special cases where either operand is zero*} 

1220 

1221 
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n" 

1222 
by (rule of_nat_less_iff [of 0, simplified]) 

1223 

1224 
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0" 

1225 
by (rule of_nat_less_iff [of _ 0, simplified]) 

1226 

1227 
lemma of_nat_le_iff [simp]: 

1228 
"of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n" 

1229 
by (simp add: not_less [symmetric] linorder_not_less [symmetric]) 

1230 

1231 
text{*Special cases where either operand is zero*} 

1232 

1233 
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n" 

1234 
by (rule of_nat_le_iff [of 0, simplified]) 

1235 

1236 
lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0" 

1237 
by (rule of_nat_le_iff [of _ 0, simplified]) 

1238 

1239 
end 

1240 

1241 
lemma of_nat_id [simp]: "of_nat n = n" 

1242 
by (induct n) auto 

1243 

1244 
lemma of_nat_eq_id [simp]: "of_nat = id" 

1245 
by (auto simp add: expand_fun_eq) 

1246 

1247 
text{*Class for unital semirings with characteristic zero. 

1248 
Includes nonordered rings like the complex numbers.*} 

1249 

1250 
class semiring_char_0 = semiring_1 + 

1251 
assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n" 

1252 

1253 
text{*Every @{text ordered_semidom} has characteristic zero.*} 

1254 

1255 
subclass (in ordered_semidom) semiring_char_0 

1256 
by unfold_locales (simp add: eq_iff order_eq_iff) 

1257 

1258 
context semiring_char_0 

1259 
begin 

1260 

1261 
text{*Special cases where either operand is zero*} 

1262 

1263 
lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" 

1264 
by (rule of_nat_eq_iff [of 0, simplified]) 

1265 

1266 
lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" 

1267 
by (rule of_nat_eq_iff [of _ 0, simplified]) 

1268 

1269 
lemma inj_of_nat: "inj of_nat" 

1270 
by (simp add: inj_on_def) 

1271 

1272 
end 

1273 

1274 

21243  1275 
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} 
1276 

22845  1277 
lemma subst_equals: 
1278 
assumes 1: "t = s" and 2: "u = t" 

1279 
shows "u = s" 

1280 
using 2 1 by (rule trans) 

1281 

21243  1282 
use "arith_data.ML" 
24091  1283 
declaration {* K arith_data_setup *} 
1284 

1285 
use "Tools/lin_arith.ML" 

1286 
declaration {* K LinArith.setup *} 

1287 

21243  1288 

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

1290 

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

24438  1292 
by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) 
21243  1293 

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

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

1297 
lemma nat_diff_split: 

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

25193  1302 
context ring_1 
1303 
begin 

1304 

1305 
lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m  n) = of_nat m  of_nat n" 

1306 
by (simp del: of_nat_add 

1307 
add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) 

1308 

1309 
end 

1310 

1311 
lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n" 

25231  1312 
unfolding abs_if by auto 
25193  1313 

21243  1314 
lemma nat_diff_split_asm: 
25162  1315 
"P(a  b::nat) = (~ (a < b & ~ P 0  (EX d. a = b + d & ~ P d)))" 
21243  1316 
 {* elimination of @{text } on @{text nat} in assumptions *} 
24438  1317 
by (simp split: nat_diff_split) 
21243  1318 

1319 
lemmas [arith_split] = nat_diff_split split_min split_max 

1320 

1321 

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

24438  1323 
by (induct m) auto 
21243  1324 

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

24438  1326 
by (induct m) auto 
21243  1327 

1328 

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

1330 

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

24438  1332 
by arith 
21243  1333 

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

24438  1335 
by arith 
21243  1336 

1337 