src/HOL/GCD.thy
changeset 41550 efa734d9b221
parent 37770 cddb3106adb8
child 41792 ff3cb0c418b7
     1.1 --- a/src/HOL/GCD.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -36,11 +36,8 @@
     1.4  subsection {* GCD and LCM definitions *}
     1.5  
     1.6  class gcd = zero + one + dvd +
     1.7 -
     1.8 -fixes
     1.9 -  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    1.10 -  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.11 -
    1.12 +  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.13 +    and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.14  begin
    1.15  
    1.16  abbreviation
    1.17 @@ -186,7 +183,7 @@
    1.18        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
    1.19        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
    1.20    shows "P (lcm x y)"
    1.21 -by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
    1.22 +  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
    1.23  
    1.24  lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
    1.25    by (simp add: lcm_int_def)
    1.26 @@ -632,13 +629,12 @@
    1.27    apply (subgoal_tac "b' = b div gcd a b")
    1.28    apply (erule ssubst)
    1.29    apply (rule div_gcd_coprime_nat)
    1.30 -  using prems
    1.31 -  apply force
    1.32 +  using z apply force
    1.33    apply (subst (1) b)
    1.34    using z apply force
    1.35    apply (subst (1) a)
    1.36    using z apply force
    1.37 -done
    1.38 +  done
    1.39  
    1.40  lemma gcd_coprime_int:
    1.41    assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
    1.42 @@ -650,13 +646,12 @@
    1.43    apply (subgoal_tac "b' = b div gcd a b")
    1.44    apply (erule ssubst)
    1.45    apply (rule div_gcd_coprime_int)
    1.46 -  using prems
    1.47 -  apply force
    1.48 +  using z apply force
    1.49    apply (subst (1) b)
    1.50    using z apply force
    1.51    apply (subst (1) a)
    1.52    using z apply force
    1.53 -done
    1.54 +  done
    1.55  
    1.56  lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
    1.57      shows "coprime d (a * b)"
    1.58 @@ -1192,13 +1187,13 @@
    1.59         by auto
    1.60       moreover
    1.61       {assume db: "d=b"
    1.62 -       from prems have ?thesis apply simp
    1.63 +       with nz H have ?thesis apply simp
    1.64           apply (rule exI[where x = b], simp)
    1.65           apply (rule exI[where x = b])
    1.66          by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
    1.67      moreover
    1.68      {assume db: "d < b"
    1.69 -        {assume "x=0" hence ?thesis  using prems by simp }
    1.70 +        {assume "x=0" hence ?thesis using nz H by simp }
    1.71          moreover
    1.72          {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
    1.73            from db have "d \<le> b - 1" by simp