Isabelle list demo

Demo.thy

theory Demo
imports Predicate_Compile Extraction
begin

datatype 'a list = Nil
  | Cons (head: 'a) (tail: "'a list")
  for map: lmap

primrec append :: "'a list ⇒ 'a list ⇒ 'a list" where
  "append Nil ys = ys"
| "append (Cons x xs) ys = Cons x (append xs ys)"

value "append (Cons 1 (Cons 2 Nil)) (Cons 4 (Cons 5 Nil))"

primrec rev :: "'a list ⇒ 'a list" where
  "rev Nil = Nil"
| "rev (Cons x xs) = append (rev xs) (Cons x Nil)"

export_code rev in Haskell

lemma "2+2 = 4" by (simp)

lemma append_nil [simp]: "append xs Nil = xs"
proof (induction xs)
  case Nil
  then show ?case by (fact append.simps)
next
  case (Cons x1 xs)
  have "append (Cons x1 xs) Nil = Cons x1 (append xs Nil)" by (fact append.simps)
  also have "append xs Nil = xs" by (fact Cons.IH)
  finally show "append (Cons x1 xs) Nil = Cons x1 xs" by (this)
qed

lemma append_assoc [simp]: "append (append xs ys) zs = append xs (append ys zs)"
  apply (induction xs)
   apply (auto)
    done

lemma rev_append [simp]: "rev (append xs ys) = append (rev ys) (rev xs)"
  apply (induction xs)
   apply (simp_all)
    done

theorem rev_rev: "rev (rev xs) = xs"
  apply (induction xs)
   apply (auto)
    done


primrec qrev :: "'a list ⇒ 'a list ⇒ 'a list" where
  "qrev Nil acc = acc"
| "qrev (Cons x xs) acc = qrev xs (Cons x acc)"

lemma [simp]: "∀ys. qrev xs ys = append (rev xs) ys"
  apply (induction xs)
  apply (auto)
    done

theorem rev_qrev: "rev xs = qrev xs Nil"
  apply (induction xs)
   apply (auto)
    done

declare rev_qrev[code]

export_code rev in Scala

  
function merge :: "'a list ⇒ 'a list ⇒ 'a list" where
  "merge Nil ys = ys"
| "merge (Cons x xs) ys = Cons x (merge ys xs)"
  by (pat_completeness) auto
  
termination
  apply (relation "measure (λ(xs, ys). size xs + size ys)")
   by (auto)

value "merge (Cons 1 (Cons 2 Nil)) (Cons 3 (Cons 4 Nil))"

end