src/HOL/Real.thy
changeset 63597 bef0277ec73b
parent 63494 ac0a3b9c6dae
child 63601 ae810a755cd2
     1.1 --- a/src/HOL/Real.thy	Fri Aug 05 09:05:03 2016 +0200
     1.2 +++ b/src/HOL/Real.thy	Fri Aug 05 09:30:20 2016 +0200
     1.3 @@ -1503,9 +1503,6 @@
     1.4  lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
     1.5    by (simp add: floor_unique_iff)
     1.6  
     1.7 -lemma floor_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
     1.8 -  by (simp add: add.commute)
     1.9 -
    1.10  lemma floor_divide_real_eq_div:
    1.11    assumes "0 \<le> b"
    1.12    shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
    1.13 @@ -1526,27 +1523,25 @@
    1.14      proof -
    1.15        have "real_of_int (j * b) < real_of_int i + 1"
    1.16          using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
    1.17 -      then show "j * b < 1 + i"
    1.18 -        by linarith
    1.19 +      then show "j * b < 1 + i" by linarith
    1.20      qed
    1.21      ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
    1.22        by (auto simp: field_simps)
    1.23      then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
    1.24        using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i]
    1.25        by linarith+
    1.26 -    then show ?thesis
    1.27 -      using b unfolding mult_less_cancel_right by auto
    1.28 +    then show ?thesis using b unfolding mult_less_cancel_right by auto
    1.29    qed
    1.30 -  with b show ?thesis
    1.31 -    by (auto split: floor_split simp: field_simps)
    1.32 +  with b show ?thesis by (auto split: floor_split simp: field_simps)
    1.33  qed
    1.34  
    1.35 -lemma floor_divide_eq_div_numeral [simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    1.36 -  by (metis floor_divide_of_int_eq of_int_numeral)
    1.37 +lemma floor_divide_eq_div_numeral [simp]:
    1.38 +  "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    1.39 +by (metis floor_divide_of_int_eq of_int_numeral)
    1.40  
    1.41  lemma floor_minus_divide_eq_div_numeral [simp]:
    1.42    "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
    1.43 -  by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
    1.44 +by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
    1.45  
    1.46  lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
    1.47    using ceiling_of_int by metis