Re: [isabelle] nat properties


Here is a proof of your lemma. Unfortunately it includes certan non trivial steps, whith whom automatic tactics do not deal.

The key here is to give a witness divisor for "nat a dvd nat b" which is "nat k", where k is the witness divisor for "a dvd b".


lemma assumes ap:"(0::int)<a" and bp:"0<b" and d: "a dvd b"
  shows "(nat a) dvd (nat b)"
using ap bp d
  from d have " EX k. b = a*k" unfolding dvd_def .
  then obtain k where bak: "b= a*k" by blast
  with ap bp have kp: "k >= 0"
    using mult_less_cancel_right_disj[where a="0" and c="k" and b="a"]
    by auto
  from ap bp have ap': "a >= 0" and bp':"b >= 0" by simp+
  from mult_nonneg_nonneg[OF ap' kp] have akp:"a*k >= 0" .
  from nat_mult_distrib[OF ap', where z'="k", symmetric] bak
    eq_nat_nat_iff[OF bp' akp] have "nat b = nat a * nat k" by simp
  thus ?thesis by auto

kuecuek at wrote:
> Hallo
> i need some properties of the nat.
> i couldn't proof the lemma below.
> [|(0::int)<a; 0<b; a dvd b|]==> (nat a) dvd (nat b)
> is there any theory which include such properties or is there a solution to
> prove this lemma?
> thanks

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