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

[Johannes Hölzl]

I will fix it.

  - Johannes

Am Sonntag, den 26.10.2014, 17:25 +0000 schrieb 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev