Re: [isabelle] nat properties

kuecuek at wrote:


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?


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
Raum: 01.11.059

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