author nipkow Sat Apr 21 08:41:42 2018 +0200 (13 months ago) changeset 68020 6aade817bee5 parent 68019 32d19862781b child 68021 b91a043c0dcb
del_min -> split_min
```     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)"
```
```     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)"
```
```     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)"
```
```     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)"
```
```    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
```