author  nipkow 
Tue, 23 Oct 2007 23:27:23 +0200  
changeset 25162  ad4d5365d9d8 
parent 25157  8b80535cd017 
child 25193  e2e1a4b00de3 
permissions  rwrr 
923  1 
(* Title: HOL/Nat.thy 
2 
ID: $Id$ 

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

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

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

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

13449  9 
header {* Natural numbers *} 
10 

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

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

16 
("arith_data.ML") 

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

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

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

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

23 

24 
typedecl ind 

25 

19573  26 
axiomatization 
27 
Zero_Rep :: ind and 

28 
Suc_Rep :: "ind => ind" 

29 
where 

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

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

13449  34 

35 
subsection {* Type nat *} 

36 

37 
text {* Type definition *} 

38 

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

13449  43 

44 
global 

45 

46 
typedef (open Nat) 

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

52 
consts 

53 
Suc :: "nat => nat" 

54 

55 
local 

56 

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

59 
lemmas [code func del] = Zero_nat_def 

60 

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

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

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

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

13449  69 
done 
70 

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

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

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

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

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

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

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

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

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

85 
rep_datatype nat 
13449  86 
distinct Suc_not_Zero Zero_not_Suc 
87 
inject Suc_Suc_eq 

21411  88 
induction nat_induct 
89 

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

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

13449  92 

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

95 

96 
lemmas nat_case_0 = nat.cases(1) 

97 
and nat_case_Suc = nat.cases(2) 

98 

24995  99 

100 
text {* Injectiveness and distinctness lemmas *} 

101 

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

25162  103 
by (rule notE, rule Suc_not_Zero) 
24995  104 

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

25162  106 
by (rule Suc_neq_Zero, erule sym) 
24995  107 

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

25162  109 
by (rule inj_Suc [THEN injD]) 
24995  110 

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

25162  112 
by auto 
24995  113 

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

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

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

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

24995  120 

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

123 

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

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

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

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

24995  133 

134 
subsection {* Arithmetic operators *} 

135 

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

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

138 

139 
primrec 

140 
add_0: "0 + n = n" 

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

142 

143 
primrec 

144 
diff_0: "m  0 = m" 

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

146 

147 
primrec 

148 
mult_0: "0 * n = 0" 

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

150 

151 

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

153 

154 
definition 

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

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

157 

158 
instance nat :: ord 

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

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

161 

162 
lemmas [code func del] = less_def le_def 

13449  163 

164 
lemma wf_pred_nat: "wf pred_nat" 

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

13449  167 
done 
168 

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

170 
apply (unfold less_def) 

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

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

175 
apply (unfold less_def) 

176 
apply (rule refl) 

177 
done 

178 

179 
subsubsection {* Introduction properties *} 

180 

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

182 
apply (unfold less_def) 

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

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

187 
apply (unfold less_def pred_nat_def) 

188 
apply (simp add: r_into_trancl) 

189 
done 

190 

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

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

195 

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

197 
apply (induct n) 

198 
apply (rule lessI) 

199 
apply (erule less_trans) 

200 
apply (rule lessI) 

201 
done 

202 

203 
subsubsection {* Elimination properties *} 

204 

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

206 
apply (unfold less_def) 

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

208 
done 

209 

210 
lemma less_asym: 

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

212 
apply (rule contrapos_np) 

213 
apply (rule less_not_sym) 

214 
apply (rule h1) 

215 
apply (erule h2) 

216 
done 

217 

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

219 
apply (unfold less_def) 

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

221 
done 

222 

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

25162  224 
by (rule notE, rule less_not_refl) 
13449  225 

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

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

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

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

231 
lemma lessE: 

232 
assumes major: "i < k" 

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

234 
shows P 

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

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

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

25162  242 
by (blast elim: lessE) 
13449  243 

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

25162  245 
by (rule notE, rule not_less0) 
13449  246 

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

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

249 
apply (rule major [THEN lessE]) 

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

13449  252 
done 
253 

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

25162  255 
by (blast elim!: less_SucE intro: less_trans) 
13449  256 

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

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

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

25162  261 
by (simp add: less_Suc_eq) 
13449  262 

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

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

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

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

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

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

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

273 
done 

274 

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

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

279 
done 

14302  280 

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

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

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

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

286 
shows "P n m" 

287 
apply (rule less_linear [THEN disjE]) 

288 
apply (erule_tac [2] disjE) 

289 
apply (erule lessCase) 

290 
apply (erule sym [THEN eqCase]) 

291 
apply (erule major) 

292 
done 

293 

294 

295 
subsubsection {* Inductive (?) properties *} 

296 

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

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

300 
done 

301 

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

303 
apply (induct n) 

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

305 
done 

306 

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

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

309 
apply (rule major [THEN lessE]) 

310 
apply (erule lessI [THEN minor]) 

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

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

25162  315 
by (blast elim: lessE dest: Suc_lessD) 
4104  316 

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

320 
apply (erule Suc_mono) 

321 
done 

322 

323 
lemma less_trans_Suc: 

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

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

328 
apply (blast dest: Suc_lessD) 

329 
done 

330 

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

333 

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

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

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

339 
lemma nat_less_induct: 

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

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

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

21243  348 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

376 
done  {* formerly called lessD *} 

377 

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

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

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

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

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

385 
apply blast 

386 
done 

387 

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

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

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

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

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

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

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

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

400 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

451 

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

455 
rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+ 

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

456 

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

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

462 
text {* 

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

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

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

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

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

470 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

471 

472 

473 
text {* 

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

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

478 

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

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

25162  481 
by auto 
13449  482 

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

25162  484 
by auto 
13449  485 

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

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

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

25162  492 
by simp 
13449  493 

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

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

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

498 
by (cases n) simp_all 

13449  499 

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

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

25140  505 

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

25162  508 
by (rule neq0_conv[THEN iffD1], iprover) 
13449  509 

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

510 
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" 
25162  511 
by (fast intro: not0_implies_Suc) 
13449  512 

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

513 
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

514 
using neq0_conv by blast 
13449  515 

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

516 
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" 
25162  517 
by (induct m') simp_all 
13449  518 

519 
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

520 
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0  (\<exists>j. m = Suc j & j < n))" 
25162  521 
by (cases m) simp_all 
13449  522 

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

523 
lemma nat_induct2: "[P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))] ==> P n" 
13449  524 
apply (rule nat_less_induct) 
525 
apply (case_tac n) 

526 
apply (case_tac [2] nat) 

527 
apply (blast intro: less_trans)+ 

528 
done 

529 

21243  530 

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

531 
subsection {* @{text LEAST} theorems for type @{typ nat}*} 
13449  532 

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

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

534 
"[ P n; ~ P 0 ] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" 
14208  535 
apply (case_tac "n", auto) 
13449  536 
apply (frule LeastI) 
537 
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

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

543 
done 

544 

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

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

13449  548 

549 

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

551 

25076  552 
lemma mono_Suc: "mono Suc" 
25162  553 
by (rule monoI) simp 
25076  554 

13449  555 
lemma min_0L [simp]: "min 0 n = (0::nat)" 
25162  556 
by (rule min_leastL) simp 
13449  557 

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

25162  559 
by (rule min_leastR) simp 
13449  560 

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

25162  562 
by (simp add: mono_Suc min_of_mono) 
13449  563 

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

25162  566 
by (simp split: nat.split) 
22191  567 

568 
lemma min_Suc2: 

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

25162  570 
by (simp split: nat.split) 
22191  571 

13449  572 
lemma max_0L [simp]: "max 0 n = (n::nat)" 
25162  573 
by (rule max_leastL) simp 
13449  574 

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

25162  576 
by (rule max_leastR) simp 
13449  577 

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

25162  579 
by (simp add: mono_Suc max_of_mono) 
13449  580 

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

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

585 
lemma max_Suc2: 

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

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

13449  589 

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

591 

592 
text {* Difference *} 

593 

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

594 
lemma diff_0_eq_0 [simp, code]: "0  n = (0::nat)" 
25162  595 
by (induct n) simp_all 
13449  596 

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

597 
lemma diff_Suc_Suc [simp, code]: "Suc(m)  Suc(n) = m  n" 
25162  598 
by (induct n) simp_all 
13449  599 

600 

601 
text {* 

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

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

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

605 
*} 

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

607 
by (simp split add: nat.split) 
13449  608 

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

609 
declare diff_Suc [simp del, code del] 
13449  610 

611 

612 
subsection {* Addition *} 

613 

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

25162  615 
by (induct m) simp_all 
13449  616 

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

25162  618 
by (induct m) simp_all 
13449  619 

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

622 

13449  623 

624 
text {* Associative law for addition *} 

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

625 
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" 
25162  626 
by (induct m) simp_all 
13449  627 

628 
text {* Commutative law for addition *} 

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

629 
lemma nat_add_commute: "m + n = n + (m::nat)" 
25162  630 
by (induct m) simp_all 
13449  631 

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

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

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

635 
apply (rule nat_add_commute) 
13449  636 
done 
637 

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

14331  641 
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" 
25162  642 
by (induct k) simp_all 
13449  643 

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

14331  647 
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" 
25162  648 
by (induct k) simp_all 
13449  649 

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

651 

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

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

25162  656 
by (cases m) simp_all 
13449  657 

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

25162  659 
by (rule trans, rule eq_commute, rule add_is_1) 
13449  660 

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

13449  663 

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

665 
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

666 
apply (simp add: nat_add_assoc del: add_0_right) 
13449  667 
done 
668 

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

669 
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" 
22718  670 
apply (induct k) 
671 
apply simp 

672 
apply(drule comp_inj_on[OF _ inj_Suc]) 

673 
apply (simp add:o_def) 

674 
done 

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

675 

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

676 

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

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

678 

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

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

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

682 

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

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

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

686 

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

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

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

690 

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

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

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

694 

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

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

697 

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

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

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

701 

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

702 

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

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

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

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

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

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

710 
show "(i * j) * k = i * (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

711 
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

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

713 
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

714 
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

715 
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

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

717 

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

718 
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0  n=0)" 
15251  719 
apply (induct m) 
22718  720 
apply (induct_tac [2] n) 
721 
apply simp_all 

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

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

723 

21243  724 

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

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

726 

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

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

728 
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)" 
25162  729 
by (induct k) simp_all 
14341
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 
text {* strict, in both arguments *} 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

732 
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

733 
apply (rule add_less_mono1 [THEN less_trans], assumption+) 
15251  734 
apply (induct j, 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 

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

737 
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

738 
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

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

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

742 
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

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

746 
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

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

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

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

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

751 

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

752 

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

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

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

757 
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

758 
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

759 
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

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

761 

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

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

764 

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

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

767 

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

768 

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

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

770 

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

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

776 
shows "P i j" 

777 
proof  

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

19870  780 
proof (induct k) 
22718  781 
case 0 
782 
show ?case by (simp add: step) 

19870  783 
next 
784 
case (Suc k) 

22718  785 
thus ?case by (auto intro: assms) 
19870  786 
qed 
22718  787 
thus "P i j" by (simp add: j) 
19870  788 
qed 
789 

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

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

793 
\begin{itemize} 

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

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

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

797 
\end{itemize} *} 

798 

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

802 

24523  803 
text{* A compact version without explicit base case: *} 
804 
lemma infinite_descent: 

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

806 
by (induct n rule: less_induct, auto) 

807 

24438  808 

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

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

811 
\begin{itemize} 

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

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

814 
\end{itemize} 

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

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

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

24438  819 
shows "P x" 
820 
proof  

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

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

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

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

827 
case (smaller n) 

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

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

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

831 
thus ?case by auto 

832 
qed 

833 
ultimately show "P x" by auto 

834 
qed 

19870  835 

24523  836 
text{* Again, without explicit base case: *} 
837 
lemma infinite_descent_measure: 

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

839 
proof  

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

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

842 
proof (induct n rule: infinite_descent, auto) 

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

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

845 
qed 

846 
ultimately show "P x" by auto 

847 
qed 

848 

849 

850 

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

851 
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

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

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

856 

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

857 

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

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

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

861 

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

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

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

865 

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

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

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

869 
lemma le_add1: "n \<le> ((n + m)::nat)" 
24438  870 
by (simp add: add_commute, rule le_add2) 
13449  871 

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

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

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

24438  876 
by (rule le_less_trans, rule le_add2, rule lessI) 
13449  877 

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

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

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

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

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

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

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

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

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

24438  891 
by (rule less_le_trans, assumption, rule le_add2) 
13449  892 

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

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

896 
done 

13449  897 

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

24438  899 
apply (rule notI) 
900 
apply (erule add_lessD1 [THEN less_irrefl]) 

901 
done 

13449  902 

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

24438  904 
by (simp add: add_commute not_add_less1) 
13449  905 

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

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

909 
done 

13449  910 

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

911 
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" 
24438  912 
apply (simp add: add_commute) 
913 
apply (erule add_leD1) 

914 
done 

13449  915 

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

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

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

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

24438  921 
by (force simp del: add_Suc_right 
13449  922 
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) 
923 

924 

925 
subsection {* Difference *} 

926 

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

24438  928 
by (induct m) simp_all 
13449  929 

930 
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

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

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

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

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

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

941 

942 
subsection {* More results about difference *} 

943 

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

944 
lemma Suc_diff_le: "n \<le> m ==> Suc m  n = Suc (m  n)" 
24438  945 
by (induct m n rule: diff_induct) simp_all 
13449  946 

947 
lemma diff_less_Suc: "m  n < Suc m" 

24438  948 
apply (induct m n rule: diff_induct) 
949 
apply (erule_tac [3] less_SucE) 

950 
apply (simp_all add: less_Suc_eq) 

951 
done 

13449  952 

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

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

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

24438  957 
by (rule le_less_trans, rule diff_le_self) 
13449  958 

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

24438  960 
by (induct i j rule: diff_induct) simp_all 
13449  961 

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

24438  963 
by (simp add: diff_diff_left) 
13449  964 

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

24438  966 
by (cases n) (auto simp add: le_simps) 
13449  967 

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

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

24438  970 
by (simp add: diff_diff_left add_commute) 
13449  971 

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

972 
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j)  k = i + (j  k)" 
24438  973 
by (induct j k rule: diff_induct) simp_all 
13449  974 

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

