src/HOL/NumberTheory/IntPrimes.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10198 2b255b772585
child 10658 b9d43a2add79
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
     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
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
     9
Comparable to Primes theory, but dvd is included here as it is not present in
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    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
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    16
Goal "(abs (z::int) = w) = (z=w & #0 <= z | z=-w & z < #0)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    17
by (auto_tac (claset(), simpset() addsimps [zabs_def]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    18
qed "zabs_eq_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    19
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    20
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    21
(** gcd lemmas **)
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    22
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    23
val gcd_non_0 = thm "gcd_non_0";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    24
val gcd_add1 = thm "gcd_add1";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    25
val gcd_commute = thm "gcd_commute";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    26
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    27
Goal "gcd (m+k, k) = gcd (m+k, m)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    28
by (simp_tac (simpset() addsimps [gcd_commute]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    29
qed "gcd_add1_eq";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    30
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9969
diff changeset
    31
Goal "m <= n ==> gcd (n, n - m) = gcd (n, m)";
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    32
by (subgoal_tac "n = m + (n-m)" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    33
by (etac ssubst 1 THEN rtac gcd_add1_eq 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    34
by (Asm_simp_tac 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    35
qed "gcd_diff2";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    36
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    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
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    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
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
    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)";
10198
paulson
parents: 10142
diff changeset
   149
by (auto_tac (claset(), simpset() addsimps [zmod_zmult_self2]));  
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   150
qed "zdvd_iff_zmod_eq_0";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   151
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   152
Goal "[| ~k<#0; k~=#0 |] ==> #0<(k::int)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   153
by (arith_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   154
val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   155
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   156
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
   157
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   158
by (subgoal_tac "#0<n" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   159
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
   160
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
   161
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
   162
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
   163
by Auto_tac;  
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   164
qed "zdvd_not_zless";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   165
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   166
Goal "(int m dvd z) = (m dvd nat(abs z))";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   167
by (auto_tac (claset(), 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   168
       simpset() addsimps [dvd_def, nat_abs_mult_distrib]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   169
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, zabs_eq_iff]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   170
by (res_inst_tac [("x","-(int k)")] exI 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   171
by (auto_tac (claset(), simpset() addsimps [zmult_int RS sym]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   172
qed "int_dvd_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   173
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   174
Goal "(z dvd int m) = (nat(abs z) dvd m)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   175
by (auto_tac (claset(), 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   176
       simpset() addsimps [dvd_def, zabs_def, zmult_int RS sym]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   177
by (res_inst_tac [("x","nat k")] exI 3); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   178
by (res_inst_tac [("x","-(int k)")] exI 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   179
by (res_inst_tac [("x","nat (-k)")] exI 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   180
by (cut_inst_tac [("k","m")] int_less_0_conv 3);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   181
by (cut_inst_tac [("k","m")] int_less_0_conv 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   182
by (auto_tac (claset(), 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   183
         simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   184
                             nat_mult_distrib RS sym, nat_eq_iff2]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   185
qed "dvd_int_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   186
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   187
Goal "(nat z dvd m) = (if #0 <= z then (z dvd int m) else m=0)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   188
by (auto_tac (claset(), simpset() addsimps [dvd_def, zmult_int RS sym]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   189
by (res_inst_tac [("x","nat k")] exI 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   190
by (cut_inst_tac [("k","m")] int_less_0_conv 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   191
by (auto_tac (claset(), 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   192
         simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   193
                             nat_mult_distrib RS sym, nat_eq_iff2]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   194
qed "nat_dvd_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   195
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   196
Goal "(-z dvd w) = (z dvd (w::int))";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   197
by (auto_tac (claset(), simpset() addsimps [dvd_def]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   198
by (ALLGOALS (res_inst_tac [("x","-k")] exI));
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   199
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   200
qed "zminus_dvd_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   201
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   202
Goal "(z dvd -w) = (z dvd (w::int))";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   203
by (auto_tac (claset(), simpset() addsimps [dvd_def]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   204
by (dtac (zminus_equation RS iffD1) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   205
by (ALLGOALS (res_inst_tac [("x","-k")] exI));
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   206
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   207
qed "dvd_zminus_iff";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   208
AddIffs [zminus_dvd_iff, dvd_zminus_iff];
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   209
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   210
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   211
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   212
(** Euclid's Algorithm and GCD                 **)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   213
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   214
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   215
Goal "zgcd(m,#0) = abs m";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   216
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
   217
qed "zgcd_0";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   218
Addsimps [zgcd_0];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   219
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   220
Goal"zgcd(#0,m) = abs m";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   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_left";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   223
Addsimps [zgcd_0_left];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   224
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   225
Goal "zgcd(-m,n) = zgcd(m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   226
by (simp_tac (simpset() addsimps [zgcd_def]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   227
qed "zgcd_zminus";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   228
Addsimps [zgcd_zminus];
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   229
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   230
Goal "zgcd(m,-n) = zgcd(m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   231
by (simp_tac (simpset() addsimps [zgcd_def]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   232
qed "zgcd_zminus2";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   233
Addsimps [zgcd_zminus2];
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   234
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   235
Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)";
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   236
by (forw_inst_tac [("b","n"), ("a","m")] pos_mod_sign 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   237
by (asm_simp_tac (simpset() addsimps [zgcd_def, zabs_def, nat_mod_distrib]) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   238
by (cut_inst_tac [("a","-m"),("b","n")] zmod_zminus1_eq_if 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   239
by (auto_tac (claset(), 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   240
              simpset() addsimps [gcd_non_0, nat_mod_distrib RS sym,
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   241
                                  zmod_zminus1_eq_if]));
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   242
by (forw_inst_tac [("a","m")] pos_mod_bound 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   243
by (asm_simp_tac (simpset() addsimps [nat_diff_distrib]) 1);  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   244
by (rtac gcd_diff2 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   245
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
   246
qed "zgcd_non_0";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   247
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   248
Goal "zgcd(m,n) = zgcd (n, m mod n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   249
by (zdiv_undefined_case_tac "n = #0" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   250
by (auto_tac
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   251
    (claset(),
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   252
     simpset() addsimps [linorder_neq_iff, zgcd_non_0]));
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   253
by (cut_inst_tac [("m","-m"),("n","-n")] zgcd_non_0 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   254
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   255
qed "zgcd_eq";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   256
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   257
Goal "zgcd(m,#1) = #1";
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   258
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
   259
qed "zgcd_1";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   260
Addsimps [zgcd_1];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   261
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   262
Goal "(zgcd(#0,m) = #1) = (abs m = #1)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   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_0_1_iff";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   265
Addsimps [zgcd_0_1_iff];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   266
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   267
Goal "zgcd(m,n) dvd m";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   268
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   269
qed "zgcd_zdvd1";
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   270
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   271
Goal "zgcd(m,n) dvd n";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   272
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   273
qed "zgcd_zdvd2";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   274
AddIffs [zgcd_zdvd1, zgcd_zdvd2];
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   275
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   276
Goal "k dvd zgcd(m,n) = (k dvd m & k dvd n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   277
by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff, 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   278
                                  dvd_int_iff, nat_dvd_iff]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   279
qed "zgcd_greatest_iff";
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   280
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   281
Goal "zgcd(m,n) = zgcd(n,m)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   282
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
   283
qed "zgcd_commute";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   284
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   285
Goal "zgcd(#1,m) = #1";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   286
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
   287
qed "zgcd_1_left";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   288
Addsimps [zgcd_1_left];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   289
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   290
Goal "zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   291
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
   292
qed "zgcd_assoc";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   293
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   294
Goal "zgcd(k,zgcd(m,n)) = zgcd(m,zgcd(k,n))";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   295
by (rtac (zgcd_commute RS trans) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   296
by (rtac (zgcd_assoc RS trans) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   297
by (rtac (zgcd_commute RS arg_cong) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   298
qed "zgcd_left_commute";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   299
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   300
(*Addition is an AC-operator*)
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   301
bind_thms ("zgcd_ac", [zgcd_assoc, zgcd_commute, zgcd_left_commute]);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   302
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   303
val gcd_mult_distrib2 = thm"gcd_mult_distrib2";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   304
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   305
Goal "#0<=k ==> k * zgcd(m,n) = zgcd(k*m, k*n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   306
by (asm_simp_tac 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   307
    (simpset() delsimps [zmult_zminus_right] 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   308
	       addsimps [zmult_zminus_right RS sym, 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   309
                         nat_mult_distrib, zgcd_def, zabs_def, 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   310
                         zmult_less_0_iff, gcd_mult_distrib2 RS sym, 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   311
                         zmult_int RS sym]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   312
qed "zgcd_zmult_distrib2";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   313
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   314
Goal "zgcd(k*m, k*n) = abs k * zgcd(m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   315
by (simp_tac (simpset() addsimps [zabs_def, zgcd_zmult_distrib2]) 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   316
qed "zgcd_zmult_distrib2_abs";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   317
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   318
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   319
Goal "#0<=m ==> zgcd(m,m) = m";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   320
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
   321
by (ALLGOALS Asm_full_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   322
qed "zgcd_self";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   323
Addsimps [zgcd_self];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   324
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   325
Goal "#0<=k ==> zgcd(k, k*n) = k";
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   326
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
   327
by (ALLGOALS Asm_full_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   328
qed "zgcd_zmult_eq_self";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   329
Addsimps [zgcd_zmult_eq_self];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   330
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   331
Goal "#0<=k ==> zgcd(k*n, k) = k";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   332
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
   333
by (ALLGOALS Asm_full_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   334
qed "zgcd_zmult_eq_self2";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   335
Addsimps [zgcd_zmult_eq_self2];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   336
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   337
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
   338
by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   339
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
   340
by (ALLGOALS (asm_simp_tac (simpset() 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   341
      addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   342
val lemma = result();
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   343
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   344
Goal "[| zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   345
by (case_tac "#0 <= m" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   346
by (blast_tac (claset() addIs [lemma]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   347
by (subgoal_tac "k dvd -m" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   348
by (rtac lemma 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   349
by Auto_tac;  
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   350
qed "zrelprime_zdvd_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   351
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   352
Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #1";
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   353
by Auto_tac;  
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   354
qed "zprime_imp_zrelprime";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   355
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   356
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
   357
by (etac zprime_imp_zrelprime 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   358
by (etac zdvd_not_zless 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   359
by (assume_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   360
qed "zless_zprime_imp_zrelprime";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   361
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   362
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
   363
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   364
by (rtac zrelprime_zdvd_zmult 1);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   365
by (rtac zprime_imp_zrelprime 1);
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   366
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   367
qed "zprime_zdvd_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   368
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   369
val gcd_add_mult = thm "gcd_add_mult";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   370
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   371
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
   372
by (rtac (zgcd_eq RS trans) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   373
by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   374
by (rtac (zgcd_eq RS sym) 1);
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   375
qed "zgcd_zadd_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   376
Addsimps [zgcd_zadd_zmult];
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   377
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   378
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   379
Goal "zgcd(m,n) dvd zgcd(k*m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   380
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   381
by (blast_tac (claset() addIs [zdvd_trans]) 1); 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   382
qed "zgcd_zdvd_zgcd_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   383
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   384
Goal "zgcd(k,n) = #1 ==> zgcd(k*m,n) dvd zgcd(m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   385
by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   386
by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   387
by (simp_tac (simpset() addsimps [zmult_commute]) 2); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   388
by (subgoal_tac "zgcd (k, zgcd (k * m, n)) =  zgcd (k * m, zgcd (k, n))" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   389
by (Asm_full_simp_tac 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   390
by (simp_tac (simpset() addsimps zgcd_ac) 1); 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   391
qed "zgcd_zmult_zdvd_zgcd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   392
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   393
val gcd_mult_cancel = thm "gcd_mult_cancel";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   394
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   395
Goal "zgcd(k,n) = #1 ==> zgcd(k*m, n) = zgcd(m,n)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   396
by (asm_full_simp_tac (simpset() addsimps [zgcd_def, 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   397
                           nat_abs_mult_distrib, gcd_mult_cancel]) 1); 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   398
qed "zgcd_zmult_cancel";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   399
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   400
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
   401
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
   402
qed "zgcd_zgcd_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   403
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   404
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
   405
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   406
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
   407
by (rtac zgcd_zdvd1 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   408
by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   409
by (rewtac dvd_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   410
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   411
qed "zdvd_iff_zgcd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   412
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   413
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   414
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   415
(** Congruences                                **)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   416
(************************************************)
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
Goalw [zcong_def] "[a=b](mod #1)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   419
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   420
qed "zcong_1";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   421
Addsimps [zcong_1];
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] "[k = k] (mod m)";
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_refl";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   426
Addsimps [zcong_refl];
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,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
   429
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   430
by (ALLGOALS (res_inst_tac [("x","-k")] exI));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   431
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   432
qed "zcong_sym";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   433
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   434
Goalw [zcong_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   435
     "[| [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
   436
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
   437
by (rtac zdvd_zadd 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   438
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   439
qed "zcong_zadd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   440
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   441
Goalw [zcong_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   442
     "[| [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
   443
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
   444
by (rtac zdvd_zdiff 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   445
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   446
qed "zcong_zdiff";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   447
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   448
Goalw [zcong_def,dvd_def]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   449
     "[| [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
   450
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   451
by (res_inst_tac [("x","k+ka")] exI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   452
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
   453
qed "zcong_trans";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   454
 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   455
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
   456
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
   457
by (rewtac zcong_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   458
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
   459
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
   460
by (blast_tac (claset() addIs [zdvd_zmult]) 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   461
by (blast_tac (claset() addIs [zdvd_zmult]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   462
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
   463
                                                zmult_commute])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   464
qed "zcong_zmult";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   465
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   466
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
   467
by (rtac zcong_zmult 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   468
by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   469
qed "zcong_scalar";
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) ==> [k*a = k*b](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_scalar2";
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
Goalw [zcong_def] "[a*m = b*m](mod m)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   477
by (rtac zdvd_zdiff 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   478
by (ALLGOALS Simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   479
qed "zcong_zmult_self";
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]
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   482
      "[| p:zprime; #0<a; [a*a = #1](mod p) |] \
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   483
\     ==> [a=#1](mod p) | [a = p-#1](mod p)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   484
by (rtac zprime_zdvd_zmult 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   485
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
   486
by (simp_tac (simpset() addsimps [zdvd_reduce]) 4);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   487
by (ALLGOALS (asm_simp_tac (simpset() 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   488
      addsimps [zdiff_zmult_distrib,zmult_commute,zdiff_zmult_distrib2])));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   489
qed "zcong_square";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   490
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   491
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
   492
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   493
by (blast_tac (claset() addIs [zcong_scalar]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   494
by (case_tac "b<a" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   495
by (stac zcong_sym 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   496
by (rewrite_goals_tac [zcong_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   497
by (ALLGOALS (rtac zrelprime_zdvd_zmult));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   498
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
   499
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
   500
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
   501
by (stac zdvd_zminus_iff 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   502
by (assume_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   503
qed "zcong_cancel";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   504
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   505
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
   506
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
   507
qed "zcong_cancel2";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   509
Goalw [zcong_def,dvd_def]
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   510
      "[| [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
   511
\     ==> [a=b](mod m*n)";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   512
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   513
by (subgoal_tac "m dvd (n*ka)" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   514
by (subgoal_tac "m dvd ka" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   515
by (case_tac "#0<=ka" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   516
by (stac (zdvd_zminus_iff RS sym) 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   517
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   518
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   519
by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   520
by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   521
by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   522
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
   523
by (rewtac dvd_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   524
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   525
by (res_inst_tac [("x","kc")] exI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   526
by (res_inst_tac [("x","k")] exI 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   527
by (simp_tac (simpset() addsimps zmult_ac) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   528
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   529
qed "zcong_zgcd_zmult_zmod";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   530
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   531
Goalw [zcong_def,dvd_def] 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   532
      "[| #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
   533
by Auto_tac;  
61b57cc1cb5a modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents: 9508
diff changeset
   534
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
   535
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
   536
by Auto_tac;  
61b57cc1cb5a modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents: 9508
diff changeset
   537
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
   538
by (rtac mod_pos_pos_trivial 3); 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   539
by Auto_tac;
9634
61b57cc1cb5a modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents: 9508
diff changeset
   540
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
   541
by (rtac mod_pos_pos_trivial 2); 
61b57cc1cb5a modified proofs: better rules for cancellation of common factors across comparisons
paulson
parents: 9508
diff changeset
   542
by Auto_tac;  
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   543
qed "zcong_zless_imp_eq";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   544
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   545
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
   546
by (cut_inst_tac [("p","p"),("a","a")] zcong_square 1);
10198
paulson
parents: 10142
diff changeset
   547
by (full_simp_tac (simpset() addsimps [zprime_def]) 1); 
paulson
parents: 10142
diff changeset
   548
by (auto_tac (claset() addIs [zcong_zless_imp_eq], simpset())); 
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   549
qed "zcong_square_zless";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   550
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   551
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
   552
by (rtac zdvd_not_zless 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   553
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   554
qed "zcong_not";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   555
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   556
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
   557
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   558
by (subgoal_tac "#0<m" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   559
by (rotate_tac ~1 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   560
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
   561
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
   562
by (dtac (zmult_zless_cancel1 RS iffD1) 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9943
diff changeset
   563
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   564
qed "zcong_zless_0";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   565
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   566
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
   567
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   568
by (subgoal_tac "[b = y] (mod m)" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   569
by (case_tac "b=#0" 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   570
by (case_tac "y=#0" 3);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   571
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
   572
                              zcong_zless_imp_eq,zle_neq_implies_zless],
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   573
              simpset() addsimps [zcong_sym]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   574
by (rewrite_goals_tac [zcong_def,dvd_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   575
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
   576
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
   577
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
   578
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
   579
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   580
qed "zcong_zless_unique";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   581
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   582
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
   583
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   584
by (ALLGOALS (res_inst_tac [("x","-k")] exI));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   585
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   586
qed "zcong_iff_lin";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   587
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   588
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
   589
by (auto_tac (claset(),simpset() addsimps [zcong_iff_lin]));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   590
qed "zgcd_zcong_zgcd";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   591
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   592
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
   593
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   594
val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   595
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   596
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
   597
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
   598
\                 (m * (b div m) + b mod m)")] trans 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   599
by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   600
by (rtac lemma 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   601
by (ALLGOALS (rtac zmod_zdiv_equality));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   602
val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   603
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   604
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
   605
by (res_inst_tac [("t","a-b")] ssubst 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   606
by (res_inst_tac [("m","m")] lemma 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   607
by (rtac trans 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   608
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
   609
by (simp_tac (simpset() addsimps [zadd_commute]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   610
qed "zcong_zmod";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   611
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   612
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
   613
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   614
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
   615
by (stac (zcong_zmod RS sym) 5);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   616
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
   617
by (rewrite_goals_tac [zcong_def,dvd_def]);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   618
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
   619
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
   620
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   621
qed "zcong_zmod_eq";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   622
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   623
Goal "[a = b] (mod -m) = [a = b] (mod m)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   624
by (auto_tac (claset(), simpset() addsimps [zcong_def]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   625
qed "zcong_zminus";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   626
AddIffs [zcong_zminus];
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   627
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   628
Goal "[a = b] (mod #0) = (a = b)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   629
by (auto_tac (claset(), simpset() addsimps [zcong_def]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   630
qed "zcong_zero";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   631
AddIffs [zcong_zero];
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   632
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   633
Goal "[a = b] (mod m) = (a mod m = b mod m)";
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   634
by (zdiv_undefined_case_tac "m = #0" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   635
by (case_tac "#0<m" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   636
by (asm_simp_tac (simpset() addsimps [zcong_zmod_eq]) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   637
by (res_inst_tac [("t","m")] (zminus_zminus RS subst) 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   638
by (stac zcong_zminus 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   639
by (stac zcong_zmod_eq 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   640
by (arith_tac 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   641
(*FIXME: finish this proof?*)
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   642
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   643
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   644
(** Modulo                                     **)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   645
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   646
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   647
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
   648
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   649
by (stac (zcong_zmod_eq RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   650
by (stac zcong_iff_lin 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   651
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
   652
by (stac zadd_commute 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   653
by (stac (zmult_assoc RS sym) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   654
by (rtac zmod_zdiv_equality 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   655
by (assume_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   656
qed "zmod_zdvd_zmod";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   657
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   658
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   659
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   660
(** Extended GCD                               **)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   661
(************************************************)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   662
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   663
val [xzgcda_eq] = xzgcda.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   664
Delsimps xzgcda.simps;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   665
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9969
diff changeset
   666
Goal "zgcd(r',r) = k --> #0 < r --> \
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   667
\     (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
   668
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
   669
                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   670
                  xzgcda.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   671
by (stac zgcd_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   672
by (stac xzgcda_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   673
by Auto_tac;
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   674
by (case_tac "r' mod r = #0" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   675
by (forw_inst_tac [("a","r'")] pos_mod_sign 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   676
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   677
by (arith_tac 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   678
by (rtac exI 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   679
by (rtac exI 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   680
by (stac xzgcda_eq 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   681
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   682
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
   683
val lemma1 = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   684
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9969
diff changeset
   685
Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r --> \
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   686
\     zgcd(r',r) = k";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   687
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
   688
                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   689
                  xzgcda.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   690
by (stac zgcd_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   691
by (stac xzgcda_eq 1);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   692
by (auto_tac (claset(), simpset() addsimps [linorder_not_le]));  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   693
by (case_tac "r' mod r = #0" 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   694
by (forw_inst_tac [("a","r'")] pos_mod_sign 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   695
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   696
by (arith_tac 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   697
by (eres_inst_tac [("P","xzgcda ?u = ?v")] rev_mp 1); 
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   698
by (stac xzgcda_eq 1);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   699
by Auto_tac;  
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   700
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
   701
val lemma2 = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   702
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9969
diff changeset
   703
Goalw [xzgcd_def] "#0 < n ==> (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
   704
by (rtac iffI 1);
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   705
by (rtac (lemma2 RS mp RS mp) 2);
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   706
by (rtac (lemma1 RS mp RS mp) 1);
9508
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   707
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   708
qed "xzgcd_correct";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   709
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   710
(* xzgcd linear *)
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   711
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   712
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
   713
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
   714
                                  zmult_assoc]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   715
val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   716
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   717
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
   718
\    ==> (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
   719
by (rtac trans 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   720
by (rtac (lemma RS sym) 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   721
by (Asm_simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   722
by (stac eq_zdiff_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   723
by (rtac (trans RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   724
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
   725
by (simp_tac (simpset() addsimps [zmult_commute]) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   726
val lemma = result();
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   727
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   728
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
   729
\          --> 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
   730
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
   731
                  ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   732
                  xzgcda.induct 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   733
by (stac xzgcda_eq 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   734
by (Simp_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   735
by (REPEAT (rtac impI 1));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   736
by (case_tac "r' mod r = #0" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   737
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
   738
by (SELECT_GOAL Safe_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   739
by (subgoal_tac "#0 < r' mod r" 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   740
by (rtac zle_neq_implies_zless 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   741
by (rtac pos_mod_sign 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   742
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
   743
                  ("s'","s'"),("s","s"),("t'","t'"),("t","t")] 
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   744
                 lemma 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   745
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   746
qed_spec_mp "xzgcda_linear";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   747
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   748
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
   749
by (etac xzgcda_linear 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   750
by (assume_tac 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   751
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   752
qed "xzgcd_linear";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   753
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   754
Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)";
9943
55c82decf3f4 zgcd now works for negative integers
paulson
parents: 9747
diff changeset
   755
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
   756
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   757
by (REPEAT (rtac exI 1));
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   758
by (etac xzgcd_linear 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   759
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   760
qed "zgcd_ex_linear";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   761
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   762
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
   763
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
   764
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   765
by (res_inst_tac [("x","s")] exI 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   766
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
   767
by (Asm_simp_tac 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   768
by (rewtac zcong_def);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   769
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
   770
qed "zcong_lineq_ex";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   771
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   772
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
   773
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   774
by (rtac zcong_zless_imp_eq 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   775
by (stac (zcong_cancel2 RS sym) 6);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   776
by (rtac zcong_trans 8);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   777
by (ALLGOALS Asm_simp_tac);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   778
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
   779
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
   780
by Auto_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   781
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
   782
by Safe_tac;
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   783
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
   784
by (stac zcong_zmod 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   785
by (stac (zmod_zmult1_eq RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   786
by (stac (zcong_zmod RS sym) 1);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   787
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
   788
by (rtac zcong_zmult 2);
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   789
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
   790
qed "zcong_lineq_unique";
4d01dbf6ded7 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff changeset
   791