added missing lemmas
authornipkow
Fri Aug 05 16:22:13 2016 +0200 (2016-08-05)
changeset 63601ae810a755cd2
parent 63600 d0fa16751d14
child 63602 7725bba95ada
added missing lemmas
src/HOL/Real.thy
     1.1 --- a/src/HOL/Real.thy	Fri Aug 05 15:44:53 2016 +0200
     1.2 +++ b/src/HOL/Real.thy	Fri Aug 05 16:22:13 2016 +0200
     1.3 @@ -1535,6 +1535,15 @@
     1.4    with b show ?thesis by (auto split: floor_split simp: field_simps)
     1.5  qed
     1.6  
     1.7 +lemma floor_one_divide_eq_div_numeral [simp]:
     1.8 +  "\<lfloor>1 / numeral b::real\<rfloor> = 1 div numeral b"
     1.9 +by (metis floor_divide_of_int_eq of_int_1 of_int_numeral)
    1.10 +
    1.11 +lemma floor_minus_one_divide_eq_div_numeral [simp]:
    1.12 +  "\<lfloor>- (1 / numeral b)::real\<rfloor> = - 1 div numeral b"
    1.13 +by (metis (mono_tags, hide_lams) div_minus_right minus_divide_right
    1.14 +    floor_divide_of_int_eq of_int_neg_numeral of_int_1)
    1.15 +
    1.16  lemma floor_divide_eq_div_numeral [simp]:
    1.17    "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    1.18  by (metis floor_divide_of_int_eq of_int_numeral)