author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
child 58871  c399ae4b836f 
permissions  rwrr 
41777  1 
(* Title: ZF/ArithSimp.thy 
9548  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 2000 University of Cambridge 

4 
*) 

5 

13328  6 
header{*Arithmetic with simplification*} 
7 

46820  8 
theory ArithSimp 
15481  9 
imports Arith 
10 
begin 

13259  11 

48891  12 
ML_file "~~/src/Provers/Arith/cancel_numerals.ML" 
13 
ML_file "~~/src/Provers/Arith/combine_numerals.ML" 

14 
ML_file "arith_data.ML" 

15 

16 

13356  17 
subsection{*Difference*} 
13259  18 

14046  19 
lemma diff_self_eq_0 [simp]: "m # m = 0" 
13259  20 
apply (subgoal_tac "natify (m) # natify (m) = 0") 
21 
apply (rule_tac [2] natify_in_nat [THEN nat_induct], auto) 

22 
done 

23 

24 
(**Addition is the inverse of subtraction**) 

25 

26 
(*We need m:nat even if we replace the RHS by natify(m), for consider e.g. 

46820  27 
n=2, m=omega; then n + (mn) = 2 + (02) = 2 \<noteq> 0 = natify(m).*) 
28 
lemma add_diff_inverse: "[ n \<le> m; m:nat ] ==> n #+ (m#n) = m" 

13259  29 
apply (frule lt_nat_in_nat, erule nat_succI) 
30 
apply (erule rev_mp) 

13784  31 
apply (rule_tac m = m and n = n in diff_induct, auto) 
13259  32 
done 
33 

46820  34 
lemma add_diff_inverse2: "[ n \<le> m; m:nat ] ==> (m#n) #+ n = m" 
13259  35 
apply (frule lt_nat_in_nat, erule nat_succI) 
36 
apply (simp (no_asm_simp) add: add_commute add_diff_inverse) 

37 
done 

38 

39 
(*Proof is IDENTICAL to that of add_diff_inverse*) 

46820  40 
lemma diff_succ: "[ n \<le> m; m:nat ] ==> succ(m) # n = succ(m#n)" 
13259  41 
apply (frule lt_nat_in_nat, erule nat_succI) 
42 
apply (erule rev_mp) 

13784  43 
apply (rule_tac m = m and n = n in diff_induct) 
13259  44 
apply (simp_all (no_asm_simp)) 
45 
done 

46 

47 
lemma zero_less_diff [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

48 
"[ m: nat; n: nat ] ==> 0 < (n # m) \<longleftrightarrow> m<n" 
13784  49 
apply (rule_tac m = m and n = n in diff_induct) 
13259  50 
apply (simp_all (no_asm_simp)) 
51 
done 

52 

53 

54 
(** Difference distributes over multiplication **) 

55 

56 
lemma diff_mult_distrib: "(m # n) #* k = (m #* k) # (n #* k)" 

57 
apply (subgoal_tac " (natify (m) # natify (n)) #* natify (k) = (natify (m) #* natify (k)) # (natify (n) #* natify (k))") 

58 
apply (rule_tac [2] m = "natify (m) " and n = "natify (n) " in diff_induct) 

59 
apply (simp_all add: diff_cancel) 

60 
done 

61 

62 
lemma diff_mult_distrib2: "k #* (m # n) = (k #* m) # (k #* n)" 

63 
apply (simp (no_asm) add: mult_commute [of k] diff_mult_distrib) 

64 
done 

65 

66 

13356  67 
subsection{*Remainder*} 
13259  68 

69 
(*We need m:nat even with natify*) 

46820  70 
lemma div_termination: "[ 0<n; n \<le> m; m:nat ] ==> m # n < m" 
13259  71 
apply (frule lt_nat_in_nat, erule nat_succI) 
72 
apply (erule rev_mp) 

73 
apply (erule rev_mp) 

13784  74 
apply (rule_tac m = m and n = n in diff_induct) 
13259  75 
apply (simp_all (no_asm_simp) add: diff_le_self) 
76 
done 

77 

78 
(*for mod and div*) 

46820  79 
lemmas div_rls = 
80 
nat_typechecks Ord_transrec_type apply_funtype 

13259  81 
div_termination [THEN ltD] 
82 
nat_into_Ord not_lt_iff_le [THEN iffD1] 

83 

46820  84 
lemma raw_mod_type: "[ m:nat; n:nat ] ==> raw_mod (m, n) \<in> nat" 
13259  85 
apply (unfold raw_mod_def) 
86 
apply (rule Ord_transrec_type) 

87 
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) 

