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
