equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where |
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)" |
13 "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)" |
14 |
14 |
15 definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \<times> 'a \<Rightarrow> 'a \<times> 'a" where |
15 definition normalize_quot :: "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} \<times> 'a \<Rightarrow> 'a \<times> 'a" where |
16 "normalize_quot = |
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))" |
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 |
18 |
19 lemma normalize_quot_zero [simp]: |
19 lemma normalize_quot_zero [simp]: |
20 "normalize_quot (a, 0) = (0, 1)" |
20 "normalize_quot (a, 0) = (0, 1)" |
116 assumes "snd x \<noteq> 0" |
116 assumes "snd x \<noteq> 0" |
117 shows "fractrel y (normalize_quot x) \<longleftrightarrow> fractrel y x" |
117 shows "fractrel y (normalize_quot x) \<longleftrightarrow> fractrel y x" |
118 using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
118 using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto |
119 |
119 |
120 |
120 |
121 lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \<Rightarrow> 'a \<times> 'a" |
121 lift_definition quot_of_fract :: |
|
122 "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract \<Rightarrow> 'a \<times> 'a" |
122 is normalize_quot |
123 is normalize_quot |
123 by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all |
124 by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all |
124 |
125 |
125 lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x" |
126 lemma quot_to_fract_quot_of_fract [simp]: "quot_to_fract (quot_of_fract x) = x" |
126 unfolding quot_to_fract_def |
127 unfolding quot_to_fract_def |