Theory RelationProperties

(*
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