975 
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i)  k = (j  k) + i" 
24438  976 
by (simp add: add_commute diff_add_assoc) 
13449  977 

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

24438  979 
by (induct n) simp_all 
13449  980 

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

24438  982 
by (simp add: diff_add_assoc) 
13449  983 

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

984 
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j  i = k) = (j = k + i)" 
24438  985 
by (auto simp add: diff_add_inverse2) 
13449  986 

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

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

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

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

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

24438  994 
by (induct m n rule: diff_induct) simp_all 
13449  995 

22718  996 
lemma less_imp_add_positive: 
997 
assumes "i < j" 

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

999 
proof 

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

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

1003 

13449  1004 
lemma diff_cancel: "(k + m)  (k + n) = m  (n::nat)" 
24438  1005 
by (induct k) simp_all 
13449  1006 

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

24438  1008 
by (simp add: diff_cancel add_commute) 
13449  1009 

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

24438  1011 
by (induct n) simp_all 
13449  1012 

1013 

1014 
text {* Difference distributes over multiplication *} 

1015 

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

24438  1017 
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) 
13449  1018 

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

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

1023 
lemmas nat_distrib = 

1024 
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 

1025 

1026 

1027 
subsection {* Monotonicity of Multiplication *} 

1028 

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

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

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

1032 
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" 
24438  1033 
by (simp add: mult_left_mono) 
13449  1034 

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

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

