# HG changeset patch
# User nipkow
# Date 881166343 -3600
# Node ID 0dfd34f0d33dab1d7b8d7d3492e82c0518dbda9f
# Parent  68c7c544570c5ace95bedbdd1e5f36cc2434c854
Replaced n ~= 0 by 0 < n

diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/Arith.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -536,6 +536,7 @@
 by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "zero_less_mult_iff";
+Addsimps [zero_less_mult_iff];
 
 goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
 by (induct_tac "m" 1);
@@ -544,6 +545,7 @@
 by (Simp_tac 1);
 by (fast_tac (claset() addss simpset()) 1);
 qed "mult_eq_1_iff";
+Addsimps [mult_eq_1_iff];
 
 goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
 by (safe_tac (claset() addSIs [mult_less_mono1]));
@@ -594,8 +596,7 @@
 by (rtac disjCI 1);
 by (rtac nat_less_cases 1 THEN assume_tac 2);
 by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
-by (best_tac (claset() addDs [mult_less_mono2] 
-                      addss (simpset() addsimps [zero_less_eq RS sym])) 1);
+by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
 qed "mult_eq_self_implies_10";
 
 
diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/Divides.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -223,7 +223,7 @@
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
-by (Blast_tac 1);
+by Safe_tac;
 qed "mod2_cases";
 
 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
@@ -234,13 +234,20 @@
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
 
+(* FIXME: this thm is subsumed by the next one. Get rid of it. *)
 goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
 by (subgoal_tac "m mod 2 < 2" 1);
 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (safe_tac (claset() addSEs [lessE]));
-by (ALLGOALS (blast_tac (claset() addIs [sym])));
+by (Asm_full_simp_tac 1);
+by (trans_tac 1);
 qed "mod2_neq_0";
 
+goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
+by (rtac iffI 1);
+by(ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod2_neq_0])));
+qed "mod2_gr_0";
+Addsimps [mod2_gr_0];
+
 goal thy "(m+m) mod 2 = 0";
 by (induct_tac "m" 1);
 by (simp_tac (simpset() addsimps [mod_less]) 1);
@@ -356,10 +363,10 @@
                                      mult_mod_distrib, add_mult_distrib2]) 1);
 qed "dvd_mod";
 
-goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
+goal thy "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
 by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
-by (asm_full_simp_tac (simpset() addsimps [mod_div_equality, zero_less_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
 qed "dvd_mod_imp_dvd";
 
 goalw thy [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/Hoare/Examples.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -67,8 +67,6 @@
 
 by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
 
-by Safe_tac;
-
 by (subgoal_tac "a*a=a pow 2" 1);
 by (Asm_simp_tac 1);
 by (stac pow_pow_reduce 1);
@@ -77,16 +75,12 @@
 by (subgoal_tac "0<2" 2);
 by (dres_inst_tac [("m","b")] mod_div_equality 2);
 
-by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
+by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[pow_0,pow_Suc,mult_assoc])));
 
-by (subgoal_tac "b~=0" 1);
 by (res_inst_tac [("n","b")] natE 1);
-by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
-by (assume_tac 4);
-
-by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
-by (rtac mod_less 1);
-by (Simp_tac 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
+by (asm_simp_tac (simpset() addsimps [pow_Suc]) 1);
 
 qed "power_by_mult";
 
diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/NatDef.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -291,15 +291,33 @@
 by (cut_facts_tac prems 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "gr_implies_not0";
-Addsimps [gr_implies_not0];
+
+goal thy "(n ~= 0) = (0 < n)";
+br iffI 1;
+ by(etac gr_implies_not0 2);
+by(rtac natE 1);
+ by(contr_tac 1);
+by(etac ssubst 1);
+by(rtac zero_less_Suc 1);
+qed "neq0_conv";
+Addsimps [neq0_conv];
+AddSDs [neq0_conv RS iffD1];
+
+bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
 
-qed_goal "zero_less_eq" thy "0 < n = (n ~= 0)" (fn _ => [
-        rtac iffI 1,
-        etac gr_implies_not0 1,
-        rtac natE 1,
-        contr_tac 1,
-        etac ssubst 1,
-        rtac zero_less_Suc 1]);
+goal thy "(~(0 < n)) = (n=0)";
+br iffI 1;
+ be swap 1;
+ by(ALLGOALS Asm_full_simp_tac);
+qed "not_gr0";
+Addsimps [not_gr0];
+
+goal thy "!!m. m<n ==> 0 < n";
+by (dtac gr_implies_not0 1);
+by (Asm_full_simp_tac 1);
+qed "gr_implies_gr0";
+Addsimps [gr_implies_gr0];
+
 
 (** Inductive (?) properties **)
 
diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/Univ.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -215,12 +215,13 @@
 by (etac less_zeroE 1);
 qed "ndepth_K0";
 
-goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case (Suc i) f k ~= 0";
+goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> 0 < nat_case (Suc i) f k";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Simp_tac);
 by (rtac impI 1);
-by (etac not_less_Least 1);
-qed "ndepth_Push_lemma";
+by (dtac not_less_Least 1);
+by (Asm_full_simp_tac 1);
+val lemma = result();
 
 goalw Univ.thy [ndepth_def,Push_Node_def]
     "ndepth (Push_Node i n) = Suc(ndepth(n))";
@@ -233,7 +234,7 @@
 by (rewtac Push_def);
 by (rtac (nat_case_Suc RS trans) 1);
 by (etac LeastI 1);
-by (etac (ndepth_Push_lemma RS mp) 1);
+by (asm_simp_tac (simpset() addsimps [lemma]) 1);
 qed "ndepth_Push_Node";
 
 
diff -r 68c7c544570c -r 0dfd34f0d33d src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Wed Dec 03 12:55:04 1997 +0100
+++ b/src/HOL/ex/Primes.ML	Wed Dec 03 17:25:43 1997 +0100
@@ -23,7 +23,7 @@
     and induction rule **)
 
 Tfl.tgoalw thy [] gcd.rules;
-by (simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq]) 1);
+by (simp_tac (simpset() addsimps [mod_less_divisor]) 1);
 val tc = result();
 
 val gcd_eq = tc RS hd gcd.rules;
@@ -37,6 +37,7 @@
 goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
 by (rtac (gcd_eq RS trans) 1);
 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Blast_tac 1);
 qed "gcd_less_0";
 Addsimps [gcd_0, gcd_less_0];
 
@@ -52,8 +53,7 @@
 goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [mod_less_divisor,zero_less_eq])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod_less_divisor])));
 by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
 qed "gcd_divides_both";
 
@@ -62,9 +62,7 @@
 goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
-by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [dvd_mod, mod_less_divisor,
-				      zero_less_eq])));
+by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[dvd_mod,mod_less_divisor])));
 qed_spec_mp "gcd_greatest";
 
 (*Function gcd yields the Greatest Common Divisor*)
@@ -83,8 +81,8 @@
 by (case_tac "k=0" 1);
 by (case_tac "n=0" 2);
 by (ALLGOALS 
-    (asm_simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq,
-				      mod_geq, mod_mult_distrib2])));
+    (asm_full_simp_tac (simpset() addsimps
+       [mod_less_divisor, mod_geq, mod_mult_distrib2])));
 qed "gcd_mult_distrib2";
 
 (*This theorem leads immediately to a proof of the uniqueness of factorization.