src/HOL/GCD.thy

changeset 60687 | 33dbbcb6a8a3 |

parent 60686 | ea5bc46c11e6 |

child 60688 | 01488b559910 |

--- a/src/HOL/GCD.thy Wed Jul 08 14:01:39 2015 +0200 +++ b/src/HOL/GCD.thy Wed Jul 08 14:01:40 2015 +0200 @@ -399,7 +399,7 @@ by (rule dvd_0_left, rule Gcd_greatest) simp lemma Gcd_0_iff [simp]: - "Gcd A = 0 \<longleftrightarrow> (\<forall>a\<in>A. a = 0)" (is "?P \<longleftrightarrow> ?Q") + "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q") proof assume ?P show ?Q @@ -407,7 +407,8 @@ fix a assume "a \<in> A" then have "Gcd A dvd a" by (rule Gcd_dvd) - with \<open>?P\<close> show "a = 0" by simp + with \<open>?P\<close> have "a = 0" by simp + then show "a \<in> {0}" by simp qed next assume ?Q @@ -415,7 +416,7 @@ proof (rule Gcd_greatest) fix a assume "a \<in> A" - with \<open>?Q\<close> have "a = 0" by simp + with \<open>?Q\<close> have "a = 0" by auto then show "0 dvd a" by simp qed then show ?P by simp @@ -424,7 +425,7 @@ lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)" proof (cases "Gcd A = 0") - case True then show ?thesis by simp + case True then show ?thesis by auto next case False from unit_factor_mult_normalize @@ -432,7 +433,7 @@ then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp with False have "unit_factor (Gcd A) = 1" by simp - with False show ?thesis by simp + with False show ?thesis by auto qed lemma Gcd_UNIV [simp]: @@ -473,7 +474,7 @@ ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))" by (rule associatedI) then show ?thesis - by (rule associated_eqI) (simp_all add: unit_factor_gcd unit_factor_Gcd) + by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd) qed lemma dvd_Gcd: -- \<open>FIXME remove\<close> @@ -509,7 +510,7 @@ then have "associated (Gcd (normalize ` A)) (Gcd A)" by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd) then show ?thesis - by (rule associated_eqI) (simp_all add: unit_factor_Gcd) + by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec) qed lemma Lcm_least: