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:
```