# Theory MiscTools

```(*
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
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)

section ‹Toolbox of various definitions and theorems about sets, relations and lists›

theory MiscTools

imports
"HOL-Library.Discrete"
"HOL-Library.Code_Target_Nat"
"HOL-Library.Indicator_Function"
Argmax
RelationProperties

begin

lemmas restrict_def = RelationOperators.restrict_def

subsection ‹Facts and notations about relations, sets and functions.›

(* We use as alternative notation for paste instead of +* also +< and overload this with the next definition *)
notation paste (infix "+<" 75)

text ‹‹+<› abbreviation permits to shorten the notation for altering a function f in a single point by giving a pair (a, b) so that the new function has value b with argument a.›

abbreviation singlepaste
where "singlepaste f pair == f +* {(fst pair, snd pair)}"
notation singlepaste (infix "+<" 75)
(* Type of g in f +< g should avoid ambiguities *)

text ‹‹--› abbreviation permits to shorten the notation for considering a function outside a single point.›

abbreviation singleoutside (infix "--" 75)
where "f -- x ≡ f outside {x}"

text ‹Turns a HOL function into a set-theoretical function›

definition (*Graph :: "('a => 'b) => ('a × 'b) set" where *)
"Graph f = {(x, f x) | x . True}"

text ‹Inverts @{term Graph} (which is equivalently done by @{term eval_rel}).›
(* Assume (x, y) is in R. Apply R to x, i.e., R ,, x,  will result in y assumed y is unique. *)

definition
"toFunction R = (λ x . (R ,, x))"

(* toFunction = eval_rel *)
lemma
"toFunction = eval_rel"
using toFunction_def by blast

lemma lm001:
"((P ∪ Q) || X) = ((P || X) ∪ (Q||X))"
unfolding restrict_def by blast

text ‹update behaves like P +* Q (paste), but without enlarging P's Domain. update is the set theoretic equivalent of the lambda function update @{term fun_upd}›

definition update
where "update P Q = P +* (Q || (Domain P))"
notation update (infix "+^" 75)

(* The operator runiqer will make out of an arbitrary relation a function by making a choice to all those elements in the domain for which the value is not unique by applying the axiom of choice. *)
definition runiqer  :: "('a × 'b) set => ('a × 'b) set"
where "runiqer R = { (x, THE y. y ∈ R `` {x})| x. x ∈ Domain R }"

text ‹@{term graph} is like @{term Graph}, but with a built-in restriction to a given set @{term X}.
This makes it computable for finite X, whereas @{term "Graph f || X"} is not computable.
Duplicates the eponymous definition found in ‹Function_Order›, which is otherwise not needed.›

definition graph
where "graph X f = {(x, f x) | x. x ∈ X}"

lemma lm002:
assumes "runiq R"
shows "R ⊇ graph (Domain R) (toFunction R)"
unfolding graph_def toFunction_def
using assms graph_def toFunction_def eval_runiq_rel by fastforce

lemma lm003:
assumes "runiq R"
shows "R ⊆ graph (Domain R) (toFunction R)"
unfolding graph_def toFunction_def
using assms eval_runiq_rel runiq_basic Domain.DomainI mem_Collect_eq subrelI by fastforce

lemma lm004:
assumes "runiq R"
shows "R = graph (Domain R) (toFunction R)"
using assms lm002 lm003 by fast

lemma domainOfGraph:
"runiq(graph X f) & Domain(graph X f)=X"
unfolding graph_def
using rightUniqueRestrictedGraph by fast

(* The following definition gives the image of a relation R for a fixed element x. It is equivalent to eval_rel for right unique R, but more general since it determines values even when R is not right unique. *)
abbreviation "eval_rel2 (R::('a × ('b set)) set) (x::'a) == ⋃ (R``{x})"
notation eval_rel2 (infix ",,," 75)

lemma imageEquivalence:
assumes "runiq (f::(('a × ('b set)) set))" "x ∈ Domain f"
shows "f,,x = f,,,x"
using assms Image_runiq_eq_eval cSup_singleton by metis

(* UNIV is the universal set containing everything of the given type. It is defined in Set.thy.*)
lemma lm005:
"Graph f=graph UNIV f"
unfolding Graph_def graph_def by simp

lemma graphIntersection:
"graph (X ∩ Y) f ⊆ ((graph X f) || Y)"
unfolding graph_def
using Int_iff mem_Collect_eq RelationOperators.restrict_ext subrelI by auto

definition runiqs
where "runiqs={f. runiq f}"

lemma outsideOutside:
"((P outside X) outside Y) = P outside (X∪Y)"
unfolding Outside_def by blast

corollary lm006:
"((P outside X) outside X) = P outside X"
using outsideOutside by force

lemma lm007:
assumes "(X ∩ Domain P) ⊆ Domain Q"
shows "P +* Q = (P outside X) +* Q"
unfolding paste_def Outside_def using assms by blast

corollary lm008:
"P +* Q = (P outside (Domain Q)) +* Q"
using lm007 by fast

corollary outsideUnion:
"R = (R outside {x}) ∪ ({x} × (R `` {x}))"
using restrict_to_singleton outside_union_restrict by metis

lemma lm009:
"P = P ∪ {x}×P``{x}"
by (metis outsideUnion sup.right_idem)

corollary lm010:
"R = (R outside {x}) +* ({x} × (R `` {x}))"
by (metis paste_outside_restrict restrict_to_singleton)

lemma lm011:
"R ⊆ R +* ({x} × (R``{x}))"
using lm010 lm008 paste_def Outside_def by fast

lemma lm012:
"R ⊇ R+*({x} × (R``{x}))"
by (metis Un_least Un_upper1 outside_union_restrict paste_def
restrict_to_singleton restriction_is_subrel)

lemma lm013:
"R = R +* ({x} × (R``{x}))"
using lm011 lm012 by force

lemma rightUniqueTrivialCartes:
assumes "trivial Y"
shows "runiq (X × Y)"
using assms runiq_def Image_subset lm013 trivial_subset lm011 by (metis(no_types))

(* Two constant functions can be combined to a function *)
lemma lm014:
"runiq ((X × {x}) +* (Y × {y}))"
using rightUniqueTrivialCartes trivial_singleton runiq_paste2 by metis

lemma lm015:
"(P || (X ∩ Y)) ⊆ (P||X)    &    P outside (X ∪ Y) ⊆ P outside X"
by (metis doubleRestriction le_sup_iff outsideOutside outside_union_restrict subset_refl)

lemma lm016:
"P || X ⊆ (P||(X ∪ Y))       &    P outside X ⊆ P outside (X ∩ Y)"
using lm015 distrib_sup_le sup_idem le_inf_iff subset_antisym sup_commute
by (metis sup_ge1)

lemma lm017:
"P``(X ∩ Domain P) = P``X"
by blast

lemma cardinalityOneSubset:
assumes "card X=1" and "X ⊆ Y"
shows "Union X ∈ Y"
using assms cardinalityOneTheElemIdentity by (metis cSup_singleton insert_subset)

lemma cardinalityOneTheElem:
assumes "card X=1" "X ⊆ Y"
shows "the_elem X ∈ Y"
using assms by (metis (full_types) insert_subset cardinalityOneTheElemIdentity)

lemma lm018:
"(R outside X1) outside X2 = (R outside X2) outside X1"
by (metis outsideOutside sup_commute)

subsection ‹Ordered relations›

(* note that card ❙X≥1 means in Isabelle that X is finite and not empty *)
lemma lm019:
assumes "card X≥1" "∀x∈X. y > x"
shows "y > Max X"
using assms by (metis (poly_guards_query) Max_in One_nat_def card_eq_0_iff lessI not_le)

(* assume the function f has a maximum in mx *)
lemma lm020:
assumes "finite X" "mx ∈ X" "f x < f mx"
shows"x ∉ argmax f X"
using assms not_less by fastforce

lemma lm021:
assumes "finite X" "mx ∈ X" "∀x ∈ X-{mx}. f x < f mx"
shows "argmax f X ⊆ {mx}"
using assms mk_disjoint_insert by force

lemma lm022:
assumes "finite X" "mx ∈ X" "∀x ∈ X-{mx}. f x < f mx"
shows "argmax f X = {mx}"
using assms lm021 by (metis argmax_non_empty_iff equals0D subset_singletonD)

(* The following corollary is essentially the same as lm022, however, is simplifies a proof in UniformTieBreaking.thy *)
corollary argmaxProperty:
"(finite X & mx ∈ X & (∀aa ∈ X-{mx}. f aa < f mx)) ⟶ argmax f X = {mx}"
using lm022 by metis

corollary lm023:
assumes "finite X" "mx ∈ X" "∀x ∈ X. x ≠ mx ⟶ f x < f mx"
shows "argmax f X = {mx}"
using assms lm022 by (metis Diff_iff insertI1)

lemma lm024:
assumes "f ∘ g = id"
shows "inj_on g UNIV" using assms
by (metis inj_on_id inj_on_imageI2)

(* Note that Pow X is the powerset of X *)
lemma lm025:
assumes "inj_on f X"
shows "inj_on (image f) (Pow X)"
using assms inj_on_image_eq_iff inj_onI PowD by (metis (mono_tags, lifting))

lemma injectionPowerset:
assumes "inj_on f Y" "X ⊆ Y"
shows "inj_on (image f) (Pow X)"
using assms lm025 by (metis subset_inj_on)

(* the finest possible partition of X, e.g., X = {1, 2, 3} goes to {{1}, {2}, {3}}. *)
definition finestpart
where "finestpart X = (%x. {x}) ` X"

