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.

Homework 9_1

This is the task corresponding to homework 9_1.

Resources

Download Files

Definitions File

theory Defs
  imports "HOL-Data_Structures.Balance" "HOL-Data_Structures.RBT_Set"
begin

fun mk_rbt :: "'a tree \<Rightarrow> 'a rbt" where
  "mk_rbt \<langle>\<rangle> = \<langle>\<rangle>"
| "mk_rbt \<langle>l, a, r\<rangle> = (let
    l'=mk_rbt l;
    r'=mk_rbt r
  in
    if min_height l > min_height r then
      B (paint Red l') a r'
    else if min_height l < min_height r then
      B l' a (paint Red r')
    else
      B l' a r'
  )"

consts list_to_rbt :: "'a list \<Rightarrow> 'a rbt"


end

Template File

theory Submission
  imports Defs
begin

fun list_to_rbt :: "'a list \<Rightarrow> 'a rbt"  where
  "list_to_rbt _ = Leaf"

lemma acomplete_alt:
  "acomplete t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
  sorry

lemma mk_rbt_inorder: "Tree2.inorder (list_to_rbt xs) = xs"
  sorry

lemma mk_rbt_color: "color (list_to_rbt xs) = Black"
  sorry

lemma mk_rbt_invh: "invh (list_to_rbt xs)"
  sorry

lemma mk_rbt_invc: "invc (list_to_rbt t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma acomplete_alt: "acomplete t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
  by (rule Submission.acomplete_alt)

lemma mk_rbt_inorder: "Tree2.inorder (list_to_rbt xs) = xs"
  by (rule Submission.mk_rbt_inorder)

lemma mk_rbt_color: "color (list_to_rbt xs) = Black"
  by (rule Submission.mk_rbt_color)

lemma mk_rbt_invh: "invh (list_to_rbt xs)"
  by (rule Submission.mk_rbt_invh)

lemma mk_rbt_invc: "invc (list_to_rbt t)"
  by (rule Submission.mk_rbt_invc)

end

Terms and Conditions