Theory Generalization

Up to index of Isabelle/ZF/gen

theory Generalization
imports ZF_Addons

header {* A theory of generalization *}

theory Generalization
imports Main_ZF ZF_Addons
begin


text {*
This theory formalizes the intuitive notion of \emph{generalization}.
*}


subsection {* Generalization situation *}

locale generalization_situation =
fixes small::i and big::i
fixes embed::i
assumes embed_inj: "embed∈inj(small, big)"
begin


text {*
In Isabelle 2009-2 locale params are not visible.
As a workaround I define their abbreviations:
*}

abbreviation "small_param ≡ small"
abbreviation "big_param ≡ big"
abbreviation "embed_param ≡ embed"

definition small2_def: "small2 ≡ range(embed)"
definition spec_def: "spec ≡ converse(embed)"

lemma spec_inj: "spec∈inj(small2, small)"
proof -
from embed_inj have "converse(embed)∈inj(range(embed), small)" by (rule inj_converse_inj)
with small2_def spec_def show ?thesis by simp
qed

lemma spec_fun: "spec: small2->small"
proof -
from embed_inj have "converse(embed): range(embed)->small" by (rule inj_converse_fun)
with small2_def spec_def show ?thesis by simp
qed

lemma embed_fun: "embed: small->big" by (rule inj_is_fun[OF embed_inj])

lemma embed_surj: "embed∈surj(small, small2)"
proof -
have "embed∈surj(small, range(embed))" by (rule fun_is_surj[OF embed_fun])
hence ?thesis "embed∈surj(small, small2)" by (unfold small2_def)
show ?thesis by fact
qed

theorem embed_bij: "embed∈bij(small, small2)"
proof -
from embed_inj have "embed∈bij(small, range(embed))" using inj_bij_range by auto
thus ?thesis by (unfold small2_def)
qed

theorem small2_sub_big: "small2⊆big" using embed_fun range_subset by (auto simp add: small2_def)

theorem spec_bij: "spec∈bij(small2, small)"
proof -
have "converse(embed)∈bij(small2, small)" by (rule bij_converse_bij[OF embed_bij])
thus ?thesis by (unfold spec_def)
qed

end

subsection {* Arbitrary generalizations *}

locale arbitrary_generalization = generalization_situation +
fixes newbig::i
fixes move::i
assumes
move_bij: "move∈bij(big, newbig)" and
move_embed: "move O embed = id(small)"
begin


text {*
In Isabelle 2009-2 locale params are not visible.
As a workaround I define their abbreviations:
*}

abbreviation "newbig_param ≡ newbig"
abbreviation "move_param ≡ move"

lemma move_fun: "move: big->newbig" using move_bij bij_is_fun by auto

lemma move_inj: "move∈inj(big, newbig)" using move_bij by (rule bij_is_inj)
lemma move_surj: "move∈surj(big, newbig)" using move_bij by (rule bij_is_surj)

lemma move_domain: "domain(move) = big" using domain_of_fun [OF move_fun] by auto

theorem move_embed_plain [simp]: "x∈small ==> move`(embed`x) = x"
proof -
assume "x: small"
with embed_fun have "move`(embed`x) = (move O embed)`x" using comp_fun_apply by auto
also have "... = id(small)`x" by (simp add: move_embed)
also with `x∈small` have "id(small)`x = x" by simp
finally show "move`(embed`x) = x" by simp
qed

definition ret_def: "ret ≡ converse(move)"

lemma ret_bij: "ret∈bij(newbig, big)" using move_bij unfolding ret_def by auto

lemma ret_inj: "ret∈inj(newbig, big)" using ret_bij by (rule bij_is_inj)
lemma ret_surj: "ret∈surj(newbig, big)" using ret_bij by (rule bij_is_surj)