1036 
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" 
24438  1037 
by (simp add: mult_mono) 
13449  1038 

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

24438  1040 
by (simp add: mult_strict_right_mono) 
13449  1041 

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

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

13449  1045 
apply (induct m) 
22718  1046 
apply simp 
1047 
apply (case_tac n) 

1048 
apply simp_all 

13449  1049 
done 
1050 

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

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

1055 
apply simp_all 

13449  1056 
done 
1057 

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

22718  1059 
apply (induct m) 
1060 
apply simp 

1061 
apply (induct n) 

1062 
apply auto 

13449  1063 
done 
1064 

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

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

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

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

1075 
done 

1076 

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

24438  1078 
by (simp add: mult_commute [of k]) 
13449  1079 

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

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

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

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

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

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

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

1089 
done 
13449  1090 

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

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

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

24438  1095 
by (subst mult_less_cancel1) simp 
13449  1096 

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

1097 
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" 
24438  1098 
by (subst mult_le_cancel1) simp 
13449  1099 

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

24438  1101 
by (subst mult_cancel1) simp 
13449  1102 

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

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

1105 
apply (drule sym) 

1106 
apply (rule disjCI) 

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

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

1111 

20588  1112 

24995  1113 
subsection {* size of a datatype value *} 
1114 

1115 
class size = type + 

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

