1(* Author: Tobias Nipkow *)
2
3section \<open>Specifications of Set ADT\<close>
4
5theory Set_Specs
6imports List_Ins_Del
7begin
8
9text \<open>The basic set interface with traditional \<open>set\<close>-based specification:\<close>
10
11locale Set =
12fixes empty :: "'s"
13fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
14fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
15fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
16fixes set :: "'s \<Rightarrow> 'a set"
17fixes invar :: "'s \<Rightarrow> bool"
18assumes set_empty:    "set empty = {}"
19assumes set_isin:     "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
20assumes set_insert:   "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
21assumes set_delete:   "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
22assumes invar_empty:  "invar empty"
23assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
24assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
25
26lemmas (in Set) set_specs =
27  set_empty set_isin set_insert set_delete invar_empty invar_insert invar_delete
28
29text \<open>The basic set interface with \<open>inorder\<close>-based specification:\<close>
30
31locale Set_by_Ordered =
32fixes empty :: "'t"
33fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
34fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
35fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
36fixes inorder :: "'t \<Rightarrow> 'a list"
37fixes inv :: "'t \<Rightarrow> bool"
38assumes inorder_empty: "inorder empty = []"
39assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
40  isin t x = (x \<in> set (inorder t))"
41assumes inorder_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
42  inorder(insert x t) = ins_list x (inorder t)"
43assumes inorder_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
44  inorder(delete x t) = del_list x (inorder t)"
45assumes inorder_inv_empty:  "inv empty"
46assumes inorder_inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
47assumes inorder_inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
48
49begin
50
51text \<open>It implements the traditional specification:\<close>
52
53definition set :: "'t \<Rightarrow> 'a set" where
54"set == List.set o inorder"
55
56definition invar :: "'t \<Rightarrow> bool" where
57"invar t == inv t \<and> sorted (inorder t)"
58
59sublocale Set
60  empty insert delete isin set invar
61proof(standard, goal_cases)
62  case 1 show ?case by (auto simp: inorder_empty set_def)
63next
64  case 2 thus ?case by(simp add: isin invar_def set_def)
65next
66  case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
67next
68  case (4 s x) thus ?case
69    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
70next
71  case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
72next
73  case 6 thus ?case by(simp add: inorder_insert inorder_inv_insert sorted_ins_list invar_def)
74next
75  case 7 thus ?case by (auto simp: inorder_delete inorder_inv_delete sorted_del_list invar_def)
76qed
77
78end
79
80
81text \<open>Set2 = Set with binary operations:\<close>
82
83locale Set2 = Set
84  where insert = insert for insert :: "'a \<Rightarrow> 's \<Rightarrow> 's" (*for typing purposes only*) +
85fixes union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
86fixes inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
87fixes diff  :: "'s \<Rightarrow> 's \<Rightarrow> 's"
88assumes set_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(union s1 s2) = set s1 \<union> set s2"
89assumes set_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(inter s1 s2) = set s1 \<inter> set s2"
90assumes set_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> set(diff s1 s2) = set s1 - set s2"
91assumes invar_union:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(union s1 s2)"
92assumes invar_inter:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(inter s1 s2)"
93assumes invar_diff:   "\<lbrakk> invar s1; invar s2 \<rbrakk> \<Longrightarrow> invar(diff s1 s2)"
94
95end
96