# HG changeset patch
# User nipkow
# Date 1524292902 -7200
# Node ID 6aade817bee5b829ddd4972a051a94cfbb0d660a
# Parent  32d19862781b2371488b865339bae2014c97b945
del_min -> split_min

diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -353,18 +353,18 @@
 using assms
 by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
 
-subsubsection \<open>\<open>del_min\<close>\<close>
+subsubsection \<open>\<open>split_min\<close>\<close>
 
-definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
-"del_min ts = (case get_min_rest ts of
+definition split_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
+"split_min ts = (case get_min_rest ts of
    (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
 
-lemma invar_del_min[simp]:
+lemma invar_split_min[simp]:
   assumes "ts \<noteq> []"
   assumes "invar ts"
-  shows "invar (del_min ts)"
+  shows "invar (split_min ts)"
 using assms
-unfolding invar_def del_min_def
+unfolding invar_def split_min_def
 by (auto
       split: prod.split tree.split
       intro!: invar_bheap_merge invar_oheap_merge
@@ -372,11 +372,11 @@
       intro!: invar_oheap_children invar_bheap_children
     )
 
-lemma mset_heap_del_min:
+lemma mset_heap_split_min:
   assumes "ts \<noteq> []"
-  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
+  shows "mset_heap ts = mset_heap (split_min ts) + {# get_min ts #}"
 using assms
-unfolding del_min_def
+unfolding split_min_def
 apply (clarsimp split: tree.split prod.split)
 apply (frule (1) get_min_rest_get_min_same_root)
 apply (frule (1) mset_get_min_rest)
@@ -391,7 +391,7 @@
 
 interpretation binheap: Priority_Queue_Merge
   where empty = "[]" and is_empty = "(=) []" and insert = insert
-  and get_min = get_min and del_min = del_min and merge = merge
+  and get_min = get_min and split_min = split_min and merge = merge
   and invar = invar and mset = mset_heap
 proof (unfold_locales, goal_cases)
   case 1 thus ?case by simp
@@ -401,7 +401,7 @@
   case 3 thus ?case by auto
 next
   case (4 q)
-  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>]
+  thus ?case using mset_heap_split_min[of q] get_min[OF _ \<open>invar q\<close>]
     by (auto simp: union_single_eq_diff)
 next
   case (5 q) thus ?case using get_min[of q] by auto
@@ -603,7 +603,7 @@
   finally show ?thesis by auto
 qed
 
-subsubsection \<open>\<open>t_del_min\<close>\<close>
+subsubsection \<open>\<open>t_split_min\<close>\<close>
 
 fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
   "t_get_min_rest [t] = 1"
@@ -639,8 +639,8 @@
 
 definition "t_rev xs = length xs + 1"
 
-definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where
-  "t_del_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
+definition t_split_min :: "'a::linorder heap \<Rightarrow> nat" where
+  "t_split_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
                     \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
   )"
 
@@ -661,12 +661,12 @@
   finally show ?thesis by (auto simp: algebra_simps)
 qed
 
-lemma t_del_min_bound_aux:
+lemma t_split_min_bound_aux:
   fixes ts
   defines "n \<equiv> size (mset_heap ts)"
   assumes BINVAR: "invar_bheap ts"
   assumes "ts\<noteq>[]"
-  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
 proof -
   obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
     by (metis surj_pair tree.exhaust_sel)
@@ -687,8 +687,8 @@
     finally show ?thesis by (auto simp: algebra_simps)
   qed
 
-  have "t_del_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
-    unfolding t_del_min_def by (simp add: GM)
+  have "t_split_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
+    unfolding t_split_min_def by (simp add: GM)
   also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
     using t_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
   also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
@@ -700,17 +700,17 @@
     unfolding n\<^sub>1_def n\<^sub>2_def n_def
     using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
     by (auto simp: mset_heap_def)
-  finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+  finally have "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
     by auto
   thus ?thesis by (simp add: algebra_simps)
 qed
 
