[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
More information about the isabelle-dev
mailing list