Re: [isabelle] even/odd with primrec



> primrec even :: "nat => bool"
>      and odd :: "nat => bool" where
> "even 0 = True" |
> "even (Suc n) = odd n" |
> "odd 0 = False" |
> "odd (Suc n) = even n"

Also note that the original specification of things does not matter as
long as you can derive the desired properties.  In that case you could
e.g. define

definition even :: "nat => bool" where
  "even n <-> n mod 2 = 0"

definition odd :: "nat => bool" where
  odd n <-> n mod 2 = 1"

and derive the recursive rules:

lemma [simp]:
  "even 0 = True"
  "even (Suc n) = odd n"
  "odd 0 = False"
  "odd (Suc n) = even n"
  <proof>

Also note that even/odd is already present in the HOL theory Parity;
just import theory Complex_Main to use it.


Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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