author  haftmann 
Thu, 06 Dec 2007 16:36:19 +0100  
changeset 25559  f14305fb698c 
parent 25534  d0b74fdd6067 
child 25563  cab4f808f791 
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 

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

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

144 

145 
primrec 

146 
add_0: "0 + n = n" 

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

148 

149 
primrec 

150 
diff_0: "m  0 = m" 

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

152 

153 
primrec 

154 
mult_0: "0 * n = 0" 

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

156 

157 

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

159 

160 
definition 

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

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

163 

25510  164 
instantiation nat :: ord 
165 
begin 

166 

167 
definition 

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

24995  169 

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

172 

173 
instance .. 

174 

175 
end 

13449  176 

177 
lemma wf_pred_nat: "wf pred_nat" 

14208  178 
apply (unfold wf_def pred_nat_def, clarify) 
179 
apply (induct_tac x, blast+) 

13449  180 
done 
181 

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

183 
apply (unfold less_def) 

14208  184 
apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast) 
13449  185 
done 
186 

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

188 
apply (unfold less_def) 

189 
apply (rule refl) 

190 
done 

191 

192 
subsubsection {* Introduction properties *} 

193 

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

195 
apply (unfold less_def) 

14208  196 
apply (rule trans_trancl [THEN transD], assumption+) 
13449  197 
done 
198 

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

200 
apply (unfold less_def pred_nat_def) 

201 
apply (simp add: r_into_trancl) 

202 
done 

203 

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

14208  205 
apply (rule less_trans, assumption) 
13449  206 
apply (rule lessI) 
207 
done 

208 

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

210 
apply (induct n) 

211 
apply (rule lessI) 

212 
apply (erule less_trans) 

213 
apply (rule lessI) 

214 
done 

215 

216 
subsubsection {* Elimination properties *} 

217 

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

219 
apply (unfold less_def) 

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

221 
done 

222 

223 
lemma less_asym: 

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

225 
apply (rule contrapos_np) 

226 
apply (rule less_not_sym) 

227 
apply (rule h1) 

228 
apply (erule h2) 

229 
done 

230 

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

232 
apply (unfold less_def) 

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

234 
done 

235 

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

25162  237 
by (rule notE, rule less_not_refl) 
13449  238 

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

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

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

241 
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t" 
25162  242 
by (rule not_sym, rule less_not_refl2) 
13449  243 

244 
lemma lessE: 

245 
assumes major: "i < k" 

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

247 
shows P 

14208  248 
apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all) 
13449  249 
apply (erule p1) 
250 
apply (rule p2) 

14208  251 
apply (simp add: less_def pred_nat_def, assumption) 
13449  252 
done 
253 

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

25162  255 
by (blast elim: lessE) 
13449  256 

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

25162  258 
by (rule notE, rule not_less0) 
13449  259 

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

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

262 
apply (rule major [THEN lessE]) 

14208  263 
apply (rule eq, blast) 
264 
apply (rule less, blast) 

13449  265 
done 
266 

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

25162  268 
by (blast elim!: less_SucE intro: less_trans) 
13449  269 

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

270 
lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)" 
25162  271 
by (simp add: less_Suc_eq) 
13449  272 

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

25162  274 
by (simp add: less_Suc_eq) 
13449  275 

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

25162  277 
by (induct n) (fast elim: less_trans lessE)+ 
13449  278 

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

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

15251  281 
apply (induct m) 
282 
apply (induct n) 

13449  283 
apply (rule refl [THEN disjI1, THEN disjI2]) 
284 
apply (rule zero_less_Suc [THEN disjI1]) 

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

286 
done 

287 

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

22718  290 
apply(simp only:less_Suc_eq) 
291 
apply blast 

292 
done 

14302  293 

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

294 
lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n  n < m)" 
13449  295 
using less_linear by blast 
296 

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

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

299 
shows "P n m" 

300 
apply (rule less_linear [THEN disjE]) 

