2033 lemma [code_abbrev]: |
2033 lemma [code_abbrev]: |
2034 "(of_rat 1 :: real) = 1" |
2034 "(of_rat 1 :: real) = 1" |
2035 by simp |
2035 by simp |
2036 |
2036 |
2037 lemma [code_abbrev]: |
2037 lemma [code_abbrev]: |
|
2038 "(of_rat (- 1) :: real) = - 1" |
|
2039 by simp |
|
2040 |
|
2041 lemma [code_abbrev]: |
2038 "(of_rat (numeral k) :: real) = numeral k" |
2042 "(of_rat (numeral k) :: real) = numeral k" |
2039 by simp |
2043 by simp |
2040 |
2044 |
2041 lemma [code_abbrev]: |
2045 lemma [code_abbrev]: |
2042 "(of_rat (- numeral k) :: real) = - numeral k" |
2046 "(of_rat (- numeral k) :: real) = - numeral k" |
2043 by simp |
2047 by simp |
2044 |
2048 |
2045 lemma [code_post]: |
2049 lemma [code_post]: |
2046 "(of_rat (0 / r) :: real) = 0" |
|
2047 "(of_rat (r / 0) :: real) = 0" |
|
2048 "(of_rat (1 / 1) :: real) = 1" |
|
2049 "(of_rat (numeral k / 1) :: real) = numeral k" |
|
2050 "(of_rat (- numeral k / 1) :: real) = - numeral k" |
|
2051 "(of_rat (1 / numeral k) :: real) = 1 / numeral k" |
2050 "(of_rat (1 / numeral k) :: real) = 1 / numeral k" |
2052 "(of_rat (1 / - numeral k) :: real) = 1 / - numeral k" |
2051 "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l" |
2053 "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l" |
2052 "(of_rat (- (1 / numeral k)) :: real) = - (1 / numeral k)" |
2054 "(of_rat (numeral k / - numeral l) :: real) = numeral k / - numeral l" |
2053 "(of_rat (- (numeral k / numeral l)) :: real) = - (numeral k / numeral l)" |
2055 "(of_rat (- numeral k / numeral l) :: real) = - numeral k / numeral l" |
|
2056 "(of_rat (- numeral k / - numeral l) :: real) = - numeral k / - numeral l" |
|
2057 by (simp_all add: of_rat_divide of_rat_minus) |
2054 by (simp_all add: of_rat_divide of_rat_minus) |
2058 |
2055 |
2059 |
2056 |
2060 text {* Operations *} |
2057 text {* Operations *} |
2061 |
2058 |