Scala World 2015

Scratch.thy

theory Scratch
imports Main
begin

fun insert :: "'a::linorder ⇒ 'a list ⇒ 'a list" where
"insert x [] = [x]" |
"insert x (y # ys) = (if x ≤ y then x # y # ys else y # insert x ys)"

inductive sorted :: "'a::linorder list ⇒ bool" where
empty: "sorted []" |
single: "sorted [x]" |
cons: "x⇩1 ≤ x⇩2 ⟹ sorted (x⇩2 # xs) ⟹ sorted (x⇩1 # x⇩2 # xs)"

code_pred sorted .

lemma
  assumes "sorted xs"
  shows "sorted (insert x xs)"
using assms
proof (induction)
  case empty
  show "sorted (insert x [])"
    by (simp add: sorted.single)
next
  case single
  show ?case sorry
next
  case cons
  show ?case sorry
qed

export_code sorted insert in Scala

end