Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Tree_Map.thy Sprache: Isabelle

Original von: Isabelle^©

(* Author: Tobias Nipkow *)

section \<open>Unbalanced Tree Implementation of Map\<close>

theory Tree_Map
imports
  Tree_Set
  Map_Specs
begin

fun lookup :: "('a::linorder*'b) tree \ 'a \ 'b option" where
"lookup Leaf x = None" |
"lookup (Node l (a,b) r) x =
  (case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)"

fun update :: "'a::linorder \ 'b \ ('a*'b) tree \ ('a*'b) tree" where
"update x y Leaf = Node Leaf (x,y) Leaf" |
"update x y (Node l (a,b) r) = (case cmp x a of
   LT \<Rightarrow> Node (update x y l) (a,b) r |
   EQ \<Rightarrow> Node l (x,y) r |
   GT \<Rightarrow> Node l (a,b) (update x y r))"

fun delete :: "'a::linorder \ ('a*'b) tree \ ('a*'b) tree" where
"delete x Leaf = Leaf" |
"delete x (Node l (a,b) r) = (case cmp x a of
  LT \<Rightarrow> Node (delete x l) (a,b) r |
  GT \<Rightarrow> Node l (a,b) (delete x r) |
  EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = split_min r in Node l ab' r')"

subsection "Functional Correctness Proofs"

lemma lookup_map_of:
  "sorted1(inorder t) \ lookup t x = map_of (inorder t) x"
by (induction t) (auto simp: map_of_simps split: option.split)

lemma inorder_update:
  "sorted1(inorder t) \ inorder(update a b t) = upd_list a b (inorder t)"
by(induction t) (auto simp: upd_list_simps)

lemma inorder_delete:
  "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)"
by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)

interpretation M: Map_by_Ordered
where empty = empty and lookup = lookup and update = update and delete = delete
and inorder = inorder and inv = "\_. True"
proof (standard, goal_cases)
  case 1 show ?case by (simp add: empty_def)
next
  case 2 thus ?case by(simp add: lookup_map_of)
next
  case 3 thus ?case by(simp add: inorder_update)
next
  case 4 thus ?case by(simp add: inorder_delete)
qed auto

end

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