301 
apply (erule_tac [2] disjE) 

302 
apply (erule lessCase) 

303 
apply (erule sym [THEN eqCase]) 

304 
apply (erule major) 

305 
done 

306 

307 

308 
subsubsection {* Inductive (?) properties *} 

309 

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

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

313 
done 

314 

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

316 
apply (induct n) 

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

318 
done 

319 

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

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

322 
apply (rule major [THEN lessE]) 

323 
apply (erule lessI [THEN minor]) 

14208  324 
apply (erule Suc_lessD [THEN minor], assumption) 
13449  325 
done 
326 

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

25162  328 
by (blast elim: lessE dest: Suc_lessD) 
4104  329 

16635  330 
lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" 
13449  331 
apply (rule iffI) 
332 
apply (erule Suc_less_SucD) 

333 
apply (erule Suc_mono) 

334 
done 

335 

336 
lemma less_trans_Suc: 

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

14208  338 
apply (induct k, simp_all) 
13449  339 
apply (insert le) 
340 
apply (simp add: less_Suc_eq) 

341 
apply (blast dest: Suc_lessD) 

342 
done 

343 

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

346 

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

25162  349 
by (induct m n rule: diff_induct) simp_all 
13449  350 

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

352 
lemma nat_less_induct: 

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

353 
assumes prem: "!!n. \<forall>m::nat. m < n > P m ==> P n" shows "P n" 
22718  354 
apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]]) 
13449  355 
apply (rule prem) 
14208  356 
apply (unfold less_def, assumption) 
13449  357 
done 
358 

14131  359 
lemmas less_induct = nat_less_induct [rule_format, case_names less] 
360 

21243  361 

24995  362 
text {* Properties of "less than or equal" *} 
13449  363 

364 
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

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

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

368 
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n" 
25162  369 
by (rule less_Suc_eq_le [THEN iffD2]) 
13449  370 

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

371 
lemma le0 [iff]: "(0::nat) \<le> n" 
22718  372 
unfolding le_def by (rule not_less0) 
13449  373 

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

374 
lemma Suc_n_not_le_n: "~ Suc n \<le> n" 
25162  375 
by (simp add: le_def) 
13449  376 

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

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

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

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

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

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

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

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

389 
done  {* formerly called lessD *} 

390 

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

391 
lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n" 
25162  392 
by (simp add: le_def less_Suc_eq) 
13449  393 

394 
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

395 
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n" 
13449  396 
apply (simp add: le_def less_Suc_eq) 
397 
using less_linear 

398 
apply blast 

399 
done 

400 

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

401 
lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)" 
25162  402 
by (blast intro: Suc_leI Suc_le_lessD) 
13449  403 

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

404 
lemma le_SucI: "m \<le> n ==> m \<le> Suc n" 
25162  405 
by (unfold le_def) (blast dest: Suc_lessD) 
13449  406 

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

407 
lemma less_imp_le: "m < n ==> m \<le> (n::nat)" 
25162  408 
by (unfold le_def) (blast elim: less_asym) 
13449  409 

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

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

413 

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

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

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

416 
lemma le_imp_less_or_eq: "m \<le> n ==> m < n  m = (n::nat)" 
22718  417 
unfolding le_def 
13449  418 
using less_linear 
22718  419 
by (blast elim: less_irrefl less_asym) 
13449  420 

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

421 
lemma less_or_eq_imp_le: "m < n  m = n ==> m \<le> (n::nat)" 
22718  422 
unfolding le_def 
13449  423 
using less_linear 
22718  424 
by (blast elim!: less_irrefl elim: less_asym) 
13449  425 

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

426 
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n  m=n)" 
25162  427 
by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq) 
13449  428 

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

430 
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n" 
25162  431 
by (rule less_or_eq_imp_le) (rule disjI2) 
13449  432 

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

433 
lemma le_refl: "n \<le> (n::nat)" 
25162  434 
by (simp add: le_eq_less_or_eq) 
13449  435 

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

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

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

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

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

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

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

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

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