1117 

1118 
use "Tools/function_package/size.ML" 

1119 

1120 
setup Size.setup 

1121 

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

25162  1123 
by (induct n) simp_all 
24995  1124 

1125 
lemma size_bool [code func]: 

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

1127 

1128 
declare "*.size" [noatp] 

1129 

1130 

18702  1131 
subsection {* Code generator setup *} 
1132 

20588  1133 
instance nat :: eq .. 
1134 

1135 
lemma [code func]: 

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

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

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

25162  1140 
by auto 
20588  1141 

1142 
lemma [code func]: 

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

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

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

22348  1147 
using Suc_le_eq less_Suc_eq_le by simp_all 
20588  1148 

21243  1149 

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

1152 

1153 
context semiring_1 

1154 
begin 

1155 

1156 
definition 

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

1159 
end 

1160 

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

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

1165 
shows "u = s" 

1166 
using 2 1 by (rule trans) 

1167 

24196  1168 

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

1172 
use "Tools/lin_arith.ML" 

1173 
declaration {* K LinArith.setup *} 

1174 

21243  1175 

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

1177 

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

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

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

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

1184 
lemma nat_diff_split: 

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

1189 
lemma nat_diff_split_asm: 

25162  1190 
"P(a  b::nat) = (~ (a < b & ~ P 0  (EX d. a = b + d & ~ P d)))" 
21243  1191 
 {* elimination of @{text } on @{text nat} in assumptions *} 
