Homework 3

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
  "isin Leaf x = False" |
  "isin (Node l a r) x =
  (if x < a then isin l x else
   if x > a then isin r x
   else True)"

fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "ins x Leaf = Node Leaf x Leaf" |
  "ins x (Node l a r) =
  (if x < a then Node (ins x l) a r else
   if x > a then Node l a (ins x r)
   else Node l a r)"

lemma set_tree_isin: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
  apply(induction t)
   apply auto
  done

lemma set_tree_ins: "set_tree (ins x t) = {x} \<union> set_tree t"
  apply(induction t)
   apply auto
  done

lemma bst_ins: "bst t \<Longrightarrow> bst (ins x t)"
  apply(induction t)
   apply (auto simp: set_tree_ins)
  done


datatype direction = L | R
type_synonym path = "direction list"

declare [[names_short]]


consts bst_remdups_aux :: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

consts get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"

consts put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"

consts valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"

consts find :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> path set"


end

Template File

theory Submission
  imports Defs
begin

fun bst_remdups_aux :: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list"  where
  "bst_remdups_aux _ = undefined"

definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"


theorem remdups_set: "set (bst_remdups xs) = set xs"
  sorry

theorem remdups_distinct: "distinct (bst_remdups xs)"
  sorry

fun sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  where
  "sublist _ = undefined"

theorem remdups_sub: "sublist (bst_remdups xs) xs"
  sorry

fun get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"  where
  "get _ = undefined"

fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"  where
  "put _ = undefined"

fun valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"  where
  "valid _ = undefined"

fun find :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> path set"  where
  "find _ = undefined"

lemma get_put: "valid t p \<Longrightarrow> put t p (get t p) = t"
  sorry

lemma put_get: "valid t p \<Longrightarrow> get (put t p s) p = s"
  sorry

lemma find_get: "p \<in> find t s \<Longrightarrow> get t p = s"
  sorry

lemma put_find: "valid t p \<Longrightarrow> p \<in> find (put t p s) s"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem remdups_set: "set (bst_remdups xs) = set xs"
  by (rule Submission.remdups_set)

theorem remdups_distinct: "distinct (bst_remdups xs)"
  by (rule Submission.remdups_distinct)

theorem remdups_sub: "sublist (bst_remdups xs) xs"
  by (rule Submission.remdups_sub)

lemma get_put: "valid t p \<Longrightarrow> put t p (get t p) = t"
  by (rule Submission.get_put)

lemma put_get: "valid t p \<Longrightarrow> get (put t p s) p = s"
  by (rule Submission.put_get)

lemma find_get: "p \<in> find t s \<Longrightarrow> get t p = s"
  by (rule Submission.find_get)

lemma put_find: "valid t p \<Longrightarrow> p \<in> find (put t p s) s"
  by (rule Submission.put_find)

end