-
Notifications
You must be signed in to change notification settings - Fork 25
/
Preliminaries.thy
167 lines (123 loc) · 6.51 KB
/
Preliminaries.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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
section \<open>Preliminaries\<close>
text \<open>We start with some definitions of the types involved.\<close>
theory Preliminaries
imports Main
begin
subsection \<open>Slots\<close>
text \<open>Slots are identified by natural numbers.\<close>
type_synonym Slot = nat
subsection \<open>Terms\<close>
text \<open>Terms are identified by natural numbers.\<close>
type_synonym Term = nat
subsubsection \<open>Maximum term of a set\<close>
text \<open>A function for finding the maximum term in a set is as follows.\<close>
definition maxTerm :: "Term set \<Rightarrow> Term"
where "maxTerm S \<equiv> THE t. t \<in> S \<and> (\<forall> t' \<in> S. t' \<le> t)"
text \<open>It works correctly on finite and nonempty sets as follows:\<close>
theorem
fixes S :: "Term set"
assumes finite: "finite S"
shows maxTerm_mem: "S \<noteq> {} \<Longrightarrow> maxTerm S \<in> S"
and maxTerm_max: "\<And> t'. t' \<in> S \<Longrightarrow> t' \<le> maxTerm S"
proof -
presume "S \<noteq> {}"
with assms
obtain t where t: "t \<in> S" "\<And> t'. t' \<in> S \<Longrightarrow> t' \<le> t"
proof (induct arbitrary: thesis)
case empty
then show ?case by simp
next
case (insert t S)
show ?case
proof (cases "S = {}")
case True hence [simp]: "insert t S = {t}" by simp
from insert.prems show ?thesis by simp
next
case False
obtain t' where t': "t' \<in> S" "\<forall> t'' \<in> S. t'' \<le> t'"
by (meson False insert.hyps(3))
from t'
show ?thesis
proof (intro insert.prems ballI)
fix t'' assume t'': "t'' \<in> insert t S"
show "t'' \<le> (if t \<le> t' then t' else t)"
proof (cases "t'' = t")
case False
with t'' have "t'' \<in> S" by simp
with t' have "t'' \<le> t'" by simp
thus ?thesis by auto
qed simp
qed simp
qed
qed
from t have "maxTerm S = t"
by (unfold maxTerm_def, intro the_equality, simp_all add: eq_iff)
with t show "maxTerm S \<in> S" "\<And>t'. t' \<in> S \<Longrightarrow> t' \<le> maxTerm S" by simp_all
qed auto
lemma
assumes "\<And>t. t \<in> S \<Longrightarrow> t \<le> t'" "finite S" "S \<noteq> {}"
shows maxTerm_le: "maxTerm S \<le> t'" using assms maxTerm_mem by auto
subsection \<open>Configurations and quorums\<close>
text \<open>Nodes are simply identified by a natural number.\<close>
datatype Node = Node nat
definition natOfNode :: "Node \<Rightarrow> nat" where "natOfNode node \<equiv> case node of Node n \<Rightarrow> n"
lemma natOfNode_Node[simp]: "natOfNode (Node n) = n" by (simp add: natOfNode_def)
lemma Node_natOfNode[simp]: "Node (natOfNode n) = n" by (cases n, simp add: natOfNode_def)
lemma natOfNode_inj[simp]: "(natOfNode n\<^sub>1 = natOfNode n\<^sub>2) = (n\<^sub>1 = n\<^sub>2)" by (metis Node_natOfNode)
text \<open>It is useful to be able to talk about whether sets-of-sets-of nodes mutually intersect or not.\<close>
definition intersects :: "Node set set \<Rightarrow> Node set set \<Rightarrow> bool" (infixl "\<frown>" 50)
where "A \<frown> B \<equiv> \<forall> a \<in> A. \<forall> b \<in> B. a \<inter> b \<noteq> {}"
definition majorities :: "Node set \<Rightarrow> Node set set"
where "majorities votingNodes = { q. card votingNodes < card (q \<inter> votingNodes) * 2 }"
lemma majorities_nonempty: assumes "q \<in> majorities Q" shows "q \<noteq> {}"
using assms by (auto simp add: majorities_def)
lemma majorities_member: assumes "q \<in> majorities Q" obtains n where "n \<in> q"
using majorities_nonempty assms by fastforce
lemma majorities_intersect:
assumes "finite votingNodes"
shows "majorities votingNodes \<frown> majorities votingNodes"
unfolding intersects_def
proof (intro ballI notI)
fix q\<^sub>1 assume q\<^sub>1: "q\<^sub>1 \<in> majorities votingNodes"
fix q\<^sub>2 assume q\<^sub>2: "q\<^sub>2 \<in> majorities votingNodes"
assume disj: "q\<^sub>1 \<inter> q\<^sub>2 = {}"
have 1: "card ((q\<^sub>1 \<inter> votingNodes) \<union> (q\<^sub>2 \<inter> votingNodes)) = card (q\<^sub>1 \<inter> votingNodes) + card (q\<^sub>2 \<inter> votingNodes)"
proof (intro card_Un_disjoint)
from assms show "finite (q\<^sub>1 \<inter> votingNodes)" by simp
from assms show "finite (q\<^sub>2 \<inter> votingNodes)" by simp
from disj show "q\<^sub>1 \<inter> votingNodes \<inter> (q\<^sub>2 \<inter> votingNodes) = {}" by auto
qed
have "card ((q\<^sub>1 \<inter> votingNodes) \<union> (q\<^sub>2 \<inter> votingNodes)) \<le> card votingNodes" by (simp add: assms card_mono)
hence 2: "2 * card (q\<^sub>1 \<inter> votingNodes) + 2 * card (q\<^sub>2 \<inter> votingNodes) \<le> 2 * card votingNodes" by (simp add: 1)
from q\<^sub>1 q\<^sub>2 have 3: "card votingNodes + card votingNodes < 2 * card (q\<^sub>1 \<inter> votingNodes) + 2 * card (q\<^sub>2 \<inter> votingNodes)"
unfolding majorities_def by auto
from 2 3 show False by simp
qed
text \<open>A configuration of the system defines the sets of master-eligible nodes whose votes count when calculating quorums.
The initial configuration of the system is fixed to some arbitrary value.\<close>
consts Vs\<^sub>0 :: "Node list"
definition V\<^sub>0 :: "Node set" where "V\<^sub>0 \<equiv> set Vs\<^sub>0"
lemma finite_V\<^sub>0: "finite V\<^sub>0" unfolding V\<^sub>0_def by auto
lemma V\<^sub>0_intersects: "majorities V\<^sub>0 \<frown> majorities V\<^sub>0" using finite_V\<^sub>0 by (intro majorities_intersect)
subsection \<open>Values\<close>
text \<open>The model is a replicated state machine, with transitions that either do nothing, alter
the configuration of the system or set a new \texttt{ClusterState}. \texttt{ClusterState} values
are modelled simply as natural numbers.\<close>
datatype ClusterState = ClusterState nat
consts CS\<^sub>0 :: ClusterState
datatype Value
= NoOp
| Reconfigure "Node list" (* update the set of voting nodes. A list rather than a set to force it to be finite *)
| ClusterStateDiff "ClusterState \<Rightarrow> ClusterState" (* a ClusterState diff *)
text \<open>Some useful definitions and lemmas follow.\<close>
fun isReconfiguration :: "Value \<Rightarrow> bool"
where "isReconfiguration (Reconfigure _) = True"
| "isReconfiguration _ = False"
fun getConf :: "Value \<Rightarrow> Node set"
where "getConf (Reconfigure conf) = set conf"
| "getConf _ = {}"
lemma getConf_finite: "finite (getConf v)"
by (metis List.finite_set getConf.elims infinite_imp_nonempty)
lemma getConf_intersects: "majorities (getConf v) \<frown> majorities (getConf v)"
by (simp add: getConf_finite majorities_intersect)
end