(*
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 RelationProperties
imports
Main
HOLUtils
RelationUtils
RelationOperators
SetUtils
Finite_SetUtils
ListUtils
begin
section {* right-uniqueness *}
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. *}
definition runiq :: "('a \ 'b) set \ bool" where
"runiq R = (\ X . trivial X \ trivial (R `` X))"
text {* alternative characterisation of right-uniqueness: the image of a singleton set is
@{const trivial}, i.e.\ an empty or singleton set. *}
lemma runiq_alt: "runiq R \ (\ x . trivial (R `` {x}))"
(* CL: The following proof, found by Sledgehammer, takes 26 ms on my machine. *)
(* unfolding runiq_def by (metis Image_empty trivial_cases trivial_empty trivial_singleton) *)
proof
assume runiq: "runiq R"
show "\ x . trivial (R `` {x})"
proof
fix x::'a
have "trivial {x}" unfolding trivial_def by simp
with runiq show "trivial (R `` {x})" unfolding runiq_def by fast
qed
next
assume triv: "\ x . trivial (R `` {x})"
have "\ X::'a set . trivial X \ trivial (R `` X)"
proof (rule allImpI)
fix X::"'a set"
assume trivial: "trivial X"
then show "trivial (R `` X)"
proof (cases rule: trivial_cases)
case empty
then show ?thesis unfolding trivial_def by simp
next
case (singleton x)
with singleton triv show ?thesis by fast
qed
qed
then show "runiq R" unfolding runiq_def by fast
qed
text {* alternative characterisation of right-uniqueness: whenever two range elements are in
relation with a domain element, they are equal. *}
(* It is surprisingly hard (but possible) to prove this automatically, be it using/unfolding runiq_def, or using runiq_alt. *)
lemma runiq_basic: "runiq R \ (\ x y y' . (x, y) \ R \ (x, y') \ R \ y = y')"
proof
assume assm: "runiq R"
{
fix x y y'
assume x_R_y: "(x, y) \ R" and x_R_y': "(x, y') \ R"
(* then have "y = y'" using assms sledgehammer doesn't find anything within reasonable time *)
have "trivial (R `` {x})" using assm unfolding runiq_alt by simp
moreover have "y \ R `` {x}" using x_R_y by simp
moreover have "y' \ R `` {x}" using x_R_y' by simp
ultimately have "y = y'" by (rule trivial_imp_no_distinct)
}
then show "\ x y y' . (x, y) \ R \ (x, y') \ R \ y = y'" by force
next
assume assm: "\ x y y' . (x, y) \ R \ (x, y') \ R \ y = y'"
have "\ X::'a set . trivial X \ trivial (R `` X)"
proof (rule allImpI)
fix X::"'a set"
assume trivial: "trivial X"
then show "trivial (R `` X)"
proof (cases rule: trivial_cases)
case empty
then show ?thesis unfolding trivial_def by simp
next
case singleton
with assm have "\ y y' . y \ R `` X \ y' \ R `` X \ y = y'" by simp
then show ?thesis by (rule no_distinct_imp_trivial)
qed
qed
then show "runiq R" unfolding runiq_def by fast
qed
text {* an alternative definition of right-uniqueness in terms of @{const eval_rel} *}
lemma runiq_wrt_eval_rel:
fixes R :: "('a \ 'b) set"
shows "runiq R \ (\x . R `` {x} \ {R ,, x})"
unfolding runiq_alt trivial_def by simp
text {* An alternative phrasing of @{thm Image_within_domain'} for right-unique relations *}
lemma Image_within_runiq_domain:
fixes x R
assumes "runiq R"
shows "x \ Domain R \ (\ y . R `` {x} = {y})"
proof
assume "x \ Domain R"
then have Im_non_empty: "R `` {x} \ {}" by fast
have triv: "trivial (R `` {x})" using assms unfolding runiq_alt by simp
then show "\ y . R `` {x} = {y}"
proof (cases rule: trivial_cases)
case empty
with Im_non_empty show ?thesis ..
next
case (singleton y)
then show ?thesis by blast
qed
next
assume "\ y . R `` {x} = {y}"
then show "x \ Domain R" by auto
qed
text {* another alternative definition of right-uniqueness in terms of @{const eval_rel} *}
lemma runiq_wrt_eval_rel':
fixes R :: "('a \ 'b) set"
shows "runiq R \ (\x \ Domain R . R `` {x} = {R ,, x})"
(* CL: possible with Sledgehammer but takes very long *)
proof
assume runiq: "runiq R"
show "\x \ Domain R . R `` {x} = {R ,, x}"
proof
fix x assume x_Dom: "x \ Domain R"
show "R `` {x} = {R ,, x}"
proof
show "R `` {x} \ {R ,, x}" using runiq unfolding runiq_wrt_eval_rel by simp
next
show "{R ,, x} \ R `` {x}"
proof
fix y assume "y \ {R ,, x}"
moreover have "\ y . R `` {x} = {y}" using runiq x_Dom Image_within_runiq_domain by fast
ultimately show "y \ R `` {x}" by (metis RelationOperators.eval_rel.simps the_elem_eq)
qed
qed
qed
next
assume "\x \ Domain R . R `` {x} = {R ,, x}"
then have "\ x \ Domain R . trivial (R `` {x})" by (metis trivial_singleton)
moreover have "\ x . x \ Domain R \ trivial (R `` {x})" by (simp add: trivial_empty Image_within_domain')
ultimately have "\ x . trivial (R `` {x})" by blast
then show "runiq R" unfolding runiq_alt .
qed
(* using eval_rel.simps runiq_alt trivial_def Image_within_domain' empty_subsetI subset_refl the_elem_eq trivial_cases
sledgehammer min [e] (runiq_wrt_eval_rel Image_within_domain' RelationOperators.eval_rel.simps empty_subsetI runiq_alt subset_refl the_elem_eq trivial_cases *)
text {* A subrelation of a right-unique relation is right-unique. *}
lemma subrel_runiq:
fixes Q::"('a \ 'b) set"
and R::"('a \ 'b) set"
assumes runiq_sup: "runiq Q"
and subset: "R \ Q"
shows "runiq R"
unfolding runiq_def
proof (rule allImpI)
fix X::"'a set"
assume "trivial X"
then have "trivial (Q `` X)" using runiq_sup unfolding runiq_def by fast
then show "trivial (R `` X)" using subset by (metis (full_types) Image_mono equalityE trivial_subset)
qed
text {* If two right-unique relations have disjoint domains, their union is right-unique too. *}
lemma disj_Un_runiq:
fixes P::"('a \ 'b) set"
and Q::"('a \ 'b) set"
assumes runiq_P: "runiq P"
and runiq_Q: "runiq Q"
and disj_Dom: "Domain P \ Domain Q = {}"
shows "runiq (P \ Q)"
proof -
have "\ x . trivial ((P \ Q) `` {x})"
proof
fix x
have triv_Im_P: "trivial (P `` {x})" using runiq_P runiq_alt by fast
have triv_Im_Q: "trivial (Q `` {x})" using runiq_Q runiq_alt by fast
have "(P \ Q) `` {x} = P `` {x} \ Q `` {x}" by fast
with disj_Dom have "(P \ Q) `` {x} = P `` {x} \ (P \ Q) `` {x} = Q `` {x}" by blast
then show "trivial ((P \ Q) `` {x})" using triv_Im_P triv_Im_Q by force
qed
then show ?thesis using runiq_alt by fast
qed
text {* A singleton relation is right-unique. *}
lemma runiq_singleton_rel: "runiq {(x, y)}" (is "runiq ?R")
unfolding runiq_def
proof (rule allImpI)
fix X::"'a set"
assume "trivial X"
then show "trivial (?R `` X)"
proof (cases rule: trivial_cases)
case empty
then show ?thesis unfolding trivial_def by simp
next
case (singleton z)
show ?thesis
proof (cases "x = z")
case True
then have "?R `` {z} = {y}" by fast
with singleton show ?thesis by (simp add: trivial_singleton)
next
case False
then have "?R `` {z} = {}" by blast
with singleton show ?thesis by (simp add: trivial_empty)
qed
qed
qed
text {* A trivial relation is right-unique *}
lemma runiq_trivial_rel:
assumes "trivial R"
shows "runiq R"
using assms runiq_singleton_rel by (metis subrel_runiq surj_pair trivial_def)
text {* The empty relation is right-unique *}
lemma runiq_emptyrel: "runiq {}" using trivial_empty runiq_trivial_rel by blast
text {* alternative characterisation of the fact that, if a relation @{term R} is right-unique,
its evaluation @{term "R,,x"} on some argument @{term x} in its domain, occurs in @{term R}'s
range. *}
lemma eval_runiq_rel:
assumes domain: "x \ Domain R"
and runiq: "runiq R"
shows "(x, R,,x) \ R"
proof -
have "trivial (R `` {x})" using runiq unfolding runiq_alt by fast
then show ?thesis
proof (cases rule: trivial_cases)
case empty
with domain have False by fast
then show ?thesis ..
next
case (singleton y)
then have "R ,, x = y" by simp
with singleton show ?thesis by blast
qed
qed
text {* The image of a singleton set under a right-unique relation is a singleton set. *}
lemma Image_runiq_eq_eval:
assumes "x \ Domain R"
and "runiq R"
shows "R `` {x} = {R ,, x}"
using assms unfolding runiq_wrt_eval_rel by blast
text {* The image of the domain of a right-unique relation @{term R} under @{term R}
is the image of the domain under the function that corresponds to the relation. *}
lemma runiq_imp_eval_eq_Im:
assumes "runiq R"
shows "R `` Domain R = (eval_rel R) ` Domain R"
proof -
have "R `` Domain R = { y . \ x \ Domain R . (x, y) \ R }" by (rule Image_def)
also have "\ = { y . \ x \ Domain R . y \ R `` {x} }" by simp
also have "\ = { y . \ x \ Domain R . y \ {R ,, x} }"
proof -
from assms have "\ x \ Domain R . R `` {x} = {R ,, x}" unfolding runiq_wrt_eval_rel' .
then have "\ y . \ x \ Domain R . y \ R `` {x} \ y \ {R ,, x}" by blast
then show ?thesis by (auto simp: Collect_mono)
qed
also have "\ = { y . \ x \ Domain R . y = the_elem (R `` {x}) }" by simp
also have "\ = { y . \ x \ Domain R . y = R ,, x }" by simp
also have "\ = (eval_rel R) ` Domain R" by (simp add: image_def)
finally show ?thesis .
qed
text {* The cardinality of the range of a finite, right-unique relation is less or equal the
cardinality of its domain. *}
lemma card_Range_le_Domain:
assumes finite_Domain: "finite (Domain R)"
and runiq: "runiq R"
shows "card (Range R) \ card (Domain R)"
proof -
have "Range R = R `` Domain R" by blast
also have "\ = (eval_rel R) ` Domain R" using runiq by (rule runiq_imp_eval_eq_Im)
finally have "Range R = (eval_rel R) ` Domain R" .
then show ?thesis using finite_Domain by (metis card_image_le)
qed
text {* right-uniqueness of a restricted relation expressed using basic set theory *}
lemma runiq_restrict: "runiq (R || X) \ (\ x \ X . \ y y' . (x, y) \ R \ (x, y') \ R \ y = y')"
proof -
have "runiq (R || X) \ (\ x y y' . (x, y) \ R || X \ (x, y') \ R || X \ y = y')"
by (rule runiq_basic)
also have "\ \ (\ x y y' . (x, y) \ { p . fst p \ X \ p \ R } \ (x, y') \ { p . fst p \ X \ p \ R } \ y = y')"
using restrict_ext' by blast
also have "\ \ (\ x \ X . \ y y' . (x, y) \ R \ (x, y') \ R \ y = y')" by auto
finally show ?thesis .
qed
subsection {* paste *}
text {* Pasting @{term Q} on @{term P} yields a right-unique relation if @{term Q} is
right-unique, and @{term P} is right-unique outside @{term Q}'s domain. *}
lemma runiq_paste1:
fixes P::"('a \ 'b) set"
and Q::"('a \ 'b) set"
assumes "runiq Q"
and "runiq (P outside Domain Q)" (is "runiq ?PoutsideQ")
shows "runiq (P +* Q)"
proof -
have paste_sub: "P +* Q \ (Q \ ?PoutsideQ)" unfolding paste_def by simp
have "Domain Q \ Domain ?PoutsideQ = {}"
using outside_reduces_domain by (metis Diff_disjoint)
with assms have "runiq (Q \ ?PoutsideQ)" by (rule disj_Un_runiq)
then show ?thesis using paste_sub by (rule subrel_runiq)
qed
text {* Pasting two right-unique relations yields a right-unique relation. *}
corollary runiq_paste2:
assumes "runiq Q"
and "runiq P"
shows "runiq (P +* Q)"
using assms runiq_paste1 subrel_runiq
by (metis Diff_subset Outside_def)
text {* Pasting a singleton relation on some other right-unique relation @{term R} yields a
right-unique relation if the single element of the singleton's domain is not yet in the
domain of @{term R}. *}
lemma runiq_paste3:
assumes "runiq R"
and "x \ Domain R"
shows "runiq (R +* {(x, y)})"
using assms runiq_paste2 runiq_singleton_rel by metis
subsection {* converse *}
text {* The inverse image of the image of a singleton set under some relation is the same
singleton set, if both the relation and its converse are right-unique and the singleton set
is in the relation's domain. *}
lemma converse_Image_singleton_Domain:
assumes runiq: "runiq R"
and runiq_conv: "runiq (R\)"
and domain: "x \ Domain R"
shows "R\ `` R `` {x} = {x}"
proof -
have sup: "{x} \ R\ `` R `` {x}" using Domain_Int_wrt_converse domain by fast
have "trivial (R `` {x})" using runiq domain by (metis runiq_def trivial_singleton)
then have "trivial (R\ `` R `` {x})"
using assms runiq_def by blast
then show ?thesis
using sup by (metis singleton_sub_trivial_uniq subset_antisym trivial_def)
qed
text {* The inverse image of the image of a singleton set under some relation is the same
singleton set or empty, if both the relation and its converse are right-unique. *}
corollary converse_Image_singleton:
assumes "runiq R"
and "runiq (R\)"
shows "R\ `` R `` {x} \ {x}"
using assms converse_Image_singleton_Domain
by (metis Image_empty Image_within_domain' empty_subsetI set_eq_subset)
text {* The inverse image of the image of a set under some relation is a subset of that set,
if both the relation and its converse are right-unique. *}
lemma converse_Image:
assumes runiq: "runiq R"
and runiq_conv: "runiq (R\)"
shows "R\ `` R `` X \ X"
proof -
have "(R O R\) `` X = (\x \ X . (R O R\) `` {x})" by (rule Image_eq_UN)
also have "\ = (\x\X. R\ `` R `` {x})" by blast
also have "\ \ (\x \ X. {x})" using converse_Image_singleton assms by fast
also have "\ = X" by simp
finally show ?thesis by fast
qed
text {* The inverse statement of @{thm disj_Image_imp_disj_Domain} holds when both the
relation and its converse are right-unique. *}
lemma disj_Domain_imp_disj_Image: assumes "Domain R \ X \ Y = {}"
assumes "runiq R"
and "runiq (R\)"
shows "R `` X \ R `` Y = {}"
proof -
let ?X_on_Dom = "Domain R \ X"
let ?Y_on_Dom = "Domain R \ Y"
have "R\ `` (R `` ?X_on_Dom) \ ?X_on_Dom" using converse_Image assms by fast
moreover have "R\ `` (R `` ?Y_on_Dom) \ ?Y_on_Dom" using converse_Image assms by metis
ultimately have "R\ `` R `` ?X_on_Dom \ R\ `` R `` ?Y_on_Dom \ {}" using assms by blast
moreover have "?X_on_Dom \ ?Y_on_Dom = {}" using assms by blast
ultimately
have "{} = Domain (R\) \ R `` ?X_on_Dom \ R `` ?Y_on_Dom"
using disj_Image_imp_disj_Domain by fast
also have "\ = Range R \ R `` ?X_on_Dom \ R `` ?Y_on_Dom" using Domain_converse by metis
also have "\ = R `` ?X_on_Dom \ R `` ?Y_on_Dom" by blast
finally show ?thesis by auto
qed
text {* The converse relation of two pasted relations is right-unique, if
the relations have disjoint domains and ranges, and if their converses are both
right-unique. *}
lemma runiq_converse_paste:
assumes runiq_P_conv: "runiq (P\)"
and runiq_Q_conv: "runiq (Q\)"
and disj_D: "Domain P \ Domain Q = {}"
and disj_R: "Range P \ Range Q = {}"
shows "runiq ((P +* Q)\)"
proof -
have "P +* Q = P \ Q" using disj_D by (rule paste_disj_domains)
then have "(P +* Q)\ = P\ \ Q\" by auto
also have "\ = P\ +* Q\" using disj_R paste_disj_domains Domain_converse by metis
finally show ?thesis using runiq_P_conv runiq_Q_conv runiq_paste2 by auto
qed
text {* The converse relation of a singleton relation pasted on some other relation @{term R} is right-unique,
if the singleton pair is not in @{term "Domain R \ Range R"}, and if @{term "R\"} is right-unique. *}
lemma runiq_converse_paste_singleton:
assumes runiq: "runiq (R\)"
and y_notin_R: "y \ Range R"
and x_notin_D: "x \ Domain R"
shows "runiq ((R +* {(x,y)})\)"
proof -
have "{(x,y)}\ = {(y,x)}" by fastforce
then have "runiq ({(x,y)}\)" using runiq_singleton_rel by metis
moreover have "Domain R \ Domain {(x,y)} = {}" and "Range R \ (Range {(x,y)})={}"
using y_notin_R x_notin_D by simp_all
ultimately show ?thesis using runiq runiq_converse_paste by blast
qed
section {* injectivity *}
text {* A relation @{term R} is injective on its domain iff any two domain elements having the same image
are equal. This definition on its own is of limited utility, as it does not assume that @{term R}
is a function, i.e.\ right-unique. *}
definition injective :: "('a \ 'b) set \ bool"
where "injective R \ (\ a \ Domain R . \ b \ Domain R . R `` {a} = R `` {b} \ a = b)"
text {* If both a relation and its converse are right-unique, it is injective on its domain. *}
lemma runiq_and_conv_imp_injective:
assumes runiq: "runiq R"
and runiq_conv: "runiq (R \)"
shows "injective R"
proof -
{
fix a assume a_Dom: "a \ Domain R"
fix b assume b_Dom: "b \ Domain R"
have "R `` {a} = R `` {b} \ a = b"
proof
assume eq_Im: "R `` {a} = R `` {b}"
from runiq a_Dom obtain Ra where Ra: "R `` {a} = {Ra}" by (metis Image_runiq_eq_eval)
from runiq b_Dom obtain Rb where Rb: "R `` {b} = {Rb}" by (metis Image_runiq_eq_eval)
from eq_Im Ra Rb have eq_Im': "Ra = Rb" by simp
from eq_Im' Ra a_Dom runiq_conv have a': "(R \) `` {Ra} = {a}"
using converse_Image_singleton_Domain runiq by metis
from eq_Im' Rb b_Dom runiq_conv have b': "(R \) `` {Rb} = {b}"
using converse_Image_singleton_Domain runiq by metis
from eq_Im' a' b' show "a = b" by simp
qed
}
then show ?thesis unfolding injective_def by blast
qed
text {* the set of all injective functions from @{term X} to @{term Y}. *}
definition injections :: "'a set \ 'b set \ ('a \ 'b) set set"
where "injections X Y = {R . Domain R = X \ Range R \ Y \ runiq R \ runiq (R\)}"
text {* the set of all injective partial functions (including total ones) from @{term X} to @{term Y}. *}
definition partial_injections :: "'a set \ 'b set \ ('a \