author  wenzelm 
Wed, 28 Nov 2001 00:37:40 +0100  
changeset 12304  8df202daf55d 
parent 11701  3d51fbf81c17 
permissions  rwrr 
3366  1 
(* Title: HOL/Divides.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
The division operators div, mod and the divides relation "dvd" 

7 
*) 

8 

9 

10 
(** Lessthen properties **) 

11 

9108  12 
bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
13 
def_wfrec RS trans); 

3366  14 

5069  15 
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \ 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

16 
\ (%f j. if j<n  n=0 then j else f (jn))"; 
4089  17 
by (simp_tac (simpset() addsimps [mod_def]) 1); 
3366  18 
qed "mod_eq"; 
19 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

20 
Goal "(%m. m div n) = wfrec (trancl pred_nat) \ 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

21 
\ (%f j. if j<n  n=0 then 0 else Suc (f (jn)))"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

22 
by (simp_tac (simpset() addsimps [div_def]) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

23 
qed "div_eq"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

24 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

25 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

26 
(** Aribtrary definitions for division by zero. Useful to simplify 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

27 
certain equations **) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

28 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

29 
Goal "a div 0 = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

30 
by (rtac (div_eq RS wf_less_trans) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

31 
by (Asm_simp_tac 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

32 
qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

33 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

34 
Goal "a mod 0 = (a::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

35 
by (rtac (mod_eq RS wf_less_trans) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

36 
by (Asm_simp_tac 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

37 
qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

38 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

39 
fun div_undefined_case_tac s i = 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

40 
case_tac s i THEN 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

41 
Full_simp_tac (i+1) THEN 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

42 
asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

43 
DIVISION_BY_ZERO_MOD]) i; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

44 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

45 
(*** Remainder ***) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

46 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

47 
Goal "m<n ==> m mod n = (m::nat)"; 
3366  48 
by (rtac (mod_eq RS wf_less_trans) 1); 
49 
by (Asm_simp_tac 1); 

50 
qed "mod_less"; 

8393  51 
Addsimps [mod_less]; 
3366  52 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

53 
Goal "~ m < (n::nat) ==> m mod n = (mn) mod n"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

54 
by (div_undefined_case_tac "n=0" 1); 
3366  55 
by (rtac (mod_eq RS wf_less_trans) 1); 
4089  56 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  57 
qed "mod_geq"; 
58 

5415  59 
(*Avoids the ugly ~m<n above*) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

60 
Goal "(n::nat) <= m ==> m mod n = (mn) mod n"; 
5415  61 
by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1); 
62 
qed "le_mod_geq"; 

63 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

64 
Goal "m mod (n::nat) = (if m<n then m else (mn) mod n)"; 
8393  65 
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); 
4774  66 
qed "mod_if"; 
67 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

68 
Goal "m mod Suc 0 = 0"; 
3366  69 
by (induct_tac "m" 1); 
8393  70 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq]))); 
3366  71 
qed "mod_1"; 
72 
Addsimps [mod_1]; 

73 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

74 
Goal "n mod n = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

75 
by (div_undefined_case_tac "n=0" 1); 
8393  76 
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); 
3366  77 
qed "mod_self"; 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

78 
Addsimps [mod_self]; 
3366  79 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

80 
Goal "(m+n) mod n = m mod (n::nat)"; 
3366  81 
by (subgoal_tac "(n + m) mod n = (n+mn) mod n" 1); 
82 
by (stac (mod_geq RS sym) 2); 

4089  83 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 
4811  84 
qed "mod_add_self2"; 
4810  85 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

86 
Goal "(n+m) mod n = m mod (n::nat)"; 
4811  87 
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); 
88 
qed "mod_add_self1"; 

4810  89 

8783  90 
Addsimps [mod_add_self1, mod_add_self2]; 
91 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

92 
Goal "(m + k*n) mod n = m mod (n::nat)"; 
4810  93 
by (induct_tac "k" 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

94 
by (ALLGOALS 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

95 
(asm_simp_tac 
8783  96 
(simpset() addsimps [read_instantiate [("y","n")] add_left_commute]))); 
4811  97 
qed "mod_mult_self1"; 
4810  98 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

99 
Goal "(m + n*k) mod n = m mod (n::nat)"; 
4811  100 
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); 
101 
qed "mod_mult_self2"; 

