Theory RelationOperators
section ‹Additional operators on relations, going beyond Relations.thy,
and properties of these operators›
theory RelationOperators
imports
SetUtils
"HOL-Library.Code_Target_Nat"
begin
subsection ‹Evaluating a relation as a function›
text ‹If an input has a unique image element under a given relation, return that element;
otherwise return a fallback value.›
fun eval_rel_or :: "('a × 'b) set ⇒ 'a ⇒ 'b ⇒ 'b"
where "eval_rel_or R a z = (let im = R `` {a} in if card im = 1 then the_elem im else z)"
text ‹right-uniqueness of a relation: the image of a @{const trivial} set (i.e.\ an empty or
singleton set) under the relation is trivial again.
This is the set-theoretical way of characterizing functions, as opposed to ‹λ› functions.›
definition runiq :: "('a × 'b) set ⇒ bool"
where "runiq R = (∀ X . trivial X ⟶ trivial (R `` X))"
subsection ‹Restriction›
text ‹restriction of a relation to a set (usually resulting in a relation with a smaller domain)›
definition restrict :: "('a × 'b) set ⇒ 'a set ⇒ ('a × 'b) set" (infix "||" 75)
where "R || X = (X × Range R) ∩ R"
text ‹extensional characterization of the pairs within a restricted relation›
lemma restrict_ext: "R || X = {(x, y) | x y . x ∈ X ∧ (x, y) ∈ R}"
unfolding restrict_def using Range_iff by blast
text ‹alternative statement of @{thm restrict_ext} without explicitly naming the pair's components›
lemma restrict_ext': "R || X = {p . fst p ∈ X ∧ p ∈ R}"
proof -
have "R || X = {(x, y) | x y . x ∈ X ∧ (x, y) ∈ R}" by (rule restrict_ext)
also have "… = { p . fst p ∈ X ∧ p ∈ R }" by force
finally show ?thesis .
qed
text ‹Restricting a relation to the empty set yields the empty set.›
lemma restrict_empty: "P || {} = {}"
unfolding restrict_def by simp
text ‹A restriction is a subrelation of the original relation.›
lemma restriction_is_subrel: "P || X ⊆ P"
using restrict_def by blast
text ‹Restricting a relation only has an effect within its domain.›
lemma restriction_within_domain: "P || X = P || (X ∩ (Domain P))"
unfolding restrict_def by fast
text ‹alternative characterization of the restriction of a relation to a singleton set›
lemma restrict_to_singleton: "P || {x} = {x} × (P `` {x})"
unfolding restrict_def by fast
subsection ‹Relation outside some set›
text ‹For a set-theoretical relation @{term R} and an ``exclusion'' set @{term X}, return those
tuples of @{term R} whose first component is not in @{term X}. In other words, exclude @{term X}
from the domain of @{term R}.›
definition Outside :: "('a × 'b) set ⇒ 'a set ⇒ ('a × 'b) set" (infix "outside" 75)
where "R outside X = R - (X × Range R)"
text ‹Considering a relation outside some set @{term X} reduces its domain by @{term X}.›
lemma outside_reduces_domain: "Domain (P outside X) = (Domain P) - X"
unfolding Outside_def by fast
text ‹Considering a relation outside a singleton set @{term "{x}"} reduces its domain by
@{term x}.›
corollary Domain_outside_singleton:
assumes "Domain R = insert x A"
and "x ∉ A"
shows "Domain (R outside {x}) = A"
using assms outside_reduces_domain by (metis Diff_insert_absorb)
text ‹For any set, a relation equals the union of its restriction to that set and its
pairs outside that set.›
lemma outside_union_restrict: "P = (P outside X) ∪ (P || X)"
unfolding Outside_def restrict_def by fast
text ‹The range of a relation @{term R} outside some exclusion set @{term X} is a
subset of the image of the domain of @{term R}, minus @{term X}, under @{term R}.›
lemma Range_outside_sub_Image_Domain: "Range (R outside X) ⊆ R `` (Domain R - X)"
using Outside_def Image_def Domain_def Range_def by blast
text ‹Considering a relation outside some set does not enlarge its range.›
lemma Range_outside_sub:
assumes "Range R ⊆ Y"
shows "Range (R outside X) ⊆ Y"
using assms outside_union_restrict by (metis Range_mono inf_sup_ord(3) subset_trans)
subsection ‹Flipping pairs of relations›
text ‹flipping a pair: exchanging first and second component›
definition flip where "flip tup = (snd tup, fst tup)"
text ‹Flipped pairs can be found in the converse relation.›
lemma flip_in_conv:
assumes "tup ∈ R"
shows "flip tup ∈ R¯"
using assms unfolding flip_def by simp
text ‹Flipping a pair twice doesn't change it.›
lemma flip_flip: "flip (flip tup) = tup"
by (metis flip_def fst_conv snd_conv surjective_pairing)
text ‹Flipping all pairs in a relation yields the converse relation.›
lemma flip_conv: "flip ` R = R¯"
proof -
have "flip ` R = { flip tup | tup . tup ∈ R }" by (metis image_Collect_mem)
also have "… = { tup . tup ∈ R¯ }" using flip_in_conv by (metis converse_converse flip_flip)
also have "… = R¯" by simp
finally show ?thesis .
qed
subsection ‹Evaluation as a function›
text ‹Evaluates a relation @{term R} for a single argument, as if it were a function.
This will only work if @{term R} is right-unique, i.e. if the image is always a singleton set.›
fun eval_rel :: "('a × 'b) set ⇒ 'a ⇒ 'b" (infix ",," 75)
where "R ,, a = the_elem (R `` {a})"
subsection ‹Paste›
text ‹the union of two binary relations @{term P} and @{term Q}, where pairs from @{term Q}
override pairs from @{term P} when their first components coincide.
This is particularly useful when P, Q are @{term runiq}, and one wants to preserve that property.›
definition paste (infix "+*" 75)
where "P +* Q = (P outside Domain Q) ∪ Q"
text ‹If a relation @{term P} is a subrelation of another relation @{term Q} on @{term Q}'s
domain, pasting @{term Q} on @{term P} is the same as forming their union.›
lemma paste_subrel:
assumes "P || Domain Q ⊆ Q"
shows "P +* Q = P ∪ Q"
unfolding paste_def using assms outside_union_restrict by blast
text ‹Pasting two relations with disjoint domains is the same as forming their union.›
lemma paste_disj_domains:
assumes "Domain P ∩ Domain Q = {}"
shows "P +* Q = P ∪ Q"
unfolding paste_def Outside_def using assms by fast
text ‹A relation @{term P} is equivalent to pasting its restriction to some set @{term X} on
@{term "P outside X"}.›
lemma paste_outside_restrict: "P = (P outside X) +* (P || X)"
proof -
have "Domain (P outside X) ∩ Domain (P || X) = {}"
unfolding Outside_def restrict_def by fast
moreover have "P = P outside X ∪ P || X" by (rule outside_union_restrict)
ultimately show ?thesis using paste_disj_domains by metis
qed
text ‹The domain of two pasted relations equals the union of their domains.›
lemma paste_Domain: "Domain(P +* Q)=Domain P∪Domain Q" unfolding paste_def Outside_def by blast
text ‹Pasting two relations yields a subrelation of their union.›
lemma paste_sub_Un: "P +* Q ⊆ P ∪ Q"
unfolding paste_def Outside_def by fast
text ‹The range of two pasted relations is a subset of the union of their ranges.›
lemma paste_Range: "Range (P +* Q) ⊆ Range P ∪ Range Q"
using paste_sub_Un by blast
end