46820  88 
apply (blast intro: div_rls) 
13259  89 
done 
90 

46820  91 
lemma mod_type [TC,iff]: "m mod n \<in> nat" 
13259  92 
apply (unfold mod_def) 
93 
apply (simp (no_asm) add: mod_def raw_mod_type) 

94 
done 

95 

96 

46820  97 
(** Aribtrary definitions for division by zero. Useful to simplify 
13259  98 
certain equations **) 
99 

100 
lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0" 

101 
apply (unfold div_def) 

102 
apply (rule raw_div_def [THEN def_transrec, THEN trans]) 

103 
apply (simp (no_asm_simp)) 

104 
done (*NOT for adding to default simpset*) 

105 

106 
lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)" 

107 
apply (unfold mod_def) 

108 
apply (rule raw_mod_def [THEN def_transrec, THEN trans]) 

109 
apply (simp (no_asm_simp)) 

110 
done (*NOT for adding to default simpset*) 

111 

112 
lemma raw_mod_less: "m<n ==> raw_mod (m,n) = m" 

113 
apply (rule raw_mod_def [THEN def_transrec, THEN trans]) 

114 
apply (simp (no_asm_simp) add: div_termination [THEN ltD]) 

115 
done 

116 

46820  117 
lemma mod_less [simp]: "[ m<n; n \<in> nat ] ==> m mod n = m" 
13259  118 
apply (frule lt_nat_in_nat, assumption) 
119 
apply (simp (no_asm_simp) add: mod_def raw_mod_less) 

120 
done 

121 

122 
lemma raw_mod_geq: 

46820  123 
"[ 0<n; n \<le> m; m:nat ] ==> raw_mod (m, n) = raw_mod (m#n, n)" 
13259  124 
apply (frule lt_nat_in_nat, erule nat_succI) 
125 
apply (rule raw_mod_def [THEN def_transrec, THEN trans]) 

13611  126 
apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast) 
13259  127 
done 
128 

129 

46820  130 
lemma mod_geq: "[ n \<le> m; m:nat ] ==> m mod n = (m#n) mod n" 
13259  131 
apply (frule lt_nat_in_nat, erule nat_succI) 
132 
apply (case_tac "n=0") 

133 
apply (simp add: DIVISION_BY_ZERO_MOD) 

134 
apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff]) 

135 
done 

136 

137 

13356  138 
subsection{*Division*} 
13259  139 

46820  140 
lemma raw_div_type: "[ m:nat; n:nat ] ==> raw_div (m, n) \<in> nat" 
13259  141 
apply (unfold raw_div_def) 
142 
apply (rule Ord_transrec_type) 

143 
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) 

46820  144 
apply (blast intro: div_rls) 
13259  145 
done 
146 

46820  147 
lemma div_type [TC,iff]: "m div n \<in> nat" 
13259  148 
apply (unfold div_def) 
149 
apply (simp (no_asm) add: div_def raw_div_type) 

150 
done 

151 

152 
lemma raw_div_less: "m<n ==> raw_div (m,n) = 0" 

153 
apply (rule raw_div_def [THEN def_transrec, THEN trans]) 

154 
apply (simp (no_asm_simp) add: div_termination [THEN ltD]) 

155 
done 

156 

46820  157 
lemma div_less [simp]: "[ m<n; n \<in> nat ] ==> m div n = 0" 
13259  158 
apply (frule lt_nat_in_nat, assumption) 
159 
apply (simp (no_asm_simp) add: div_def raw_div_less) 

160 
done 

161 

46820  162 
lemma raw_div_geq: "[ 0<n; n \<le> m; m:nat ] ==> raw_div(m,n) = succ(raw_div(m#n, n))" 
163 
apply (subgoal_tac "n \<noteq> 0") 

13259  164 
prefer 2 apply blast 
165 
apply (frule lt_nat_in_nat, erule nat_succI) 

166 
apply (rule raw_div_def [THEN def_transrec, THEN trans]) 

46820  167 
apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) 
13259  168 
done 
169 

170 
lemma div_geq [simp]: 

46820  171 
"[ 0<n; n \<le> m; m:nat ] ==> m div n = succ ((m#n) div n)" 
13259  172 
apply (frule lt_nat_in_nat, erule nat_succI) 
173 
apply (simp (no_asm_simp) add: div_def raw_div_geq) 

174 
done 

175 

176 
declare div_less [simp] div_geq [simp] 

177 

178 

179 
(*A key result*) 

180 
lemma mod_div_lemma: "[ m: nat; n: nat ] ==> (m div n)#*n #+ m mod n = m" 

181 
apply (case_tac "n=0") 

182 
apply (simp add: DIVISION_BY_ZERO_MOD) 

183 
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) 

184 
apply (erule complete_induct) 

185 
apply (case_tac "x<n") 

186 
txt{*case x<n*} 

187 
apply (simp (no_asm_simp)) 

46820  188 
txt{*case @{term"n \<le> x"}*} 
13259  189 
apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse) 
190 
done 

191 

192 
lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)" 

193 
apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ") 

46820  194 
apply force 
13259  195 
apply (subst mod_div_lemma, auto) 
196 
done 

197 

198 
lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m" 

199 
apply (simp (no_asm_simp) add: mod_div_equality_natify) 

200 
done 

201 

202 

13356  203 
subsection{*Further Facts about Remainder*} 
204 

205 
text{*(mainly for mutilated chess board)*} 

13259  206 

207 
lemma mod_succ_lemma: 

46820  208 
"[ 0<n; m:nat; n:nat ] 
13259  209 
==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" 
210 
apply (erule complete_induct) 

211 
apply (case_tac "succ (x) <n") 

212 
txt{* case succ(x) < n *} 

213 
apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self) 

214 
apply (simp add: ltD [THEN mem_imp_not_eq]) 

46820  215 
txt{* case @{term"n \<le> succ(x)"} *} 
13259  216 
apply (simp add: mod_geq not_lt_iff_le) 
217 
apply (erule leE) 

218 
apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ) 

219 
txt{*equality case*} 

220 
apply (simp add: diff_self_eq_0) 

221 
done 

222 

223 
lemma mod_succ: 

224 
"n:nat ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" 

225 
apply (case_tac "n=0") 

226 
apply (simp (no_asm_simp) add: natify_succ DIVISION_BY_ZERO_MOD) 

227 
apply (subgoal_tac "natify (succ (m)) mod n = (if succ (natify (m) mod n) = n then 0 else succ (natify (m) mod n))") 

228 
prefer 2 

229 
apply (subst natify_succ) 

230 
apply (rule mod_succ_lemma) 

231 
apply (auto simp del: natify_succ simp add: nat_into_Ord [THEN Ord_0_lt_iff]) 

232 
done 

233 

234 
lemma mod_less_divisor: "[ 0<n; n:nat ] ==> m mod n < n" 

235 
apply (subgoal_tac "natify (m) mod n < n") 

236 
apply (rule_tac [2] i = "natify (m) " in complete_induct) 

46820  237 
apply (case_tac [3] "x<n", auto) 
238 
txt{* case @{term"n \<le> x"}*} 

13259  239 
apply (simp add: mod_geq not_lt_iff_le div_termination [THEN ltD]) 
240 
done 

241 

242 
lemma mod_1_eq [simp]: "m mod 1 = 0" 

13784  243 
by (cut_tac n = 1 in mod_less_divisor, auto) 
13259  244 

245 
lemma mod2_cases: "b<2 ==> k mod 2 = b  k mod 2 = (if b=1 then 0 else 1)" 

