Re: [isabelle] nat properties



kuecuek at 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

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")


--
Steven Obua
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching

Tel: ++49 (0)89 / 289-17328
EMail: obua at in.tum.de
Raum: 01.11.059






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