(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Marco B. Caminati http://caminati.co.nr * Manfred Kerber <mnfrd.krbr@gmail.com> * Christoph Lange <math.semantic.web@gmail.com> * Colin Rowat <c.rowat@bham.ac.uk> 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) *) section ‹Additional properties of relations, and operators on relations, as they have been defined by Relations.thy› theory RelationProperties imports RelationOperators begin subsection ‹Right-Uniqueness› (* flip is applied to pairs so that (flip (x, y)) = (y, x) *) lemma injflip: "inj_on flip A" by (metis flip_flip inj_on_def) lemma lm01: "card P = card (P^-1)" using card_image flip_conv injflip by metis lemma cardinalityOneTheElemIdentity: "(card X = 1) = (X={the_elem X})" by (metis One_nat_def card_Suc_eq card.empty empty_iff the_elem_eq) lemma lm02: "trivial X = (X={} ∨ card X=1)" using cardinalityOneTheElemIdentity order_refl subset_singletonD trivial_def trivial_empty by (metis(no_types)) lemma lm03: "trivial P = trivial (P^-1)" using trivial_def subset_singletonD subset_refl subset_insertI cardinalityOneTheElemIdentity converse_inject converse_empty lm01 by metis (* The range of P restricted to X is equal to the image of X through P *) lemma restrictedRange: "Range (P||X) = P``X" unfolding restrict_def by blast lemma doubleRestriction: "((P || X) || Y) = (P || (X ∩ Y))" unfolding restrict_def by fast lemma restrictedDomain: "Domain (R||X) = Domain R ∩ X" using restrict_def by fastforce text ‹A subrelation of a right-unique relation is right-unique.› lemma subrel_runiq: assumes "runiq Q" "P ⊆ Q" shows "runiq P" using assms runiq_def by (metis Image_mono subsetI trivial_subset) lemma rightUniqueInjectiveOnFirstImplication: assumes "runiq P" shows "inj_on fst P" unfolding inj_on_def using assms runiq_def trivial_def trivial_imp_no_distinct the_elem_eq surjective_pairing subsetI Image_singleton_iff by (metis(no_types)) text ‹alternative characterization of right-uniqueness: the image of a singleton set is @{const trivial}, i.e.\ an empty or a singleton set.› lemma runiq_alt: "runiq R ⟷ (∀ x . trivial (R `` {x}))" unfolding runiq_def by (metis Image_empty2 trivial_empty_or_singleton trivial_singleton) text ‹an alternative definition of right-uniqueness in terms of @{const eval_rel}› (* Note that R `` {x} is the image of {x} under R and R ,, x gives you an element y such that R x y. Because of right-uniqueness in this case the element is determined, otherwise it may be undetermined *) lemma runiq_wrt_eval_rel: "runiq R = (∀x . R `` {x} ⊆ {R ,, x})" by (metis eval_rel.simps runiq_alt trivial_def) lemma rightUniquePair: assumes "runiq f" assumes "(x,y)∈f" shows "y=f,,x" using assms runiq_wrt_eval_rel subset_singletonD Image_singleton_iff equals0D singletonE by fast lemma runiq_basic: "runiq R ⟷ (∀ x y y' . (x, y) ∈ R ∧ (x, y') ∈ R ⟶ y = y')" unfolding runiq_alt trivial_same by blast lemma rightUniqueFunctionAfterInverse: assumes "runiq f" shows "f``(f^-1``Y) ⊆ Y" using assms runiq_basic ImageE converse_iff subsetI by (metis(no_types)) lemma lm04: assumes "runiq f" "y1 ∈ Range f" shows "(f^-1 `` {y1} ∩ f^-1 `` {y2} ≠ {}) = (f^-1``{y1}=f^-1``{y2})" using assms rightUniqueFunctionAfterInverse by fast lemma converse_Image: assumes runiq: "runiq R" and runiq_conv: "runiq (R^-1)" shows "(R^-1) `` R `` X ⊆ X" using assms by (metis converse_converse rightUniqueFunctionAfterInverse) lemma lm05: assumes "inj_on fst P" shows "runiq P" unfolding runiq_basic using assms fst_conv inj_on_def old.prod.inject by (metis(no_types)) (* Another characterization of runiq, relating the set theoretical expression P to the injectivity of the function fst applied to P *) lemma rightUniqueInjectiveOnFirst: "(runiq P) = (inj_on fst P)" using rightUniqueInjectiveOnFirstImplication lm05 by blast lemma disj_Un_runiq: assumes "runiq P" "runiq Q" "(Domain P) ∩ (Domain Q) = {}" shows "runiq (P ∪ Q)" using assms rightUniqueInjectiveOnFirst fst_eq_Domain injection_union by metis lemma runiq_paste1: assumes "runiq Q" "runiq (P outside Domain Q)" shows "runiq (P +* Q)" unfolding paste_def using assms disj_Un_runiq Diff_disjoint Un_commute outside_reduces_domain by (metis (poly_guards_query)) corollary runiq_paste2: assumes "runiq Q" "runiq P" shows "runiq (P +* Q)" using assms runiq_paste1 subrel_runiq Diff_subset Outside_def by (metis) (* Let f be a function, then its graph {(x, f x)} and all its restrictions such that P x for arbitrary P are right-unique. *) lemma rightUniqueRestrictedGraph: "runiq {(x,f x)| x. P x}" unfolding runiq_basic by fast lemma rightUniqueSetCardinality: assumes "x ∈ Domain R" "runiq R" shows "card (R``{x})=1" using assms lm02 DomainE Image_singleton_iff empty_iff by (metis runiq_alt) 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" "runiq R" shows "R `` {x} = {R ,, x}" using assms rightUniqueSetCardinality by (metis eval_rel.simps cardinalityOneTheElemIdentity) lemma lm06: assumes "trivial f" shows "runiq f" using assms trivial_subset_non_empty runiq_basic snd_conv by fastforce text ‹A singleton relation is right-unique.› corollary runiq_singleton_rel: "runiq {(x, y)}" using trivial_singleton lm06 by fast text ‹The empty relation is right-unique› lemma runiq_emptyrel: "runiq {}" using trivial_empty lm06 by blast (* characterization of right-uniqueness with ∃! *) lemma runiq_wrt_ex1: "runiq R ⟷ (∀ a ∈ Domain R . ∃! b . (a, b) ∈ R)" using runiq_basic by (metis Domain.DomainI Domain.cases) text ‹alternative characterization 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. Note that we need runiq R in order to get a definite value for @{term "R,,x"}› lemma eval_runiq_rel: assumes domain: "x ∈ Domain R" and runiq: "runiq R" shows "(x, R,,x) ∈ R" using assms by (metis rightUniquePair runiq_wrt_ex1) text ‹Evaluating a right-unique relation as a function on the relation's domain yields an element from its range.› lemma eval_runiq_in_Range: assumes "runiq R" and "a ∈ Domain R" shows "R ,, a ∈ Range R" using assms by (metis Range_iff eval_runiq_rel) 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 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 images of two disjoint sets under an injective function are disjoint.› lemma disj_Domain_imp_disj_Image: assumes "Domain R ∩ X ∩ Y = {}" assumes "runiq R" and "runiq (R¯)" shows "(R `` X) ∩ (R `` Y) = {}" using assms unfolding runiq_basic by blast lemma runiq_converse_paste_singleton: assumes "runiq (P^-1)" "y∉(Range P)" shows "runiq ((P +* {(x,y)})¯)" (is "?u (?P^-1)") proof - have "(?P) ⊆ P ∪ {(x,y)}" using assms by (metis paste_sub_Un) then have "?P^-1 ⊆ P^-1 ∪ ({(x,y)}^-1)" by blast moreover have "... = P^-1 ∪ {(y,x)}" by fast moreover have "Domain (P^-1) ∩ Domain {(y,x)} = {}" using assms(2) by auto ultimately moreover have "?u (P^-1 ∪ {(y,x)})" using assms(1) by (metis disj_Un_runiq runiq_singleton_rel) ultimately show ?thesis by (metis subrel_runiq) qed subsection ‹Injectivity› text ‹The following is a classical definition of 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 following definition is a constructive (computational) characterization of the set of all injections X Y, represented by a list. That is, we define the list of all injective functions (represented as relations) from one set (represented as a list) to another set. We formally prove the equivalence of the constructive and the classical definition in Universes.thy.› fun injections_alg (* :: "'a list ⇒ 'b::linorder set ⇒ ('a × 'b) set list" *) where "injections_alg [] Y = [{}]" | "injections_alg (x # xs) Y = concat [ [ R +* {(x,y)} . y ← sorted_list_of_set (Y - Range R) ] . R ← injections_alg xs Y ]" (* We need this as a list in order to be able to iterate over it. It would be easy to provide an alternative of type ('a × 'b) set set, by using ⋃ and set comprehension. *) lemma Image_within_domain': fixes x R shows "(x ∈ Domain R) = (R `` {x} ≠ {})" by blast end