SSL Leftist_Heap.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section \<open>Leftist Heap\<close>

theory Leftist_Heap
imports
  "HOL-Library.Pattern_Aliases"
  Tree2
  Priority_Queue_Specs
  Complex_Main
  "HOL-Library.Time_Commands"
begin

fun mset_tree :: "('a*'b) tree \ 'a multiset" where
"mset_tree Leaf = {#}" |
"mset_tree (Node l (a, _) r) = {#a#} + mset_tree l + mset_tree r"

type_synonym 'a lheap = "('a*nat)tree"

fun mht :: "'a lheap \ nat" where
"mht Leaf = 0" |
"mht (Node _ (_, n) _) = n"

text\<open>The invariants:\<close>

fun (in linorder) heap :: "('a*'b) tree \ bool" where
"heap Leaf = True" |
"heap (Node l (m, _) r) =
  ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"

fun ltree :: "'a lheap \ bool" where
"ltree Leaf = True" |
"ltree (Node l (a, n) r) =
(min_height l \<ge> min_height r \<and> n = min_height r + 1 \<and> ltree l & ltree r)"

definition empty :: "'a lheap" where
"empty = Leaf"

definition node :: "'a lheap \ 'a \ 'a lheap \ 'a lheap" where
"node l a r =
(let mhl = mht l; mhr = mht r
  in if mhl \<ge> mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)"

fun get_min :: "'a lheap \ 'a" where
"get_min(Node l (a, n) r) = a"

text \<open>For function \<open>merge\<close>:\<close>
unbundle pattern_aliases

fun merge :: "'a::ord lheap \ 'a lheap \ 'a lheap" where
"merge Leaf t = t" |
"merge t Leaf = t" |
"merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
    else node l2 a2 (merge t1 r2))"

text \<open>Termination of @{const merge}: by sum or lexicographic product of the sizes
of the two arguments. Isabelle uses a lexicographic product.\<close>

lemma merge_code: "merge t1 t2 = (case (t1,t2) of
  (Leaf, _) \<Rightarrow> t2 |
  (_, Leaf) \<Rightarrow> t1 |
  (Node l1 (a1, n1) r1, Node l2 (a2, n2) r2) \<Rightarrow>
    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))"
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)

hide_const (open) insert

definition insert :: "'a::ord \ 'a lheap \ 'a lheap" where
"insert x t = merge (Node Leaf (x,1) Leaf) t"

fun del_min :: "'a::ord lheap \ 'a lheap" where
"del_min Leaf = Leaf" |
"del_min (Node l _ r) = merge l r"

subsection "Lemmas"

lemma mset_tree_empty: "mset_tree t = {#} \ t = Leaf"
by(cases t) auto

lemma mht_eq_min_height: "ltree t \ mht t = min_height t"
by(cases t) auto

lemma ltree_node: "ltree (node l a r) \ ltree l \ ltree r"
by(auto simp add: node_def mht_eq_min_height)

lemma heap_node: "heap (node l a r) \
  heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)"
by(auto simp add: node_def)

lemma set_tree_mset: "set_tree t = set_mset(mset_tree t)"
by(induction t) auto

subsection "Functional Correctness"

lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2"
by (induction t1 t2 rule: merge.induct) (auto simp add: node_def ac_simps)

lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
by (auto simp add: insert_def mset_merge)

lemma get_min: "\ heap t; t \ Leaf \ \ get_min t = Min(set_tree t)"
by (cases t) (auto simp add: eq_Min_iff)

lemma mset_del_min: "mset_tree (del_min t) = mset_tree t - {# get_min t #}"
by (cases t) (auto simp: mset_merge)

lemma ltree_merge: "\ ltree l; ltree r \ \ ltree (merge l r)"
by(induction l r rule: merge.induct)(auto simp: ltree_node)

lemma heap_merge: "\ heap l; heap r \ \ heap (merge l r)"
proof(induction l r rule: merge.induct)
  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un set_tree_mset)
qed simp_all

lemma ltree_insert: "ltree t \ ltree(insert x t)"
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)

lemma heap_insert: "heap t \ heap(insert x t)"
by(simp add: insert_def heap_merge del: merge.simps split: tree.split)

lemma ltree_del_min: "ltree t \ ltree(del_min t)"
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)

lemma heap_del_min: "heap t \ 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
to show that leftist heaps satisfy the specification of priority queues with merge.\<close>

interpretation lheap: Priority_Queue_Merge
where empty = empty and is_empty = "\t. t = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
and invar = "\t. heap t \ ltree t" and mset = mset_tree
proof(standard, goal_cases)
  case 1 show ?case by (simp add: empty_def)
next
  case (2 q) show ?case by (cases q) auto
next
  case 3 show ?case by(rule mset_insert)
next
  case 4 show ?case by(rule mset_del_min)
next
  case 5 thus ?case by(simp add: get_min mset_tree_empty set_tree_mset)
next
  case 6 thus ?case by(simp add: empty_def)
next
  case 7 thus ?case by(simp add: heap_insert ltree_insert)
next
  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
next
  case 9 thus ?case by (simp add: mset_merge)
next
  case 10 thus ?case by (simp add: heap_merge ltree_merge)
qed

subsection "Complexity"

text \<open>Auxiliary time functions (which are both 0):\<close>
time_fun mht
time_fun node

lemma T_mht_0[simp]: "T_mht t = 0"
by(cases t)auto

text \<open>Define timing function\<close>
time_fun merge
time_fun insert
time_fun del_min

lemma T_merge_min_height: "ltree l \ ltree r \ T_merge l r \ min_height l + min_height r + 1"
proof(induction l r rule: merge.induct)
  case 3 thus ?case by(auto)
qed simp_all

corollary T_merge_log: assumes "ltree l" "ltree r"
  shows "T_merge l r \ log 2 (size1 l) + log 2 (size1 r) + 1"
using le_log2_of_power[OF min_height_size1[of l]]
  le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms
by linarith

corollary T_insert_log: "ltree t \ T_insert x t \ log 2 (size1 t) + 2"
using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
by(simp split: tree.split)

corollary T_del_min_log: assumes "ltree t"
  shows "T_del_min t \ 2 * log 2 (size1 t) + 1"
proof(cases t rule: tree2_cases)
  case Leaf thus ?thesis using assms by simp
next
  case [simp]: (Node l _ _ r)
  show ?thesis
    using \<open>ltree t\<close> T_merge_log[of l r]
      log_mono[of 2 "size1 l" "size1 t"] log_mono[of 2 "size1 r" "size1 t"]
    by (simp del: T_merge.simps)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.