246 
apply (subgoal_tac "k mod 2: 2") 

247 
prefer 2 apply (simp add: mod_less_divisor [THEN ltD]) 

248 
apply (drule ltD, auto) 

249 
done 

250 

251 
lemma mod2_succ_succ [simp]: "succ(succ(m)) mod 2 = m mod 2" 

252 
apply (subgoal_tac "m mod 2: 2") 

253 
prefer 2 apply (simp add: mod_less_divisor [THEN ltD]) 

254 
apply (auto simp add: mod_succ) 

255 
done 

256 

257 
lemma mod2_add_more [simp]: "(m#+m#+n) mod 2 = n mod 2" 

258 
apply (subgoal_tac " (natify (m) #+natify (m) #+n) mod 2 = n mod 2") 

259 
apply (rule_tac [2] n = "natify (m) " in nat_induct) 

260 
apply auto 

261 
done 

262 

263 
lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0" 

13784  264 
by (cut_tac n = 0 in mod2_add_more, auto) 
13259  265 

266 

13356  267 
subsection{*Additional theorems about @{text "\<le>"}*} 
13259  268 

46820  269 
lemma add_le_self: "m:nat ==> m \<le> (m #+ n)" 
13259  270 
apply (simp (no_asm_simp)) 
271 
done 

272 

46820  273 
lemma add_le_self2: "m:nat ==> m \<le> (n #+ m)" 
13259  274 
apply (simp (no_asm_simp)) 
275 
done 

276 

277 
(*** Monotonicity of Multiplication ***) 

278 

46820  279 
lemma mult_le_mono1: "[ i \<le> j; j:nat ] ==> (i#*k) \<le> (j#*k)" 
280 
apply (subgoal_tac "natify (i) #*natify (k) \<le> j#*natify (k) ") 

13259  281 
apply (frule_tac [2] lt_nat_in_nat) 
282 
apply (rule_tac [3] n = "natify (k) " in nat_induct) 

283 
apply (simp_all add: add_le_mono) 

284 
done 

285 

46820  286 
(* @{text"\<le>"} monotonicity, BOTH arguments*) 
287 
lemma mult_le_mono: "[ i \<le> j; k \<le> l; j:nat; l:nat ] ==> i#*k \<le> j#*l" 

13259  288 
apply (rule mult_le_mono1 [THEN le_trans], assumption+) 
289 
apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+) 

290 
done 

291 

292 
(*strict, in 1st argument; proof is by induction on k>0. 

293 
I can't see how to relax the typing conditions.*) 

294 
lemma mult_lt_mono2: "[ i<j; 0<k; j:nat; k:nat ] ==> k#*i < k#*j" 

295 
apply (erule zero_lt_natE) 

296 
apply (frule_tac [2] lt_nat_in_nat) 

297 
apply (simp_all (no_asm_simp)) 

298 
apply (induct_tac "x") 

299 
apply (simp_all (no_asm_simp) add: add_lt_mono) 

300 
done 

301 

302 
lemma mult_lt_mono1: "[ i<j; 0<k; j:nat; k:nat ] ==> i#*k < j#*k" 

303 
apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k]) 

304 
done 

305 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

306 
lemma add_eq_0_iff [iff]: "m#+n = 0 \<longleftrightarrow> natify(m)=0 & natify(n)=0" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

307 
apply (subgoal_tac "natify (m) #+ natify (n) = 0 \<longleftrightarrow> natify (m) =0 & natify (n) =0") 
13259  308 
apply (rule_tac [2] n = "natify (m) " in natE) 
309 
apply (rule_tac [4] n = "natify (n) " in natE) 

310 
apply auto 

311 
done 

312 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

313 
lemma zero_lt_mult_iff [iff]: "0 < m#*n \<longleftrightarrow> 0 < natify(m) & 0 < natify(n)" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

314 
apply (subgoal_tac "0 < natify (m) #*natify (n) \<longleftrightarrow> 0 < natify (m) & 0 < natify (n) ") 
13259  315 
apply (rule_tac [2] n = "natify (m) " in natE) 
316 
apply (rule_tac [4] n = "natify (n) " in natE) 

