Quelle Set_Specs.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

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

theory Set_Specs
imports List_Ins_Del
begin

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

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 \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>

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 \<in> 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 \<open>It implements the traditional specification:\<close>

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 \<open>Set2 = Set with binary operations:\<close>

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

quality67%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.