[isabelle-dev] Fwd: [isabelle] natfloor_div_nat not general enough

Lawrence Paulson lp15 at cam.ac.uk
Sun Oct 26 18:25:11 CET 2014

```FYI: the lemma is used only once, in Real.thy, and not at all in the AFP.

Still worth fixing though. Any volunteers?

Larry

> Begin forwarded message:
>
> From: Joachim Breitner <breitner at kit.edu>
> To: isabelle-users at cl.cam.ac.uk
> Date: 26 October 2014 14:15:40 GMT
> Subject: [isabelle] natfloor_div_nat not general enough
>
> Hi,
>
> Real.thy contains the lemma
>
> lemma natfloor_div_nat:
>  assumes "1 <= x" and "y > 0"
>  shows "natfloor (x / real y) = natfloor x div y"
>
> but the first assumption is redundant:
>
>
> lemma natfloor_div_nat:
>  assumes "y > 0"
>  shows "natfloor (x / real y) = natfloor x div y"
> proof-
>  have "x ≤ 0 ∨ x ≥ 0 ∧ x < 1 ∨ 1 ≤ x" by arith
>  thus ?thesis
>  proof(elim conjE disjE)
>    assume *: "1 ≤ x"
>    show ?thesis by (rule Real.natfloor_div_nat[OF * assms])
>  next
>    assume *: "x ≤ 0"
>    moreover
>    from * assms have "x / y ≤ 0" by (simp add: field_simps)
>    ultimately
>    show ?thesis by (simp add: natfloor_neg)
>  next
>    assume *: "x ≥ 0" "x < 1"
>    hence "natfloor x = 0" by (auto intro: natfloor_eq)
>    moreover
>    from * assms have "x / y ≥ 0" and "x / y < 1" by (auto simp add: field_simps)
>    hence "natfloor (x/y) = 0" by (auto intro: natfloor_eq)
>    ultimately
>    show ?thesis by simp
>  qed
> qed
>
> Greetings,
> Joachim
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner

```