317 
apply (rule_tac [3] n = "natify (n) " in natE) 

318 
apply auto 

319 
done 

320 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

321 
lemma mult_eq_1_iff [iff]: "m#*n = 1 \<longleftrightarrow> natify(m)=1 & natify(n)=1" 
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

322 
apply (subgoal_tac "natify (m) #* natify (n) = 1 \<longleftrightarrow> natify (m) =1 & natify (n) =1") 
13259  323 
apply (rule_tac [2] n = "natify (m) " in natE) 
324 
apply (rule_tac [4] n = "natify (n) " in natE) 

325 
apply auto 

326 
done 

327 

328 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

329 
lemma mult_is_zero: "[m: nat; n: nat] ==> (m #* n = 0) \<longleftrightarrow> (m = 0  n = 0)" 
13259  330 
apply auto 
331 
apply (erule natE) 

332 
apply (erule_tac [2] natE, auto) 

333 
done 

334 

335 
lemma mult_is_zero_natify [iff]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

336 
"(m #* n = 0) \<longleftrightarrow> (natify(m) = 0  natify(n) = 0)" 
13259  337 
apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero) 
338 
apply auto 

339 
done 

340 

341 

13356  342 
subsection{*Cancellation Laws for Common Factors in Comparisons*} 
13259  343 

344 
lemma mult_less_cancel_lemma: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

345 
"[ k: nat; m: nat; n: nat ] ==> (m#*k < n#*k) \<longleftrightarrow> (0<k & m<n)" 
13259  346 
apply (safe intro!: mult_lt_mono1) 
347 
apply (erule natE, auto) 

348 
apply (rule not_le_iff_lt [THEN iffD1]) 

349 
apply (drule_tac [3] not_le_iff_lt [THEN [2] rev_iffD2]) 

350 
prefer 5 apply (blast intro: mult_le_mono1, auto) 

351 
done 

352 

353 
lemma mult_less_cancel2 [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

354 
"(m#*k < n#*k) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))" 
13259  355 
apply (rule iff_trans) 
356 
apply (rule_tac [2] mult_less_cancel_lemma, auto) 

357 
done 

358 

359 
lemma mult_less_cancel1 [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

360 
"(k#*m < k#*n) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))" 
13259  361 
apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k]) 
362 
done 

363 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

364 
lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))" 
13259  365 
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) 
366 
apply auto 

367 
done 

368 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

369 
lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))" 
13259  370 
apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) 
371 
apply auto 

372 
done 

373 

46820  374 
lemma mult_le_cancel_le1: "k \<in> nat ==> k #* m \<le> k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) \<le> 1)" 
13784  375 
by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto) 
13259  376 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

377 
lemma Ord_eq_iff_le: "[ Ord(m); Ord(n) ] ==> m=n \<longleftrightarrow> (m \<le> n & n \<le> m)" 
13259  378 
by (blast intro: le_anti_sym) 
379 

380 
lemma mult_cancel2_lemma: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

381 
"[ k: nat; m: nat; n: nat ] ==> (m#*k = n#*k) \<longleftrightarrow> (m=n  k=0)" 
13259  382 
apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m]) 
383 
apply (auto simp add: Ord_0_lt_iff) 

384 
done 

385 

386 
lemma mult_cancel2 [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

387 
"(m#*k = n#*k) \<longleftrightarrow> (natify(m) = natify(n)  natify(k) = 0)" 
13259  388 
apply (rule iff_trans) 
389 
apply (rule_tac [2] mult_cancel2_lemma, auto) 

390 
done 

391 

392 
lemma mult_cancel1 [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

393 
"(k#*m = k#*n) \<longleftrightarrow> (natify(m) = natify(n)  natify(k) = 0)" 
13259  394 
apply (simp (no_asm) add: mult_cancel2 mult_commute [of k]) 
395 
done 

396 

397 

398 
(** Cancellation law for division **) 

399 

400 
lemma div_cancel_raw: 

401 
"[ 0<n; 0<k; k:nat; m:nat; n:nat ] ==> (k#*m) div (k#*n) = m div n" 

13784  402 
apply (erule_tac i = m in complete_induct) 
13259  403 
apply (case_tac "x<n") 
404 
apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2) 

405 
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] 