448 
lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)" 
25162  449 
by (simp add: le_simps) 
13449  450 

451 
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

452 
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)" 
25162  453 
by (simp add: le_def nat_neq_iff) (blast 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 le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n" 
25162  456 
by (rule iffD2, rule nat_less_le, rule conjI) 
13449  457 

458 
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

459 
lemma nat_le_linear: "(m::nat) \<le> n  n \<le> m" 
13449  460 
apply (simp add: le_eq_less_or_eq) 
22718  461 
using less_linear by blast 
13449  462 

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

464 

22318  465 
instance nat :: wellorder 
14691  466 
by intro_classes 
467 
(assumption  

468 
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

469 

22718  470 
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 
15921  471 

13449  472 
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)" 
25162  473 
by (blast elim!: less_SucE) 
13449  474 

475 
text {* 

476 
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

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

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

480 
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)" 
25162  481 
by (rule not_less_less_Suc_eq, rule leD) 
13449  482 

483 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

484 

485 

486 
text {* 

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

13449  489 
but via @{text reorient_simproc} in Bin 
490 
*} 

491 

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

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

25162  494 
by auto 
13449  495 

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

25162  497 
by auto 
13449  498 

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

500 
NOTE USE OF @{text "=="} *} 
13449  501 
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c" 
25162  502 
by simp 
13449  503 

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

25162  505 
by simp 
13449  506 

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

507 
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m" 
25162  508 
by (cases n) simp_all 
509 

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

511 
by (cases n) simp_all 

13449  512 

22718  513 
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0" 
25162  514 
by (cases n) simp_all 
13449  515 

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

25140  518 

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

25162  521 
by (rule neq0_conv[THEN iffD1], iprover) 
13449  522 

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

523 
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" 
25162  524 
by (fast intro: not0_implies_Suc) 
13449  525 

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

526 
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

527 
using neq0_conv by blast 
13449  528 

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

529 
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" 
25162  530 
by (induct m') simp_all 
13449  531 

532 
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

533 
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0  (\<exists>j. m = Suc j & j < n))" 
25162  534 
by (cases m) simp_all 
13449  535 

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

536 
lemma nat_induct2: "[P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))] ==> P n" 
13449  537 
apply (rule nat_less_induct) 
538 
apply (case_tac n) 

539 
apply (case_tac [2] nat) 

540 
apply (blast intro: less_trans)+ 

541 
done 

542 

21243  543 

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

544 
subsection {* @{text LEAST} theorems for type @{typ nat}*} 
13449  545 

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

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

547 
"[ P n; ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" 
14208  548 
apply (case_tac "n", auto) 
13449  549 
apply (frule LeastI) 
550 
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

551 
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 
13449  552 
apply (erule_tac [2] Least_le) 
14208  553 
apply (case_tac "LEAST x. P x", auto) 
13449  554 
apply (drule_tac P = "%x. P (Suc x) " in Least_le) 
555 
apply (blast intro: order_antisym) 

556 
done 

557 

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

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

13449  561 

562 

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

564 

25076  565 
lemma mono_Suc: "mono Suc" 
25162  566 
by (rule monoI) simp 
25076  567 

13449  568 
lemma min_0L [simp]: "min 0 n = (0::nat)" 
25162  569 
by (rule min_leastL) simp 
13449  570 

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

25162  572 
by (rule min_leastR) simp 
13449  573 

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

25162  575 
by (simp add: mono_Suc min_of_mono) 
13449  576 

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

25162  579 
by (simp split: nat.split) 
22191  580 

581 
lemma min_Suc2: 

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

25162  583 
by (simp split: nat.split) 
22191  584 

13449  585 
lemma max_0L [simp]: "max 0 n = (n::nat)" 
25162  586 
by (rule max_leastL) simp 
13449  587 

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

25162  589 
by (rule max_leastR) simp 
13449  590 

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

25162  592 
by (simp add: mono_Suc max_of_mono) 
13449  593 

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

