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{*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{*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 func_imagedef 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\<^isub>0
where II: "f`(x\<^isub>0) = y" and "x\<^isub>0 ∈ C"
using func_imagedef by auto;
with A1 A2 I `x∈A` have
"f ∈ inj(A,B)" "f`(x) = f`(x\<^isub>0)" "x∈A" "x\<^isub>0 ∈ A"
by auto;
then have "x = x\<^isub>0" by (rule inj_apply_equality);
with `x ∈ A-C` `x\<^isub>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 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{*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\<^isub>0 where "i\<^isub>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{*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{*Fixing variables in functions*}
text{*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{*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\<^isub>1 = "{⟨y,f`⟨x,y⟩⟩. y ∈ Y}"
let ?f\<^isub>2 = "{⟨x,f`⟨x,y⟩⟩. x ∈ X}";
from A1 A2 have I:
"Fix1stVar(f,x) = ?f\<^isub>1"
"Fix2ndVar(f,y) = ?f\<^isub>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\<^isub>1 : Y -> Z" and "?f\<^isub>2 : X -> Z"
by auto;
with A2 have "?f\<^isub>1`(y) = f`⟨x,y⟩" and "?f\<^isub>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\<^isub>1 ⊆ X"
shows "Fix2ndVar(restrict(f,X\<^isub>1×Y),y) = restrict(Fix2ndVar(f,y),X\<^isub>1)"
proof -
let ?g = "Fix2ndVar(restrict(f,X\<^isub>1×Y),y)"
let ?h = "restrict(Fix2ndVar(f,y),X\<^isub>1)"
from A3 have I: "X\<^isub>1×Y ⊆ X×Y" by auto;
with A1 have II: "restrict(f,X\<^isub>1×Y) : X\<^isub>1×Y -> Z"
using restrict_type2 by simp;
with A2 have "?g : X\<^isub>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\<^isub>1 -> Z"
using restrict_type2 by simp;
moreover
{ fix z assume A4: "z ∈ X\<^isub>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\<^isub>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