Email Gateway (Oct 02 2021 at 09:19): Email Gateway (Oct 02 2021 at 09:19):From: "N. Raghavendra" <nyraghu27132@gmail.com>
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.
Email Gateway (Oct 02 2021 at 09:25):From: Jakub Kądziołka <kuba@kadziolka.net>
The workflow of producing a verified program in Isabelle goes the other
way around — you define the functions in your Isabelle code, and then
instruct Isabelle to generate the corresponding code in SML, OCaml,
Haskell, or Scala, by using the export_code command (see
https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf).
The SML_file command imports your definitions on the meta level — they
can be used to write automation for finding the proofs, but are
completely outside of the logic and nothing can be proved about them.
Hope this helps.
Regards,
Jakub Kądziołka
Email Gateway (Oct 03 2021 at 05:15):From: "N. Raghavendra" <nyraghu27132@gmail.com>
Thanks for the clarification. I'll see the program extraction manual.
Regards,
Raghu.
At 2021-10-02T11:20:12+02:00, Jakub Kądziołka wrote:
Email Gateway (Oct 03 2021 at 05:17):From: "N. Raghavendra" <nyraghu27132@gmail.com>
At 2021-10-02T13:35:27+02:00, Buday Gergely István wrote:
If you wanted to verify ML programs you might take a look at CakeML
where you can verify ML programs down to machine code using HOL4.
Thanks for the pointer. It seems a bit far from my interests now.
Regards,
Raghu.
Last updated: Jul 15 2022 at 23:21 UTC