Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Map_Specs.thy Sprache: Isabelle

Original von: Isabelle^©

(* Author: Tobias Nipkow *)

section \<open>Specifications of Map ADT\<close>

theory Map_Specs
imports AList_Upd_Del
begin

text \<open>The basic map interface with traditional \<open>set\<close>-based specification:\<close>

locale Map =
fixes empty :: "'m"
fixes update :: "'a \ 'b \ 'm \ 'm"
fixes delete :: "'a \ 'm \ 'm"
fixes lookup :: "'m \ 'a \ 'b option"
fixes invar :: "'m \ bool"
assumes map_empty: "lookup empty = (\_. None)"
and map_update: "invar m \ lookup(update a b m) = (lookup m)(a := Some b)"
and map_delete: "invar m \ lookup(delete a m) = (lookup m)(a := None)"
and invar_empty: "invar empty"
and invar_update: "invar m \ invar(update a b m)"
and invar_delete: "invar m \ invar(delete a m)"

lemmas (in Map) map_specs =
  map_empty map_update map_delete invar_empty invar_update invar_delete

text \<open>The basic map interface with \<open>inorder\<close>-based specification:\<close>

locale Map_by_Ordered =
fixes empty :: "'t"
fixes update :: "'a::linorder \ 'b \ 't \ 't"
fixes delete :: "'a \ 't \ 't"
fixes lookup :: "'t \ 'a \ 'b option"
fixes inorder :: "'t \ ('a * 'b) list"
fixes inv :: "'t \ bool"
assumes inorder_empty: "inorder empty = []"
and inorder_lookup: "inv t \ sorted1 (inorder t) \
  lookup t a = map_of (inorder t) a"
and inorder_update: "inv t \ sorted1 (inorder t) \
  inorder(update a b t) = upd_list a b (inorder t)"
and inorder_delete: "inv t \ sorted1 (inorder t) \
  inorder(delete a t) = del_list a (inorder t)"
and inorder_inv_empty:  "inv empty"
and inorder_inv_update: "inv t \ sorted1 (inorder t) \ inv(update a b t)"
and inorder_inv_delete: "inv t \ sorted1 (inorder t) \ inv(delete a t)"

begin

text \<open>It implements the traditional specification:\<close>

definition invar :: "'t \ bool" where
"invar t == inv t \ sorted1 (inorder t)"

sublocale Map
  empty update delete lookup invar
proof(standard, goal_cases)
  case 1 show ?case by (auto simp: inorder_lookup inorder_empty inorder_inv_empty)
next
  case 2 thus ?case
    by(simp add: fun_eq_iff inorder_update inorder_inv_update map_of_ins_list inorder_lookup
         sorted_upd_list invar_def)
next
  case 3 thus ?case
    by(simp add: fun_eq_iff inorder_delete inorder_inv_delete map_of_del_list inorder_lookup
         sorted_del_list invar_def)
next
  case 4 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
next
  case 5 thus ?case by(simp add: inorder_update inorder_inv_update sorted_upd_list invar_def)
next
  case 6 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
qed

end

end

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