4810  102 

4811  103 
Addsimps [mod_mult_self1, mod_mult_self2]; 
3366  104 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

105 
Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

106 
by (div_undefined_case_tac "n=0" 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

107 
by (div_undefined_case_tac "k=0" 1); 
9870  108 
by (induct_thm_tac nat_less_induct "m" 1); 
4774  109 
by (stac mod_if 1); 
110 
by (Asm_simp_tac 1); 

8393  111 
by (asm_simp_tac (simpset() addsimps [mod_geq, 
4774  112 
diff_less, diff_mult_distrib]) 1); 
3366  113 
qed "mod_mult_distrib"; 
114 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

115 
Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

116 
by (asm_simp_tac 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

117 
(simpset() addsimps [read_instantiate [("m","k")] mult_commute, 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

118 
mod_mult_distrib]) 1); 
3366  119 
qed "mod_mult_distrib2"; 
120 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

121 
Goal "(m*n) mod n = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

122 
by (div_undefined_case_tac "n=0" 1); 
3366  123 
by (induct_tac "m" 1); 
8393  124 
by (Asm_simp_tac 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

125 
by (rename_tac "k" 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

126 
by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1); 
4089  127 
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); 
3366  128 
qed "mod_mult_self_is_0"; 
7082  129 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

130 
Goal "(n*m) mod n = (0::nat)"; 
7082  131 
by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1); 
132 
qed "mod_mult_self1_is_0"; 

133 
Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0]; 

3366  134 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

135 

3366  136 
(*** Quotient ***) 
137 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

138 
Goal "m<n ==> m div n = (0::nat)"; 
3366  139 
by (rtac (div_eq RS wf_less_trans) 1); 
140 
by (Asm_simp_tac 1); 

141 
qed "div_less"; 

8393  142 
Addsimps [div_less]; 
3366  143 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

144 
Goal "[ 0<n; ~m<n ] ==> m div n = Suc((mn) div n)"; 
3366  145 
by (rtac (div_eq RS wf_less_trans) 1); 
4089  146 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  147 
qed "div_geq"; 
148 

5415  149 
(*Avoids the ugly ~m<n above*) 
150 
Goal "[ 0<n; n<=m ] ==> m div n = Suc((mn) div n)"; 

151 
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); 

152 
qed "le_div_geq"; 

153 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

154 
Goal "0<n ==> m div n = (if m<n then 0 else Suc((mn) div n))"; 
8393  155 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
4774  156 
qed "div_if"; 
157 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

158 

3366  159 
(*Main Result about quotient and remainder.*) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

160 
Goal "(m div n)*n + m mod n = (m::nat)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

161 
by (div_undefined_case_tac "n=0" 1); 
9870  162 
by (induct_thm_tac nat_less_induct "m" 1); 
4774  163 
by (stac mod_if 1); 
164 
by (ALLGOALS (asm_simp_tac 

8393  165 
(simpset() addsimps [add_assoc, div_geq, 
5537  166 
add_diff_inverse, diff_less]))); 
3366  167 
qed "mod_div_equality"; 
168 

4358  169 
(* a simple rearrangement of mod_div_equality: *) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

170 
Goal "(n::nat) * (m div n) = m  (m mod n)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

171 
by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); 
9912  172 
by (full_simp_tac (simpset() addsimps mult_ac) 1); 
173 
by (arith_tac 1); 

4358  174 
qed "mult_div_cancel"; 
175 

10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

176 
Goal "0<n ==> m mod n < (n::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

177 
by (induct_thm_tac nat_less_induct "m" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

178 
by (case_tac "na<n" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

179 
(*case n le na*) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

180 
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

181 
(*case na<n*) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

182 
by (Asm_simp_tac 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

183 
qed "mod_less_divisor"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

184 
Addsimps [mod_less_divisor]; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

185 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

186 
(*** More division laws ***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

187 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

188 
Goal "0<n ==> (m*n) div n = (m::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

189 
by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

190 
by Auto_tac; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

191 
qed "div_mult_self_is_m"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

192 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

193 
Goal "0<n ==> (n*m) div n = (m::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

194 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

195 
qed "div_mult_self1_is_m"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

196 
Addsimps [div_mult_self_is_m, div_mult_self1_is_m]; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

197 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

198 
(*mod_mult_distrib2 above is the counterpart for remainder*) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

199 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

200 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

201 
(*** Proving facts about div and mod using quorem ***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

202 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

203 
Goal "[ b*q' + r' <= b*q + r; 0 < b; r < b ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

204 
\ ==> q' <= (q::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

205 
by (rtac leI 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

206 
by (stac less_iff_Suc_add 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

207 
by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2])); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

208 
qed "unique_quotient_lemma"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

209 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

210 
Goal "[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

211 
\ ==> q = q'"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

212 
by (asm_full_simp_tac 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

213 
(simpset() addsimps split_ifs @ [Divides.quorem_def]) 1); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

214 
by Auto_tac; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

215 
by (REPEAT 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

216 
(blast_tac (claset() addIs [order_antisym] 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

217 
addDs [order_eq_refl RS unique_quotient_lemma, 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

218 
sym]) 1)); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

219 
qed "unique_quotient"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

220 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

221 
Goal "[ quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

222 
\ ==> r = r'"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

223 
by (subgoal_tac "q = q'" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

224 
by (blast_tac (claset() addIs [unique_quotient]) 2); 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

225 
by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

226 
qed "unique_remainder"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

227 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

228 
Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

229 
by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

230 
by (auto_tac 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

231 
(claset() addEs [sym], 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

232 
simpset() addsimps mult_ac@[Divides.quorem_def])); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

233 
qed "quorem_div_mod"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

234 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

235 
Goal "[ quorem((a,b),(q,r)); 0 < b ] ==> a div b = q"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

236 
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

237 
qed "quorem_div"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

238 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

239 
Goal "[ quorem((a,b),(q,r)); 0 < b ] ==> a mod b = r"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

240 
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

241 
qed "quorem_mod"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

242 

10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

243 
(** A dividend of zero **) 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

244 

322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

245 
Goal "0 div m = (0::nat)"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

246 
by (div_undefined_case_tac "m=0" 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

247 
by (Asm_simp_tac 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

248 
qed "div_0"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

249 

322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

250 
Goal "0 mod m = (0::nat)"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

251 
by (div_undefined_case_tac "m=0" 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

252 
by (Asm_simp_tac 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

253 
qed "mod_0"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

254 
Addsimps [div_0, mod_0]; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

255 

10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

256 
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

257 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

258 
Goal "[ quorem((b,c),(q,r)); 0 < c ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

259 
\ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

260 
by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

261 
by (auto_tac 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

262 
(claset(), 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

263 
simpset() addsimps split_ifs@mult_ac@ 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

264 
[Divides.quorem_def, add_mult_distrib2])); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

265 
val lemma = result(); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

266 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

267 
Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

268 
by (div_undefined_case_tac "c = 0" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

269 
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

270 
qed "div_mult1_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

271 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

272 
Goal "(a*b) mod c = a*(b mod c) mod (c::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

273 
by (div_undefined_case_tac "c = 0" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

274 
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

275 
qed "mod_mult1_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

276 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

277 
Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

278 
by (rtac trans 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

279 
by (res_inst_tac [("s","b*a mod c")] trans 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

280 
by (rtac mod_mult1_eq 2); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

281 
by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute]))); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

282 
qed "mod_mult1_eq'"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

283 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

284 
Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

285 
by (rtac (mod_mult1_eq' RS trans) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

286 
by (rtac mod_mult1_eq 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

287 
qed "mod_mult_distrib_mod"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

288 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

289 
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

290 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

291 
Goal "[ quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

292 
\ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

293 
by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

294 
by (auto_tac 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

295 
(claset(), 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

296 
simpset() addsimps split_ifs@mult_ac@ 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

297 
[Divides.quorem_def, add_mult_distrib2])); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

298 
val lemma = result(); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

299 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

300 
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

301 
Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

302 
by (div_undefined_case_tac "c = 0" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

303 
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

304 
MRS lemma RS quorem_div]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

305 
qed "div_add1_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

306 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

307 
Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

308 
by (div_undefined_case_tac "c = 0" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

309 
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

310 
MRS lemma RS quorem_mod]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

311 
qed "mod_add1_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

312 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

313 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

314 
(*** proving a div (b*c) = (a div b) div c ***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

315 

10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

316 
(** first, a lemma to bound the remainder **) 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

317 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

318 
Goal "[ (0::nat) < c; r < b ] ==> b * (q mod c) + r < b * c"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

319 
by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

320 
by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

321 
by Auto_tac; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

322 
by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

323 
by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1); 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

324 
val mod_lemma = result(); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

325 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

326 
Goal "[ quorem ((a,b), (q,r)); 0 < b; 0 < c ] \ 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

327 
\ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

328 
by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

329 
by (auto_tac 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

330 
(claset(), 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

331 
simpset() addsimps mult_ac@ 
10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

332 
[Divides.quorem_def, add_mult_distrib2 RS sym, 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

333 
mod_lemma])); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

334 
val lemma = result(); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

335 

10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

336 
Goal "a div (b*c) = (a div b) div (c::nat)"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

337 
by (div_undefined_case_tac "b=0" 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

338 
by (div_undefined_case_tac "c=0" 1); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

339 
by (force_tac (claset(), 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

340 
simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

341 
qed "div_mult2_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

342 

10600
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

343 
Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"; 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

344 
by (div_undefined_case_tac "b=0" 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

345 
by (div_undefined_case_tac "c=0" 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

346 
by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1); 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

347 
by (auto_tac (claset(), 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

348 
simpset() addsimps [mult_commute, 
322475c2cb75
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents:
10559
diff
changeset

349 
quorem_div_mod RS lemma RS quorem_mod])); 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

350 
qed "mod_mult2_eq"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

351 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

352 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

353 
(*** Cancellation of common factors in "div" ***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

354 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

355 
Goal "[ (0::nat) < b; 0 < c ] ==> (c*a) div (c*b) = a div b"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

356 
by (stac div_mult2_eq 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

357 
by Auto_tac; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

358 
val lemma1 = result(); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

359 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

360 
Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

361 
by (div_undefined_case_tac "b = 0" 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

362 
by (auto_tac 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

363 
(claset(), 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

364 
simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

365 
lemma1, lemma2])); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

366 
qed "div_mult_mult1"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

367 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

368 
Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

369 
by (dtac div_mult_mult1 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

370 
by (auto_tac (claset(), simpset() addsimps [mult_commute])); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

371 
qed "div_mult_mult2"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

372 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

373 
Addsimps [div_mult_mult1, div_mult_mult2]; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

374 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

375 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

376 
(*** Distribution of factors over "mod" 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

377 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

378 
Could prove these as in Integ/IntDiv.ML, but we already have 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

379 
mod_mult_distrib and mod_mult_distrib2 above! 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

380 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

381 
Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

382 
qed "mod_mult_mult1"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

383 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

384 
Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

385 
qed "mod_mult_mult2"; 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

386 
***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

387 

d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

388 
(*** Further facts about div and mod ***) 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

389 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

390 
Goal "m div Suc 0 = m"; 
3366  391 
by (induct_tac "m" 1); 
8393  392 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); 
3366  393 
qed "div_1"; 
394 
Addsimps [div_1]; 

395 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

396 
Goal "0<n ==> n div n = (1::nat)"; 
8393  397 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
3366  398 
qed "div_self"; 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

399 
Addsimps [div_self]; 
4811  400 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

401 
Goal "0<n ==> (m+n) div n = Suc (m div n)"; 
4811  402 
by (subgoal_tac "(n + m) div n = Suc ((n+mn) div n)" 1); 
403 
by (stac (div_geq RS sym) 2); 

404 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 

405 
qed "div_add_self2"; 

406 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

407 
Goal "0<n ==> (n+m) div n = Suc (m div n)"; 
4811  408 
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); 
409 
qed "div_add_self1"; 

410 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

411 
Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"; 
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

412 
by (stac div_add1_eq 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

413 
by (stac div_mult1_eq 1); 
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10195
diff
changeset

414 
by (Asm_simp_tac 1); 
4811  415 
qed "div_mult_self1"; 
416 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

417 
Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)"; 
4811  418 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); 
419 
qed "div_mult_self2"; 

420 

421 
Addsimps [div_mult_self1, div_mult_self2]; 

422 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

423 
(* Monotonicity of div in first argument *) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

424 
Goal "ALL m::nat. m <= n > (m div k) <= (n div k)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

425 
by (div_undefined_case_tac "k=0" 1); 
9870  426 
by (induct_thm_tac nat_less_induct "n" 1); 
3718  427 
by (Clarify_tac 1); 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

428 
by (case_tac "n<k" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

429 
(* 1 case n<k *) 
8393  430 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

431 
(* 2 case n >= k *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

432 
by (case_tac "m<k" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

433 
(* 2.1 case m<k *) 
8393  434 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

435 
(* 2.2 case m>=k *) 
4089  436 
by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

437 
qed_spec_mp "div_le_mono"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

438 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

439 
(* Antimonotonicity of div in second argument *) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

440 
Goal "!!m::nat. [ 0<m; m<=n ] ==> (k div n) <= (k div m)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

441 
by (subgoal_tac "0<n" 1); 
6073  442 
by (Asm_simp_tac 2); 
9870  443 
by (induct_thm_tac nat_less_induct "k" 1); 
3496  444 
by (rename_tac "k" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

445 
by (case_tac "k<n" 1); 
8393  446 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

447 
by (subgoal_tac "~(k<m)" 1); 
6073  448 
by (Asm_simp_tac 2); 
4089  449 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

450 
by (subgoal_tac "(kn) div n <= (km) div n" 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

451 
by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2)); 
5318  452 
by (rtac le_trans 1); 
5316  453 
by (Asm_simp_tac 1); 
454 
by (asm_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

455 
qed "div_le_mono2"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

456 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

457 
Goal "m div n <= (m::nat)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

458 
by (div_undefined_case_tac "n=0" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

459 
by (subgoal_tac "m div n <= m div 1" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

460 
by (Asm_full_simp_tac 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

461 
by (rtac div_le_mono2 1); 
6073  462 
by (ALLGOALS Asm_simp_tac); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

463 
qed "div_le_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

464 
Addsimps [div_le_dividend]; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

465 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

466 
(* Similar for "less than" *) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

467 
Goal "!!n::nat. 1<n ==> (0 < m) > (m div n < m)"; 
9870  468 
by (induct_thm_tac nat_less_induct "m" 1); 
3496  469 
by (rename_tac "m" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

470 
by (case_tac "m<n" 1); 
8393  471 
by (Asm_full_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

472 
by (subgoal_tac "0<n" 1); 
6073  473 
by (Asm_simp_tac 2); 
4089  474 
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

475 
by (case_tac "n<m" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

476 
by (subgoal_tac "(mn) div n < (mn)" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

477 
by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); 
4089  478 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 
479 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

480 
(* case n=m *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

481 
by (subgoal_tac "m=n" 1); 
6073  482 
by (Asm_simp_tac 2); 
8393  483 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

484 
qed_spec_mp "div_less_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

485 
Addsimps [div_less_dividend]; 
3366  486 

487 
(*** Further facts about mod (mainly for the mutilated chess board ***) 

488 

10964  489 
Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 
490 
by (div_undefined_case_tac "n=0" 1); 

9870  491 
by (induct_thm_tac nat_less_induct "m" 1); 
8860  492 
by (case_tac "Suc(na)<n" 1); 
3366  493 
(* case Suc(na) < n *) 
8860  494 
by (forward_tac [lessI RS less_trans] 1 
495 
THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1); 

3366  496 
(* case n <= Suc(na) *) 
5415  497 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
498 
mod_geq]) 1); 

8860  499 
by (auto_tac (claset(), 
500 
simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq])); 

3366  501 
qed "mod_Suc"; 
502 

503 

504 
(************************************************) 

505 
(** Divides Relation **) 

506 
(************************************************) 

507 

11593  508 
Goalw [dvd_def] "n = m * k ==> m dvd n"; 
11373  509 
by (Blast_tac 1); 
510 
qed "dvdI"; 

511 

11365  512 
Goalw [dvd_def] "!!P. [m dvd n; !!k. n = m*k ==> P] ==> P"; 
513 
by (Blast_tac 1); 

514 
qed "dvdE"; 

515 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

516 
Goalw [dvd_def] "m dvd (0::nat)"; 
4089  517 
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); 
3366  518 
qed "dvd_0_right"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

519 
AddIffs [dvd_0_right]; 
3366  520 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

521 
Goalw [dvd_def] "0 dvd m ==> m = (0::nat)"; 
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

522 
by Auto_tac; 
3366  523 
qed "dvd_0_left"; 
524 

11373  525 
Goal "(0 dvd (m::nat)) = (m = 0)"; 
526 
by (blast_tac (claset() addIs [dvd_0_left]) 1); 

527 
qed "dvd_0_left_iff"; 

528 
AddIffs [dvd_0_left_iff]; 

529 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

530 
Goalw [dvd_def] "Suc 0 dvd k"; 
3366  531 
by (Simp_tac 1); 
532 
qed "dvd_1_left"; 

533 
AddIffs [dvd_1_left]; 

534 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

535 
Goal "(m dvd Suc 0) = (m = Suc 0)"; 
11365  536 
by (simp_tac (simpset() addsimps [dvd_def]) 1); 
537 
qed "dvd_1_iff_1"; 

538 
Addsimps [dvd_1_iff_1]; 

539 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

540 
Goalw [dvd_def] "m dvd (m::nat)"; 
4089  541 
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); 
3366  542 
qed "dvd_refl"; 
543 
Addsimps [dvd_refl]; 

544 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

545 
Goalw [dvd_def] "[ m dvd n; n dvd p ] ==> m dvd (p::nat)"; 
4089  546 
by (blast_tac (claset() addIs [mult_assoc] ) 1); 
3366  547 
qed "dvd_trans"; 
548 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

549 
Goalw [dvd_def] "[ m dvd n; n dvd m ] ==> m = (n::nat)"; 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

550 
by (force_tac (claset() addDs [mult_eq_self_implies_10], 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

551 
simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1); 
3366  552 
qed "dvd_anti_sym"; 
553 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

554 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (m+n :: nat)"; 
4089  555 
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); 
3366  556 
qed "dvd_add"; 
557 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

558 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (mn :: nat)"; 
4089  559 
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); 
3366  560 
qed "dvd_diff"; 
561 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

562 
Goal "[ k dvd mn; k dvd n; n<=m ] ==> k dvd (m::nat)"; 
3457  563 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
4089  564 
by (blast_tac (claset() addIs [dvd_add]) 1); 
3366  565 
qed "dvd_diffD"; 
566 

11365  567 
Goal "[ k dvd mn; k dvd m; n<=m ] ==> k dvd (n::nat)"; 
568 
by (dres_inst_tac [("m","m")] dvd_diff 1); 

569 
by Auto_tac; 

570 
qed "dvd_diffD1"; 

571 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

572 
Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)"; 
4089  573 
by (blast_tac (claset() addIs [mult_left_commute]) 1); 
3366  574 
qed "dvd_mult"; 
575 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

576 
Goal "k dvd m ==> k dvd (m*n :: nat)"; 
3366  577 
by (stac mult_commute 1); 
578 
by (etac dvd_mult 1); 

579 
qed "dvd_mult2"; 

580 

581 
(* k dvd (m*k) *) 

582 
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; 

583 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

584 
Goal "(k dvd n + k) = (k dvd (n::nat))"; 
7499  585 
by (rtac iffI 1); 
586 
by (etac dvd_add 2); 

587 
by (rtac dvd_refl 2); 

7493  588 
by (subgoal_tac "n = (n+k)k" 1); 
589 
by (Simp_tac 2); 

7499  590 
by (etac ssubst 1); 
591 
by (etac dvd_diff 1); 

592 
by (rtac dvd_refl 1); 

7493  593 
qed "dvd_reduce"; 
594 

11383  595 
Goalw [dvd_def] "!!n::nat. [ f dvd m; f dvd n ] ==> f dvd m mod n"; 
596 
by (div_undefined_case_tac "n=0" 1); 

597 
by Auto_tac; 

598 
by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1); 

3366  599 
qed "dvd_mod"; 
600 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

601 
Goal "[ (k::nat) dvd m mod n; k dvd n ] ==> k dvd m"; 
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

602 
by (subgoal_tac "k dvd (m div n)*n + m mod n" 1); 
4089  603 
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); 
4356  604 
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); 
3366  605 
qed "dvd_mod_imp_dvd"; 
606 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

607 
Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"; 
9881  608 
by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
609 
qed "dvd_mod_iff"; 

610 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

611 
Goalw [dvd_def] "!!k::nat. [ k*m dvd k*n; 0<k ] ==> m dvd n"; 
3366  612 
by (etac exE 1); 
4089  613 
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
3366  614 
qed "dvd_mult_cancel"; 
615 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

616 
Goal "0<m ==> (m*n dvd m) = (n = (1::nat))"; 
11396  617 
by Auto_tac; 
618 
by (subgoal_tac "m*n dvd m*1" 1); 

619 
by (dtac dvd_mult_cancel 1); 

620 
by Auto_tac; 

621 
qed "dvd_mult_cancel1"; 

622 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset

623 
Goal "0<m ==> (n*m dvd m) = (n = (1::nat))"; 
11396  624 
by (stac mult_commute 1); 
625 
by (etac dvd_mult_cancel1 1); 

626 
qed "dvd_mult_cancel2"; 

627 

10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset

628 
Goalw [dvd_def] "[ i dvd m; j dvd n] ==> i*j dvd (m*n :: nat)"; 
3718  629 
by (Clarify_tac 1); 
3366  630 
by (res_inst_tac [("x","k*ka")] exI 1); 
4089  631 
by (asm_simp_tac (simpset() addsimps mult_ac) 1); 
3366  632 
qed "mult_dvd_mono"; 
633 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

634 
Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k"; 
4089  635 
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); 
3366  636 
by (Blast_tac 1); 
637 
qed "dvd_mult_left"; 

638 

11313  639 
Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k"; 
640 
by (Clarify_tac 1); 

641 
by (res_inst_tac [("x","i*k")] exI 1); 

642 
by (simp_tac (simpset() addsimps mult_ac) 1); 

643 
qed "dvd_mult_right"; 

644 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

645 
Goalw [dvd_def] "[ k dvd n; 0 < n ] ==> k <= (n::nat)"; 
3718  646 
by (Clarify_tac 1); 
4089  647 
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); 
3457  648 
by (etac conjE 1); 
649 
by (rtac le_trans 1); 

650 
by (rtac (le_refl RS mult_le_mono) 2); 

3366  651 
by (etac Suc_leI 2); 
652 
by (Simp_tac 1); 

653 
qed "dvd_imp_le"; 

654 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

655 
Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

656 
by (div_undefined_case_tac "k=0" 1); 
3724  657 
by Safe_tac; 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

658 
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

659 
by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1); 
3366  660 
by (stac mult_commute 1); 
661 
by (Asm_simp_tac 1); 

662 
qed "dvd_eq_mod_eq_0"; 

10195
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

663 

11593  664 
Goal "n dvd m ==> n * (m div n) = (m::nat)"; 
665 
by (subgoal_tac "m mod n = 0" 1); 

666 
by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1); 

667 
by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1); 

668 
qed "dvd_mult_div_cancel"; 

669 

10195
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

670 
Goal "(m mod d = 0) = (EX q::nat. m = d*q)"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

671 
by (auto_tac (claset(), 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

672 
simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def])); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

673 
qed "mod_eq_0_iff"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

674 
AddSDs [mod_eq_0_iff RS iffD1]; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

675 

325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

676 
(*Loses information, namely we also have r<d provided d is nonzero*) 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

677 
Goal "(m mod d = r) ==> EX q::nat. m = r + q*d"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

678 
by (cut_inst_tac [("m","m")] mod_div_equality 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

679 
by (full_simp_tac (simpset() addsimps add_ac) 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

680 
by (blast_tac (claset() addIs [sym]) 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

681 
qed "mod_eqD"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

682 