modified proofs: better rules for cancellation of common factors across comparisons
--- a/src/HOL/NumberTheory/EulerFermat.ML Thu Aug 17 11:55:47 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML Thu Aug 17 11:56:47 2000 +0200
@@ -130,12 +130,8 @@
"[| #0<m; zgcd(x,m) = #1 |] \
\ ==> card (noXRRset m x) = card (norRRset m)";
by (rtac card_image 1);
-by (rewtac inj_on_def);
-by (auto_tac (claset(),simpset() addsimps [Bnor_fin]));
-by (case_tac "x=#0" 1);
+by (auto_tac (claset(),simpset() addsimps [inj_on_def, Bnor_fin]));
by (asm_full_simp_tac (simpset() addsimps [BnorRset_eq]) 1);
-by (stac (zmult_cancel2 RS sym) 1);
-by (ALLGOALS Asm_simp_tac);
qed "card_nor_eq_noX";
Goalw [is_RRset_def,phi_def]
--- a/src/HOL/NumberTheory/IntPrimes.ML Thu Aug 17 11:55:47 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML Thu Aug 17 11:56:47 2000 +0200
@@ -140,15 +140,10 @@
by Auto_tac;
by (subgoal_tac "#0<n" 1);
by (blast_tac (claset() addIs [zless_trans]) 2);
-by (case_tac "k<#0" 1);
-by (rotate_tac ~2 1);
-by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
-by (case_tac "k=#0" 1);
-by (subgoal_tac "n*k < n*#1" 2);
-by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 2);
-by (subgoal_tac "#0<k" 2);
-by (rtac lemma 3);
-by (ALLGOALS Asm_full_simp_tac);
+by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
+by (subgoal_tac "n*k < n*#1" 1);
+by (dtac (zmult_zless_cancel1 RS iffD1) 1);
+by Auto_tac;
qed "zdvd_not_zless";
@@ -512,15 +507,16 @@
Goalw [zcong_def,dvd_def]
"[| #0<=a; a<m; #0<=b; b<m; [a = b] (mod m) |] ==> a = b";
-by (rtac (eq_iff_zdiff_eq_0 RS iffD2) 1);
-by Auto_tac;
-by (subgoal_tac "k=#0" 1);
-by (subgoal_tac "#-1<k & k<#1" 2);
+by Auto_tac;
+by (dres_inst_tac [("f", "%z. z mod m")] arg_cong 1);
+by (cut_inst_tac [("z","a"),("w","b")] zless_linear 1);
+by Auto_tac;
+by (subgoal_tac "(a - b) mod m = a-b" 2);
+by (rtac mod_pos_pos_trivial 3);
by Auto_tac;
-by (ALLGOALS (rtac iffD1));
-by (res_inst_tac [("k","m")] zmult_zless_cancel1 3);
-by (res_inst_tac [("k","m")] zmult_zless_cancel1 1);
-by Auto_tac;
+by (subgoal_tac "(m + (a - b)) mod m = m + (a - b)" 1);
+by (rtac mod_pos_pos_trivial 2);
+by Auto_tac;
qed "zcong_zless_imp_eq";
Goal "[| p:zprime; #0<a; a<p; [a*a = #1](mod p) |] ==> a = #1 | a = p-#1";
@@ -544,8 +540,8 @@
by (rotate_tac ~1 1);
by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
by (subgoal_tac "m*k<m*#1" 1);
-by (asm_full_simp_tac (simpset() delsimps [zmult_1_right]) 1);
-by (ALLGOALS Asm_full_simp_tac);
+by (dtac (zmult_zless_cancel1 RS iffD1) 1);
+by Auto_tac;
qed "zcong_zless_0";
Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
@@ -680,7 +676,6 @@
("y","s'"),("z","s"),("aa","t'"),("ab","t")]
xzgcda.induct 1);
by (stac xzgcda_eq 1);
-by (rewtac Let_def);
by (Simp_tac 1);
by (REPEAT (rtac impI 1));
by (case_tac "r' mod r = #0" 1);