Email Gateway (Aug 18 2022 at 09:39): Email Gateway (Aug 18 2022 at 09:39):From: kuecuek@rbg.informatik.tu-darmstadt.de
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
Email Gateway (Aug 18 2022 at 09:39):From: Amine Chaieb <chaieb@in.tum.de>
kuecueck,
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".
Amine.
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
proof-
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
qed
kuecuek@rbg.informatik.tu-darmstadt.de 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
Email Gateway (Aug 18 2022 at 09:39):From: Amine Chaieb <chaieb@in.tum.de>
kuecueck,
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".
Amine.
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
proof-
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
qed
kuecuek@rbg.informatik.tu-darmstadt.de wrote:
Email Gateway (Aug 18 2022 at 09:40):From: Steven Obua <obua@in.tum.de>
kuecuek@rbg.informatik.tu-darmstadt.de wrote:
Actually, there is a theory (IntDiv.thy in HOL/Integ) which has lemmas
for this kind of situation. In your case the following works:
lemma "[|(0::int)<a; 0<b; a dvd b|]==> (nat a) dvd (nat b)"
by (simp add: "nat_dvd_iff")
Last updated: May 03 2024 at 12:27 UTC