Quelle  Map_Specs.thy

(* Author: Tobias Nipkow *)

section ‹Specifications of Map ADT›

theory Map_Specs
imports AList_Upd_Del
begin

text ‹The basic map interface with @{typ "'a ==> 'b option"} based specification:›

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 ‹The basic map interface with ‹inorder›-based specification:›

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 ‹It implements the traditional specification:›

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