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