406 
div_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD]) 

407 
done 

408 

409 
lemma div_cancel: 

410 
"[ 0 < natify(n); 0 < natify(k) ] ==> (k#*m) div (k#*n) = m div n" 

46820  411 
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" 
13259  412 
in div_cancel_raw) 
413 
apply auto 

414 
done 

415 

416 

13356  417 
subsection{*More Lemmas about Remainder*} 
13259  418 

419 
lemma mult_mod_distrib_raw: 

420 
"[ k:nat; m:nat; n:nat ] ==> (k#*m) mod (k#*n) = k #* (m mod n)" 

421 
apply (case_tac "k=0") 

422 
apply (simp add: DIVISION_BY_ZERO_MOD) 

423 
apply (case_tac "n=0") 

424 
apply (simp add: DIVISION_BY_ZERO_MOD) 

425 
apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) 

13784  426 
apply (erule_tac i = m in complete_induct) 
13259  427 
apply (case_tac "x<n") 
428 
apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2) 

46820  429 
apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] 
13259  430 
mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD]) 
431 
done 

432 

433 
lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)" 

46820  434 
apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" 
13259  435 
in mult_mod_distrib_raw) 
436 
apply auto 

437 
done 

438 

439 
lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)" 

440 
apply (simp (no_asm) add: mult_commute mod_mult_distrib2) 

441 
done 

442 

443 
lemma mod_add_self2_raw: "n \<in> nat ==> (m #+ n) mod n = m mod n" 

444 
apply (subgoal_tac " (n #+ m) mod n = (n #+ m # n) mod n") 

46820  445 
apply (simp add: add_commute) 
446 
apply (subst mod_geq [symmetric], auto) 

13259  447 
done 
448 

449 
lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n" 

450 
apply (cut_tac n = "natify (n) " in mod_add_self2_raw) 

451 
apply auto 

452 
done 

453 

454 
lemma mod_add_self1 [simp]: "(n#+m) mod n = m mod n" 

455 
apply (simp (no_asm_simp) add: add_commute mod_add_self2) 

456 
done 

457 

458 
lemma mod_mult_self1_raw: "k \<in> nat ==> (m #+ k#*n) mod n = m mod n" 

459 
apply (erule nat_induct) 

460 
apply (simp_all (no_asm_simp) add: add_left_commute [of _ n]) 

461 
done 

462 

463 
lemma mod_mult_self1 [simp]: "(m #+ k#*n) mod n = m mod n" 

464 
apply (cut_tac k = "natify (k) " in mod_mult_self1_raw) 

465 
apply auto 

466 
done 

467 

468 
lemma mod_mult_self2 [simp]: "(m #+ n#*k) mod n = m mod n" 

469 
apply (simp (no_asm) add: mult_commute mod_mult_self1) 

470 
done 

471 

472 
(*Lemma for gcd*) 

473 
lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1  m=0" 

474 
apply (subgoal_tac "m: nat") 

46820  475 
prefer 2 
13259  476 
apply (erule ssubst) 
46820  477 
apply simp 
13259  478 
apply (rule disjCI) 
479 
apply (drule sym) 

480 
apply (rule Ord_linear_lt [of "natify(n)" 1]) 

46820  481 
apply simp_all 
482 
apply (subgoal_tac "m #* n = 0", simp) 

13259  483 
apply (subst mult_natify2 [symmetric]) 
484 
apply (simp del: mult_natify2) 

485 
apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto) 

486 
done 

487 

488 
lemma less_imp_succ_add [rule_format]: 

46820  489 
"[ m<n; n: nat ] ==> \<exists>k\<in>nat. n = succ(m#+k)" 
13259  490 
apply (frule lt_nat_in_nat, assumption) 
491 
apply (erule rev_mp) 

492 
apply (induct_tac "n") 

493 
apply (simp_all (no_asm) add: le_iff) 

