src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 60599 f8bb070dc98b parent 60598 78ca5674c66a child 60600 87fbfea0bd0a
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:34 2015 +0200
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Jun 27 20:20:36 2015 +0200
1.3 @@ -82,27 +82,29 @@
1.4    by (cases "a = 0") simp_all
1.5
1.6  lemma associated_iff_normed_eq:
1.7 -  "associated a b \<longleftrightarrow> a div normalization_factor a = b div normalization_factor b"
1.8 -proof (cases "b = 0", simp, cases "a = 0", metis associated_0(1) normalization_0_iff, rule iffI)
1.9 -  let ?nf = normalization_factor
1.10 -  assume "a \<noteq> 0" "b \<noteq> 0" "a div ?nf a = b div ?nf b"
1.11 -  hence "a = b * (?nf a div ?nf b)"
1.12 -    apply (subst (asm) unit_eq_div1, blast, subst (asm) unit_div_commute, blast)
1.13 -    apply (subst div_mult_swap, simp, simp)
1.14 -    done
1.15 -  with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> have "\<exists>c. is_unit c \<and> a = c * b"
1.16 -    by (intro exI[of _ "?nf a div ?nf b"], force simp: mult_ac)
1.17 -  then obtain c where "is_unit c" and "a = c * b" by blast
1.18 -  then show "associated a b" by (rule is_unit_associatedI)
1.19 +  "associated a b \<longleftrightarrow> a div normalization_factor a = b div normalization_factor b" (is "?P \<longleftrightarrow> ?Q")
1.20 +proof (cases "a = 0 \<or> b = 0")
1.21 +  case True then show ?thesis by (auto dest: sym)
1.22  next
1.23 -  let ?nf = normalization_factor
1.24 -  assume "a \<noteq> 0" "b \<noteq> 0" "associated a b"
1.25 -  then obtain c where "is_unit c" and "a = c * b" by (blast elim: associated_is_unitE)
1.26 -  then show "a div ?nf a = b div ?nf b"
1.27 -    apply (simp only: \<open>a = c * b\<close> normalization_factor_mult normalization_factor_unit)
1.28 -    apply (rule div_mult_mult1, force)
1.29 -    done
1.30 +  case False then have "a \<noteq> 0" and "b \<noteq> 0" by auto
1.31 +  show ?thesis
1.32 +  proof
1.33 +    assume ?Q
1.34 +    from \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close>
1.35 +    have "is_unit (normalization_factor a div normalization_factor b)"
1.36 +      by auto
1.37 +    moreover from \<open>?Q\<close> \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close>
1.38 +    have "a = (normalization_factor a div normalization_factor b) * b"
1.39 +      by (simp add: ac_simps div_mult_swap unit_eq_div1)
1.40 +    ultimately show "associated a b" by (rule is_unit_associatedI)
1.41 +  next
1.42 +    assume ?P
1.43 +    then obtain c where "is_unit c" and "a = c * b"
1.44 +      by (blast elim: associated_is_unitE)
1.45 +    then show ?Q
1.46 +      by (auto simp add: normalization_factor_mult normalization_factor_unit)
1.47    qed
1.48 +qed
1.49
1.50  lemma normed_associated_imp_eq:
1.51    "associated a b \<Longrightarrow> normalization_factor a \<in> {0, 1} \<Longrightarrow> normalization_factor b \<in> {0, 1} \<Longrightarrow> a = b"
```