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