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: