Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Heaps.thy Sprache: Isabelle

Original von: 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)"

sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert
and get_min = "value" 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(simp add: mset_del_min)
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

sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert
and get_min = "value" 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

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.