lemma finestPart:
"finestpart X = {{x}|x . x∈X}"
unfolding finestpart_def by blast

lemma finestPartUnion:
"X=⋃ (finestpart X)"
using finestPart by auto

lemma lm026:
"Union ∘ finestpart = id"
using finestpart_def finestPartUnion by fastforce

lemma lm027:
"inj_on Union (finestpart ` UNIV)"
using lm026 by (metis inj_on_id inj_on_imageI)

lemma nonEqualitySetOfSets:
assumes "X ≠ Y"
shows "{{x}| x. x ∈ X} ≠ {{x}| x. x ∈ Y}"
using assms by auto

corollary lm028:
"inj_on finestpart UNIV"
using nonEqualitySetOfSets finestPart by (metis (lifting, no_types) injI)

(* E.g. in the following example, with X = {{1}, {1,2}}, x can be {1} and {1,2} and Y is {{1}} and {{1},{2}}, that is, the lefthand and righthand sides evaluate to {{1},{2}} *)
lemma unionFinestPart:
"{Y | Y. ∃x.((Y ∈ finestpart x) ∧ (x ∈ X))} = ⋃(finestpart`X)"
by auto

(* Now we specialize the previous lemma to the situation where X consists of a relation (that is is a set of pairs) *)
lemma rangeSetOfPairs:
"Range {(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ X} =
{Y. ∃x. ((Y ∈ finestpart x) ∧ (x ∈ Range X))}"
by auto

(* Further specialization to a singleton for Y *)
lemma setOfPairsEquality:
"{(fst pair, {y})| y pair. y ∈ snd pair & pair ∈ X} =
{(fst pair, Y)| Y pair. Y ∈ finestpart (snd pair) & pair ∈ X}"
using finestpart_def by fastforce

lemma setOfPairs:
"{(fst pair, {y})| y. y ∈  snd pair} =
{fst pair} × {{y}| y. y ∈ snd pair}"
by fastforce

lemma lm029:
"x ∈ X = ({x} ∈ finestpart X)"
using finestpart_def by force

lemma pairDifference:
"{(x,X)}-{(x,Y)} = {x}×({X}-{Y})"
by blast

