(* 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) *) header {* Additional material that we would have expected in Relation.thy *} theory RelationUtils imports Relation begin section {* Domain *} text{* If a relation is left-total on a set @{term A}, its superrelations are left-total on @{term A} too. *} lemma suprel_left_total_on: fixes R :: "('a \ 'b) set" and S :: "('a \ 'b) set" and A :: "'a set" assumes "A \ Domain R" and "R \ Q" shows "A \ Domain Q" using assms by fast section {* Image *} text {* The image of a relation is only effective within the domain of that relation *} lemma Image_within_domain: "R `` X = R `` (X \ Domain R)" by fast text {* An alternative phrasing of @{thm Image_within_domain} *} lemma Image_within_domain': fixes x R shows "x \ Domain R \ R `` {x} \ {}" using Image_within_domain by blast text {* The image of a set outside a relation's domain under that domain is empty. *} lemma Image_outside_domain: fixes X::"'a set" and R::"('a \ 'b) set" shows "X \ Domain R = {} \ R `` X = {}" using Image_within_domain by blast text {* If the images of two sets @{term X} and @{term Y} under a relation @{term R} are disjoint, @{term X} and @{term Y} are disjoint on the domain of @{term R}. *} lemma disj_Image_imp_disj_Domain: assumes "R `` X \ R `` Y = {}" shows "Domain R \ X \ Y = {}" using assms by auto section {* Converse *} text {* alternative characterisation of the intersection of a relation's domain with some set, in terms of the converse relation *} lemma Domain_Int_wrt_converse: "Domain R \ X \ R\ `` (R `` X)" by fast end