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.10  lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
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.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.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.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)"