This repository has been archived by the owner on Jan 8, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
USet.thy
144 lines (114 loc) · 3.65 KB
/
USet.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
theory USet
imports CvRDT HOL.Set HOL.Fun
begin
datatype 'a USet = USet "'a set"
definition "initial = USet Set.empty"
fun add :: "'a USet => 'a => 'a USet" where
"add (USet s) e = USet (Set.union s {e})"
fun query :: "'a USet => 'a set" where
"query (USet s) = s"
fun less_eq :: "'a USet => 'a USet => bool" where
"less_eq (USet s1) (USet s2) = Set.subset_eq s1 s2"
fun less :: "'a USet => 'a USet => bool" where
"less (USet s1) (USet s2) = Set.subset s1 s2"
fun merge :: "'a USet => 'a USet => 'a USet" where
"merge (USet s1) (USet s2) = USet (Set.union s1 s2)"
(* USet properties *)
lemma query_contains_add: "e \<in> query (add s e)"
apply (induct s)
by auto
lemma add_creates_no_item: "\<not> a \<in> (query s) & \<not> (a = b) ==> \<not> a \<in> (query (add s b))"
apply (induct s)
by auto
lemma initial_contains_nothing: "\<not> e \<in> (query initial)"
by (simp add: initial_def)
lemma updated_preserves_items: "e \<in> query s ==> e \<in> query (add s a)"
apply (induct s)
by auto
lemma merge_preserves_items: "e \<in> query a ==> e \<in> query (merge a b)"
apply (induct a)
apply (induct b)
by auto
lemma merge_creates_no_item: "\<not> e \<in> query a \<and> \<not> e \<in> query b ==> \<not> e \<in> query (merge a b)"
apply (induct a)
apply (induct b)
by auto
lemma merge_identity_right: "(e \<in> query a) = (e \<in> query (merge a initial))"
unfolding initial_def
apply (induct a)
by auto
lemma merge_identity_left: "(e \<in> query a) = (e \<in> query (merge initial a))"
unfolding initial_def
apply (induct a)
by auto
(* CvRDT properties *)
lemma less_eq_empty: "less_eq initial x"
unfolding initial_def
apply (induct x)
by auto
lemma less_eq_reflexive: "less_eq x x"
apply (induct x)
by auto
lemma less_comb: "less x y = (less_eq x y & (~ less_eq y x))"
apply (induct x)
apply (induct y)
by auto
lemma less_eq_transitive: "less_eq x y ==> less_eq y z ==> less_eq x z"
apply (induct x)
apply (induct y)
apply (induct z)
by auto
lemma less_eq_eq: "less_eq x y ==> less_eq y x ==> x = y"
apply (induct x)
apply (induct y)
by auto
lemma less_eq_merge_left: "less_eq x (merge x y)"
apply (induct x)
apply (induct y)
by auto
lemma less_eq_merge_right: "less_eq y (merge x y)"
apply (induct x)
apply (induct y)
by auto
lemma less_eq_merge_count: "less_eq a c ==> less_eq b c ==> less_eq (merge a b) c"
apply (induct a)
apply (induct b)
apply (induct c)
by auto
lemma less_eq_add_monotonic: "less_eq a (add a u)"
apply (induct a)
by auto
(* USet methods *)
interpretation USetCvRDT : CvRDT
USet.initial
USet.less_eq
USet.less
USet.merge
USet.query
USet.add
proof
show "\<And>x. USet.less_eq initial x"
by (simp add:less_eq_empty)
show "\<And>x. USet.less_eq x x"
by (simp add:less_eq_reflexive)
show "\<And>x y. USet.less x y = (USet.less_eq x y \<and> \<not> USet.less_eq y x)"
by (simp add:less_comb)
show "\<And>x y z.
USet.less_eq x y \<Longrightarrow>
USet.less_eq y z \<Longrightarrow> USet.less_eq x z"
by (simp add:less_eq_transitive)
show "\<And>x y. USet.less_eq x y \<Longrightarrow> USet.less_eq y x \<Longrightarrow> x = y"
by (simp add:less_eq_eq)
show "\<And>x y. USet.less_eq x (USet.merge x y)"
by (simp add:less_eq_merge_left)
show "\<And>y x. USet.less_eq y (USet.merge x y)"
by (simp add:less_eq_merge_right)
show "\<And>y x z.
USet.less_eq y x \<Longrightarrow>
USet.less_eq z x \<Longrightarrow>
USet.less_eq (USet.merge y z) x"
by (simp add:less_eq_merge_count)
show "\<And>a u. USet.less_eq a (add a u)"
by (simp add:less_eq_add_monotonic)
qed
end