24438  1192 
by (simp split: nat_diff_split) 
21243  1193 

1194 
lemmas [arith_split] = nat_diff_split split_min split_max 

1195 

1196 

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

24438  1198 
by (induct m) auto 
21243  1199 

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

24438  1201 
by (induct m) auto 
21243  1202 

1203 

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

1205 

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

24438  1207 
by arith 
21243  1208 

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

24438  1210 
by arith 
21243  1211 

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

24438  1213 
by arith 
21243  1214 

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

24438  1216 
by arith 
21243  1217 

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

24438  1219 
by arith 
21243  1220 

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

24438  1222 
by arith 
21243  1223 

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

1225 
second premise n\<le>m*) 

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

24438  1227 
by arith 
21243  1228 

1229 

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

1231 

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

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

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

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

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

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

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

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

1244 

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

1246 

1247 
(* Monotonicity of subtraction in first argument *) 

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

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

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

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

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

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

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

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

1260 
text{*Lemmas for ex/Factorization*} 

1261 

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

24438  1263 
by (cases m) auto 
21243  1264 

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

24438  1266 
by (cases m) auto 
21243  1267 

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

24438  1269 
by (cases m) auto 
21243  1270 

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

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

1272 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1289 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1306 

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

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

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

1309 

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

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

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

1313 
text{*Rewriting to pull differences out*} 

1314 

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

24438  1316 
by arith 
21243  1317 

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

24438  1319 
by arith 
21243  1320 

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

24438  1322 
by arith 
21243  1323 

1324 
(*The others are 

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

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

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

1328 
lemmas add_diff_assoc = diff_add_assoc [symmetric] 

1329 
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] 