Theory Universes

(*
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 ‹Sets of injections, partitions, allocations expressed as suitable subsets of the corresponding universes›

theory Universes

imports 
"HOL-Library.Code_Target_Nat"
StrictCombinatorialAuction 
"HOL-Library.Indicator_Function"

begin

subsection ‹Preliminary lemmas›

lemma lm001: 
  assumes "Y ∈ set (all_partitions_alg X)" 
  shows "distinct Y"
  using assms distinct_sorted_list_of_set all_partitions_alg_def all_partitions_equivalence'
  by metis

(* This is a variant of the bridging theorem that the classical and constructive definitions of all_partitions characterize the same set *)
lemma lm002: 
  assumes "finite G" 
  shows "all_partitions G  =  set ` (set (all_partitions_alg G))"
  using assms sortingSameSet all_partitions_alg_def all_partitions_paper_equiv_alg
        distinct_sorted_list_of_set image_set 
  by metis




subsection ‹Definitions of various subsets of @{term UNIV}.›

(* For with R = {({1,2},2), ({2,3},3)} is a choice relation, choosing one element of the set. *)
abbreviation "isChoice R == ∀x. R``{x} ⊆ x"
abbreviation "partitionsUniverse == {X. is_non_overlapping X}"
lemma "partitionsUniverse ⊆ Pow UNIV" 
  by simp       

abbreviation "partitionValuedUniverse == ⋃ P ∈ partitionsUniverse. Pow (UNIV × P)"
lemma "partitionValuedUniverse ⊆ Pow (UNIV × (Pow UNIV))" 
  by simp

abbreviation "injectionsUniverse == {R. (runiq R) & (runiq (R^-1))}"

(* allocations are injections so that goods are allocated at most once and the range from a partition of the goods. *)
abbreviation "allocationsUniverse == injectionsUniverse ∩ partitionValuedUniverse"
abbreviation "totalRels X Y == {R. Domain R = X & Range R ⊆ Y}"




subsection ‹Results about the sets defined in the previous section›

lemma lm003: 
  assumes "∀ x1 ∈ X. (x1 ≠ {} & (∀ x2 ∈ X-{x1}. x1 ∩ x2  =  {}))" 
  shows "is_non_overlapping X" 
  unfolding is_non_overlapping_def using assms by fast

lemma lm004: 
  assumes "∀x ∈ X. f x ∈ x" 
  shows "isChoice (graph X f)" 
  using assms
  by (metis Image_within_domain' empty_subsetI insert_subset graphEqImage domainOfGraph 
            runiq_wrt_eval_rel subset_trans)

lemma lm006: "injections X Y ⊆ injectionsUniverse" 
  using injections_def by fast

lemma lm007: "injections X Y ⊆ injectionsUniverse" 
  using injections_def by blast

lemma lm008: "injections X Y = totalRels X Y ∩ injectionsUniverse" 
  using injections_def by (simp add: Collect_conj_eq Int_assoc)

lemma allocationInverseRangeDomainProperty: 
  assumes "a ∈ allAllocations N G" 
  shows  "a^-1 ∈ injections (Range a) N & 
          (Range a) partitions G & 
          Domain a ⊆ N" 
  unfolding injections_def using assms all_partitions_def injections_def by fastforce

lemma lm009: 
  assumes "is_non_overlapping XX" "YY ⊆ XX" 
  shows "(XX - YY) partitions (⋃ XX - ⋃ YY)"
proof -
  let ?xx="XX - YY" let ?X="⋃ XX" let ?Y="⋃ YY"
  let ?x="?X - ?Y"
  have "∀ y ∈ YY. ∀ x∈?xx. y ∩ x={}" using assms is_non_overlapping_def 
       by (metis Diff_iff rev_subsetD)
  then have "⋃ ?xx ⊆ ?x" using assms by blast
  then have "⋃ ?xx = ?x" by blast
  moreover have "is_non_overlapping ?xx" using subset_is_non_overlapping 
       by (metis Diff_subset assms(1))
  ultimately
  show ?thesis using is_partition_of_def by blast
qed

lemma allocationRightUniqueRangeDomain: 
  assumes "a ∈ possible_allocations_rel G N" 
  shows "runiq a & 
         runiq (a¯) & 
         (Domain a) partitions G & 
         Range a ⊆ N" 
proof -
  obtain Y where
  0: "a ∈ injections Y N & Y ∈ all_partitions G" using assms by auto
  show ?thesis using 0 injections_def all_partitions_def mem_Collect_eq by fastforce
qed

(* converse of the previous lemma *)
lemma lm010: 
  assumes "runiq a" "runiq (a¯)" "(Domain a) partitions G" "Range a ⊆ N"
  shows "a ∈ possible_allocations_rel G N"
proof -
  have "a ∈ injections (Domain a) N" unfolding injections_def 
    using assms(1) assms(2)  assms(4) by blast
  moreover have "Domain a ∈ all_partitions G" using assms(3) all_partitions_def by fast
  ultimately show ?thesis using assms(1) by auto
qed

(* lemma allocationRightUniqueRangeDomain and lm010 combined *)
lemma allocationProperty: 
  "a ∈ possible_allocations_rel G N ⟷
   runiq a & runiq (a¯) & (Domain a) partitions G & Range a ⊆ N"
  using allocationRightUniqueRangeDomain lm010 by blast

lemma lm011: 
  "possible_allocations_rel' G N ⊆ injectionsUniverse"
  using injections_def by force

lemma lm012: 
  "possible_allocations_rel G N ⊆ {a. (Range a) ⊆ N & (Domain a) ∈ all_partitions G}"
  using injections_def by fastforce

lemma lm013: 
  "injections X Y = injections X Y" 
  using injections_def by metis

lemma lm014: 
  "all_partitions X = all_partitions' X" 
  using all_partitions_def is_partition_of_def by auto

lemma lm015: 
  "possible_allocations_rel' A B  =  possible_allocations_rel A B" 
  (is "?A=?B")
proof -
  have "?B=⋃ { injections Y B | Y . Y ∈ all_partitions A }"
    by auto 
  moreover have "... = ?A" using lm014 by metis
  ultimately show ?thesis by presburger
qed

lemma lm016: 
  "possible_allocations_rel G N ⊆ 
   injectionsUniverse ∩ {a. Range a ⊆ N & Domain a ∈ all_partitions G}"
  using lm012 lm011 injections_def by fastforce

lemma lm017: 
  "possible_allocations_rel G N ⊇ 
   injectionsUniverse ∩ {a. Domain a ∈ all_partitions G & Range a ⊆ N}"
  using injections_def by auto

(* combination of the previous two lemmas *)
lemma lm018: 
  "possible_allocations_rel G N   = 
   injectionsUniverse ∩ {a. Domain a ∈ all_partitions G & Range a ⊆ N}"
  using lm016 lm017 by blast

(* all possible injections can be flipped and gives the same *)
lemma lm019: 
  "converse ` injectionsUniverse = injectionsUniverse" 
  by auto

lemma lm020: 
  "converse`(A ∩ B)  =  (converse`A) ∩ (converse`B)" 
  by force

lemma allocationInjectionsUnivervseProperty: 
  "allAllocations N G = 
   injectionsUniverse ∩ {a. Domain a ⊆ N & Range a ∈ all_partitions G}"
proof -
  let ?A="possible_allocations_rel G N" 
  let ?c=converse 
  let ?I=injectionsUniverse 
  let ?P="all_partitions G" 
  let ?d=Domain 
  let ?r=Range
  have "?c`?A = (?c`?I) ∩ ?c` ({a. ?r a ⊆ N & ?d a ∈ ?P})" using lm018 by fastforce
  moreover have "... = (?c`?I) ∩ {aa. ?d aa ⊆ N & ?r aa ∈ ?P}" by fastforce
  moreover have "... = ?I ∩ {aa. ?d aa ⊆ N & ?r aa ∈ ?P}" using lm019 by metis
  ultimately show ?thesis by presburger
qed

lemma lm021: 
  "allAllocations N G ⊆ injectionsUniverse" 
  using allocationInjectionsUnivervseProperty by fast

lemma lm022: 
  "allAllocations N G ⊆ partitionValuedUniverse"
  using allocationInverseRangeDomainProperty is_partition_of_def is_non_overlapping_def 
  by auto blast

corollary allAllocationsUniverse: 
  "allAllocations N G ⊆ allocationsUniverse" 
  using lm021 lm022 by (metis (lifting, mono_tags) inf.bounded_iff)

corollary posssibleAllocationsRelCharacterization: 
  "a ∈ allAllocations N G = 
   (a ∈ injectionsUniverse & Domain a ⊆ N & Range a ∈ all_partitions G)" 
  using allocationInjectionsUnivervseProperty Int_Collect Int_iff by (metis (lifting))

corollary lm023: 
  assumes "a ∈ allAllocations N1 G" 
  shows   "a ∈ allAllocations (N1 ∪ N2) G"
proof - 
  have "Domain a ⊆ N1 ∪ N2" using assms(1) posssibleAllocationsRelCharacterization 
       by (metis le_supI1) 
  moreover have "a ∈ injectionsUniverse & Range a ∈ all_partitions G" 
       using assms posssibleAllocationsRelCharacterization by blast 
  ultimately show ?thesis using posssibleAllocationsRelCharacterization by blast 
qed

corollary lm024: 
  "allAllocations N1 G ⊆ allAllocations (N1 ∪ N2) G"
  using lm023 by (metis subsetI)

lemma lm025: 
  assumes "(⋃ P1) ∩ (⋃ P2) = {}" 
          "is_non_overlapping P1" "is_non_overlapping P2" 
          "X ∈ P1 ∪ P2" "Y ∈ P1 ∪ P2" "X ∩ Y ≠ {}" 
  shows "(X = Y)" 
  unfolding is_non_overlapping_def using assms is_non_overlapping_def by fast

lemma lm026: 
  assumes "(⋃ P1) ∩ (⋃ P2) = {}" 
          "is_non_overlapping P1"
          "is_non_overlapping P2" 
          "X ∈ P1 ∪ P2" 
          "Y ∈ P1 ∪ P2" 
          "(X = Y)" 
  shows "X ∩ Y ≠ {}" 
  unfolding is_non_overlapping_def using assms is_non_overlapping_def by fast

lemma lm027:  
  assumes "(⋃ P1) ∩ (⋃ P2) = {}" 
          "is_non_overlapping P1" 
          "is_non_overlapping P2"
  shows "is_non_overlapping (P1 ∪ P2)" 
  unfolding is_non_overlapping_def using assms lm025 lm026 by metis

lemma lm028: 
  "Range Q ∪ (Range (P outside (Domain Q))) = Range (P +* Q)"
  by (simp add: paste_def Range_Un_eq Un_commute)

lemma lm029: 
  assumes "a1 ∈ injectionsUniverse" 
          "a2 ∈ injectionsUniverse" 
          "(Range a1) ∩ (Range a2)={}" 
          "(Domain a1) ∩ (Domain a2) = {}" 
  shows "a1 ∪ a2 ∈ injectionsUniverse" 
  using assms disj_Un_runiq 
  by (metis (no_types) Domain_converse converse_Un mem_Collect_eq)

lemma nonOverlapping:  
  assumes "R ∈ partitionValuedUniverse" 
  shows "is_non_overlapping (Range R)"
proof -
  obtain P where
  0: "P ∈ partitionsUniverse & R ⊆ UNIV × P" using assms by blast
  have "Range R ⊆ P" using 0 by fast
  then show ?thesis using 0 mem_Collect_eq subset_is_non_overlapping by (metis)
qed

lemma allocationUnion: 
  assumes "a1 ∈ allocationsUniverse" 
          "a2 ∈ allocationsUniverse" 
          "(⋃ (Range a1)) ∩ (⋃ (Range a2)) = {}"
          "(Domain a1) ∩ (Domain a2) = {}" 
  shows "a1 ∪ a2 ∈ allocationsUniverse"
proof -
  let ?a="a1 ∪ a2" 
  let ?b1="a1^-1" 
  let ?b2="a2^-1" 
  let ?r=Range 
  let ?d=Domain
  let ?I=injectionsUniverse 
  let ?P=partitionsUniverse 
  let ?PV=partitionValuedUniverse 
  let ?u=runiq
  let ?b="?a^-1" 
  let ?p=is_non_overlapping
  have "?p (?r a1) & ?p (?r a2)" using assms nonOverlapping by blast then
  moreover have "?p (?r a1 ∪ ?r a2)" using assms by (metis lm027)
  then moreover have "(?r a1 ∪ ?r a2) ∈ ?P" by simp
  moreover have "?r ?a = (?r a1 ∪ ?r a2)" using assms by fast
  ultimately moreover have "?p (?r ?a)" using lm027 assms by fastforce
  then moreover have "?a ∈ ?PV" using assms by fast
  moreover have "?r a1 ∩ (?r a2) ⊆ Pow (⋃ (?r a1) ∩ (⋃ (?r a2)))" by auto
  ultimately moreover have "{} ∉ (?r a1) & {} ∉ (?r a2)" 
        using is_non_overlapping_def by (metis Int_empty_left)
  ultimately moreover have "?r a1 ∩ (?r a2) = {}" 
        using assms nonOverlapping is_non_overlapping_def by auto
  ultimately moreover have "?a ∈ ?I" using lm029 assms by fastforce
  ultimately show ?thesis by blast
qed

(* - stands here for set difference *)
lemma lm030: 
  assumes "a ∈ injectionsUniverse" 
  shows "a - b ∈ injectionsUniverse" 
  using assms 
  by (metis (lifting) Diff_subset converse_mono mem_Collect_eq subrel_runiq)

(* Note that -` is the inverse image of a lambda function. *)
lemma lm031: 
  "{a. Domain a ⊆ N    &   Range a ∈ all_partitions G} =
   (Domain -`(Pow N))  ∩  (Range -` (all_partitions G)) " 
  by fastforce

lemma lm032: 
  "allAllocations N G = 
   injectionsUniverse ∩ ((Range -` (all_partitions G)) ∩ (Domain -`(Pow N)))"
  using allocationInjectionsUnivervseProperty lm031 by (metis (no_types) Int_commute)

(* -` is the reverse image of a function. This is a variant of lm023 with different bracketing *)
corollary lm033: 
  "allAllocations N G = 
   injectionsUniverse ∩ (Range -` (all_partitions G)) ∩ (Domain -`(Pow N))" 
  using lm032 Int_assoc by (metis)

lemma lm034: 
  assumes "a ∈ allAllocations N G" 
  shows "(a^-1 ∈ injections (Range a) N & 
         Range a ∈ all_partitions G)"
  using assms 
  by (metis (mono_tags, opaque_lifting) posssibleAllocationsRelCharacterization
                                   allocationInverseRangeDomainProperty)

lemma lm035: 
  assumes "a^-1 ∈ injections (Range a) N" "Range a ∈ all_partitions G" 
  shows "a ∈ allAllocations N G" 
  using assms image_iff by fastforce

lemma allocationReverseInjective: 
  "a ∈ allAllocations N G = 
   (a^-1 ∈ injections (Range a) N  &  Range a ∈ all_partitions G)"
  using lm034 lm035 by metis

lemma lm036: 
  assumes "a ∈ allAllocations N G" 
  shows "a ∈ injections (Domain a) (Range a) & 
         Range a ∈ all_partitions G &
         Domain a ⊆ N"
  using assms mem_Collect_eq injections_def posssibleAllocationsRelCharacterization order_refl 
  by (metis (mono_tags, lifting))

lemma lm037: 
  assumes "a ∈ injections (Domain a) (Range a)" 
          "Range a ∈ all_partitions G" 
          "Domain a ⊆ N" 
  shows "a ∈ allAllocations N G" 
  using assms mem_Collect_eq posssibleAllocationsRelCharacterization injections_def 
  by (metis (erased, lifting))

lemma characterizationallAllocations: 
  "a ∈ allAllocations N G = (a ∈ injections (Domain a) (Range a)  & 
   Range a ∈ all_partitions G & 
   Domain a ⊆ N)" 
  using lm036 lm037 by metis

