*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] natfloor_div_nat not general enough*From*: Joachim Breitner <breitner at kit.edu>*Date*: Sun, 26 Oct 2014 15:15:40 +0100

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

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Next by Date: Re: [isabelle] how to know which rules to apply before apply(auto)?
- Previous by Thread: Re: [isabelle] Vocabulary question: is the real name of HOL, λHOL?
- Next by Thread: [isabelle] is it possible to find the function from lemmas and which command can do?
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list