src/HOL/GCD.thy
changeset 35216 7641e8d831d2
parent 35028 108662d50512
child 35368 19b340c3f1ff
     1.1 --- a/src/HOL/GCD.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/GCD.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -156,7 +156,7 @@
     1.4        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
     1.5        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
     1.6    shows "P (gcd x y)"
     1.7 -by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
     1.8 +by (insert assms, auto, arith)
     1.9  
    1.10  lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
    1.11    by (simp add: gcd_int_def)
    1.12 @@ -457,7 +457,7 @@
    1.13    apply (case_tac "y > 0")
    1.14    apply (subst gcd_non_0_int, auto)
    1.15    apply (insert gcd_non_0_int [of "-y" "-x"])
    1.16 -  apply (auto simp add: gcd_neg1_int gcd_neg2_int)
    1.17 +  apply auto
    1.18  done
    1.19  
    1.20  lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
    1.21 @@ -557,7 +557,7 @@
    1.22    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.23      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    1.24        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    1.25 -  have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
    1.26 +  have "?g \<noteq> 0" using nz by simp
    1.27    then have gp: "?g > 0" by arith
    1.28    from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
    1.29    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
    1.30 @@ -824,7 +824,7 @@
    1.31    {assume "?g = 0" with ab n have ?thesis by auto }
    1.32    moreover
    1.33    {assume z: "?g \<noteq> 0"
    1.34 -    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
    1.35 +    hence zn: "?g ^ n \<noteq> 0" using n by simp
    1.36      from gcd_coprime_exists_nat[OF z]
    1.37      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
    1.38        by blast
    1.39 @@ -852,7 +852,7 @@
    1.40    {assume "?g = 0" with ab n have ?thesis by auto }
    1.41    moreover
    1.42    {assume z: "?g \<noteq> 0"
    1.43 -    hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
    1.44 +    hence zn: "?g ^ n \<noteq> 0" using n by simp
    1.45      from gcd_coprime_exists_int[OF z]
    1.46      obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
    1.47        by blast
    1.48 @@ -1109,7 +1109,7 @@
    1.49      (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
    1.50    using ex
    1.51    apply clarsimp
    1.52 -  apply (rule_tac x="d" in exI, simp add: dvd_add)
    1.53 +  apply (rule_tac x="d" in exI, simp)
    1.54    apply (case_tac "a * x = b * y + d" , simp_all)
    1.55    apply (rule_tac x="x + y" in exI)
    1.56    apply (rule_tac x="y" in exI)
    1.57 @@ -1124,10 +1124,10 @@
    1.58    apply(induct a b rule: ind_euclid)
    1.59    apply blast
    1.60    apply clarify
    1.61 -  apply (rule_tac x="a" in exI, simp add: dvd_add)
    1.62 +  apply (rule_tac x="a" in exI, simp)
    1.63    apply clarsimp
    1.64    apply (rule_tac x="d" in exI)
    1.65 -  apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
    1.66 +  apply (case_tac "a * x = b * y + d", simp_all)
    1.67    apply (rule_tac x="x+y" in exI)
    1.68    apply (rule_tac x="y" in exI)
    1.69    apply algebra
    1.70 @@ -1693,8 +1693,7 @@
    1.71    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    1.72     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
    1.73  apply(auto simp add:inj_on_def)
    1.74 -apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    1.75 -             dvd.neq_le_trans dvd_triv_left)
    1.76 +apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
    1.77  apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    1.78               dvd.neq_le_trans dvd_triv_right mult_commute)
    1.79  done