lemma lm030:
assumes "⋃ P = X"
shows "P ⊆ Pow X"
using assms by blast

lemma lm031:
"argmax f {x} = {x}"
by auto

lemma sortingSameSet:
assumes "finite X"
shows "set (sorted_list_of_set X) = X"
using assms by simp

(* We assume for the next lemma that f has value in numbers, and sum f A is
sum f(x) for x in A. *)
lemma lm032:
assumes "finite A"
shows "sum f A = sum f (A ∩ B) + sum f (A - B)"
using assms by (metis DiffD2 Int_iff Un_Diff_Int Un_commute finite_Un sum.union_inter_neutral)

corollary sumOutside:
assumes "finite g"
shows "sum f g = sum f (g outside X) + (sum f (g||X))"
unfolding Outside_def restrict_def using assms add.commute inf_commute lm032 by (metis)

lemma lm033:
assumes "(Domain P ⊆ Domain Q)"
shows "(P +* Q) = Q"
unfolding paste_def Outside_def using assms by fast

lemma lm034:
assumes "(P +* Q=Q)"
shows "(Domain P ⊆ Domain Q)"
using assms paste_def Outside_def by blast

lemma lm035:
"(Domain P ⊆ Domain Q) = (P +* Q=Q)"
using lm033 lm034 by metis

lemma
"(P||(Domain Q)) +* Q = Q"
by (metis Int_lower2 restrictedDomain lm035)

lemma lm036:
"P||X   =   P outside (Domain P - X)"
using Outside_def restrict_def by fastforce

lemma lm037:
"(P outside X) ⊆    P || ((Domain P)-X)"
using lm036 lm016 by (metis Int_commute restrictedDomain outside_reduces_domain)

lemma lm038:
"Domain (P outside X) ∩ Domain (Q || X) = {}"
using lm036
by (metis Diff_disjoint Domain_empty_iff Int_Diff inf_commute restrictedDomain
outside_reduces_domain restrict_empty)

lemma lm039:
"(P outside X) ∩ (Q || X) = {}"
using lm038 by fast

lemma lm040:
"(P outside (X ∪ Y)) ∩ (Q || X) = {}   &   (P outside X) ∩ (Q || (X ∩ Z)) = {}"
using Outside_def restrict_def lm039 lm015 by fast

lemma lm041:
"P outside X    =    P || ((Domain P) - X)"
using Outside_def restrict_def lm037 by fast

lemma lm042:
"R``(X-Y) = (R||X)``(X-Y)"
using restrict_def by blast

(* x is a (non-empty) element of the family XX whose union is a subset of X *)
lemma lm043:
assumes "⋃ XX ⊆ X" "x ∈ XX" "x ≠ {}"
shows "x ∩ X ≠ {}"
using assms by blast

(* Note that set converts lists such as L1 into sets. L1 is here a list of lists and l an element, that is, a list. We assume furthermore that f2 is constant function with the fixed 2nd argument N. Then we can convert lists to sets in a canonical way. *)
lemma lm044:
assumes "∀l ∈ set L1. set L2 = f2 (set l) N"
shows "set [set L2. l <- L1]  =  {f2 P N| P. P ∈ set (map set L1)}"
using assms by auto

(* Two Variants of the previous lemma *)
lemma setVsList:
assumes "∀l ∈ set (g1 G). set (g2 l N) = f2 (set l) N"
shows "set [set (g2 l N). l <- (g1 G)]  =  {f2 P N| P. P ∈ set (map set (g1 G))}"
using assms by auto

lemma lm045:
"(∀l ∈ set (g1 G). set (g2 l N) = f2 (set l) N) -->
{f2 P N| P. P ∈ set (map set (g1 G))} = set [set (g2 l N). l <- g1 G]"
by auto

lemma lm046:
assumes "X ∩ Y  =  {}"
shows "R``X = (R outside Y)``X"
using assms Outside_def Image_def by blast

lemma lm047:
assumes "(Range P) ∩ (Range Q) = {}" "runiq (P^-1)" "runiq (Q^-1)"
shows "runiq ((P ∪ Q)^-1)"
using assms by (metis Domain_converse converse_Un disj_Un_runiq)

lemma lm048:
assumes "(Range P) ∩ (Range Q) = {}" "runiq (P^-1)" "runiq (Q^-1)"
shows "runiq ((P +* Q)^-1)"
using lm047 assms subrel_runiq by (metis converse_converse converse_subset_swap paste_sub_Un)

