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.
theory Defs imports Main begin datatype 'a mtree = Leaf | Node (left: "'a mtree") (minimum: 'a) (element: 'a) (right: "'a mtree") end
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
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