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 <breit...@kit.edu> > > > To: isabelle-us...@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-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
