--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sat Apr 21 08:41:42 2018 +0200
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Sat Apr 21 11:13:35 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>split_min\<close>\<close>
+subsubsection \<open>\<open>del_min\<close>\<close>
-definition split_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
-"split_min ts = (case get_min_rest ts of
+definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
+"del_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_split_min[simp]:
+lemma invar_del_min[simp]:
assumes "ts \<noteq> []"
assumes "invar ts"
- shows "invar (split_min ts)"
+ shows "invar (del_min ts)"
using assms
-unfolding invar_def split_min_def
+unfolding invar_def del_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_split_min:
+lemma mset_heap_del_min:
assumes "ts \<noteq> []"
- shows "mset_heap ts = mset_heap (split_min ts) + {# get_min ts #}"
+ shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
using assms
-unfolding split_min_def
+unfolding del_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 split_min = split_min and merge = merge
+ and get_min = get_min and del_min = del_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_split_min[of q] get_min[OF _ \<open>invar q\<close>]
+ thus ?case using mset_heap_del_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_split_min\<close>\<close>
+subsubsection \<open>\<open>t_del_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_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)
+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)
\<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_split_min_bound_aux:
+lemma t_del_min_bound_aux:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
assumes BINVAR: "invar_bheap ts"
assumes "ts\<noteq>[]"
- shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
+ shows "t_del_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_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)
+ 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)
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_split_min ts \<le> 6 * log 2 (n+1) + 3"
+ finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
by auto
thus ?thesis by (simp add: algebra_simps)
qed
-lemma t_split_min_bound:
+lemma t_del_min_bound:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
assumes "invar ts"
assumes "ts\<noteq>[]"
- shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
-using assms t_split_min_bound_aux unfolding invar_def by blast
+ shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
+using assms t_del_min_bound_aux unfolding invar_def by blast
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Sat Apr 21 08:41:42 2018 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Sat Apr 21 11:13:35 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 split_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
-"split_min Leaf = Leaf" |
-"split_min (Node n l x r) = merge l r"
+fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
+"del_min Leaf = Leaf" |
+"del_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_split_min: "mset_tree (split_min h) = mset_tree h - {# get_min h #}"
+lemma mset_del_min: "mset_tree (del_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_split_min: "ltree t \<Longrightarrow> ltree(split_min t)"
+lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
-lemma heap_split_min: "heap t \<Longrightarrow> heap(split_min t)"
+lemma heap_del_min: "heap t \<Longrightarrow> heap(del_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 split_min = split_min
+and insert = insert and del_min = del_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_split_min)
+ case 4 show ?case by(rule mset_del_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_split_min ltree_split_min)
+ case 8 thus ?case by(simp add: heap_del_min ltree_del_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_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"
+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"
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_split_min_log: assumes "ltree t"
- shows "t_split_min t \<le> 2 * log 2 (size1 t) + 1"
+corollary t_del_min_log: assumes "ltree t"
+ shows "t_del_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_split_min t = t_merge t1 t2" by simp
+ have "t_del_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 Sat Apr 21 08:41:42 2018 +0200
+++ b/src/HOL/Data_Structures/Priority_Queue.thy Sat Apr 21 11:13:35 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 split_min :: "'q \<Rightarrow> 'q"
+and del_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_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
- mset (split_min q) = mset q - {# get_min q #}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
+ mset (del_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_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>