src/HOL/Data_Structures/Tree234_Set.thy
changeset 68020 6aade817bee5
parent 67965 aaa31cd0caef
child 68109 cebf36c14226
     1.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -154,13 +154,13 @@
     1.4  "node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
     1.5  "node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
     1.6  
     1.7 -fun del_min :: "'a tree234 \<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 (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
    1.11 -"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    1.12 -"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
    1.13 -"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))"
    1.14 +fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
    1.15 +"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
    1.16 +"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    1.17 +"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
    1.18 +"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
    1.19 +"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" |
    1.20 +"split_min (Node4 l a m b n c r) = (let (x,l') = split_min l in (x, node41 l' a m b n c r))"
    1.21  
    1.22  fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
    1.23  "del k Leaf = T\<^sub>d Leaf" |
    1.24 @@ -175,23 +175,23 @@
    1.25  "del k (Node2 l a r) = (case cmp k a of
    1.26    LT \<Rightarrow> node21 (del k l) a r |
    1.27    GT \<Rightarrow> node22 l a (del k r) |
    1.28 -  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
    1.29 +  EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
    1.30  "del k (Node3 l a m b r) = (case cmp k a of
    1.31    LT \<Rightarrow> node31 (del k 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> (case cmp k b of
    1.35             LT \<Rightarrow> node32 l a (del k m) b r |
    1.36 -           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
    1.37 +           EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
    1.38             GT \<Rightarrow> node33 l a m b (del k r)))" |
    1.39  "del k (Node4 l a m b n c r) = (case cmp k b of
    1.40    LT \<Rightarrow> (case cmp k a of
    1.41            LT \<Rightarrow> node41 (del k l) a m b n c r |
    1.42 -          EQ \<Rightarrow> let (a',m') = del_min m in node42 l a' m' b n c r |
    1.43 +          EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r |
    1.44            GT \<Rightarrow> node42 l a (del k m) b n c r) |
    1.45 -  EQ \<Rightarrow> let (b',n') = del_min n in node43 l a m b' n' c r |
    1.46 +  EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r |
    1.47    GT \<Rightarrow> (case cmp k c of
    1.48             LT \<Rightarrow> node43 l a m b (del k n) c r |
    1.49 -           EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
    1.50 +           EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' |
    1.51             GT \<Rightarrow> node44 l a m b n c (del k r)))"
    1.52  
    1.53  definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
    1.54 @@ -259,16 +259,16 @@
    1.55    inorder_node31 inorder_node32 inorder_node33
    1.56    inorder_node41 inorder_node42 inorder_node43 inorder_node44
    1.57  
    1.58 -lemma del_minD:
    1.59 -  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    1.60 +lemma split_minD:
    1.61 +  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    1.62    x # inorder(tree\<^sub>d t') = inorder t"
    1.63 -by(induction t arbitrary: t' rule: del_min.induct)
    1.64 +by(induction t arbitrary: t' rule: split_min.induct)
    1.65    (auto simp: inorder_nodes split: prod.splits)
    1.66  
    1.67  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    1.68    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    1.69  by(induction t rule: del.induct)
    1.70 -  (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
    1.71 +  (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits)
    1.72    (* 30 secs (2016) *)
    1.73  
    1.74  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    1.75 @@ -476,23 +476,23 @@
    1.76    height_node31 height_node32 height_node33
    1.77    height_node41 height_node42 height_node43 height_node44
    1.78  
    1.79 -lemma height_del_min:
    1.80 -  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    1.81 -by(induct t arbitrary: x t' rule: del_min.induct)
    1.82 +lemma height_split_min:
    1.83 +  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    1.84 +by(induct t arbitrary: x t' rule: split_min.induct)
    1.85    (auto simp: heights split: prod.splits)
    1.86  
    1.87  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    1.88  by(induction x t rule: del.induct)
    1.89 -  (auto simp add: heights height_del_min split!: if_split prod.split)
    1.90 +  (auto simp add: heights height_split_min split!: if_split prod.split)
    1.91  
    1.92 -lemma bal_del_min:
    1.93 -  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    1.94 -by(induct t arbitrary: x t' rule: del_min.induct)
    1.95 -  (auto simp: heights height_del_min bals split: prod.splits)
    1.96 +lemma bal_split_min:
    1.97 +  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    1.98 +by(induct t arbitrary: x t' rule: split_min.induct)
    1.99 +  (auto simp: heights height_split_min bals split: prod.splits)
   1.100  
   1.101  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   1.102  by(induction x t rule: del.induct)
   1.103 -  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
   1.104 +  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
   1.105  
   1.106  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   1.107  by(simp add: delete_def bal_tree\<^sub>d_del)