# HG changeset patch # User huffman # Date 1181661630 -7200 # Node ID 6a83ca5fe2824d2fe44205f9e6f1fc00898aec47 # Parent 0261d2da0b1cb422dca27cb0caaa378a7ff69179 more of_rat lemmas diff -r 0261d2da0b1c -r 6a83ca5fe282 src/HOL/Real/Rational.thy --- a/src/HOL/Real/Rational.thy Tue Jun 12 17:04:26 2007 +0200 +++ b/src/HOL/Real/Rational.thy Tue Jun 12 17:20:30 2007 +0200 @@ -508,24 +508,21 @@ lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" by (induct a, induct b, simp add: add_rat of_rat_rat add_frac_eq) +lemma of_rat_minus: "of_rat (- a) = - of_rat a" +by (induct a, simp add: minus_rat of_rat_rat) + +lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" +by (simp only: diff_minus of_rat_add of_rat_minus) + lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" apply (induct a, induct b, simp add: mult_rat of_rat_rat) apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) done -lemma nonzero_inverse_divide: - fixes a b :: "'a::field" - shows "\a \ 0; b \ 0\ \ inverse (a / b) = b / a" -apply (simp add: divide_inverse) -apply (simp add: nonzero_inverse_mult_distrib nonzero_imp_inverse_nonzero) -apply (simp add: nonzero_inverse_inverse_eq) -done - lemma nonzero_of_rat_inverse: "a \ 0 \ of_rat (inverse a) = inverse (of_rat a)" -apply (induct a) -apply (simp add: Zero_rat_def inverse_rat eq_rat of_rat_rat) -apply (simp add: nonzero_inverse_divide) +apply (rule inverse_unique [symmetric]) +apply (simp add: of_rat_mult [symmetric]) done lemma of_rat_inverse: @@ -542,4 +539,36 @@ = of_rat a / of_rat b" by (cases "b = 0", simp_all add: nonzero_of_rat_divide) +lemma of_rat_power: + "(of_rat (a ^ n)::'a::{field_char_0,recpower}) = of_rat a ^ n" +by (induct n) (simp_all add: of_rat_mult power_Suc) + +lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" +apply (induct a, induct b) +apply (simp add: of_rat_rat eq_rat) +apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) +apply (simp only: of_int_mult [symmetric] of_int_eq_iff) +done + +lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] + +lemma of_rat_eq_id [simp]: "of_rat = (id :: rat \ rat)" +proof + fix a + show "of_rat a = id a" + by (induct a) + (simp add: of_rat_rat divide_rat Fract_of_int_eq [symmetric]) +qed + +text{*Collapse nested embeddings*} +lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" +by (induct n) (simp_all add: of_rat_add) + +lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" +by (cases z rule: int_diff_cases', simp add: of_rat_diff) + +lemma of_rat_number_of_eq [simp]: + "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})" +by (simp add: number_of_eq) + end