tuned proof
authorhaftmann
Sat Jun 27 20:20:36 2015 +0200 (2015-06-27)
changeset 60599f8bb070dc98b
parent 60598 78ca5674c66a
child 60600 87fbfea0bd0a
tuned proof
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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"