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