lemma lm049:
assumes "runiq R"
shows "card (R `` {a}) = 1 ⟷ a ∈ Domain R"
using assms card_Suc_eq One_nat_def
by (metis Image_within_domain' Suc_neq_Zero assms rightUniqueSetCardinality)

(* triples a can be bracket in any way, i.e., (1st, (2nd, 3rd)) → ((1st, 2nd), 3rd).*)
lemma lm050:
"inj (λa. ((fst a, fst (snd a)), snd (snd a)))"
by (auto intro: injI)

lemma lm051:
assumes "finite X" "x > Max X"
shows "x ∉ X"
using assms Max.coboundedI by (metis leD)

lemma lm052:
assumes "finite A" "A ≠ {}"
shows "Max (f`A) ∈ f`A"
using assms by (metis Max_in finite_imageI image_is_empty)

(* Note that in the following -` means the inverse image of the following set. *)
lemma lm053:
"argmax f A ⊆ f -` {Max (f ` A)}"
by force

lemma lm054:
"argmax f A = A ∩ { x . f x = Max (f ` A) }"
by auto

lemma lm055:
"(x ∈ argmax f X) = (x ∈ X & f x = Max (f ` X))"
using argmax.simps mem_Collect_eq by (metis (mono_tags, lifting))

lemma rangeEmpty:
"Range -` {{}} = {{}}"
by auto

lemma finitePairSecondRange:
"(∀ pair ∈ R. finite (snd pair)) = (∀ y ∈ Range R. finite y)"
by fastforce

lemma lm056:
"fst ` P = snd ` (P^-1)"
by force

lemma lm057:
"fst pair = snd (flip pair) & snd pair = fst (flip pair)"
unfolding flip_def by simp

lemma flip_flip2:
"flip ∘ flip   =   id"
using flip_flip by fastforce

lemma lm058:
"fst = (snd∘flip)"
using lm057 by fastforce

lemma lm059:
"snd = (fst∘flip)"
using lm057 by fastforce

lemma lm060:
"inj_on fst P = inj_on (snd∘flip) P"
using lm058 by metis

lemma lm062:
"inj_on fst P = inj_on snd (P^-1)"
using lm060 flip_conv by (metis converse_converse inj_on_imageI lm059)

lemma sumPairsInverse:
assumes "runiq (P^-1)"
shows "sum (f ∘ snd) P = sum f (Range P)"
using assms lm062 converse_converse rightUniqueInjectiveOnFirst rightUniqueInjectiveOnFirst
sum.reindex snd_eq_Range
by metis

lemma notEmptyFinestpart:
assumes "X ≠ {}"
shows "finestpart X ≠ {}"
using assms finestpart_def by blast

lemma lm063:
assumes "inj_on g X"
shows "sum f (g`X) = sum (f ∘ g) X"
using assms by (metis sum.reindex)

lemma functionOnFirstEqualsSecond:
assumes "runiq R" "z ∈ R"
shows "R,,(fst z) = snd z"
using assms by (metis rightUniquePair surjective_pairing)

lemma lm064:
assumes "runiq R"
shows "sum (toFunction R) (Domain R) = sum snd R"
using assms toFunction_def sum.reindex_cong functionOnFirstEqualsSecond
rightUniqueInjectiveOnFirst
by (metis (no_types) fst_eq_Domain)

corollary lm065:
assumes "runiq (f||X)"
shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum snd (f||X)"
using assms lm064 by (metis Int_commute restrictedDomain)

lemma lm066:
"Range (R outside X) = R``((Domain R) - X)"
by (metis Diff_idemp ImageE Range.intros Range_outside_sub_Image_Domain lm041
lm042 order_class.order.antisym subsetI)

lemma lm067:
"(R||X) `` X = R``X"
using Int_absorb doubleRestriction restrictedRange by metis

lemma lm068:
assumes "x ∈ Domain (f||X)"
shows "(f||X)``{x} = f``{x}"
using assms doubleRestriction restrictedRange Int_empty_right Int_iff
Int_insert_right_if1 restrictedDomain
by metis

lemma lm069:
assumes "x ∈ X ∩ Domain f" "runiq (f||X)"
shows "(f||X),,x = f,,x"
using assms doubleRestriction restrictedRange Int_empty_right Int_iff Int_insert_right_if1
eval_rel.simps
by metis

lemma lm070:
assumes "runiq (f||X)"
shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum (toFunction f) (X ∩ Domain f)"
using assms sum.cong lm069 toFunction_def by metis

corollary sumRestrictedToDomainInvariant:
assumes "runiq (f||X)"
shows "sum (toFunction f) (X ∩ Domain f) = sum snd (f||X)"
using assms lm065 lm070 by fastforce

corollary sumRestrictedOnFunction:
assumes "runiq (f||X)"
shows "sum (toFunction (f||X)) (X ∩ Domain f) = sum snd (f||X)"
using assms lm064 restrictedDomain Int_commute by metis

lemma cardFinestpart:
"card (finestpart X) = card X"
using finestpart_def by (metis (lifting) card_image inj_on_inverseI the_elem_eq)

corollary lm071:
"finestpart {} = {}    &    card ∘ finestpart = card"
using cardFinestpart finestpart_def by fastforce

lemma finiteFinestpart:
"finite (finestpart X) = finite X"
using finestpart_def lm071
by (metis card_eq_0_iff empty_is_image finite.simps cardFinestpart)

lemma lm072:
"finite ∘ finestpart = finite"
using finiteFinestpart by fastforce

lemma finestpartSubset:
assumes "X ⊆ Y"
shows "finestpart X ⊆ finestpart Y"
using assms finestpart_def by (metis image_mono)

corollary lm073:
assumes "x ∈ X"
shows "finestpart x ⊆ finestpart (⋃ X)"
using assms finestpartSubset by (metis Union_upper)

lemma lm074:
"⋃ (finestpart ` XX) ⊆ finestpart (⋃ XX)"
using finestpart_def lm073 by force

lemma lm075:
"⋃ (finestpart ` XX) ⊇ finestpart (⋃ XX)"
(is "?L ⊇ ?R")
unfolding finestpart_def using finestpart_def by auto

corollary commuteUnionFinestpart:
"⋃ (finestpart ` XX) = finestpart (⋃ XX)"
using lm074 lm075 by fast

lemma unionImage:
assumes "runiq a"
shows "{(x, {y})| x y. y ∈ ⋃ (a``{x}) & x ∈ Domain a} =
{(x, {y})| x y. y ∈ a,,x & x ∈ Domain a}"
using assms Image_runiq_eq_eval
by (metis (lifting, no_types) cSup_singleton)

lemma lm076:
assumes "runiq P"
shows "card (Domain P) = card P"
using assms rightUniqueInjectiveOnFirst card_image by (metis Domain_fst)

lemma finiteDomainImpliesFinite:
assumes "runiq f"
shows "finite (Domain f) = finite f"
using assms Domain_empty_iff card_eq_0_iff finite.emptyI lm076 by metis

(* A relation for the sum of all y∈Y of f(x,y) for a fixed x. *)
lemma sumCurry:
"sum ((curry f) x) Y = sum f ({x} × Y)"
proof -
let ?f="% y. (x, y)" let ?g="(curry f) x" let ?h=f
have "inj_on ?f Y" by (metis(no_types) Pair_inject inj_onI)
moreover have "{x} × Y = ?f ` Y" by fast
moreover have "∀ y. y ∈ Y ⟶ ?g y = ?h (?f y)" by simp
ultimately show ?thesis using sum.reindex_cong by metis
qed

lemma lm077:
"sum (%y. f (x,y)) Y = sum f ({x}×Y)"
using sumCurry Sigma_cong curry_def sum.cong by fastforce

corollary lm078:
assumes "finite X"
shows "sum f X = sum f (X-Y) + (sum f (X ∩ Y))"
using assms Diff_iff IntD2 Un_Diff_Int finite_Un inf_commute sum.union_inter_neutral
by metis

lemma lm079:
"(P +* Q)``(Domain Q∩X)  =  Q``(Domain Q∩X)"
unfolding paste_def Outside_def Image_def Domain_def by blast

corollary lm080:
"(P +* Q)``(X∩(Domain Q))  =  Q``X"
using Int_commute lm079 by (metis lm017)

corollary lm081:
assumes "X ∩ (Domain Q) = {}"
shows "(P +* Q) `` X = (P outside (Domain Q))`` X"
using assms paste_def by fast

lemma lm082:
assumes "X∩Y = {}"
shows "(P outside Y)``X=P``X"
using assms Outside_def by blast

corollary lm083:
assumes "X∩ (Domain Q) = {}"
shows "(P +* Q)``X=P``X"
using assms lm081 lm082 by metis

lemma lm084:
assumes "finite X" "finite Y" "card(X∩Y) = card X"
shows "X ⊆ Y"
using assms by (metis Int_lower1 Int_lower2 card_seteq order_refl)

lemma cardinalityIntersectionEquality:
assumes "finite X" "finite Y" "card X = card Y"
shows "(card (X∩Y) = card X)     =    (X = Y)"
using assms lm084 by (metis card_seteq le_iff_inf order_refl)

lemma lm085: (*fixes f::"'a => 'b" fixes P::"'a => bool" fixes xx::"'a"*)
assumes "P xx"
shows "{(x,f x)| x. P x},,xx   =   f xx"
proof -
let ?F="{(x,f x)| x. P x}" let ?X="?F``{xx}"
have "?X={f xx}" using Image_def assms by blast thus ?thesis by fastforce
qed

lemma graphEqImage:
assumes "x ∈ X"
shows "graph X f,,x   =   f x"
unfolding graph_def using assms lm085 by (metis (mono_tags) Gr_def)

lemma lm086:
"Graph f,,x    =    f x"
using UNIV_I graphEqImage lm005 by (metis(no_types))

lemma lm087:
"toFunction (Graph f)    =    f"    (is "?L=_")
proof -
{fix x have "?L x=f x" unfolding toFunction_def lm086 by metis}
thus ?thesis by blast
qed

lemma lm088:
"R outside X ⊆ R"
by (metis outside_union_restrict subset_Un_eq sup_left_idem)

lemma lm089:
"Range(f outside X) ⊇ (Range f)-(f``X)"
using Outside_def by blast

lemma lm090:
assumes "runiq P"
shows "(P¯``((Range P)-Y)) ∩ ((P¯)``Y)   =   {}"
using assms rightUniqueFunctionAfterInverse by blast

lemma lm091:
assumes "runiq (P¯)"
shows "(P``((Domain P) - X)) ∩ (P``X)  =  {}"
using assms rightUniqueFunctionAfterInverse by fast

lemma lm092:
assumes "runiq f" "runiq (f^-1)"
shows "Range(f outside X) ⊆ (Range f)-(f``X)"
using assms Diff_triv lm091 lm066 Diff_iff ImageE Range_iff subsetI by metis

lemma rangeOutside:
assumes "runiq f" "runiq (f^-1)"
shows "Range(f outside X) = (Range f)-(f``X)"
using assms lm089 lm092 by (metis order_class.order.antisym)

(* X and Y are family of sets such that any x and y in X and Y resp. are disjoint. *)
lemma unionIntersectionEmpty:
"(∀x∈X. ∀y∈Y. x∩y = {}) = ((⋃X)∩(⋃ Y)={})"
by blast

lemma setEqualityAsDifference:
"{x}-{y} = {}  =  (x = y)"
by auto

lemma lm093:
assumes "R ≠ {}" "Domain R ∩ X ≠ {}"
shows "R``X ≠ {}"
using assms by blast

lemma lm095:
"R ⊆ (Domain R) × (Range R)"
by auto

lemma finiteRelationCharacterization:
"(finite (Domain Q) & finite (Range Q)) = finite Q"
using rev_finite_subset finite_SigmaI lm095 finite_Domain finite_Range by metis

lemma familyUnionFiniteEverySetFinite:
assumes "finite (⋃ XX)"
shows "∀X ∈ XX. finite X"
using assms by (metis Union_upper finite_subset)

lemma lm096:
assumes "runiq f" "X ⊆ (f^-1)``Y"
shows "f``X ⊆ Y"
using assms rightUniqueFunctionAfterInverse by (metis Image_mono order_refl subset_trans)

lemma lm097:
assumes "y ∈ f``{x}" "runiq f"
shows "f,,x = y"
using assms by (metis Image_singleton_iff rightUniquePair)

subsection ‹Indicator function in set-theoretical form.›

abbreviation
"Outside' X f == f outside X"

abbreviation
"Chi X Y == (Y × {0::nat}) +* (X × {1})"
notation Chi (infix "<||" 80)

abbreviation
"chii X Y == toFunction (X <|| Y)"
notation chii (infix "<|" 80)

(* X is a set and chi X is a function that returns 1 for elements X and 0 else. *)
abbreviation
"chi X == indicator X"

lemma lm098:
"runiq (X <|| Y)"
by (rule lm014)

lemma lm099:
assumes "x ∈ X"
shows "1 ∈ (X <|| Y) `` {x}"
using assms toFunction_def paste_def Outside_def runiq_def lm014 by blast

lemma lm100:
assumes "x ∈ Y-X"
shows "0 ∈ (X <|| Y) `` {x}"
using assms toFunction_def paste_def Outside_def runiq_def lm014 by blast

lemma lm101:
assumes "x ∈ X ∪ Y"
shows "(X <|| Y),,x = chi X x" (is "?L=?R")
using assms lm014 lm099 lm100 lm097
by (metis DiffI Un_iff indicator_simps(1) indicator_simps(2))

lemma lm102:
assumes "x ∈ X ∪ Y"
shows "(X <| Y) x = chi X x"
using assms toFunction_def lm101 by metis

corollary lm103:
"sum (X <| Y) (X∪Y) = sum (chi X) (X∪Y)"
using lm102 sum.cong by metis

corollary lm104:
assumes "∀x∈X. f x = g x"
shows "sum f X = sum g X"
using assms by (metis (poly_guards_query) sum.cong)

corollary lm105:
assumes "∀x∈X. f x = g x" "Y⊆X"
shows "sum f Y = sum g Y"
using assms lm104 by (metis contra_subsetD)

corollary lm106:
assumes "Z ⊆ X ∪ Y"
shows "sum (X <| Y) Z = sum (chi X) Z"
proof -
have "∀x∈Z.(X<|Y) x=(chi X) x" using assms lm102 in_mono by metis
thus ?thesis using lm104 by blast
qed

corollary lm107:
"sum (chi X) (Z - X) = 0"
by simp

corollary lm108:
assumes "Z ⊆ X ∪ Y"
shows "sum (X <| Y) (Z - X) = 0"
using assms lm107 lm106 Diff_iff in_mono subsetI by metis

corollary lm109:
assumes "finite Z"
shows "sum (X <| Y) Z    =    sum (X <| Y) (Z - X)   +  (sum (X <| Y) (Z ∩ X))"
using lm078 assms by blast

corollary lm110:
assumes "Z ⊆ X ∪ Y" "finite Z"
shows "sum (X <| Y) Z = sum (X <| Y) (Z ∩ X)"

corollary lm111:
assumes "finite Z"
shows "sum (chi X) Z = card (X ∩ Z)"
using assms sum_indicator_eq_card by (metis Int_commute)

corollary lm112:
assumes "Z ⊆ X ∪ Y" "finite Z"
shows "sum (X <| Y) Z = card (Z ∩ X)"
using assms lm111 by (metis lm106 sum_indicator_eq_card)

corollary subsetCardinality:
assumes "Z ⊆ X ∪ Y" "finite Z"
shows "(sum (X <| Y) X) - (sum (X <| Y) Z) = card X - card (Z ∩ X)"
using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)

corollary differenceSumVsCardinality:
assumes "Z ⊆ X ∪ Y" "finite Z"
shows "int (sum (X <| Y) X) - int (sum (X <| Y) Z) =  int (card X) - int (card (Z ∩ X))"
using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)

