|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Map_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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
