Quelle Heaps.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section \<open>Heaps\<close>

theory Heaps
imports
  "HOL-Library.Tree_Multiset"
  Priority_Queue_Specs
begin

text \<open>Heap = priority queue on trees:\<close>

locale Heap =
fixes insert :: "('a::linorder) \ 'a tree \ 'a tree"
and  del_min :: "'a tree \ 'a tree"
assumes mset_insert: "heap q \ mset_tree (insert x q) = {#x#} + mset_tree q"
and    mset_del_min: "\ heap q; q \ Leaf \ \ mset_tree (del_min q) = mset_tree q - {#value q#}"
and     heap_insert: "heap q \ heap(insert x q)"
and    heap_del_min: "heap q \ heap(del_min q)"
begin

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

fun is_empty :: "'a tree \ bool" where
"is_empty t = (t = Leaf)"

fun get_min :: "'a tree \ 'a" where
"get_min (Node l a r) = a"

sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert
and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree
proof (standard, goal_cases)
  case 1 thus ?case by (simp add: empty_def)
next
  case 2 thus ?case by(auto)
next
  case 3 thus ?case by(simp add: mset_insert)
next
  case 4 thus ?case by(auto simp add: mset_del_min neq_Leaf_iff)
next
  case 5 thus ?case by(auto simp: neq_Leaf_iff Min_insert2 simp del: Un_iff)
next
  case 6 thus ?case by(simp add: empty_def)
next
  case 7 thus ?case by(simp add: heap_insert)
next
  case 8 thus ?case by(simp add: heap_del_min)
qed

end

text \<open>Once you have \<open>merge\<close>, \<open>insert\<close> and \<open>del_min\<close> are easy:\<close>

locale Heap_Merge =
fixes merge :: "'a::linorder tree \ 'a tree \ 'a tree"
assumes mset_merge: "\ heap q1; heap q2 \ \ mset_tree (merge q1 q2) = mset_tree q1 + mset_tree q2"
and invar_merge: "\ heap q1; heap q2 \ \ heap (merge q1 q2)"
begin

fun insert :: "'a \ 'a tree \ 'a tree" where
"insert x t = merge (Node Leaf x Leaf) t"

fun del_min :: "'a tree \ 'a tree" where
"del_min Leaf = Leaf" |
"del_min (Node l x r) = merge l r"

interpretation Heap insert del_min
proof(standard, goal_cases)
  case 1 thus ?case by(simp add:mset_merge)
next
  case (2 q) thus ?case by(cases q)(auto simp: mset_merge)
next
  case 3 thus ?case by (simp add: invar_merge)
next
  case (4 q) thus ?case by (cases q)(auto simp: invar_merge)
qed

lemmas local_empty_def = local.empty_def
lemmas local_get_min_def = local.get_min.simps

sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert
and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree and merge = merge
proof(standard, goal_cases)
  case 1 thus ?case by (simp add: mset_merge)
next
  case 2 thus ?case by (simp add: invar_merge)
qed

end

end

quality97%

¤ Dauer der Verarbeitung: 0.13 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.