25162  596 
by (simp split: nat.split) 
22191  597 

598 
lemma max_Suc2: 

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

25162  600 
by (simp split: nat.split) 
22191  601 

13449  602 

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

604 

605 
text {* Difference *} 

606 

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

607 
lemma diff_0_eq_0 [simp, code]: "0  n = (0::nat)" 
25162  608 
by (induct n) simp_all 
13449  609 

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

610 
lemma diff_Suc_Suc [simp, code]: "Suc(m)  Suc(n) = m  n" 
25162  611 
by (induct n) simp_all 
13449  612 

613 

614 
text {* 

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

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

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

618 
*} 

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

620 
by (simp split add: nat.split) 
13449  621 

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

622 
declare diff_Suc [simp del, code del] 
13449  623 

624 

625 
subsection {* Addition *} 

626 

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

25162  628 
by (induct m) simp_all 
13449  629 

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

25162  631 
by (induct m) simp_all 
13449  632 

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

635 

13449  636 

637 
text {* Associative law for addition *} 

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

638 
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" 
25162  639 
by (induct m) simp_all 
13449  640 

641 
text {* Commutative law for addition *} 

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

642 
lemma nat_add_commute: "m + n = n + (m::nat)" 
25162  643 
by (induct m) simp_all 
13449  644 

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

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

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

648 
apply (rule nat_add_commute) 
13449  649 
done 
650 

14331  651 
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" 
25162  652 
by (induct k) simp_all 
13449  653 

14331  654 
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" 
25162  655 
by (induct k) simp_all 
13449  656 

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

14331  660 
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" 
25162  661 
by (induct k) simp_all 
13449  662 

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

664 

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

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

25162  669 
by (cases m) simp_all 
13449  670 

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

25162  672 
by (rule trans, rule eq_commute, rule add_is_1) 
13449  673 

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

13449  676 

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

678 
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

679 
apply (simp add: nat_add_assoc del: add_0_right) 
13449  680 
done 
681 

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

682 
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" 
22718  683 
apply (induct k) 
684 
apply simp 

685 
apply(drule comp_inj_on[OF _ inj_Suc]) 

686 
apply (simp add:o_def) 

687 
done 

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

688 

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

689 

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

690 
subsection {* Multiplication *} 
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 
text {* right annihilation in product *} 
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

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

695 

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

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

697 
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" 
25162  698 
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

699 

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

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

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

703 

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

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

705 
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)" 
25162  706 
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

707 

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

708 
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)" 
25162  709 
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

710 

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

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

712 
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" 
25162  713 
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

714 

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

715 

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

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

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

720 
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

721 
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

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

723 
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

724 
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

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

726 
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

727 
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

728 
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

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

730 

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

731 
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0  n=0)" 
15251  732 
apply (induct m) 
22718  733 
apply (induct_tac [2] n) 
734 
apply simp_all 

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

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

736 

21243  737 

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

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

739 

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

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

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

743 

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

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

745 
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

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

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

749 

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

750 
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

751 
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

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

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

755 
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

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

759 
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

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

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

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

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

764 

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

765 

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

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

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

770 
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

771 
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

772 
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

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

774 

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

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

777 

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

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

780 

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

781 

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

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

783 

19870  784 
text{*An induction rule for estabilishing binary relations*} 
22718  785 
lemma less_Suc_induct: 
19870  786 
assumes less: "i < j" 
787 
and step: "!!i. P i (Suc i)" 

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

789 
shows "P i j" 

790 
proof  

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

19870  793 
proof (induct k) 
22718  794 
case 0 
795 
show ?case by (simp add: step) 

19870  796 
next 
797 
case (Suc k) 

22718  798 
thus ?case by (auto intro: assms) 
19870  799 
qed 
22718  800 
thus "P i j" by (simp add: j) 
19870  801 
qed 
802 

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

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

806 
\begin{itemize} 

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

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

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

810 
\end{itemize} *} 

811 

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