494 
apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric]) 

495 
done 

496 

497 
lemma less_iff_succ_add: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

498 
"[ m: nat; n: nat ] ==> (m<n) \<longleftrightarrow> (\<exists>k\<in>nat. n = succ(m#+k))" 
13259  499 
by (auto intro: less_imp_succ_add) 
500 

14055  501 
lemma add_lt_elim2: 
502 
"\<lbrakk>a #+ d = b #+ c; a < b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c < d" 

46820  503 
by (drule less_imp_succ_add, auto) 
14055  504 

505 
lemma add_le_elim2: 

46820  506 
"\<lbrakk>a #+ d = b #+ c; a \<le> b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c \<le> d" 
507 
by (drule less_imp_succ_add, auto) 

14055  508 

13356  509 

510 
subsubsection{*More Lemmas About Difference*} 

13259  511 

512 
lemma diff_is_0_lemma: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

513 
"[ m: nat; n: nat ] ==> m # n = 0 \<longleftrightarrow> m \<le> n" 
13784  514 
apply (rule_tac m = m and n = n in diff_induct, simp_all) 
13259  515 
done 
516 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

517 
lemma diff_is_0_iff: "m # n = 0 \<longleftrightarrow> natify(m) \<le> natify(n)" 
13259  518 
by (simp add: diff_is_0_lemma [symmetric]) 
519 

520 
lemma nat_lt_imp_diff_eq_0: 

521 
"[ a:nat; b:nat; a<b ] ==> a # b = 0" 

46820  522 
by (simp add: diff_is_0_iff le_iff) 
13259  523 

14055  524 
lemma raw_nat_diff_split: 
46820  525 
"[ a:nat; b:nat ] ==> 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

526 
(P(a # b)) \<longleftrightarrow> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))" 
13259  527 
apply (case_tac "a < b") 
528 
apply (force simp add: nat_lt_imp_diff_eq_0) 

46820  529 
apply (rule iffI, force, simp) 
13259  530 
apply (drule_tac x="a#b" in bspec) 
46820  531 
apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) 
13259  532 
done 
533 

14055  534 
lemma nat_diff_split: 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

535 
"(P(a # b)) \<longleftrightarrow> 
46820  536 
(natify(a) < natify(b) \<longrightarrow>P(0)) & (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))" 
14055  537 
apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split) 
538 
apply simp_all 

539 
done 

540 

14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

541 
text{*Difference and lessthan*} 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

542 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

543 
lemma diff_lt_imp_lt: "[(k#i) < (k#j); i\<in>nat; j\<in>nat; k\<in>nat] ==> j<i" 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

544 
apply (erule rev_mp) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

545 
apply (simp split add: nat_diff_split, auto) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

546 
apply (blast intro: add_le_self lt_trans1) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

547 
apply (rule not_le_iff_lt [THEN iffD1], auto) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

548 
apply (subgoal_tac "i #+ da < j #+ d", force) 
46820  549 
apply (blast intro: add_le_lt_mono) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

550 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

551 

46820  552 
lemma lt_imp_diff_lt: "[j<i; i\<le>k; k\<in>nat] ==> (k#i) < (k#j)" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

553 
apply (frule le_in_nat, assumption) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

554 
apply (frule lt_nat_in_nat, assumption) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

555 
apply (simp split add: nat_diff_split, auto) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

556 
apply (blast intro: lt_asym lt_trans2) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

557 
apply (blast intro: lt_irrefl lt_trans2) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

558 
apply (rule not_le_iff_lt [THEN iffD1], auto) 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

559 
apply (subgoal_tac "j #+ d < i #+ da", force) 
46820  560 
apply (blast intro: add_lt_le_mono) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

561 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

562 

c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

563 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

564 
lemma diff_lt_iff_lt: "[i\<le>k; j\<in>nat; k\<in>nat] ==> (k#i) < (k#j) \<longleftrightarrow> j<i" 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

565 
apply (frule le_in_nat, assumption) 
46820  566 
apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt) 
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

567 
done 
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14055
diff
changeset

568 

9548  569 
end 