(*
Auction Theory Toolbox (http://formare.github.io/auctions/)
Authors:
* Marco B. Caminati
* Christoph Lange
Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)
theory RelationOperators
imports
Main
begin
section {* restriction *}
text {* restriction of a relation to a set (usually resulting in a relation with a smaller domain) *}
definition restrict
(* TODO MC: compare with restr in SchorrWaite.thy
CL@MC: doesn't seem helpful, as its type "('a \ 'a) set \ ('a \ bool) \ ('a \ 'a) set" is
more specific than what we need. *)
:: "('a \ 'b) set \ 'a set \ ('a \ 'b) set" (infix "||" 75)
where "R || X = X \ Range R \ R"
text {* extensional characterisation 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
(* CL: This proof seems impossible for sledgehammer. Range_iff is not a simp rule. I managed
to arrive at this point after painfully rewriting the set comprehension in very small steps,
only to see that most of these steps could be proved 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 characterisation of the restriction of a relation to a singleton set *}
lemma restrict_to_singleton: "P || {x} = {x} \ P `` {x}"
unfolding restrict_def by fast
section {* 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) (* MC: 75 or whatever, for what I know *)
where "Outside R 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
using 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 doesn't enlarge its range. *}
lemma Range_outside_sub:
assumes "Range R \ Y"
shows "Range (R outside X) \ Y"
using assms
using outside_union_restrict
by (metis Range_mono inf_sup_ord(3) subset_trans)
section {* 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 a total function, i.e. if the image is always a singleton set. *}
fun eval_rel :: "('a \ 'b) set \ 'a \ 'b" (infix ",," 75) (* . (Mizar's notation) confuses Isar *)
where "eval_rel R a = the_elem (R `` {a})"
section {* 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 *}
definition paste (infix "+*" 75)
where "P +* Q = (P outside Domain Q) \ Q"
(* Avoids possible conflicts btw P & Q using `outside',
thus giving precedence to Q. This is particularly useful when
P, Q are functions, and one wants to preserve that property. *)
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