FDS Week 4 homework

Definitions File

theory Defs
  imports Main
begin

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

end

Template File

theory Submission
  imports Defs
begin

fun set_mtree2 where 
  "set_mtree2 _ = undefined"

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

fun max_val :: "'a::{linorder,zero} mtree => 'a" where
  "max_val _ = undefined"

lemma mbst_correct: "mbst (Node l m a r) ==> max_val (Node l m a r) = m"
  sorry

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

lemma mbst_mins: "mbst t ==> mbst (mins x t)"
  sorry

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

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

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

lemma mtree_in_range_works: "mbst t ==> 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 Submission
begin

lemma mbst_correct: "mbst (Node l m a r) ==> max_val (Node l m a r) = m"
  by (rule mbst_correct)

lemma mbst_mins: "mbst t ==> mbst (mins x t)"
  by (rule mbst_mins)

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

lemma mtree_in_range_works: "mbst t ==> 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