Homework 3

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

fun rotate :: "'a tree \<Rightarrow> 'a tree" where
  "rotate \<langle>\<langle>l1,a,l2\<rangle>,b,r\<rangle> = \<langle>l1,a,\<langle>l2,b,r\<rangle>\<rangle>"
| "rotate x = x"

declare [[names_short]]


consts rlc :: "'a tree \<Rightarrow> bool"

consts rotate1 :: "'a tree \<Rightarrow> 'a tree"

consts pot :: "'a tree \<Rightarrow> nat"


end

Template File

theory Submission
  imports Defs
begin

fun rlc :: "'a tree \<Rightarrow> bool"  where
  "rlc _ = True"

value "rlc \<langle>\<langle>\<rangle>,1::nat,\<langle>\<langle>\<rangle>,2,\<langle>\<langle>\<rangle>,3,\<langle>\<rangle>\<rangle>\<rangle>\<rangle>"
value "\<not>rlc \<langle>\<langle>\<rangle>,1::nat,\<langle>\<langle>\<langle>\<rangle>,3,\<langle>\<rangle>\<rangle>,2,\<langle>\<rangle>\<rangle>\<rangle>"

lemma bst_rotate[simp]: "bst t \<Longrightarrow> bst (rotate t)"
  sorry

lemma set_rotate[simp]: "set_tree (rotate t) = set_tree t"
  sorry

fun rotate1 :: "'a tree \<Rightarrow> 'a tree"  where
  "rotate1 _ = Leaf"

fun pot :: "'a tree \<Rightarrow> nat"  where
  "pot _ = 0"

lemma pot_0: "rlc t \<longleftrightarrow> pot t = 0"
  sorry

lemma pot_rotate_n[simp]: "pot ((rotate1 ^^ n) t) = pot t - n"
  sorry

theorem rlc_rotate: "\<exists>n \<le> size t. rlc ((rotate1 ^^ n) t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma bst_rotate: "bst t \<Longrightarrow> bst (rotate t)"
  by (rule Submission.bst_rotate)

lemma set_rotate: "set_tree (rotate t) = set_tree t"
  by (rule Submission.set_rotate)

lemma pot_0: "rlc t \<longleftrightarrow> pot t = 0"
  by (rule Submission.pot_0)

lemma pot_rotate_n: "pot ((rotate1 ^^ n) t) = pot t - n"
  by (rule Submission.pot_rotate_n)

theorem rlc_rotate: "\<exists>n \<le> size t. rlc ((rotate1 ^^ n) t)"
  by (rule Submission.rlc_rotate)

end