Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 3

This is the task corresponding to homework 3.

Resources

Download Files

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

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"

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

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 _ _ = []"

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 _ _ = True"

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

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

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

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

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

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

Terms and Conditions