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