src/HOL/Data_Structures/Binomial_Heap.thy
 changeset 68020 6aade817bee5 parent 67486 d617e84bb2b1 child 68021 b91a043c0dcb
```     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
```