lemma ret_restrict: "embed = restrict(ret, small)"
proof -
have "converse(move) O move O embed = converse(move) O id(small)" using move_embed by auto
hence "(converse(move) O move) O embed = converse(move) O id(small)" using comp_assoc by auto
moreover
with left_comp_inverse move_inj have i [simp]: "converse(move) O move = id(big)" by simp
ultimately have a: "id(big) O embed = converse(move) O id(small)" by simp
with embed_fun have "embed⊆small×big" using fun_is_rel by auto
hence "id(big) O embed = embed" using left_comp_id by auto
with a have "embed = converse(move) O id(small)" by auto
hence "embed = restrict(converse(move), small)" using right_comp_id_any by auto
thus "embed = restrict(ret, small)" using right_comp_id_any unfolding ret_def by auto
qed

end

subsection {* ZF generalization *}

text {* We will need this lemma to assert that ZF generalization is an arbitrary generalization: *}

lemma mem_not_refl_2: "{t}∉t"
proof
assume as: "{t}∈t"
let ?A = "{t,{t}}"
have nz: "?A ≠ 0" by auto
have "∀x∈?A. ∃y∈x. y∈?A"
proof
fix "x" assume "x∈?A"
have x_in_A: "x∈?A" by fact
have ex: "∃y∈x. y∈?A"
proof cases
assume "x=t"
with as have "{t}∈x ∧ {t}∈?A" by auto
thus ?thesis by auto
next
assume "x≠t"
with x_in_A have "x={t}" by auto
with as have "t∈x ∧ t∈?A" by auto
thus ?thesis by auto
qed
thus "∃y∈x. y∈?A" by auto
qed
with foundation show False by auto
qed

locale ZF_generalization = generalization_situation
begin


definition token_def: "token ≡ Pow(\<Union>(\<Union>(small)))"

lemma token_not_small: "⟨token,x⟩∉small"
proof
assume "⟨token,x⟩∈small"
hence "{{token,token}, {token,x}}∈small" by (simp add: Pair_def)
hence "{{token}, {token,x}}∈small" by auto
hence "{token}∈ \<Union>(small)" by auto
hence "{token} ⊆ \<Union>(\<Union>(small))" by auto
hence "{token}∈Pow(\<Union>(\<Union>(small)))" by auto
hence "{token}∈token" by (simp add: token_def)
with mem_not_refl_2 show False by contradiction
qed

definition zf_move_fun::"i=>i" where zf_move_fun_def: "zf_move_fun(x) ≡ if x: small2 then spec`x else ⟨token,x⟩"
definition zf_move_def: "zf_move ≡ (lam x:big. zf_move_fun(x))"

definition zf_newbig_def: "zf_newbig ≡ range(zf_move)"

lemma zf_move_domain: "domain(zf_move) = big" using domain_lam by (auto simp add: zf_move_def)

lemma zf_move_fun: "zf_move: big->zf_newbig" by (simp add: lam_is_fun zf_move_def zf_newbig_def)

theorem small_less_zf_newbig: "small ⊆ zf_newbig"
proof
fix x
assume s: "x∈small"
with embed_fun have "embed`x∈range(embed)" by (rule apply_rangeI)
hence s1: "embed`x∈small2" by (unfold small2_def)
with small2_sub_big have s2: "embed`x∈big" by auto
hence "zf_move`(embed`x) = zf_move_fun(embed`x)" by (auto simp add: zf_move_def)
with s1 have "zf_move`(embed`x) = spec`(embed`x)" by (simp add: zf_move_fun_def)
with embed_inj s spec_def have x_val: "zf_move`(embed`x) = x" using left_inverse by auto
from zf_move_fun s2 have "zf_move`(embed`x)∈range(zf_move)" by (rule apply_rangeI)
with x_val have "x∈range(zf_move)" by auto
with x_val zf_newbig_def show "x∈zf_newbig" by auto
qed