(* type conversion in Isabelle *)
lemma lm113:
"int (n::nat) = real n"
by simp

(* same as differenceSumVsCardinality but for type real *)
corollary differenceSumVsCardinalityReal:
assumes "Z⊆X∪Y" "finite Z"
shows "real (sum (X <| Y) X) - real (sum (X <| Y) Z) =
real (card X) - real (card (Z ∩ X))"
using assms lm112 by (metis Int_absorb2 Un_upper1 card.infinite equalityE sum.infinite)

subsection ‹Lists›
(* If there is an element in a list satisfying P, then the list of all elements satisfying P is not the empty list *)
lemma lm114:
assumes "∃ n ∈ {0..<size l}. P (l!n)"
shows "[n. n ← [0..<size l], P (l!n)] ≠ []"
using assms by auto

(* Assume ll is an element of list l, then there is an index n such that the n-th entry of l is ll. *)
lemma lm115:
assumes "ll ∈ set (l::'a list)"
shows "∃ n∈ (nth l) -` (set l). ll=l!n"
using assms(1) by (metis in_set_conv_nth vimageI2)

(* variant of the above *)
lemma lm116:
assumes "ll ∈ set (l::'a list)"
shows "∃ n. ll=l!n & n < size l & n >= 0"
using assms in_set_conv_nth by (metis le0)

(* another variant of the above *)
lemma lm117:
assumes "P -` {True} ∩ set l ≠ {}"
shows "∃ n ∈ {0..<size l}. P (l!n)"
using assms lm116 by fastforce

(* variant of lm114 *)
lemma nonEmptyListFiltered:
assumes "P -` {True} ∩ set l ≠ {}"
shows "[n. n ← [0..<size l], P (l!n)] ≠ []"
using assms filterpositions2_def lm117 lm114 by metis

(* take the elements of a list l which are also in a set X then this forms a subset of X intersection with the elements of the list *)
lemma lm118:
"(nth l) ` set ([n. n ← [0..<size l], (%x. x∈X) (l!n)]) ⊆ X∩set l"
by force

(* variant of the above *)
corollary lm119:
"(nth l)` set (filterpositions2 (%x.(x∈X)) l) ⊆ X ∩  set l"
unfolding filterpositions2_def using lm118 by fast

lemma lm120:
"(n∈{0..<N}) = ((n::nat) < N)"
using atLeast0LessThan lessThan_iff by metis

(* If X is a set of indices then the corresponding elements combined are a subset of all the elements of the list. *)
lemma lm121:
assumes "X ⊆ {0..<size list}"
shows "(nth list)`X ⊆ set list"
using assms atLeastLessThan_def atLeast0LessThan lessThan_iff by auto

(* The indices of the elements of a list satisfying a predicate P are a subset of all the indices. *)
lemma lm122:
"set ([n. n ← [0..<size l], P (l!n)]) ⊆ {0..<size l}"
by force

(* variant of the above *)
lemma lm123:
"set (filterpositions2 pre list) ⊆ {0..<size list}"
using filterpositions2_def lm122 by metis

subsection ‹Computing all the permutations of a list›
abbreviation
"rotateLeft == rotate"
abbreviation
"rotateRight n l == rotateLeft (size l - (n mod (size l))) l"

(* for n in {0, ..., size l} inserts x in l so that it will have index n in the output*)
(* note that for other n, the behaviour is not guaranteed to be consistent with that *)
abbreviation
"insertAt x l n == rotateRight n (x#(rotateLeft n l))"

(* for n in {0,..., fact(size l) - 1 },
perm2 l n gives all and only the possible permutations of l *)
fun perm2 where
"perm2 [] = (%n. [])" |
"perm2 (x#l) = (%n. insertAt x ((perm2 l) (n div (1+size l)))
(n mod (1+size l)))"

abbreviation
"takeAll P list == map (nth list) (filterpositions2 P list)"

lemma permutationNotEmpty:
assumes "l ≠ []"
shows "perm2 l n ≠ []"
using assms perm2.simps(2) rotate_is_Nil_conv by (metis neq_Nil_conv)

lemma lm124:
"set (takeAll P list) = ((nth list) ` set (filterpositions2 P list))"
by simp

corollary listIntersectionWithSet:
"set (takeAll (%x.(x∈X)) l) ⊆  (X ∩ set l)"
using lm119 lm124 by metis

corollary lm125:
"set (takeAll P list) ⊆ set list"
using lm123 lm124 lm121 by metis

lemma takeAllSubset:
"set (takeAll (%x. x∈ P) list) ⊆ P"
by (metis Int_subset_iff listIntersectionWithSet)

lemma lm126:
"set (insertAt x l n) = {x} ∪ set l"
by simp

lemma lm127:
"∀n. set (perm2 [] n) = set []"
by simp

lemma lm128:
assumes "∀n. (set (perm2 l n) = set l)"
shows "set (perm2 (x#l) n) = {x} ∪ set l"
using assms lm126 by force

(* Combining the previous two lemmas we get inductively that the set of elements in a permuted list are the same as the elements in the original list. This is weaker than saying (perm2 l n) is a permutation of l, but suffices for our purposes. *)
corollary permutationInvariance:
"∀n. set (perm2 (l::'a list) n) = set l"
proof (induct l)
let ?P = "%l::('a list). (∀n. set (perm2 l n)  =  set l)"
show "?P []" using lm127 by force
fix x fix l
assume "?P l" then
show "?P (x#l)" by force
qed

(* variant of listIntersectionWithSet with permutation added *)
corollary takeAllPermutation:
"set (perm2 (takeAll (%x.(x∈X)) l) n)  ⊆  X ∩ set l"
using listIntersectionWithSet permutationInvariance by metis

(* "subList list1 list2" extracts the components of list1 according to the indices given in list2, e.g.,  "subList [1::nat,2,3,4] [0,2]" gives [1,3] *)
abbreviation "subList l xl == map (nth l) (takeAll (%x. x ≤ size l) xl)"

subsection ‹A more computable version of @{term toFunction}.›

(* If R is a relation and the image of x is unique then take that, else take the fallback *)
abbreviation "toFunctionWithFallback R fallback ==
(% x. if (R``{x} = {R,,x}) then (R,,x) else fallback)"
notation
toFunctionWithFallback (infix "Else" 75)

abbreviation sum' where
"sum' R X == sum (R Else 0) X"

lemma lm129:
assumes "runiq f" "x ∈ Domain f"
shows "(f Else 0) x = (toFunction f) x"
using assms by (metis Image_runiq_eq_eval toFunction_def)

lemma lm130:
assumes "runiq f"
shows "sum (f Else 0) (X∩(Domain f))  =  sum (toFunction f) (X∩(Domain f))"
using assms sum.cong lm129 by fastforce

lemma lm131:
assumes "Y ⊆ f-`{0}"
shows "sum f Y  =  0"
using assms by (metis rev_subsetD sum.neutral vimage_singleton_eq)

lemma lm132:
assumes "Y ⊆ f-`{0}" "finite X"
shows "sum f X = sum f (X-Y)"
using Int_lower2 add.comm_neutral assms(1) assms(2) lm078 lm131 order_trans
by (metis (no_types))

(* - means the complement of a set. *)
lemma lm133:
"-(Domain f) ⊆ (f Else 0)-`{0}"
by fastforce

corollary lm134:
assumes "finite X"
shows "sum (f Else 0) X    =   sum (f Else 0) (X∩Domain f)"
proof -
have "X∩Domain f=X-(-Domain f)" by simp
thus ?thesis using assms lm133 lm132 by fastforce
qed

corollary lm135:
assumes "finite X"
shows "sum (f Else 0) (X∩Domain f)   =   sum (f Else 0) X"
(is "?L=?R")
proof -
have "?R=?L" using assms by (rule lm134)
thus ?thesis by simp
qed

corollary lm136:
assumes "finite X" "runiq f"
shows "sum (f Else 0) X = sum (toFunction f) (X∩Domain f)"
(is "?L=?R")
proof -
have "?R = sum (f Else 0) (X∩Domain f) " using assms(2) lm130 by fastforce
moreover have "... = ?L" using assms(1) by (rule lm135)
ultimately show ?thesis by presburger
qed

lemma lm137:
"sum (f Else 0) X = sum' f X"
by fast

corollary lm138:
assumes "finite X" "runiq f"
shows "sum (toFunction f) (X∩Domain f)   =   sum' f X"
using assms lm137 lm136 by fastforce

lemma lm139:
"argmax (sum' b) = (argmax ∘ sum') b"
by simp

lemma domainConstant:
"Domain (Y × {0::nat}) = Y & Domain (X × {1}) = X"
by blast

lemma domainCharacteristicFunction:
"Domain (X <|| Y) = X ∪ Y"
using domainConstant paste_Domain sup_commute by metis

lemma functionEquivalenceOnSets:
assumes "∀x ∈ X. f x = g x"
shows "f`X = g`X"
using assms by (metis image_cong)

