121 lemma One_rat_def: "1 = Fract 1 1" |
121 lemma One_rat_def: "1 = Fract 1 1" |
122 by transfer simp |
122 by transfer simp |
123 |
123 |
124 lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" |
124 lift_definition plus_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" |
125 is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)" |
125 is "\<lambda>x y. (fst x * snd y + fst y * snd x, snd x * snd y)" |
126 by (clarsimp, simp add: left_distrib, simp add: mult_ac) |
126 by (clarsimp, simp add: distrib_right, simp add: mult_ac) |
127 |
127 |
128 lemma add_rat [simp]: |
128 lemma add_rat [simp]: |
129 assumes "b \<noteq> 0" and "d \<noteq> 0" |
129 assumes "b \<noteq> 0" and "d \<noteq> 0" |
130 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
130 shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" |
131 using assms by transfer simp |
131 using assms by transfer simp |
614 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) |
614 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) |
615 #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] |
615 #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] |
616 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) |
616 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) |
617 #> Lin_Arith.add_simps [@{thm neg_less_iff_less}, |
617 #> Lin_Arith.add_simps [@{thm neg_less_iff_less}, |
618 @{thm True_implies_equals}, |
618 @{thm True_implies_equals}, |
619 read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm right_distrib}, |
619 read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left}, |
620 read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm right_distrib}, |
620 read_instantiate @{context} [(("a", 0), "(neg_numeral ?v)")] @{thm distrib_left}, |
621 @{thm divide_1}, @{thm divide_zero_left}, |
621 @{thm divide_1}, @{thm divide_zero_left}, |
622 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
622 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
623 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
623 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
624 @{thm of_int_minus}, @{thm of_int_diff}, |
624 @{thm of_int_minus}, @{thm of_int_diff}, |
625 @{thm of_int_of_nat_eq}] |
625 @{thm of_int_of_nat_eq}] |