# HG changeset patch
# User paulson
# Date 976699906 -3600
# Node ID b9d43a2add79cc88f21a29f5a2bafad82de62299
# Parent  7e5d659899bfff26a5cdc0a736b6b663a9bffc8d
tidying and replacement of "integer" rules by "order" ones

diff -r 7e5d659899bf -r b9d43a2add79 src/HOL/NumberTheory/Chinese.ML
--- 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();
 
diff -r 7e5d659899bf -r b9d43a2add79 src/HOL/NumberTheory/EulerFermat.ML
--- 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);
diff -r 7e5d659899bf -r b9d43a2add79 src/HOL/NumberTheory/IntPrimes.ML
--- 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")] 
diff -r 7e5d659899bf -r b9d43a2add79 src/HOL/NumberTheory/WilsonBij.ML
--- 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  *******************)
diff -r 7e5d659899bf -r b9d43a2add79 src/HOL/NumberTheory/WilsonRuss.ML
--- 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)";