Skip to content

Instantly share code, notes, and snippets.

@larsrh larsrh/Scratch.thy
Created Sep 24, 2015

Embed
What would you like to do?
Scala World 2015
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.