Yiming Xu (Sep 26 2024 at 13:29): Yiming Xu (Sep 26 2024 at 13:29):Specifically: Given an n-ary relation R \subseteq W^n and a set X subseteq W. I want the closure of X generated from X in R. i.e. the smallest set X' such that X \subseteq X' and for all x1,...,xn, if x1 in X' and (x1,...,xn) in R, then all of x2,...,xn are in X'. Is there already a canonical way to obtain this set?
Yiming Xu (Sep 26 2024 at 13:29):If no obvious existing things, I will just do inductive relation.
Mathias Fleury (Sep 26 2024 at 13:50):Isn't that just ‹{(a,a). a ∈X} × R›?
Mathias Fleury (Sep 26 2024 at 13:50):up to that giving (x1, (x2, ..., xn))
Yiming Xu (Sep 26 2024 at 14:41):I am afraid I do not get it. Why does the closure condition hold? What I want is an "underlying set for the reflexive and transitive closure". If (x1,...,xn) in R and x1 in X', and if for xn we have (xn,v1,...,v_n-1) in R, then we include all the v's into X'. The product set is not even a subset of W (I am not searching for a subset of W^n).
Mathias Fleury (Sep 26 2024 at 14:47):When n=2, this is the transitive closure of R over all elements in X right?
Mathias Fleury (Sep 26 2024 at 15:02):This is what I understand from your description
context
fixes R :: ‹(('a × 'a × 'a) × ('a × 'a × 'a)) set› and X :: ‹'a set›
begin
definition my_rel where
‹my_rel = {(a,e). ∃b c d e f. ((a, b, c), (d, e, f)) ∈ R} ∪ {(a,f). ∃b c d e. ((a, b, c), (d, e, f)) ∈ R}›
definition my_set where
‹my_set = my_rel⇧*›
lemma
assumes ‹x1 ∈ X› and ‹((x1, x2,x3), (v1, v2, v3)) ∈ R›
shows ‹(x1, v2) ∈ my_set›
using assms by (fastforce simp: my_set_def my_rel_def)
end
Basically you are reinterpreting you predicate R as binary relation where every reachable tuple is reachable in your binary relation (my_rel) and then you do the transitive closure
Mathias Fleury (Sep 26 2024 at 15:04):I have never seen such concept before
Yiming Xu (Sep 26 2024 at 15:16):The R :: ‹(('a × 'a × 'a) × ('a × 'a × 'a)) set› seems to be a binary relation on tuples. Is this "R" already and re-interpretation? Sorry for my poor description if it is confusing. When n = 2, yes, it is the underlying set of the transitive closure (I will not bother with extending the relation in a proper way, but just want to get the "reachable points" from a n-ary predicate, that is why I emphasise "underlying set"). But for R :: ‹(('a × 'a × 'a) × ('a × 'a × 'a)) set›, it seems like R is already a binary relation on tuples, not an arbitrary relation. If this is my misunderstanding and this R is intended to be a 6-ary predicate instead, I still need some hints to get it.
Yiming Xu (Sep 26 2024 at 15:20):I do not intend to make "{(a,e). ∃b c d e f. ((a, b, c), (d, e, f)) ∈ R}" if R is a 3-ary relation:
In the case we have (a,b,c) in R and (b,c,e) in R, than yes, e can be reached from a. But (a,b,c) and (d,e,f) are not connected, so I do not want (a,e) to be included in the closure.
Mathias Fleury (Sep 26 2024 at 15:31):So:
context
fixes R :: ‹('a × 'a × 'a × 'a × 'a × 'a) set› and X :: ‹'a set›
begin
definition my_rel where
‹my_rel = {(a,e). ∃b c d e f. (a, b, c, d, e, f) ∈ R} ∪
{(a,c). ∃b d e f. (a, b, c, d, e, f) ∈ R} ∪
{(a,d). ∃b c e f. (a, b, c, d, e, f) ∈ R} ∪
{(a,e). ∃b c d f. (a, b, c, d, e, f) ∈ R} ∪
{(a,f). ∃b c d e . (a, b, c, d, e, f) ∈ R}›
definition my_set where
‹my_set = my_rell⇧+`` X›
lemma
assumes ‹x1 ∈ X› and ‹(x1, x2,x3, v1, v2, v3) ∈ R›
shows ‹(v2) ∈ my_set›
using assms by (auto intro!: bexI[of _ x1] simp: my_set_def my_rel_def Image_iff)
end
with proper usage of X now
Yiming Xu (Sep 26 2024 at 15:36):I think I see. A wise way to reuse instead of reinvent! I will check the details of the notational technology in your code when I encounter them! Many thanks!
Mathias Fleury (Sep 26 2024 at 15:37):The most important for notation: control-click to see the definitions
Yiming Xu (Sep 26 2024 at 15:39):Thank you! I am told about this, and recently find it is not always possible, but I believe it will work in this case!
Last updated: Dec 21 2024 at 16:20 UTC