-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathBinary_operations.thy
276 lines (257 loc) · 13.6 KB
/
Binary_operations.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
theory Binary_operations
imports Bij_betw_simplicial_complex_bool_func
begin
section\<open>Binary operations over Boolean functions and simplicial complexes\<close>
text\<open>In this theory some results on binary operations over Boolean functions and
their relationship to operations over the induced simplicial complexes are
presented. We follow the presentation by Chastain and Scoville~\cite[Sect. 1.1]{CHSC}.\<close>
definition bool_fun_or :: "nat \<Rightarrow> (bool vec \<Rightarrow> bool) \<Rightarrow> (bool vec \<Rightarrow> bool) \<Rightarrow> (bool vec \<Rightarrow> bool)"
where "(bool_fun_or n f g) \<equiv> (\<lambda>x. f x \<or> g x)"
definition bool_fun_and :: "nat \<Rightarrow> (bool vec \<Rightarrow> bool) \<Rightarrow> (bool vec \<Rightarrow> bool) \<Rightarrow> (bool vec \<Rightarrow> bool)"
where "(bool_fun_and n f g) \<equiv> (\<lambda>x. f x \<and> g x)"
lemma eq_union_or:
"simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
= simplicial_complex_induced_by_monotone_boolean_function n f
\<union> simplicial_complex_induced_by_monotone_boolean_function n g"
(is "?sc n (?bf_or n f g) = ?sc n f \<union> ?sc n g")
proof
show "?sc n f \<union> ?sc n g \<subseteq> ?sc n (?bf_or n f g)"
proof
fix \<sigma> :: "nat set"
assume "\<sigma> \<in> (?sc n f \<union> ?sc n g)"
hence sigma: "\<sigma> \<in> ?sc n f \<or> \<sigma> \<in> ?sc n g" by auto
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
\<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
proof (cases "\<sigma> \<in> ?sc n f")
case True
from simplicial_complex.simplicial_complex_implies_true [OF True]
show "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
\<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)" by fast
next
case False
hence sigmain: "\<sigma> \<in> ?sc n g" using sigma by fast
from simplicial_complex.simplicial_complex_implies_true [OF sigmain]
show "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
\<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)" by fast
qed
thus "\<sigma> \<in> ?sc n (?bf_or n f g)"
using simplicial_complex_induced_by_monotone_boolean_function_def
using bool_fun_or_def sigma by auto
qed
next
show "?sc n (?bf_or n f g) \<subseteq> ?sc n f \<union> ?sc n g"
proof
fix \<sigma>::"nat set"
assume sigma: "\<sigma> \<in> ?sc n (?bf_or n f g)"
hence "bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
unfolding simplicial_complex.bool_vec_from_simplice_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
unfolding ceros_of_boolean_input_def
by auto (smt (verit) dim_vec eq_vecI index_vec)+
hence "(f (simplicial_complex.bool_vec_from_simplice n \<sigma>))
\<or> (g (simplicial_complex.bool_vec_from_simplice n \<sigma>))"
unfolding bool_fun_or_def
by auto
hence "\<sigma> \<in> ?sc n f \<or> \<sigma> \<in> ?sc n g"
by (smt (z3) sigma bool_fun_or_def mem_Collect_eq
simplicial_complex_induced_by_monotone_boolean_function_def)
thus "\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f
\<union> simplicial_complex_induced_by_monotone_boolean_function n g"
by auto
qed
qed
lemma eq_inter_and:
"simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
= simplicial_complex_induced_by_monotone_boolean_function n f
\<inter> simplicial_complex_induced_by_monotone_boolean_function n g"
(is "?sc n (?bf_and n f g) = ?sc n f \<inter> ?sc n g")
proof
show "?sc n f \<inter> ?sc n g \<subseteq> ?sc n (?bf_and n f g)"
proof
fix \<sigma> :: "nat set"
assume "\<sigma> \<in> (?sc n f \<inter> ?sc n g)"
hence sigma: "\<sigma> \<in> ?sc n f \<and> \<sigma> \<in> ?sc n g" by auto
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
\<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
proof -
from sigma have sigmaf: "\<sigma> \<in> ?sc n f" and sigmag: "\<sigma> \<in> ?sc n g"
by auto
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
using simplicial_complex.simplicial_complex_implies_true [OF sigmaf] .
moreover have "g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
using simplicial_complex.simplicial_complex_implies_true [OF sigmag] .
ultimately show ?thesis by fast
qed
thus "\<sigma> \<in> ?sc n (?bf_and n f g)"
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
unfolding bool_fun_and_def
using sigma apply auto
by (smt (z3) Collect_cong ceros_of_boolean_input_def dim_vec index_vec mem_Collect_eq
simplicial_complex.bool_vec_from_simplice_def
simplicial_complex_induced_by_monotone_boolean_function_def)
qed
next
show "?sc n (?bf_and n f g) \<subseteq> ?sc n f \<inter> ?sc n g"
proof
fix \<sigma> :: "nat set"
assume sigma: "\<sigma> \<in> ?sc n (?bf_and n f g)"
hence "bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
unfolding simplicial_complex.bool_vec_from_simplice_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
unfolding ceros_of_boolean_input_def
by auto (smt (verit) dim_vec eq_vecI index_vec)+
hence "(f (simplicial_complex.bool_vec_from_simplice n \<sigma>))
\<and> (g (simplicial_complex.bool_vec_from_simplice n \<sigma>))"
unfolding bool_fun_and_def
by auto
hence "\<sigma> \<in> ?sc n f \<and> \<sigma> \<in> ?sc n g"
using bool_fun_and_def sigma simplicial_complex_induced_by_monotone_boolean_function_def by auto
thus "\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f
\<inter> simplicial_complex_induced_by_monotone_boolean_function n g"
by auto
qed
qed
definition bool_fun_ast :: "(nat \<times> nat) \<Rightarrow> (bool vec \<Rightarrow> bool) \<times> (bool vec \<Rightarrow> bool)
\<Rightarrow> (bool vec \<times> bool vec \<Rightarrow> bool)"
where "(bool_fun_ast n f) \<equiv> (\<lambda> (x,y). (fst f x) \<and> (snd f y))"
definition
simplicial_complex_induced_by_monotone_boolean_function_ast
:: "(nat \<times> nat) \<Rightarrow> ((bool vec \<times> bool vec \<Rightarrow> bool)) \<Rightarrow> (nat set * nat set) set"
where "simplicial_complex_induced_by_monotone_boolean_function_ast n f =
{z. \<exists>x y. dim_vec x = fst n \<and> dim_vec y = snd n \<and> f (x, y)
\<and> ((ceros_of_boolean_input x), (ceros_of_boolean_input y)) = z}"
lemma fst_es_simplice:
"a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f
\<Longrightarrow> (\<exists>x y. f (x, y) \<and> (ceros_of_boolean_input x) = fst(a))"
by (smt (verit) fst_conv mem_Collect_eq
simplicial_complex_induced_by_monotone_boolean_function_ast_def)
lemma snd_es_simplice:
"a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f
\<Longrightarrow> (\<exists>x y. f (x, y) \<and> (ceros_of_boolean_input y) = snd(a))"
by (smt (verit) snd_conv mem_Collect_eq
simplicial_complex_induced_by_monotone_boolean_function_ast_def)
definition set_ast :: "(nat set) set \<Rightarrow> (nat set) set \<Rightarrow> ((nat set*nat set) set)"
where "set_ast A B \<equiv> {c. \<exists>a\<in>A. \<exists>b\<in>B. c = (a,b)}"
definition set_fst :: "(nat*nat) set \<Rightarrow> nat set"
where "set_fst AB = {a. \<exists>ab\<in>AB. a = fst ab}"
lemma set_fst_simp [simp]:
assumes "y \<noteq> {}"
shows "set_fst (x \<times> y) = x"
proof
show "set_fst (x \<times> y) \<subseteq> x"
by (smt (verit) SigmaE mem_Collect_eq prod.sel(1) set_fst_def subsetI)
show "x \<subseteq> set_fst (x \<times> y)"
proof
fix a::"nat"
assume "a \<in> x"
then obtain b where "b \<in> y" and "(a,b) \<in> (x\<times>y)"
using assms by blast
then show "a \<in> set_fst (x \<times> y)"
using set_fst_def by fastforce
qed
qed
definition set_snd :: "(nat*nat) set \<Rightarrow> nat set"
where "set_snd AB = {b. \<exists>ab\<in>AB. b = snd(ab)}"
lemma
simplicial_complex_ast_implies_fst_true:
assumes "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast nn
(bool_fun_ast nn f)"
shows "fst f (simplicial_complex.bool_vec_from_simplice (fst nn) (fst \<gamma>))"
using assms
unfolding simplicial_complex.bool_vec_from_simplice_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
unfolding bool_fun_ast_def
unfolding ceros_of_boolean_input_def
apply auto
by (smt (verit, ccfv_threshold) bool_fun_ast_def case_prod_conv dim_vec index_vec vec_eq_iff)
lemma
simplicial_complex_ast_implies_snd_true:
assumes "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast nn
(bool_fun_ast nn f)"
shows "snd f (simplicial_complex.bool_vec_from_simplice (snd nn) (snd \<gamma>))"
using assms
unfolding simplicial_complex.bool_vec_from_simplice_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
unfolding bool_fun_ast_def
unfolding ceros_of_boolean_input_def
by auto (smt (verit, ccfv_threshold) bool_fun_ast_def
case_prod_conv dim_vec index_vec vec_eq_iff)
lemma eq_ast:
"simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
= set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
(simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
proof
show "set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
(simplicial_complex_induced_by_monotone_boolean_function m (snd f))
\<subseteq> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
(bool_fun_ast (n, m) f)"
proof
fix \<gamma>::"nat set*nat set"
assume pert: "\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
(simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
hence f: "(fst \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
unfolding set_ast_def
by auto
have sigma: "fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))"
using simplicial_complex.simplicial_complex_implies_true [OF f] .
from pert have g: "(snd \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
unfolding set_ast_def by auto
have tau: "(snd f) (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))"
using simplicial_complex.simplicial_complex_implies_true [OF g] .
from sigma and tau have sigtau: "bool_fun_ast (n, m) f
((simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)),
(simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)))"
unfolding bool_fun_ast_def
by auto
from sigtau
show "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
(bool_fun_ast (n, m) f)"
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
unfolding bool_fun_ast_def
using sigma apply auto
using f g simplicial_complex_induced_by_monotone_boolean_function_def by fastforce
qed
next
show "simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
(bool_fun_ast (n, m) f)
\<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
(simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
proof
fix \<gamma> :: "nat set*nat set"
assume pert: "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
(bool_fun_ast (n, m) f)"
have sigma: "(fst \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
unfolding bool_fun_ast_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
apply auto
apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)"], safe)
using simplicial_complex.bool_vec_from_simplice_def apply auto[1]
apply (metis fst_conv pert simplicial_complex_ast_implies_fst_true)
using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
apply fastforce
using ceros_of_boolean_input_def pert
simplicial_complex.bool_vec_from_simplice_def
simplicial_complex_induced_by_monotone_boolean_function_ast_def by force
have tau: "(snd \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
unfolding bool_fun_ast_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
apply auto
apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)"], safe)
using simplicial_complex.bool_vec_from_simplice_def apply auto[1]
apply (metis snd_conv pert simplicial_complex_ast_implies_snd_true)
using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
apply fastforce
using ceros_of_boolean_input_def pert
simplicial_complex.bool_vec_from_simplice_def
simplicial_complex_induced_by_monotone_boolean_function_ast_def by force
from sigma and tau
show "\<gamma> \<in> set_ast
(simplicial_complex_induced_by_monotone_boolean_function n (fst f))
(simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
using set_ast_def
by force
qed
qed
end