Homework 4

Definitions File

theory Defs
  imports Main
begin

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


consts set_mtree2 :: "'a mtree \<Rightarrow> 'a set"

consts mbst :: "'a::{linorder,zero} mtree \<Rightarrow> bool"

consts min_val :: "'a::{linorder,zero} mtree \<Rightarrow> 'a"

consts mins :: "'a::{linorder,zero} \<Rightarrow> 'a mtree \<Rightarrow> 'a mtree"

consts misin :: "'a::linorder \<Rightarrow> 'a mtree \<Rightarrow> bool"

consts mtree_in_range :: "'a::linorder mtree \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

fun set_mtree2 :: "'a mtree \<Rightarrow> 'a set"  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_min: "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 mbst_mins: "mbst t \<Longrightarrow> mbst (mins x t)"
  sorry

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

lemma misin_set: "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 mbst_range: "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 Submission
begin

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

lemma mbst_mins: "mbst t \<Longrightarrow> mbst (mins x t)"
  by (rule Submission.mbst_mins)

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

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

end