src/HOL/GCD.thy
changeset 60687 33dbbcb6a8a3
parent 60686 ea5bc46c11e6
child 60688 01488b559910
     1.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:39 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
     1.3 @@ -399,7 +399,7 @@
     1.4    by (rule dvd_0_left, rule Gcd_greatest) simp
     1.5  
     1.6  lemma Gcd_0_iff [simp]:
     1.7 -  "Gcd A = 0 \<longleftrightarrow> (\<forall>a\<in>A. a = 0)" (is "?P \<longleftrightarrow> ?Q")
     1.8 +  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
     1.9  proof
    1.10    assume ?P
    1.11    show ?Q
    1.12 @@ -407,7 +407,8 @@
    1.13      fix a
    1.14      assume "a \<in> A"
    1.15      then have "Gcd A dvd a" by (rule Gcd_dvd)
    1.16 -    with \<open>?P\<close> show "a = 0" by simp
    1.17 +    with \<open>?P\<close> have "a = 0" by simp
    1.18 +    then show "a \<in> {0}" by simp
    1.19    qed
    1.20  next
    1.21    assume ?Q
    1.22 @@ -415,7 +416,7 @@
    1.23    proof (rule Gcd_greatest)
    1.24      fix a
    1.25      assume "a \<in> A"
    1.26 -    with \<open>?Q\<close> have "a = 0" by simp
    1.27 +    with \<open>?Q\<close> have "a = 0" by auto
    1.28      then show "0 dvd a" by simp
    1.29    qed
    1.30    then show ?P by simp
    1.31 @@ -424,7 +425,7 @@
    1.32  lemma unit_factor_Gcd:
    1.33    "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
    1.34  proof (cases "Gcd A = 0")
    1.35 -  case True then show ?thesis by simp
    1.36 +  case True then show ?thesis by auto
    1.37  next
    1.38    case False
    1.39    from unit_factor_mult_normalize
    1.40 @@ -432,7 +433,7 @@
    1.41    then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
    1.42    then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
    1.43    with False have "unit_factor (Gcd A) = 1" by simp
    1.44 -  with False show ?thesis by simp
    1.45 +  with False show ?thesis by auto
    1.46  qed
    1.47  
    1.48  lemma Gcd_UNIV [simp]:
    1.49 @@ -473,7 +474,7 @@
    1.50    ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
    1.51      by (rule associatedI)
    1.52    then show ?thesis
    1.53 -    by (rule associated_eqI) (simp_all add: unit_factor_gcd unit_factor_Gcd)
    1.54 +    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
    1.55  qed
    1.56  
    1.57  lemma dvd_Gcd: -- \<open>FIXME remove\<close>
    1.58 @@ -509,7 +510,7 @@
    1.59    then have "associated (Gcd (normalize ` A)) (Gcd A)"
    1.60      by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
    1.61    then show ?thesis
    1.62 -    by (rule associated_eqI) (simp_all add: unit_factor_Gcd)
    1.63 +    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
    1.64  qed
    1.65  
    1.66  lemma Lcm_least: