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.

FDS Week 4 homework

Week 4 homewokr

Resources

Download Files

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

Terms and Conditions