Re: [isabelle] learning isabelle



Hi,

Ruben Henner Zilibowitz wrote:
> Just trying to learn isabelle and had trouble with the following:
> 
> primrec
> "checksort (x#y#zs) = ((x <= y) \<and> (checksort (y#zs)))"
> "checksort _ = True"

primrec only supports primitive recursion, i.e. pattern matching on
lists must emply only the patterns (x#xs) and [].  In your
specification, you could get along by using explicit case distinction on
the right hand side:

consts checksort :: "'a::order list => bool"

primrec
  "checksort (x#xs) <-> (case xs of y # _ => x <= y & checksort xs | _
=> True)"
  "checksort [] = True"

Alternativly, consider the "function" command.

Hope this helps,
	Florian

begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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