Theory HOL-Data_Structures.Set_Specs

(* Author: Tobias Nipkow *)

section ‹Specifications of Set ADT›

theory Set_Specs
imports List_Ins_Del
begin

text ‹The basic set interface with traditional set›-based specification:›

locale Set =
fixes empty :: "'s"
fixes insert :: "'a  's  's"
fixes delete :: "'a  's  's"
fixes isin :: "'s  'a  bool"
fixes set :: "'s  'a set"
fixes invar :: "'s  bool"
assumes set_empty:    "set empty = {}"
assumes set_isin:     "invar s  isin s x = (x  set s)"
assumes set_insert:   "invar s  set(insert x s) = set s  {x}"
assumes set_delete:   "invar s  set(delete x s) = set s - {x}"
assumes invar_empty:  "invar empty"
assumes invar_insert: "invar s  invar(insert x s)"
assumes invar_delete: "invar s  invar(delete x s)"

lemmas (in Set) set_specs =
  set_empty set_isin set_insert set_delete invar_empty invar_insert invar_delete

text ‹The basic set interface with inorder›-based specification:›

locale Set_by_Ordered =
fixes empty :: "'t"
fixes insert :: "'a::linorder  't  't"
fixes delete :: "'a  't  't"
fixes isin :: "'t  'a  bool"
fixes inorder :: "'t  'a list"
fixes inv :: "'t  bool"
assumes inorder_empty: "inorder empty = []"
assumes isin: "inv t  sorted(inorder t) 
  isin t x = (x  set (inorder t))"
assumes inorder_insert: "inv t  sorted(inorder t) 
  inorder(insert x t) = ins_list x (inorder t)"
assumes inorder_delete: "inv t  sorted(inorder t) 
  inorder(delete x t) = del_list x (inorder t)"
assumes inorder_inv_empty:  "inv empty"
assumes inorder_inv_insert: "inv t  sorted(inorder t)  inv(insert x t)"
assumes inorder_inv_delete: "inv t  sorted(inorder t)  inv(delete x t)"

begin

text ‹It implements the traditional specification:›

definition set :: "'t  'a set" where
"set = List.set o inorder"

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

sublocale Set
  empty insert delete isin set invar
proof(standard, goal_cases)
  case 1 show ?case by (auto simp: inorder_empty set_def)
next
  case 2 thus ?case by(simp add: isin invar_def set_def)
next
  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
next
  case (4 s x) thus ?case
    by (auto simp: inorder_delete set_del_list invar_def set_def)
next
  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
next
  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
next
  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
qed

end


text ‹Set2 = Set with binary operations:›

locale Set2 = Set
  where insert = insert for insert :: "'a  's  's" (*for typing purposes only*) +
fixes union :: "'s  's  's"
fixes inter :: "'s  's  's"
fixes diff  :: "'s  's  's"
assumes set_union:   " invar s1; invar s2   set(union s1 s2) = set s1  set s2"
assumes set_inter:   " invar s1; invar s2   set(inter s1 s2) = set s1  set s2"
assumes set_diff:   " invar s1; invar s2   set(diff s1 s2) = set s1 - set s2"
assumes invar_union:   " invar s1; invar s2   invar(union s1 s2)"
assumes invar_inter:   " invar s1; invar s2   invar(inter s1 s2)"
assumes invar_diff:   " invar s1; invar s2   invar(diff s1 s2)"

end