author | paulson |
Wed, 13 Sep 2000 18:46:09 +0200 | |
changeset 9943 | 55c82decf3f4 |
parent 9747 | 043098ba5098 |
child 9969 | 4753185f1dd2 |
permissions | -rw-r--r-- |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
1 |
(* Title: IntPrimes.ML |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
9943 | 3 |
Author: Thomas M. Rasmussen & L C Paulson |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
6 |
dvd relation, GCD, Euclid's extended algorithm, primes, congruences |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
7 |
(all on the Integers) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
8 |
|
9943 | 9 |
Comparable to Primes theory, but dvd is included here as it is not present in |
10 |
IntDiv. Also includes extended GCD and congruences -- not present in Primes. |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
11 |
*) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
12 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
13 |
eta_contract:=false; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
14 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
15 |
|
9943 | 16 |
Goal "(abs (z::int) = w) = (z=w & #0 <= z | z=-w & z < #0)"; |
17 |
by (auto_tac (claset(), simpset() addsimps [zabs_def])); |
|
18 |
qed "zabs_eq_iff"; |
|
19 |
||
20 |
||
21 |
(** gcd lemmas **) |
|
22 |
||
23 |
val gcd_non_0 = thm "gcd_non_0"; |
|
24 |
val gcd_add1 = thm "gcd_add1"; |
|
25 |
val gcd_commute = thm "gcd_commute"; |
|
26 |
||
27 |
Goal "gcd (m+k, k) = gcd (m+k, m)"; |
|
28 |
by (simp_tac (simpset() addsimps [gcd_commute]) 1); |
|
29 |
qed "gcd_add1_eq"; |
|
30 |
||
31 |
Goal "m <= n \\<Longrightarrow> gcd (n, n - m) = gcd (n, m)"; |
|
32 |
by (subgoal_tac "n = m + (n-m)" 1); |
|
33 |
by (etac ssubst 1 THEN rtac gcd_add1_eq 1); |
|
34 |
by (Asm_simp_tac 1); |
|
35 |
qed "gcd_diff2"; |
|
36 |
||
37 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
38 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
39 |
(** Divides relation 'dvd' **) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
40 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
41 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
42 |
Goalw [dvd_def] "(m::int) dvd #0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
43 |
by (blast_tac (claset() addIs [zmult_0_right RS sym]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
44 |
qed "zdvd_0_right"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
45 |
AddIffs [zdvd_0_right]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
46 |
|
9943 | 47 |
Goalw [dvd_def] "(#0 dvd (m::int)) = (m = #0)"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
48 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
49 |
qed "zdvd_0_left"; |
9943 | 50 |
AddIffs [zdvd_0_left]; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
51 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
52 |
Goalw [dvd_def] "#1 dvd (m::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
53 |
by (Simp_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
54 |
qed "zdvd_1_left"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
55 |
AddIffs [zdvd_1_left]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
56 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
57 |
Goalw [dvd_def] "m dvd (m::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
58 |
by (blast_tac (claset() addIs [zmult_1_right RS sym]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
59 |
qed "zdvd_refl"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
60 |
Addsimps [zdvd_refl]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
61 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
62 |
Goalw [dvd_def] "[| m dvd n; n dvd k |] ==> m dvd (k::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
63 |
by (blast_tac (claset() addIs [zmult_assoc] ) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
64 |
qed "zdvd_trans"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
65 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
66 |
Goalw [dvd_def] "(m dvd -n) = (m dvd (n::int))"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
67 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
68 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
69 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
70 |
qed "zdvd_zminus_iff"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
71 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
72 |
Goalw [dvd_def] "(-m dvd n) = (m dvd (n::int))"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
73 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
74 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
75 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
76 |
qed "zdvd_zminus2_iff"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
77 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
78 |
Goalw [dvd_def] "[| #0<m; #0<n; m dvd n; n dvd m |] ==> m = (n::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
79 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
80 |
by (asm_full_simp_tac |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
81 |
(simpset() addsimps [zmult_assoc,zmult_eq_self_iff, |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
82 |
int_0_less_mult_iff, zmult_eq_1_iff]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
83 |
qed "zdvd_anti_sym"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
84 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
85 |
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
86 |
by (blast_tac (claset() addIs [zadd_zmult_distrib2 RS sym]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
87 |
qed "zdvd_zadd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
88 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
89 |
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
90 |
by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
91 |
qed "zdvd_zdiff"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
92 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
93 |
Goal "[| k dvd (m-n); k dvd n |] ==> k dvd (m::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
94 |
by (subgoal_tac "m=n+(m-n)" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
95 |
by (etac ssubst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
96 |
by (blast_tac (claset() addIs [zdvd_zadd]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
97 |
by (Simp_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
98 |
qed "zdvd_zdiffD"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
99 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
100 |
Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
101 |
by (blast_tac (claset() addIs [zmult_left_commute]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
102 |
qed "zdvd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
103 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
104 |
Goal "k dvd (m::int) ==> k dvd (m*n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
105 |
by (stac zmult_commute 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
106 |
by (etac zdvd_zmult 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
107 |
qed "zdvd_zmult2"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
108 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
109 |
(* k dvd (m*k) *) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
110 |
AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
111 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
112 |
Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
113 |
by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
114 |
by (Blast_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
115 |
qed "zdvd_zmultD2"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
116 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
117 |
Goal "(j*k) dvd n ==> k dvd (n::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
118 |
by (rtac zdvd_zmultD2 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
119 |
by (stac zmult_commute 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
120 |
by (assume_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
121 |
qed "zdvd_zmultD"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
122 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
123 |
Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> (i*j) dvd (m*n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
124 |
by (Clarify_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
125 |
by (res_inst_tac [("x","k*ka")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
126 |
by (asm_simp_tac (simpset() addsimps zmult_ac) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
127 |
qed "zdvd_zmult_mono"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
128 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
129 |
Goal "k dvd (n + k*m) = k dvd (n::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
130 |
by (rtac iffI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
131 |
by (etac zdvd_zadd 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
132 |
by (subgoal_tac "n = (n+k*m)-k*m" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
133 |
by (etac ssubst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
134 |
by (etac zdvd_zdiff 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
135 |
by (ALLGOALS Simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
136 |
qed "zdvd_reduce"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
137 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
138 |
Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd (m mod n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
139 |
by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1])); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
140 |
qed "zdvd_zmod"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
141 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
142 |
Goal "[| k dvd (m mod n); k dvd n |] ==> k dvd (m::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
143 |
by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
144 |
by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
145 |
by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
146 |
qed "zdvd_zmod_imp_zdvd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
147 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
148 |
Goalw [dvd_def] "(k dvd n) = (n mod (k::int) = #0)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
149 |
by (zdiv_undefined_case_tac "k=#0" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
150 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
151 |
by (res_inst_tac [("x","n div k")] exI 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
152 |
by (rtac trans 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
153 |
by (res_inst_tac [("b","k")] zmod_zdiv_equality 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
154 |
by (ALLGOALS Asm_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
155 |
qed "zdvd_iff_zmod_eq_0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
156 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
157 |
Goal "[| ~k<#0; k~=#0 |] ==> #0<(k::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
158 |
by (arith_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
159 |
val lemma = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
160 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
161 |
Goalw [dvd_def] "[| #0<m; m<n |] ==> ~n dvd (m::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
162 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
163 |
by (subgoal_tac "#0<n" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
164 |
by (blast_tac (claset() addIs [zless_trans]) 2); |
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
165 |
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
166 |
by (subgoal_tac "n*k < n*#1" 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
167 |
by (dtac (zmult_zless_cancel1 RS iffD1) 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
168 |
by Auto_tac; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
169 |
qed "zdvd_not_zless"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
170 |
|
9943 | 171 |
Goal "(int m dvd z) = (m dvd nat(abs z))"; |
172 |
by (auto_tac (claset(), |
|
173 |
simpset() addsimps [dvd_def, nat_abs_mult_distrib])); |
|
174 |
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, zabs_eq_iff])); |
|
175 |
by (res_inst_tac [("x","-(int k)")] exI 2); |
|
176 |
by (auto_tac (claset(), simpset() addsimps [zmult_int RS sym])); |
|
177 |
qed "int_dvd_iff"; |
|
178 |
||
179 |
Goal "(z dvd int m) = (nat(abs z) dvd m)"; |
|
180 |
by (auto_tac (claset(), |
|
181 |
simpset() addsimps [dvd_def, zabs_def, zmult_int RS sym])); |
|
182 |
by (res_inst_tac [("x","nat k")] exI 3); |
|
183 |
by (res_inst_tac [("x","-(int k)")] exI 2); |
|
184 |
by (res_inst_tac [("x","nat (-k)")] exI 1); |
|
185 |
by (cut_inst_tac [("k","m")] int_less_0_conv 3); |
|
186 |
by (cut_inst_tac [("k","m")] int_less_0_conv 1); |
|
187 |
by (auto_tac (claset(), |
|
188 |
simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff, |
|
189 |
nat_mult_distrib RS sym, nat_eq_iff2])); |
|
190 |
qed "dvd_int_iff"; |
|
191 |
||
192 |
Goal "(nat z dvd m) = (if #0 <= z then (z dvd int m) else m=0)"; |
|
193 |
by (auto_tac (claset(), simpset() addsimps [dvd_def, zmult_int RS sym])); |
|
194 |
by (res_inst_tac [("x","nat k")] exI 1); |
|
195 |
by (cut_inst_tac [("k","m")] int_less_0_conv 1); |
|
196 |
by (auto_tac (claset(), |
|
197 |
simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff, |
|
198 |
nat_mult_distrib RS sym, nat_eq_iff2])); |
|
199 |
qed "nat_dvd_iff"; |
|
200 |
||
201 |
Goal "(-z dvd w) = (z dvd (w::int))"; |
|
202 |
by (auto_tac (claset(), simpset() addsimps [dvd_def])); |
|
203 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
|
204 |
by Auto_tac; |
|
205 |
qed "zminus_dvd_iff"; |
|
206 |
||
207 |
Goal "(z dvd -w) = (z dvd (w::int))"; |
|
208 |
by (auto_tac (claset(), simpset() addsimps [dvd_def])); |
|
209 |
by (dtac (zminus_equation RS iffD1) 1); |
|
210 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
|
211 |
by Auto_tac; |
|
212 |
qed "dvd_zminus_iff"; |
|
213 |
AddIffs [zminus_dvd_iff, dvd_zminus_iff]; |
|
214 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
215 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
216 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
217 |
(** Euclid's Algorithm and GCD **) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
218 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
219 |
|
9943 | 220 |
Goal "zgcd(m,#0) = abs m"; |
221 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
222 |
qed "zgcd_0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
223 |
Addsimps [zgcd_0]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
224 |
|
9943 | 225 |
Goal"zgcd(#0,m) = abs m"; |
226 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
227 |
qed "zgcd_0_left"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
228 |
Addsimps [zgcd_0_left]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
229 |
|
9943 | 230 |
Goal "zgcd(-m,n) = zgcd(m,n)"; |
231 |
by (simp_tac (simpset() addsimps [zgcd_def]) 1); |
|
232 |
qed "zgcd_zminus"; |
|
233 |
Addsimps [zgcd_zminus]; |
|
234 |
||
235 |
Goal "zgcd(m,-n) = zgcd(m,n)"; |
|
236 |
by (simp_tac (simpset() addsimps [zgcd_def]) 1); |
|
237 |
qed "zgcd_zminus2"; |
|
238 |
Addsimps [zgcd_zminus2]; |
|
239 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
240 |
Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)"; |
9943 | 241 |
by (forw_inst_tac [("b","n"), ("a","m")] pos_mod_sign 1); |
242 |
by (asm_simp_tac (simpset() addsimps [zgcd_def, zabs_def, nat_mod_distrib]) 1); |
|
243 |
by (cut_inst_tac [("a","-m"),("b","n")] zmod_zminus1_eq_if 1); |
|
244 |
by (auto_tac (claset(), |
|
245 |
simpset() addsimps [gcd_non_0, nat_mod_distrib RS sym, |
|
246 |
zmod_zminus1_eq_if])); |
|
247 |
by (forw_inst_tac [("a","m")] pos_mod_bound 1); |
|
248 |
by (asm_simp_tac (simpset() addsimps [nat_diff_distrib]) 1); |
|
249 |
by (rtac gcd_diff2 1); |
|
250 |
by (asm_full_simp_tac (simpset() addsimps [nat_le_eq_zle]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
251 |
qed "zgcd_non_0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
252 |
|
9943 | 253 |
Goal "zgcd(m,n) = zgcd (n, m mod n)"; |
254 |
by (zdiv_undefined_case_tac "n = #0" 1); |
|
255 |
by (auto_tac |
|
256 |
(claset(), |
|
257 |
simpset() addsimps [linorder_neq_iff, zgcd_non_0])); |
|
258 |
by (cut_inst_tac [("m","-m"),("n","-n")] zgcd_non_0 1); |
|
259 |
by Auto_tac; |
|
260 |
qed "zgcd_eq"; |
|
261 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
262 |
Goal "zgcd(m,#1) = #1"; |
9943 | 263 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
264 |
qed "zgcd_1"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
265 |
Addsimps [zgcd_1]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
266 |
|
9943 | 267 |
Goal "(zgcd(#0,m) = #1) = (abs m = #1)"; |
268 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
269 |
qed "zgcd_0_1_iff"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
270 |
Addsimps [zgcd_0_1_iff]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
271 |
|
9943 | 272 |
Goal "zgcd(m,n) dvd m"; |
273 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); |
|
274 |
qed "zgcd_zdvd1"; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
275 |
|
9943 | 276 |
Goal "zgcd(m,n) dvd n"; |
277 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); |
|
278 |
qed "zgcd_zdvd2"; |
|
279 |
AddIffs [zgcd_zdvd1, zgcd_zdvd2]; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
280 |
|
9943 | 281 |
Goal "k dvd zgcd(m,n) = (k dvd m & k dvd n)"; |
282 |
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff, |
|
283 |
dvd_int_iff, nat_dvd_iff]) 1); |
|
284 |
qed "zgcd_greatest_iff"; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
285 |
|
9943 | 286 |
Goal "zgcd(m,n) = zgcd(n,m)"; |
287 |
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_commute"]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
288 |
qed "zgcd_commute"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
289 |
|
9943 | 290 |
Goal "zgcd(#1,m) = #1"; |
291 |
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_1_left"]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
292 |
qed "zgcd_1_left"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
293 |
Addsimps [zgcd_1_left]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
294 |
|
9943 | 295 |
Goal "zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))"; |
296 |
by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_assoc"]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
297 |
qed "zgcd_assoc"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
298 |
|
9943 | 299 |
Goal "zgcd(k,zgcd(m,n)) = zgcd(m,zgcd(k,n))"; |
300 |
by (rtac (zgcd_commute RS trans) 1); |
|
301 |
by (rtac (zgcd_assoc RS trans) 1); |
|
302 |
by (rtac (zgcd_commute RS arg_cong) 1); |
|
303 |
qed "zgcd_left_commute"; |
|
304 |
||
305 |
(*Addition is an AC-operator*) |
|
306 |
bind_thms ("zgcd_ac", [zgcd_assoc, zgcd_commute, zgcd_left_commute]); |
|
307 |
||
308 |
val gcd_mult_distrib2 = thm"gcd_mult_distrib2"; |
|
309 |
||
310 |
Goal "#0<=k ==> k * zgcd(m,n) = zgcd(k*m, k*n)"; |
|
311 |
by (asm_simp_tac |
|
312 |
(simpset() delsimps [zmult_zminus_right] |
|
313 |
addsimps [zmult_zminus_right RS sym, |
|
314 |
nat_mult_distrib, zgcd_def, zabs_def, |
|
315 |
zmult_less_0_iff, gcd_mult_distrib2 RS sym, |
|
316 |
zmult_int RS sym]) 1); |
|
317 |
qed "zgcd_zmult_distrib2"; |
|
318 |
||
319 |
Goal "zgcd(k*m, k*n) = abs k * zgcd(m,n)"; |
|
320 |
by (simp_tac (simpset() addsimps [zabs_def, zgcd_zmult_distrib2]) 1); |
|
321 |
qed "zgcd_zmult_distrib2_abs"; |
|
322 |
||
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
323 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
324 |
Goal "#0<=m ==> zgcd(m,m) = m"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
325 |
by (cut_inst_tac [("k","m"),("m","#1"),("n","#1")] zgcd_zmult_distrib2 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
326 |
by (ALLGOALS Asm_full_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
327 |
qed "zgcd_self"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
328 |
Addsimps [zgcd_self]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
329 |
|
9943 | 330 |
Goal "#0<=k ==> zgcd(k, k*n) = k"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
331 |
by (cut_inst_tac [("k","k"),("m","#1"),("n","n")] zgcd_zmult_distrib2 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
332 |
by (ALLGOALS Asm_full_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
333 |
qed "zgcd_zmult_eq_self"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
334 |
Addsimps [zgcd_zmult_eq_self]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
335 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
336 |
Goal "#0<=k ==> zgcd(k*n, k) = k"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
337 |
by (cut_inst_tac [("k","k"),("m","n"),("n","#1")] zgcd_zmult_distrib2 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
338 |
by (ALLGOALS Asm_full_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
339 |
qed "zgcd_zmult_eq_self2"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
340 |
Addsimps [zgcd_zmult_eq_self2]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
341 |
|
9943 | 342 |
Goal "[| zgcd(n,k)=#1; k dvd (m*n); #0 <= m |] ==> k dvd m"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
343 |
by (subgoal_tac "m = zgcd(m*n, m*k)" 1); |
9943 | 344 |
by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
345 |
by (ALLGOALS (asm_simp_tac (simpset() |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
346 |
addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff]))); |
9943 | 347 |
val lemma = result(); |
348 |
||
349 |
Goal "[| zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m"; |
|
350 |
by (case_tac "#0 <= m" 1); |
|
351 |
by (blast_tac (claset() addIs [lemma]) 1); |
|
352 |
by (subgoal_tac "k dvd -m" 1); |
|
353 |
by (rtac lemma 2); |
|
354 |
by Auto_tac; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
355 |
qed "zrelprime_zdvd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
356 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
357 |
Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #1"; |
9943 | 358 |
by Auto_tac; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
359 |
qed "zprime_imp_zrelprime"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
360 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
361 |
Goal "[| p:zprime; #0<n; n<p |] ==> zgcd(n,p) = #1"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
362 |
by (etac zprime_imp_zrelprime 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
363 |
by (etac zdvd_not_zless 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
364 |
by (assume_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
365 |
qed "zless_zprime_imp_zrelprime"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
366 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
367 |
Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
368 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
369 |
by (rtac zrelprime_zdvd_zmult 1); |
9943 | 370 |
by (rtac zprime_imp_zrelprime 1); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
371 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
372 |
qed "zprime_zdvd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
373 |
|
9943 | 374 |
val gcd_add_mult = thm "gcd_add_mult"; |
375 |
||
376 |
Goal "zgcd(m + n*k, n) = zgcd(m,n)"; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
377 |
by (rtac (zgcd_eq RS trans) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
378 |
by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
9943 | 379 |
by (rtac (zgcd_eq RS sym) 1); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
380 |
qed "zgcd_zadd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
381 |
Addsimps [zgcd_zadd_zmult]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
382 |
|
9943 | 383 |
|
384 |
Goal "zgcd(m,n) dvd zgcd(k*m,n)"; |
|
385 |
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); |
|
386 |
by (blast_tac (claset() addIs [zdvd_trans]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
387 |
qed "zgcd_zdvd_zgcd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
388 |
|
9943 | 389 |
Goal "zgcd(k,n) = #1 ==> zgcd(k*m,n) dvd zgcd(m,n)"; |
390 |
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); |
|
391 |
by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 1); |
|
392 |
by (simp_tac (simpset() addsimps [zmult_commute]) 2); |
|
393 |
by (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))" 1); |
|
394 |
by (Asm_full_simp_tac 1); |
|
395 |
by (simp_tac (simpset() addsimps zgcd_ac) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
396 |
qed "zgcd_zmult_zdvd_zgcd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
397 |
|
9943 | 398 |
val gcd_mult_cancel = thm "gcd_mult_cancel"; |
399 |
||
400 |
Goal "zgcd(k,n) = #1 ==> zgcd(k*m, n) = zgcd(m,n)"; |
|
401 |
by (asm_full_simp_tac (simpset() addsimps [zgcd_def, |
|
402 |
nat_abs_mult_distrib, gcd_mult_cancel]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
403 |
qed "zgcd_zmult_cancel"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
404 |
|
9943 | 405 |
Goal "[| zgcd(k,m) = #1; zgcd(n,m) = #1 |] ==> zgcd(k*n,m) = #1"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
406 |
by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
407 |
qed "zgcd_zgcd_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
408 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
409 |
Goal "#0<m ==> (m dvd n) = (zgcd(n,m) = m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
410 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
411 |
by (res_inst_tac [("n","zgcd(n,m)")] zdvd_trans 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
412 |
by (rtac zgcd_zdvd1 3); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
413 |
by (ALLGOALS Asm_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
414 |
by (rewtac dvd_def); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
415 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
416 |
qed "zdvd_iff_zgcd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
417 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
418 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
419 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
420 |
(** Congruences **) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
421 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
422 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
423 |
Goalw [zcong_def] "[a=b](mod #1)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
424 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
425 |
qed "zcong_1"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
426 |
Addsimps [zcong_1]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
427 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
428 |
Goalw [zcong_def] "[k = k] (mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
429 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
430 |
qed "zcong_refl"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
431 |
Addsimps [zcong_refl]; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
432 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
433 |
Goalw [zcong_def,dvd_def] "[a = b](mod m) = [b = a](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
434 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
435 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
436 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
437 |
qed "zcong_sym"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
438 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
439 |
Goalw [zcong_def] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
440 |
"[| [a = b] (mod m); [c = d] (mod m) |] ==> [a+c = b+d](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
441 |
by (res_inst_tac [("s","(a-b)+(c-d)")] subst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
442 |
by (rtac zdvd_zadd 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
443 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
444 |
qed "zcong_zadd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
445 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
446 |
Goalw [zcong_def] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
447 |
"[| [a = b] (mod m); [c = d] (mod m) |] ==> [a-c = b-d](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
448 |
by (res_inst_tac [("s","(a-b)-(c-d)")] subst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
449 |
by (rtac zdvd_zdiff 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
450 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
451 |
qed "zcong_zdiff"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
452 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
453 |
Goalw [zcong_def,dvd_def] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
454 |
"[| [a = b](mod m); [b = c](mod m) |] ==> [a = c](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
455 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
456 |
by (res_inst_tac [("x","k+ka")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
457 |
by (asm_full_simp_tac (simpset() addsimps zadd_ac@[zadd_zmult_distrib2]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
458 |
qed "zcong_trans"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
459 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
460 |
Goal "[| [a = b] (mod m); [c = d] (mod m) |] ==> [a*c = b*d](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
461 |
by (res_inst_tac [("b","b*c")] zcong_trans 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
462 |
by (rewtac zcong_def); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
463 |
by (res_inst_tac [("s","c*(a-b)")] subst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
464 |
by (res_inst_tac [("s","b*(c-d)")] subst 3); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
465 |
by (blast_tac (claset() addIs [zdvd_zmult]) 4); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
466 |
by (blast_tac (claset() addIs [zdvd_zmult]) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
467 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
468 |
zmult_commute]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
469 |
qed "zcong_zmult"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
470 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
471 |
Goal "[a = b] (mod m) ==> [a*k = b*k](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
472 |
by (rtac zcong_zmult 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
473 |
by (ALLGOALS Asm_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
474 |
qed "zcong_scalar"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
475 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
476 |
Goal "[a = b] (mod m) ==> [k*a = k*b](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
477 |
by (rtac zcong_zmult 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
478 |
by (ALLGOALS Asm_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
479 |
qed "zcong_scalar2"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
480 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
481 |
Goalw [zcong_def] "[a*m = b*m](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
482 |
by (rtac zdvd_zdiff 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
483 |
by (ALLGOALS Simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
484 |
qed "zcong_zmult_self"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
485 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
486 |
Goalw [zcong_def] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
487 |
"[| p:zprime; #0<a; [a*a = #1](mod p) |] \ |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
488 |
\ ==> [a=#1](mod p) | [a = p-#1](mod p)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
489 |
by (rtac zprime_zdvd_zmult 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
490 |
by (res_inst_tac [("s","a*a - #1 + p*(#1-a)")] subst 3); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
491 |
by (simp_tac (simpset() addsimps [zdvd_reduce]) 4); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
492 |
by (ALLGOALS (asm_simp_tac (simpset() |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
493 |
addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
494 |
qed "zcong_square"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
495 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
496 |
Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [a*k = b*k](mod m) = [a = b](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
497 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
498 |
by (blast_tac (claset() addIs [zcong_scalar]) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
499 |
by (case_tac "b<a" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
500 |
by (stac zcong_sym 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
501 |
by (rewrite_goals_tac [zcong_def]); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
502 |
by (ALLGOALS (rtac zrelprime_zdvd_zmult)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
503 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
504 |
by (subgoal_tac "m dvd (-(a*k - b*k))" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
505 |
by (asm_full_simp_tac (simpset() addsimps [zminus_zdiff_eq]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
506 |
by (stac zdvd_zminus_iff 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
507 |
by (assume_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
508 |
qed "zcong_cancel"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
509 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
510 |
Goal "[| #0<=m; zgcd(k,m) = #1 |] ==> [k*a = k*b](mod m) = [a = b](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
511 |
by (asm_simp_tac (simpset() addsimps [zmult_commute,zcong_cancel]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
512 |
qed "zcong_cancel2"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
513 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
514 |
Goalw [zcong_def,dvd_def] |
9943 | 515 |
"[| [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \ |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
516 |
\ ==> [a=b](mod m*n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
517 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
518 |
by (subgoal_tac "m dvd (n*ka)" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
519 |
by (subgoal_tac "m dvd ka" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
520 |
by (case_tac "#0<=ka" 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
521 |
by (stac (zdvd_zminus_iff RS sym) 3); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
522 |
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2); |
9943 | 523 |
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2); |
524 |
by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2); |
|
525 |
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2); |
|
526 |
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2); |
|
527 |
by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 2); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
528 |
by (rewtac dvd_def); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
529 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
530 |
by (res_inst_tac [("x","kc")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
531 |
by (res_inst_tac [("x","k")] exI 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
532 |
by (simp_tac (simpset() addsimps zmult_ac) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
533 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
534 |
qed "zcong_zgcd_zmult_zmod"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
535 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
536 |
Goalw [zcong_def,dvd_def] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
537 |
"[| #0<=a; a<m; #0<=b; b<m; [a = b] (mod m) |] ==> a = b"; |
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
538 |
by Auto_tac; |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
539 |
by (dres_inst_tac [("f", "%z. z mod m")] arg_cong 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
540 |
by (cut_inst_tac [("z","a"),("w","b")] zless_linear 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
541 |
by Auto_tac; |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
542 |
by (subgoal_tac "(a - b) mod m = a-b" 2); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
543 |
by (rtac mod_pos_pos_trivial 3); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
544 |
by Auto_tac; |
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
545 |
by (subgoal_tac "(m + (a - b)) mod m = m + (a - b)" 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
546 |
by (rtac mod_pos_pos_trivial 2); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
547 |
by Auto_tac; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
548 |
qed "zcong_zless_imp_eq"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
549 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
550 |
Goal "[| p:zprime; #0<a; a<p; [a*a = #1](mod p) |] ==> a = #1 | a = p-#1"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
551 |
by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
552 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
553 |
by (res_inst_tac [("Pa","a=p-#1")] swap 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
554 |
by (rtac zcong_zless_imp_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
555 |
by (rtac zcong_zless_imp_eq 7); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
556 |
by (rewtac zprime_def); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
557 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
558 |
qed "zcong_square_zless"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
559 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
560 |
Goalw [zcong_def] "[| #0<a; a<m; #0<b; b<a |] ==> ~[a = b] (mod m) "; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
561 |
by (rtac zdvd_not_zless 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
562 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
563 |
qed "zcong_not"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
564 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
565 |
Goalw [zcong_def,dvd_def] "[| #0<=a; a<m; [a=#0](mod m) |] ==> a = #0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
566 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
567 |
by (subgoal_tac "#0<m" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
568 |
by (rotate_tac ~1 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
569 |
by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
570 |
by (subgoal_tac "m*k<m*#1" 1); |
9634
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
571 |
by (dtac (zmult_zless_cancel1 RS iffD1) 1); |
61b57cc1cb5a
modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents:
9508
diff
changeset
|
572 |
by Auto_tac; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
573 |
qed "zcong_zless_0"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
574 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
575 |
Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
576 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
577 |
by (subgoal_tac "[b = y] (mod m)" 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
578 |
by (case_tac "b=#0" 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
579 |
by (case_tac "y=#0" 3); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
580 |
by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0, |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
581 |
zcong_zless_imp_eq,zle_neq_implies_zless], |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
582 |
simpset() addsimps [zcong_sym])); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
583 |
by (rewrite_goals_tac [zcong_def,dvd_def]); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
584 |
by (res_inst_tac [("x","a mod m")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
585 |
by (auto_tac (claset(),simpset() addsimps [pos_mod_sign,pos_mod_bound])); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
586 |
by (res_inst_tac [("x","-(a div m)")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
587 |
by (cut_inst_tac [("a","a"),("b","m")] zmod_zdiv_equality 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
588 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
589 |
qed "zcong_zless_unique"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
590 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
591 |
Goalw [zcong_def,dvd_def] "([a = b] (mod m)) = (EX k. b = a + m*k)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
592 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
593 |
by (ALLGOALS (res_inst_tac [("x","-k")] exI)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
594 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
595 |
qed "zcong_iff_lin"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
596 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
597 |
Goal "[| #0<m; zgcd(a,m) = #1; [a = b] (mod m) |] ==> zgcd(b,m) = #1"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
598 |
by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin])); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
599 |
qed "zgcd_zcong_zgcd"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
600 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
601 |
Goal "[| a=c; b=d |] ==> a-b = c-(d::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
602 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
603 |
val lemma = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
604 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
605 |
Goal "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
606 |
by (res_inst_tac [("s","(m * (a div m) + a mod m) - \ |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
607 |
\ (m * (b div m) + b mod m)")] trans 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
608 |
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
609 |
by (rtac lemma 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
610 |
by (ALLGOALS (rtac zmod_zdiv_equality)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
611 |
val lemma = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
612 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
613 |
Goalw [zcong_def] "[a = b] (mod m) = [a mod m = b mod m](mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
614 |
by (res_inst_tac [("t","a-b")] ssubst 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
615 |
by (res_inst_tac [("m","m")] lemma 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
616 |
by (rtac trans 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
617 |
by (res_inst_tac [("k","m"),("m","a div m - b div m")] zdvd_reduce 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
618 |
by (simp_tac (simpset() addsimps [zadd_commute]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
619 |
qed "zcong_zmod"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
620 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
621 |
Goal "#0<m ==> [a = b] (mod m) = (a mod m = b mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
622 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
623 |
by (res_inst_tac [("m","m")] zcong_zless_imp_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
624 |
by (stac (zcong_zmod RS sym) 5); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
625 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
626 |
by (rewrite_goals_tac [zcong_def,dvd_def]); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
627 |
by (res_inst_tac [("x","a div m - b div m")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
628 |
by (res_inst_tac [("m1","m")] (lemma RS trans) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
629 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
630 |
qed "zcong_zmod_eq"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
631 |
|
9943 | 632 |
Goal "[a = b] (mod -m) = [a = b] (mod m)"; |
633 |
by (auto_tac (claset(), simpset() addsimps [zcong_def])); |
|
634 |
qed "zcong_zminus"; |
|
635 |
AddIffs [zcong_zminus]; |
|
636 |
||
637 |
Goal "[a = b] (mod #0) = (a = b)"; |
|
638 |
by (auto_tac (claset(), simpset() addsimps [zcong_def])); |
|
639 |
qed "zcong_zero"; |
|
640 |
AddIffs [zcong_zero]; |
|
641 |
||
642 |
Goal "[a = b] (mod m) = (a mod m = b mod m)"; |
|
643 |
by (zdiv_undefined_case_tac "m = #0" 1); |
|
644 |
by (case_tac "#0<m" 1); |
|
645 |
by (asm_simp_tac (simpset() addsimps [zcong_zmod_eq]) 1); |
|
646 |
by (res_inst_tac [("t","m")] (zminus_zminus RS subst) 1); |
|
647 |
by (stac zcong_zminus 1); |
|
648 |
by (stac zcong_zmod_eq 1); |
|
649 |
by (arith_tac 1); |
|
650 |
(*FIXME: finish this proof?*) |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
651 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
652 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
653 |
(** Modulo **) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
654 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
655 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
656 |
Goalw [dvd_def] "[| #0<(m::int); m dvd b |] ==> (a mod b mod m) = (a mod m)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
657 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
658 |
by (stac (zcong_zmod_eq RS sym) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
659 |
by (stac zcong_iff_lin 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
660 |
by (res_inst_tac [("x","k*(a div (m*k))")] exI 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
661 |
by (stac zadd_commute 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
662 |
by (stac (zmult_assoc RS sym) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
663 |
by (rtac zmod_zdiv_equality 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
664 |
by (assume_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
665 |
qed "zmod_zdvd_zmod"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
666 |
|
9943 | 667 |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
668 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
669 |
(** Extended GCD **) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
670 |
(************************************************) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
671 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
672 |
val [xzgcda_eq] = xzgcda.simps; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
673 |
Delsimps xzgcda.simps; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
674 |
|
9943 | 675 |
Goal "zgcd(r',r) = k --> #0 < r \\<longrightarrow> \ |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
676 |
\ (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
677 |
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
678 |
("y","s'"),("z","s"),("aa","t'"),("ab","t")] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
679 |
xzgcda.induct 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
680 |
by (stac zgcd_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
681 |
by (stac xzgcda_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
682 |
by Auto_tac; |
9943 | 683 |
by (case_tac "r' mod r = #0" 1); |
684 |
by (forw_inst_tac [("a","r'")] pos_mod_sign 2); |
|
685 |
by Auto_tac; |
|
686 |
by (arith_tac 2); |
|
687 |
by (rtac exI 1); |
|
688 |
by (rtac exI 1); |
|
689 |
by (stac xzgcda_eq 1); |
|
690 |
by Auto_tac; |
|
691 |
by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
692 |
val lemma1 = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
693 |
|
9943 | 694 |
Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r \\<longrightarrow> \ |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
695 |
\ zgcd(r',r) = k"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
696 |
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
697 |
("y","s'"),("z","s"),("aa","t'"),("ab","t")] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
698 |
xzgcda.induct 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
699 |
by (stac zgcd_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
700 |
by (stac xzgcda_eq 1); |
9943 | 701 |
by (auto_tac (claset(), simpset() addsimps [linorder_not_le])); |
702 |
by (case_tac "r' mod r = #0" 1); |
|
703 |
by (forw_inst_tac [("a","r'")] pos_mod_sign 2); |
|
704 |
by Auto_tac; |
|
705 |
by (arith_tac 2); |
|
706 |
by (eres_inst_tac [("P","xzgcda ?u = ?v")] rev_mp 1); |
|
707 |
by (stac xzgcda_eq 1); |
|
708 |
by Auto_tac; |
|
709 |
by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
710 |
val lemma2 = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
711 |
|
9943 | 712 |
Goalw [xzgcd_def] "#0 < n \\<Longrightarrow> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
713 |
by (rtac iffI 1); |
9943 | 714 |
by (rtac (lemma2 RS mp RS mp) 2); |
715 |
by (rtac (lemma1 RS mp RS mp) 1); |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
716 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
717 |
qed "xzgcd_correct"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
718 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
719 |
(* xzgcd linear *) |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
720 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
721 |
Goal "(a-r*b)*m + (c-r*d)*(n::int) = (a*m + c*n) - r*(b*m + d*n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
722 |
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib,zadd_zmult_distrib2, |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
723 |
zmult_assoc]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
724 |
val lemma = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
725 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
726 |
Goal "[| r' = s'*m + t'*n; r = s*m + t*n |] \ |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
727 |
\ ==> (r' mod r) = (s' - (r' div r)*s)*m + (t' - (r' div r)*t)*(n::int)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
728 |
by (rtac trans 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
729 |
by (rtac (lemma RS sym) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
730 |
by (Asm_simp_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
731 |
by (stac eq_zdiff_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
732 |
by (rtac (trans RS sym) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
733 |
by (res_inst_tac [("b","s*m + t*n")] zmod_zdiv_equality 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
734 |
by (simp_tac (simpset() addsimps [zmult_commute]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
735 |
val lemma = result(); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
736 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
737 |
Goal "#0<r --> xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \ |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
738 |
\ --> r' = s'*m + t'*n --> r = s*m + t*n --> rn = sn*m + tn*n"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
739 |
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"), |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
740 |
("y","s'"),("z","s"),("aa","t'"),("ab","t")] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
741 |
xzgcda.induct 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
742 |
by (stac xzgcda_eq 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
743 |
by (Simp_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
744 |
by (REPEAT (rtac impI 1)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
745 |
by (case_tac "r' mod r = #0" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
746 |
by (asm_full_simp_tac (simpset() addsimps [xzgcda_eq]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
747 |
by (SELECT_GOAL Safe_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
748 |
by (subgoal_tac "#0 < r' mod r" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
749 |
by (rtac zle_neq_implies_zless 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
750 |
by (rtac pos_mod_sign 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
751 |
by (cut_inst_tac [("m","m"),("n","n"),("r'","r'"),("r","r"), |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
752 |
("s'","s'"),("s","s"),("t'","t'"),("t","t")] |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
753 |
lemma 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
754 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
755 |
qed_spec_mp "xzgcda_linear"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
756 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
757 |
Goalw [xzgcd_def] "[| #0<n; xzgcd m n = (r,s,t) |] ==> r = s*m + t*n"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
758 |
by (etac xzgcda_linear 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
759 |
by (assume_tac 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
760 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
761 |
qed "xzgcd_linear"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
762 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
763 |
Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)"; |
9943 | 764 |
by (asm_full_simp_tac (simpset() addsimps [xzgcd_correct]) 1); |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
765 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
766 |
by (REPEAT (rtac exI 1)); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
767 |
by (etac xzgcd_linear 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
768 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
769 |
qed "zgcd_ex_linear"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
770 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
771 |
Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX x. [a*x = #1](mod n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
772 |
by (cut_inst_tac [("m","a"),("n","n"),("k","#1")] zgcd_ex_linear 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
773 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
774 |
by (res_inst_tac [("x","s")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
775 |
by (res_inst_tac [("b","s*a+t*n")] zcong_trans 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
776 |
by (Asm_simp_tac 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
777 |
by (rewtac zcong_def); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
778 |
by (simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
779 |
qed "zcong_lineq_ex"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
780 |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
781 |
Goal "[| #0<n; zgcd(a,n) = #1 |] ==> EX! x. #0<=x & x<n & [a*x = b](mod n)"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
782 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
783 |
by (rtac zcong_zless_imp_eq 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
784 |
by (stac (zcong_cancel2 RS sym) 6); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
785 |
by (rtac zcong_trans 8); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
786 |
by (ALLGOALS Asm_simp_tac); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
787 |
by (asm_full_simp_tac (simpset() addsimps [zcong_sym]) 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
788 |
by (cut_inst_tac [("a","a"),("n","n")] zcong_lineq_ex 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
789 |
by Auto_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
790 |
by (res_inst_tac [("x","x*b mod n")] exI 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
791 |
by Safe_tac; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
792 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_bound,pos_mod_sign]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
793 |
by (stac zcong_zmod 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
794 |
by (stac (zmod_zmult1_eq RS sym) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
795 |
by (stac (zcong_zmod RS sym) 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
796 |
by (subgoal_tac "[a*x*b = #1*b](mod n)" 1); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
797 |
by (rtac zcong_zmult 2); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
798 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_assoc]))); |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
799 |
qed "zcong_lineq_unique"; |
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
800 |