author | wenzelm |
Fri, 26 Oct 2001 23:58:21 +0200 | |
changeset 11952 | b10f1e8862f4 |
parent 11701 | 3d51fbf81c17 |
child 12304 | 8df202daf55d |
permissions | -rw-r--r-- |
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 |
(** Less-then 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 (j-n))"; |
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 (j-n)))"; |
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 = (m-n) 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 = (m-n) 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 (m-n) 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+m-n) 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((m-n) 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((m-n) 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((m-n) 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+m-n) 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 "(k-n) div n <= (k-m) 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 "(m-n) div n < (m-n)" 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"; |
|
11593 | 511 |
AddXIs [dvdI]; |
11373 | 512 |
|
11365 | 513 |
Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"; |
514 |
by (Blast_tac 1); |
|
515 |
qed "dvdE"; |
|
11593 | 516 |
AddXEs [dvdE]; |
11365 | 517 |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset
|
518 |
Goalw [dvd_def] "m dvd (0::nat)"; |
4089 | 519 |
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
3366 | 520 |
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
|
521 |
AddIffs [dvd_0_right]; |
3366 | 522 |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset
|
523 |
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
|
524 |
by Auto_tac; |
3366 | 525 |
qed "dvd_0_left"; |
526 |
||
11373 | 527 |
Goal "(0 dvd (m::nat)) = (m = 0)"; |
528 |
by (blast_tac (claset() addIs [dvd_0_left]) 1); |
|
529 |
qed "dvd_0_left_iff"; |
|
530 |
AddIffs [dvd_0_left_iff]; |
|
531 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset
|
532 |
Goalw [dvd_def] "Suc 0 dvd k"; |
3366 | 533 |
by (Simp_tac 1); |
534 |
qed "dvd_1_left"; |
|
535 |
AddIffs [dvd_1_left]; |
|
536 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset
|
537 |
Goal "(m dvd Suc 0) = (m = Suc 0)"; |
11365 | 538 |
by (simp_tac (simpset() addsimps [dvd_def]) 1); |
539 |
qed "dvd_1_iff_1"; |
|
540 |
Addsimps [dvd_1_iff_1]; |
|
541 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
542 |
Goalw [dvd_def] "m dvd (m::nat)"; |
4089 | 543 |
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); |
3366 | 544 |
qed "dvd_refl"; |
545 |
Addsimps [dvd_refl]; |
|
546 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
547 |
Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"; |
4089 | 548 |
by (blast_tac (claset() addIs [mult_assoc] ) 1); |
3366 | 549 |
qed "dvd_trans"; |
550 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
551 |
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
|
552 |
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
|
553 |
simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1); |
3366 | 554 |
qed "dvd_anti_sym"; |
555 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
556 |
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"; |
4089 | 557 |
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); |
3366 | 558 |
qed "dvd_add"; |
559 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
560 |
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"; |
4089 | 561 |
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); |
3366 | 562 |
qed "dvd_diff"; |
563 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
564 |
Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)"; |
3457 | 565 |
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
4089 | 566 |
by (blast_tac (claset() addIs [dvd_add]) 1); |
3366 | 567 |
qed "dvd_diffD"; |
568 |
||
11365 | 569 |
Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)"; |
570 |
by (dres_inst_tac [("m","m")] dvd_diff 1); |
|
571 |
by Auto_tac; |
|
572 |
qed "dvd_diffD1"; |
|
573 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
574 |
Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)"; |
4089 | 575 |
by (blast_tac (claset() addIs [mult_left_commute]) 1); |
3366 | 576 |
qed "dvd_mult"; |
577 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
578 |
Goal "k dvd m ==> k dvd (m*n :: nat)"; |
3366 | 579 |
by (stac mult_commute 1); |
580 |
by (etac dvd_mult 1); |
|
581 |
qed "dvd_mult2"; |
|
582 |
||
583 |
(* k dvd (m*k) *) |
|
584 |
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; |
|
585 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
586 |
Goal "(k dvd n + k) = (k dvd (n::nat))"; |
7499 | 587 |
by (rtac iffI 1); |
588 |
by (etac dvd_add 2); |
|
589 |
by (rtac dvd_refl 2); |
|
7493 | 590 |
by (subgoal_tac "n = (n+k)-k" 1); |
591 |
by (Simp_tac 2); |
|
7499 | 592 |
by (etac ssubst 1); |
593 |
by (etac dvd_diff 1); |
|
594 |
by (rtac dvd_refl 1); |
|
7493 | 595 |
qed "dvd_reduce"; |
596 |
||
11383 | 597 |
Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"; |
598 |
by (div_undefined_case_tac "n=0" 1); |
|
599 |
by Auto_tac; |
|
600 |
by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1); |
|
3366 | 601 |
qed "dvd_mod"; |
602 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
603 |
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
|
604 |
by (subgoal_tac "k dvd (m div n)*n + m mod n" 1); |
4089 | 605 |
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); |
4356 | 606 |
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); |
3366 | 607 |
qed "dvd_mod_imp_dvd"; |
608 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
609 |
Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"; |
9881 | 610 |
by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); |
611 |
qed "dvd_mod_iff"; |
|
612 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
613 |
Goalw [dvd_def] "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"; |
3366 | 614 |
by (etac exE 1); |
4089 | 615 |
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); |
3366 | 616 |
qed "dvd_mult_cancel"; |
617 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset
|
618 |
Goal "0<m ==> (m*n dvd m) = (n = (1::nat))"; |
11396 | 619 |
by Auto_tac; |
620 |
by (subgoal_tac "m*n dvd m*1" 1); |
|
621 |
by (dtac dvd_mult_cancel 1); |
|
622 |
by Auto_tac; |
|
623 |
qed "dvd_mult_cancel1"; |
|
624 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11593
diff
changeset
|
625 |
Goal "0<m ==> (n*m dvd m) = (n = (1::nat))"; |
11396 | 626 |
by (stac mult_commute 1); |
627 |
by (etac dvd_mult_cancel1 1); |
|
628 |
qed "dvd_mult_cancel2"; |
|
629 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10600
diff
changeset
|
630 |
Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"; |
3718 | 631 |
by (Clarify_tac 1); |
3366 | 632 |
by (res_inst_tac [("x","k*ka")] exI 1); |
4089 | 633 |
by (asm_simp_tac (simpset() addsimps mult_ac) 1); |
3366 | 634 |
qed "mult_dvd_mono"; |
635 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset
|
636 |
Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k"; |
4089 | 637 |
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); |
3366 | 638 |
by (Blast_tac 1); |
639 |
qed "dvd_mult_left"; |
|
640 |
||
11313 | 641 |
Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k"; |
642 |
by (Clarify_tac 1); |
|
643 |
by (res_inst_tac [("x","i*k")] exI 1); |
|
644 |
by (simp_tac (simpset() addsimps mult_ac) 1); |
|
645 |
qed "dvd_mult_right"; |
|
646 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset
|
647 |
Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)"; |
3718 | 648 |
by (Clarify_tac 1); |
4089 | 649 |
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
3457 | 650 |
by (etac conjE 1); |
651 |
by (rtac le_trans 1); |
|
652 |
by (rtac (le_refl RS mult_le_mono) 2); |
|
3366 | 653 |
by (etac Suc_leI 2); |
654 |
by (Simp_tac 1); |
|
655 |
qed "dvd_imp_le"; |
|
656 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset
|
657 |
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
|
658 |
by (div_undefined_case_tac "k=0" 1); |
3724 | 659 |
by Safe_tac; |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
660 |
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
|
661 |
by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1); |
3366 | 662 |
by (stac mult_commute 1); |
663 |
by (Asm_simp_tac 1); |
|
664 |
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
|
665 |
|
11593 | 666 |
Goal "n dvd m ==> n * (m div n) = (m::nat)"; |
667 |
by (subgoal_tac "m mod n = 0" 1); |
|
668 |
by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1); |
|
669 |
by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1); |
|
670 |
qed "dvd_mult_div_cancel"; |
|
671 |
||
10195
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset
|
672 |
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
|
673 |
by (auto_tac (claset(), |
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset
|
674 |
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
|
675 |
qed "mod_eq_0_iff"; |
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset
|
676 |
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
|
677 |
|
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset
|
678 |
(*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
|
679 |
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
|
680 |
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
|
681 |
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
|
682 |
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
|
683 |
qed "mod_eqD"; |
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset
|
684 |