-
Notifications
You must be signed in to change notification settings - Fork 0
/
Alternative_price_function.thy
277 lines (257 loc) · 16.2 KB
/
Alternative_price_function.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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
(*<*)
theory Alternative_price_function
imports
Formula_prices
begin
(*>*)
chapter \<open>Alternative price function\<close>
text \<open>\label{chap:alternative_price_function}\<close>
text \<open>It is not immediately clear that \textsf{expr} defines the same function as \cite[Definition 5]{bisping2023process}. In this Section, we define \textsf{alt\_expr}, that basically defines the expressiveness function of \cite[Definition 5]{bisping2023process} and provide the Isabelle proof that the formalizations of \textsf{expr} and \textsf{alt\_expr} define the same function.\<close>
subsubsection \<open>Definition\<close>
text \<open>\textit{
\textnormal{\textsf{alt\_expr}:} $\textnormal{HML}[\Sigma] \rightarrow (\mathbb{N \cup \infty})^6$ of a formula interpreted as $6 \times 1$-dimensional vectors is an expressiveness function, recursively defined by:}
\begin{minipage}{0.45\textwidth}
\[
\textsf{alt\_expr}(\langle a \rangle \varphi) :=
\begin{pmatrix}
1 + \textsf{alt\_expr}_1(\varphi) \\
\textsf{alt\_expr}_2(\varphi) \\
\textsf{alt\_expr}_3(\varphi) \\
\textsf{alt\_expr}_4(\varphi) \\
\textsf{alt\_expr}_5(\varphi) \\
\textsf{alt\_expr}_6(\varphi) \\
\end{pmatrix}
\]
\end{minipage}
\hfill
\begin{minipage}{0.45\textwidth}
\[
\textsf{alt\_expr}(\neg \varphi) :=
\begin{pmatrix}
\textsf{alt\_expr}_1(\varphi) \\
\textsf{alt\_expr}_2(\varphi) \\
\textsf{alt\_expr}_3(\varphi) \\
\textsf{alt\_expr}_4(\varphi) \\
\textsf{alt\_expr}_5(\varphi) \\
1 + \textsf{alt\_expr}_6(\varphi) \\
\end{pmatrix}
\]
\end{minipage}
\[
\textsf{alt\_expr}\left( \bigwedge_{i \in I} \psi_i \right) := \sup(\{
\begin{pmatrix}
0 \\
1 + \sup_{i \in I} \textsf{alt\_expr}_2(\psi_i) \\
\sup_{i \in Pos} \textsf{alt\_expr}_1(\psi_i) \\
\sup_{i \in Pos \backslash \mathcal{R}} \textsf{alt\_expr}_1(\psi_i) \\
\sup_{i \in Neg} \textsf{alt\_expr}_1(\psi_i) \\
0 \\
\end{pmatrix} \} \cup \{\textsf{alt\_expr}(\psi_i) | i \in I\}
\]
Where $Pos$, $Neg$ and $\mathcal{R}$ are defined as in Definition 2.3.1.
Remark: The only deviation from \cite[Definition 5]{bisping2023process} is that we include infinity in the range of the function since we allow for infinite branching conjunctions.
\<close>
text \<open>\textbf{Proposition} \textit{The definitions of \textnormal{\textsf{expr}} and \textnormal{\textsf{alt\_expr}} coincide.}\<close>
text \<open>We can directly formalize the alternative expressiveness function as \<open>alt_expr\<close>. The only deviation is that we have to use \<open>fst\<close> to access the first and \<open>snd\<close> to access subsequent dimensions.
The lemma \<open>expr_def_equivalence\<close> demonstrates that \<open>alt_expr\<close> and \<open>expr\<close> define the same function\<close>
function alt_expr :: "('a, 's)hml \<Rightarrow> enat \<times> enat \<times> enat \<times> enat \<times> enat \<times> enat" where
"alt_expr TT = (0, 1, 0, 0, 0, 0)" |
"alt_expr (hml_pos \<alpha> \<phi>) = (1 + fst (alt_expr \<phi>),
fst (snd (alt_expr \<phi>)),
fst (snd (snd (alt_expr \<phi>))),
fst (snd (snd (snd (alt_expr \<phi>)))),
fst (snd (snd (snd (snd (alt_expr \<phi>))))),
snd (snd (snd (snd (snd (alt_expr \<phi>))))))" |
"alt_expr (hml_conj I J \<Phi>) = (Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> alt_expr \<circ> \<Phi>) ` J),
1 + Sup ((fst \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J),
(Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)),
(Sup (((fst \<circ> alt_expr) ` (pos_r (\<Phi> ` I))) \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)),
(Sup ((fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J \<union> (fst \<circ> alt_expr \<circ> \<Phi>) ` J)),
(Sup ((snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> ((eSuc \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J))))"
by ((meson hml.exhaust), simp+)
text \<open>In order to demonstrate termination of the function, we establish that each sequence of recursive function calls reaches a base case.
For this, we define a well-founded relation and show that function calls are contained within this relation.
A relation \( R \subseteq X \times X \) is considered well-founded if every non-empty subset \( X' \subseteq X \) contains a minimal element \( m \) such that \( (x, m) \notin R \) for all \( x \in X' \).
This ensures that $R$ does not contain infinite descending chains, ensuring that the function reaches a base case and terminates after a finite number of steps.
\<close>
inductive_set HML_wf_rel :: "(('a, 's)hml) rel" where
"\<phi> = \<Phi> i \<and> i \<in> (I \<union> J) \<Longrightarrow> (\<phi>, (hml_conj I J \<Phi>)) \<in> HML_wf_rel" |
"(\<phi>, (hml_pos \<alpha> \<phi>)) \<in> HML_wf_rel"
lemma HML_wf_rel_is_wf: \<open>wf HML_wf_rel\<close>
unfolding wf_def
proof safe
fix P
assume assm: "\<forall>x. (\<forall>y. (y, x) \<in> HML_wf_rel \<longrightarrow> P y) \<longrightarrow> P x"
show "\<And>\<phi>. P \<phi>" proof-
fix \<phi>
show "P \<phi>" proof(induction \<phi>)
case TT
then show ?case
using HML_wf_rel.cases assm by blast
next
case (hml_pos x1 \<phi>)
then show ?case
using HML_wf_rel.cases hml.inject hml.simps assm
by (smt (verit, best))
next
case (hml_conj x1 x2 x3)
then show ?case
using assm
by (metis HML_wf_rel.cases hml.inject(2) hml.simps(8) rangeI)
qed
qed
qed
lemma pos_r_subs: "pos_r (\<Phi> ` I) \<subseteq> (\<Phi> ` I)"
by auto
termination
apply rule
using HML_wf_rel_is_wf HML_wf_rel.simps Un_iff pos_r_subs by fastforce+
(*<*)
lemma \<^marker>\<open>tag (proof) visible\<close> expr_6_alt_expr_eq:
assumes "\<And>x. x \<in> \<Phi> ` I \<Longrightarrow> expr_6 x = snd (snd (snd (snd (snd (alt_expr x)))))"
shows "(expr_6 \<circ> \<Phi>) ` I = (snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I"
proof -
have "(expr_6 \<circ> \<Phi>) ` I = (\<lambda>x. snd (snd (snd (snd (snd (alt_expr (\<Phi> x))))))) ` I"
by (simp add: assms)
also have "... = (snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I"
by auto
finally show ?thesis .
qed
lemma \<^marker>\<open>tag (proof) visible\<close> expr_6_eSuc_eq:
assumes "\<And>x. x \<in> \<Phi> ` J \<Longrightarrow> eSuc (expr_6 x) = eSuc (snd (snd (snd (snd (snd (alt_expr x))))))"
shows "((eSuc \<circ> expr_6 \<circ> \<Phi>) ` J) = ((eSuc \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
proof-
have "((eSuc \<circ> expr_6 \<circ> \<Phi>) ` J) = (\<lambda>x. eSuc (snd (snd (snd (snd (snd (alt_expr (\<Phi> x)))))))) ` J"
using assms by force
also have "... = ((eSuc \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
by auto
finally show ?thesis.
qed
lemma \<^marker>\<open>tag (proof) visible\<close> expr_5_dir_eq:
assumes "\<forall>x \<in> \<Phi> ` (I \<union> J). expr_5 x = fst (snd (snd (snd (snd (alt_expr x)))))"
shows "((expr_5 \<circ> \<Phi>) ` I \<union> (expr_5 \<circ> \<Phi>) ` J) =
((fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
proof-
have "((expr_5 \<circ> \<Phi>) ` I \<union> (expr_5 \<circ> \<Phi>) ` J) = (\<lambda>x. fst (snd (snd (snd (snd (alt_expr (\<Phi> x))))))) ` (I \<union> J)"
using assms
by auto
also have "... = (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` (I \<union> J)"
by auto
also have "... = ((fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
by blast
finally show ?thesis.
qed
(*>*)
lemma expr_def_equivalence:
shows "expr \<phi> = alt_expr \<phi>"
proof(induction \<phi>)
case TT
have "expr TT = (0, 1, 0, 0, 0, 0)" using expr.simps expr_1.simps(1) expr_2.simps(1) expr_3.simps(1) expr_4.simps(1) expr_5.simps(1) expr_6.simps(1)
by force
then show ?case using alt_expr.simps(1)
by force
next
case (hml_pos \<alpha> \<phi>)
hence IH: "(expr_1 \<phi>, expr_2 \<phi>, expr_3 \<phi>, expr_4 \<phi>, expr_5 \<phi>, expr_6 \<phi>) =
(fst (alt_expr \<phi>),
fst (snd (alt_expr \<phi>)),
fst (snd (snd (alt_expr \<phi>))),
fst (snd (snd (snd (alt_expr \<phi>)))),
fst (snd (snd (snd (snd (alt_expr \<phi>))))),
snd (snd (snd (snd (snd (alt_expr \<phi>))))))"
by auto
have expr: "expr (hml_pos \<alpha> \<phi>) = (1 + (expr_1 \<phi>), expr_2 \<phi>, expr_3 \<phi>, expr_4 \<phi>, expr_5 \<phi>, expr_6 \<phi>)"
using expr.simps expr_1.simps expr_2.simps expr_3.simps expr_4.simps expr_5.simps expr_6.simps
by simp
have "alt_expr (hml_pos \<alpha> \<phi>) =
(1 + fst (alt_expr \<phi>),
fst (snd (alt_expr \<phi>)),
fst (snd (snd (alt_expr \<phi>))),
fst (snd (snd (snd (alt_expr \<phi>)))),
fst (snd (snd (snd (snd (alt_expr \<phi>))))),
snd (snd (snd (snd (snd (alt_expr \<phi>))))))"
using alt_expr.simps(2) by auto
then show ?case using expr IH by force
next
case (hml_conj I J \<Phi>)
hence IH: "\<forall>\<phi> \<in> \<Phi> ` I. (expr_1 \<phi>, expr_2 \<phi>, expr_3 \<phi>, expr_4 \<phi>, expr_5 \<phi>, expr_6 \<phi>) =
(fst (alt_expr \<phi>),
fst (snd (alt_expr \<phi>)),
fst (snd (snd (alt_expr \<phi>))),
fst (snd (snd (snd (alt_expr \<phi>)))),
fst (snd (snd (snd (snd (alt_expr \<phi>))))),
snd (snd (snd (snd (snd (alt_expr \<phi>))))))"
"\<forall>\<phi> \<in> \<Phi> ` J. (expr_1 \<phi>, expr_2 \<phi>, expr_3 \<phi>, expr_4 \<phi>, expr_5 \<phi>, expr_6 \<phi>) =
(fst (alt_expr \<phi>),
fst (snd (alt_expr \<phi>)),
fst (snd (snd (alt_expr \<phi>))),
fst (snd (snd (snd (alt_expr \<phi>)))),
fst (snd (snd (snd (snd (alt_expr \<phi>))))),
snd (snd (snd (snd (snd (alt_expr \<phi>))))))"
by simp+
hence e1: "Sup ((expr_1 \<circ> \<Phi>) ` I \<union> (expr_1 \<circ> \<Phi>) ` J) = Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> alt_expr \<circ> \<Phi>) ` J)"
by (smt (verit, best) Pair_inject comp_apply image_cong image_eqI)
have e2: "1 + Sup ((expr_2 \<circ> \<Phi>) ` I \<union> (expr_2 \<circ> \<Phi>) ` J) = 1 + Sup ((fst \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
using IH Sup_le_iff
by (smt (verit) Pair_inject comp_apply image_cong image_eqI)
have e3: "(Sup ((expr_1 \<circ> \<Phi>) ` I \<union> (expr_3 \<circ> \<Phi>) ` I \<union> (expr_3 \<circ> \<Phi>) ` J)) =
(Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J))"
using IH Sup_le_iff
by (smt (verit, ccfv_SIG) Pair_inject comp_apply image_comp image_cong)
have e4: "Sup ((expr_1 ` (pos_r (\<Phi> ` I))) \<union> (expr_4 \<circ> \<Phi>) ` I \<union> (expr_4 \<circ> \<Phi>) ` J) =
(Sup (((fst \<circ> alt_expr) ` (pos_r (\<Phi> ` I))) \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J))"
proof-
have sup_pos_r: "\<forall>x \<in> pos_r (\<Phi> ` I). expr_1 x = (fst \<circ> alt_expr) x"
using IH
by (metis (no_types, lifting) Diff_iff Pair_inject comp_apply pos_r.simps)
hence "Sup (expr_1 ` pos_r (\<Phi> ` I)) = Sup ((fst \<circ> alt_expr) ` pos_r (\<Phi> ` I))"
by (meson SUP_cong)
have "\<forall>x \<in> \<Phi> ` (I \<union> J). expr_4 x = fst (snd (snd (snd (alt_expr x))))"
using IH
by blast+
hence "Sup ((expr_4 \<circ> \<Phi>) ` I \<union> (expr_4 \<circ> \<Phi>) ` J) =
Sup ((fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union>
(fst \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
using SUP_cong by auto
then show ?thesis using sup_pos_r
by (metis (no_types, lifting) Sup_union_distrib image_cong inf_sup_aci(6))
qed
have e5: "(Sup ((expr_5 \<circ> \<Phi>) ` I \<union> (expr_5 \<circ> \<Phi>) ` J \<union> (expr_1 \<circ> \<Phi>) ` J)) =
(Sup ((fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J \<union> (fst \<circ> alt_expr \<circ> \<Phi>) ` J))"
using IH
proof-
have fa_e5: "\<forall>x \<in> \<Phi> ` (I \<union> J). expr_5 x = fst (snd (snd (snd (snd (alt_expr x)))))"
"\<forall>x \<in> \<Phi> ` J. expr_1 x = fst (alt_expr x)"
using IH
by blast+
hence "Sup ((expr_1 \<circ> \<Phi>) ` J )= Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` J)"
by fastforce
have "Sup ((expr_5 \<circ> \<Phi>) ` I \<union> (expr_5 \<circ> \<Phi>) ` J) =
Sup ((fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> (fst \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
using expr_5_dir_eq fa_e5 by force
then show ?thesis
using \<open>Sup ((expr_1 \<circ> \<Phi>) ` J )= Sup ((fst \<circ> alt_expr \<circ> \<Phi>) ` J)\<close>
by (simp add: Sup_union_distrib)
qed
have e6: "(Sup ((expr_6 \<circ> \<Phi>) ` I \<union> ((eSuc \<circ> expr_6 \<circ> \<Phi>) ` J))) =
(Sup ((snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I \<union> ((eSuc \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)))"
proof-
have "\<forall>x \<in> \<Phi> ` I. expr_6 x = snd (snd (snd (snd (snd (alt_expr x)))))"
"\<forall>x \<in> \<Phi> ` J. expr_6 x = snd (snd (snd (snd (snd (alt_expr x)))))"
using IH by blast+
from this(1) have "((expr_6 \<circ> \<Phi>) ` I) = ((snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I)"
using expr_6_alt_expr_eq by force
hence "Sup ((expr_6 \<circ> \<Phi>) ` I) = Sup ((snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I)"
by presburger
have "\<forall>x \<in> \<Phi> ` J. eSuc (expr_6 x) = eSuc (snd (snd (snd (snd (snd (alt_expr x))))))"
using \<open>\<forall>x \<in> \<Phi> ` J. expr_6 x = snd (snd (snd (snd (snd (alt_expr x)))))\<close> by simp
hence "Sup ((eSuc \<circ> expr_6 \<circ> \<Phi>) ` J) = Sup ((eSuc \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` J)"
using expr_6_eSuc_eq by auto
then show ?thesis using \<open>Sup ((expr_6 \<circ> \<Phi>) ` I) = Sup ((snd \<circ> snd \<circ> snd \<circ> snd \<circ> snd \<circ> alt_expr \<circ> \<Phi>) ` I)\<close>
by (simp add: Sup_union_distrib)
qed
then show ?case using e1 e2 e3 e4 e5 e6 by simp
qed
(*<*)
end
(*>*)