lemma lm038: 
  assumes "a ∈ partitionValuedUniverse" 
  shows "a - b ∈ partitionValuedUniverse" 
  using assms subset_is_non_overlapping by fast

lemma reducedAllocation: 
  assumes "a ∈ allocationsUniverse" 
  shows "a - b ∈ allocationsUniverse" 
  using assms lm030 lm038 by auto

lemma lm039: 
  assumes "a ∈ injectionsUniverse" 
  shows "a ∈ injections (Domain a) (Range a)"
  using assms injections_def mem_Collect_eq order_refl by blast

lemma lm040: 
  assumes "a ∈ allocationsUniverse" 
  shows "a ∈ allAllocations (Domain a) (⋃ (Range a))"
proof -
  let ?r=Range 
  let ?p=is_non_overlapping 
  let ?P=all_partitions 
  have "?p (?r a)" using assms nonOverlapping Int_iff by blast 
  then have "?r a ∈ ?P (⋃ (?r a))" unfolding all_partitions_def 
     using is_partition_of_def mem_Collect_eq by (metis) 
  then show ?thesis 
     using assms IntI Int_lower1 equalityE allocationInjectionsUnivervseProperty 
           mem_Collect_eq rev_subsetD 
     by (metis (lifting, no_types))
qed

lemma lm041: 
  "({X} ∈ partitionsUniverse) = (X ≠ {})" 
  using is_non_overlapping_def by fastforce

lemma lm042: 
  "{(x, X)} - {(x, {})} ∈ partitionValuedUniverse" 
  using lm041 by auto

lemma singlePairInInjectionsUniverse: 
  "{(x, X)} ∈ injectionsUniverse" 
  unfolding runiq_basic using runiq_singleton_rel by blast

lemma allocationUniverseProperty: 
  "{(x,X)} - {(x,{})} ∈ allocationsUniverse" 
  using lm042 singlePairInInjectionsUniverse lm030 Int_iff by (metis (no_types))

(* PP is a family of partitions *)
lemma lm043: 
  assumes "is_non_overlapping PP" "is_non_overlapping (Union PP)" 
  shows "is_non_overlapping (Union ` PP)"
proof -
  let ?p=is_non_overlapping 
  let ?U=Union 
  let ?P2="?U PP" 
  let ?P1="?U ` PP" 
  have 
  0: "∀ X∈?P1. ∀ Y ∈ ?P1. (X ∩ Y = {} ⟶ X ≠ Y)" 
      using assms is_non_overlapping_def Int_absorb Int_empty_left UnionI Union_disjoint 
            ex_in_conv imageE 
      by (metis (opaque_lifting, no_types))
  {
    fix X Y 
    assume 
    1: "X ∈ ?P1 & Y∈?P1 & X ≠ Y"
    then obtain XX YY 
    where 
    2: "X = ?U XX & Y=?U YY & XX∈PP & YY∈PP" by blast
    then have "XX ⊆ Union PP & YY ⊆ Union PP & XX ∩ YY = {}" 
    using 1 2 is_non_overlapping_def assms(1) Sup_upper by metis
    then moreover have "∀ x∈XX. ∀ y∈YY. x ∩ y = {}" using assms(2) is_non_overlapping_def 
         by (metis IntI empty_iff subsetCE)
    ultimately have "X ∩ Y={}" using assms 0 1 2 is_non_overlapping_def by auto
  }
  then show ?thesis using 0 is_non_overlapping_def by metis
qed

(* A preservation of reallocating goods of the participants in X to a single participant i. *)
lemma lm044: 
  assumes "a ∈ allocationsUniverse" 
  shows "(a - ((X∪{i})×(Range a))) ∪ 
         ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}) ∈ allocationsUniverse & 
         ⋃ (Range ((a - ((X∪{i})×(Range a))) ∪ ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}))) =
         ⋃(Range a)"
proof -
  let ?d=Domain 
  let ?r=Range 
  let ?U=Union 
  let ?p=is_non_overlapping 
  let ?P=partitionsUniverse 
  let ?u=runiq 
  let ?Xi="X ∪ {i}" 
  let ?b="?Xi × (?r a)" 
  let ?a1="a - ?b" 
  let ?Yi="a``?Xi" 
  let ?Y="?U ?Yi" 
  let ?A2="{(i, ?Y)}" 
  let ?a3="{(i,{})}" 
  let ?a2="?A2 - ?a3" 
  let ?aa1="a outside ?Xi" 
  let ?c="?a1 ∪ ?a2" 
  let ?t1="?c ∈ allocationsUniverse" 
  have 
  1: "?U(?r(?a1∪?a2))=?U(?r ?a1) ∪ (?U(?r ?a2))" by (metis Range_Un_eq Union_Un_distrib) 
  have 
  2: "?U(?r a) ⊆ ?U(?r ?a1) ∪ ?U(a``?Xi) & ?U(?r ?a1) ∪ ?U(?r ?a2) ⊆ ?U(?r a)" by blast
  have
  3: "?u a & ?u (a^-1) & ?p (?r a) & ?r ?a1 ⊆ ?r a & ?Yi ⊆ ?r a" 
     using assms Int_iff nonOverlapping mem_Collect_eq by auto 
  then have 
  4: "?p (?r ?a1) & ?p ?Yi" using subset_is_non_overlapping by metis 
  have "?a1 ∈ allocationsUniverse & ?a2 ∈ allocationsUniverse" 
     using allocationUniverseProperty assms(1) reducedAllocation by fastforce 
  then have "(?a1 = {} ∨ ?a2 = {})⟶ ?t1" 
     using Un_empty_left by (metis (lifting, no_types) Un_absorb2 empty_subsetI) 
  moreover have "(?a1 = {} ∨ ?a2 = {})⟶ ?U (?r a) = ?U (?r ?a1) ∪ ?U (?r ?a2)" by fast 
  ultimately have 
  5: "(?a1 = {} ∨ ?a2 = {})⟶ ?thesis" using 1 by simp
  { 
    assume
    6: "?a1≠{} & ?a2≠{}" 
    then have "?r ?a2⊇{?Y}" 
         using Diff_cancel Range_insert empty_subsetI insert_Diff_single insert_iff insert_subset 
         by (metis (opaque_lifting, no_types)) 
    then have 
    7: "?U (?r a) = ?U (?r ?a1) ∪ ?U (?r ?a2)" using 2 by blast
    have "?r ?a1 ≠ {} & ?r ?a2 ≠ {}" using 6 by auto
    moreover have "?r ?a1 ⊆ a``(?d ?a1)" using assms by blast
    moreover have "?Yi ∩ (a``(?d a - ?Xi)) = {}" 
         using assms 3 6 Diff_disjoint intersectionEmptyRelationIntersectionEmpty by metis
    ultimately moreover have "?r ?a1 ∩ ?Yi = {} & ?Yi ≠ {}" by blast
    ultimately moreover have "?p {?r ?a1, ?Yi}" unfolding is_non_overlapping_def 
         using IntI Int_commute empty_iff insert_iff subsetI subset_empty by metis
    moreover have "?U {?r ?a1, ?Yi} ⊆ ?r a" by auto
    then moreover have "?p (?U {?r ?a1, ?Yi})" by (metis "3" Outside_def subset_is_non_overlapping)
    ultimately moreover have "?p (?U`{(?r ?a1), ?Yi})" using lm043 by fast
    moreover have "... = {?U (?r ?a1), ?Y}" by force
    ultimately moreover have "∀ x ∈ ?r ?a1. ∀ y∈?Yi. x ≠ y" 
    using IntI empty_iff by metis
    ultimately moreover have "∀ x ∈ ?r ?a1. ∀ y∈?Yi. x ∩ y = {}" 
       using 3 4 6 is_non_overlapping_def by (metis rev_subsetD)
    ultimately have "?U (?r ?a1) ∩ ?Y = {}" using unionIntersectionEmpty
proof -
  have "∀v0. v0 ∈ Range (a - (X ∪ {i}) × Range a) ⟶ (∀v1. v1 ∈ a `` (X ∪ {i}) ⟶ v0 ∩ v1 = {})" 
    by (metis (no_types) ‹∀x∈Range (a - (X ∪ {i}) × Range a). ∀y∈a `` (X ∪ {i}). x ∩ y = {}›) 
  thus "⋃(Range (a - (X ∪ {i}) × Range a)) ∩ ⋃(a `` (X ∪ {i})) = {}" by blast
qed 
  then have 
    "?U (?r ?a1) ∩ (?U (?r ?a2)) = {}" by blast
    moreover have "?d ?a1 ∩ (?d ?a2) = {}" by blast
    moreover have "?a1 ∈ allocationsUniverse" using assms(1) reducedAllocation by blast
    moreover have "?a2 ∈ allocationsUniverse" using allocationUniverseProperty by fastforce
    ultimately have "?a1 ∈ allocationsUniverse & ?a2 ∈ allocationsUniverse &
                     ⋃(Range ?a1) ∩ ⋃(Range ?a2) = {} & Domain ?a1 ∩ Domain ?a2 = {}" 
      by blast 
    then have ?t1 using allocationUnion by auto       
    then have ?thesis using 1 7 by simp
  }
  then show ?thesis using 5 by linarith
