(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2011 Victor Porton

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{Generalization\_ZF.thy}*}

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.

*}

section{* 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 @{text "small2"} set as the range of @{text "embed"}.*}

definition (in generalization) "small2 ≡ range(embed)";

text{*We define @{text "spec"} as the converse of @{text "embed"}.*}

definition (in generalization) "spec ≡ converse(embed)"

text{*Spec is an injection from range of @{text "embed"} to @{text "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 @{text "embed"} to @{text "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 @{text "small"}small to @{text "big"}.*}

lemma (in generalization) embed_fun: shows "embed: small->big"

using embed_inj inj_is_fun by simp;

text{*Embed is a surjection from @{text "small"} to @{text "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 @{text "small"} and @{text "small2"}.*}

theorem (in generalization) embed_bij: shows "embed ∈ bij(small, small2)"

using embed_inj inj_bij_range small2_def by simp;

text{* @{text "small2"} (i.e. range of @{text "embed"}) is a

subset of @{text "big"}.*}

theorem (in generalization) small2_sub_big: shows "small2 ⊆ big"

using embed_fun func1_1_L5B small2_def by simp;

text{*@{text "spec"} is a bijection beween @{text "small2"} and @{text "small"}.*}

theorem (in generalization) spec_bij: shows "spec ∈ bij(small2, small)"

using bij_converse_bij embed_bij spec_def by simp;

section{*Arbitrary generalizations *}

text{*This section considers a more general situation.*}

text{*The next locale extends @{text "generalization"}

adding another big set and the @{text "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 @{text "generalization1"} context we define @{text "ret"}

as the converse of @{text "move"}.*}

definition (in generalization1) "ret ≡ converse(move)";

text{* @{text "move"} is a map from @{text "big"} to @{text "newbig"}.*}

lemma (in generalization1) move_fun: shows "move: big->newbig"

using move_bij bij_is_fun by simp;

text{*@{text "move"} is an injection from @{text "big"} to @{text "newbig"}. *}

lemma (in generalization1) move_inj: shows "move∈inj(big, newbig)"

using move_bij bij_is_inj by simp;

text{*Move is a surjection @{text "big"} to @{text "newbig"}.*}

lemma (in generalization1) move_surj: shows "move∈surj(big, newbig)"

using move_bij bij_is_surj by simp;

text{* @{text "big"} is the domain of @{text "move"}.*}

lemma (in generalization1) move_domain: shows "domain(move) = big"

using domain_of_fun move_fun by simp;

text{*Composing @{text "move"} with @{text "embed"} takes elements of

@{text "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{* @{text "ret"} is a bijection from @{text "newbig"}newbig to @{text "big"}.*}

lemma (in generalization1) ret_bij: shows "ret∈bij(newbig, big)"

using move_bij ret_def by simp;

text{* @{text "ret"} is a injection from @{text "newbig"} onto @{text "big"}.*}

lemma (in generalization1) ret_inj: shows "ret ∈ inj(newbig,big)"

using ret_bij bij_is_inj by simp;

text{* @{text "ret"} is a surjection from @{text "newbig"} onto @{text "big"}.*}

lemma (in generalization1) ret_surj: shows "ret ∈ surj(newbig,big)"

using ret_bij bij_is_surj by simp

text{* @{text "embed"} is a restriciton of @{text "ret"} to @{text "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;

section{*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(\<Union>(\<Union>(small)))";

text{*Definition of function moving the @{text "small"} set into @{text "big"}.*}

definition (in generalization)

"zf_move_fun(x) ≡ if x∈small2 then spec`(x) else ⟨token,x⟩";

text{*Definition of @{text "zf_move"} - the ZF version of @{text "zf_move_fun"}.*}

definition (in generalization)

"zf_move ≡ {⟨x,zf_move_fun(x)⟩. x∈big}"

text{*Definition of @{text "zf_newbig"} as the range of @{text "zf_move"}.*}

definition (in generalization) "zf_newbig ≡ range(zf_move)"

text{* @{text "zf_move"} is a function that maps @{text "big"} to @{text "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{* @{text "token"} is not in @{text "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 @{text "zf_move"} is @{text "big"}.*}

lemma (in generalization) zf_move_domain: shows "domain(zf_move) = big"

using zf_move_fun func1_1_L1 by simp;

text{* @{text "small"} is a subset of @{text "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{* @{text "zf_move"} is an injection from @{text "big"}

to @{text "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{* @{text "zf_move"} is a surjection of @{text "big"} onto @{text "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{* @{text "zf_move"} is a bijection from @{text "big"} to @{text "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 @{text "zf_move"}

and @{text "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 @{text "zf_move"} and @{text "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