[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

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.