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.

FDS Week 8 Homework Bonus

Week 8 homework Bonus.

Resources

Download Files

Definitions File

theory Defs
  imports Main "HOL-Data_Structures.Tree23_Set"
begin

fun join :: "'a tree23 \<Rightarrow> 'a tree23 \<Rightarrow> 'a upI" where
  "join Leaf Leaf = TI Leaf"
| "join (Node2 l1 a r1) (Node2 l2 b r2) = 
    (case join r1 l2 of TI t \<Rightarrow> TI (Node3 l1 a t b r2)
                      | OF t1 c t2 \<Rightarrow> OF (Node2 l1 a t1) c (Node2 t2 b r2))"
| "join (Node2 l1 a r1) (Node3 l2 b m2 c r2) = 
    (case join r1 l2 of TI t \<Rightarrow> OF (Node2 l1 a t) b (Node2 m2 c r2)
                      | OF t1 d t2 \<Rightarrow> OF (Node2 l1 a t1) d (Node3 t2 b m2 c r2))"
| "join (Node3 l1 a m1 b r1) (Node2 l2 c r2) = 
    (case join r1 l2 of TI t \<Rightarrow> OF (Node2 l1 a m1) b (Node2 t c r2)
                      | OF t1 d t2 \<Rightarrow> OF (Node3 l1 a m1 b t1) d (Node2 t2 c r2))"
| "join (Node3 l1 a m1 b r1) (Node3 l2 c m2 d r2) = 
    (case join r1 l2 of TI t \<Rightarrow> OF (Node3 l1 a m1 b t) c (Node2 m2 d r2)
                      | OF t1 e t2 \<Rightarrow> OF (Node3 l1 a m1 b t1) e (Node3 t2 c m2 d r2))"

end

Template File

theory Template
  imports Defs
begin

fun del' :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
  "del' _ _ = undefined"

lemma inorder_del': "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> 
                        inorder(treeD (del' x t)) = del_list x (inorder t)"
  sorry

lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del' x t))"
  sorry

end

Check File

theory Check
  imports Template
begin

lemma inorder_del': "\<lbrakk>complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
                        inorder(treeD (del' x t)) = del_list x (inorder t)"
  by(rule inorder_del')

lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del' x t))"
  by(rule complete_treeD_del)

end

Terms and Conditions