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

### 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