Replaced n ~= 0 by 0 < n
authornipkow
Wed Dec 03 17:25:43 1997 +0100 (1997-12-03)
changeset 43560dfd34f0d33d
parent 4355 68c7c544570c
child 4357 b852e2d2a39a
Replaced n ~= 0 by 0 < n
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Hoare/Examples.ML
src/HOL/NatDef.ML
src/HOL/Univ.ML
src/HOL/ex/Primes.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Dec 03 12:55:04 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Dec 03 17:25:43 1997 +0100
     1.3 @@ -536,6 +536,7 @@
     1.4  by (induct_tac "n" 2);
     1.5  by (ALLGOALS Asm_simp_tac);
     1.6  qed "zero_less_mult_iff";
     1.7 +Addsimps [zero_less_mult_iff];
     1.8  
     1.9  goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
    1.10  by (induct_tac "m" 1);
    1.11 @@ -544,6 +545,7 @@
    1.12  by (Simp_tac 1);
    1.13  by (fast_tac (claset() addss simpset()) 1);
    1.14  qed "mult_eq_1_iff";
    1.15 +Addsimps [mult_eq_1_iff];
    1.16  
    1.17  goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
    1.18  by (safe_tac (claset() addSIs [mult_less_mono1]));
    1.19 @@ -594,8 +596,7 @@
    1.20  by (rtac disjCI 1);
    1.21  by (rtac nat_less_cases 1 THEN assume_tac 2);
    1.22  by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
    1.23 -by (best_tac (claset() addDs [mult_less_mono2] 
    1.24 -                      addss (simpset() addsimps [zero_less_eq RS sym])) 1);
    1.25 +by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
    1.26  qed "mult_eq_self_implies_10";
    1.27  
    1.28  
     2.1 --- a/src/HOL/Divides.ML	Wed Dec 03 12:55:04 1997 +0100
     2.2 +++ b/src/HOL/Divides.ML	Wed Dec 03 17:25:43 1997 +0100
     2.3 @@ -223,7 +223,7 @@
     2.4  by (subgoal_tac "k mod 2 < 2" 1);
     2.5  by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
     2.6  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
     2.7 -by (Blast_tac 1);
     2.8 +by Safe_tac;
     2.9  qed "mod2_cases";
    2.10  
    2.11  goal thy "Suc(Suc(m)) mod 2 = m mod 2";
    2.12 @@ -234,13 +234,20 @@
    2.13  qed "mod2_Suc_Suc";
    2.14  Addsimps [mod2_Suc_Suc];
    2.15  
    2.16 +(* FIXME: this thm is subsumed by the next one. Get rid of it. *)
    2.17  goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1";
    2.18  by (subgoal_tac "m mod 2 < 2" 1);
    2.19  by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
    2.20 -by (safe_tac (claset() addSEs [lessE]));
    2.21 -by (ALLGOALS (blast_tac (claset() addIs [sym])));
    2.22 +by (Asm_full_simp_tac 1);
    2.23 +by (trans_tac 1);
    2.24  qed "mod2_neq_0";
    2.25  
    2.26 +goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
    2.27 +by (rtac iffI 1);
    2.28 +by(ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod2_neq_0])));
    2.29 +qed "mod2_gr_0";
    2.30 +Addsimps [mod2_gr_0];
    2.31 +
    2.32  goal thy "(m+m) mod 2 = 0";
    2.33  by (induct_tac "m" 1);
    2.34  by (simp_tac (simpset() addsimps [mod_less]) 1);
    2.35 @@ -356,10 +363,10 @@
    2.36                                       mult_mod_distrib, add_mult_distrib2]) 1);
    2.37  qed "dvd_mod";
    2.38  
    2.39 -goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
    2.40 +goal thy "!!k. [| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
    2.41  by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
    2.42  by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
    2.43 -by (asm_full_simp_tac (simpset() addsimps [mod_div_equality, zero_less_eq]) 1);
    2.44 +by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
    2.45  qed "dvd_mod_imp_dvd";
    2.46  
    2.47  goalw thy [dvd_def]  "!!k m n. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
     3.1 --- a/src/HOL/Hoare/Examples.ML	Wed Dec 03 12:55:04 1997 +0100
     3.2 +++ b/src/HOL/Hoare/Examples.ML	Wed Dec 03 17:25:43 1997 +0100
     3.3 @@ -67,8 +67,6 @@
     3.4  
     3.5  by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
     3.6  
     3.7 -by Safe_tac;
     3.8 -
     3.9  by (subgoal_tac "a*a=a pow 2" 1);
    3.10  by (Asm_simp_tac 1);
    3.11  by (stac pow_pow_reduce 1);
    3.12 @@ -77,16 +75,12 @@
    3.13  by (subgoal_tac "0<2" 2);
    3.14  by (dres_inst_tac [("m","b")] mod_div_equality 2);
    3.15  
    3.16 -by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
    3.17 +by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[pow_0,pow_Suc,mult_assoc])));
    3.18  
    3.19 -by (subgoal_tac "b~=0" 1);
    3.20  by (res_inst_tac [("n","b")] natE 1);
    3.21 -by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
    3.22 -by (assume_tac 4);
    3.23 -
    3.24 -by (ALLGOALS (asm_full_simp_tac ((simpset_of Arith.thy) addsimps [pow_0,pow_Suc,mult_assoc])));
    3.25 -by (rtac mod_less 1);
    3.26 -by (Simp_tac 1);
    3.27 +by (hyp_subst_tac 1);
    3.28 +by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
    3.29 +by (asm_simp_tac (simpset() addsimps [pow_Suc]) 1);
    3.30  
    3.31  qed "power_by_mult";
    3.32  
     4.1 --- a/src/HOL/NatDef.ML	Wed Dec 03 12:55:04 1997 +0100
     4.2 +++ b/src/HOL/NatDef.ML	Wed Dec 03 17:25:43 1997 +0100
     4.3 @@ -291,15 +291,33 @@
     4.4  by (cut_facts_tac prems 1);
     4.5  by (ALLGOALS Asm_full_simp_tac);
     4.6  qed "gr_implies_not0";
     4.7 -Addsimps [gr_implies_not0];
     4.8 +
     4.9 +goal thy "(n ~= 0) = (0 < n)";
    4.10 +br iffI 1;
    4.11 + by(etac gr_implies_not0 2);
    4.12 +by(rtac natE 1);
    4.13 + by(contr_tac 1);
    4.14 +by(etac ssubst 1);
    4.15 +by(rtac zero_less_Suc 1);
    4.16 +qed "neq0_conv";
    4.17 +Addsimps [neq0_conv];
    4.18 +AddSDs [neq0_conv RS iffD1];
    4.19 +
    4.20 +bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
    4.21  
    4.22 -qed_goal "zero_less_eq" thy "0 < n = (n ~= 0)" (fn _ => [
    4.23 -        rtac iffI 1,
    4.24 -        etac gr_implies_not0 1,
    4.25 -        rtac natE 1,
    4.26 -        contr_tac 1,
    4.27 -        etac ssubst 1,
    4.28 -        rtac zero_less_Suc 1]);
    4.29 +goal thy "(~(0 < n)) = (n=0)";
    4.30 +br iffI 1;
    4.31 + be swap 1;
    4.32 + by(ALLGOALS Asm_full_simp_tac);
    4.33 +qed "not_gr0";
    4.34 +Addsimps [not_gr0];
    4.35 +
    4.36 +goal thy "!!m. m<n ==> 0 < n";
    4.37 +by (dtac gr_implies_not0 1);
    4.38 +by (Asm_full_simp_tac 1);
    4.39 +qed "gr_implies_gr0";
    4.40 +Addsimps [gr_implies_gr0];
    4.41 +
    4.42  
    4.43  (** Inductive (?) properties **)
    4.44  
     5.1 --- a/src/HOL/Univ.ML	Wed Dec 03 12:55:04 1997 +0100
     5.2 +++ b/src/HOL/Univ.ML	Wed Dec 03 17:25:43 1997 +0100
     5.3 @@ -215,12 +215,13 @@
     5.4  by (etac less_zeroE 1);
     5.5  qed "ndepth_K0";
     5.6  
     5.7 -goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case (Suc i) f k ~= 0";
     5.8 +goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> 0 < nat_case (Suc i) f k";
     5.9  by (nat_ind_tac "k" 1);
    5.10  by (ALLGOALS Simp_tac);
    5.11  by (rtac impI 1);
    5.12 -by (etac not_less_Least 1);
    5.13 -qed "ndepth_Push_lemma";
    5.14 +by (dtac not_less_Least 1);
    5.15 +by (Asm_full_simp_tac 1);
    5.16 +val lemma = result();
    5.17  
    5.18  goalw Univ.thy [ndepth_def,Push_Node_def]
    5.19      "ndepth (Push_Node i n) = Suc(ndepth(n))";
    5.20 @@ -233,7 +234,7 @@
    5.21  by (rewtac Push_def);
    5.22  by (rtac (nat_case_Suc RS trans) 1);
    5.23  by (etac LeastI 1);
    5.24 -by (etac (ndepth_Push_lemma RS mp) 1);
    5.25 +by (asm_simp_tac (simpset() addsimps [lemma]) 1);
    5.26  qed "ndepth_Push_Node";
    5.27  
    5.28  
     6.1 --- a/src/HOL/ex/Primes.ML	Wed Dec 03 12:55:04 1997 +0100
     6.2 +++ b/src/HOL/ex/Primes.ML	Wed Dec 03 17:25:43 1997 +0100
     6.3 @@ -23,7 +23,7 @@
     6.4      and induction rule **)
     6.5  
     6.6  Tfl.tgoalw thy [] gcd.rules;
     6.7 -by (simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq]) 1);
     6.8 +by (simp_tac (simpset() addsimps [mod_less_divisor]) 1);
     6.9  val tc = result();
    6.10  
    6.11  val gcd_eq = tc RS hd gcd.rules;
    6.12 @@ -37,6 +37,7 @@
    6.13  goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
    6.14  by (rtac (gcd_eq RS trans) 1);
    6.15  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    6.16 +by (Blast_tac 1);
    6.17  qed "gcd_less_0";
    6.18  Addsimps [gcd_0, gcd_less_0];
    6.19  
    6.20 @@ -52,8 +53,7 @@
    6.21  goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
    6.22  by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
    6.23  by (case_tac "n=0" 1);
    6.24 -by (ALLGOALS 
    6.25 -    (asm_simp_tac (simpset() addsimps [mod_less_divisor,zero_less_eq])));
    6.26 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod_less_divisor])));
    6.27  by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
    6.28  qed "gcd_divides_both";
    6.29  
    6.30 @@ -62,9 +62,7 @@
    6.31  goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
    6.32  by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
    6.33  by (case_tac "n=0" 1);
    6.34 -by (ALLGOALS 
    6.35 -    (asm_simp_tac (simpset() addsimps [dvd_mod, mod_less_divisor,
    6.36 -				      zero_less_eq])));
    6.37 +by (ALLGOALS(asm_full_simp_tac(simpset() addsimps[dvd_mod,mod_less_divisor])));
    6.38  qed_spec_mp "gcd_greatest";
    6.39  
    6.40  (*Function gcd yields the Greatest Common Divisor*)
    6.41 @@ -83,8 +81,8 @@
    6.42  by (case_tac "k=0" 1);
    6.43  by (case_tac "n=0" 2);
    6.44  by (ALLGOALS 
    6.45 -    (asm_simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq,
    6.46 -				      mod_geq, mod_mult_distrib2])));
    6.47 +    (asm_full_simp_tac (simpset() addsimps
    6.48 +       [mod_less_divisor, mod_geq, mod_mult_distrib2])));
    6.49  qed "gcd_mult_distrib2";
    6.50  
    6.51  (*This theorem leads immediately to a proof of the uniqueness of factorization.