dont rename PQ.del_min
authornipkow
Sat Apr 21 11:13:35 2018 +0200 (4 weeks ago)
changeset 68021b91a043c0dcb
parent 68020 6aade817bee5
child 68022 c8a506be83bd
dont rename PQ.del_min
src/HOL/Data_Structures/Binomial_Heap.thy
src/HOL/Data_Structures/Leftist_Heap.thy
src/HOL/Data_Structures/Priority_Queue.thy
     1.1 --- a/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Sat Apr 21 11:13:35 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>split_min\<close>\<close>
     1.8 +subsubsection \<open>\<open>del_min\<close>\<close>
     1.9  
    1.10 -definition split_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
    1.11 -"split_min ts = (case get_min_rest ts of
    1.12 +definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
    1.13 +"del_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_split_min[simp]:
    1.17 +lemma invar_del_min[simp]:
    1.18    assumes "ts \<noteq> []"
    1.19    assumes "invar ts"
    1.20 -  shows "invar (split_min ts)"
    1.21 +  shows "invar (del_min ts)"
    1.22  using assms
    1.23 -unfolding invar_def split_min_def
    1.24 +unfolding invar_def del_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_split_min:
    1.33 +lemma mset_heap_del_min:
    1.34    assumes "ts \<noteq> []"
    1.35 -  shows "mset_heap ts = mset_heap (split_min ts) + {# get_min ts #}"
    1.36 +  shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}"
    1.37  using assms
    1.38 -unfolding split_min_def
    1.39 +unfolding del_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 split_min = split_min and merge = merge
    1.48 +  and get_min = get_min and del_min = del_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_split_min[of q] get_min[OF _ \<open>invar q\<close>]
    1.57 +  thus ?case using mset_heap_del_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_split_min\<close>\<close>
    1.66 +subsubsection \<open>\<open>t_del_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_split_min :: "'a::linorder heap \<Rightarrow> nat" where
    1.75 -  "t_split_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_del_min :: "'a::linorder heap \<Rightarrow> nat" where
    1.77 +  "t_del_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_split_min_bound_aux:
    1.86 +lemma t_del_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_split_min ts \<le> 6 * log 2 (n+1) + 3"
    1.92 +  shows "t_del_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_split_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_split_min_def by (simp add: GM)
   1.102 +  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.103 +    unfolding t_del_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_split_min ts \<le> 6 * log 2 (n+1) + 3"
   1.112 +  finally have "t_del_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_split_min_bound:
   1.118 +lemma t_del_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_split_min ts \<le> 6 * log 2 (n+1) + 3"
   1.124 -using assms t_split_min_bound_aux unfolding invar_def by blast
   1.125 +  shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3"
   1.126 +using assms t_del_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/Leftist_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sat Apr 21 11:13:35 2018 +0200
     2.3 @@ -67,9 +67,9 @@
     2.4  definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
     2.5  "insert x t = merge (Node 1 Leaf x Leaf) t"
     2.6  
     2.7 -fun split_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
     2.8 -"split_min Leaf = Leaf" |
     2.9 -"split_min (Node n l x r) = merge l r"
    2.10 +fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
    2.11 +"del_min Leaf = Leaf" |
    2.12 +"del_min (Node n l x r) = merge l r"
    2.13  
    2.14  
    2.15  subsection "Lemmas"
    2.16 @@ -99,7 +99,7 @@
    2.17  lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
    2.18  by (induction h) (auto simp add: eq_Min_iff)
    2.19  
    2.20 -lemma mset_split_min: "mset_tree (split_min h) = mset_tree h - {# get_min h #}"
    2.21 +lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
    2.22  by (cases h) (auto simp: mset_merge)
    2.23  
    2.24  lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
    2.25 @@ -130,10 +130,10 @@
    2.26  lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
    2.27  by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
    2.28  
    2.29 -lemma ltree_split_min: "ltree t \<Longrightarrow> ltree(split_min t)"
    2.30 +lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
    2.31  by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
    2.32  
    2.33 -lemma heap_split_min: "heap t \<Longrightarrow> heap(split_min t)"
    2.34 +lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
    2.35  by(cases t)(auto simp add: heap_merge simp del: merge.simps)
    2.36  
    2.37  text \<open>Last step of functional correctness proof: combine all the above lemmas
    2.38 @@ -141,7 +141,7 @@
    2.39  
    2.40  interpretation lheap: Priority_Queue_Merge
    2.41  where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
    2.42 -and insert = insert and split_min = split_min
    2.43 +and insert = insert and del_min = del_min
    2.44  and get_min = get_min and merge = merge
    2.45  and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
    2.46  proof(standard, goal_cases)
    2.47 @@ -151,7 +151,7 @@
    2.48  next
    2.49    case 3 show ?case by(rule mset_insert)
    2.50  next
    2.51 -  case 4 show ?case by(rule mset_split_min)
    2.52 +  case 4 show ?case by(rule mset_del_min)
    2.53  next
    2.54    case 5 thus ?case by(simp add: get_min mset_tree_empty)
    2.55  next
    2.56 @@ -159,7 +159,7 @@
    2.57  next
    2.58    case 7 thus ?case by(simp add: heap_insert ltree_insert)
    2.59  next
    2.60 -  case 8 thus ?case by(simp add: heap_split_min ltree_split_min)
    2.61 +  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
    2.62  next
    2.63    case 9 thus ?case by (simp add: mset_merge)
    2.64  next
    2.65 @@ -196,9 +196,9 @@
    2.66  definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
    2.67  "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
    2.68  
    2.69 -fun t_split_min :: "'a::ord lheap \<Rightarrow> nat" where
    2.70 -"t_split_min Leaf = 1" |
    2.71 -"t_split_min (Node n l a r) = t_merge l r"
    2.72 +fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
    2.73 +"t_del_min Leaf = 1" |
    2.74 +"t_del_min (Node n l a r) = t_merge l r"
    2.75  
    2.76  lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
    2.77  proof(induction l r rule: merge.induct)
    2.78 @@ -229,13 +229,13 @@
    2.79    finally show ?thesis by simp
    2.80  qed
    2.81  
    2.82 -corollary t_split_min_log: assumes "ltree t"
    2.83 -  shows "t_split_min t \<le> 2 * log 2 (size1 t) + 1"
    2.84 +corollary t_del_min_log: assumes "ltree t"
    2.85 +  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
    2.86  proof(cases t)
    2.87    case Leaf thus ?thesis using assms by simp
    2.88  next
    2.89    case [simp]: (Node _ t1 _ t2)
    2.90 -  have "t_split_min t = t_merge t1 t2" by simp
    2.91 +  have "t_del_min t = t_merge t1 t2" by simp
    2.92    also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
    2.93      using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
    2.94    also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
     3.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Sat Apr 21 08:41:42 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Sat Apr 21 11:13:35 2018 +0200
     3.3 @@ -13,18 +13,18 @@
     3.4  and is_empty :: "'q \<Rightarrow> bool"
     3.5  and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
     3.6  and get_min :: "'q \<Rightarrow> 'a"
     3.7 -and split_min :: "'q \<Rightarrow> 'q"
     3.8 +and del_min :: "'q \<Rightarrow> 'q"
     3.9  and invar :: "'q \<Rightarrow> bool"
    3.10  and mset :: "'q \<Rightarrow> 'a multiset"
    3.11  assumes mset_empty: "mset empty = {#}"
    3.12  and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
    3.13  and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
    3.14 -and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    3.15 -    mset (split_min q) = mset q - {# get_min q #}"
    3.16 +and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    3.17 +    mset (del_min q) = mset q - {# get_min q #}"
    3.18  and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
    3.19  and invar_empty: "invar empty"
    3.20  and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
    3.21 -and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
    3.22 +and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
    3.23  
    3.24  text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
    3.25