815 

24523  816 
text{* A compact version without explicit base case: *} 
817 
lemma infinite_descent: 

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

819 
by (induct n rule: less_induct, auto) 

820 

24438  821 

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

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

824 
\begin{itemize} 

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

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

827 
\end{itemize} 

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

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

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

832 
shows "P x" 

24438  833 
proof  
834 
obtain n where "n = V x" by auto 

25482  835 
moreover have "\<And>x. V x = n \<Longrightarrow> P x" 
24523  836 
proof (induct n rule: infinite_descent0) 
24438  837 
case 0  "i.e. $V(x) = 0$" 
25482  838 
with A0 show "P x" by auto 
24438  839 
next  "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$" 
840 
case (smaller n) 

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

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

845 
qed 

846 
ultimately show "P x" by auto 

847 
qed 

19870  848 

24523  849 
text{* Again, without explicit base case: *} 
850 
lemma infinite_descent_measure: 

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

852 
proof  

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

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

855 
proof (induct n rule: infinite_descent, auto) 

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

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

858 
qed 

859 
ultimately show "P x" by auto 

860 
qed 

861 

862 

863 

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

864 
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

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

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

869 

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

870 

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

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

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

874 

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

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

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

878 

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

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

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

882 
lemma le_add1: "n \<le> ((n + m)::nat)" 
24438  883 
by (simp add: add_commute, rule le_add2) 
13449  884 

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

24438  886 
by (rule le_less_trans, rule le_add1, rule lessI) 
13449  887 

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

24438  889 
by (rule le_less_trans, rule le_add2, rule lessI) 
13449  890 

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

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

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

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

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

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

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

24438  901 
by (rule less_le_trans, assumption, rule le_add1) 
13449  902 

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

24438  904 
by (rule less_le_trans, assumption, rule le_add2) 
13449  905 

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

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

909 
done 

13449  910 

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

24438  912 
apply (rule notI) 
913 
apply (erule add_lessD1 [THEN less_irrefl]) 

914 
done 

13449  915 

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

24438  917 
by (simp add: add_commute not_add_less1) 
13449  918 

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

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

922 
done 

13449  923 

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

924 
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" 
24438  925 
apply (simp add: add_commute) 
926 
apply (erule add_leD1) 

927 
done 

13449  928 

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

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

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

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

24438  934 
by (force simp del: add_Suc_right 
13449  935 
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) 
936 

937 

938 
subsection {* Difference *} 

939 

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

24438  941 
by (induct m) simp_all 
13449  942 

943 
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

944 
if @{term "n \<le> m"} then @{term "n + (m  n) = m"}. *} 
13449  945 
lemma add_diff_inverse: "~ m < n ==> n + (m  n) = (m::nat)" 
24438  946 
by (induct m n rule: diff_induct) simp_all 
13449  947 

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

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

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

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

954 

955 
subsection {* More results about difference *} 

956 

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

957 
lemma Suc_diff_le: "n \<le> m ==> Suc m  n = Suc (m  n)" 
24438  958 
by (induct m n rule: diff_induct) simp_all 
13449  959 

960 
lemma diff_less_Suc: "m  n < Suc m" 

24438  961 
apply (induct m n rule: diff_induct) 
962 
apply (erule_tac [3] less_SucE) 

963 
apply (simp_all add: less_Suc_eq) 

964 
done 

13449  965 

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

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

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

24438  970 
by (rule le_less_trans, rule diff_le_self) 
13449  971 

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

24438  973 
by (induct i j rule: diff_induct) simp_all 
13449  974 

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

24438  976 
by (simp add: diff_diff_left) 
13449  977 

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

24438  979 
by (cases n) (auto simp add: le_simps) 
13449  980 

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

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

24438  983 
by (simp add: diff_diff_left add_commute) 
13449  984 

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

985 
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j)  k = i + (j  k)" 
24438  986 
by (induct j k rule: diff_induct) simp_all 
13449  987 

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