-lemma t_del_min_bound:
+lemma t_split_min_bound:
   fixes ts
   defines "n \<equiv> size (mset_heap ts)"
   assumes "invar ts"
   assumes "ts\<noteq>[]"
-  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
-using assms t_del_min_bound_aux unfolding invar_def by blast
+  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
+using assms t_split_min_bound_aux unfolding invar_def by blast
 
 end
\ No newline at end of file
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Brother12_Map.thy
--- a/src/HOL/Data_Structures/Brother12_Map.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -44,7 +44,7 @@
   (case cmp x a of
      LT \<Rightarrow> n2 (del x l) (a,b) r |
      GT \<Rightarrow> n2 l (a,b) (del x r) |
-     EQ \<Rightarrow> (case del_min r of
+     EQ \<Rightarrow> (case split_min r of
               None \<Rightarrow> N1 l |
               Some (ab, r') \<Rightarrow> n2 l ab r'))"
 
@@ -84,7 +84,7 @@
 lemma inorder_del:
   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
 by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
-     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
+     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
 
 lemma inorder_delete:
   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
@@ -151,16 +151,16 @@
     qed
     moreover
     have ?case if [simp]: "x=a"
-    proof (cases "del_min r")
+    proof (cases "split_min r")
       case None
       show ?thesis
       proof cases
         assume "r \<in> B h"
-        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
+        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
       next
         assume "r \<notin> B h"
         hence "r \<in> U h" using lr by auto
-        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
+        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
       qed
     next
       case [simp]: (Some br')
@@ -168,12 +168,12 @@
       show ?thesis
       proof cases
         assume "r \<in> B h"
-        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
+        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
         show ?thesis by simp
       next
         assume "r \<notin> B h"
         hence "l \<in> B h" and "r \<in> U h" using lr by auto
-        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
+        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
         show ?thesis by simp
       qed
     qed
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -92,14 +92,14 @@
   N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
 "n2 t1 a1 t2 = N2 t1 a1 t2"
 
-fun del_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
-"del_min N0 = None" |
-"del_min (N1 t) =
-  (case del_min t of
+fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
+"split_min N0 = None" |
+"split_min (N1 t) =
+  (case split_min t of
      None \<Rightarrow> None |
      Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
-"del_min (N2 t1 a t2) =
-  (case del_min t1 of
+"split_min (N2 t1 a t2) =
+  (case split_min t1 of
      None \<Rightarrow> Some (a, N1 t2) |
      Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
 
@@ -110,7 +110,7 @@
   (case cmp x a of
      LT \<Rightarrow> n2 (del x l) a r |
      GT \<Rightarrow> n2 l a (del x r) |
-     EQ \<Rightarrow> (case del_min r of
+     EQ \<Rightarrow> (case split_min r of
               None \<Rightarrow> N1 l |
               Some (b, r') \<Rightarrow> n2 l b r'))"
 
@@ -189,15 +189,15 @@
 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
 by(cases "(l,a,r)" rule: n2.cases) (auto)
 
-lemma inorder_del_min:
-  "t \<in> T h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
-  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
+lemma inorder_split_min:
+  "t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
+  (split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
 by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
 
 lemma inorder_del:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
 by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
-     inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
+     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
 
 lemma inorder_delete:
   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
@@ -331,15 +331,15 @@
 apply(erule exE bexE conjE imageE | simp | erule disjE)+
 done
 
-lemma del_minNoneN0: "\<lbrakk>t \<in> B h; del_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
+lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
 by (cases t) (auto split: option.splits)
 
-lemma del_minNoneN1 : "\<lbrakk>t \<in> U h; del_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
-by (cases h) (auto simp: del_minNoneN0  split: option.splits)
+lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
+by (cases h) (auto simp: split_minNoneN0  split: option.splits)
 
-lemma del_min_type:
-  "t \<in> B h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
-  "t \<in> U h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
+lemma split_min_type:
+  "t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
+  "t \<in> U h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
 proof (induction h arbitrary: t a t')
   case (Suc h)
   { case 1
@@ -347,12 +347,12 @@
       t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
       by auto
     show ?case
-    proof (cases "del_min t1")
+    proof (cases "split_min t1")
       case None
       show ?thesis
       proof cases
         assume "t1 \<in> B h"
-        with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
+        with split_minNoneN0[OF this None] 1 show ?thesis by(auto)
       next
         assume "t1 \<notin> B h"
         thus ?thesis using 1 None by (auto)
@@ -376,9 +376,9 @@
   { case 2
     then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
     show ?case
-    proof (cases "del_min t1")
+    proof (cases "split_min t1")
       case None
-      with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
+      with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
     next
       case [simp]: (Some bt')
       obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
@@ -421,16 +421,16 @@
     qed
     moreover
     have ?case if [simp]: "x=a"
-    proof (cases "del_min r")
+    proof (cases "split_min r")
       case None
       show ?thesis
       proof cases
         assume "r \<in> B h"
-        with del_minNoneN0[OF this None] lr show ?thesis by(simp)
+        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
       next
         assume "r \<notin> B h"
         hence "r \<in> U h" using lr by auto
-        with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
+        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
       qed
     next
       case [simp]: (Some br')
@@ -438,12 +438,12 @@
       show ?thesis
       proof cases
         assume "r \<in> B h"
-        from del_min_type(1)[OF this] n2_type3[OF lr(1)]
+        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
         show ?thesis by simp
       next
         assume "r \<notin> B h"
         hence "l \<in> B h" and "r \<in> U h" using lr by auto
-        from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
+        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
         show ?thesis by simp
       qed
     qed
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -67,9 +67,9 @@
 definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "insert x t = merge (Node 1 Leaf x Leaf) t"
 
-fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
-"del_min Leaf = Leaf" |
-"del_min (Node n l x r) = merge l r"
+fun split_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
+"split_min Leaf = Leaf" |
+"split_min (Node n l x r) = merge l r"
 
 
 subsection "Lemmas"
@@ -99,7 +99,7 @@
 lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
 by (induction h) (auto simp add: eq_Min_iff)
 
-lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
+lemma mset_split_min: "mset_tree (split_min h) = mset_tree h - {# get_min h #}"
 by (cases h) (auto simp: mset_merge)
 
 lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
@@ -130,10 +130,10 @@
 lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
 by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
 
-lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
+lemma ltree_split_min: "ltree t \<Longrightarrow> ltree(split_min t)"
 by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
 
-lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
+lemma heap_split_min: "heap t \<Longrightarrow> heap(split_min t)"
 by(cases t)(auto simp add: heap_merge simp del: merge.simps)
 
 text \<open>Last step of functional correctness proof: combine all the above lemmas
@@ -141,7 +141,7 @@
 
 interpretation lheap: Priority_Queue_Merge
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
-and insert = insert and del_min = del_min
+and insert = insert and split_min = split_min
 and get_min = get_min and merge = merge
 and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
 proof(standard, goal_cases)
@@ -151,7 +151,7 @@
 next
   case 3 show ?case by(rule mset_insert)
 next
-  case 4 show ?case by(rule mset_del_min)
+  case 4 show ?case by(rule mset_split_min)
 next
   case 5 thus ?case by(simp add: get_min mset_tree_empty)
 next
@@ -159,7 +159,7 @@
 next
   case 7 thus ?case by(simp add: heap_insert ltree_insert)
 next
-  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+  case 8 thus ?case by(simp add: heap_split_min ltree_split_min)
 next
   case 9 thus ?case by (simp add: mset_merge)
 next
@@ -196,9 +196,9 @@
 definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
 "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
 
-fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
-"t_del_min Leaf = 1" |
-"t_del_min (Node n l a r) = t_merge l r"
+fun t_split_min :: "'a::ord lheap \<Rightarrow> nat" where
+"t_split_min Leaf = 1" |
+"t_split_min (Node n l a r) = t_merge l r"
 
 lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
 proof(induction l r rule: merge.induct)
@@ -229,13 +229,13 @@
   finally show ?thesis by simp
 qed
 
-corollary t_del_min_log: assumes "ltree t"
-  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
+corollary t_split_min_log: assumes "ltree t"
+  shows "t_split_min t \<le> 2 * log 2 (size1 t) + 1"
 proof(cases t)
   case Leaf thus ?thesis using assms by simp
 next
   case [simp]: (Node _ t1 _ t2)
-  have "t_del_min t = t_merge t1 t2" by simp
+  have "t_split_min t = t_merge t1 t2" by simp
   also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
     using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
   also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Priority_Queue.thy
--- a/src/HOL/Data_Structures/Priority_Queue.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Priority_Queue.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -13,18 +13,18 @@
 and is_empty :: "'q \<Rightarrow> bool"
 and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
 and get_min :: "'q \<Rightarrow> 'a"
-and del_min :: "'q \<Rightarrow> 'q"
+and split_min :: "'q \<Rightarrow> 'q"
 and invar :: "'q \<Rightarrow> bool"
 and mset :: "'q \<Rightarrow> 'a multiset"
 assumes mset_empty: "mset empty = {#}"
 and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
 and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
-and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
-    mset (del_min q) = mset q - {# get_min q #}"
+and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
+    mset (split_min q) = mset q - {# get_min q #}"
 and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
 and invar_empty: "invar empty"
 and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
-and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
 
 text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
 
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -88,23 +88,23 @@
 "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
   LT \<Rightarrow> node21 (del x l) ab1 r |
   GT \<Rightarrow> node22 l ab1 (del x r) |
-  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
+  EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" |
 "del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
   LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
-  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
+  EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r |
   GT \<Rightarrow> (case cmp x (fst ab2) of
            LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
-           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
+           EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' |
            GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
 "del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
   LT \<Rightarrow> (case cmp x (fst ab1) of
            LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
-           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
+           EQ \<Rightarrow> let (ab',t2') = split_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
            GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
-  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
+  EQ \<Rightarrow> let (ab',t3') = split_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
   GT \<Rightarrow> (case cmp x (fst ab3) of
           LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
-          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
+          EQ \<Rightarrow> let (ab',t4') = split_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
           GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
 
 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
@@ -130,7 +130,7 @@
 lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
-  (auto simp: del_list_simps inorder_nodes del_minD split!: if_splits prod.splits)
+  (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits)
 (* 30 secs (2016) *)
 
 lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
@@ -148,11 +148,11 @@
 
 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
-  (auto simp add: heights height_del_min split!: if_split prod.split)
+  (auto simp add: heights height_split_min split!: if_split prod.split)
 
 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
+  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
 
 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
 by(simp add: delete_def bal_tree\<^sub>d_del)
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree234_Set.thy
--- a/src/HOL/Data_Structures/Tree234_Set.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree234_Set.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -154,13 +154,13 @@
 "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))" |
 "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))"
 
-fun del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
-"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
-"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
-"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
-"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
-"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" |
-"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))"
+fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
+"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
+"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
+"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
+"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
+"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" |
+"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))"
 
 fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
 "del k Leaf = T\<^sub>d Leaf" |
@@ -175,23 +175,23 @@
 "del k (Node2 l a r) = (case cmp k a of
   LT \<Rightarrow> node21 (del k l) a r |
   GT \<Rightarrow> node22 l a (del k r) |
-  EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+  EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
 "del k (Node3 l a m b r) = (case cmp k a of
   LT \<Rightarrow> node31 (del k l) a m b r |
-  EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+  EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
   GT \<Rightarrow> (case cmp k b of
            LT \<Rightarrow> node32 l a (del k m) b r |
-           EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+           EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
            GT \<Rightarrow> node33 l a m b (del k r)))" |
 "del k (Node4 l a m b n c r) = (case cmp k b of
   LT \<Rightarrow> (case cmp k a of
           LT \<Rightarrow> node41 (del k l) a m b n c r |
-          EQ \<Rightarrow> let (a',m') = del_min m in node42 l a' m' b n c r |
+          EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r |
           GT \<Rightarrow> node42 l a (del k m) b n c r) |
-  EQ \<Rightarrow> let (b',n') = del_min n in node43 l a m b' n' c r |
+  EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r |
   GT \<Rightarrow> (case cmp k c of
            LT \<Rightarrow> node43 l a m b (del k n) c r |
-           EQ \<Rightarrow> let (c',r') = del_min r in node44 l a m b n c' r' |
+           EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' |
            GT \<Rightarrow> node44 l a m b n c (del k r)))"
 
 definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
@@ -259,16 +259,16 @@
   inorder_node31 inorder_node32 inorder_node33
   inorder_node41 inorder_node42 inorder_node43 inorder_node44
 
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
+lemma split_minD:
+  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   x # inorder(tree\<^sub>d t') = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
+by(induction t arbitrary: t' rule: split_min.induct)
   (auto simp: inorder_nodes split: prod.splits)
 
 lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
-  (auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits)
+  (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits)
   (* 30 secs (2016) *)
 
 lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
@@ -476,23 +476,23 @@
   height_node31 height_node32 height_node33
   height_node41 height_node42 height_node43 height_node44
 
-lemma height_del_min:
-  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
-by(induct t arbitrary: x t' rule: del_min.induct)
+lemma height_split_min:
+  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+by(induct t arbitrary: x t' rule: split_min.induct)
   (auto simp: heights split: prod.splits)
 
 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
-  (auto simp add: heights height_del_min split!: if_split prod.split)
+  (auto simp add: heights height_split_min split!: if_split prod.split)
 
-lemma bal_del_min:
-  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights height_del_min bals split: prod.splits)
+lemma bal_split_min:
+  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+by(induct t arbitrary: x t' rule: split_min.induct)
+  (auto simp: heights height_split_min bals split: prod.splits)
 
 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split)
+  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
 
 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
 by(simp add: delete_def bal_tree\<^sub>d_del)
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree23_Map.thy
--- a/src/HOL/Data_Structures/Tree23_Map.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -57,13 +57,13 @@
 "del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
   LT \<Rightarrow> node21 (del x l) ab1 r |
   GT \<Rightarrow> node22 l ab1 (del x r) |
-  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
+  EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" |
 "del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
   LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
-  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
+  EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r |
   GT \<Rightarrow> (case cmp x (fst ab2) of
            LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
-           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
+           EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' |
            GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
 
 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
@@ -89,7 +89,7 @@
 lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
-  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
+  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
 
 corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
@@ -107,11 +107,11 @@
 
 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
-  (auto simp add: heights max_def height_del_min split: prod.split)
+  (auto simp add: heights max_def height_split_min split: prod.split)
 
 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
+  (auto simp: bals bal_split_min height_del height_split_min split: prod.split)
 
 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
 by(simp add: delete_def bal_tree\<^sub>d_del)
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -102,13 +102,13 @@
 "node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
 "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))"
 
-fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
-"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
-"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
-"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
-"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
+fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
+"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
+"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
+"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
+"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
 
-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>,
+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>,
 in which case balancedness implies that so are the others. Exercise.\<close>
 
 fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
@@ -123,15 +123,15 @@
   (case cmp x a of
      LT \<Rightarrow> node21 (del x l) a r |
      GT \<Rightarrow> node22 l a (del x r) |
-     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
+     EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
 "del x (Node3 l a m b r) =
   (case cmp x a of
      LT \<Rightarrow> node31 (del x l) a m b r |
-     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
+     EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
      GT \<Rightarrow>
        (case cmp x b of
           LT \<Rightarrow> node32 l a (del x m) b r |
-          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
+          EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
           GT \<Rightarrow> node33 l a m b (del x r)))"
 
 definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
@@ -182,16 +182,16 @@
 lemmas inorder_nodes = inorder_node21 inorder_node22
   inorder_node31 inorder_node32 inorder_node33
 
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
+lemma split_minD:
+  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   x # inorder(tree\<^sub>d t') = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
+by(induction t arbitrary: t' rule: split_min.induct)
   (auto simp: inorder_nodes split: prod.splits)
 
 lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
 by(induction t rule: del.induct)
-  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
+  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
 
 lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   inorder(delete x t) = del_list x (inorder t)"
@@ -350,23 +350,23 @@
 lemmas heights = height'_node21 height'_node22
   height'_node31 height'_node32 height'_node33
 
-lemma height_del_min:
-  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
-by(induct t arbitrary: x t' rule: del_min.induct)
+lemma height_split_min:
+  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+by(induct t arbitrary: x t' rule: split_min.induct)
   (auto simp: heights split: prod.splits)
 
 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
 by(induction x t rule: del.induct)
-  (auto simp: heights max_def height_del_min split: prod.splits)
+  (auto simp: heights max_def height_split_min split: prod.splits)
 
-lemma bal_del_min:
-  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
-by(induct t arbitrary: x t' rule: del_min.induct)
-  (auto simp: heights height_del_min bals split: prod.splits)
+lemma bal_split_min:
+  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+by(induct t arbitrary: x t' rule: split_min.induct)
+  (auto simp: heights height_split_min bals split: prod.splits)
 
 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
 by(induction x t rule: del.induct)
-  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
+  (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
 
 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
 by(simp add: delete_def bal_tree\<^sub>d_del)
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree_Map.thy
--- a/src/HOL/Data_Structures/Tree_Map.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -25,7 +25,7 @@
 "delete x (Node l (a,b) r) = (case cmp x a of
   LT \<Rightarrow> Node (delete x l) (a,b) r |
   GT \<Rightarrow> Node l (a,b) (delete x r) |
-  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"
+  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = split_min r in Node l ab' r')"
 
 
 subsection "Functional Correctness Proofs"
@@ -40,7 +40,7 @@
 
 lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
+by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
 
 interpretation Map_by_Ordered
 where empty = Leaf and lookup = lookup and update = update and delete = delete
diff -r 32d19862781b -r 6aade817bee5 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Apr 20 22:22:46 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Sat Apr 21 08:41:42 2018 +0200
@@ -27,9 +27,9 @@
      EQ \<Rightarrow> Node l a r |
      GT \<Rightarrow> Node l a (insert x r))"
 
-fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
-"del_min (Node l a r) =
-  (if l = Leaf then (a,r) else let (x,l') = del_min l in (x, Node l' a r))"
+fun split_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
+"split_min (Node l a r) =
+  (if l = Leaf then (a,r) else let (x,l') = split_min l in (x, Node l' a r))"
 
 fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "delete x Leaf = Leaf" |
@@ -37,7 +37,7 @@
   (case cmp x a of
      LT \<Rightarrow>  Node (delete x l) a r |
      GT \<Rightarrow>  Node l a (delete x r) |
-     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"
+     EQ \<Rightarrow> if r = Leaf then l else let (a',r') = split_min r in Node l a' r')"
 
 
 subsection "Functional Correctness Proofs"
@@ -50,14 +50,14 @@
 by(induction t) (auto simp: ins_list_simps)
 
 
-lemma del_minD:
-  "del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
-by(induction t arbitrary: t' rule: del_min.induct)
+lemma split_minD:
+  "split_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> x # inorder t' = inorder t"
+by(induction t arbitrary: t' rule: split_min.induct)
   (auto simp: sorted_lems split: prod.splits if_splits)
 
 lemma inorder_delete:
   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
+by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete