zgcd now works for negative integers
authorpaulson
Wed Sep 13 18:46:09 2000 +0200 (2000-09-13)
changeset 994355c82decf3f4
parent 9942 87f0809a06a9
child 9944 2a705d1af4dc
zgcd now works for negative integers
src/HOL/NumberTheory/Chinese.ML
src/HOL/NumberTheory/EulerFermat.ML
src/HOL/NumberTheory/IntPrimes.ML
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/WilsonBij.ML
     1.1 --- a/src/HOL/NumberTheory/Chinese.ML	Wed Sep 13 18:45:10 2000 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.ML	Wed Sep 13 18:46:09 2000 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  qed_spec_mp "funprod_pos";
     1.5  
     1.6  Goal "(ALL i. k<=i & i<=(k+l) --> zgcd (mf i, mf m) = #1) --> \
     1.7 -\      #0 < mf m --> zgcd (funprod mf k l, mf m) = #1";
     1.8 +\     zgcd (funprod mf k l, mf m) = #1";
     1.9  by (induct_tac "l" 1);
    1.10  by (ALLGOALS Simp_tac);
    1.11  by (REPEAT (rtac impI 1));
    1.12 @@ -111,13 +111,11 @@
    1.13  by (blast_tac (claset() addIs [lemma]) 1);
    1.14  by (REPEAT (rtac impI 1));
    1.15  by (rtac zcong_zgcd_zmult_zmod 1);
    1.16 -by (blast_tac (claset() addIs [lemma]) 3);
    1.17 -by (stac zgcd_commute 4);
    1.18 -by (rtac funprod_zgcd 6);
    1.19 -by (rtac funprod_pos 5);
    1.20 -by (rtac funprod_pos 2);
    1.21 -by (rewrite_goals_tac [m_cond_def,km_cond_def,lincong_sol_def]);
    1.22 -by Auto_tac;
    1.23 +by (blast_tac (claset() addIs [lemma]) 1);
    1.24 +by (stac zgcd_commute 2);
    1.25 +by (rtac funprod_zgcd 2);
    1.26 +by (auto_tac (claset(), 
    1.27 +              simpset() addsimps [m_cond_def,km_cond_def,lincong_sol_def]));  
    1.28  qed_spec_mp "zcong_funprod";
    1.29  
    1.30  
    1.31 @@ -133,9 +131,8 @@
    1.32  by (rtac zcong_lineq_unique 1);
    1.33  by (stac zgcd_zmult_cancel 2);
    1.34  by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]);
    1.35 -by (case_tac "i=0" 4);
    1.36 -by (case_tac "i=n" 5);
    1.37  by (ALLGOALS Asm_simp_tac);
    1.38 +by Auto_tac;  
    1.39  by (stac zgcd_zmult_cancel 3);
    1.40  by (Asm_simp_tac 3);
    1.41  by (ALLGOALS (rtac funprod_zgcd));
     2.1 --- a/src/HOL/NumberTheory/EulerFermat.ML	Wed Sep 13 18:45:10 2000 +0200
     2.2 +++ b/src/HOL/NumberTheory/EulerFermat.ML	Wed Sep 13 18:46:09 2000 +0200
     2.3 @@ -8,6 +8,12 @@
     2.4  to achieve the extended version)
     2.5  *)
     2.6  
     2.7 +(*LCP: not sure why this lemma is needed now*)
     2.8 +Goal "(abs z = (#1::int)) = (z = #1 | z = #-1)";
     2.9 +by (auto_tac (claset(), simpset() addsimps [zabs_def]));  
    2.10 +qed "abs_eq_1_iff";
    2.11 +AddIffs [abs_eq_1_iff];
    2.12 +
    2.13  
    2.14  (***  norRRset  ***)
    2.15  
    2.16 @@ -112,12 +118,12 @@
    2.17  (***  noXRRset  ***)
    2.18  
    2.19  Goalw [is_RRset_def] 
    2.20 -      "[| #0<m; is_RRset A m; #0<m |] ==> a:A --> zgcd (a,m) = #1";
    2.21 +      "is_RRset A m ==> a:A --> zgcd (a,m) = #1";
    2.22  by (rtac RsetR.induct 1);
    2.23  by Auto_tac;
    2.24  qed_spec_mp "RRset_gcd";
    2.25  
    2.26 -Goal "[|  A : RsetR m; #0<m; zgcd (x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
    2.27 +Goal "[| A : RsetR m;  #0<m; zgcd(x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
    2.28  by (etac RsetR.induct 1);
    2.29  by (ALLGOALS Simp_tac);
    2.30  by (rtac RsetR.insert 1);
    2.31 @@ -144,17 +150,16 @@
    2.32  qed "noX_is_RRset";
    2.33  
    2.34  Goal "[| #1<m; is_RRset A m; a:A |] \
    2.35 -\    ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
    2.36 -\        (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
    2.37 +\     ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
    2.38 +\         (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
    2.39  by (rtac (norR_mem_unique RS ex1_implies_ex RS ex_someI) 1);
    2.40  by (rtac RRset_gcd 2);
    2.41  by (ALLGOALS Asm_simp_tac);
    2.42  val lemma_some = result();
    2.43  
    2.44  Goalw [RRset2norRR_def]
    2.45 -      "[| #1<m; is_RRset A m; a:A |] \
    2.46 -\     ==> zcong a (RRset2norRR A m a) m & \
    2.47 -\         (RRset2norRR A m a):(norRRset m)";
    2.48 +     "[| #1<m; is_RRset A m; a:A |] \
    2.49 +\     ==> [a = RRset2norRR A m a] (mod m) & (RRset2norRR A m a):(norRRset m)";
    2.50  by (Asm_simp_tac 1);
    2.51  by (rtac lemma_some 1);
    2.52  by (ALLGOALS Asm_simp_tac);
    2.53 @@ -234,7 +239,7 @@
    2.54  qed "bijzcong_zcong_prod";
    2.55  
    2.56  Goalw [norRRset_def,phi_def]
    2.57 -      "#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
    2.58 +      "a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
    2.59  by (induct_thm_tac BnorRset_induct "a m" 1);
    2.60  by (stac BnorRset_eq 2);
    2.61  by (rewtac Let_def);
    2.62 @@ -244,7 +249,7 @@
    2.63  qed_spec_mp "Bnor_prod_zgcd";
    2.64  
    2.65  Goalw [norRRset_def,phi_def]
    2.66 -      "[| #0<m; zgcd(x,m) = #1 |] ==> zcong (x^phi(m)) #1 m";
    2.67 +      "[| #0<m; zgcd(x,m) = #1 |] ==> [x^phi(m) = #1] (mod m)";
    2.68  by (case_tac "x=#0" 1);
    2.69  by (case_tac "m=#1" 2);
    2.70  by (rtac iffD1 3);
    2.71 @@ -274,9 +279,6 @@
    2.72  by (stac BnorRset_eq 1);
    2.73  by (rewtac Let_def);
    2.74  by Auto_tac;
    2.75 -by (asm_simp_tac (simpset() addsimps [Bnor_mem_zle_swap,Bnor_fin]) 1);
    2.76 -by (stac (int_int_eq RS sym) 1);
    2.77 -by Auto_tac;
    2.78  qed_spec_mp "Bnor_prime";
    2.79  
    2.80  Goalw [phi_def,norRRset_def]
    2.81 @@ -287,7 +289,7 @@
    2.82  by (ALLGOALS Asm_simp_tac);
    2.83  qed "phi_prime";
    2.84  
    2.85 -Goal "[| p:zprime; ~p dvd x |] ==> zcong (x^(nat (p-#1))) #1 p";
    2.86 +Goal "[| p:zprime; ~p dvd x |] ==> [x^(nat (p-#1)) = #1] (mod p)";
    2.87  by (stac (phi_prime RS sym) 1);
    2.88  by (rtac EulerFermatTheorem 2);
    2.89  by (etac zprime_imp_zrelprime 3);
     3.1 --- a/src/HOL/NumberTheory/IntPrimes.ML	Wed Sep 13 18:45:10 2000 +0200
     3.2 +++ b/src/HOL/NumberTheory/IntPrimes.ML	Wed Sep 13 18:46:09 2000 +0200
     3.3 @@ -1,19 +1,40 @@
     3.4  (*  Title:	IntPrimes.ML
     3.5      ID:         $Id$
     3.6 -    Author:	Thomas M. Rasmussen
     3.7 +    Author:	Thomas M. Rasmussen & L C Paulson
     3.8      Copyright	2000  University of Cambridge
     3.9  
    3.10  dvd relation, GCD, Euclid's extended algorithm, primes, congruences
    3.11  (all on the Integers)
    3.12  
    3.13 -Comparable to 'Primes' theory but dvd is included here as it is not present in
    3.14 -'IntDiv'. Also includes extended GCD and congruences not
    3.15 -present in 'Primes'.  Also a few extra theorems concerning 'mod'
    3.16 +Comparable to Primes theory, but dvd is included here as it is not present in
    3.17 +IntDiv.  Also includes extended GCD and congruences -- not present in Primes. 
    3.18  *)
    3.19  
    3.20  eta_contract:=false;
    3.21  
    3.22  
    3.23 +Goal "(abs (z::int) = w) = (z=w & #0 <= z | z=-w & z < #0)";
    3.24 +by (auto_tac (claset(), simpset() addsimps [zabs_def]));  
    3.25 +qed "zabs_eq_iff";
    3.26 +
    3.27 +
    3.28 +(** gcd lemmas **)
    3.29 +
    3.30 +val gcd_non_0 = thm "gcd_non_0";
    3.31 +val gcd_add1 = thm "gcd_add1";
    3.32 +val gcd_commute = thm "gcd_commute";
    3.33 +
    3.34 +Goal "gcd (m+k, k) = gcd (m+k, m)";
    3.35 +by (simp_tac (simpset() addsimps [gcd_commute]) 1); 
    3.36 +qed "gcd_add1_eq";
    3.37 +
    3.38 +Goal "m <= n \\<Longrightarrow> gcd (n, n - m) = gcd (n, m)";
    3.39 +by (subgoal_tac "n = m + (n-m)" 1);
    3.40 +by (etac ssubst 1 THEN rtac gcd_add1_eq 1);
    3.41 +by (Asm_simp_tac 1);
    3.42 +qed "gcd_diff2";
    3.43 +
    3.44 +
    3.45  (************************************************)
    3.46  (** Divides relation 'dvd'                     **)
    3.47  (************************************************)
    3.48 @@ -23,9 +44,10 @@
    3.49  qed "zdvd_0_right";
    3.50  AddIffs [zdvd_0_right];
    3.51  
    3.52 -Goalw [dvd_def] "#0 dvd (m::int) ==> m = #0";
    3.53 +Goalw [dvd_def] "(#0 dvd (m::int)) = (m = #0)";
    3.54  by Auto_tac;
    3.55  qed "zdvd_0_left";
    3.56 +AddIffs [zdvd_0_left];
    3.57  
    3.58  Goalw [dvd_def] "#1 dvd (m::int)";
    3.59  by (Simp_tac 1);
    3.60 @@ -146,139 +168,158 @@
    3.61  by Auto_tac;  
    3.62  qed "zdvd_not_zless";
    3.63  
    3.64 +Goal "(int m dvd z) = (m dvd nat(abs z))";
    3.65 +by (auto_tac (claset(), 
    3.66 +       simpset() addsimps [dvd_def, nat_abs_mult_distrib]));  
    3.67 +by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, zabs_eq_iff]));  
    3.68 +by (res_inst_tac [("x","-(int k)")] exI 2);
    3.69 +by (auto_tac (claset(), simpset() addsimps [zmult_int RS sym]));  
    3.70 +qed "int_dvd_iff";
    3.71 +
    3.72 +Goal "(z dvd int m) = (nat(abs z) dvd m)";
    3.73 +by (auto_tac (claset(), 
    3.74 +       simpset() addsimps [dvd_def, zabs_def, zmult_int RS sym]));  
    3.75 +by (res_inst_tac [("x","nat k")] exI 3); 
    3.76 +by (res_inst_tac [("x","-(int k)")] exI 2);
    3.77 +by (res_inst_tac [("x","nat (-k)")] exI 1);
    3.78 +by (cut_inst_tac [("k","m")] int_less_0_conv 3);
    3.79 +by (cut_inst_tac [("k","m")] int_less_0_conv 1);
    3.80 +by (auto_tac (claset(), 
    3.81 +         simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
    3.82 +                             nat_mult_distrib RS sym, nat_eq_iff2]));  
    3.83 +qed "dvd_int_iff";
    3.84 +
    3.85 +Goal "(nat z dvd m) = (if #0 <= z then (z dvd int m) else m=0)";
    3.86 +by (auto_tac (claset(), simpset() addsimps [dvd_def, zmult_int RS sym]));  
    3.87 +by (res_inst_tac [("x","nat k")] exI 1);
    3.88 +by (cut_inst_tac [("k","m")] int_less_0_conv 1);
    3.89 +by (auto_tac (claset(), 
    3.90 +         simpset() addsimps [int_0_le_mult_iff, zmult_less_0_iff,
    3.91 +                             nat_mult_distrib RS sym, nat_eq_iff2]));  
    3.92 +qed "nat_dvd_iff";
    3.93 +
    3.94 +Goal "(-z dvd w) = (z dvd (w::int))";
    3.95 +by (auto_tac (claset(), simpset() addsimps [dvd_def]));  
    3.96 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
    3.97 +by Auto_tac;  
    3.98 +qed "zminus_dvd_iff";
    3.99 +
   3.100 +Goal "(z dvd -w) = (z dvd (w::int))";
   3.101 +by (auto_tac (claset(), simpset() addsimps [dvd_def]));  
   3.102 +by (dtac (zminus_equation RS iffD1) 1);
   3.103 +by (ALLGOALS (res_inst_tac [("x","-k")] exI));
   3.104 +by Auto_tac;  
   3.105 +qed "dvd_zminus_iff";
   3.106 +AddIffs [zminus_dvd_iff, dvd_zminus_iff];
   3.107 +
   3.108  
   3.109  (************************************************)
   3.110  (** Euclid's Algorithm and GCD                 **)
   3.111  (************************************************)
   3.112  
   3.113 -val [zgcd_eq] = zgcd.simps;
   3.114 -Delsimps zgcd.simps;
   3.115 -
   3.116 -Goal "zgcd(m,#0) = m";
   3.117 -by (rtac (zgcd_eq RS trans) 1);
   3.118 -by (Simp_tac 1);
   3.119 +Goal "zgcd(m,#0) = abs m";
   3.120 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 
   3.121  qed "zgcd_0";
   3.122  Addsimps [zgcd_0];
   3.123  
   3.124 -Goal"#0<(m::int) ==> zgcd(#0,m) = m";
   3.125 -by (auto_tac (claset(), simpset() addsimps zgcd.simps));
   3.126 +Goal"zgcd(#0,m) = abs m";
   3.127 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 
   3.128  qed "zgcd_0_left";
   3.129  Addsimps [zgcd_0_left];
   3.130  
   3.131 +Goal "zgcd(-m,n) = zgcd(m,n)";
   3.132 +by (simp_tac (simpset() addsimps [zgcd_def]) 1); 
   3.133 +qed "zgcd_zminus";
   3.134 +Addsimps [zgcd_zminus];
   3.135 +
   3.136 +Goal "zgcd(m,-n) = zgcd(m,n)";
   3.137 +by (simp_tac (simpset() addsimps [zgcd_def]) 1); 
   3.138 +qed "zgcd_zminus2";
   3.139 +Addsimps [zgcd_zminus2];
   3.140 +
   3.141  Goal "#0<n ==> zgcd(m,n) = zgcd (n, m mod n)";
   3.142 -by (rtac (zgcd_eq RS trans) 1);
   3.143 -by (Asm_simp_tac 1);
   3.144 +by (forw_inst_tac [("b","n"), ("a","m")] pos_mod_sign 1);
   3.145 +by (asm_simp_tac (simpset() addsimps [zgcd_def, zabs_def, nat_mod_distrib]) 1);
   3.146 +by (cut_inst_tac [("a","-m"),("b","n")] zmod_zminus1_eq_if 1);
   3.147 +by (auto_tac (claset(), 
   3.148 +              simpset() addsimps [gcd_non_0, nat_mod_distrib RS sym,
   3.149 +                                  zmod_zminus1_eq_if]));
   3.150 +by (forw_inst_tac [("a","m")] pos_mod_bound 1);
   3.151 +by (asm_simp_tac (simpset() addsimps [nat_diff_distrib]) 1);  
   3.152 +by (rtac gcd_diff2 1);
   3.153 +by (asm_full_simp_tac (simpset() addsimps [nat_le_eq_zle]) 1); 
   3.154  qed "zgcd_non_0";
   3.155  
   3.156 +Goal "zgcd(m,n) = zgcd (n, m mod n)";
   3.157 +by (zdiv_undefined_case_tac "n = #0" 1);
   3.158 +by (auto_tac
   3.159 +    (claset(),
   3.160 +     simpset() addsimps [linorder_neq_iff, zgcd_non_0]));
   3.161 +by (cut_inst_tac [("m","-m"),("n","-n")] zgcd_non_0 1);
   3.162 +by Auto_tac;  
   3.163 +qed "zgcd_eq";
   3.164 +
   3.165  Goal "zgcd(m,#1) = #1";
   3.166 -by (simp_tac (simpset() addsimps [zgcd_non_0]) 1);
   3.167 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 
   3.168  qed "zgcd_1";
   3.169  Addsimps [zgcd_1];
   3.170  
   3.171 -Goal "(zgcd(#0,m) = #1) = (m = #1)";
   3.172 -by (auto_tac (claset(),simpset() addsimps zgcd.simps));
   3.173 +Goal "(zgcd(#0,m) = #1) = (abs m = #1)";
   3.174 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def]) 1); 
   3.175  qed "zgcd_0_1_iff";
   3.176  Addsimps [zgcd_0_1_iff];
   3.177  
   3.178 -Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
   3.179 -by (induct_thm_tac zgcd.induct "m n" 1);
   3.180 -by (case_tac "n=#0" 1);
   3.181 -by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
   3.182 -              simpset() addsimps [zle_neq_implies_zless,neq_commute,
   3.183 -                                  pos_mod_sign,zgcd_non_0]));
   3.184 -by (ALLGOALS (rotate_tac 1));
   3.185 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zle_anti_sym])));
   3.186 -qed_spec_mp "zgcd_zdvd_both";
   3.187 -
   3.188 -bind_thm ("zgcd_zdvd1", zgcd_zdvd_both RS conjunct1);
   3.189 -bind_thm ("zgcd_zdvd2", zgcd_zdvd_both RS conjunct2);
   3.190 -
   3.191 -Goal "[| (n::int) <= #0;  #0 <= n; #0 ~= n |] ==> False";
   3.192 -by (asm_full_simp_tac (simpset() addsimps [zle_anti_sym]) 1);
   3.193 -val lemma_false = result();
   3.194 -
   3.195 -Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
   3.196 -by (induct_thm_tac zgcd.induct "m n" 1);
   3.197 -by (case_tac "n=#0" 1);
   3.198 -by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
   3.199 -        simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
   3.200 -qed_spec_mp "zgcd_greatest";
   3.201 -
   3.202 -Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
   3.203 -by (induct_thm_tac zgcd.induct "m n" 1);
   3.204 -by (auto_tac (claset(), simpset() addsimps zgcd.simps));
   3.205 -qed_spec_mp "zgcd_zless";
   3.206 +Goal "zgcd(m,n) dvd m";
   3.207 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 
   3.208 +qed "zgcd_zdvd1";
   3.209  
   3.210 -Goalw [is_zgcd_def] "#0<(n::int) ==> is_zgcd (zgcd(m,n)) m n";
   3.211 -by (asm_simp_tac (simpset() addsimps 
   3.212 -      [zgcd_greatest,zgcd_zdvd_both,zgcd_zless]) 1);
   3.213 -qed "is_zgcd";
   3.214 -
   3.215 -Goalw [is_zgcd_def] "[| is_zgcd m a b; is_zgcd n a b |] ==> m=n";
   3.216 -by (blast_tac (claset() addIs [zdvd_anti_sym]) 1);
   3.217 -qed "is_zgcd_unique";
   3.218 -
   3.219 -Goalw [is_zgcd_def] "[| is_zgcd m a b; k dvd a; k dvd b |] ==> k dvd m";
   3.220 -by (Blast_tac 1);
   3.221 -qed "is_zgcd_zdvd";
   3.222 -
   3.223 -Goalw [is_zgcd_def] "is_zgcd k m n = is_zgcd k n m";
   3.224 -by (Blast_tac 1);
   3.225 -qed "is_zgcd_commute";
   3.226 +Goal "zgcd(m,n) dvd n";
   3.227 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff]) 1); 
   3.228 +qed "zgcd_zdvd2";
   3.229 +AddIffs [zgcd_zdvd1, zgcd_zdvd2];
   3.230  
   3.231 -Goalw [is_zgcd_def] "is_zgcd k (-m) n = is_zgcd k m n";
   3.232 -by (asm_full_simp_tac (simpset() addsimps [zdvd_zminus_iff]) 1);
   3.233 -qed "is_zgcd_zminus";
   3.234 +Goal "k dvd zgcd(m,n) = (k dvd m & k dvd n)";
   3.235 +by (simp_tac (simpset() addsimps [zgcd_def, zabs_def, int_dvd_iff, 
   3.236 +                                  dvd_int_iff, nat_dvd_iff]) 1); 
   3.237 +qed "zgcd_greatest_iff";
   3.238  
   3.239 -Goal "#0<(n::int) ==> zgcd(-m,n) = zgcd(m,n)";
   3.240 -by (rtac is_zgcd_unique 1);
   3.241 -by (rtac is_zgcd 1);
   3.242 -by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_zminus]) 2);
   3.243 -by (assume_tac 1);
   3.244 -qed "zgcd_zminus";
   3.245 -
   3.246 -Goal "[| #0<(m::int); #0<n |] ==> zgcd(m,n) = zgcd(n,m)";
   3.247 -by (rtac is_zgcd_unique 1);
   3.248 -by (rtac is_zgcd 2);
   3.249 -by (asm_simp_tac (simpset() addsimps [is_zgcd,is_zgcd_commute]) 1);
   3.250 -by (assume_tac 1);
   3.251 +Goal "zgcd(m,n) = zgcd(n,m)";
   3.252 +by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_commute"]) 1); 
   3.253  qed "zgcd_commute";
   3.254  
   3.255 -Goal "#0<=(m::int) ==> zgcd(#1,m) = #1";
   3.256 -by (case_tac "m=#0" 1);
   3.257 -by (stac zgcd_commute 2);
   3.258 -by (ALLGOALS (asm_full_simp_tac (simpset() 
   3.259 -      addsimps [zle_neq_implies_zless,neq_commute])));
   3.260 +Goal "zgcd(#1,m) = #1";
   3.261 +by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_1_left"]) 1); 
   3.262  qed "zgcd_1_left";
   3.263  Addsimps [zgcd_1_left];
   3.264  
   3.265 -Goal "[| #0<(m::int); #0<n |] ==> zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))";
   3.266 -by (rtac is_zgcd_unique 1);
   3.267 -by (rtac is_zgcd 2);
   3.268 -by (rewrite_goals_tac [is_zgcd_def]);
   3.269 -by Auto_tac;
   3.270 -by (rtac zgcd_greatest 3);
   3.271 -by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 2);
   3.272 -by (res_inst_tac [("n","zgcd (k,m)")] zdvd_trans 5);
   3.273 -by (rtac zgcd_greatest 8);
   3.274 -by (rtac zgcd_greatest 9);
   3.275 -by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 12);
   3.276 -by (res_inst_tac [("n","zgcd (m,n)")] zdvd_trans 11);
   3.277 -by (ALLGOALS (asm_simp_tac (simpset() 
   3.278 -      addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless])));
   3.279 +Goal "zgcd(zgcd(k,m),n) = zgcd(k,zgcd(m,n))";
   3.280 +by (simp_tac (simpset() addsimps [zgcd_def, thm"gcd_assoc"]) 1); 
   3.281  qed "zgcd_assoc";
   3.282  
   3.283 -Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
   3.284 -by (induct_thm_tac zgcd.induct "m n" 1);
   3.285 -by (case_tac "n=#0" 1);
   3.286 -by (auto_tac (claset() addDs [lemma_false],
   3.287 -              simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
   3.288 -                                  zgcd_non_0,neq_commute]));
   3.289 -by (case_tac "k=#0" 1);
   3.290 -by (ALLGOALS (asm_full_simp_tac (simpset() 
   3.291 -      addsimps [zle_neq_implies_zless,zgcd_non_0,zmod_zmult_zmult1,
   3.292 -                int_0_less_mult_iff,neq_commute])));
   3.293 -qed_spec_mp "zgcd_zmult_distrib2";
   3.294 +Goal "zgcd(k,zgcd(m,n)) = zgcd(m,zgcd(k,n))";
   3.295 +by (rtac (zgcd_commute RS trans) 1);
   3.296 +by (rtac (zgcd_assoc RS trans) 1);
   3.297 +by (rtac (zgcd_commute RS arg_cong) 1);
   3.298 +qed "zgcd_left_commute";
   3.299 +
   3.300 +(*Addition is an AC-operator*)
   3.301 +bind_thms ("zgcd_ac", [zgcd_assoc, zgcd_commute, zgcd_left_commute]);
   3.302 +
   3.303 +val gcd_mult_distrib2 = thm"gcd_mult_distrib2";
   3.304 +
   3.305 +Goal "#0<=k ==> k * zgcd(m,n) = zgcd(k*m, k*n)";
   3.306 +by (asm_simp_tac 
   3.307 +    (simpset() delsimps [zmult_zminus_right] 
   3.308 +	       addsimps [zmult_zminus_right RS sym, 
   3.309 +                         nat_mult_distrib, zgcd_def, zabs_def, 
   3.310 +                         zmult_less_0_iff, gcd_mult_distrib2 RS sym, 
   3.311 +                         zmult_int RS sym]) 1); 
   3.312 +qed "zgcd_zmult_distrib2";
   3.313 +
   3.314 +Goal "zgcd(k*m, k*n) = abs k * zgcd(m,n)";
   3.315 +by (simp_tac (simpset() addsimps [zabs_def, zgcd_zmult_distrib2]) 1);
   3.316 +qed "zgcd_zmult_distrib2_abs";
   3.317 +
   3.318  
   3.319  Goal "#0<=m ==> zgcd(m,m) = m";
   3.320  by (cut_inst_tac [("k","m"),("m","#1"),("n","#1")] zgcd_zmult_distrib2 1);
   3.321 @@ -286,7 +327,7 @@
   3.322  qed "zgcd_self";
   3.323  Addsimps [zgcd_self];
   3.324  
   3.325 -Goal "[| #0<=k; #0<=n |] ==> zgcd(k, k*n) = k";
   3.326 +Goal "#0<=k ==> zgcd(k, k*n) = k";
   3.327  by (cut_inst_tac [("k","k"),("m","#1"),("n","n")] zgcd_zmult_distrib2 1);
   3.328  by (ALLGOALS Asm_full_simp_tac);
   3.329  qed "zgcd_zmult_eq_self";
   3.330 @@ -298,16 +339,23 @@
   3.331  qed "zgcd_zmult_eq_self2";
   3.332  Addsimps [zgcd_zmult_eq_self2];
   3.333  
   3.334 -Goal "[| #0<=(m::int); #0<=k; zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
   3.335 +Goal "[| zgcd(n,k)=#1; k dvd (m*n); #0 <= m |] ==> k dvd m";
   3.336  by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
   3.337 -by (etac ssubst 1 THEN rtac zgcd_greatest 1);
   3.338 +by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1);
   3.339  by (ALLGOALS (asm_simp_tac (simpset() 
   3.340        addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
   3.341 +val lemma = result();
   3.342 +
   3.343 +Goal "[| zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
   3.344 +by (case_tac "#0 <= m" 1);
   3.345 +by (blast_tac (claset() addIs [lemma]) 1); 
   3.346 +by (subgoal_tac "k dvd -m" 1);
   3.347 +by (rtac lemma 2);
   3.348 +by Auto_tac;  
   3.349  qed "zrelprime_zdvd_zmult";
   3.350  
   3.351  Goalw [zprime_def] "[| p:zprime; ~p dvd n |] ==> zgcd(n,p) = #1";
   3.352 -by (cut_inst_tac [("m","n"),("n","p")] zgcd_zdvd_both 1);
   3.353 -by Auto_tac;
   3.354 +by Auto_tac;  
   3.355  qed "zprime_imp_zrelprime";
   3.356  
   3.357  Goal "[| p:zprime; #0<n; n<p |] ==> zgcd(n,p) = #1";
   3.358 @@ -319,61 +367,42 @@
   3.359  Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n";
   3.360  by Safe_tac;
   3.361  by (rtac zrelprime_zdvd_zmult 1);
   3.362 -by (rtac zprime_imp_zrelprime 3);
   3.363 -by (SELECT_GOAL (rewrite_goals_tac [zprime_def]) 2);
   3.364 +by (rtac zprime_imp_zrelprime 1);
   3.365  by Auto_tac;
   3.366  qed "zprime_zdvd_zmult";
   3.367  
   3.368 -Goal "#0<n ==> zgcd(m+n*k,n) = zgcd(m,n)";
   3.369 +val gcd_add_mult = thm "gcd_add_mult";
   3.370 +
   3.371 +Goal "zgcd(m + n*k, n) = zgcd(m,n)";
   3.372  by (rtac (zgcd_eq RS trans) 1);
   3.373 -by Auto_tac;
   3.374  by (simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
   3.375 -by (rtac trans 1);
   3.376 -by (rtac (zgcd_eq RS sym) 2);
   3.377 -by Auto_tac;
   3.378 +by (rtac (zgcd_eq RS sym) 1);
   3.379  qed "zgcd_zadd_zmult";
   3.380  Addsimps [zgcd_zadd_zmult];
   3.381  
   3.382 -Goal "#0<=n ==> zgcd(m,n) dvd zgcd(k*m,n)";
   3.383 -by (rtac zgcd_greatest 1);
   3.384 -by (rtac zdvd_trans 2);
   3.385 -by (rtac zgcd_zdvd1 2);
   3.386 -by (rtac zgcd_zdvd2 4);
   3.387 -by (ALLGOALS Asm_simp_tac);
   3.388 +
   3.389 +Goal "zgcd(m,n) dvd zgcd(k*m,n)";
   3.390 +by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 
   3.391 +by (blast_tac (claset() addIs [zdvd_trans]) 1); 
   3.392  qed "zgcd_zdvd_zgcd_zmult";
   3.393  
   3.394 -Goal "[| #0<k; #0<m; #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m,n) dvd zgcd(m,n)";
   3.395 -by (rtac zgcd_greatest 1);
   3.396 -by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 2);
   3.397 -by (stac zmult_commute 5);
   3.398 -by (stac (zgcd_assoc RS sym) 4);
   3.399 -by (rtac zless_imp_zle 3);
   3.400 -by (ALLGOALS (asm_simp_tac (simpset() 
   3.401 -      addsimps [zgcd_zdvd1,zgcd_zdvd2,zgcd_zless,int_0_less_mult_iff])));
   3.402 +Goal "zgcd(k,n) = #1 ==> zgcd(k*m,n) dvd zgcd(m,n)";
   3.403 +by (simp_tac (simpset() addsimps [zgcd_greatest_iff]) 1); 
   3.404 +by (res_inst_tac [("n","k")] zrelprime_zdvd_zmult 1);
   3.405 +by (simp_tac (simpset() addsimps [zmult_commute]) 2); 
   3.406 +by (subgoal_tac "zgcd (k, zgcd (k * m, n)) =  zgcd (k * m, zgcd (k, n))" 1);
   3.407 +by (Asm_full_simp_tac 1); 
   3.408 +by (simp_tac (simpset() addsimps zgcd_ac) 1); 
   3.409  qed "zgcd_zmult_zdvd_zgcd";
   3.410  
   3.411 -Goal "[| #0<n; zgcd(k,n) = #1 |] ==> zgcd(k*m, n) = zgcd(m,n)";
   3.412 -by (rtac zdvd_anti_sym 1);
   3.413 -by (rtac zgcd_zdvd_zgcd_zmult 4);
   3.414 -by (case_tac "m=#0" 3);
   3.415 -by (case_tac "k=#0" 4);
   3.416 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zless])));
   3.417 -by (case_tac "#0<k" 1);
   3.418 -by (ALLGOALS (case_tac "#0<m"));
   3.419 -by (rtac zgcd_zmult_zdvd_zgcd 1);
   3.420 -by (subgoal_tac "zgcd (k*(-m),n) dvd zgcd (-m,n)" 5);
   3.421 -by (rtac zgcd_zmult_zdvd_zgcd 6);
   3.422 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   3.423 -by (subgoal_tac "zgcd ((-k)*m,n) dvd zgcd (m,n)" 2);
   3.424 -by (rtac zgcd_zmult_zdvd_zgcd 3);
   3.425 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   3.426 -by (subgoal_tac "zgcd ((-k)*(-m),n) dvd zgcd (-m,n)" 3);
   3.427 -by (rtac zgcd_zmult_zdvd_zgcd 4);
   3.428 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zgcd_zminus])));
   3.429 -by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
   3.430 +val gcd_mult_cancel = thm "gcd_mult_cancel";
   3.431 +
   3.432 +Goal "zgcd(k,n) = #1 ==> zgcd(k*m, n) = zgcd(m,n)";
   3.433 +by (asm_full_simp_tac (simpset() addsimps [zgcd_def, 
   3.434 +                           nat_abs_mult_distrib, gcd_mult_cancel]) 1); 
   3.435  qed "zgcd_zmult_cancel";
   3.436  
   3.437 -Goal "[| #0<m; zgcd(k,m) = #1; zgcd(n,m) = #1 |] ==> zgcd(k*n,m) = #1";
   3.438 +Goal "[| zgcd(k,m) = #1; zgcd(n,m) = #1 |] ==> zgcd(k*n,m) = #1";
   3.439  by (asm_simp_tac (simpset() addsimps [zgcd_zmult_cancel]) 1);
   3.440  qed "zgcd_zgcd_zmult";
   3.441  
   3.442 @@ -483,7 +512,7 @@
   3.443  qed "zcong_cancel2";
   3.444  
   3.445  Goalw [zcong_def,dvd_def]
   3.446 -      "[| #0<m; #0<n; [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \
   3.447 +      "[| [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \
   3.448  \     ==> [a=b](mod m*n)";
   3.449  by Auto_tac;
   3.450  by (subgoal_tac "m dvd (n*ka)" 1);
   3.451 @@ -491,12 +520,11 @@
   3.452  by (case_tac "#0<=ka" 2);
   3.453  by (stac (zdvd_zminus_iff RS sym) 3);
   3.454  by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
   3.455 -by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 4);
   3.456 -by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 4);
   3.457 -by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 4);
   3.458 -by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 6);
   3.459 -by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 6);
   3.460 -by (ALLGOALS Asm_simp_tac);
   3.461 +by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
   3.462 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2);
   3.463 +by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
   3.464 +by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
   3.465 +by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 2);
   3.466  by (rewtac dvd_def);
   3.467  by Safe_tac;
   3.468  by (res_inst_tac [("x","kc")] exI 1);
   3.469 @@ -601,6 +629,25 @@
   3.470  by Auto_tac;
   3.471  qed "zcong_zmod_eq";
   3.472  
   3.473 +Goal "[a = b] (mod -m) = [a = b] (mod m)";
   3.474 +by (auto_tac (claset(), simpset() addsimps [zcong_def]));  
   3.475 +qed "zcong_zminus";
   3.476 +AddIffs [zcong_zminus];
   3.477 +
   3.478 +Goal "[a = b] (mod #0) = (a = b)";
   3.479 +by (auto_tac (claset(), simpset() addsimps [zcong_def]));  
   3.480 +qed "zcong_zero";
   3.481 +AddIffs [zcong_zero];
   3.482 +
   3.483 +Goal "[a = b] (mod m) = (a mod m = b mod m)";
   3.484 +by (zdiv_undefined_case_tac "m = #0" 1);
   3.485 +by (case_tac "#0<m" 1);
   3.486 +by (asm_simp_tac (simpset() addsimps [zcong_zmod_eq]) 1); 
   3.487 +by (res_inst_tac [("t","m")] (zminus_zminus RS subst) 1); 
   3.488 +by (stac zcong_zminus 1);
   3.489 +by (stac zcong_zmod_eq 1);
   3.490 +by (arith_tac 1); 
   3.491 +(*FIXME: finish this proof?*)
   3.492  
   3.493  (************************************************)
   3.494  (** Modulo                                     **)
   3.495 @@ -617,6 +664,7 @@
   3.496  by (assume_tac 1);
   3.497  qed "zmod_zdvd_zmod";
   3.498  
   3.499 +
   3.500  (************************************************)
   3.501  (** Extended GCD                               **)
   3.502  (************************************************)
   3.503 @@ -624,7 +672,7 @@
   3.504  val [xzgcda_eq] = xzgcda.simps;
   3.505  Delsimps xzgcda.simps;
   3.506  
   3.507 -Goal "zgcd(r',r) = k --> \
   3.508 +Goal "zgcd(r',r) = k --> #0 < r \\<longrightarrow> \
   3.509  \     (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))";
   3.510  by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
   3.511                    ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
   3.512 @@ -632,23 +680,39 @@
   3.513  by (stac zgcd_eq 1);
   3.514  by (stac xzgcda_eq 1);
   3.515  by Auto_tac;
   3.516 +by (case_tac "r' mod r = #0" 1);
   3.517 +by (forw_inst_tac [("a","r'")] pos_mod_sign 2);
   3.518 +by Auto_tac;  
   3.519 +by (arith_tac 2);
   3.520 +by (rtac exI 1);
   3.521 +by (rtac exI 1);
   3.522 +by (stac xzgcda_eq 1);
   3.523 +by Auto_tac;  
   3.524 +by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 
   3.525  val lemma1 = result();
   3.526  
   3.527 -Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> \
   3.528 +Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r \\<longrightarrow>  \
   3.529  \     zgcd(r',r) = k";
   3.530  by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
   3.531                    ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
   3.532                    xzgcda.induct 1);
   3.533  by (stac zgcd_eq 1);
   3.534  by (stac xzgcda_eq 1);
   3.535 -by Auto_tac;
   3.536 +by (auto_tac (claset(), simpset() addsimps [linorder_not_le]));  
   3.537 +by (case_tac "r' mod r = #0" 1);
   3.538 +by (forw_inst_tac [("a","r'")] pos_mod_sign 2);
   3.539 +by Auto_tac;  
   3.540 +by (arith_tac 2);
   3.541 +by (eres_inst_tac [("P","xzgcda ?u = ?v")] rev_mp 1); 
   3.542 +by (stac xzgcda_eq 1);
   3.543 +by Auto_tac;  
   3.544 +by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 
   3.545  val lemma2 = result();
   3.546  
   3.547 -Goalw [xzgcd_def] "(zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
   3.548 +Goalw [xzgcd_def] "#0 < n \\<Longrightarrow> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
   3.549  by (rtac iffI 1);
   3.550 -by (ALLGOALS (rtac mp));
   3.551 -by (rtac lemma2 3);
   3.552 -by (rtac lemma1 1);
   3.553 +by (rtac (lemma2 RS mp RS mp) 2);
   3.554 +by (rtac (lemma1 RS mp RS mp) 1);
   3.555  by Auto_tac;
   3.556  qed "xzgcd_correct";
   3.557  
   3.558 @@ -697,7 +761,7 @@
   3.559  qed "xzgcd_linear";
   3.560  
   3.561  Goal "[| #0<n; zgcd(m,n) = k |] ==> (EX s t. k = s*m + t*n)";
   3.562 -by (full_simp_tac (simpset() addsimps [xzgcd_correct]) 1);
   3.563 +by (asm_full_simp_tac (simpset() addsimps [xzgcd_correct]) 1);
   3.564  by Safe_tac;
   3.565  by (REPEAT (rtac exI 1));
   3.566  by (etac xzgcd_linear 1);
     4.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Wed Sep 13 18:45:10 2000 +0200
     4.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed Sep 13 18:46:09 2000 +0200
     4.3 @@ -4,20 +4,14 @@
     4.4      Copyright	2000  University of Cambridge
     4.5  *)
     4.6  
     4.7 -IntPrimes = Main + IntDiv +
     4.8 +IntPrimes = Main + IntDiv + Primes +
     4.9  
    4.10  consts
    4.11 -  is_zgcd  :: [int,int,int] => bool         
    4.12 -  zgcd     :: "int*int => int"              
    4.13    xzgcda   :: "int*int*int*int*int*int*int*int => int*int*int"
    4.14    xzgcd    :: "[int,int] => int*int*int" 
    4.15    zprime   :: int set
    4.16    zcong    :: [int,int,int] => bool     ("(1[_ = _] '(mod _'))")
    4.17    
    4.18 -recdef zgcd "measure ((%(m,n).(nat n)) ::int*int=>nat)"
    4.19 -    simpset "simpset() addsimps [pos_mod_bound]"
    4.20 -    "zgcd (m, n) = (if n<=#0 then m else zgcd(n, m mod n))"
    4.21 -
    4.22  recdef xzgcda 
    4.23         "measure ((%(m,n,r',r,s',s,t',t).(nat r))
    4.24                   ::int*int*int*int*int*int*int*int=>nat)"
    4.25 @@ -26,12 +20,13 @@
    4.26            (if r<=#0 then (r',s',t') else  
    4.27             xzgcda(m,n,r,r' mod r,s,s'-(r' div r)*s,t,t'-(r' div r)*t))"
    4.28  
    4.29 +constdefs
    4.30 +  zgcd     :: "int*int => int"              
    4.31 +      "zgcd == %(x,y). int (gcd(nat (abs x), nat (abs y)))"
    4.32 +
    4.33  defs
    4.34    xzgcd_def    "xzgcd m n == xzgcda (m,n,m,n,#1,#0,#0,#1)"
    4.35  
    4.36 -  is_zgcd_def  "is_zgcd p m n == #0 < p  &  p dvd m  &  p dvd n  &
    4.37 -                                 (ALL d. d dvd m & d dvd n --> d dvd p)"
    4.38 -
    4.39    zprime_def   "zprime == {p. #1<p & (ALL m. m dvd p --> m=#1 | m=p)}"
    4.40  
    4.41    zcong_def    "[a=b] (mod m) == m dvd (a-b)"
     5.1 --- a/src/HOL/NumberTheory/WilsonBij.ML	Wed Sep 13 18:45:10 2000 +0200
     5.2 +++ b/src/HOL/NumberTheory/WilsonBij.ML	Wed Sep 13 18:46:09 2000 +0200
     5.3 @@ -214,12 +214,11 @@
     5.4  Goal "p:zprime ==> [zfact(p-#1) = #-1](mod p)";
     5.5  by (subgoal_tac "zcong ((p-#1)*zfact(p-#2)) (#-1*#1) p" 1);
     5.6  by (rtac zcong_zmult 2);
     5.7 -by (SELECT_GOAL (rewtac zprime_def) 1);
     5.8 +by (full_simp_tac (simpset() addsimps [zprime_def]) 1); 
     5.9  by (stac zfact_eq 1);
    5.10  by (res_inst_tac [("t","p-#1-#1"),("s","p-#2")] subst 1);
    5.11  by Auto_tac;
    5.12 -by (SELECT_GOAL (rewtac zcong_def) 1);
    5.13 -by (Asm_simp_tac 1);
    5.14 +by (asm_simp_tac (simpset() addsimps [zcong_def]) 1); 
    5.15  by (stac (d22set_prod_zfact RS sym) 1);
    5.16  by (rtac bijER_zcong_prod_1 1);
    5.17  by (rtac bijER_d22set 2);