src/HOL/Computational_Algebra/Normalized_Fraction.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65435 378175f44328
child 66886 960509bfd47e
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Computational_Algebra/Normalized_Fraction.thy
     2     Author:     Manuel Eberl
     3 *)
     4 
     5 theory Normalized_Fraction
     6 imports 
     7   Main 
     8   Euclidean_Algorithm
     9   Fraction_Field
    10 begin
    11 
    12 definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
    13   "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
    14 
    15 definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \<times> 'a \<Rightarrow> 'a \<times> 'a" where
    16   "normalize_quot = 
    17      (\<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))" 
    18 
    19 definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
    20   "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
    21   
    22 lemma not_normalized_fracts_0_denom [simp]: "(a, 0) \<notin> normalized_fracts"
    23   by (auto simp: normalized_fracts_def)
    24 
    25 lemma unit_factor_snd_normalize_quot [simp]:
    26   "unit_factor (snd (normalize_quot x)) = 1"
    27   by (simp add: normalize_quot_def case_prod_unfold Let_def dvd_unit_factor_div
    28                 mult_unit_dvd_iff unit_factor_mult unit_factor_gcd)
    29   
    30 lemma snd_normalize_quot_nonzero [simp]: "snd (normalize_quot x) \<noteq> 0"
    31   using unit_factor_snd_normalize_quot[of x] 
    32   by (auto simp del: unit_factor_snd_normalize_quot)
    33   
    34 lemma normalize_quot_aux:
    35   fixes a b
    36   assumes "b \<noteq> 0"
    37   defines "d \<equiv> gcd a b * unit_factor b"
    38   shows   "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d"
    39           "d dvd a" "d dvd b" "d \<noteq> 0"
    40 proof -
    41   from assms show "d dvd a" "d dvd b"
    42     by (simp_all add: d_def mult_unit_dvd_iff)
    43   thus "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d" "d \<noteq> 0"
    44     by (auto simp: normalize_quot_def Let_def d_def \<open>b \<noteq> 0\<close>)
    45 qed
    46 
    47 lemma normalize_quotE:
    48   assumes "b \<noteq> 0"
    49   obtains d where "a = fst (normalize_quot (a,b)) * d" "b = snd (normalize_quot (a,b)) * d"
    50                   "d dvd a" "d dvd b" "d \<noteq> 0"
    51   using that[OF normalize_quot_aux[OF assms]] .
    52   
    53 lemma normalize_quotE':
    54   assumes "snd x \<noteq> 0"
    55   obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d"
    56                   "d dvd fst x" "d dvd snd x" "d \<noteq> 0"
    57 proof -
    58   from normalize_quotE[OF assms, of "fst x"] guess d .
    59   from this show ?thesis unfolding prod.collapse by (intro that[of d])
    60 qed
    61   
    62 lemma coprime_normalize_quot:
    63   "coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
    64   by (simp add: normalize_quot_def case_prod_unfold Let_def
    65         div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
    66 
    67 lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
    68   by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
    69 
    70 lemma normalize_quot_eq_iff:
    71   assumes "b \<noteq> 0" "d \<noteq> 0"
    72   shows   "normalize_quot (a,b) = normalize_quot (c,d) \<longleftrightarrow> a * d = b * c"
    73 proof -
    74   define x y where "x = normalize_quot (a,b)" and "y = normalize_quot (c,d)" 
    75   from normalize_quotE[OF assms(1), of a] normalize_quotE[OF assms(2), of c]
    76     obtain d1 d2 
    77       where "a = fst x * d1" "b = snd x * d1" "c = fst y * d2" "d = snd y * d2" "d1 \<noteq> 0" "d2 \<noteq> 0"
    78     unfolding x_def y_def by metis
    79   hence "a * d = b * c \<longleftrightarrow> fst x * snd y = snd x * fst y" by simp
    80   also have "\<dots> \<longleftrightarrow> fst x = fst y \<and> snd x = snd y"
    81     by (intro coprime_crossproduct') (simp_all add: x_def y_def coprime_normalize_quot)
    82   also have "\<dots> \<longleftrightarrow> x = y" using prod_eqI by blast
    83   finally show "x = y \<longleftrightarrow> a * d = b * c" ..
    84 qed
    85 
    86 lemma normalize_quot_eq_iff':
    87   assumes "snd x \<noteq> 0" "snd y \<noteq> 0"
    88   shows   "normalize_quot x = normalize_quot y \<longleftrightarrow> fst x * snd y = snd x * fst y"
    89   using assms by (cases x, cases y, hypsubst) (subst normalize_quot_eq_iff, simp_all)
    90 
    91 lemma normalize_quot_id: "x \<in> normalized_fracts \<Longrightarrow> normalize_quot x = x"
    92   by (auto simp: normalized_fracts_def normalize_quot_def case_prod_unfold)
    93 
    94 lemma normalize_quot_idem [simp]: "normalize_quot (normalize_quot x) = normalize_quot x"
    95   by (rule normalize_quot_id) simp_all
    96 
    97 lemma fractrel_iff_normalize_quot_eq:
    98   "fractrel x y \<longleftrightarrow> normalize_quot x = normalize_quot y \<and> snd x \<noteq> 0 \<and> snd y \<noteq> 0"
    99   by (cases x, cases y) (auto simp: fractrel_def normalize_quot_eq_iff)
   100   
   101 lemma fractrel_normalize_quot_left:
   102   assumes "snd x \<noteq> 0"
   103   shows   "fractrel (normalize_quot x) y \<longleftrightarrow> fractrel x y"
   104   using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto
   105 
   106 lemma fractrel_normalize_quot_right:
   107   assumes "snd x \<noteq> 0"
   108   shows   "fractrel y (normalize_quot x) \<longleftrightarrow> fractrel y x"
   109   using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto
   110 
   111   
   112 lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \<Rightarrow> 'a \<times> 'a" 
   113     is normalize_quot
   114   by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all
   115   
   116 lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x"
   117   unfolding quot_to_fract_def
   118 proof transfer
   119   fix x :: "'a \<times> 'a" assume rel: "fractrel x x"
   120   define x' where "x' = normalize_quot x"
   121   obtain a b where [simp]: "x = (a, b)" by (cases x)
   122   from rel have "b \<noteq> 0" by simp
   123   from normalize_quotE[OF this, of a] guess d .
   124   hence "a = fst x' * d" "b = snd x' * d" "d \<noteq> 0" "snd x' \<noteq> 0" by (simp_all add: x'_def)
   125   thus "fractrel (case x' of (a, b) \<Rightarrow> if b = 0 then (0, 1) else (a, b)) x"
   126     by (auto simp add: case_prod_unfold)
   127 qed
   128 
   129 lemma quot_of_fract_quot_to_fract: "quot_of_fract (quot_to_fract x) = normalize_quot x"
   130 proof (cases "snd x = 0")
   131   case True
   132   thus ?thesis unfolding quot_to_fract_def
   133     by transfer (simp add: case_prod_unfold normalize_quot_def)
   134 next
   135   case False
   136   thus ?thesis unfolding quot_to_fract_def by transfer (simp add: case_prod_unfold)
   137 qed
   138 
   139 lemma quot_of_fract_quot_to_fract': 
   140   "x \<in> normalized_fracts \<Longrightarrow> quot_of_fract (quot_to_fract x) = x"
   141   unfolding quot_to_fract_def by transfer (auto simp: normalize_quot_id)
   142 
   143 lemma quot_of_fract_in_normalized_fracts [simp]: "quot_of_fract x \<in> normalized_fracts"
   144   by transfer simp
   145 
   146 lemma normalize_quotI:
   147   assumes "a * d = b * c" "b \<noteq> 0" "(c, d) \<in> normalized_fracts"
   148   shows   "normalize_quot (a, b) = (c, d)"
   149 proof -
   150   from assms have "normalize_quot (a, b) = normalize_quot (c, d)"
   151     by (subst normalize_quot_eq_iff) auto
   152   also have "\<dots> = (c, d)" by (intro normalize_quot_id) fact
   153   finally show ?thesis .
   154 qed
   155 
   156 lemma td_normalized_fract:
   157   "type_definition quot_of_fract quot_to_fract normalized_fracts"
   158   by standard (simp_all add: quot_of_fract_quot_to_fract')
   159 
   160 lemma quot_of_fract_add_aux:
   161   assumes "snd x \<noteq> 0" "snd y \<noteq> 0" 
   162   shows   "(fst x * snd y + fst y * snd x) * (snd (normalize_quot x) * snd (normalize_quot y)) =
   163              snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) +
   164              snd (normalize_quot x) * fst (normalize_quot y))"
   165 proof -
   166   from normalize_quotE'[OF assms(1)] guess d . note d = this
   167   from normalize_quotE'[OF assms(2)] guess e . note e = this
   168   show ?thesis by (simp_all add: d e algebra_simps)
   169 qed
   170 
   171 
   172 locale fract_as_normalized_quot
   173 begin
   174 setup_lifting td_normalized_fract
   175 end
   176 
   177 
   178 lemma quot_of_fract_add:
   179   "quot_of_fract (x + y) = 
   180      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y
   181       in  normalize_quot (a * d + b * c, b * d))"
   182   by transfer (insert quot_of_fract_add_aux, 
   183                simp_all add: Let_def case_prod_unfold normalize_quot_eq_iff)
   184 
   185 lemma quot_of_fract_uminus:
   186   "quot_of_fract (-x) = (let (a,b) = quot_of_fract x in (-a, b))"
   187   by transfer (auto simp: case_prod_unfold Let_def normalize_quot_def dvd_neg_div mult_unit_dvd_iff)
   188 
   189 lemma quot_of_fract_diff:
   190   "quot_of_fract (x - y) = 
   191      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y
   192       in  normalize_quot (a * d - b * c, b * d))" (is "_ = ?rhs")
   193 proof -
   194   have "x - y = x + -y" by simp
   195   also have "quot_of_fract \<dots> = ?rhs"
   196     by (simp only: quot_of_fract_add quot_of_fract_uminus Let_def case_prod_unfold) simp_all
   197   finally show ?thesis .
   198 qed
   199 
   200 lemma normalize_quot_mult_coprime:
   201   assumes "coprime a b" "coprime c d" "unit_factor b = 1" "unit_factor d = 1"
   202   defines "e \<equiv> fst (normalize_quot (a, d))" and "f \<equiv> snd (normalize_quot (a, d))"
   203      and  "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
   204   shows   "normalize_quot (a * c, b * d) = (e * g, f * h)"
   205 proof (rule normalize_quotI)
   206   from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
   207   from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
   208   from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
   209   from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
   210   from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
   211     by simp_all
   212   from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
   213   with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
   214     by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
   215 qed (insert assms(3,4), auto)
   216 
   217 lemma normalize_quot_mult:
   218   assumes "snd x \<noteq> 0" "snd y \<noteq> 0"
   219   shows   "normalize_quot (fst x * fst y, snd x * snd y) = normalize_quot 
   220              (fst (normalize_quot x) * fst (normalize_quot y),
   221               snd (normalize_quot x) * snd (normalize_quot y))"
   222 proof -
   223   from normalize_quotE'[OF assms(1)] guess d . note d = this
   224   from normalize_quotE'[OF assms(2)] guess e . note e = this
   225   show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff)
   226 qed
   227 
   228 lemma quot_of_fract_mult:
   229   "quot_of_fract (x * y) = 
   230      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
   231           (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
   232       in  (e*g, f*h))"
   233   by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
   234                  coprime_normalize_quot normalize_quot_mult [symmetric])
   235   
   236 lemma normalize_quot_0 [simp]: 
   237     "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
   238   by (simp_all add: normalize_quot_def)
   239   
   240 lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0"
   241   by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff)
   242   find_theorems "_ div _ = 0"
   243   
   244 lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1"
   245   by transfer auto
   246 
   247 lemma normalize_quot_swap:
   248   assumes "a \<noteq> 0" "b \<noteq> 0"
   249   defines "a' \<equiv> fst (normalize_quot (a, b))" and "b' \<equiv> snd (normalize_quot (a, b))"
   250   shows   "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')"
   251 proof (rule normalize_quotI)
   252   from normalize_quotE[OF assms(2), of a] guess d . note d = this [folded assms(3,4)]
   253   show "b * (a' div unit_factor a') = a * (b' div unit_factor a')"
   254     using assms(1,2) d 
   255     by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
   256   have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
   257   thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
   258     using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
   259 qed fact+
   260   
   261 lemma quot_of_fract_inverse:
   262   "quot_of_fract (inverse x) = 
   263      (let (a,b) = quot_of_fract x; d = unit_factor a 
   264       in  if d = 0 then (0, 1) else (b div d, a div d))"
   265 proof (transfer, goal_cases)
   266   case (1 x)
   267   from normalize_quot_swap[of "fst x" "snd x"] show ?case
   268     by (auto simp: Let_def case_prod_unfold)
   269 qed
   270 
   271 lemma normalize_quot_div_unit_left:
   272   fixes x y u
   273   assumes "is_unit u"
   274   defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))"
   275   shows "normalize_quot (x div u, y) = (x' div u, y')"
   276 proof (cases "y = 0")
   277   case False
   278   from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
   279   from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
   280   with False d \<open>is_unit u\<close> show ?thesis
   281     by (intro normalize_quotI)
   282        (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
   283           gcd_div_unit1)
   284 qed (simp_all add: assms)
   285 
   286 lemma normalize_quot_div_unit_right:
   287   fixes x y u
   288   assumes "is_unit u"
   289   defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))"
   290   shows "normalize_quot (x, y div u) = (x' * u, y')"
   291 proof (cases "y = 0")
   292   case False
   293   from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
   294   from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
   295   with False d \<open>is_unit u\<close> show ?thesis
   296     by (intro normalize_quotI)
   297        (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
   298           gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
   299 qed (simp_all add: assms)
   300 
   301 lemma normalize_quot_normalize_left:
   302   fixes x y u
   303   defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))"
   304   shows "normalize_quot (normalize x, y) = (x' div unit_factor x, y')"
   305   using normalize_quot_div_unit_left[of "unit_factor x" x y]
   306   by (cases "x = 0") (simp_all add: assms)
   307   
   308 lemma normalize_quot_normalize_right:
   309   fixes x y u
   310   defines "x' \<equiv> fst (normalize_quot (x, y))" and "y' \<equiv> snd (normalize_quot (x, y))"
   311   shows "normalize_quot (x, normalize y) = (x' * unit_factor y, y')"
   312   using normalize_quot_div_unit_right[of "unit_factor y" x y]
   313   by (cases "y = 0") (simp_all add: assms)
   314   
   315 lemma quot_of_fract_0 [simp]: "quot_of_fract 0 = (0, 1)"
   316   by transfer auto
   317 
   318 lemma quot_of_fract_1 [simp]: "quot_of_fract 1 = (1, 1)"
   319   by transfer (rule normalize_quotI, simp_all add: normalized_fracts_def)
   320 
   321 lemma quot_of_fract_divide:
   322   "quot_of_fract (x / y) = (if y = 0 then (0, 1) else
   323      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
   324           (e,f) = normalize_quot (a,c); (g,h) = normalize_quot (d,b)
   325       in  (e * g, f * h)))" (is "_ = ?rhs")
   326 proof (cases "y = 0")
   327   case False
   328   hence A: "fst (quot_of_fract y) \<noteq> 0" by transfer auto
   329   have "x / y = x * inverse y" by (simp add: divide_inverse)
   330   also from False A have "quot_of_fract \<dots> = ?rhs"
   331     by (simp only: quot_of_fract_mult quot_of_fract_inverse)
   332        (simp_all add: Let_def case_prod_unfold fst_quot_of_fract_0_imp
   333           normalize_quot_div_unit_left normalize_quot_div_unit_right 
   334           normalize_quot_normalize_right normalize_quot_normalize_left)
   335   finally show ?thesis .
   336 qed simp_all
   337 
   338 end