src/HOL/Data_Structures/Tree23_Set.thy
 changeset 68020 6aade817bee5 parent 67965 aaa31cd0caef child 68109 cebf36c14226
```     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Fri Apr 20 22:22:46 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sat Apr 21 08:41:42 2018 +0200
1.3 @@ -102,13 +102,13 @@
1.4  "node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
1.5  "node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
1.6
1.7 -fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
1.8 -"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
1.9 -"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
1.10 -"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
1.11 -"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
1.12 +fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
1.13 +"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
1.14 +"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
1.15 +"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
1.16 +"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
1.17
1.18 -text \<open>In the base cases of \<open>del_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
1.19 +text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
1.20  in which case balancedness implies that so are the others. Exercise.\<close>
1.21
1.22  fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
1.23 @@ -123,15 +123,15 @@
1.24    (case cmp x a of
1.25       LT \<Rightarrow> node21 (del x l) a r |
1.26       GT \<Rightarrow> node22 l a (del x r) |
1.27 -     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
1.28 +     EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
1.29  "del x (Node3 l a m b r) =
1.30    (case cmp x a of
1.31       LT \<Rightarrow> node31 (del x l) a m b r |
1.32 -     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
1.33 +     EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
1.34       GT \<Rightarrow>
1.35         (case cmp x b of
1.36            LT \<Rightarrow> node32 l a (del x m) b r |
1.37 -          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
1.38 +          EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
1.39            GT \<Rightarrow> node33 l a m b (del x r)))"
1.40
1.41  definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
1.42 @@ -182,16 +182,16 @@
1.43  lemmas inorder_nodes = inorder_node21 inorder_node22
1.44    inorder_node31 inorder_node32 inorder_node33
1.45
1.46 -lemma del_minD:
1.47 -  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
1.48 +lemma split_minD:
1.49 +  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
1.50    x # inorder(tree\<^sub>d t') = inorder t"
1.51 -by(induction t arbitrary: t' rule: del_min.induct)
1.52 +by(induction t arbitrary: t' rule: split_min.induct)
1.53    (auto simp: inorder_nodes split: prod.splits)
1.54
1.55  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
1.56    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
1.57  by(induction t rule: del.induct)
1.58 -  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
1.59 +  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
1.60
1.61  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
1.62    inorder(delete x t) = del_list x (inorder t)"
1.63 @@ -350,23 +350,23 @@
1.64  lemmas heights = height'_node21 height'_node22
1.65    height'_node31 height'_node32 height'_node33
1.66
1.67 -lemma height_del_min:
1.68 -  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
1.69 -by(induct t arbitrary: x t' rule: del_min.induct)
1.70 +lemma height_split_min:
1.71 +  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
1.72 +by(induct t arbitrary: x t' rule: split_min.induct)
1.73    (auto simp: heights split: prod.splits)
1.74
1.75  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
1.76  by(induction x t rule: del.induct)
1.77 -  (auto simp: heights max_def height_del_min split: prod.splits)
1.78 +  (auto simp: heights max_def height_split_min split: prod.splits)
1.79
1.80 -lemma bal_del_min:
1.81 -  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
1.82 -by(induct t arbitrary: x t' rule: del_min.induct)
1.83 -  (auto simp: heights height_del_min bals split: prod.splits)
1.84 +lemma bal_split_min:
1.85 +  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
1.86 +by(induct t arbitrary: x t' rule: split_min.induct)
1.87 +  (auto simp: heights height_split_min bals split: prod.splits)
1.88
1.89  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
1.90  by(induction x t rule: del.induct)
1.91 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
1.92 +  (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
1.93
1.94  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
1.95  by(simp add: delete_def bal_tree\<^sub>d_del)
```