988 
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i)  k = (j  k) + i" 
24438  989 
by (simp add: add_commute diff_add_assoc) 
13449  990 

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

24438  992 
by (induct n) simp_all 
13449  993 

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

24438  995 
by (simp add: diff_add_assoc) 
13449  996 

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

997 
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j  i = k) = (j = k + i)" 
24438  998 
by (auto simp add: diff_add_inverse2) 
13449  999 

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

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

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

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

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

24438  1007 
by (induct m n rule: diff_induct) simp_all 
13449  1008 

22718  1009 
lemma less_imp_add_positive: 
1010 
assumes "i < j" 

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

1012 
proof 

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

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

1016 

13449  1017 
lemma diff_cancel: "(k + m)  (k + n) = m  (n::nat)" 
24438  1018 
by (induct k) simp_all 
13449  1019 

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

24438  1021 
by (simp add: diff_cancel add_commute) 
13449  1022 

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

24438  1024 
by (induct n) simp_all 
13449  1025 

1026 

1027 
text {* Difference distributes over multiplication *} 

1028 

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

24438  1030 
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) 
13449  1031 

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

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

1036 
lemmas nat_distrib = 

1037 
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 

1038 

1039 

1040 
subsection {* Monotonicity of Multiplication *} 

1041 

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

1042 
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k" 
24438  1043 
by (simp add: mult_right_mono) 
13449  1044 

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

1045 
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" 
24438  1046 
by (simp add: mult_left_mono) 
13449  1047 

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

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

1049 
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" 
24438  1050 
by (simp add: mult_mono) 
13449  1051 

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

24438  1053 
by (simp add: mult_strict_right_mono) 
13449  1054 

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

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

13449  1058 
apply (induct m) 
22718  1059 
apply simp 
1060 
apply (case_tac n) 

1061 
apply simp_all 

13449  1062 
done 
1063 

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

1064 
lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)" 
13449  1065 
apply (induct m) 
22718  1066 
apply simp 
1067 
apply (case_tac n) 

1068 
apply simp_all 

13449  1069 
done 
1070 

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

22718  1072 
apply (induct m) 
1073 
apply simp 

1074 
apply (induct n) 

1075 
apply auto 

13449  1076 
done 
1077 

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

1078 
lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" 
13449  1079 
apply (rule trans) 
14208  1080 
apply (rule_tac [2] mult_eq_1_iff, fastsimp) 
13449  1081 
done 
1082 

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

1083 
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)" 
13449  1084 
apply (safe intro!: mult_less_mono1) 
14208  1085 
apply (case_tac k, auto) 
13449  1086 
apply (simp del: le_0_eq add: linorder_not_le [symmetric]) 
1087 
apply (blast intro: mult_le_mono1) 

1088 
done 

1089 

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

24438  1091 
by (simp add: mult_commute [of k]) 
13449  1092 

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

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

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

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

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

1099 
lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n  (k = (0::nat)))" 
25162  1100 
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

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

1102 
done 
13449  1103 

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

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

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

24438  1108 
by (subst mult_less_cancel1) simp 
13449  1109 

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

1110 
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" 
24438  1111 
by (subst mult_le_cancel1) simp 
13449  1112 

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

24438  1114 
by (subst mult_cancel1) simp 
13449  1115 

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

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

1118 
apply (drule sym) 

1119 
apply (rule disjCI) 

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

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

1124 

20588  1125 

24995  1126 
subsection {* size of a datatype value *} 
1127 

1128 
class size = type + 

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

1130 

1131 
use "Tools/function_package/size.ML" 

1132 

1133 
setup Size.setup 

1134 

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

25162  1136 
by (induct n) simp_all 
24995  1137 

1138 
lemma size_bool [code func]: 

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

1140 

1141 
declare "*.size" [noatp] 

1142 

1143 

18702  1144 
subsection {* Code generator setup *} 
1145 

20588  1146 
lemma [code func]: 
25145  1147 
"(0\<Colon>nat) \<le> m \<longleftrightarrow> True" 
1148 
"Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m" 

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

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

