del_min -> split_min
authornipkow
Sat Apr 21 08:41:42 2018 +0200 (13 months ago)
changeset 680206aade817bee5
parent 68019 32d19862781b
child 68021 b91a043c0dcb
del_min -> split_min
src/HOL/Data_Structures/Binomial_Heap.thy
src/HOL/Data_Structures/Brother12_Map.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Leftist_Heap.thy
src/HOL/Data_Structures/Priority_Queue.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Map.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -353,18 +353,18 @@
     1.4  using assms
     1.5  by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
     1.6  
     1.7 -subsubsection \<open>\<open>del_min\<close>\<close>
     1.8 +subsubsection \<open>\<open>split_min\<close>\<close>
     1.9  
    1.10 -definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
    1.11 -"del_min ts = (case get_min_rest ts of
    1.12 +definition split_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
    1.13 +"split_min ts = (case get_min_rest ts of
    1.14     (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
    1.15  
    1.16 -lemma invar_del_min[simp]:
    1.17 +lemma invar_split_min[simp]:
    1.18    assumes "ts \<noteq> []"
    1.19    assumes "invar ts"
    1.20 -  shows "invar (del_min ts)"
    1.21 +  shows "invar (split_min ts)"
    1.22  using assms
    1.23 -unfolding invar_def del_min_def
    1.24 +unfolding invar_def split_min_def
    1.25  by (auto
    1.26        split: prod.split tree.split
    1.27        intro!: invar_bheap_merge invar_oheap_merge
    1.28 @@ -372,11 +372,11 @@
    1.29        intro!: invar_oheap_children invar_bheap_children
    1.30      )
    1.31  
    1.32 -lemma mset_heap_del_min:
    1.33 +lemma mset_heap_split_min:
    1.34    assumes "ts \<noteq> []"
    1.35 -  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
    1.36 +  shows "mset_heap ts = mset_heap (split_min ts) + {# get_min ts #}"
    1.37  using assms
    1.38 -unfolding del_min_def
    1.39 +unfolding split_min_def
    1.40  apply (clarsimp split: tree.split prod.split)
    1.41  apply (frule (1) get_min_rest_get_min_same_root)
    1.42  apply (frule (1) mset_get_min_rest)
    1.43 @@ -391,7 +391,7 @@
    1.44  
    1.45  interpretation binheap: Priority_Queue_Merge
    1.46    where empty = "[]" and is_empty = "(=) []" and insert = insert
    1.47 -  and get_min = get_min and del_min = del_min and merge = merge
    1.48 +  and get_min = get_min and split_min = split_min and merge = merge
    1.49    and invar = invar and mset = mset_heap
    1.50  proof (unfold_locales, goal_cases)
    1.51    case 1 thus ?case by simp
    1.52 @@ -401,7 +401,7 @@
    1.53    case 3 thus ?case by auto
    1.54  next
    1.55    case (4 q)
    1.56 -  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>]
    1.57 +  thus ?case using mset_heap_split_min[of q] get_min[OF _ \<open>invar q\<close>]
    1.58      by (auto simp: union_single_eq_diff)
    1.59  next
    1.60    case (5 q) thus ?case using get_min[of q] by auto
    1.61 @@ -603,7 +603,7 @@
    1.62    finally show ?thesis by auto
    1.63  qed
    1.64  
    1.65 -subsubsection \<open>\<open>t_del_min\<close>\<close>
    1.66 +subsubsection \<open>\<open>t_split_min\<close>\<close>
    1.67  
    1.68  fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
    1.69    "t_get_min_rest [t] = 1"
    1.70 @@ -639,8 +639,8 @@
    1.71  
    1.72  definition "t_rev xs = length xs + 1"
    1.73  
    1.74 -definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where
    1.75 -  "t_del_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
    1.76 +definition t_split_min :: "'a::linorder heap \<Rightarrow> nat" where
    1.77 +  "t_split_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
    1.78                      \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
    1.79    )"
    1.80  
    1.81 @@ -661,12 +661,12 @@
    1.82    finally show ?thesis by (auto simp: algebra_simps)
    1.83  qed
    1.84  
    1.85 -lemma t_del_min_bound_aux:
    1.86 +lemma t_split_min_bound_aux:
    1.87    fixes ts
    1.88    defines "n \<equiv> size (mset_heap ts)"
    1.89    assumes BINVAR: "invar_bheap ts"
    1.90    assumes "ts\<noteq>[]"
    1.91 -  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
    1.92 +  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
    1.93  proof -
    1.94    obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
    1.95      by (metis surj_pair tree.exhaust_sel)
    1.96 @@ -687,8 +687,8 @@
    1.97      finally show ?thesis by (auto simp: algebra_simps)
    1.98    qed
    1.99  
   1.100 -  have "t_del_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
   1.101 -    unfolding t_del_min_def by (simp add: GM)
   1.102 +  have "t_split_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
   1.103 +    unfolding t_split_min_def by (simp add: GM)
   1.104    also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
   1.105      using t_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
   1.106    also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
   1.107 @@ -700,17 +700,17 @@
   1.108      unfolding n\<^sub>1_def n\<^sub>2_def n_def
   1.109      using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
   1.110      by (auto simp: mset_heap_def)
   1.111 -  finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
   1.112 +  finally have "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
   1.113      by auto
   1.114    thus ?thesis by (simp add: algebra_simps)
   1.115  qed
   1.116  
   1.117 -lemma t_del_min_bound:
   1.118 +lemma t_split_min_bound:
   1.119    fixes ts
   1.120    defines "n \<equiv> size (mset_heap ts)"
   1.121    assumes "invar ts"
   1.122    assumes "ts\<noteq>[]"
   1.123 -  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
   1.124 -using assms t_del_min_bound_aux unfolding invar_def by blast
   1.125 +  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
   1.126 +using assms t_split_min_bound_aux unfolding invar_def by blast
   1.127  
   1.128  end
   1.129 \ No newline at end of file
     2.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Fri Apr 20 22:22:46 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sat Apr 21 08:41:42 2018 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4    (case cmp x a of
     2.5       LT \<Rightarrow> n2 (del x l) (a,b) r |
     2.6       GT \<Rightarrow> n2 l (a,b) (del x r) |
     2.7 -     EQ \<Rightarrow> (case del_min r of
     2.8 +     EQ \<Rightarrow> (case split_min r of
     2.9                None \<Rightarrow> N1 l |
    2.10                Some (ab, r') \<Rightarrow> n2 l ab r'))"
    2.11  
    2.12 @@ -84,7 +84,7 @@
    2.13  lemma inorder_del:
    2.14    "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    2.15  by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
    2.16 -     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
    2.17 +     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
    2.18  
    2.19  lemma inorder_delete:
    2.20    "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    2.21 @@ -151,16 +151,16 @@
    2.22      qed
    2.23      moreover
    2.24      have ?case if [simp]: "x=a"
    2.25 -    proof (cases "del_min r")
    2.26 +    proof (cases "split_min r")
    2.27        case None
    2.28        show ?thesis
    2.29        proof cases
    2.30          assume "r \<in> B h"
    2.31 -        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
    2.32 +        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
    2.33        next
    2.34          assume "r \<notin> B h"
    2.35          hence "r \<in> U h" using lr by auto
    2.36 -        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    2.37 +        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
    2.38        qed
    2.39      next
    2.40        case [simp]: (Some br')
    2.41 @@ -168,12 +168,12 @@
    2.42        show ?thesis
    2.43        proof cases
    2.44          assume "r \<in> B h"
    2.45 -        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
    2.46 +        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
    2.47          show ?thesis by simp
    2.48        next
    2.49          assume "r \<notin> B h"
    2.50          hence "l \<in> B h" and "r \<in> U h" using lr by auto
    2.51 -        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
    2.52 +        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
    2.53          show ?thesis by simp
    2.54        qed
    2.55      qed
     3.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     3.3 @@ -92,14 +92,14 @@
     3.4    N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
     3.5  "n2 t1 a1 t2 = N2 t1 a1 t2"
     3.6  
     3.7 -fun del_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
     3.8 -"del_min N0 = None" |
     3.9 -"del_min (N1 t) =
    3.10 -  (case del_min t of
    3.11 +fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
    3.12 +"split_min N0 = None" |
    3.13 +"split_min (N1 t) =
    3.14 +  (case split_min t of
    3.15       None \<Rightarrow> None |
    3.16       Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
    3.17 -"del_min (N2 t1 a t2) =
    3.18 -  (case del_min t1 of
    3.19 +"split_min (N2 t1 a t2) =
    3.20 +  (case split_min t1 of
    3.21       None \<Rightarrow> Some (a, N1 t2) |
    3.22       Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
    3.23  
    3.24 @@ -110,7 +110,7 @@
    3.25    (case cmp x a of
    3.26       LT \<Rightarrow> n2 (del x l) a r |
    3.27       GT \<Rightarrow> n2 l a (del x r) |
    3.28 -     EQ \<Rightarrow> (case del_min r of
    3.29 +     EQ \<Rightarrow> (case split_min r of
    3.30                None \<Rightarrow> N1 l |
    3.31                Some (b, r') \<Rightarrow> n2 l b r'))"
    3.32  
    3.33 @@ -189,15 +189,15 @@
    3.34  lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
    3.35  by(cases "(l,a,r)" rule: n2.cases) (auto)
    3.36  
    3.37 -lemma inorder_del_min:
    3.38 -  "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
    3.39 -  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
    3.40 +lemma inorder_split_min:
    3.41 +  "t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
    3.42 +  (split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
    3.43  by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
    3.44  
    3.45  lemma inorder_del:
    3.46    "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    3.47  by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
    3.48 -     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
    3.49 +     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
    3.50  
    3.51  lemma inorder_delete:
    3.52    "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    3.53 @@ -331,15 +331,15 @@
    3.54  apply(erule exE bexE conjE imageE | simp | erule disjE)+
    3.55  done
    3.56  
    3.57 -lemma del_minNoneN0: "\<lbrakk>t \<in> B h; del_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
    3.58 +lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
    3.59  by (cases t) (auto split: option.splits)
    3.60  
    3.61 -lemma del_minNoneN1 : "\<lbrakk>t \<in> U h; del_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
    3.62 -by (cases h) (auto simp: del_minNoneN0  split: option.splits)
    3.63 +lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
    3.64 +by (cases h) (auto simp: split_minNoneN0  split: option.splits)
    3.65  
    3.66 -lemma del_min_type:
    3.67 -  "t \<in> B h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
    3.68 -  "t \<in> U h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
    3.69 +lemma split_min_type:
    3.70 +  "t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
    3.71 +  "t \<in> U h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
    3.72  proof (induction h arbitrary: t a t')
    3.73    case (Suc h)
    3.74    { case 1
    3.75 @@ -347,12 +347,12 @@
    3.76        t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
    3.77        by auto
    3.78      show ?case
    3.79 -    proof (cases "del_min t1")
    3.80 +    proof (cases "split_min t1")
    3.81        case None
    3.82        show ?thesis
    3.83        proof cases
    3.84          assume "t1 \<in> B h"
    3.85 -        with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
    3.86 +        with split_minNoneN0[OF this None] 1 show ?thesis by(auto)
    3.87        next
    3.88          assume "t1 \<notin> B h"
    3.89          thus ?thesis using 1 None by (auto)
    3.90 @@ -376,9 +376,9 @@
    3.91    { case 2
    3.92      then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
    3.93      show ?case
    3.94 -    proof (cases "del_min t1")
    3.95 +    proof (cases "split_min t1")
    3.96        case None
    3.97 -      with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
    3.98 +      with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
    3.99      next
   3.100        case [simp]: (Some bt')
   3.101        obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
   3.102 @@ -421,16 +421,16 @@
   3.103      qed
   3.104      moreover
   3.105      have ?case if [simp]: "x=a"
   3.106 -    proof (cases "del_min r")
   3.107 +    proof (cases "split_min r")
   3.108        case None
   3.109        show ?thesis
   3.110        proof cases
   3.111          assume "r \<in> B h"
   3.112 -        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   3.113 +        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
   3.114        next
   3.115          assume "r \<notin> B h"
   3.116          hence "r \<in> U h" using lr by auto
   3.117 -        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   3.118 +        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   3.119        qed
   3.120      next
   3.121        case [simp]: (Some br')
   3.122 @@ -438,12 +438,12 @@
   3.123        show ?thesis
   3.124        proof cases
   3.125          assume "r \<in> B h"
   3.126 -        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   3.127 +        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
   3.128          show ?thesis by simp
   3.129        next
   3.130          assume "r \<notin> B h"
   3.131          hence "l \<in> B h" and "r \<in> U h" using lr by auto
   3.132 -        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   3.133 +        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   3.134          show ?thesis by simp
   3.135        qed
   3.136      qed
     4.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Fri Apr 20 22:22:46 2018 +0200
     4.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
     4.3 @@ -67,9 +67,9 @@
     4.4  definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
     4.5  "insert x t = merge (Node 1 Leaf x Leaf) t"
     4.6  
     4.7 -fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
     4.8 -"del_min Leaf = Leaf" |
     4.9 -"del_min (Node n l x r) = merge l r"
    4.10 +fun split_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
    4.11 +"split_min Leaf = Leaf" |
    4.12 +"split_min (Node n l x r) = merge l r"
    4.13  
    4.14  
    4.15  subsection "Lemmas"
    4.16 @@ -99,7 +99,7 @@
    4.17  lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
    4.18  by (induction h) (auto simp add: eq_Min_iff)
    4.19  
    4.20 -lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
    4.21 +lemma mset_split_min: "mset_tree (split_min h) = mset_tree h - {# get_min h #}"
    4.22  by (cases h) (auto simp: mset_merge)
    4.23  
    4.24  lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
    4.25 @@ -130,10 +130,10 @@
    4.26  lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
    4.27  by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
    4.28  
    4.29 -lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
    4.30 +lemma ltree_split_min: "ltree t \<Longrightarrow> ltree(split_min t)"
    4.31  by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
    4.32  
    4.33 -lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
    4.34 +lemma heap_split_min: "heap t \<Longrightarrow> heap(split_min t)"
    4.35  by(cases t)(auto simp add: heap_merge simp del: merge.simps)
    4.36  
    4.37  text \<open>Last step of functional correctness proof: combine all the above lemmas
    4.38 @@ -141,7 +141,7 @@
    4.39  
    4.40  interpretation lheap: Priority_Queue_Merge
    4.41  where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
    4.42 -and insert = insert and del_min = del_min
    4.43 +and insert = insert and split_min = split_min
    4.44  and get_min = get_min and merge = merge
    4.45  and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
    4.46  proof(standard, goal_cases)
    4.47 @@ -151,7 +151,7 @@
    4.48  next
    4.49    case 3 show ?case by(rule mset_insert)
    4.50  next
    4.51 -  case 4 show ?case by(rule mset_del_min)
    4.52 +  case 4 show ?case by(rule mset_split_min)
    4.53  next
    4.54    case 5 thus ?case by(simp add: get_min mset_tree_empty)
    4.55  next
    4.56 @@ -159,7 +159,7 @@
    4.57  next
    4.58    case 7 thus ?case by(simp add: heap_insert ltree_insert)
    4.59  next
    4.60 -  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
    4.61 +  case 8 thus ?case by(simp add: heap_split_min ltree_split_min)
    4.62  next
    4.63    case 9 thus ?case by (simp add: mset_merge)
    4.64  next
    4.65 @@ -196,9 +196,9 @@
    4.66  definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
    4.67  "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
    4.68  
    4.69 -fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
    4.70 -"t_del_min Leaf = 1" |
    4.71 -"t_del_min (Node n l a r) = t_merge l r"
    4.72 +fun t_split_min :: "'a::ord lheap \<Rightarrow> nat" where
    4.73 +"t_split_min Leaf = 1" |
    4.74 +"t_split_min (Node n l a r) = t_merge l r"
    4.75  
    4.76  lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
    4.77  proof(induction l r rule: merge.induct)
    4.78 @@ -229,13 +229,13 @@
    4.79    finally show ?thesis by simp
    4.80  qed
    4.81  
    4.82 -corollary t_del_min_log: assumes "ltree t"
    4.83 -  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
    4.84 +corollary t_split_min_log: assumes "ltree t"
    4.85 +  shows "t_split_min t \<le> 2 * log 2 (size1 t) + 1"
    4.86  proof(cases t)
    4.87    case Leaf thus ?thesis using assms by simp
    4.88  next
    4.89    case [simp]: (Node _ t1 _ t2)
    4.90 -  have "t_del_min t = t_merge t1 t2" by simp
    4.91 +  have "t_split_min t = t_merge t1 t2" by simp
    4.92    also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
    4.93      using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
    4.94    also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
     5.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Fri Apr 20 22:22:46 2018 +0200
     5.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Sat Apr 21 08:41:42 2018 +0200
     5.3 @@ -13,18 +13,18 @@
     5.4  and is_empty :: "'q \<Rightarrow> bool"
     5.5  and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
     5.6  and get_min :: "'q \<Rightarrow> 'a"
     5.7 -and del_min :: "'q \<Rightarrow> 'q"
     5.8 +and split_min :: "'q \<Rightarrow> 'q"
     5.9  and invar :: "'q \<Rightarrow> bool"
    5.10  and mset :: "'q \<Rightarrow> 'a multiset"
    5.11  assumes mset_empty: "mset empty = {#}"
    5.12  and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
    5.13  and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
    5.14 -and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    5.15 -    mset (del_min q) = mset q - {# get_min q #}"
    5.16 +and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    5.17 +    mset (split_min q) = mset q - {# get_min q #}"
    5.18  and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
    5.19  and invar_empty: "invar empty"
    5.20  and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
    5.21 -and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
    5.22 +and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
    5.23  
    5.24  text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
    5.25  
     6.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Fri Apr 20 22:22:46 2018 +0200
     6.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sat Apr 21 08:41:42 2018 +0200
     6.3 @@ -88,23 +88,23 @@
     6.4  "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
     6.5    LT \<Rightarrow> node21 (del x l) ab1 r |
     6.6    GT \<Rightarrow> node22 l ab1 (del x r) |
     6.7 -  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
     6.8 +  EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" |
     6.9  "del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
    6.10    LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
    6.11 -  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
    6.12 +  EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r |
    6.13    GT \<Rightarrow> (case cmp x (fst ab2) of
    6.14             LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
    6.15 -           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
    6.16 +           EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' |
    6.17             GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
    6.18  "del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
    6.19    LT \<Rightarrow> (case cmp x (fst ab1) of
    6.20             LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
    6.21 -           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
    6.22 +           EQ \<Rightarrow> let (ab',t2') = split_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
    6.23             GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
    6.24 -  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
    6.25 +  EQ \<Rightarrow> let (ab',t3') = split_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
    6.26    GT \<Rightarrow> (case cmp x (fst ab3) of
    6.27            LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
    6.28 -          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
    6.29 +          EQ \<Rightarrow> let (ab',t4') = split_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
    6.30            GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
    6.31  
    6.32  definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
    6.33 @@ -130,7 +130,7 @@
    6.34  lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    6.35    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    6.36  by(induction t rule: del.induct)
    6.37 -  (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits)
    6.38 +  (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits)
    6.39  (* 30 secs (2016) *)
    6.40  
    6.41  lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    6.42 @@ -148,11 +148,11 @@
    6.43  
    6.44  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    6.45  by(induction x t rule: del.induct)
    6.46 -  (auto simp add: heights height_del_min split!: if_split prod.split)
    6.47 +  (auto simp add: heights height_split_min split!: if_split prod.split)
    6.48  
    6.49  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    6.50  by(induction x t rule: del.induct)
    6.51 -  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
    6.52 +  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
    6.53  
    6.54  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    6.55  by(simp add: delete_def bal_tree\<^sub>d_del)
     7.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     7.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     7.3 @@ -154,13 +154,13 @@
     7.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))" |
     7.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))"
     7.6  
     7.7 -fun del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
     7.8 -"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
     7.9 -"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    7.10 -"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
    7.11 -"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    7.12 -"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
    7.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))"
    7.14 +fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
    7.15 +"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
    7.16 +"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    7.17 +"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
    7.18 +"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
    7.19 +"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" |
    7.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))"
    7.21  
    7.22  fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
    7.23  "del k Leaf = T\<^sub>d Leaf" |
    7.24 @@ -175,23 +175,23 @@
    7.25  "del k (Node2 l a r) = (case cmp k a of
    7.26    LT \<Rightarrow> node21 (del k l) a r |
    7.27    GT \<Rightarrow> node22 l a (del k r) |
    7.28 -  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
    7.29 +  EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
    7.30  "del k (Node3 l a m b r) = (case cmp k a of
    7.31    LT \<Rightarrow> node31 (del k l) a m b r |
    7.32 -  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
    7.33 +  EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
    7.34    GT \<Rightarrow> (case cmp k b of
    7.35             LT \<Rightarrow> node32 l a (del k m) b r |
    7.36 -           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
    7.37 +           EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
    7.38             GT \<Rightarrow> node33 l a m b (del k r)))" |
    7.39  "del k (Node4 l a m b n c r) = (case cmp k b of
    7.40    LT \<Rightarrow> (case cmp k a of
    7.41            LT \<Rightarrow> node41 (del k l) a m b n c r |
    7.42 -          EQ \<Rightarrow> let (a',m') = del_min m in node42 l a' m' b n c r |
    7.43 +          EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r |
    7.44            GT \<Rightarrow> node42 l a (del k m) b n c r) |
    7.45 -  EQ \<Rightarrow> let (b',n') = del_min n in node43 l a m b' n' c r |
    7.46 +  EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r |
    7.47    GT \<Rightarrow> (case cmp k c of
    7.48             LT \<Rightarrow> node43 l a m b (del k n) c r |
    7.49 -           EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
    7.50 +           EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' |
    7.51             GT \<Rightarrow> node44 l a m b n c (del k r)))"
    7.52  
    7.53  definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
    7.54 @@ -259,16 +259,16 @@
    7.55    inorder_node31 inorder_node32 inorder_node33
    7.56    inorder_node41 inorder_node42 inorder_node43 inorder_node44
    7.57  
    7.58 -lemma del_minD:
    7.59 -  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    7.60 +lemma split_minD:
    7.61 +  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    7.62    x # inorder(tree\<^sub>d t') = inorder t"
    7.63 -by(induction t arbitrary: t' rule: del_min.induct)
    7.64 +by(induction t arbitrary: t' rule: split_min.induct)
    7.65    (auto simp: inorder_nodes split: prod.splits)
    7.66  
    7.67  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    7.68    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    7.69  by(induction t rule: del.induct)
    7.70 -  (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
    7.71 +  (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits)
    7.72    (* 30 secs (2016) *)
    7.73  
    7.74  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    7.75 @@ -476,23 +476,23 @@
    7.76    height_node31 height_node32 height_node33
    7.77    height_node41 height_node42 height_node43 height_node44
    7.78  
    7.79 -lemma height_del_min:
    7.80 -  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    7.81 -by(induct t arbitrary: x t' rule: del_min.induct)
    7.82 +lemma height_split_min:
    7.83 +  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    7.84 +by(induct t arbitrary: x t' rule: split_min.induct)
    7.85    (auto simp: heights split: prod.splits)
    7.86  
    7.87  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    7.88  by(induction x t rule: del.induct)
    7.89 -  (auto simp add: heights height_del_min split!: if_split prod.split)
    7.90 +  (auto simp add: heights height_split_min split!: if_split prod.split)
    7.91  
    7.92 -lemma bal_del_min:
    7.93 -  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    7.94 -by(induct t arbitrary: x t' rule: del_min.induct)
    7.95 -  (auto simp: heights height_del_min bals split: prod.splits)
    7.96 +lemma bal_split_min:
    7.97 +  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    7.98 +by(induct t arbitrary: x t' rule: split_min.induct)
    7.99 +  (auto simp: heights height_split_min bals split: prod.splits)
   7.100  
   7.101  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   7.102  by(induction x t rule: del.induct)
   7.103 -  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
   7.104 +  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
   7.105  
   7.106  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   7.107  by(simp add: delete_def bal_tree\<^sub>d_del)
     8.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Fri Apr 20 22:22:46 2018 +0200
     8.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sat Apr 21 08:41:42 2018 +0200
     8.3 @@ -57,13 +57,13 @@
     8.4  "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
     8.5    LT \<Rightarrow> node21 (del x l) ab1 r |
     8.6    GT \<Rightarrow> node22 l ab1 (del x r) |
     8.7 -  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
     8.8 +  EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" |
     8.9  "del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
    8.10    LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
    8.11 -  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
    8.12 +  EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r |
    8.13    GT \<Rightarrow> (case cmp x (fst ab2) of
    8.14             LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
    8.15 -           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
    8.16 +           EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' |
    8.17             GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
    8.18  
    8.19  definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    8.20 @@ -89,7 +89,7 @@
    8.21  lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    8.22    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    8.23  by(induction t rule: del.induct)
    8.24 -  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
    8.25 +  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    8.26  
    8.27  corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
    8.28    inorder(delete x t) = del_list x (inorder t)"
    8.29 @@ -107,11 +107,11 @@
    8.30  
    8.31  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    8.32  by(induction x t rule: del.induct)
    8.33 -  (auto simp add: heights max_def height_del_min split: prod.split)
    8.34 +  (auto simp add: heights max_def height_split_min split: prod.split)
    8.35  
    8.36  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    8.37  by(induction x t rule: del.induct)
    8.38 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
    8.39 +  (auto simp: bals bal_split_min height_del height_split_min split: prod.split)
    8.40  
    8.41  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    8.42  by(simp add: delete_def bal_tree\<^sub>d_del)
     9.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Fri Apr 20 22:22:46 2018 +0200
     9.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sat Apr 21 08:41:42 2018 +0200
     9.3 @@ -102,13 +102,13 @@
     9.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))" |
     9.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))"
     9.6  
     9.7 -fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
     9.8 -"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
     9.9 -"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    9.10 -"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    9.11 -"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
    9.12 +fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
    9.13 +"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
    9.14 +"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    9.15 +"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
    9.16 +"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
    9.17  
    9.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>,
    9.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>,
    9.20  in which case balancedness implies that so are the others. Exercise.\<close>
    9.21  
    9.22  fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    9.23 @@ -123,15 +123,15 @@
    9.24    (case cmp x a of
    9.25       LT \<Rightarrow> node21 (del x l) a r |
    9.26       GT \<Rightarrow> node22 l a (del x r) |
    9.27 -     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
    9.28 +     EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
    9.29  "del x (Node3 l a m b r) =
    9.30    (case cmp x a of
    9.31       LT \<Rightarrow> node31 (del x l) a m b r |
    9.32 -     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
    9.33 +     EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
    9.34       GT \<Rightarrow>
    9.35         (case cmp x b of
    9.36            LT \<Rightarrow> node32 l a (del x m) b r |
    9.37 -          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
    9.38 +          EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
    9.39            GT \<Rightarrow> node33 l a m b (del x r)))"
    9.40  
    9.41  definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    9.42 @@ -182,16 +182,16 @@
    9.43  lemmas inorder_nodes = inorder_node21 inorder_node22
    9.44    inorder_node31 inorder_node32 inorder_node33
    9.45  
    9.46 -lemma del_minD:
    9.47 -  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    9.48 +lemma split_minD:
    9.49 +  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
    9.50    x # inorder(tree\<^sub>d t') = inorder t"
    9.51 -by(induction t arbitrary: t' rule: del_min.induct)
    9.52 +by(induction t arbitrary: t' rule: split_min.induct)
    9.53    (auto simp: inorder_nodes split: prod.splits)
    9.54  
    9.55  lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    9.56    inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
    9.57  by(induction t rule: del.induct)
    9.58 -  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
    9.59 +  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
    9.60  
    9.61  lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    9.62    inorder(delete x t) = del_list x (inorder t)"
    9.63 @@ -350,23 +350,23 @@
    9.64  lemmas heights = height'_node21 height'_node22
    9.65    height'_node31 height'_node32 height'_node33
    9.66  
    9.67 -lemma height_del_min:
    9.68 -  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    9.69 -by(induct t arbitrary: x t' rule: del_min.induct)
    9.70 +lemma height_split_min:
    9.71 +  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
    9.72 +by(induct t arbitrary: x t' rule: split_min.induct)
    9.73    (auto simp: heights split: prod.splits)
    9.74  
    9.75  lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
    9.76  by(induction x t rule: del.induct)
    9.77 -  (auto simp: heights max_def height_del_min split: prod.splits)
    9.78 +  (auto simp: heights max_def height_split_min split: prod.splits)
    9.79  
    9.80 -lemma bal_del_min:
    9.81 -  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    9.82 -by(induct t arbitrary: x t' rule: del_min.induct)
    9.83 -  (auto simp: heights height_del_min bals split: prod.splits)
    9.84 +lemma bal_split_min:
    9.85 +  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
    9.86 +by(induct t arbitrary: x t' rule: split_min.induct)
    9.87 +  (auto simp: heights height_split_min bals split: prod.splits)
    9.88  
    9.89  lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
    9.90  by(induction x t rule: del.induct)
    9.91 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
    9.92 +  (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
    9.93  
    9.94  corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
    9.95  by(simp add: delete_def bal_tree\<^sub>d_del)
    10.1 --- a/src/HOL/Data_Structures/Tree_Map.thy	Fri Apr 20 22:22:46 2018 +0200
    10.2 +++ b/src/HOL/Data_Structures/Tree_Map.thy	Sat Apr 21 08:41:42 2018 +0200
    10.3 @@ -25,7 +25,7 @@
    10.4  "delete x (Node l (a,b) r) = (case cmp x a of
    10.5    LT \<Rightarrow> Node (delete x l) (a,b) r |
    10.6    GT \<Rightarrow> Node l (a,b) (delete x r) |
    10.7 -  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
    10.8 +  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = split_min r in Node l ab' r')"
    10.9  
   10.10  
   10.11  subsection "Functional Correctness Proofs"
   10.12 @@ -40,7 +40,7 @@
   10.13  
   10.14  lemma inorder_delete:
   10.15    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
   10.16 -by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
   10.17 +by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
   10.18  
   10.19  interpretation Map_by_Ordered
   10.20  where empty = Leaf and lookup = lookup and update = update and delete = delete
    11.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Apr 20 22:22:46 2018 +0200
    11.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Sat Apr 21 08:41:42 2018 +0200
    11.3 @@ -27,9 +27,9 @@
    11.4       EQ \<Rightarrow> Node l a r |
    11.5       GT \<Rightarrow> Node l a (insert x r))"
    11.6  
    11.7 -fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
    11.8 -"del_min (Node l a r) =
    11.9 -  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
   11.10 +fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
   11.11 +"split_min (Node l a r) =
   11.12 +  (if l = Leaf then (a,r) else let (x,l') = split_min l in (x, Node l' a r))"
   11.13  
   11.14  fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   11.15  "delete x Leaf = Leaf" |
   11.16 @@ -37,7 +37,7 @@
   11.17    (case cmp x a of
   11.18       LT \<Rightarrow>  Node (delete x l) a r |
   11.19       GT \<Rightarrow>  Node l a (delete x r) |
   11.20 -     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
   11.21 +     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = split_min r in Node l a' r')"
   11.22  
   11.23  
   11.24  subsection "Functional Correctness Proofs"
   11.25 @@ -50,14 +50,14 @@
   11.26  by(induction t) (auto simp: ins_list_simps)
   11.27  
   11.28  
   11.29 -lemma del_minD:
   11.30 -  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
   11.31 -by(induction t arbitrary: t' rule: del_min.induct)
   11.32 +lemma split_minD:
   11.33 +  "split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
   11.34 +by(induction t arbitrary: t' rule: split_min.induct)
   11.35    (auto simp: sorted_lems split: prod.splits if_splits)
   11.36  
   11.37  lemma inorder_delete:
   11.38    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
   11.39 -by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
   11.40 +by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
   11.41  
   11.42  interpretation Set_by_Ordered
   11.43  where empty = Leaf and isin = isin and insert = insert and delete = delete