Theory Permutation_models
section ‹Permutation models›
theory Permutation_models
imports ZFfin
begin
text ‹A useful tool of constructing models with specific properties is the Bernays-Rieger permutation method,
which redefines the membership relation. We show that a permutation model obtained in this way preserves extensionality,
empty set, powerset, union, and replacement. The method has been used, inter alia, in several works directly relevant to our formalization
(\<^cite>‹Rieger1957›, \<^cite>‹VopenkaHajek1963›, \<^cite>‹BaratellaFerro1993›, \<^cite>‹ManciniZambella2001›)›
locale permutation_model = L_setext_empty_power_union_repl +
fixes perm
assumes
bij_perm: "bij (perm :: 'a ⇒ 'a)" and
SR_fmem: "SetRelation (λ x y. x ε perm y)"
begin
abbreviation perm_mem (infixr "ε⇧f" 51) where
"perm_mem x y ≡ x ε perm y"
sublocale L_setext_empty
by unfold_locales
interpretation pm: L_setext perm_mem
proof (unfold_locales, rule iffI, blast)
show "x = y" if "∀z. z ε⇧f x = z ε⇧f y" for x y
using that[folded setext[of "perm x" "perm y"]] bij_perm
by (simp add: bij_betw_def inj_eq)
qed
lemma SFP_fmem[SFP_rules]: "SetFormulaPredicate (λΞ. Ξ m ε⇧f Ξ n)"
by (rule transform_variables[OF SR_fmem[unfolded SetRelation_def], of "id(0:=m,1:=n)", simplified])
lemma SR_perm_eq: "SetRelation (λ x y. perm x = y)"
unfolding SetRelation_def setext logsimps by (rule SFP_rules)+
lemma permSFP_SFP: assumes "pm.SetFormulaPredicate P" shows "SetFormulaPredicate P"
proof (rule pm.SetFormulaPredicate.induct[OF assms])
show "SetFormulaPredicate (λΞ. Ξ m ε⇧f Ξ n)" for m n
using transform_variables[OF SR_fmem[unfolded SetRelation_def], of "id(0:=_,1:=_)"] by simp
qed (simp_all add: SFP_rules)
lemma perm_model:
shows "L_setext_empty_power_union_repl perm_mem"
proof
write pm.subsetM (infix "⊆⇧f" 51 )
have finv: "perm ((inv perm) u) = u" for u
using bij_perm bij_inv_eq_iff by fast
have finv': "(inv perm) (perm u) = u" for u
using bij_perm bij_inv_eq_iff by metis
have inv_iff: "(inv perm) x = y ⟷ perm y = x" for x y
using bij_perm finv finv' by auto
have SR_f': "SetRelation (λ x y. (inv perm) x = y)"
using SR_sym[OF SR_perm_eq, unfolded SR_perm_eq] unfolding inv_iff.
have finv_unique: "∀u. ∃!v. v = inv perm u"
using bij_perm by blast
obtain femp where femp_def: "perm femp = ∅"
using bij_perm bij_pointE by metis
show "∃x. ∀y. ¬ y ε⇧f x"
using femp_def by (metis empty_is_empty)
have fsubset: "x ⊆⇧f y ⟷ (perm x) ⊆⇩M (perm y)" for x y
unfolding pm.subsetM_def subsetM_def..
show "∀x. ∃y. ∀u. u ε⇧f y = u ⊆⇧f x"
unfolding fsubset
proof
fix x
obtain y' where y': "⋀ u. u ε y' ⟷ u ⊆⇩M (perm x)"
using power[rule_format, of "perm x"] by blast
obtain y where y: "⋀ u. (u ε y) = (∃v. v ε y' ∧ inv perm v = u)"
using replf[OF SR_f'[unfolded SetRelation_def], rule_format, of _ y', simplified] by blast
have "∀v. (v ε perm (inv perm y)) ⟷ perm v ⊆⇩M perm x"
using y y' bij_perm bij_inv_eq_iff by metis
then show "∃y. ∀v. (v ε perm y) = perm v ⊆⇩M perm x"
by blast
qed
show "∀x. ∃y. ∀v. v ε⇧f y = (∃u. u ε⇧f x ∧ v ε⇧f u)"
proof
fix x
obtain x' where x': "⋀ u. (u ε x') = (∃v. v ε perm x ∧ perm v = u)"
using replf[OF SR_perm_eq[unfolded SetRelation_def], simplified]
using replf[OF SR_f'[unfolded SetRelation_def], rule_format, simplified] by blast
obtain y where y: "⋀ v. v ε y ⟷ (∃ u. u ε x' ∧ v ε u)"
using union[rule_format, of x'] by blast
have "∀v. (v ε perm (inv perm y)) ⟷ (∃u. u ε perm x ∧ v ε perm u)"
using y x' bij_perm finv by auto
then show "∃y. ∀v. (v ε perm y) = (∃u. u ε perm x ∧ v ε perm u)"
by blast
qed
fix P Ξ
assume "pm.SetFormulaPredicate P"
show "(∀u. ∃!v. P (Ξ(0 := u, 1 := v))) ⟶ (∀x. ∃z. ∀v. v ε⇧f z = (∃u. u ε⇧f x ∧ P (Ξ(0 := u, 1 := v))))"
proof (rule impI, rule allI)
assume "∀u. ∃!v. P (Ξ(0 := u, 1 := v))"
fix x
have "SetFormulaPredicate P"
by (simp add: ‹pm.SetFormulaPredicate P› permSFP_SFP)
from replf[rule_format, OF this ‹∀u. ∃!v. P (Ξ(0 := u, 1 := v))›[rule_format], of "perm x"]
obtain z where "∀v. (v ε z) = (∃u. u ε perm x ∧ P (Ξ(0 := u, 1 := v)))"
by blast
hence "∀v. (v ε perm ((inv perm) z)) = (∃u. u ε perm x ∧ P (Ξ(0 := u, 1 := v)))"
unfolding finv.
thus "∃z. ∀v. (v ε perm z) = (∃u. u ε perm x ∧ P (Ξ(0 := u, 1 := v))) "
by blast
qed
qed
end
end