tuned floor lemmas
authornipkow
Fri Aug 05 09:30:20 2016 +0200 (2016-08-05)
changeset 63597bef0277ec73b
parent 63596 24d329f666c5
child 63598 025d6e52d86f
tuned floor lemmas
src/HOL/Archimedean_Field.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Fri Aug 05 09:05:03 2016 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Aug 05 09:30:20 2016 +0200
     1.3 @@ -642,6 +642,9 @@
     1.4      by (auto simp add: frac_def algebra_simps)
     1.5  qed
     1.6  
     1.7 +lemma floor_add2[simp]: "frac x = 0 \<or> frac y = 0 \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
     1.8 +by (metis add.commute add.left_neutral frac_lt_1 floor_add)
     1.9 +
    1.10  lemma frac_add:
    1.11    "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"
    1.12    by (simp add: frac_def floor_add)
     2.1 --- a/src/HOL/Real.thy	Fri Aug 05 09:05:03 2016 +0200
     2.2 +++ b/src/HOL/Real.thy	Fri Aug 05 09:30:20 2016 +0200
     2.3 @@ -1503,9 +1503,6 @@
     2.4  lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
     2.5    by (simp add: floor_unique_iff)
     2.6  
     2.7 -lemma floor_add2[simp]: "\<lfloor>of_int a + x\<rfloor> = a + \<lfloor>x\<rfloor>"
     2.8 -  by (simp add: add.commute)
     2.9 -
    2.10  lemma floor_divide_real_eq_div:
    2.11    assumes "0 \<le> b"
    2.12    shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
    2.13 @@ -1526,27 +1523,25 @@
    2.14      proof -
    2.15        have "real_of_int (j * b) < real_of_int i + 1"
    2.16          using \<open>a < 1 + real_of_int i\<close> \<open>real_of_int j * real_of_int b \<le> a\<close> by force
    2.17 -      then show "j * b < 1 + i"
    2.18 -        by linarith
    2.19 +      then show "j * b < 1 + i" by linarith
    2.20      qed
    2.21      ultimately have "(j - i div b) * b \<le> i mod b" "i mod b < ((j - i div b) + 1) * b"
    2.22        by (auto simp: field_simps)
    2.23      then have "(j - i div b) * b < 1 * b" "0 * b < ((j - i div b) + 1) * b"
    2.24        using pos_mod_bound [OF b, of i] pos_mod_sign [OF b, of i]
    2.25        by linarith+
    2.26 -    then show ?thesis
    2.27 -      using b unfolding mult_less_cancel_right by auto
    2.28 +    then show ?thesis using b unfolding mult_less_cancel_right by auto
    2.29    qed
    2.30 -  with b show ?thesis
    2.31 -    by (auto split: floor_split simp: field_simps)
    2.32 +  with b show ?thesis by (auto split: floor_split simp: field_simps)
    2.33  qed
    2.34  
    2.35 -lemma floor_divide_eq_div_numeral [simp]: "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    2.36 -  by (metis floor_divide_of_int_eq of_int_numeral)
    2.37 +lemma floor_divide_eq_div_numeral [simp]:
    2.38 +  "\<lfloor>numeral a / numeral b::real\<rfloor> = numeral a div numeral b"
    2.39 +by (metis floor_divide_of_int_eq of_int_numeral)
    2.40  
    2.41  lemma floor_minus_divide_eq_div_numeral [simp]:
    2.42    "\<lfloor>- (numeral a / numeral b)::real\<rfloor> = - numeral a div numeral b"
    2.43 -  by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
    2.44 +by (metis divide_minus_left floor_divide_of_int_eq of_int_neg_numeral of_int_numeral)
    2.45  
    2.46  lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
    2.47    using ceiling_of_int by metis