22348  1151 
using Suc_le_eq less_Suc_eq_le by simp_all 
20588  1152 

21243  1153 

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

24196  1156 

1157 
context semiring_1 

1158 
begin 

1159 

25559  1160 
primrec 
1161 
of_nat :: "nat \<Rightarrow> 'a" 

1162 
where 

1163 
of_nat_0: "of_nat 0 = 0" 

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

25193  1165 

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

1167 
by simp 

1168 

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

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

1171 

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

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

1174 

24196  1175 
end 
1176 

25193  1177 
context ordered_semidom 
1178 
begin 

1179 

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

1181 
apply (induct m, simp_all) 

1182 
apply (erule order_trans) 

1183 
apply (rule ord_le_eq_trans [OF _ add_commute]) 

1184 
apply (rule less_add_one [THEN less_imp_le]) 

1185 
done 

1186 

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

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

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

1190 
done 

1191 

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

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

1194 
apply (insert zero_le_imp_of_nat) 

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

1196 
done 

1197 

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

1199 
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less) 

1200 

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

1202 

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

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

1205 

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

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

1208 

1209 
lemma of_nat_le_iff [simp]: 

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

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

1212 

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

1214 

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

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

1217 

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

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

1220 

1221 
end 

1222 

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

1224 
by (induct n) auto 

1225 

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

1227 
by (auto simp add: expand_fun_eq) 

1228 

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

1230 
Includes nonordered rings like the complex numbers.*} 

1231 

1232 
class semiring_char_0 = semiring_1 + 

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

1234 

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

1236 

1237 
subclass (in ordered_semidom) semiring_char_0 

1238 
by unfold_locales (simp add: eq_iff order_eq_iff) 

1239 

1240 
context semiring_char_0 

1241 
begin 

1242 

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

1244 

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

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

1247 

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

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

1250 

1251 
lemma inj_of_nat: "inj of_nat" 

1252 
by (simp add: inj_on_def) 

1253 

1254 
end 

1255 

1256 

21243  1257 
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} 
1258 

22845  1259 
lemma subst_equals: 
1260 
assumes 1: "t = s" and 2: "u = t" 

1261 
shows "u = s" 

1262 
using 2 1 by (rule trans) 

1263 

21243  1264 
use "arith_data.ML" 
24091  1265 
declaration {* K arith_data_setup *} 
1266 

1267 
use "Tools/lin_arith.ML" 

1268 
declaration {* K LinArith.setup *} 

1269 

21243  1270 

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

1272 

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

24438  1274 
by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add) 
21243  1275 

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

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

1279 
lemma nat_diff_split: 

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

25193  1284 
context ring_1 
1285 
begin 

1286 

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

1288 
by (simp del: of_nat_add 

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

1290 

1291 
end 

1292 

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

25231  1294 
unfolding abs_if by auto 
25193  1295 

21243  1296 
lemma nat_diff_split_asm: 
25162  1297 
"P(a  b::nat) = (~ (a < b & ~ P 0  (EX d. a = b + d & ~ P d)))" 
21243  1298 
 {* elimination of @{text } on @{text nat} in assumptions *} 
24438  1299 
by (simp split: nat_diff_split) 
21243  1300 

1301 
lemmas [arith_split] = nat_diff_split split_min split_max 

1302 

1303 

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

24438  1305 
by (induct m) auto 
21243  1306 

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

24438  1308 
by (induct m) auto 
21243  1309 

1310 

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

1312 

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

24438  1314 
by arith 
21243  1315 

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

24438  1317 
by arith 
21243  1318 

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

24438  1320 
by arith 
21243  1321 

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

24438  1323 
by arith 
21243  1324 

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

24438  1326 
by arith 
21243  1327 

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

24438  1329 
by arith 
21243  1330 

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

1332 
second premise n\<le>m*) 

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

24438  1334 
by arith 
21243  1335 

1336 
