--- a/src/HOL/NumberTheory/Chinese.ML Wed Dec 13 10:31:08 2000 +0100
+++ b/src/HOL/NumberTheory/Chinese.ML Wed Dec 13 10:31:46 2000 +0100
@@ -99,7 +99,7 @@
by (res_inst_tac [("k","kf n")] zcong_cancel2 1);
by (res_inst_tac [("b","bf n")] zcong_trans 3);
by (stac zcong_sym 4);
-by (rtac zless_imp_zle 1);
+by (rtac order_less_imp_le 1);
by (ALLGOALS Asm_simp_tac);
val lemma = result();
--- a/src/HOL/NumberTheory/EulerFermat.ML Wed Dec 13 10:31:08 2000 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.ML Wed Dec 13 10:31:46 2000 +0100
@@ -57,7 +57,7 @@
by (induct_thm_tac BnorRset.induct "a m" 1);
by Auto_tac;
by (case_tac "a=b" 1);
-by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
+by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 2);
by (Asm_simp_tac 1);
by (ALLGOALS (stac BnorRset_eq));
by (rewtac Let_def);
@@ -96,14 +96,14 @@
by (cut_inst_tac [("a","a"),("m","m")] zcong_zless_unique 1);
by Auto_tac;
by (res_inst_tac [("m","m")] zcong_zless_imp_eq 2);
-by (auto_tac (claset() addIs [Bnor_mem_zle,Bnor_mem_zg,zcong_trans,
- zless_imp_zle,lemma],
+by (auto_tac (claset() addIs [Bnor_mem_zle, Bnor_mem_zg, zcong_trans,
+ order_less_imp_le, lemma],
simpset() addsimps [zcong_sym]));
by (res_inst_tac [("x","b")] exI 1);
by Safe_tac;
by (rtac Bnor_mem_if 1);
by (case_tac "b=#0" 2);
-by (auto_tac (claset() addIs [zle_neq_implies_zless], simpset()));
+by (auto_tac (claset() addIs [order_less_le RS iffD2], simpset()));
by (SELECT_GOAL (rewtac zcong_def) 2);
by (subgoal_tac "zgcd(a,m) = m" 2);
by (stac (zdvd_iff_zgcd RS sym) 3);
@@ -263,7 +263,7 @@
by (rewtac zcongm_def);
by (rtac RRset2norRR_correct1 3);
by (rtac RRset2norRR_inj 6);
-by (auto_tac (claset() addIs [zle_neq_implies_zless],
+by (auto_tac (claset() addIs [order_less_le RS iffD2],
simpset() addsimps [noX_is_RRset]));
by (rewrite_goals_tac [noXRRset_def,norRRset_def]);
by (rtac finite_imageI 1);
--- a/src/HOL/NumberTheory/IntPrimes.ML Wed Dec 13 10:31:08 2000 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.ML Wed Dec 13 10:31:46 2000 +0100
@@ -569,7 +569,7 @@
by (case_tac "b=#0" 2);
by (case_tac "y=#0" 3);
by (auto_tac (claset() addIs [zcong_trans,zcong_zless_0,
- zcong_zless_imp_eq,zle_neq_implies_zless],
+ zcong_zless_imp_eq,order_less_le],
simpset() addsimps [zcong_sym]));
by (rewrite_goals_tac [zcong_def,dvd_def]);
by (res_inst_tac [("x","a mod m")] exI 1);
@@ -725,6 +725,8 @@
by (simp_tac (simpset() addsimps [zmult_commute]) 1);
val lemma = result();
+bind_thm ("order_le_neq_implies_less", [order_less_le, conjI] MRS iffD2);
+
Goal "#0<r --> xzgcda(m,n,r',r,s',s,t',t) = (rn,sn,tn) \
\ --> r' = s'*m + t'*n --> r = s*m + t*n --> rn = sn*m + tn*n";
by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
@@ -737,7 +739,7 @@
by (asm_full_simp_tac (simpset() addsimps [xzgcda_eq]) 1);
by (SELECT_GOAL Safe_tac 1);
by (subgoal_tac "#0 < r' mod r" 1);
-by (rtac zle_neq_implies_zless 2);
+by (rtac order_le_neq_implies_less 2);
by (rtac pos_mod_sign 2);
by (cut_inst_tac [("m","m"),("n","n"),("r'","r'"),("r","r"),
("s'","s'"),("s","s"),("t'","t'"),("t","t")]
--- a/src/HOL/NumberTheory/WilsonBij.ML Wed Dec 13 10:31:08 2000 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.ML Wed Dec 13 10:31:46 2000 +0100
@@ -77,11 +77,11 @@
Goal "[| p:zprime; #1<a; a<p-#1 |] ==> #1<(inv p a)";
by (subgoal_tac "(inv p a) ~= #1" 1);
by (subgoal_tac "(inv p a) ~= #0" 1);
-by (rtac zle_neq_implies_zless 1);
+by (stac order_less_le 1);
by (stac (zle_add1_eq_le RS sym) 1);
-by (rtac zle_neq_implies_zless 1);
-by (rtac inv_not_0 4);
-by (rtac inv_not_1 7);
+by (stac order_less_le 1);
+by (rtac inv_not_0 2);
+by (rtac inv_not_1 5);
by Auto_tac;
by (rtac inv_ge 1);
by Auto_tac;
@@ -89,11 +89,8 @@
(* ditto *)
Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
-by (rtac zle_neq_implies_zless 1);
-by (rtac inv_not_p_minus_1 2);
-by Auto_tac;
-by (rtac inv_less 1);
-by Auto_tac;
+by (stac order_less_le 1);
+by (asm_full_simp_tac (simpset() addsimps [inv_not_p_minus_1, inv_less]) 1);
qed "inv_less_p_minus_1";
(************* Bijection *******************)
--- a/src/HOL/NumberTheory/WilsonRuss.ML Wed Dec 13 10:31:08 2000 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.ML Wed Dec 13 10:31:46 2000 +0100
@@ -84,11 +84,11 @@
by (case_tac "#0<=(inv p a)" 1);
by (subgoal_tac "(inv p a) ~= #1" 1);
by (subgoal_tac "(inv p a) ~= #0" 1);
-by (rtac zle_neq_implies_zless 1);
+by (stac order_less_le 1);
by (stac (zle_add1_eq_le RS sym) 1);
-by (rtac zle_neq_implies_zless 1);
-by (rtac inv_not_0 4);
-by (rtac inv_not_1 7);
+by (stac order_less_le 1);
+by (rtac inv_not_0 2);
+by (rtac inv_not_1 5);
by Auto_tac;
by (rewrite_goals_tac [inv_def,zprime_def]);
by (asm_full_simp_tac (simpset() addsimps [pos_mod_sign]) 1);
@@ -96,8 +96,8 @@
Goal "[| p:zprime; #1<a; a<p-#1 |] ==> (inv p a)<p-#1";
by (case_tac "(inv p a)<p" 1);
-by (rtac zle_neq_implies_zless 1);
-by (rtac inv_not_p_minus_1 2);
+by (stac order_less_le 1);
+by (asm_full_simp_tac (simpset() addsimps [inv_not_p_minus_1]) 1);
by Auto_tac;
by (rewrite_goals_tac [inv_def,zprime_def]);
by (asm_full_simp_tac (simpset() addsimps [pos_mod_bound]) 1);
@@ -275,12 +275,6 @@
(********** Wilson *************)
-Goal "[| z-#1<=w; z-#1~=w |] ==> z<=(w::int)";
-by (stac (zle_add1_eq_le RS sym) 1);
-by (rtac zle_neq_implies_zless 1);
-by Auto_tac;
-val lemma = result();
-
Goalw [zprime_def,dvd_def] "[| p : zprime; p ~= #2; p ~= #3 |] ==> #5<=p";
by (case_tac "p=#4" 1);
by Auto_tac;
@@ -291,10 +285,7 @@
by Safe_tac;
by (res_inst_tac [("x","#2")] exI 1);
by Auto_tac;
-by (rtac lemma 1);
-by (rtac lemma 1);
-by (rtac lemma 1);
-by Auto_tac;
+by (arith_tac 1);
qed "prime_g_5";
Goal "p:zprime ==> [zfact(p-#1) = #-1] (mod p)";