src/HOL/Computational_Algebra/Normalized_Fraction.thy
 changeset 67051 e7e54a0b9197 parent 66886 960509bfd47e child 67078 6a85b8a9c28c
```     1.1 --- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -16,6 +16,15 @@
1.4    "normalize_quot =
1.5       (\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))"
1.6
1.7 +lemma normalize_quot_zero [simp]:
1.8 +  "normalize_quot (a, 0) = (0, 1)"
1.9 +  by (simp add: normalize_quot_def)
1.10 +
1.11 +lemma normalize_quot_proj [simp]:
1.12 +  "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
1.13 +  "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
1.14 +  using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
1.15 +
1.16  definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
1.17    "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
1.18
1.19 @@ -61,8 +70,8 @@
1.20
1.21  lemma coprime_normalize_quot:
1.22    "coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
1.23 -  by (simp add: normalize_quot_def case_prod_unfold Let_def
1.24 -        div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
1.25 +  by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2)
1.26 +    (metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit)
1.27
1.28  lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
1.29    by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
1.30 @@ -203,15 +212,26 @@
1.31       and  "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
1.32    shows   "normalize_quot (a * c, b * d) = (e * g, f * h)"
1.33  proof (rule normalize_quotI)
1.34 +  from assms have "gcd a b = 1" "gcd c d = 1"
1.35 +    by simp_all
1.36    from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
1.37 -  from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
1.38 -  from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
1.39 -  from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
1.40 +  with assms have "normalize b = b" "normalize d = d"
1.41 +    by (auto intro: normalize_unit_factor_eqI)
1.42 +  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
1.43 +  note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
1.44 +  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
1.45 +  note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
1.46 +  from k l show "a * c * (f * h) = b * d * (e * g)"
1.47 +    by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
1.48    from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
1.49      by simp_all
1.50    from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
1.51 -  with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
1.52 -    by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
1.53 +  with k l assms(1,2) \<open>b \<noteq> 0\<close> \<open>d \<noteq> 0\<close> \<open>unit_factor b = 1\<close> \<open>unit_factor d = 1\<close>
1.54 +    \<open>normalize b = b\<close> \<open>normalize d = d\<close>
1.55 +  show "(e * g, f * h) \<in> normalized_fracts"
1.56 +    by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def
1.57 +      coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd)
1.58 +      (metis coprime_mult_left_iff coprime_mult_right_iff)
1.59  qed (insert assms(3,4), auto)
1.60
1.61  lemma normalize_quot_mult:
1.62 @@ -230,8 +250,8 @@
1.63       (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
1.64            (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
1.65        in  (e*g, f*h))"
1.66 -  by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
1.67 -                 coprime_normalize_quot normalize_quot_mult [symmetric])
1.68 +  by transfer
1.69 +     (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)
1.70
1.71  lemma normalize_quot_0 [simp]:
1.72      "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
1.73 @@ -254,7 +274,9 @@
1.74      by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
1.75    have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
1.76    thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
1.77 -    using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
1.78 +    using assms(1,2) d
1.79 +    by (auto simp: normalized_fracts_def ac_simps)
1.80 +      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
1.81  qed fact+
1.82
1.83  lemma quot_of_fract_inverse:
1.84 @@ -274,12 +296,19 @@
1.85    shows "normalize_quot (x div u, y) = (x' div u, y')"
1.86  proof (cases "y = 0")
1.87    case False
1.88 -  from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
1.89 -  from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
1.90 -  with False d \<open>is_unit u\<close> show ?thesis
1.91 -    by (intro normalize_quotI)
1.92 -       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
1.93 -          gcd_div_unit1)
1.94 +  define v where "v = 1 div u"
1.95 +  with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v"
1.96 +    by simp_all
1.97 +  from \<open>is_unit v\<close> have "coprime v = top"
1.98 +    by (simp add: fun_eq_iff is_unit_left_imp_coprime)
1.99 +  from normalize_quotE[OF False, of x] guess d .
1.100 +  note d = this[folded assms(2,3)]
1.101 +  from assms have "coprime x' y'" "unit_factor y' = 1"
1.102 +    by (simp_all add: coprime_normalize_quot)
1.103 +  with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')"
1.104 +    by (auto simp: normalized_fracts_def intro: normalize_quotI)
1.105 +  then show ?thesis
1.106 +    by (simp add: u)
1.107  qed (simp_all add: assms)
1.108
1.109  lemma normalize_quot_div_unit_right:
1.110 @@ -291,10 +320,8 @@
1.111    case False
1.112    from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
1.113    from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
1.114 -  with False d \<open>is_unit u\<close> show ?thesis
1.115 -    by (intro normalize_quotI)
1.116 -       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
1.117 -          gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
1.118 +  with d \<open>is_unit u\<close> show ?thesis
1.119 +    by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
1.120  qed (simp_all add: assms)
1.121
1.122  lemma normalize_quot_normalize_left:
```