src/HOL/Data_Structures/Leftist_Heap.thy
changeset 68020 6aade817bee5
parent 67406 23307fd33906
child 68021 b91a043c0dcb
     1.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -67,9 +67,9 @@
     1.4  definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
     1.5  "insert x t = merge (Node 1 Leaf x Leaf) t"
     1.6  
     1.7 -fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
     1.8 -"del_min Leaf = Leaf" |
     1.9 -"del_min (Node n l x r) = merge l r"
    1.10 +fun split_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
    1.11 +"split_min Leaf = Leaf" |
    1.12 +"split_min (Node n l x r) = merge l r"
    1.13  
    1.14  
    1.15  subsection "Lemmas"
    1.16 @@ -99,7 +99,7 @@
    1.17  lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
    1.18  by (induction h) (auto simp add: eq_Min_iff)
    1.19  
    1.20 -lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
    1.21 +lemma mset_split_min: "mset_tree (split_min h) = mset_tree h - {# get_min h #}"
    1.22  by (cases h) (auto simp: mset_merge)
    1.23  
    1.24  lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
    1.25 @@ -130,10 +130,10 @@
    1.26  lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
    1.27  by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
    1.28  
    1.29 -lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
    1.30 +lemma ltree_split_min: "ltree t \<Longrightarrow> ltree(split_min t)"
    1.31  by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
    1.32  
    1.33 -lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
    1.34 +lemma heap_split_min: "heap t \<Longrightarrow> heap(split_min t)"
    1.35  by(cases t)(auto simp add: heap_merge simp del: merge.simps)
    1.36  
    1.37  text \<open>Last step of functional correctness proof: combine all the above lemmas
    1.38 @@ -141,7 +141,7 @@
    1.39  
    1.40  interpretation lheap: Priority_Queue_Merge
    1.41  where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
    1.42 -and insert = insert and del_min = del_min
    1.43 +and insert = insert and split_min = split_min
    1.44  and get_min = get_min and merge = merge
    1.45  and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
    1.46  proof(standard, goal_cases)
    1.47 @@ -151,7 +151,7 @@
    1.48  next
    1.49    case 3 show ?case by(rule mset_insert)
    1.50  next
    1.51 -  case 4 show ?case by(rule mset_del_min)
    1.52 +  case 4 show ?case by(rule mset_split_min)
    1.53  next
    1.54    case 5 thus ?case by(simp add: get_min mset_tree_empty)
    1.55  next
    1.56 @@ -159,7 +159,7 @@
    1.57  next
    1.58    case 7 thus ?case by(simp add: heap_insert ltree_insert)
    1.59  next
    1.60 -  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
    1.61 +  case 8 thus ?case by(simp add: heap_split_min ltree_split_min)
    1.62  next
    1.63    case 9 thus ?case by (simp add: mset_merge)
    1.64  next
    1.65 @@ -196,9 +196,9 @@
    1.66  definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
    1.67  "t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
    1.68  
    1.69 -fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
    1.70 -"t_del_min Leaf = 1" |
    1.71 -"t_del_min (Node n l a r) = t_merge l r"
    1.72 +fun t_split_min :: "'a::ord lheap \<Rightarrow> nat" where
    1.73 +"t_split_min Leaf = 1" |
    1.74 +"t_split_min (Node n l a r) = t_merge l r"
    1.75  
    1.76  lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
    1.77  proof(induction l r rule: merge.induct)
    1.78 @@ -229,13 +229,13 @@
    1.79    finally show ?thesis by simp
    1.80  qed
    1.81  
    1.82 -corollary t_del_min_log: assumes "ltree t"
    1.83 -  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
    1.84 +corollary t_split_min_log: assumes "ltree t"
    1.85 +  shows "t_split_min t \<le> 2 * log 2 (size1 t) + 1"
    1.86  proof(cases t)
    1.87    case Leaf thus ?thesis using assms by simp
    1.88  next
    1.89    case [simp]: (Node _ t1 _ t2)
    1.90 -  have "t_del_min t = t_merge t1 t2" by simp
    1.91 +  have "t_split_min t = t_merge t1 t2" by simp
    1.92    also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
    1.93      using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
    1.94    also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"