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
```