Theory Generalization_ZF
section ‹Generalizations›
theory Generalization_ZF imports func1
begin
text‹
This theory formalizes the intuitive notion of \emph{generalization}.
See http://www.mathematics21.org/generalization.html for more details.
Contributed by Victor Porton.
›
subsection‹Generalization situation›
text‹In mathematics it is often encountered that a small set $S$
naturally bijectively corresponds to a
subset $R$ of a larger set $B$. (In other words, there is specified an injection
$E$ from $S$ to $B$.) It is a widespread practice to equate $S$ with $R$.
But strictly speaking this equating may contradict to the axioms of ZF/ZFC
because we are not insured against $S\cap B\neq \emptyset$ incidents.
To work around of this (and formulate things exactly what could benefit
computer proof assistants) we will replace the set B with a new set B
having a bijection $M : B \rightarrow B$ such that $M \circ E = id_S$.
(I call this bijection $M$ from the first letter of the word "move"
which signifies the move from the old set $B$ to a new set $B$.
This section contains some basic lemmas holding in this setup.
›
text‹The next locale defines our assumptions.›
locale generalization =
fixes small and big
fixes embed
assumes embed_inj: "embed ∈ inj(small, big)"
text‹We define the ‹small2› set as the range of ‹embed›.›
definition (in generalization) "small2 ≡ range(embed)"
text‹We define ‹spec› as the converse of ‹embed›.›
definition (in generalization) "spec ≡ converse(embed)"
text‹Spec is an injection from range of ‹embed› to ‹small›.›
lemma (in generalization) spec_inj: shows "spec ∈ inj(small2, small)"
using embed_inj inj_converse_inj small2_def spec_def by simp
text‹Spec maps range of ‹embed› to ‹small›.›
lemma (in generalization) spec_fun: shows "spec: small2→small"
using embed_inj inj_converse_fun small2_def spec_def by simp
text‹Embed maps ‹small›small to ‹big›.›
lemma (in generalization) embed_fun: shows "embed: small→big"
using embed_inj inj_is_fun by simp
text‹Embed is a surjection from ‹small› to ‹small2›.›
lemma (in generalization) embed_surj: shows "embed ∈ surj(small, small2)"
using fun_is_surj embed_fun small2_def by simp
text‹Embed is a bijection between ‹small› and ‹small2›.›
theorem (in generalization) embed_bij: shows "embed ∈ bij(small, small2)"
using embed_inj inj_bij_range small2_def by simp
text‹‹small2› (i.e. range of ‹embed›) is a
subset of ‹big›.›
theorem (in generalization) small2_sub_big: shows "small2 ⊆ big"
using embed_fun func1_1_L5B small2_def by simp
text‹‹spec› is a bijection beween ‹small2› and ‹small›.›
theorem (in generalization) spec_bij: shows "spec ∈ bij(small2, small)"
using bij_converse_bij embed_bij spec_def by simp
subsection‹Arbitrary generalizations›
text‹This section considers a more general situation.›
text‹The next locale extends ‹generalization›
adding another big set and the ‹move› operation.›
locale generalization1 = generalization +
fixes newbig
fixes move
assumes move_bij: "move ∈ bij(big, newbig)"
assumes move_embed: "move O embed = id(small)"
text‹in ‹generalization1› context we define ‹ret›
as the converse of ‹move›.›
definition (in generalization1) "ret ≡ converse(move)"
text‹‹move› is a map from ‹big› to ‹newbig›.›
lemma (in generalization1) move_fun: shows "move: big→newbig"
using move_bij bij_is_fun by simp
text‹‹move› is an injection from ‹big› to ‹newbig›.›
lemma (in generalization1) move_inj: shows "move∈inj(big, newbig)"
using move_bij bij_is_inj by simp
text‹Move is a surjection ‹big› to ‹newbig›.›
lemma (in generalization1) move_surj: shows "move∈surj(big, newbig)"
using move_bij bij_is_surj by simp
text‹‹big› is the domain of ‹move›.›
lemma (in generalization1) move_domain: shows "domain(move) = big"
using domain_of_fun move_fun by simp
text‹Composing ‹move› with ‹embed› takes elements of
‹small› to themselves.›
theorem (in generalization1) move_embed_plain: assumes "x∈small"
shows "move`(embed`(x)) = x"
proof -
from assms have "move`(embed`(x)) = (move O embed)`(x)"
using embed_fun comp_fun_apply by simp
with assms show ?thesis using move_embed by simp
qed
text‹‹ret› is a bijection from ‹newbig›newbig to ‹big›.›
lemma (in generalization1) ret_bij: shows "ret∈bij(newbig, big)"
using move_bij ret_def by simp
text‹‹ret› is a injection from ‹newbig› onto ‹big›.›
lemma (in generalization1) ret_inj: shows "ret ∈ inj(newbig,big)"
using ret_bij bij_is_inj by simp
text‹‹ret› is a surjection from ‹newbig› onto ‹big›.›
lemma (in generalization1) ret_surj: shows "ret ∈ surj(newbig,big)"
using ret_bij bij_is_surj by simp
text‹‹embed› is a restriciton of ‹ret› to ‹small›.›
lemma (in generalization1) ret_restrict: shows "embed = restrict(ret, small)"
proof -
have "embed⊆small×big"
using fun_is_rel embed_fun by auto
moreover
have "(converse(move) O move) O embed = converse(move) O id(small)"
using move_embed comp_assoc by auto
then have a: "id(big) O embed = converse(move) O id(small)"
using left_comp_inverse move_inj by simp
ultimately show ?thesis using left_comp_id right_comp_id_any ret_def
by auto
qed
subsection‹ZF generalization›
text‹We continue material from the previous section.›
text‹We will need this lemma to assert that ZF generalization
is an arbitrary generalization:›
lemma mem_not_refl_2: shows "{t} ∉ t"
using foundation by auto
text‹Definition of token.›
definition (in generalization) "token ≡ Pow(⋃(⋃(small)))"
text‹Definition of function moving the ‹small› set into ‹big›.›
definition (in generalization)
"zf_move_fun(x) ≡ if x∈small2 then spec`(x) else ⟨token,x⟩"
text‹Definition of ‹zf_move› - the ZF version of ‹zf_move_fun›.›
definition (in generalization)
"zf_move ≡ {⟨x,zf_move_fun(x)⟩. x∈big}"
text‹Definition of ‹zf_newbig› as the range of ‹zf_move›.›
definition (in generalization) "zf_newbig ≡ range(zf_move)"
text‹‹zf_move› is a function that maps ‹big› to ‹newbig›.›
lemma (in generalization) zf_move_fun: shows "zf_move: big→zf_newbig"
using lam_is_fun_range zf_move_def zf_newbig_def by simp
text‹‹token› is not in ‹small›.›
lemma (in generalization) token_not_small: shows "⟨token,x⟩∉small"
proof
assume "⟨token,x⟩∈small"
then have "{token}∈token" using token_def Pair_def by auto
then show False using mem_not_refl_2 by blast
qed
text‹Domain of ‹zf_move› is ‹big›.›
lemma (in generalization) zf_move_domain: shows "domain(zf_move) = big"
using zf_move_fun func1_1_L1 by simp
text‹‹small› is a subset of ‹big›.›
theorem (in generalization) small_less_zf_newbig:
shows "small ⊆ zf_newbig"
proof
fix x
assume s: "x ∈ small"
then have s1: "embed`(x) ∈ small2"
using embed_fun apply_rangeI small2_def
by simp
then have s2: "embed`(x)∈big" using small2_sub_big by auto
with s1 s have x_val: "zf_move`(embed`(x)) = x"
using ZF_fun_from_tot_val zf_move_fun embed_inj
left_inverse spec_def zf_move_def zf_move_fun_def
by simp
from s2 have "zf_move`(embed`(x))∈range(zf_move)"
using zf_move_fun apply_rangeI by simp
with x_val show "x ∈ zf_newbig" using zf_newbig_def by auto
qed
text‹‹zf_move› is an injection from ‹big›
to ‹zf_newbig›.›
theorem (in generalization) zf_move_inj: shows "zf_move∈inj(big, zf_newbig)"
proof -
have "∀a∈big. ∀b∈big.
zf_move`(a) = zf_move`(b) ⟶ a=b"
proof -
{
fix a b
assume "a∈big" and "b∈big"
then have spec1_a: "a∈small2 ⟶ zf_move`(a) = spec`(a)" and
spec2_a: "a∉small2 ⟶ zf_move`a = ⟨token,a⟩" and
spec1_b: "b∈small2 ⟶ zf_move`(b) = spec`(b)" and
spec2_b: "b∉small2 ⟶ zf_move`(b) = ⟨token,b⟩"
using ZF_fun_from_tot_val1 zf_move_fun_def zf_move_def
by auto
assume move_eq: "zf_move`(a) = zf_move`(b)"
have "a=b"
proof -
{ assume "a∈small2" and "b∈small2"
with ‹a∈small2› spec1_a ‹b∈small2› spec1_b move_eq
have I: "spec`(a) = spec`(b)" by simp
have "spec ∈ inj(small2,small)"
using spec_inj by simp
then have "spec ∈
{f:small2 → small. ∀w∈small2. ∀x∈small2. f`(w)=f`(x) ⟶ w=x}"
unfolding inj_def by auto
hence "∀w∈small2. ∀x∈small2. spec`(w)=spec`(x) ⟶ w=x" by auto
with ‹a∈small2› ‹b∈small2› I have "a=b" by auto
}
moreover
{ assume "a∈small2" "b∉small2"
with spec1_a spec_fun have ma_s: "zf_move`a∈small"
using apply_funtype by auto
from ‹b∉small2› spec2_b have "zf_move`b∉small"
using token_not_small by auto
with move_eq ma_s have False by auto
}
moreover
{ assume "a∉small2" and "b∈small2"
with spec1_b spec_fun have mb_s: "zf_move`(b)∈small"
using apply_funtype by auto
from ‹a∉small2› spec2_a have "zf_move`(a)∉small"
using token_not_small by auto
with move_eq mb_s have False by auto
}
moreover
{ assume "a∉small2" and "b∉small2"
with spec2_a spec2_b have
"zf_move`(a) = ⟨token,a⟩" and
"zf_move`(b) = ⟨token,b⟩"
by auto
with move_eq have "a=b" by auto
}
ultimately show "a=b" by auto
qed
}
thus ?thesis by auto
qed
with zf_move_fun show ?thesis using inj_def by simp
qed
text‹‹zf_move› is a surjection of ‹big› onto ‹zf_newbig›.›
theorem (in generalization) zf_move_surj:
shows "zf_move ∈ surj(big,zf_newbig)"
using zf_move_fun fun_is_surj zf_newbig_def by simp
text‹‹zf_move› is a bijection from ‹big› to ‹zf_newbig›.›
theorem (in generalization) zf_move_bij: shows "zf_move ∈ bij(big, zf_newbig)"
using zf_move_inj inj_bij_range zf_newbig_def by simp
text‹The essential condition to prove that composition of ‹zf_move›
and ‹embed› is identity.›
theorem (in generalization) zf_move_embed:
assumes "x ∈ small" shows "zf_move`(embed`(x)) = x"
using assms embed_fun apply_rangeI small2_sub_big ZF_fun_from_tot_val1
embed_inj small2_def spec_def zf_move_def zf_move_fun_def by auto
text‹Composition of ‹zf_move› and ‹embed› is identity.›
theorem (in generalization) zf_embed_move: shows "zf_move O embed = id(small)"
proof -
have "∀y∈small. zf_move`(embed`y) = y" and
"embed: small→big" and "zf_move: big→zf_newbig"
using zf_move_embed embed_fun zf_move_fun by auto
then show ?thesis using comp_eq_id_iff1 by blast
qed
end