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