theorem zf_move_inj: "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" "b∈big"
assume move_eq: "zf_move`a = zf_move`b"
have spec1_a: "a:small2 ==> zf_move`a = spec`a"
proof -
assume "a∈small2"
with `a∈big` show ?thesis by (simp add: zf_move_def zf_move_fun_def)
qed
have spec1_b: "b∈small2 ==> zf_move`b = spec`b"
proof -
assume "b∈small2"
with `b∈big` show ?thesis by (simp add: zf_move_def zf_move_fun_def)
qed
have spec2_a: "a∉small2 ==> zf_move`a = ⟨token,a⟩"
proof -
assume "a∉small2"
with `a∈big` show ?thesis by (simp add: zf_move_def zf_move_fun_def)
qed
have spec2_b: "b∉small2 ==> zf_move`b = ⟨token,b⟩"
proof -
assume "b∉small2"
with `b∈big` show ?thesis by (simp add: zf_move_def zf_move_fun_def)
qed
have "a=b"
proof -
{ assume "a∈small2" "b∈small2"
from `a∈small2` have "zf_move`a = spec`a" by (rule spec1_a)
moreover
from `b∈small2` have "zf_move`b = spec`b" by (rule spec1_b)
ultimately
have "spec`a = spec`b" using move_eq by auto
with spec_inj `a:small2` `b:small2` have "a=b" using inj_def by auto
}
moreover
{ assume "a∈small2" "b∉small2"
from `a∈small2` have "zf_move`a = spec`a" by (rule spec1_a)
with spec_fun `a∈small2` have ma_s: "zf_move`a∈small" using apply_funtype by auto
from `b∉small2` have "zf_move`b = ⟨token,b⟩" by (rule spec2_b)
hence "zf_move`b∉small" using token_not_small by auto
with move_eq ma_s have False by auto
}
moreover
{ assume "a∉small2" "b∈small2"
from `b∈small2` have "zf_move`b = spec`b" by (rule spec1_b)
with spec_fun `b∈small2` have mb_s: "zf_move`b∈small" using apply_funtype by auto
from `a∉small2` have "zf_move`a = ⟨token,a⟩" by (rule spec2_a)
hence "zf_move`a∉small" using token_not_small by auto
with move_eq mb_s have False by auto
}
moreover
{ assume "a∉small2" "b∉small2"
from `a∉small2` have mt_a: "zf_move`a = ⟨token,a⟩" by (rule spec2_a)
moreover
from `b∉small2` have mt_b: "zf_move`b = ⟨token,b⟩" by (rule spec2_b)
from move_eq mt_a mt_b have "⟨token,a⟩=⟨token,b⟩" by auto -- "Order of from conditions is important to not cause infinite loop"
hence "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

theorem zf_move_surj: "zf_move∈surj(big, zf_newbig)"
proof -
have "zf_move∈surj(big, range(zf_move))" by (rule fun_is_surj[OF zf_move_fun])
hence ?thesis "zf_move∈surj(big, zf_newbig)" by (unfold zf_newbig_def)
show ?thesis by fact
qed

theorem zf_move_bij: "zf_move∈bij(big, zf_newbig)"
proof -
from zf_move_inj have "zf_move∈bij(big, range(zf_move))" using inj_bij_range by auto
thus ?thesis by (unfold zf_newbig_def)
qed

theorem zf_move_embed [simp]: "x∈small ==> zf_move`(embed`x) = x"
proof -
assume "x∈small"
with embed_fun have "embed`x∈range(embed)" by (rule apply_rangeI)
hence s1: "embed`x∈small2" by (unfold small2_def)
with small2_sub_big have "embed`x∈big" by auto
with s1 have "zf_move`(embed`x) = spec`(embed`x)" by (auto simp add: zf_move_def zf_move_fun_def)
also from embed_inj `x∈small` spec_def have "spec`(embed`x) = x" by auto
finally show "zf_move`(embed`x) = x" by auto
qed

theorem zf_embed_move: "zf_move O embed = id(small)"
proof -
have "∀y∈small. zf_move`(embed`y) = y" by simp
moreover
have "embed: small->big" by (rule embed_fun)
moreover
have "zf_move: big->zf_newbig" by (rule zf_move_fun)
ultimately show ?thesis using comp_eq_id_iff1 by blast
qed

end

text {* Next prove that ZF generalization is an arbitrary generalization: *}
sublocale ZF_generalization arbitrary_generalization small big embed zf_newbig zf_move
proof
show "zf_move∈bij(big, zf_newbig)" using zf_move_bij by auto
show "zf_move O embed = id(small)" using zf_embed_move by auto
qed

end