--- 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
--- 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
--- 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
--- 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"
--- 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>
--- 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)
--- 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)
--- 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)
--- 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)
--- 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
--- 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