|
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 = {}" |
|
17 assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)" |
|
18 assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)" |
|
19 assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}" |
|
20 assumes "invar s \<Longrightarrow> invar(insert a s)" |
|
21 assumes "invar s \<Longrightarrow> invar(delete a s)" |
|
22 |
|
23 locale Set_by_Ordered = |
|
24 fixes empty :: "'t" |
|
25 fixes insert :: "'a::linorder \<Rightarrow> 't \<Rightarrow> 't" |
|
26 fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't" |
|
27 fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool" |
|
28 fixes inorder :: "'t \<Rightarrow> 'a list" |
|
29 fixes wf :: "'t \<Rightarrow> bool" |
|
30 assumes empty: "inorder empty = []" |
|
31 assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
|
32 isin t a = (a \<in> elems (inorder t))" |
|
33 assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
|
34 inorder(insert a t) = ins_list a (inorder t)" |
|
35 assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> |
|
36 inorder(delete a t) = del_list a (inorder t)" |
|
37 assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)" |
|
38 assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)" |
|
39 begin |
|
40 |
|
41 sublocale Set |
|
42 empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)" |
|
43 proof(standard, goal_cases) |
|
44 case 1 show ?case by (auto simp: empty) |
|
45 next |
|
46 case 2 thus ?case by(simp add: isin) |
|
47 next |
|
48 case 3 thus ?case by(simp add: insert) |
|
49 next |
|
50 case (4 s a) show ?case |
|
51 using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted) |
|
52 next |
|
53 case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list) |
|
54 next |
|
55 case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list) |
|
56 qed |
|
57 |
|
58 end |
|
59 |
|
60 end |