How do I write this function in SML

Question

I am trying to write a function in Isabelle for some tasks in an assignment and I wanted to make sure that my function works correctly so I thought about testing it in SML but I can't seem to be able to figure out how to write it. I have never used/wrote/learned functional programming so I am having a little trouble with it. Can someone help me or maybe if there is something in Isabelle about testing how a function works can he point me to the correct direction?

The functions are the following and basically are removing the first occurrence of an element in a list and removing all occurrences from a list

fun del1:: "'a ⇒ 'a list ⇒ 'a list" where
  "del1 a Nil = Nil" |
  "del1 a (x#xs) = (if x = a then xs else x#(del1 a xs))"


fun delall:: "'a ⇒ 'a list ⇒ 'a list" where
  "delall a Nil = Nil" |
  "delall a (x#xs) = (if x = a then (delall a xs) else x#(delall a xs))"

Answer 1

I am not quite sure whether I get your question. First, the syntax of Isabelle/HOL and SML is not very different. If you just want to get variants of your function in SML, probably the fastest way is using Isabelle's code generator

export_code del1 delall in SML

which results in something like

fun del1 A_ a [] = []
  | del1 A_ a (x :: xs) = (if HOL.eq A_ x a then xs else x :: del1 A_ a xs);

fun delall A_ a [] = []
  | delall A_ a (x :: xs) =
    (if HOL.eq A_ x a then delall A_ a xs else x :: delall A_ a xs);

However, since this contains some Isabelle specific stuff (like a dictionary construction to get rid of type classes) maybe you prefer hand-written code:

fun del1 a [] = []
  | del1 a (x::xs) = if x = a then xs else x :: (del1 a xs)

fun delall a [] = []
  | delall a (x::xs) = if x = a then delall a xs else x :: delall a xs

On the other hand, if you just want to try out your functions on some inputs, you can do that inside Isabelle using value. E.g.,

value "del1 (2::nat) [1, 2 , 3]"
value "delall ''x'' [''x'', ''y'', ''z'', ''q'', ''x'']"

Answer 2

There is little to add to the answer by Chris, only this detail: In Isabelle2013-2 the Isabelle/jEdit Documentation panel has a few quickstart examples. This includes src/HOL/ex/ML.thy which shows a little bit of Isabelle/HOL as logical language and SML as functional language, and some connections between them.