src/HOL/NumberTheory/IntPrimes.thy
changeset 13517 42efec18f5b2
parent 13193 d5234c261813
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 23 07:34:20 2002 +0200
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Aug 23 07:41:05 2002 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
     1.5    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
     1.6     apply (simp add: zmod_zdiv_equality [symmetric])
     1.7 -  apply (simp add: zdvd_zadd zdvd_zmult2)
     1.8 +  apply (simp only: zdvd_zadd zdvd_zmult2)
     1.9    done
    1.10  
    1.11  lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)"
    1.12 @@ -602,8 +602,7 @@
    1.13    apply (rule_tac x = "a mod m" in exI)
    1.14    apply (auto simp add: pos_mod_sign pos_mod_bound)
    1.15    apply (rule_tac x = "-(a div m)" in exI)
    1.16 -  apply (cut_tac a = a and b = m in zmod_zdiv_equality)
    1.17 -  apply auto
    1.18 +  apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
    1.19    done
    1.20  
    1.21  lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
    1.22 @@ -624,13 +623,8 @@
    1.23    done
    1.24  
    1.25  lemma aux: "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
    1.26 -  apply (rule_tac "s" = "(m * (a div m) + a mod m) - (m * (b div m) + b mod m)"
    1.27 -    in trans)
    1.28 -   prefer 2
    1.29 -   apply (simp add: zdiff_zmult_distrib2)
    1.30 -  apply (rule aux)
    1.31 -   apply (rule_tac [!] zmod_zdiv_equality)
    1.32 -  done
    1.33 +by(simp add: zdiff_zmult_distrib2 zadd_zdiff_eq eq_zdiff_eq zadd_ac)
    1.34 +
    1.35  
    1.36  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
    1.37    apply (unfold zcong_def)
    1.38 @@ -685,9 +679,7 @@
    1.39     prefer 2
    1.40     apply (subst zcong_iff_lin)
    1.41     apply (rule_tac x = "k * (a div (m * k))" in exI)
    1.42 -   apply (subst zadd_commute)
    1.43 -   apply (subst zmult_assoc [symmetric])
    1.44 -   apply (rule_tac zmod_zdiv_equality)
    1.45 +   apply(simp add:zmult_assoc [symmetric])
    1.46    apply assumption
    1.47    done
    1.48  
    1.49 @@ -756,11 +748,7 @@
    1.50      ==> (r' mod r) = (s' - (r' div r) * s) * m + (t' - (r' div r) * t) * (n::int)"
    1.51    apply (rule trans)
    1.52     apply (rule_tac [2] aux [symmetric])
    1.53 -  apply simp
    1.54 -  apply (subst eq_zdiff_eq)
    1.55 -  apply (rule trans [symmetric])
    1.56 -  apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality)
    1.57 -  apply (simp add: zmult_commute)
    1.58 +  apply (simp add: eq_zdiff_eq zmult_commute)
    1.59    done
    1.60  
    1.61  lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y"