[isabelle-dev] natfloor_div_nat not general enough

[Johannes Hölzl]

This is now generalized in the repository:

This generalizes to floor, and removes the assumption 0 <= y
  http://isabelle.in.tum.de/repos/isabelle/rev/d17b3844b726

This finally removes the assumption 0 <= x
  http://isabelle.in.tum.de/repos/isabelle/rev/387f65e69dd5


 - Johannes

Am Montag, den 27.10.2014, 09:42 +0100 schrieb 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
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev