(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2005, 2006 Slawomir Kolodynski

This program is free software Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED

WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF

MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,

PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS

OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,

WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR

OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,

EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

header{*\isaheader{func1.thy}*}

theory func1 imports func Fol1 ZF1

begin

text{*This theory covers basic properties of function spaces.

A set of functions with domain $X$ and values in the set $Y$

is denoted in Isabelle as $X\rightarrow Y$. It just happens

that the colon ":" is a synonym of the set membership symbol

$\in$ in Isabelle/ZF so we can write $f:X\rightarrow Y$ instead of

$f \in X\rightarrow Y$. This is the only case that we use the colon

instead of the regular set membership symbol.*}

section{*Properties of functions, function spaces and (inverse) images.*}

text{*Functions in ZF are sets of pairs. This means

that if $f: X\rightarrow Y $ then $f\subseteq X\times Y$.

This section is mostly about consequences of this understanding

of the notion of function.

*}

text{*We define the notion of function that preserves a collection here.

Given two collection of sets a function preserves the collections if

the inverse image of sets in one collection belongs to the second one.

This notion does not have a name in romantic math. It is used to define

continuous functions in @{text "Topology_ZF_2"} theory.

We define it here so that we can

use it for other purposes, like defining measurable functions.

Recall that @{text "f-``(A)"} means the inverse image of the set $A$.*}

definition

"PresColl(f,S,T) ≡ ∀ A∈T. f-``(A)∈S"

text{*A definition that allows to get the first factor of the

domain of a binary function $f: X\times Y \rightarrow Z$.*}

definition

"fstdom(f) ≡ domain(domain(f))"

text{*If a function maps $A$ into another set, then $A$ is the

domain of the function.*}

lemma func1_1_L1: assumes "f:A->C" shows "domain(f) = A"

using assms domain_of_fun by simp

text{*Standard Isabelle defines a @{text "function(f)"} predicate.

the next lemma shows that our function satisfy that predicate.

It is a special version of Isabelle's @{text "fun_is_function"}.*}

lemma fun_is_fun: assumes "f:X->Y" shows "function(f)"

using assms fun_is_function by simp

text{*A lemma explains what @{text "fstdom"} is for.*}

lemma fstdomdef: assumes A1: "f: X×Y -> Z" and A2: "Y≠0"

shows "fstdom(f) = X"

proof -

from A1 have "domain(f) = X×Y" using func1_1_L1

by simp

with A2 show "fstdom(f) = X" unfolding fstdom_def by auto

qed

text{*A first-order version of @{text "Pi_type"}. *}

lemma func1_1_L1A: assumes A1: "f:X->Y" and A2: "∀x∈X. f`(x) ∈ Z"

shows "f:X->Z"

proof -

{ fix x assume "x∈X"

with A2 have "f`(x) ∈ Z" by simp }

with A1 show "f:X->Z" by (rule Pi_type)

qed

text{*A variant of @{text "func1_1_L1A"}.*}

lemma func1_1_L1B: assumes A1: "f:X->Y" and A2: "Y⊆Z"

shows "f:X->Z"

proof -

from A1 A2 have "∀x∈X. f`(x) ∈ Z"

using apply_funtype by auto

with A1 show "f:X->Z" using func1_1_L1A by blast

qed

text{*There is a value for each argument.*}

lemma func1_1_L2: assumes A1: "f:X->Y" "x∈X"

shows "∃y∈Y. ⟨x,y⟩ ∈ f"

proof-

from A1 have "f`(x) ∈ Y" using apply_type by simp

moreover from A1 have "⟨ x,f`(x)⟩∈ f" using apply_Pair by simp

ultimately show ?thesis by auto

qed

text{*The inverse image is the image of converse. True for relations as well.*}

lemma vimage_converse: shows "r-``(A) = converse(r)``(A)"

using vimage_iff image_iff converse_iff by auto

text{*The image is the inverse image of converse.*}

lemma image_converse: shows "converse(r)-``(A) = r``(A)"

using vimage_iff image_iff converse_iff by auto

text{*The inverse image by a composition is the composition of inverse images.*}

lemma vimage_comp: shows "(r O s)-``(A) = s-``(r-``(A))"

using vimage_converse converse_comp image_comp image_converse by simp

text{*A version of @{text "vimage_comp"} for three functions.*}

lemma vimage_comp3: shows "(r O s O t)-``(A) = t-``(s-``(r-``(A)))"

using vimage_comp by simp

text{*Inverse image of any set is contained in the domain.*}

lemma func1_1_L3: assumes A1: "f:X->Y" shows "f-``(D) ⊆ X"

proof-

have "∀x. x∈f-``(D) --> x ∈ domain(f)"

using vimage_iff domain_iff by auto

with A1 have "∀x. (x ∈ f-``(D)) --> (x∈X)" using func1_1_L1 by simp

then show ?thesis by auto

qed

text{*The inverse image of the range is the domain.*}

lemma func1_1_L4: assumes "f:X->Y" shows "f-``(Y) = X"

using assms func1_1_L3 func1_1_L2 vimage_iff by blast

text{*The arguments belongs to the domain and values to the range.*}

lemma func1_1_L5:

assumes A1: "⟨ x,y⟩ ∈ f" and A2: "f:X->Y"

shows "x∈X ∧ y∈Y"

proof

from A1 A2 show "x∈X" using apply_iff by simp

with A2 have "f`(x)∈ Y" using apply_type by simp

with A1 A2 show "y∈Y" using apply_iff by simp

qed

text{*Function is a subset of cartesian product.*}

lemma fun_subset_prod: assumes A1: "f:X->Y" shows "f ⊆ X×Y"

proof

fix p assume "p ∈ f"

with A1 have "∃x∈X. p = ⟨x, f`(x)⟩"

using Pi_memberD by simp

then obtain x where I: "p = ⟨x, f`(x)⟩"

by auto

with A1 `p ∈ f` have "x∈X ∧ f`(x) ∈ Y"

using func1_1_L5 by blast

with I show "p ∈ X×Y" by auto

qed

text{*The (argument, value) pair belongs to the graph of the function.*}

lemma func1_1_L5A:

assumes A1: "f:X->Y" "x∈X" "y = f`(x)"

shows "⟨x,y⟩ ∈ f" "y ∈ range(f)"

proof -

from A1 show "⟨x,y⟩ ∈ f" using apply_Pair by simp

then show "y ∈ range(f)" using rangeI by simp

qed

text{*The next theorem illustrates the meaning of the concept of

function in ZF.*}

theorem fun_is_set_of_pairs: assumes A1: "f:X->Y"

shows "f = {⟨x, f`(x)⟩. x ∈ X}"

proof

from A1 show "{⟨x, f`(x)⟩. x ∈ X} ⊆ f" using func1_1_L5A

by auto

next

{ fix p assume "p ∈ f"

with A1 have "p ∈ X×Y" using fun_subset_prod

by auto

with A1 `p ∈ f` have "p ∈ {⟨x, f`(x)⟩. x ∈ X}"

using apply_equality by auto

} thus "f ⊆ {⟨x, f`(x)⟩. x ∈ X}" by auto

qed

text{*The range of function thet maps $X$ into $Y$ is contained in $Y$.*}

lemma func1_1_L5B:

assumes A1: "f:X->Y" shows "range(f) ⊆ Y"

proof

fix y assume "y ∈ range(f)"

then obtain x where "⟨ x,y⟩ ∈ f"

using range_def converse_def domain_def by auto

with A1 show "y∈Y" using func1_1_L5 by blast

qed

text{*The image of any set is contained in the range.*}

lemma func1_1_L6: assumes A1: "f:X->Y"

shows "f``(B) ⊆ range(f)" and "f``(B) ⊆ Y"

proof -

show "f``(B) ⊆ range(f)" using image_iff rangeI by auto

with A1 show "f``(B) ⊆ Y" using func1_1_L5B by blast

qed

text{*The inverse image of any set is contained in the domain.*}

lemma func1_1_L6A: assumes A1: "f:X->Y" shows "f-``(A)⊆X"

proof

fix x

assume A2: "x∈f-``(A)" then obtain y where "⟨ x,y⟩ ∈ f"

using vimage_iff by auto

with A1 show "x∈X" using func1_1_L5 by fast

qed

text{*Image of a greater set is greater.*}

lemma func1_1_L8: assumes A1: "A⊆B" shows "f``(A)⊆ f``(B)"

using assms image_Un by auto

text{* A set is contained in the the inverse image of its image.

There is similar theorem in @{text "equalities.thy"}

(@{text "function_image_vimage"})

which shows that the image of inverse image of a set

is contained in the set.*}

lemma func1_1_L9: assumes A1: "f:X->Y" and A2: "A⊆X"

shows "A ⊆ f-``(f``(A))"

proof -

from A1 A2 have "∀x∈A. ⟨ x,f`(x)⟩ ∈ f" using apply_Pair by auto

then show ?thesis using image_iff by auto

qed

text{*The inverse image of the image of the domain is the domain.*}

lemma inv_im_dom: assumes A1: "f:X->Y" shows "f-``(f``(X)) = X"

proof

from A1 show "f-``(f``(X)) ⊆ X" using func1_1_L3 by simp

from A1 show "X ⊆ f-``(f``(X))" using func1_1_L9 by simp

qed

text{*A technical lemma needed to make the @{text "func1_1_L11"}

proof more clear.*}

lemma func1_1_L10:

assumes A1: "f ⊆ X×Y" and A2: "∃!y. (y∈Y ∧ ⟨x,y⟩ ∈ f)"

shows "∃!y. ⟨x,y⟩ ∈ f"

proof

from A2 show "∃y. ⟨x, y⟩ ∈ f" by auto

fix y n assume "⟨x,y⟩ ∈ f" and "⟨x,n⟩ ∈ f"

with A1 A2 show "y=n" by auto

qed

text{*If $f\subseteq X\times Y$ and for every $x\in X$ there is exactly

one $y\in Y$ such that $(x,y)\in f$ then $f$ maps $X$ to $Y$.*}

lemma func1_1_L11:

assumes "f ⊆ X×Y" and "∀x∈X. ∃!y. y∈Y ∧ ⟨x,y⟩ ∈ f"

shows "f: X->Y" using assms func1_1_L10 Pi_iff_old by simp

text{*A set defined by a lambda-type expression is a fuction. There is a

similar lemma in func.thy, but I had problems with lambda expressions syntax

so I could not apply it. This lemma is a workaround for this. Besides, lambda

expressions are not readable.

*}

lemma func1_1_L11A: assumes A1: "∀x∈X. b(x) ∈ Y"

shows "{⟨ x,y⟩ ∈ X×Y. b(x) = y} : X->Y"

proof -

let ?f = "{⟨ x,y⟩ ∈ X×Y. b(x) = y}"

have "?f ⊆ X×Y" by auto

moreover have "∀x∈X. ∃!y. y∈Y ∧ ⟨ x,y⟩ ∈ ?f"

proof

fix x assume A2: "x∈X"

show "∃!y. y∈Y ∧ ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"

proof

from A2 A1 show

"∃y. y∈Y ∧ ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"

by simp

next

fix y y1

assume "y∈Y ∧ ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"

and "y1∈Y ∧ ⟨x, y1⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"

then show "y = y1" by simp

qed

qed

ultimately show "{⟨ x,y⟩ ∈ X×Y. b(x) = y} : X->Y"

using func1_1_L11 by simp

qed

text{*The next lemma will replace @{text "func1_1_L11A"} one day.*}

lemma ZF_fun_from_total: assumes A1: "∀x∈X. b(x) ∈ Y"

shows "{⟨x,b(x)⟩. x∈X} : X->Y"

proof -

let ?f = "{⟨x,b(x)⟩. x∈X}"

{ fix x assume A2: "x∈X"

have "∃!y. y∈Y ∧ ⟨x, y⟩ ∈ ?f"

proof

from A1 A2 show "∃y. y∈Y ∧ ⟨x, y⟩ ∈ ?f"

by simp

next fix y y1 assume "y∈Y ∧ ⟨x, y⟩ ∈ ?f"

and "y1∈Y ∧ ⟨x, y1⟩ ∈ ?f"

then show "y = y1" by simp

qed

} then have "∀x∈X. ∃!y. y∈Y ∧ ⟨ x,y⟩ ∈ ?f"

by simp

moreover from A1 have "?f ⊆ X×Y" by auto

ultimately show ?thesis using func1_1_L11

by simp

qed

text{*The value of a function defined by a meta-function is this

meta-function.*}

lemma func1_1_L11B:

assumes A1: "f:X->Y" "x∈X"

and A2: "f = {⟨ x,y⟩ ∈ X×Y. b(x) = y}"

shows "f`(x) = b(x)"

proof -

from A1 have "⟨ x,f`(x)⟩ ∈ f" using apply_iff by simp

with A2 show ?thesis by simp

qed

text{*The next lemma will replace @{text "func1_1_L11B"} one day.*}

lemma ZF_fun_from_tot_val:

assumes A1: "f:X->Y" "x∈X"

and A2: "f = {⟨x,b(x)⟩. x∈X}"

shows "f`(x) = b(x)"

proof -

from A1 have "⟨ x,f`(x)⟩ ∈ f" using apply_iff by simp

with A2 show ?thesis by simp

qed

text{*Identical meaning as @{text " ZF_fun_from_tot_val"}, but

phrased a bit differently.*}

lemma ZF_fun_from_tot_val0:

assumes "f:X->Y" and "f = {⟨x,b(x)⟩. x∈X}"

shows "∀x∈X. f`(x) = b(x)"

using assms ZF_fun_from_tot_val by simp

text{*Another way of expressing that lambda expression is a function.*}

lemma lam_is_fun_range: assumes "f={⟨x,g(x)⟩. x∈X}"

shows "f:X->range(f)"

proof -

have "∀x∈X. g(x) ∈ range({⟨x,g(x)⟩. x∈X})" unfolding range_def

by auto

then have "{⟨x,g(x)⟩. x∈X} : X->range({⟨x,g(x)⟩. x∈X})"

by (rule ZF_fun_from_total)

with assms show ?thesis by auto

qed

text{*Yet another way of expressing value of a function.*}

lemma ZF_fun_from_tot_val1:

assumes "x∈X" shows "{⟨x,b(x)⟩. x∈X}`(x)=b(x)"

proof -

let ?f = "{⟨x,b(x)⟩. x∈X}"

have "?f:X->range(?f)" using lam_is_fun_range by simp

with assms show ?thesis using ZF_fun_from_tot_val0 by simp

qed

text{*We can extend a function by specifying its values on a set

disjoint with the domain.*}

lemma func1_1_L11C: assumes A1: "f:X->Y" and A2: "∀x∈A. b(x)∈B"

and A3: "X∩A = 0" and Dg: "g = f ∪ {⟨x,b(x)⟩. x∈A}"

shows

"g : X∪A -> Y∪B"

"∀x∈X. g`(x) = f`(x)"

"∀x∈A. g`(x) = b(x)"

proof -

let ?h = "{⟨x,b(x)⟩. x∈A}"

from A1 A2 A3 have

I: "f:X->Y" "?h : A->B" "X∩A = 0"

using ZF_fun_from_total by auto

then have "f∪?h : X∪A -> Y∪B"

by (rule fun_disjoint_Un)

with Dg show "g : X∪A -> Y∪B" by simp

{ fix x assume A4: "x∈A"

with A1 A3 have "(f∪?h)`(x) = ?h`(x)"

using func1_1_L1 fun_disjoint_apply2

by blast

moreover from I A4 have "?h`(x) = b(x)"

using ZF_fun_from_tot_val by simp

ultimately have "(f∪?h)`(x) = b(x)"

by simp

} with Dg show "∀x∈A. g`(x) = b(x)" by simp

{ fix x assume A5: "x∈X"

with A3 I have "x ∉ domain(?h)"

using func1_1_L1 by auto

then have "(f∪?h)`(x) = f`(x)"

using fun_disjoint_apply1 by simp

} with Dg show "∀x∈X. g`(x) = f`(x)" by simp

qed

text{*We can extend a function by specifying its value at a point that

does not belong to the domain.*}

lemma func1_1_L11D: assumes A1: "f:X->Y" and A2: "a∉X"

and Dg: "g = f ∪ {⟨a,b⟩}"

shows

"g : X∪{a} -> Y∪{b}"

"∀x∈X. g`(x) = f`(x)"

"g`(a) = b"

proof -

let ?h = "{⟨a,b⟩}"

from A1 A2 Dg have I:

"f:X->Y" "∀x∈{a}. b∈{b}" "X∩{a} = 0" "g = f ∪ {⟨x,b⟩. x∈{a}}"

by auto

then show "g : X∪{a} -> Y∪{b}"

by (rule func1_1_L11C)

from I show "∀x∈X. g`(x) = f`(x)"

by (rule func1_1_L11C)

from I have "∀x∈{a}. g`(x) = b"

by (rule func1_1_L11C)

then show "g`(a) = b" by auto

qed

text{*A technical lemma about extending a function both by defining

on a set disjoint with the domain and on a point that does not belong

to any of those sets.*}

lemma func1_1_L11E:

assumes A1: "f:X->Y" and

A2: "∀x∈A. b(x)∈B" and

A3: "X∩A = 0" and A4: "a∉ X∪A"

and Dg: "g = f ∪ {⟨x,b(x)⟩. x∈A} ∪ {⟨a,c⟩}"

shows

"g : X∪A∪{a} -> Y∪B∪{c}"

"∀x∈X. g`(x) = f`(x)"

"∀x∈A. g`(x) = b(x)"

"g`(a) = c"

proof -

let ?h = "f ∪ {⟨x,b(x)⟩. x∈A}"

from assms show "g : X∪A∪{a} -> Y∪B∪{c}"

using func1_1_L11C func1_1_L11D by simp

from A1 A2 A3 have I:

"f:X->Y" "∀x∈A. b(x)∈B" "X∩A = 0" "?h = f ∪ {⟨x,b(x)⟩. x∈A}"

by auto

from assms have

II: "?h : X∪A -> Y∪B" "a∉ X∪A" "g = ?h ∪ {⟨a,c⟩}"

using func1_1_L11C by auto

then have III: "∀x∈X∪A. g`(x) = ?h`(x)" by (rule func1_1_L11D)

moreover from I have "∀x∈X. ?h`(x) = f`(x)"

by (rule func1_1_L11C)

ultimately show "∀x∈X. g`(x) = f`(x)" by simp

from I have "∀x∈A. ?h`(x) = b(x)" by (rule func1_1_L11C)

with III show "∀x∈A. g`(x) = b(x)" by simp

from II show "g`(a) = c" by (rule func1_1_L11D)

qed

text{*A way of defining a function on a union of two possibly overlapping sets. We decompose the

union into two differences and the intersection and define a function separately on each part.*}

lemma fun_union_overlap: assumes "∀x∈A∩B. h(x) ∈ Y" "∀x∈A-B. f(x) ∈ Y" "∀x∈B-A. g(x) ∈ Y"

shows "{⟨x,if x∈A-B then f(x) else if x∈B-A then g(x) else h(x)⟩. x ∈ A∪B}: A∪B -> Y"

proof -

let ?F = "{⟨x,if x∈A-B then f(x) else if x∈B-A then g(x) else h(x)⟩. x ∈ A∩B}"

from assms have "∀x∈A∪B. (if x∈A-B then f(x) else if x∈B-A then g(x) else h(x)) ∈ Y"

by auto

then show ?thesis by (rule ZF_fun_from_total)

qed

text{*Inverse image of intersection is the intersection of inverse images.*}

lemma invim_inter_inter_invim: assumes "f:X->Y"

shows "f-``(A∩B) = f-``(A) ∩ f-``(B)"

using assms fun_is_fun function_vimage_Int by simp

text{*The inverse image of an intersection of a nonempty collection of sets

is the intersection of the

inverse images. This generalizes @{text "invim_inter_inter_invim"}

which is proven for the case of two sets.*}

lemma func1_1_L12:

assumes A1: "B ⊆ Pow(Y)" and A2: "B≠0" and A3: "f:X->Y"

shows "f-``(\<Inter>B) = (\<Inter>U∈B. f-``(U))"

proof

from A2 show "f-``(\<Inter>B) ⊆ (\<Inter>U∈B. f-``(U))" by blast

show "(\<Inter>U∈B. f-``(U)) ⊆ f-``(\<Inter>B)"

proof

fix x assume A4: "x ∈ (\<Inter>U∈B. f-``(U))"

from A3 have "∀U∈B. f-``(U) ⊆ X" using func1_1_L6A by simp

with A4 have "∀U∈B. x∈X" by auto

with A2 have "x∈X" by auto

with A3 have "∃!y. ⟨ x,y⟩ ∈ f" using Pi_iff_old by simp

with A2 A4 show "x ∈ f-``(\<Inter>B)" using vimage_iff by blast

qed

qed

text{*The inverse image of a set does not change when we intersect

the set with the image of the domain.*}

lemma inv_im_inter_im: assumes "f:X->Y"

shows "f-``(A ∩ f``(X)) = f-``(A)"

using assms invim_inter_inter_invim inv_im_dom func1_1_L6A

by blast

text{*If the inverse image of a set is not empty, then the set is not empty.

Proof by contradiction.*}

lemma func1_1_L13: assumes A1:"f-``(A) ≠ 0" shows "A≠0"

using assms by auto

text{*If the image of a set is not empty, then the set is not empty.

Proof by contradiction.*}

lemma func1_1_L13A: assumes A1: "f``(A)≠0" shows "A≠0"

using assms by auto

text{*What is the inverse image of a singleton?*}

lemma func1_1_L14: assumes "f∈X->Y"

shows "f-``({y}) = {x∈X. f`(x) = y}"

using assms func1_1_L6A vimage_singleton_iff apply_iff by auto

text{*A lemma that can be used instead @{text "fun_extension_iff"}

to show that two functions are equal *}

lemma func_eq: assumes "f: X->Y" "g: X->Z"

and "∀x∈X. f`(x) = g`(x)"

shows "f = g" using assms fun_extension_iff by simp

text{*Function defined on a singleton is a single pair.*}

lemma func_singleton_pair: assumes A1: "f : {a}->X"

shows "f = {⟨a, f`(a)⟩}"

proof -

let ?g = "{⟨a, f`(a)⟩}"

note A1

moreover have "?g : {a} -> {f`(a)}" using singleton_fun by simp

moreover have "∀x ∈ {a}. f`(x) = ?g`(x)" using singleton_apply

by simp

ultimately show "f = ?g" by (rule func_eq)

qed

text{*A single pair is a function on a singleton. This is

similar to @{text "singleton_fun"} from standard Isabelle/ZF.*}

lemma pair_func_singleton: assumes A1: "y ∈ Y"

shows "{⟨x,y⟩} : {x} -> Y"

proof -

have "{⟨x,y⟩} : {x} -> {y}" using singleton_fun by simp

moreover from A1 have "{y} ⊆ Y" by simp

ultimately show "{⟨x,y⟩} : {x} -> Y"

by (rule func1_1_L1B)

qed

text{*The value of a pair on the first element is the second one.*}

lemma pair_val: shows "{⟨x,y⟩}`(x) = y"

using singleton_fun apply_equality by simp

text{* A more familiar definition of inverse image.*}

lemma func1_1_L15: assumes A1: "f:X->Y"

shows "f-``(A) = {x∈X. f`(x) ∈ A}"

proof -

have "f-``(A) = (\<Union>y∈A . f-``{y})"

by (rule vimage_eq_UN)

with A1 show ?thesis using func1_1_L14 by auto

qed

text{*A more familiar definition of image.*}

lemma func_imagedef: assumes A1: "f:X->Y" and A2: "A⊆X"

shows "f``(A) = {f`(x). x ∈ A}"

proof

from A1 show "f``(A) ⊆ {f`(x). x ∈ A}"

using image_iff apply_iff by auto

show "{f`(x). x ∈ A} ⊆ f``(A)"

proof

fix y assume "y ∈ {f`(x). x ∈ A}"

then obtain x where "x∈A ∧ y = f`(x)"

by auto

with A1 A2 show "y ∈ f``(A)"

using apply_iff image_iff by auto

qed

qed

text{*The image of a set contained in domain under identity is the same set.*}

lemma image_id_same: assumes "A⊆X" shows "id(X)``(A) = A"

using assms id_type id_conv by auto

text{*The inverse image of a set contained in domain under identity is the same set.*}

lemma vimage_id_same: assumes "A⊆X" shows "id(X)-``(A) = A"

using assms id_type id_conv by auto

text{*What is the image of a singleton?*}

lemma singleton_image:

assumes "f∈X->Y" and "x∈X"

shows "f``{x} = {f`(x)}"

using assms func_imagedef by auto

text{*If an element of the domain of a function belongs to a set,

then its value belongs to the imgage of that set.*}

lemma func1_1_L15D: assumes "f:X->Y" "x∈A" "A⊆X"

shows "f`(x) ∈ f``(A)"

using assms func_imagedef by auto

text{*Range is the image of the domain. Isabelle/ZF defines

@{text "range(f)"} as @{text "domain(converse(f))"},

and that's why we have something to prove here.*}

lemma range_image_domain:

assumes A1: "f:X->Y" shows "f``(X) = range(f)"

proof

show "f``(X) ⊆ range(f)" using image_def by auto

{ fix y assume "y ∈ range(f)"

then obtain x where "⟨y,x⟩ ∈ converse(f)" by auto

with A1 have "x∈X" using func1_1_L5 by blast

with A1 have "f`(x) ∈ f``(X)" using func_imagedef

by auto

with A1 `⟨y,x⟩ ∈ converse(f)` have "y ∈ f``(X)"

using apply_equality by auto

} then show "range(f) ⊆ f``(X)" by auto

qed

text{*The difference of images is contained in the image of difference.*}

lemma diff_image_diff: assumes A1: "f: X->Y" and A2: "A⊆X"

shows "f``(X) - f``(A) ⊆ f``(X-A)"

proof

fix y assume "y ∈ f``(X) - f``(A)"

hence "y ∈ f``(X)" and I: "y ∉ f``(A)" by auto

with A1 obtain x where "x∈X" and II: "y = f`(x)"

using func_imagedef by auto

with A1 A2 I have "x∉A"

using func1_1_L15D by auto

with `x∈X` have "x ∈ X-A" "X-A ⊆ X" by auto

with A1 II show "y ∈ f``(X-A)"

using func1_1_L15D by simp

qed

text{*The image of an intersection is contained in the

intersection of the images.*}

lemma image_of_Inter: assumes A1: "f:X->Y" and

A2: "I≠0" and A3: "∀i∈I. P(i) ⊆ X"

shows "f``(\<Inter>i∈I. P(i)) ⊆ ( \<Inter>i∈I. f``(P(i)) )"

proof

fix y assume A4: "y ∈ f``(\<Inter>i∈I. P(i))"

from A1 A2 A3 have "f``(\<Inter>i∈I. P(i)) = {f`(x). x ∈ ( \<Inter>i∈I. P(i) )}"

using ZF1_1_L7 func_imagedef by simp

with A4 obtain x where "x ∈ ( \<Inter>i∈I. P(i) )" and "y = f`(x)"

by auto

with A1 A2 A3 show "y ∈ ( \<Inter>i∈I. f``(P(i)) )" using func_imagedef

by auto

qed

text{*The image of union is the union of images.*}

lemma image_of_Union: assumes A1: "f:X->Y" and A2: "∀A∈M. A⊆X"

shows "f``(\<Union>M) = \<Union>{f``(A). A∈M}"

proof

from A2 have "\<Union>M ⊆ X" by auto

{ fix y assume "y ∈ f``(\<Union>M)"

with A1 `\<Union>M ⊆ X` obtain x where "x∈\<Union>M" and I: "y = f`(x)"

using func_imagedef by auto

then obtain A where "A∈M" and "x∈A" by auto

with assms I have "y ∈ \<Union>{f``(A). A∈M}" using func_imagedef by auto

} thus "f``(\<Union>M) ⊆ \<Union>{f``(A). A∈M}" by auto

{ fix y assume "y ∈ \<Union>{f``(A). A∈M}"

then obtain A where "A∈M" and "y ∈ f``(A)" by auto

with assms `\<Union>M ⊆ X` have "y ∈ f``(\<Union>M)" using func_imagedef by auto

} thus "\<Union>{f``(A). A∈M} ⊆ f``(\<Union>M)" by auto

qed

text{*The image of a nonempty subset of domain is nonempty.*}

lemma func1_1_L15A:

assumes A1: "f: X->Y" and A2: "A⊆X" and A3: "A≠0"

shows "f``(A) ≠ 0"

proof -

from A3 obtain x where "x∈A" by auto

with A1 A2 have "f`(x) ∈ f``(A)"

using func_imagedef by auto

then show "f``(A) ≠ 0" by auto

qed

text{*The next lemma allows to prove statements about the values in the

domain of a function given a statement about values in the range.*}

lemma func1_1_L15B:

assumes "f:X->Y" and "A⊆X" and "∀y∈f``(A). P(y)"

shows "∀x∈A. P(f`(x))"

using assms func_imagedef by simp

text{*An image of an image is the image of a composition.*}

lemma func1_1_L15C: assumes A1: "f:X->Y" and A2: "g:Y->Z"

and A3: "A⊆X"

shows

"g``(f``(A)) = {g`(f`(x)). x∈A}"

"g``(f``(A)) = (g O f)``(A)"

proof -

from A1 A3 have "{f`(x). x∈A} ⊆ Y"

using apply_funtype by auto

with A2 have "g``{f`(x). x∈A} = {g`(f`(x)). x∈A}"

using func_imagedef by auto

with A1 A3 show I: "g``(f``(A)) = {g`(f`(x)). x∈A}"

using func_imagedef by simp

from A1 A3 have "∀x∈A. (g O f)`(x) = g`(f`(x))"

using comp_fun_apply by auto

with I have "g``(f``(A)) = {(g O f)`(x). x∈A}"

by simp

moreover from A1 A2 A3 have "(g O f)``(A) = {(g O f)`(x). x∈A}"

using comp_fun func_imagedef by blast

ultimately show "g``(f``(A)) = (g O f)``(A)"

by simp

qed

text{*What is the image of a set defined by a meta-fuction?*}

lemma func1_1_L17:

assumes A1: "f ∈ X->Y" and A2: "∀x∈A. b(x) ∈ X"

shows "f``({b(x). x∈A}) = {f`(b(x)). x∈A}"

proof -

from A2 have "{b(x). x∈A} ⊆ X" by auto

with A1 show ?thesis using func_imagedef by auto

qed

text{*What are the values of composition of three functions?*}

lemma func1_1_L18: assumes A1: "f:A->B" "g:B->C" "h:C->D"

and A2: "x∈A"

shows

"(h O g O f)`(x) ∈ D"

"(h O g O f)`(x) = h`(g`(f`(x)))"

proof -

from A1 have "(h O g O f) : A->D"

using comp_fun by blast

with A2 show "(h O g O f)`(x) ∈ D" using apply_funtype

by simp

from A1 A2 have "(h O g O f)`(x) = h`( (g O f)`(x))"

using comp_fun comp_fun_apply by blast

with A1 A2 show "(h O g O f)`(x) = h`(g`(f`(x)))"

using comp_fun_apply by simp

qed

text{*A composition of functions is a function. This is a slight

generalization of standard Isabelle's @{text "comp_fun"}

*}

lemma comp_fun_subset:

assumes A1: "g:A->B" and A2: "f:C->D" and A3: "B ⊆ C"

shows "f O g : A -> D"

proof -

from A1 A3 have "g:A->C" by (rule func1_1_L1B)

with A2 show "f O g : A -> D" using comp_fun by simp

qed

text{* This lemma supersedes the lemma @{text "comp_eq_id_iff"}

in Isabelle/ZF. Contributed by Victor Porton.*}

lemma comp_eq_id_iff1: assumes A1: "g: B->A" and A2: "f: A->C"

shows "(∀y∈B. f`(g`(y)) = y) <-> f O g = id(B)"

proof -

from assms have "f O g: B->C" and "id(B): B->B"

using comp_fun id_type by auto

then have "(∀y∈B. (f O g)`y = id(B)`(y)) <-> f O g = id(B)"

by (rule fun_extension_iff)

moreover from A1 have

"∀y∈B. (f O g)`y = f`(g`y)" and "∀y∈B. id(B)`(y) = y"

by auto

ultimately show "(∀y∈B. f`(g`y) = y) <-> f O g = id(B)" by simp

qed

text{*A lemma about a value of a function that is a union of

some collection of functions.*}

lemma fun_Union_apply: assumes A1: "\<Union>F : X->Y" and

A2: "f∈F" and A3: "f:A->B" and A4: "x∈A"

shows "(\<Union>F)`(x) = f`(x)"

proof -

from A3 A4 have "⟨x, f`(x)⟩ ∈ f" using apply_Pair

by simp

with A2 have "⟨x, f`(x)⟩ ∈ \<Union>F" by auto

with A1 show "(\<Union>F)`(x) = f`(x)" using apply_equality

by simp

qed

section{*Functions restricted to a set*}

text{*Standard Isabelle/ZF defines the notion @{text "restrict(f,A)"}

of to mean a function (or relation) $f$ restricted to a set.

This means that if $f$ is a function defined on $X$ and $A$

is a subset of $X$ then @{text "restrict(f,A)"} is a function

whith the same values as $f$, but whose domain is $A$.*}

text{*What is the inverse image of a set under a restricted fuction?*}

lemma func1_2_L1: assumes A1: "f:X->Y" and A2: "B⊆X"

shows "restrict(f,B)-``(A) = f-``(A) ∩ B"

proof -

let ?g = "restrict(f,B)"

from A1 A2 have "?g:B->Y"

using restrict_type2 by simp

with A2 A1 show "?g-``(A) = f-``(A) ∩ B"

using func1_1_L15 restrict_if by auto

qed

text{*A criterion for when one function is a restriction of another.

The lemma below provides a result useful in the actual proof of the

criterion and applications.*}

lemma func1_2_L2:

assumes A1: "f:X->Y" and A2: "g ∈ A->Z"

and A3: "A⊆X" and A4: "f ∩ A×Z = g"

shows "∀x∈A. g`(x) = f`(x)"

proof

fix x assume "x∈A"

with A2 have "⟨ x,g`(x)⟩ ∈ g" using apply_Pair by simp

with A4 A1 show "g`(x) = f`(x)" using apply_iff by auto

qed

text{*Here is the actual criterion.*}

lemma func1_2_L3:

assumes A1: "f:X->Y" and A2: "g:A->Z"

and A3: "A⊆X" and A4: "f ∩ A×Z = g"

shows "g = restrict(f,A)"

proof

from A4 show "g ⊆ restrict(f, A)" using restrict_iff by auto

show "restrict(f, A) ⊆ g"

proof

fix z assume A5:"z ∈ restrict(f,A)"

then obtain x y where D1:"z∈f ∧ x∈A ∧ z = ⟨x,y⟩"

using restrict_iff by auto

with A1 have "y = f`(x)" using apply_iff by auto

with A1 A2 A3 A4 D1 have "y = g`(x)" using func1_2_L2 by simp

with A2 D1 show "z∈g" using apply_Pair by simp

qed

qed

text{*Which function space a restricted function belongs to?*}

lemma func1_2_L4:

assumes A1: "f:X->Y" and A2: "A⊆X" and A3: "∀x∈A. f`(x) ∈ Z"

shows "restrict(f,A) : A->Z"

proof -

let ?g = "restrict(f,A)"

from A1 A2 have "?g : A->Y"

using restrict_type2 by simp

moreover {

fix x assume "x∈A"

with A1 A3 have "?g`(x) ∈ Z" using restrict by simp}

ultimately show ?thesis by (rule Pi_type)

qed

text{*A simpler case of @{text "func1_2_L4"}, where

the range of the original and restricted function are the same.

*}

corollary restrict_fun: assumes A1: "f:X->Y" and A2: "A⊆X"

shows "restrict(f,A) : A -> Y"

proof -

from assms have "∀x∈A. f`(x) ∈ Y" using apply_funtype

by auto

with assms show ?thesis using func1_2_L4 by simp

qed

text{*A composition of two functions is the same as

composition with a restriction.*}

lemma comp_restrict:

assumes A1: "f : A->B" and A2: "g : X -> C" and A3: "B⊆X"

shows "g O f = restrict(g,B) O f"

proof -

from assms have "g O f : A -> C" using comp_fun_subset

by simp

moreover from assms have "restrict(g,B) O f : A -> C"

using restrict_fun comp_fun by simp

moreover from A1 have

"∀x∈A. (g O f)`(x) = (restrict(g,B) O f)`(x)"

using comp_fun_apply apply_funtype restrict

by simp

ultimately show "g O f = restrict(g,B) O f"

by (rule func_eq)

qed

text{*A way to look at restriction. Contributed by Victor Porton.*}

lemma right_comp_id_any: shows "r O id(C) = restrict(r,C)"

unfolding restrict_def by auto

section{*Constant functions*}

text{*Constant functions are trivial, but still we need to

prove some properties to shorten proofs.*}

text{*We define constant($=c$) functions on a set $X$

in a natural way as ConstantFunction$(X,c)$. *}

definition

"ConstantFunction(X,c) ≡ X×{c}"

text{*Constant function belongs to the function space.*}

lemma func1_3_L1:

assumes A1: "c∈Y" shows "ConstantFunction(X,c) : X->Y"

proof -

from A1 have "X×{c} = {⟨ x,y⟩ ∈ X×Y. c = y}"

by auto

with A1 show ?thesis using func1_1_L11A ConstantFunction_def

by simp

qed

text{*Constant function is equal to the constant on its domain.*}

lemma func1_3_L2: assumes A1: "x∈X"

shows "ConstantFunction(X,c)`(x) = c"

proof -

have "ConstantFunction(X,c) ∈ X->{c}"

using func1_3_L1 by simp

moreover from A1 have "⟨ x,c⟩ ∈ ConstantFunction(X,c)"

using ConstantFunction_def by simp

ultimately show ?thesis using apply_iff by simp

qed

section{*Injections, surjections, bijections etc.*}

text{*In this section we prove the properties of the spaces

of injections, surjections and bijections that we can't find in the

standard Isabelle's @{text "Perm.thy"}.*}

text{*For injections the image a difference of two sets is

the difference of images*}

lemma inj_image_dif:

assumes A1: "f ∈ inj(A,B)" and A2: "C ⊆ A"

shows "f``(A-C) = f``(A) - f``(C)"

proof

show "f``(A - C) ⊆ f``(A) - f``(C)"

proof

fix y assume A3: "y ∈ f``(A - C)"

from A1 have "f:A->B" using inj_def by simp

moreover have "A-C ⊆ A" by auto

ultimately have "f``(A-C) = {f`(x). x ∈ A-C}"

using func_imagedef by simp

with A3 obtain x where I: "f`(x) = y" and "x ∈ A-C"

by auto

hence "x∈A" by auto

with `f:A->B` I have "y ∈ f``(A)"

using func_imagedef by auto

moreover have "y ∉ f``(C)"

proof -

{ assume "y ∈ f``(C)"

with A2 `f:A->B` obtain x⇩_{0}

where II: "f`(x⇩_{0}) = y" and "x⇩_{0}∈ C"

using func_imagedef by auto

with A1 A2 I `x∈A` have

"f ∈ inj(A,B)" "f`(x) = f`(x⇩_{0})" "x∈A" "x⇩_{0}∈ A"

by auto

then have "x = x⇩_{0}" by (rule inj_apply_equality)

with `x ∈ A-C` `x⇩_{0}∈ C` have False by simp

} thus ?thesis by auto

qed

ultimately show "y ∈ f``(A) - f``(C)" by simp

qed

from A1 A2 show "f``(A) - f``(C) ⊆ f``(A-C)"

using inj_def diff_image_diff by auto

qed

text{*For injections the image of intersection is the intersection of images.*}

lemma inj_image_inter: assumes A1: "f ∈ inj(X,Y)" and A2: "A⊆X" "B⊆X"

shows "f``(A∩B) = f``(A) ∩ f``(B)"

proof

show "f``(A∩B) ⊆ f``(A) ∩ f``(B)" using image_Int_subset by simp

{ from A1 have "f:X->Y" using inj_def by simp

fix y assume "y ∈ f``(A) ∩ f``(B)"

then have "y ∈ f``(A)" and "y ∈ f``(B)" by auto

with A2 `f:X->Y` obtain x⇩_{A}x⇩_{B}where

"x⇩_{A}∈ A" "x⇩_{B}∈ B" and I: "y = f`(x⇩_{A})" "y = f`(x⇩_{B})"

using func_imagedef by auto

with A2 have "x⇩_{A}∈ X" "x⇩_{B}∈ X" and " f`(x⇩_{A}) = f`(x⇩_{B})" by auto

with A1 have "x⇩_{A}= x⇩_{B}" using inj_def by auto

with `x⇩_{A}∈ A` `x⇩_{B}∈ B` have "f`(x⇩_{A}) ∈ {f`(x). x ∈ A∩B}" by auto

moreover from A2 `f:X->Y` have "f``(A∩B) = {f`(x). x ∈ A∩B}"

using func_imagedef by blast

ultimately have "f`(x⇩_{A}) ∈ f``(A∩B)" by simp

with I have "y ∈ f``(A∩B)" by simp

} thus "f``(A) ∩ f``(B) ⊆ f``(A ∩ B)" by auto

qed

text{*For surjection from $A$ to $B$ the image of

the domain is $B$.*}

lemma surj_range_image_domain: assumes A1: "f ∈ surj(A,B)"

shows "f``(A) = B"

proof -

from A1 have "f``(A) = range(f)"

using surj_def range_image_domain by auto

with A1 show "f``(A) = B" using surj_range

by simp

qed

text{*For injections the inverse image of an image is the same set.*}

lemma inj_vimage_image: assumes "f ∈ inj(X,Y)" and "A⊆X"

shows "f-``(f``(A)) = A"

proof -

have "f-``(f``(A)) = (converse(f) O f)``(A)"

using vimage_converse image_comp by simp

with assms show ?thesis using left_comp_inverse image_id_same

by simp

qed

text{*For surjections the image of an inverse image is the same set.*}

lemma surj_image_vimage: assumes A1: "f ∈ surj(X,Y)" and A2: "A⊆Y"

shows "f``(f-``(A)) = A"

proof -

have "f``(f-``(A)) = (f O converse(f))``(A)"

using vimage_converse image_comp by simp

with assms show ?thesis using right_comp_inverse image_id_same

by simp

qed

text{*A lemma about how a surjection maps collections of subsets in domain and rangge.*}

lemma surj_subsets: assumes A1: "f ∈ surj(X,Y)" and A2: "B ⊆ Pow(Y)"

shows "{ f``(U). U ∈ {f-``(V). V∈B} } = B"

proof

{ fix W assume "W ∈ { f``(U). U ∈ {f-``(V). V∈B} }"

then obtain U where I: "U ∈ {f-``(V). V∈B}" and II: "W = f``(U)" by auto

then obtain V where "V∈B" and "U = f-``(V)" by auto

with II have "W = f``(f-``(V))" by simp

moreover from assms `V∈B` have "f ∈ surj(X,Y)" and "V⊆Y" by auto

ultimately have "W=V" using surj_image_vimage by simp

with `V∈B` have "W ∈ B" by simp

} thus "{ f``(U). U ∈ {f-``(V). V∈B} } ⊆ B" by auto

{ fix W assume "W∈B"

let ?U = "f-``(W)"

from `W∈B` have "?U ∈ {f-``(V). V∈B}" by auto

moreover from A1 A2 `W∈B` have "W = f``(?U)" using surj_image_vimage by auto

ultimately have "W ∈ { f``(U). U ∈ {f-``(V). V∈B} }" by auto

} thus "B ⊆ { f``(U). U ∈ {f-``(V). V∈B} }" by auto

qed

text{*Restriction of an bijection to a set without a point

is a a bijection.*}

lemma bij_restrict_rem:

assumes A1: "f ∈ bij(A,B)" and A2: "a∈A"

shows "restrict(f, A-{a}) ∈ bij(A-{a}, B-{f`(a)})"

proof -

let ?C = "A-{a}"

from A1 have "f ∈ inj(A,B)" "?C ⊆ A"

using bij_def by auto

then have "restrict(f,?C) ∈ bij(?C, f``(?C))"

using restrict_bij by simp

moreover have "f``(?C) = B-{f`(a)}"

proof -

from A2 `f ∈ inj(A,B)` have "f``(?C) = f``(A) - f``{a}"

using inj_image_dif by simp

moreover from A1 have "f``(A) = B"

using bij_def surj_range_image_domain by auto

moreover from A1 A2 have "f``{a} = {f`(a)}"

using bij_is_fun singleton_image by blast

ultimately show "f``(?C) = B-{f`(a)}" by simp

qed

ultimately show ?thesis by simp

qed

text{*The domain of a bijection between $X$ and $Y$ is $X$.*}

lemma domain_of_bij:

assumes A1: "f ∈ bij(X,Y)" shows "domain(f) = X"

proof -

from A1 have "f:X->Y" using bij_is_fun by simp

then show "domain(f) = X" using func1_1_L1 by simp

qed

text{*The value of the inverse of an injection on a point of the image

of a set belongs to that set.*}

lemma inj_inv_back_in_set:

assumes A1: "f ∈ inj(A,B)" and A2: "C⊆A" and A3: "y ∈ f``(C)"

shows

"converse(f)`(y) ∈ C"

"f`(converse(f)`(y)) = y"

proof -

from A1 have I: "f:A->B" using inj_is_fun by simp

with A2 A3 obtain x where II: "x∈C" "y = f`(x)"

using func_imagedef by auto

with A1 A2 show "converse(f)`(y) ∈ C" using left_inverse

by auto

from A1 A2 I II show "f`(converse(f)`(y)) = y"

using func1_1_L5A right_inverse by auto

qed

text{*For injections if a value at a point

belongs to the image of a set, then the point

belongs to the set. *}

lemma inj_point_of_image:

assumes A1: "f ∈ inj(A,B)" and A2: "C⊆A" and

A3: "x∈A" and A4: "f`(x) ∈ f``(C)"

shows "x ∈ C"

proof -

from A1 A2 A4 have "converse(f)`(f`(x)) ∈ C"

using inj_inv_back_in_set by simp

moreover from A1 A3 have "converse(f)`(f`(x)) = x"

using left_inverse_eq by simp

ultimately show "x ∈ C" by simp

qed

text{*For injections the image of intersection is

the intersection of images.*}

lemma inj_image_of_Inter: assumes A1: "f ∈ inj(A,B)" and

A2: "I≠0" and A3: "∀i∈I. P(i) ⊆ A"

shows "f``(\<Inter>i∈I. P(i)) = ( \<Inter>i∈I. f``(P(i)) )"

proof

from A1 A2 A3 show "f``(\<Inter>i∈I. P(i)) ⊆ ( \<Inter>i∈I. f``(P(i)) )"

using inj_is_fun image_of_Inter by auto

from A1 A2 A3 have "f:A->B" and "( \<Inter>i∈I. P(i) ) ⊆ A"

using inj_is_fun ZF1_1_L7 by auto

then have I: "f``(\<Inter>i∈I. P(i)) = { f`(x). x ∈ ( \<Inter>i∈I. P(i) ) }"

using func_imagedef by simp

{ fix y assume A4: "y ∈ ( \<Inter>i∈I. f``(P(i)) )"

let ?x = "converse(f)`(y)"

from A2 obtain i⇩_{0}where "i⇩_{0}∈ I" by auto

with A1 A4 have II: "y ∈ range(f)" using inj_is_fun func1_1_L6

by auto

with A1 have III: "f`(?x) = y" using right_inverse by simp

from A1 II have IV: "?x ∈ A" using inj_converse_fun apply_funtype

by blast

{ fix i assume "i∈I"

with A3 A4 III have "P(i) ⊆ A" and "f`(?x) ∈ f``(P(i))"

by auto

with A1 IV have "?x ∈ P(i)" using inj_point_of_image

by blast

} then have "∀i∈I. ?x ∈ P(i)" by simp

with A2 I have "f`(?x) ∈ f``( \<Inter>i∈I. P(i) )"

by auto

with III have "y ∈ f``( \<Inter>i∈I. P(i) )" by simp

} then show "( \<Inter>i∈I. f``(P(i)) ) ⊆ f``( \<Inter>i∈I. P(i) )"

by auto

qed

text{*An injection is injective onto its range. Suggested by Victor Porton.*}

lemma inj_inj_range: assumes "f ∈ inj(A,B)"

shows "f ∈ inj(A,range(f))"

using assms inj_def range_of_fun by auto

text{*An injection is a bijection on its range. Suggested by Victor Porton. *}

lemma inj_bij_range: assumes "f ∈ inj(A,B)"

shows "f ∈ bij(A,range(f))"

proof -

from assms have "f ∈ surj(A,range(f))" using inj_def fun_is_surj

by auto

with assms show ?thesis using inj_inj_range bij_def by simp

qed

text{*A lemma about extending a surjection by one point.*}

lemma surj_extend_point:

assumes A1: "f ∈ surj(X,Y)" and A2: "a∉X" and

A3: "g = f ∪ {⟨a,b⟩}"

shows "g ∈ surj(X∪{a},Y∪{b})"

proof -

from A1 A2 A3 have "g : X∪{a} -> Y∪{b}"

using surj_def func1_1_L11D by simp

moreover have "∀y ∈ Y∪{b}. ∃x ∈ X∪{a}. y = g`(x)"

proof

fix y assume "y ∈ Y ∪ {b}"

then have "y ∈ Y ∨ y = b" by auto

moreover

{ assume "y ∈ Y"

with A1 obtain x where "x∈X" and "y = f`(x)"

using surj_def by auto

with A1 A2 A3 have "x ∈ X∪{a}" and "y = g`(x)"

using surj_def func1_1_L11D by auto

then have "∃x ∈ X∪{a}. y = g`(x)" by auto }

moreover

{ assume "y = b"

with A1 A2 A3 have "y = g`(a)"

using surj_def func1_1_L11D by auto

then have "∃x ∈ X∪{a}. y = g`(x)" by auto }

ultimately show "∃x ∈ X∪{a}. y = g`(x)"

by auto

qed

ultimately show "g ∈ surj(X∪{a},Y∪{b})"

using surj_def by auto

qed

text{*A lemma about extending an injection by one point.

Essentially the same as standard Isabelle's @{text "inj_extend"}.

*}

lemma inj_extend_point: assumes "f ∈ inj(X,Y)" "a∉X" "b∉Y"

shows "(f ∪ {⟨a,b⟩}) ∈ inj(X∪{a},Y∪{b})"

proof -

from assms have "cons(⟨a,b⟩,f) ∈ inj(cons(a, X), cons(b, Y))"

using assms inj_extend by simp

moreover have "cons(⟨a,b⟩,f) = f ∪ {⟨a,b⟩}" and

"cons(a, X) = X∪{a}" and "cons(b, Y) = Y∪{b}"

by auto

ultimately show ?thesis by simp

qed

text{*A lemma about extending a bijection by one point.*}

lemma bij_extend_point: assumes "f ∈ bij(X,Y)" "a∉X" "b∉Y"

shows "(f ∪ {⟨a,b⟩}) ∈ bij(X∪{a},Y∪{b})"

using assms surj_extend_point inj_extend_point bij_def

by simp

text{*A quite general form of the $a^{-1}b = 1$

implies $a=b$ law.*}

lemma comp_inv_id_eq:

assumes A1: "converse(b) O a = id(A)" and

A2: "a ⊆ A×B" "b ∈ surj(A,B)"

shows "a = b"

proof -

from A1 have "(b O converse(b)) O a = b O id(A)"

using comp_assoc by simp

with A2 have "id(B) O a = b O id(A)"

using right_comp_inverse by simp

moreover

from A2 have "a ⊆ A×B" and "b ⊆ A×B"

using surj_def fun_subset_prod

by auto

then have "id(B) O a = a" and "b O id(A) = b"

using left_comp_id right_comp_id by auto

ultimately show "a = b" by simp

qed

text{*A special case of @{text "comp_inv_id_eq"} -

the $a^{-1}b = 1$ implies $a=b$ law for bijections.*}

lemma comp_inv_id_eq_bij:

assumes A1: "a ∈ bij(A,B)" "b ∈ bij(A,B)" and

A2: "converse(b) O a = id(A)"

shows "a = b"

proof -

from A1 have "a ⊆ A×B" and "b ∈ surj(A,B)"

using bij_def surj_def fun_subset_prod

by auto

with A2 show "a = b" by (rule comp_inv_id_eq)

qed

text{*Converse of a converse of a bijection the same bijection.

This is a special case of @{text "converse_converse"} from standard Isabelle's

@{text "equalities"} theory where it is proved for relations.*}

lemma bij_converse_converse: assumes "a ∈ bij(A,B)"

shows "converse(converse(a)) = a"

proof -

from assms have "a ⊆ A×B" using bij_def surj_def fun_subset_prod by simp

then show ?thesis using converse_converse by simp

qed

text{*If a composition of bijections is identity, then one is the inverse

of the other.*}

lemma comp_id_conv: assumes A1: "a ∈ bij(A,B)" "b ∈ bij(B,A)" and

A2: "b O a = id(A)"

shows "a = converse(b)" and "b = converse(a)"

proof -

from A1 have "a ∈ bij(A,B)" and "converse(b) ∈ bij(A,B)" using bij_converse_bij

by auto

moreover from assms have "converse(converse(b)) O a = id(A)"

using bij_converse_converse by simp

ultimately show "a = converse(b)" by (rule comp_inv_id_eq_bij)

with assms show "b = converse(a)" using bij_converse_converse by simp

qed

text{*A version of @{text "comp_id_conv"} with weaker assumptions.*}

lemma comp_conv_id: assumes A1: "a ∈ bij(A,B)" and A2: "b:B->A" and

A3: "∀x∈A. b`(a`(x)) = x"

shows "b ∈ bij(B,A)" and "a = converse(b)" and "b = converse(a)"

proof -

have "b ∈ surj(B,A)"

proof -

have "∀x∈A. ∃y∈B. b`(y) = x"

proof -

{ fix x assume "x∈A"

let ?y = "a`(x)"

from A1 A3 `x∈A` have "?y∈B" and "b`(?y) = x"

using bij_def inj_def apply_funtype by auto

hence "∃y∈B. b`(y) = x" by auto

} thus ?thesis by simp

qed

with A2 show "b ∈ surj(B,A)" using surj_def by simp

qed

moreover have "b ∈ inj(B,A)"

proof -

have "∀w∈B.∀y∈B. b`(w) = b`(y) --> w=y"

proof -

{ fix w y assume "w∈B" "y∈B" and I: "b`(w) = b`(y)"

from A1 have "a ∈ surj(A,B)" unfolding bij_def by simp

with `w∈B` obtain x⇩_{w}where "x⇩_{w}∈ A" and II: "a`(x⇩_{w}) = w"

using surj_def by auto

with I have "b`(a`(x⇩_{w})) = b`(y)" by simp

moreover from `a ∈ surj(A,B)` `y∈B` obtain x⇩_{y}where

"x⇩_{y}∈ A" and III: "a`(x⇩_{y}) = y"

using surj_def by auto

moreover from A3 `x⇩_{w}∈ A` `x⇩_{y}∈ A` have "b`(a`(x⇩_{w})) = x⇩_{w}" and "b`(a`(x⇩_{y})) = x⇩_{y}"

by auto

ultimately have "x⇩_{w}= x⇩_{y}" by simp

with II III have "w=y" by simp

} thus ?thesis by auto

qed

with A2 show "b ∈ inj(B,A)" using inj_def by auto

qed

ultimately show "b ∈ bij(B,A)" using bij_def by simp

from assms have "b O a = id(A)" using bij_def inj_def comp_eq_id_iff1 by auto

with A1 `b ∈ bij(B,A)` show "a = converse(b)" and "b = converse(a)"

using comp_id_conv by auto

qed

text{*For a surjection the union if images of singletons

is the whole range.*}

lemma surj_singleton_image: assumes A1: "f ∈ surj(X,Y)"

shows "(\<Union>x∈X. {f`(x)}) = Y"

proof

from A1 show "(\<Union>x∈X. {f`(x)}) ⊆ Y"

using surj_def apply_funtype by auto

next

{ fix y assume "y ∈ Y"

with A1 have "y ∈ (\<Union>x∈X. {f`(x)})"

using surj_def by auto

} then show "Y ⊆ (\<Union>x∈X. {f`(x)})" by auto

qed

section{*Functions of two variables*}

text{* In this section we consider functions whose domain is a cartesian product

of two sets. Such functions are called functions of two variables (although really

in ZF all functions admit only one argument).

For every function of two variables we can define families of

functions of one variable by fixing the other variable. This section

establishes basic definitions and results for this concept.*}

text{*We can create functions of two variables by combining functions of one variable.*}

lemma cart_prod_fun: assumes "f⇩_{1}:X⇩_{1}->Y⇩_{1}" "f⇩_{2}:X⇩_{2}->Y⇩_{2}" and

"g = {⟨p,⟨f⇩_{1}`(fst(p)),f⇩_{2}`(snd(p))⟩⟩. p ∈ X⇩_{1}×X⇩_{2}}"

shows "g: X⇩_{1}×X⇩_{2}-> Y⇩_{1}×Y⇩_{2}" using assms apply_funtype ZF_fun_from_total by simp

text{*A reformulation of @{text "cart_prod_fun"} above in a sligtly different notation.*}

lemma prod_fun:

assumes "f:X⇩_{1}->X⇩_{2}" "g:X⇩_{3}->X⇩_{4}"

shows "{⟨⟨x,y⟩,⟨f`x,g`y⟩⟩. ⟨x,y⟩∈X⇩_{1}×X⇩_{3}}:X⇩_{1}×X⇩_{3}->X⇩_{2}×X⇩_{4}"

proof -

have "{⟨⟨x,y⟩,⟨f`x,g`y⟩⟩. ⟨x,y⟩∈X⇩_{1}×X⇩_{3}} = {⟨p,⟨f`(fst(p)),g`(snd(p))⟩⟩. p ∈ X⇩_{1}×X⇩_{3}}"

by auto

with assms show ?thesis using cart_prod_fun by simp

qed

text{*Product of two surjections is a surjection.*}

theorem prod_functions_surj:

assumes "f∈surj(A,B)" "g∈surj(C,D)"

shows "{⟨⟨a1,a2⟩,⟨f`a1,g`a2⟩⟩.⟨a1,a2⟩∈A×C} ∈ surj(A×C,B×D)"

proof -

let ?h = "{⟨⟨x, y⟩, f`(x), g`(y)⟩ . ⟨x,y⟩ ∈ A × C}"

from assms have fun: "f:A->B""g:C->D" unfolding surj_def by auto

then have pfun: "?h : A × C -> B × D" using prod_fun by auto

{

fix b assume "b∈B×D"

then obtain b1 b2 where "b=⟨b1,b2⟩" "b1∈B" "b2∈D" by auto

with assms obtain a1 a2 where "f`(a1)=b1" "g`(a2)=b2" "a1∈A" "a2∈C"

unfolding surj_def by blast

hence "⟨⟨a1,a2⟩,⟨b1,b2⟩⟩ ∈ ?h" by auto

with pfun have "?h`⟨a1,a2⟩=⟨b1,b2⟩" using apply_equality by auto

with `b=⟨b1,b2⟩` `a1∈A` `a2∈C` have "∃a∈A×C. ?h`(a)=b"

by auto

} hence "∀b∈B×D. ∃a∈A×C. ?h`(a) = b" by auto

with pfun show ?thesis unfolding surj_def by auto

qed

text{*For a function of two variables created from functions of one variable as in

@{text "cart_prod_fun"} above, the inverse image of a cartesian product of sets is the

cartesian product of inverse images.*}

lemma cart_prod_fun_vimage: assumes "f⇩_{1}:X⇩_{1}->Y⇩_{1}" "f⇩_{2}:X⇩_{2}->Y⇩_{2}" and

"g = {⟨p,⟨f⇩_{1}`(fst(p)),f⇩_{2}`(snd(p))⟩⟩. p ∈ X⇩_{1}×X⇩_{2}}"

shows "g-``(A⇩_{1}×A⇩_{2}) = f⇩_{1}-``(A⇩_{1}) × f⇩_{2}-``(A⇩_{2})"

proof -

from assms have "g: X⇩_{1}×X⇩_{2}-> Y⇩_{1}×Y⇩_{2}" using cart_prod_fun

by simp

then have "g-``(A⇩_{1}×A⇩_{2}) = {p ∈ X⇩_{1}×X⇩_{2}. g`(p) ∈ A⇩_{1}×A⇩_{2}}" using func1_1_L15

by simp

with assms `g: X⇩_{1}×X⇩_{2}-> Y⇩_{1}×Y⇩_{2}` show "g-``(A⇩_{1}×A⇩_{2}) = f⇩_{1}-``(A⇩_{1}) × f⇩_{2}-``(A⇩_{2})"

using ZF_fun_from_tot_val func1_1_L15 by auto

qed

text{*For a function of two variables defined on $X\times Y$, if we fix an

$x\in X$ we obtain a function on $Y$.

Note that if @{text "domain(f)"} is $X\times Y$, @{text "range(domain(f))"}

extracts $Y$ from $X\times Y$.*}

definition

"Fix1stVar(f,x) ≡ {⟨y,f`⟨x,y⟩⟩. y ∈ range(domain(f))}"

text{*For every $y\in Y$ we can fix the second variable in a binary function

$f: X\times Y \rightarrow Z$ to get a function on $X$.*}

definition

"Fix2ndVar(f,y) ≡ {⟨x,f`⟨x,y⟩⟩. x ∈ domain(domain(f))}"

text{*We defined @{text "Fix1stVar"} and @{text "Fix2ndVar"} so that

the domain of the function is not listed in the arguments, but is recovered

from the function. The next lemma is a technical fact that makes it easier

to use this definition.*}

lemma fix_var_fun_domain: assumes A1: "f : X×Y -> Z"

shows

"x∈X --> Fix1stVar(f,x) = {⟨y,f`⟨x,y⟩⟩. y ∈ Y}"

"y∈Y --> Fix2ndVar(f,y) = {⟨x,f`⟨x,y⟩⟩. x ∈ X}"

proof -

from A1 have I: "domain(f) = X×Y" using func1_1_L1 by simp

{ assume "x∈X"

with I have "range(domain(f)) = Y" by auto

then have "Fix1stVar(f,x) = {⟨y,f`⟨x,y⟩⟩. y ∈ Y}"

using Fix1stVar_def by simp

} then show "x∈X --> Fix1stVar(f,x) = {⟨y,f`⟨x,y⟩⟩. y ∈ Y}"

by simp

{ assume "y∈Y"

with I have "domain(domain(f)) = X" by auto

then have "Fix2ndVar(f,y) = {⟨x,f`⟨x,y⟩⟩. x ∈ X}"

using Fix2ndVar_def by simp

} then show "y∈Y --> Fix2ndVar(f,y) = {⟨x,f`⟨x,y⟩⟩. x ∈ X}"

by simp

qed

text{*If we fix the first variable, we get a function of the second variable.*}

lemma fix_1st_var_fun: assumes A1: "f : X×Y -> Z" and A2: "x∈X"

shows "Fix1stVar(f,x) : Y -> Z"

proof -

from A1 A2 have "∀y∈Y. f`⟨x,y⟩ ∈ Z"

using apply_funtype by simp

then have "{⟨y,f`⟨x,y⟩⟩. y ∈ Y} : Y -> Z"

using ZF_fun_from_total by simp

with A1 A2 show "Fix1stVar(f,x) : Y -> Z"

using fix_var_fun_domain by simp

qed

text{*If we fix the second variable, we get a function of the first

variable.*}

lemma fix_2nd_var_fun: assumes A1: "f : X×Y -> Z" and A2: "y∈Y"

shows "Fix2ndVar(f,y) : X -> Z"

proof -

from A1 A2 have "∀x∈X. f`⟨x,y⟩ ∈ Z"

using apply_funtype by simp

then have "{⟨x,f`⟨x,y⟩⟩. x ∈ X} : X -> Z"

using ZF_fun_from_total by simp

with A1 A2 show "Fix2ndVar(f,y) : X -> Z"

using fix_var_fun_domain by simp

qed

text{*What is the value of @{text "Fix1stVar(f,x)"} at $y\in Y$

and the value of @{text "Fix2ndVar(f,y)"} at $x\in X$"? *}

lemma fix_var_val:

assumes A1: "f : X×Y -> Z" and A2: "x∈X" "y∈Y"

shows

"Fix1stVar(f,x)`(y) = f`⟨x,y⟩"

"Fix2ndVar(f,y)`(x) = f`⟨x,y⟩"

proof -

let ?f⇩_{1}= "{⟨y,f`⟨x,y⟩⟩. y ∈ Y}"

let ?f⇩_{2}= "{⟨x,f`⟨x,y⟩⟩. x ∈ X}"

from A1 A2 have I:

"Fix1stVar(f,x) = ?f⇩_{1}"

"Fix2ndVar(f,y) = ?f⇩_{2}"

using fix_var_fun_domain by auto

moreover from A1 A2 have

"Fix1stVar(f,x) : Y -> Z"

"Fix2ndVar(f,y) : X -> Z"

using fix_1st_var_fun fix_2nd_var_fun by auto

ultimately have "?f⇩_{1}: Y -> Z" and "?f⇩_{2}: X -> Z"

by auto

with A2 have "?f⇩_{1}`(y) = f`⟨x,y⟩" and "?f⇩_{2}`(x) = f`⟨x,y⟩"

using ZF_fun_from_tot_val by auto

with I show

"Fix1stVar(f,x)`(y) = f`⟨x,y⟩"

"Fix2ndVar(f,y)`(x) = f`⟨x,y⟩"

by auto

qed

text{*Fixing the second variable commutes with restrictig the domain.*}

lemma fix_2nd_var_restr_comm:

assumes A1: "f : X×Y -> Z" and A2: "y∈Y" and A3: "X⇩_{1}⊆ X"

shows "Fix2ndVar(restrict(f,X⇩_{1}×Y),y) = restrict(Fix2ndVar(f,y),X⇩_{1})"

proof -

let ?g = "Fix2ndVar(restrict(f,X⇩_{1}×Y),y)"

let ?h = "restrict(Fix2ndVar(f,y),X⇩_{1})"

from A3 have I: "X⇩_{1}×Y ⊆ X×Y" by auto

with A1 have II: "restrict(f,X⇩_{1}×Y) : X⇩_{1}×Y -> Z"

using restrict_type2 by simp

with A2 have "?g : X⇩_{1}-> Z"

using fix_2nd_var_fun by simp

moreover

from A1 A2 have III: "Fix2ndVar(f,y) : X -> Z"

using fix_2nd_var_fun by simp

with A3 have "?h : X⇩_{1}-> Z"

using restrict_type2 by simp

moreover

{ fix z assume A4: "z ∈ X⇩_{1}"

with A2 I II have "?g`(z) = f`⟨z,y⟩"

using restrict fix_var_val by simp

also from A1 A2 A3 A4 have "f`⟨z,y⟩ = ?h`(z)"

using restrict fix_var_val by auto

finally have "?g`(z) = ?h`(z)" by simp

} then have "∀z ∈ X⇩_{1}. ?g`(z) = ?h`(z)" by simp

ultimately show "?g = ?h" by (rule func_eq)

qed

text{*The next lemma expresses the inverse image of a set by function with fixed

first variable in terms of the original function.*}

lemma fix_1st_var_vimage:

assumes A1: "f : X×Y -> Z" and A2: "x∈X"

shows "Fix1stVar(f,x)-``(A) = {y∈Y. ⟨x,y⟩ ∈ f-``(A)}"

proof -

from assms have "Fix1stVar(f,x)-``(A) = {y∈Y. Fix1stVar(f,x)`(y) ∈ A}"

using fix_1st_var_fun func1_1_L15 by blast

with assms show ?thesis using fix_var_val func1_1_L15 by auto

qed

text{*The next lemma expresses the inverse image of a set by function with fixed

second variable in terms of the original function.*}

lemma fix_2nd_var_vimage:

assumes A1: "f : X×Y -> Z" and A2: "y∈Y"

shows "Fix2ndVar(f,y)-``(A) = {x∈X. ⟨x,y⟩ ∈ f-``(A)}"

proof -

from assms have I: "Fix2ndVar(f,y)-``(A) = {x∈X. Fix2ndVar(f,y)`(x) ∈ A}"

using fix_2nd_var_fun func1_1_L15 by blast

with assms show ?thesis using fix_var_val func1_1_L15 by auto

qed

end