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