qed

corollary allocationsUniverseOutsideUnion: 
  assumes "a ∈ allocationsUniverse" 
  shows   "(a outside (X∪{i})) ∪ ({i}×({⋃(a``(X∪{i}))}-{{}})) ∈ allocationsUniverse & 
           ⋃(Range((a outside (X∪{i})) ∪ ({i}×({⋃(a``(X∪{i}))}-{{}})))) = ⋃(Range a)"
proof -
  have "a - ((X∪{i})×(Range a)) = a outside (X ∪ {i})" using Outside_def by metis
  moreover have "(a - ((X∪{i})×(Range a))) ∪ ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}) ∈
                 allocationsUniverse"
           using assms lm044 by fastforce
  moreover have "⋃ (Range ((a - ((X∪{i})×(Range a))) ∪ ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}))) = 
                 ⋃(Range a)"
  using assms lm044 by (metis (no_types))
  ultimately have 
     "(a outside (X∪{i})) ∪ ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}) ∈ allocationsUniverse & 
      ⋃ (Range ((a outside (X∪{i})) ∪ ({(i, ⋃ (a``(X ∪ {i})))} - {(i,{})}))) = ⋃(Range a)" 
         by simp
  moreover have "{(i, ⋃ (a``(X ∪ {i})))} - {(i,{})} = {i} × ({⋃ (a``(X∪{i}))} - {{}})" 
         by fast
  ultimately show ?thesis by auto
qed

(* If there is an allocation with a participant in its domain, then the goods allocated are non-empty *)
lemma lm045: 
  assumes "Domain a ∩ X ≠ {}" "a ∈ allocationsUniverse" 
  shows   "⋃(a``X) ≠ {}"
proof -
  let ?p = is_non_overlapping 
  let ?r = Range
  have "?p (?r a)" using assms Int_iff nonOverlapping by auto
  moreover have "a``X ⊆ ?r a" by fast
  ultimately have "?p (a``X)" using assms subset_is_non_overlapping by blast
  moreover have "a``X ≠ {}" using assms by fast
  ultimately show ?thesis by (metis Union_member all_not_in_conv no_empty_in_non_overlapping)
qed

(* i is an additional bidder added to X *)
corollary lm046: 
  assumes "Domain a ∩ X ≠ {}" "a ∈ allocationsUniverse" 
  shows   "{⋃(a``(X∪{i}))}-{{}}  =  {⋃(a``(X∪{i}))}" 
  using assms lm045 by fast

(* variant of allocationsUniverseOutsideUnion *)
corollary lm047: 
  assumes "a ∈ allocationsUniverse"
          "(Domain a) ∩ X ≠ {}" 
  shows   "(a outside (X∪{i})) ∪ ({i}×{⋃(a``(X∪{i}))}) ∈ allocationsUniverse & 
                         ⋃(Range((a outside (X∪{i})) ∪ ({i}×{⋃(a``(X∪{i}))}))) = ⋃(Range a)"
proof -
  let ?t1 = "(a outside (X∪{i})) ∪ ({i}×({⋃(a``(X∪{i}))}-{{}})) ∈ allocationsUniverse"
  let ?t2 = "⋃(Range((a outside (X∪{i})) ∪ ({i}×({⋃(a``(X∪{i}))}-{{}})))) = ⋃(Range a)"
  have 
  0: "a ∈ allocationsUniverse" using assms(1) by fast 
  then have "?t1 & ?t2" using allocationsUniverseOutsideUnion 
  proof - 
    have "a ∈ allocationsUniverse ⟶ 
          a outside (X ∪ {i}) ∪ {i} × ({⋃(a `` (X ∪ {i}))} - {{}}) ∈ allocationsUniverse"
      using allocationsUniverseOutsideUnion by fastforce
    hence "a outside (X ∪ {i}) ∪ {i} × ({⋃(a `` (X ∪ {i}))} - {{}}) ∈ allocationsUniverse"
      by (metis "0")
    thus "a outside (X ∪ {i}) ∪ {i} × ({⋃(a `` (X ∪ {i}))} - {{}}) ∈ 
           allocationsUniverse ∧ ⋃(Range (a outside (X ∪ {i}) ∪ {i} × ({⋃(a `` (X ∪ {i}))} - {{}})))
          = ⋃(Range a)"
          using "0" by (metis (no_types) allocationsUniverseOutsideUnion)
  qed
  moreover have 
  "{⋃(a``(X∪{i}))}-{{}} = {⋃(a``(X∪{i}))}" using lm045 assms by fast
  ultimately show ?thesis by auto
qed