subsection ‹Cardinalities of sets.›
lemma lm140:
assumes "runiq R" "runiq (R^-1)"
shows "(R``A) ∩ (R``B) = R``(A∩B)"
using assms rightUniqueInjectiveOnFirst converse_Image by force

lemma intersectionEmptyRelationIntersectionEmpty:
assumes "runiq (R^-1)" "runiq R" "X1 ∩ X2 = {}"
shows "(R``X1) ∩ (R``X2) = {}"
using assms by (metis disj_Domain_imp_disj_Image inf_assoc inf_bot_right)

lemma lm141:
assumes "runiq f" "trivial Y"
shows "trivial (f `` (f^-1 `` Y))"
using assms by (metis rightUniqueFunctionAfterInverse trivial_subset)

lemma lm142:
assumes "trivial X"
shows "card (Pow X)∈{1,2}"
using trivial_empty_or_singleton card_Pow Pow_empty assms trivial_implies_finite
cardinalityOneTheElemIdentity power_one_right the_elem_eq
by (metis insert_iff)

lemma lm143:
assumes "card (Pow A) = 1"
shows "A = {}"
using assms by (metis Pow_bottom Pow_top cardinalityOneTheElemIdentity singletonD)

(* Note that in Isabelle infinite sets have cardinality 0 *)
lemma lm144:
"(¬ (finite A)) = (card (Pow A) = 0)"
by auto

corollary lm145:
"(finite A) = (card (Pow A) ≠ 0)"
using lm144 by metis

lemma lm146:
assumes "card (Pow A) ≠ 0"
shows "card A=Discrete.log (card (Pow A))"
using assms log_exp card_Pow by (metis card.infinite finite_Pow_iff)

lemma log_2 [simp]:
"Discrete.log 2 = 1"
using log_exp [of 1] by simp

lemma lm147:
assumes "card (Pow A) = 2"
shows "card A = 1"
using assms lm146 [of A] by simp

lemma lm148:
assumes "card (Pow X) = 1 ∨ card (Pow X) = 2"
shows "trivial X"
using assms trivial_empty_or_singleton lm143 lm147 cardinalityOneTheElemIdentity by metis

lemma lm149:
"trivial A = (card (Pow A) ∈ {1,2})"
using lm148 lm142 by blast

lemma lm150:
assumes "R ⊆ f" "runiq f" "Domain f = Domain R"
shows "runiq R"
using assms by (metis subrel_runiq)

lemma lm151:
assumes "f ⊆ g" "runiq g" "Domain f = Domain g"
shows "g ⊆ f"
using assms Domain_iff contra_subsetD runiq_wrt_ex1 subrelI
by (metis (full_types,opaque_lifting))

lemma lm152:
assumes "R ⊆ f" "runiq f" "Domain f ⊆ Domain R"
shows "f = R"
using assms lm151 by (metis Domain_mono dual_order.antisym)

lemma lm153:
"graph X f = (Graph f) || X"
using inf_top.left_neutral lm005 domainOfGraph restrictedDomain lm152 graphIntersection
restriction_is_subrel subrel_runiq subset_iff
by (metis (erased, lifting))

lemma lm154:
"graph (X ∩ Y) f = (graph X f) || Y"
using doubleRestriction lm153 by metis

lemma restrictionVsIntersection:
"{(x, f x)| x. x ∈ X2} || X1 = {(x, f x)| x. x ∈ X2 ∩ X1}"
using graph_def lm154 by metis

lemma lm155:
assumes "runiq f" "X ⊆ Domain f"
shows "graph X (toFunction f) = (f||X)"
proof -
have "⋀v w. (v::'a set) ⊆ w ⟶ w ∩ v = v" by (simp add: Int_commute inf.absorb1)
thus "graph X (toFunction f) = f || X" by (metis assms(1) assms(2) doubleRestriction lm004 lm153)
qed

lemma lm156:
"(Graph f) `` X = f ` X"
unfolding Graph_def image_def by auto

lemma lm157:
assumes "X ⊆ Domain f" "runiq f"
shows "f``X = (eval_rel f)`X"
using assms lm156 by (metis restrictedRange lm153 lm155 toFunction_def)

lemma cardOneImageCardOne:
assumes "card A = 1"
shows "card (f`A) = 1"
using assms card_image card_image_le
proof -
have "finite (f`A)" using assms One_nat_def Suc_not_Zero card.infinite finite_imageI
by (metis(no_types))
moreover have "f`A ≠ {}" using assms by fastforce
moreover have "card (f`A) ≤ 1" using assms card_image_le One_nat_def Suc_not_Zero card.infinite
by (metis)
ultimately show ?thesis by (metis assms image_empty image_insert
cardinalityOneTheElemIdentity the_elem_eq)
qed

lemma cardOneTheElem:
assumes "card A = 1"
shows "the_elem (f`A) = f (the_elem A)"
using assms image_empty image_insert the_elem_eq by (metis cardinalityOneTheElemIdentity)

(* With split being the inverse of curry we have with g as swap f,  (g x y) = (f y x) *)
abbreviation
"swap f == curry ((case_prod f) ∘ flip)" (*swaps the two arguments of a function*)

(* X is finite if and only if X is the set of elements of some list. *)
lemma lm158:
"finite X   =  (X ∈ range set)"
by (metis List.finite_set finite_list image_iff rangeI)

(* as above, just as lambda expression *)
lemma lm159:
"finite = (%X. X∈range set)"
using lm158 by metis

lemma lm160:
"swap f = (%x. %y. f y x)"
by (metis comp_eq_dest_lhs curry_def flip_def fst_conv old.prod.case snd_conv)

subsection ‹Some easy properties on real numbers›
lemma lm161:
fixes a::real
fixes b c
shows "a*b - a*c=a*(b-c)"
by (metis real_scaleR_def real_vector.scale_right_diff_distrib)

lemma lm162:
fixes a::real
fixes b c
shows "a*b - c*b=(a-c)*b"
using lm161 by (metis mult.commute)

end

```