src/HOL/Archimedean_Field.thy
 changeset 47592 a6b76247534d parent 47307 5e5ca36692b3 child 54281 b01057e72233
equal inserted replaced
47583:f3f0e06549c2 47592:a6b76247534d
`   444   using ceiling_diff_of_int [of x "neg_numeral v"] by simp`
`   444   using ceiling_diff_of_int [of x "neg_numeral v"] by simp`
`   445 `
`   445 `
`   446 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"`
`   446 lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"`
`   447   using ceiling_diff_of_int [of x 1] by simp`
`   447   using ceiling_diff_of_int [of x 1] by simp`
`   448 `
`   448 `
`       `
`   449 lemma ceiling_diff_floor_le_1: "ceiling x - floor x \<le> 1"`
`       `
`   450 proof -`
`       `
`   451   have "of_int \<lceil>x\<rceil> - 1 < x" `
`       `
`   452     using ceiling_correct[of x] by simp`
`       `
`   453   also have "x < of_int \<lfloor>x\<rfloor> + 1"`
`       `
`   454     using floor_correct[of x] by simp_all`
`       `
`   455   finally have "of_int (\<lceil>x\<rceil> - \<lfloor>x\<rfloor>) < (of_int 2::'a)"`
`       `
`   456     by simp`
`       `
`   457   then show ?thesis`
`       `
`   458     unfolding of_int_less_iff by simp`
`       `
`   459 qed`
`   449 `
`   460 `
`   450 subsection {* Negation *}`
`   461 subsection {* Negation *}`
`   451 `
`   462 `
`   452 lemma floor_minus: "floor (- x) = - ceiling x"`
`   463 lemma floor_minus: "floor (- x) = - ceiling x"`
`   453   unfolding ceiling_def by simp`
`   464   unfolding ceiling_def by simp`