(* The bid vector does not decrease when you bid for extra goods *)
abbreviation 
  "bidMonotonicity b i == 
  (∀ t t'. (trivial t & trivial t' & Union t ⊆ Union t') ⟶ 
           sum b ({i}×t) ≤ sum b ({i}×t'))" 

(* adding the goods in X weakly increases the revenue *)
lemma lm048: 
  assumes "bidMonotonicity b i" "runiq a" 
  shows  "sum b ({i}×((a outside X)``{i})) ≤ sum b ({i}×{⋃(a``(X∪{i}))})"
proof -
  let ?u = runiq 
  let ?I = "{i}" 
  let ?R = "a outside X" 
  let ?U = Union 
  let ?Xi = "X ∪?I"
  let ?t1 = "?R``?I" 
  let ?t2 = "{?U (a``?Xi)}"
  have "?U (?R``?I) ⊆ ?U (?R``(X∪?I))" by blast
  moreover have "... ⊆ ?U (a``(X∪?I))" using Outside_def by blast
  ultimately have "?U (?R``?I) ⊆ ?U (a``(X∪?I))" by auto
  then have 
  0: "?U ?t1 ⊆ ?U ?t2" by auto
  have "?u a" using assms by fast 
  moreover have "?R ⊆ a" using Outside_def by blast ultimately
  have "?u ?R" using subrel_runiq by metis
  then have "trivial ?t1" by (metis runiq_alt)
  moreover have "trivial ?t2" by (metis trivial_singleton)
  ultimately show ?thesis using assms 0 by blast
qed

lemma lm049:  
  assumes "XX ∈ partitionValuedUniverse" 
  shows "{} ∉ Range XX" 
  using assms mem_Collect_eq no_empty_in_non_overlapping by auto

corollary emptyNotInRange: 
  assumes "a ∈ allAllocations N G" 
  shows "{} ∉ Range a" 
  using assms lm049 allAllocationsUniverse by auto blast

lemma lm050: 
  assumes "a ∈ allAllocations N G" 
  shows "Range a ⊆ Pow G"
  using assms allocationInverseRangeDomainProperty is_partition_of_def by (metis subset_Pow_Union)

corollary lm051: 
  assumes "a ∈ allAllocations N G" 
  shows "Domain a ⊆ N & Range a ⊆ Pow G - {{}}" 
  using assms lm050 insert_Diff_single emptyNotInRange subset_insert
        allocationInverseRangeDomainProperty by metis

corollary allocationPowerset: 
  assumes "a ∈ allAllocations N G" 
  shows "a ⊆ N × (Pow G - {{}})" 
  using assms lm051 by blast

corollary lm052: 
  "allAllocations N G ⊆ Pow (N×(Pow G-{{}}))" 
  using allocationPowerset by blast

(* reformulation of 43c with given set of goods and set of participants *)
lemma lm053: 
  assumes  "a ∈ allAllocations N G" 
           "i ∈ N-X" 
           "Domain a ∩ X ≠ {}" 
  shows   "a outside (X ∪ {i}) ∪ ({i} × {⋃(a``(X∪{i}))}) ∈ 
           allAllocations (N-X) (⋃ (Range a))"
proof -
  let ?R = "a outside X" 
  let ?I = "{i}" 
  let ?U = Union 
  let ?u = runiq  
  let ?r = Range 
  let ?d = Domain
  let ?aa = "a outside (X ∪ {i}) ∪ ({i} × {?U(a``(X∪{i}))})" 
  have 
  1: "a ∈ allocationsUniverse" using assms(1) allAllocationsUniverse  rev_subsetD by blast
  have "i ∉ X" using assms by fast 
  then have 
  2: "?d a - X ∪ {i} = ?d a ∪ {i} - X" by fast
  have "a ∈ allocationsUniverse" using 1 by fast 
  moreover have "?d a ∩ X ≠ {}" using assms by fast 
  ultimately have "?aa ∈ allocationsUniverse & ?U (?r ?aa) = ?U (?r a)" apply (rule lm047) done
  then have "?aa ∈ allAllocations (?d ?aa) (?U (?r a))"
     using lm040 by (metis (lifting, mono_tags))
  then have "?aa ∈ allAllocations (?d ?aa ∪ (?d a - X ∪ {i}))  (?U (?r a))"
     by (metis lm023)
  moreover have "?d a - X ∪ {i} = ?d ?aa ∪ (?d a - X ∪ {i})" using Outside_def by auto
  ultimately have "?aa ∈ allAllocations (?d a - X ∪ {i}) (?U (?r a))" by simp
  then have "?aa ∈ allAllocations (?d a ∪ {i} - X) (?U (?r a))" using 2 by simp
  moreover have "?d a ⊆ N" using assms(1) posssibleAllocationsRelCharacterization by metis
  then moreover have "(?d a ∪ {i} - X) ∪ (N - X) = N - X" using assms by fast
  ultimately have "?aa ∈ allAllocations (N - X) (?U (?r a))" using lm024 
    by (metis (lifting, no_types) in_mono)
  then show ?thesis by fast
qed

lemma lm054: 
  assumes "bidMonotonicity (b::_ => real) i" 
          "a ∈ allocationsUniverse" 
          "Domain a ∩ X ≠ {}" 
          "finite a"
  shows   "sum b (a outside X) ≤ 
           sum b (a outside (X ∪ {i}) ∪ ({i} × {⋃(a``(X∪{i}))}))"
proof -
  let ?R = "a outside X" 
  let ?I = "{i}" 
  let ?U = Union 
  let ?u = runiq 
  let ?r = Range 
  let ?d = Domain
  let ?aa = "a outside (X ∪ {i}) ∪ ({i} × {?U(a``(X∪{i}))})"
  have "a ∈ injectionsUniverse" using assms by fast 
  then have 
  0: "?u a" by simp
  moreover have "?R ⊆ a & ?R--i ⊆ a" using Outside_def using lm088 by auto
  ultimately have "finite (?R -- i) & ?u (?R--i) & ?u ?R" 
    using finite_subset subrel_runiq by (metis assms(4))
  then moreover have "trivial ({i}×(?R``{i}))" using runiq_def 
    by (metis trivial_cartesian trivial_singleton)
  moreover have "∀X. (?R -- i) ∩ ({i}×X)={}" using outside_reduces_domain by force
  ultimately have 
  1: "finite (?R--i) & finite ({i}×(?R``{i})) & (?R -- i) ∩ ({i}×(?R``{i}))={} & 
      finite ({i} × {?U(a``(X∪{i}))}) & (?R -- i) ∩ ({i} × {?U(a``(X∪{i}))})={}" 
    using Outside_def trivial_implies_finite by fast 
  have "?R = (?R -- i) ∪ ({i}×?R``{i})" by (metis outsideUnion)
  then have "sum b ?R = sum b (?R -- i) + sum b ({i}×(?R``{i}))" 
    using 1 sum.union_disjoint by (metis (lifting) sum.union_disjoint)
  moreover have "sum b ({i}×(?R``{i})) ≤ sum b ({i}×{?U(a``(X∪{i}))})" 
    using lm048 assms(1) 0 by metis
  ultimately have "sum b ?R ≤ sum b (?R -- i) + sum b ({i}×{?U(a``(X∪{i}))})" by linarith
  moreover have "... = sum b (?R -- i ∪ ({i} × {?U(a``(X∪{i}))}))" 
  using 1 sum.union_disjoint by auto
  moreover have "... = sum b ?aa" by (metis outsideOutside)
  ultimately show ?thesis by simp
qed

lemma elementOfPartitionOfFiniteSetIsFinite: 
  assumes "finite X" "XX ∈ all_partitions X" 
  shows "finite XX" 
  using all_partitions_def is_partition_of_def 
  by (metis assms(1) assms(2) finite_UnionD mem_Collect_eq)

lemma lm055: 
  assumes "finite N" "finite G" "a ∈ allAllocations N G"
  shows "finite a" 
  using assms finiteRelationCharacterization rev_finite_subset 
  by (metis characterizationallAllocations elementOfPartitionOfFiniteSetIsFinite)

lemma allAllocationsFinite: 
  assumes "finite N" "finite G" 
  shows "finite (allAllocations N G)"
proof -
  have "finite (Pow(N×(Pow G-{{}})))" using assms finite_Pow_iff by blast
  then show ?thesis using lm052 rev_finite_subset by (metis(no_types))
qed

corollary lm056: 
  assumes "bidMonotonicity (b::_ => real) i" 
          "a ∈ allAllocations N G" 
          "i ∈ N-X" 
          "Domain a ∩ X ≠ {}" 
          "finite N" 
          "finite G" 
  shows   "Max ((sum b)`(allAllocations (N-X) G)) ≥ 
           sum b (a outside X)"
proof -
  let ?aa = "a outside (X ∪ {i}) ∪ ({i} × {⋃(a``(X∪{i}))})"
  have "bidMonotonicity (b::_ => real) i" using assms(1) by fast
  moreover have "a ∈ allocationsUniverse" using assms(2) allAllocationsUniverse by blast
  moreover have "Domain a ∩ X ≠ {}" using assms(4) by auto
  moreover have "finite a" using assms lm055 by metis 
  ultimately have 
  0: "sum b (a outside X) ≤ sum b ?aa" by (rule lm054)
  have "?aa ∈ allAllocations (N-X) (⋃ (Range a))" using assms lm053 by metis
  moreover have "⋃ (Range a) = G" 
    using assms allocationInverseRangeDomainProperty is_partition_of_def by metis
  ultimately have "sum b ?aa ∈ (sum b)`(allAllocations (N-X) G)" by (metis imageI)
  moreover have "finite ((sum b)`(allAllocations (N-X) G))" 
    using assms allAllocationsFinite assms(5,6) by (metis finite_Diff finite_imageI)
  ultimately have "sum b ?aa ≤ Max ((sum b)`(allAllocations (N-X) G))" by auto
  then show ?thesis using 0 by linarith
qed

lemma cardinalityPreservation: 
  assumes "∀X ∈ XX. finite X" "is_non_overlapping XX" 
  shows   "card (⋃ XX) = sum card XX" 
  by (metis assms is_non_overlapping_def card_Union_disjoint disjointI)

corollary cardSumCommute: 
  assumes "XX partitions X" "finite X" "finite XX" 
  shows   "card (⋃ XX) = sum card XX" 
  using assms cardinalityPreservation by (metis is_partition_of_def familyUnionFiniteEverySetFinite)

(* Σ_x∈ (Union C) (f x)   is the same as Σ_x∈ C (Σ_set∈ C (Σ_x∈set (f x))) *)
lemma sumUnionDisjoint1: 
  assumes "∀A∈C. finite A" "∀A∈C. ∀B∈C. A ≠ B ⟶ A Int B = {}" 
  shows "sum f (Union C) = sum (sum f) C" 
  using assms sum.Union_disjoint by fastforce

corollary sumUnionDisjoint2: 
  assumes "∀x∈X. finite x" "is_non_overlapping X" 
  shows "sum f (⋃ X) = sum (sum f) X" 
  using assms sumUnionDisjoint1 is_non_overlapping_def by fast

corollary sumUnionDisjoint3: 
  assumes "∀x∈X. finite x" "X partitions XX" 
  shows "sum f XX = sum (sum f) X" 
  using assms by (metis is_partition_of_def sumUnionDisjoint2)
 
corollary sum_associativity: 
  assumes "finite x" "X partitions x" 
  shows  "sum f x = sum (sum f) X" 
  using assms sumUnionDisjoint3 
  by (metis is_partition_of_def familyUnionFiniteEverySetFinite)

lemma lm057: 
  assumes "a ∈ allocationsUniverse" "Domain a ⊆ N" "⋃(Range a) = G" 
  shows   "a ∈ allAllocations N G" 
  using assms posssibleAllocationsRelCharacterization lm040 by (metis (mono_tags, lifting))

corollary lm058: 
  "(allocationsUniverse ∩ {a. (Domain a) ⊆ N & ⋃(Range a) = G}) ⊆
   allAllocations N G"
  using lm057 by fastforce

corollary lm059: 
  "allAllocations N G ⊆ {a. (Domain a) ⊆ N}" 
  using allocationInverseRangeDomainProperty by blast

corollary lm060: 
  "allAllocations N G ⊆ {a. ⋃(Range a) = G}" 
  using is_partition_of_def allocationInverseRangeDomainProperty mem_Collect_eq subsetI
  by (metis(mono_tags))

corollary lm061: 
  "allAllocations N G  ⊆  allocationsUniverse &
   allAllocations N G ⊆ {a. (Domain a) ⊆ N & ⋃(Range a) = G}" 
  using lm059 lm060 conj_subset_def allAllocationsUniverse by (metis (no_types))

corollary allAllocationsIntersectionSubset: 
  "allAllocations N G ⊆ 
   allocationsUniverse ∩ {a. (Domain a) ⊆ N & ⋃(Range a) = G}"
  (is "?L ⊆ ?R1 ∩ ?R2")
proof - 
  have "?L ⊆ ?R1 & ?L ⊆ ?R2" by (rule lm061) thus ?thesis by auto 
qed

corollary allAllocationsIntersection: 
  "allAllocations N G = 
   (allocationsUniverse ∩ {a. (Domain a) ⊆ N & ⋃(Range a) = G})" 
  (is "?L = ?R") 
proof -
  have "?L ⊆ ?R" using allAllocationsIntersectionSubset by metis 
  moreover have "?R ⊆ ?L" using lm058 by fast
  ultimately show ?thesis by force
qed

corollary allAllocationsIntersectionSetEquals: 
  "a ∈ allAllocations N G  = 
   (a ∈ allocationsUniverse  & (Domain a) ⊆ N & ⋃(Range a) = G)" 
  using allAllocationsIntersection Int_Collect by (metis (mono_tags, lifting))

corollary allocationsUniverseOutside: 
  assumes "a ∈ allocationsUniverse" 
  shows "a outside X ∈ allocationsUniverse" 
  using assms Outside_def by (metis (lifting, mono_tags) reducedAllocation)


subsection ‹Bridging theorem for injections›

lemma lm062: 
  "totalRels {} Y = {{}}" 
  by fast

lemma lm063: 
  "{} ∈ injectionsUniverse" 
  by (metis CollectI converse_empty runiq_emptyrel)

lemma lm064: 
  "injectionsUniverse ∩ (totalRels {} Y)  =  {{}}" 
  using lm062 lm063 by fast

lemma lm065: 
  assumes "runiq f" "x∉Domain f" 
  shows "{ f ∪ {(x, y)} | y . y ∈ A } ⊆ runiqs" 
  unfolding paste_def runiqs_def using assms runiq_basic by blast

lemma lm066: 
  "converse ` (converse ` X)  =  X" 
  by auto

lemma lm067: 
  "runiq (f^-1) = (f ∈ converse`runiqs)" 
  unfolding runiqs_def by auto

lemma lm068: 
  assumes "runiq (f^-1)" "A ∩ Range f  =  {}" 
  shows   "converse ` { f ∪ {(x, y)} | y . y ∈ A } ⊆ runiqs" 
  using assms lm065 by fast

lemma lm069: 
  assumes "f∈converse`runiqs" "A ∩ Range f  =  {}" 
  shows   "{f ∪ {(x, y)}| y. y ∈ A} ⊆ converse`runiqs" 
  (is "?l ⊆ ?r")
proof -
  have "runiq (f^-1)" using assms(1) lm067 by blast 
  then have "converse ` ?l ⊆ runiqs" using assms(2) by (rule lm068) 
  then have "?r ⊇ converse`(converse`?l)" by auto
  moreover have "converse`(converse`?l)=?l" by (rule lm066)
  ultimately show ?thesis by simp
qed

lemma lm070: 
  "{ R ∪ {(x, y)} | y . y ∈ A } ⊆ totalRels ({x} ∪ Domain R) (A ∪ Range R)" 
  by force

lemma lm071: 
  "injectionsUniverse  =  runiqs ∩ converse`runiqs" 
  unfolding runiqs_def by auto

lemma lm072: 
  assumes "f ∈ injectionsUniverse" "x ∉ Domain f" "A ∩ (Range f) = {}" 
  shows   "{f ∪ {(x, y)}| y. y ∈ A} ⊆ injectionsUniverse" 
  (is "?l ⊆ ?r") 
proof -  
  have "f ∈ converse`runiqs" using assms(1) lm071 by blast
  then have "?l ⊆ converse`runiqs" using assms(3) by (rule lm069)
  moreover have "?l ⊆ runiqs" using assms(1,2) lm065 by force 
  ultimately show ?thesis using lm071 by blast
qed

lemma lm073: 
  "injections X Y = totalRels X Y ∩ injectionsUniverse" 
  using lm008 by metis

lemma lm074: 
  assumes "f ∈ injectionsUniverse" 
  shows   "f outside A ∈ injectionsUniverse" 
  using assms by (metis (no_types) Outside_def lm030)

lemma lm075: 
  assumes "R ∈ totalRels A B" 
  shows   "R outside C ∈ totalRels (A-C) B" 
  unfolding Outside_def using assms by blast

lemma lm076: 
  assumes "g ∈ injections A B" 
  shows   "g outside C ∈ injections (A - C) B" 
  using assms Outside_def Range_outside_sub lm030 mem_Collect_eq outside_reduces_domain
  unfolding injections_def 
  by fastforce

lemma lm077: 
  assumes "g ∈ injections A B" 
  shows   "g outside C ∈ injections (A - C) B"
  using assms lm076 by metis

lemma lm078: 
  "{x}×{y}={(x,y)}" 
  by simp

lemma lm079: 
  assumes "x ∈ Domain f" "runiq f" 
  shows "{x}×f``{x} = {(x,f,,x)}" 
  using assms lm078 Image_runiq_eq_eval by metis

corollary lm080: 
  assumes "x ∈ Domain f" "runiq f" 
  shows   "f = (f -- x) ∪ {(x,f,,x)}" 
  using assms lm079 outsideUnion by metis

lemma lm081: 
  assumes "f ∈ injectionsUniverse" 
  shows   "Range(f outside A) = Range f - f``A" 
  using assms mem_Collect_eq rangeOutside by (metis)

lemma lm082: 
  assumes "g ∈ injections X Y" "x ∈ Domain g" 
  shows   "g ∈ {g--x ∪ {(x,y)}|y. y ∈ Y - (Range(g--x))}" 
proof - 
  let ?f = "g--x" 
  have "g∈injectionsUniverse" using assms(1) lm008 by fast 
  then moreover have "g,,x ∈ g``{x}" 
       using assms(2) by (metis Image_runiq_eq_eval insertI1 mem_Collect_eq)
  ultimately have "g,,x ∈ Y-Range ?f" using lm081 assms(1) unfolding injections_def by fast 
  moreover have "g=?f∪{(x, g,,x)}" 
     using assms lm080 mem_Collect_eq unfolding injections_def by (metis (lifting)) 
  ultimately show ?thesis by blast 
qed

corollary lm083: 
  assumes "x ∉ X" "g ∈ injections ({x} ∪ X) Y" 
  shows "g--x ∈ injections X Y" 
  using assms lm077 by (metis Diff_insert_absorb insert_is_Un)

corollary lm084: 
  assumes "x ∉ X" "g ∈ injections ({x} ∪ X) Y" 
  (is "g ∈ injections (?X) Y") 
  shows   "∃ f ∈ injections X Y. g ∈ {f ∪ {(x,y)}|y. y ∈ Y - (Range f)}" 
proof - 
  let ?f = "g--x" 
  have 
  0: "g∈injections ?X Y" using assms by metis 
  have "Domain g=?X" 
    using assms(2) mem_Collect_eq unfolding injections_def by (metis (mono_tags, lifting))
  then have 
  1: "x ∈ Domain g" by simp then have "?f ∈ injections X Y" using assms lm083 by fast
  moreover have "g∈{?f∪{(x,y)}|y. y∈Y-Range ?f}" using 0 1 by (rule lm082)
  ultimately show ?thesis by blast
qed

corollary lm085: 
  assumes "x ∉ X" 
  shows  "injections ({x} ∪ X) Y ⊆ 
          (⋃ f ∈ injections X Y. {f ∪ {(x, y)} | y . y ∈ Y - (Range f)})"
  using assms lm084 by auto

lemma lm086: 
  assumes "x ∉ X" 
  shows  "(⋃ f∈injections X Y. {f ∪ {(x, y)} | y . y ∈ Y-Range f}) ⊆ 
          injections ({x} ∪ X) Y" 
  using assms lm072 injections_def lm073 lm070 
proof -
  { fix f 
    assume "f ∈ injections X Y" 
    then have 
    0: "f ∈ injectionsUniverse & x ∉ Domain f & Domain f = X & Range f ⊆ Y" 
      using assms unfolding injections_def by fast 
    then have "f ∈ injectionsUniverse" by fast 
    moreover have "x ∉ Domain f" using 0 by fast
    moreover have 
    1: "(Y-Range f) ∩ Range f = {}" by blast
    ultimately have "{f ∪ {(x, y)} | y . y ∈ (Y-Range f)} ⊆ injectionsUniverse" by (rule lm072)
    moreover have "{f ∪ {(x, y)} | y . y ∈ (Y-Range f)} ⊆ totalRels ({x} ∪ X) Y" 
      using lm070 0 by force
    ultimately have "{f ∪ {(x, y)} | y . y ∈ (Y-Range f)} ⊆ 
                     injectionsUniverse ∩ totalRels ({x}∪X) Y" 
        by auto
  }
  thus ?thesis using lm008 unfolding injections_def by blast
qed

corollary injectionsUnionCommute: 
  assumes "x ∉ X" 
  shows   "(⋃ f∈injections X Y. {f ∪ {(x, y)} | y . y ∈ Y - (Range f)}) = 
           injections ({x} ∪ X) Y" 
  (is "?r=injections ?X _") 
proof - 
  have 
  0: "?r = (⋃ f∈injections X Y. {f ∪ {(x, y)} | y . y ∈ Y-Range f})" 
    (is "_=?r'") by blast 
  have "?r' ⊆ injections ?X Y" using assms by (rule lm086) moreover have "... = injections ?X Y"
    unfolding lm005 
  by simp ultimately have "?r ⊆ injections ?X Y" using 0 by simp
  moreover have "injections ?X Y ⊆ ?r" using assms by (rule lm085) 
  ultimately show ?thesis by blast
qed

lemma lm087: 
  assumes "∀ x. (P x ⟶ (f x = g x))" 
  shows   "Union {f x|x. P x} = Union {g x | x. P x}" 
  using assms by blast

lemma lm088: 
  assumes "x ∉ Domain R" 
  shows "R +* {(x,y)} = R ∪ {(x,y)}" 
  using assms
  by (metis (erased, lifting) Domain_empty Domain_insert Int_insert_right_if0
                              disjoint_iff_not_equal ex_in_conv paste_disj_domains)

(* Union of {f ...} where f ranges over injections X Y *)
lemma lm089: 
  assumes "x ∉ X" 
  shows "(⋃ f ∈ injections X Y. {f +* {(x, y)} | y . y ∈ Y-Range f}) = 
         (⋃ f ∈ injections X Y. {f ∪  {(x, y)}  | y . y ∈ Y-Range f})" 
  (is "?l = ?r") 
proof - 
  have 
  0: "∀f ∈ injections X Y. x ∉ Domain f" unfolding injections_def using assms by fast 
  then have 
  1: "?l=Union {{f +* {(x, y)} | y . y ∈ Y-Range f}|f .f ∈ injections X Y & x ∉ Domain f}" 
  (is "_=?l'") using assms by auto 
  moreover have 
  2: "?r=Union {{f ∪ {(x, y)} | y . y ∈ Y-Range f}|f .f ∈ injections X Y & x ∉ Domain f}" 
  (is "_=?r'") using assms 0 by auto 
  have "∀ f. f∈injections X Y & x ∉ Domain f ⟶ 
        {f +* {(x, y)} | y . y ∈ Y-Range f}={f ∪ {(x, y)} | y . y ∈ Y-Range f}" 
       using lm088 by force 
  then have "?l'=?r'" by (rule lm087) 
  then show "?l = ?r" using 1 2 by presburger
qed

corollary lm090: 
  assumes "x ∉ X" 
  shows   "(⋃ f ∈ injections X Y. {f +* {(x, y)} | y . y ∈ Y-Range f}) = 
           injections ({x} ∪ X) Y" 
  (is "?l=?r")
proof - 
  have "?l=(⋃ f∈injections X Y. {f ∪ {(x, y)} | y . y ∈ Y-Range f})" using assms by (rule lm089)
  moreover have "... = ?r" using assms by (rule injectionsUnionCommute) 
  ultimately show ?thesis by simp 
qed

lemma lm091: 
  "set [ f ∪ {(x,y)} . y ← (filter (%y. y ∉ (Range f)) Y) ] = 
   {f ∪ {(x,y)} | y . y ∈ (set Y) -     (Range f)}" 
  by auto

(* relationship of list and set notation for function application *)
lemma lm092: 
  assumes "∀x ∈ set L. set (F x) = G x" 
  shows "set (concat [ F x . x <- L]) = (⋃ x∈set L. G x)"
  using assms by force

(* relationship of list and set notation for function extension *)
lemma lm093: 
  "set (concat [ [ f ∪ {(x,y)} . y ← (filter (%y. y ∉ Range f) Y) ]. f ← F ]) =
   (⋃ f ∈ set F. {f ∪ {(x,y)} | y . y ∈ (set Y) - (Range f)})" 
  by auto

(* relationship of list vs set comprehension versions of function update*)
lemma lm094: 
  assumes "finite Y" 
  shows   "set [ f +* {(x,y)} . y ← sorted_list_of_set (Y - (Range f)) ] =
           {      f +* {(x,y)} | y . y ∈                 Y - (Range f)}" 
  using assms by auto

lemma lm095: 
  assumes "finite Y" 
  shows "set (concat [[f +* {(x,y)}. y ← sorted_list_of_set(Y - (Range f))]. f ← F]) =
         (⋃ f ∈ set F.{f +* {(x,y)} | y . y ∈ Y - (Range f)})" 
  using assms lm094 lm092 by auto

subsection ‹Computable injections›

fun injectionsAlg 
    where 
    "injectionsAlg [] (Y::'a list) = [{}]" |
    "injectionsAlg (x#xs) Y = 
       concat [ [R∪{(x,y)}. y ← (filter (%y. y ∉ Range R) Y)]
               .R ← injectionsAlg xs Y ]"

corollary lm096: 
  "set (injectionsAlg (x # xs) Y) = 
   (⋃ f ∈ set (injectionsAlg xs Y). {f ∪ {(x,y)} | y . y ∈ (set Y) - (Range f)})" 
  using lm093 by auto

corollary lm097: 
  assumes "set (injectionsAlg xs Y) = injections (set xs) (set Y)" 
  shows   "set (injectionsAlg (x # xs) Y) = 
           (⋃ f ∈ injections (set xs) (set Y). {f ∪ {(x,y)} | y . y ∈ (set Y) - (Range f)})" 
  using assms lm096 by auto

text‹We sometimes use parallel @{term abbreviation} and @{term definition} for the same object to save typing `unfolding xxx' each time. There is also different behaviour in the code extraction.›

lemma lm098:  
  "injections {} Y  =  {{}}" 
  by (simp add: lm008 lm062 runiq_emptyrel)

lemma lm099: 
  "injections {} Y  =  {{}}" 
  unfolding injections_def by (metis lm098 injections_def)

lemma injectionsFromEmptyIsEmpty: 
  "injectionsAlg [] Y  =  [{}]" 
  by simp

(* Relation between classical and algorithm definition of injections for induction step *)
lemma lm100: 
  assumes "x ∉ set xs" "set (injectionsAlg xs Y) = injections (set xs) (set Y)" 
  shows   "set (injectionsAlg (x # xs) Y) = injections ({x} ∪ set xs) (set Y)" 
  (is "?l=?r")
proof - 
  have "?l = (⋃ f∈injections (set xs) (set Y). {f ∪ {(x,y)} | y . y ∈ (set Y)-Range f})" 
  using assms(2) by (rule lm097) 
  moreover have "... = ?r" using assms(1) by (rule injectionsUnionCommute) 
  ultimately show ?thesis by simp
qed

lemma lm101: 
  assumes "x ∉ set xs" 
          "set (injections_alg xs Y) = injections (set xs) Y" 
          "finite Y" 
  shows    "set (injections_alg (x#xs) Y) = injections ({x} ∪ set xs) Y" 
  (is "?l=?r")
proof - 
  have "?l = (⋃ f∈injections (set xs) Y. {f +* {(x,y)} | y . y ∈ Y-Range f})" 
  using assms(2,3) lm095 by auto
  moreover have "... = ?r" using assms(1) by (rule lm090) 
  ultimately show ?thesis by simp
qed

lemma listInduct: 
  assumes "P []" "∀ xs x. P xs ⟶ P (x#xs)" 
  shows   "∀x. P x"
  using assms by (metis structInduct)

lemma injectionsFromEmptyAreEmpty: 
  "set (injections_alg [] Z) = {{}}" 
  by simp

theorem injections_equiv: 
  assumes "finite Y" and "distinct X" 
  shows  "set (injections_alg X Y) = injections (set X) Y"
proof -
  let ?P="λ l. distinct l ⟶ (set (injections_alg l Y)=injections (set l) Y)"
  have "?P []" using injectionsFromEmptyAreEmpty list.set(1) lm099 by metis
  moreover have "∀x xs. ?P xs ⟶ ?P (x#xs)" 
    using assms(1) lm101 by (metis distinct.simps(2) insert_is_Un list.simps(15)) 
  ultimately have "?P X" by (rule structInduct)
  then show ?thesis using assms(2) by blast
qed

lemma lm102: 
  assumes "l ∈ set (all_partitions_list G)" "distinct G" 
  shows   "distinct l" 
  using assms by (metis all_partitions_equivalence')

(* apply bridging theorem injections_equiv to the partitions of all goods *)
lemma bridgingInjection: 
  assumes "card N > 0" "distinct G" 
  shows "∀l ∈ set (all_partitions_list G). set (injections_alg l N) = 
         injections (set l) N"
  using lm102 injections_equiv assms by (metis card_ge_0_finite)

(* list vs set comprehension on partitions with bridging theorem *)
lemma lm103: 
  assumes "card N > 0" "distinct G"
  shows "{injections P N| P. P ∈ all_partitions (set G)} =
         set [set (injections_alg l N) . l ← all_partitions_list G]" 
proof -
  let ?g1 = all_partitions_list 
  let ?f2 = injections 
  let ?g2 = injections_alg
  have "∀l ∈ set (?g1 G). set (?g2 l N) = ?f2 (set l) N" using assms bridgingInjection by blast
  then have "set [set (?g2 l N). l <- ?g1 G] = {?f2 P N| P. P ∈ set (map set (?g1 G))}" 
     apply (rule setVsList) done
  moreover have "... = {?f2 P N| P. P ∈ all_partitions (set G)}" 
     using all_partitions_paper_equiv_alg assms by blast
  ultimately show ?thesis by presburger
qed

(* apply Union to both sides in lm103 *)
lemma lm104: 
  assumes "card N > 0" "distinct G" 
  shows   "Union {injections P N| P. P ∈ all_partitions (set G)} =
           Union (set [set (injections_alg l N) . l ← all_partitions_list G])" 
  (is "Union ?L = Union ?R")
proof - 
  have "?L = ?R" using assms by (rule lm103) thus ?thesis by presburger 
qed

(* bridging lemma for allAllocations *)
corollary allAllocationsBridgingLemma: 
  assumes "card N > 0" "distinct G" 
  shows   "allAllocations N (set G) = 
           set(allAllocationsAlg N G)" 
proof -
  let ?LL = "⋃ {injections P N| P. P ∈ all_partitions (set G)}"
  let ?RR = "⋃ (set [set (injections_alg l N) . l ← all_partitions_list G])"
  have "?LL = ?RR" using assms by (rule lm104)
  then have "converse ` ?LL = converse ` ?RR" by simp
  thus ?thesis by force
qed

end