[isabelle] How to verify properties of simple SML programs



I am using Isabelle for the first time.  I would like to verify
properties of simple SML programs.  For example, I have an SML file
with the following content:

-- foo.sml

fun foldr _ y [] = y
  | foldr f y (x :: xs) = f (x, (foldr f y xs))

fun foldl _ y [] = y
  | foldl f y (x :: xs) = foldl f (f (x, y)) xs

-- end of file

I am able to import this SML from an Isabelle file like this

-- foo.thy

theory foo
  imports Pure
begin

SML_file ‹foo.sml›

end

-- end of file

Now how do I prove, e.g., that

foldl f y xs = foldr f y (rev xs)

Thanks!

Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/




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