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

[Lawrence Paulson]

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