FDS Week 4 Homework

Definitions File

theory Defs
  imports Main
begin

datatype 'a mtree = Leaf | Node (left: "'a mtree") (minimum: 'a) (element: 'a) (right: "'a mtree")

end
  

Template File

theory Template
  imports Defs
begin

fun set_mtree2 where   
  "set_mtree2 _ = undefined"

fun mbst :: "'a::{linorder,zero} mtree \<Rightarrow> bool" where  
  "mbst _ = undefined"

fun min_val :: "'a::{linorder,zero} mtree \<Rightarrow> 'a" where
  "min_val _ = undefined"

lemma mbst_works: "mbst (Node l m a r) \<Longrightarrow> min_val (Node l m a r) = m"
  sorry

fun mins :: "'a::{linorder,zero} \<Rightarrow> 'a mtree \<Rightarrow> 'a mtree" where  
  "mins _ _ = undefined"

lemma mins_set: "mbst t \<Longrightarrow> set_mtree2 (mins x t) = insert x (set_mtree2 t)"
  sorry

lemma mins_works: "mbst t \<Longrightarrow> mbst (mins x t)"
  sorry

fun misin :: "'a::linorder \<Rightarrow> 'a mtree \<Rightarrow> bool" where
  "misin _ _ = undefined"

lemma misin_works: "mbst t \<Longrightarrow> misin x t \<longleftrightarrow> x\<in>set_mtree2 t"
  sorry

fun mtree_in_range :: "'a::linorder mtree \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list"
  where
    "mtree_in_range _ _ _ = undefined"

lemma mtree_in_range_works: "mbst t \<Longrightarrow> set (mtree_in_range t u v) = {x\<in>set_mtree2 t. u\<le>x \<and> x\<le>v}"
  sorry

end
  

Check File

theory Check
  imports Template
begin

lemma mbst_works: "mbst (Node l m a r) \<Longrightarrow> min_val (Node l m a r) = m"  
  by (rule mbst_works)

lemma mins_works: "mbst t \<Longrightarrow> mbst (mins x t)"
  by (rule mins_works)

lemma misin_works: "mbst t \<Longrightarrow> misin x t \<longleftrightarrow> x\<in>set_mtree2 t"
  by (rule misin_works)

lemma mtree_in_range_works: "mbst t \<Longrightarrow> set (mtree_in_range t u v) = {x\<in>set_mtree2 t. u\<le>x \<and> x\<le>v}"  
  by (rule mtree_in_range_works)

end