61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section {* Implementing Ordered Sets *}
|
|
4 |
|
|
5 |
theory Set_by_Ordered
|
|
6 |
imports List_Ins_Del
|
|
7 |
begin
|
|
8 |
|
|
9 |
locale Set =
|
|
10 |
fixes empty :: "'s"
|
|
11 |
fixes insert :: "'a \<Rightarrow> 's \<Rightarrow> 's"
|
|
12 |
fixes delete :: "'a \<Rightarrow> 's \<Rightarrow> 's"
|
|
13 |
fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool"
|
|
14 |
fixes set :: "'s \<Rightarrow> 'a set"
|
|
15 |
fixes invar :: "'s \<Rightarrow> bool"
|
|
16 |
assumes set_empty: "set empty = {}"
|
|
17 |
assumes set_isin: "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
|
|
18 |
assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
|
|
19 |
assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
|
|
20 |
assumes invar_empty: "invar empty"
|
|
21 |
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"
|
|
22 |
assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)"
|
|
23 |
|
|
24 |
locale Set_by_Ordered =
|
|
25 |
fixes empty :: "'t"
|
|
26 |
fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't"
|
|
27 |
fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
|
|
28 |
fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
|
|
29 |
fixes inorder :: "'t \<Rightarrow> 'a list"
|
|
30 |
fixes inv :: "'t \<Rightarrow> bool"
|
|
31 |
assumes empty: "inorder empty = []"
|
|
32 |
assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
|
|
33 |
isin t x = (x \<in> elems (inorder t))"
|
|
34 |
assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
|
|
35 |
inorder(insert x t) = ins_list x (inorder t)"
|
|
36 |
assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
|
|
37 |
inorder(delete x t) = del_list x (inorder t)"
|
|
38 |
assumes inv_empty: "inv empty"
|
|
39 |
assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
|
|
40 |
assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
|
|
41 |
begin
|
|
42 |
|
|
43 |
sublocale Set
|
|
44 |
empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
|
|
45 |
proof(standard, goal_cases)
|
|
46 |
case 1 show ?case by (auto simp: empty)
|
|
47 |
next
|
|
48 |
case 2 thus ?case by(simp add: isin)
|
|
49 |
next
|
|
50 |
case 3 thus ?case by(simp add: insert set_ins_list)
|
|
51 |
next
|
|
52 |
case (4 s x) thus ?case
|
|
53 |
using delete[OF 4, of x] by (auto simp: distinct_if_sorted elems_del_list_eq)
|
|
54 |
next
|
|
55 |
case 5 thus ?case by(simp add: empty inv_empty)
|
|
56 |
next
|
|
57 |
case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
|
|
58 |
next
|
|
59 |
case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
|
|
60 |
qed
|
|
61 |
|
|
62 |
end
|
|
63 |
|
|
64 |
end
|