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)