Homework 4

Definitions File

theory Defs
  imports Main
begin

datatype 'a rtree = Leaf | Node "'a rtree" nat 'a "'a rtree"

definition "at_index i l x \<equiv> i<length l \<and> l!i=x"

declare Let_def [simp]
declare [[names_short]]


consts num_nodes :: "'a rtree \<Rightarrow> nat"

consts rbst :: "'a::linorder rtree \<Rightarrow> bool"

consts rins :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree"

consts risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool"

consts inorder :: "'a rtree \<Rightarrow> 'a list"

consts rank :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> nat"

consts select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a"


end

Template File

theory Submission
  imports Defs
begin

fun num_nodes :: "'a rtree \<Rightarrow> nat"  where
  "num_nodes _ = undefined"

fun rbst :: "'a::linorder rtree \<Rightarrow> bool"  where
  "rbst _ = undefined"

fun rins :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree"  where
  "rins _ = undefined"

lemma rins_set: "set_rtree (rins x t) = insert x (set_rtree t)"
  sorry

lemma rins_invar: "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
  sorry

fun risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool"  where
  "risin _ = undefined"

lemma risin_set: "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
  sorry

fun inorder :: "'a rtree \<Rightarrow> 'a list"  where
  "inorder _ = undefined"

fun rank :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> nat"  where
  "rank _ = undefined"

lemma inorder_index: "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
  sorry

fun select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a"  where
  "select _ = undefined"

lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma rins_set: "set_rtree (rins x t) = insert x (set_rtree t)"
  by (rule Submission.rins_set)

lemma rins_invar: "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
  by (rule Submission.rins_invar)

lemma risin_set: "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
  by (rule Submission.risin_set)

lemma inorder_index: "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
  by (rule Submission.inorder_index)

lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
  by (rule Submission.select_correct)

end