Theory MSOinHOL_lowenheim_skolem_lemmas
theory MSOinHOL_lowenheim_skolem_lemmas
imports
MSOinHOL_faithfulness_locale
MSOinHOL_comprehension
"HOL-Library.Countable_Set"
begin
text ‹Supporting lemmas for the downward Loewenheim--Skolem construction
in ‹MSOinHOL_lowenheim_skolem›. This file holds the technical
machinery (Skolem-witness operators ‹wF› / ‹wS›, the omega-stage
iteration ‹stage›, monotonicity / countability / common-stage
lemmas). The main theorems live in the parent file.›
text ‹Lemma ‹coincidence› (generalises ‹L12› / ‹N12›): truth depends only on
the free variables of ‹φ›. Compact structured induction; the binder
cases use IH after extending the agreement through the bound-variable
update via ‹EnvMod_def› / ‹SetMod_def›.›
lemma coincidence:
assumes "⋀x. x free_in φ ⟹ g x = g' x"
and "⋀X. X free2_in φ ⟹ G X = G' X"
shows "(⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g',G' ⊨⇧d φ)"
using assms
proof (induct φ arbitrary: g g' G G')
case (AtmD r u v) thus ?case by simp
next
case (PrdD X z) thus ?case by simp
next
case (NegD φ)
have "(⟨I,D,E⟩,g,G ⊨⇧d φ) = (⟨I,D,E⟩,g',G' ⊨⇧d φ)"
using NegD.hyps NegD.prems(1,2)
is_free.simps(3) is_free2.simps(3)
by presburger
thus ?case by simp
next
case (AndD φ ψ)
from AndD.hyps[of g g' G G'] AndD.prems show ?case by simp
next
case (ExD y φ)
have "(⟨I,D,E⟩,g[y←d],G ⊨⇧d φ) = (⟨I,D,E⟩,g'[y←d],G' ⊨⇧d φ)"
for d
using EnvMod_def ExD.hyps ExD.prems(1,2)
is_free.simps(5) is_free2.simps(5)
by presburger
thus ?case by simp
next
case (ExD2 Y φ)
have "(⟨I,D,E⟩,g,G⟨Y←S⟩ ⊨⇧d φ) = (⟨I,D,E⟩,g',G'⟨Y←S⟩ ⊨⇧d φ)" for S
by (rule ExD2.hyps) (use ExD2.prems in ‹auto simp: SetMod_def›)
thus ?case by simp
qed
text ‹The formula type ‹ℱ› is countable (datatype over countable atoms).›
instance ℱ :: countable by countable_datatype
text ‹Pad a finite parameter list to a total assignment (default outside
its range).›
definition padA :: "D ⇒ D list ⇒ (V ⇒ D)"
where "padA d0 xs = (λi. if i < length xs then xs ! i else d0)"
definition padB :: "(D ⇒ bool) ⇒ (D ⇒ bool) list ⇒ (V2 ⇒ (D ⇒ bool))"
where "padB S0 Ss = (λi. if i < length Ss then Ss ! i else S0)"
text ‹First-order (FO) and second-order (SO) Skolem witness functions
‹wF› and ‹wS› for a single existential demand of the form
‹∃y. ψ› or ‹∃⇩2Y. ψ›. A partial assignment is supplied as a list of
free-variable values padded out by defaults ‹d⇩0› and ‹S⇩0›
(via ‹padA› / ‹padB›). The function then asks whether the existential
demand is satisfiable in the big model ‹(I,D,E)›; if so it picks a
satisfying witness via the ‹SOME› operator, and otherwise
falls back to the default. These witnesses are the per-step building
blocks of the Tarski--Vaught stage construction below, which feeds
every existential demand of the formula with a witness whose value
comes from the big model but whose name lives in the (countable)
hull.›
definition wF ::
"ℐ ⇒ (D ⇒ bool) ⇒ ((D ⇒ bool) ⇒ bool)
⇒ D ⇒ (D ⇒ bool) ⇒ ℱ ⇒ V ⇒ D list
⇒ (D ⇒ bool) list ⇒ D"
where
"wF I D E d0 S0 ψ y xs Ss =
(if (∃d. D d ∧ ⟨I,D,E⟩,(padA d0 xs)[y←d],(padB S0 Ss) ⊨⇧d ψ)
then (SOME d. D d ∧
⟨I,D,E⟩,(padA d0 xs)[y←d],(padB S0 Ss) ⊨⇧d ψ)
else d0)"
definition wS ::
"ℐ ⇒ (D ⇒ bool) ⇒ ((D ⇒ bool) ⇒ bool)
⇒ D ⇒ (D ⇒ bool) ⇒ ℱ ⇒ V2 ⇒ D list
⇒ (D ⇒ bool) list ⇒ (D ⇒ bool)"
where
"wS I D E d0 S0 ψ Y xs Ss =
(if (∃S. E S ∧
⟨I,D,E⟩,(padA d0 xs),(padB S0 Ss)⟨Y←S⟩ ⊨⇧d ψ)
then (SOME S. E S ∧
⟨I,D,E⟩,(padA d0 xs),(padB S0 Ss)⟨Y←S⟩ ⊨⇧d ψ)
else S0)"
lemma wF_mem: "D d0 ⟹ D (wF I D E d0 S0 ψ y xs Ss)"
unfolding wF_def
by (cases "∃d. D d ∧
⟨I,D,E⟩,(padA d0 xs)[y←d],(padB S0 Ss) ⊨⇧d ψ";
simp, metis (mono_tags, lifting) someI_ex)
lemma wS_mem: "E S0 ⟹ E (wS I D E d0 S0 ψ Y xs Ss)"
unfolding wS_def
by (cases "∃S. E S ∧
⟨I,D,E⟩,(padA d0 xs),(padB S0 Ss)⟨Y←S⟩ ⊨⇧d ψ";
simp, metis (mono_tags, lifting) someI_ex)
text ‹Witness-membership specialised to seeds @{text "g 0"} /
@{text "G 0"}: no extra ‹D (g 0)› premise.›
lemma wF_mem_seed:
"g into D ⟹ D (wF I D E (g 0) S⇩0 ψ y xs Ss)"
by (blast intro: wF_mem)
lemma wS_mem_seed:
"G into E ⟹ E (wS I D E d⇩0 (G 0) ψ Y xs Ss)"
by (blast intro: wS_mem)
text ‹The omega-stage (FO carrier, SO carrier): step ‹n+1› adds every
‹wF› / ‹wS› witness over parameter lists drawn from the carriers at
stage ‹n›.›
primrec stage ::
"ℐ ⇒ (D ⇒ bool) ⇒ ((D ⇒ bool) ⇒ bool)
⇒ (V ⇒ D) ⇒ (V2 ⇒ (D ⇒ bool)) ⇒ nat
⇒ ((D ⇒ bool) × ((D ⇒ bool) ⇒ bool))"
where
"stage I D E g G 0 = (Range g, Range G)"
| "stage I D E g G (Suc n) =
((λd. fst (stage I D E g G n) d
∨ (∃ψ y xs Ss.
(∀x∈set xs. fst (stage I D E g G n) x)
∧ (∀S∈set Ss. snd (stage I D E g G n) S)
∧ d = wF I D E (g 0) (G 0) ψ y xs Ss)),
(λS. snd (stage I D E g G n) S
∨ (∃ψ Y xs Ss.
(∀x∈set xs. fst (stage I D E g G n) x)
∧ (∀S'∈set Ss. snd (stage I D E g G n) S')
∧ S = wS I D E (g 0) (G 0) ψ Y xs Ss)))"
text ‹Helper: countability of a binary product (from
‹countable_SIGMA›).›
lemma countable_Times2:
"countable A ⟹ countable B ⟹ countable (A × B)"
using countable_SIGMA[of A "λ_. B"] by (simp add: Sigma_def)
text ‹An explicit Skolem witness produced from parameters drawn from
stage ‹n› sits in stage ‹Suc n› (FO / SO). Direct from the second
clause of ‹stage›.›
lemma fst_stage_Suc_intro:
"∀x∈set xs. fst (stage I D E g G N) x ⟹
∀S∈set Ss. snd (stage I D E g G N) S ⟹
fst (stage I D E g G (Suc N)) (wF I D E (g 0) (G 0) ψ y xs Ss)"
by (simp, blast)
lemma snd_stage_Suc_intro:
"∀x∈set xs. fst (stage I D E g G N) x ⟹
∀S∈set Ss. snd (stage I D E g G N) S ⟹
snd (stage I D E g G (Suc N)) (wS I D E (g 0) (G 0) ψ Y xs Ss)"
by (simp, blast)
text ‹The next two lemmas are instances of the coincidence lemma in
which the assignments ‹a›, ‹b› are first restricted to the
free-variable prefix of ‹ψ› (the indices ‹[0..<fresh ψ]› and
‹[0..<fresh2 ψ]›) and then re-extended to total assignments via
‹padA› / ‹padB› with defaults ‹d⇩0›, ‹S⇩0›. Because ‹ψ› can only
look at the variables it actually uses, the value of ‹ψ› under the
padded assignment coincides with its value under the original one.
This is precisely the rewrite needed for the Tarski--Vaught step:
the truth of an existential demand on the partial (padded) assignment
is the truth of the same demand on the original assignment, so a
witness chosen for the padded form automatically refutes / verifies
the original form, and the truth transfer through one stage of the
hull construction goes through by @{method simp} alone.›
lemma pad_truth_eq_FO:
"(⟨I,D,E⟩, (padA d⇩0 (map a [0..<fresh ψ]))[y←d], (padB S⇩0 (map b [0..<fresh2 ψ])) ⊨⇧d ψ) = (⟨I,D,E⟩, a[y←d], b ⊨⇧d ψ)"
by (rule coincidence)
(auto dest!: L6 N6 simp: EnvMod_def padA_def padB_def)
lemma pad_truth_eq_SO:
"(⟨I,D,E⟩, padA d⇩0 (map a [0..<fresh ψ]), (padB S⇩0 (map b [0..<fresh2 ψ]))⟨Y←S⟩ ⊨⇧d ψ) = (⟨I,D,E⟩, a, b⟨Y←S⟩ ⊨⇧d ψ)"
by (rule coincidence)
(auto dest!: L6 N6 simp: SetMod_def padA_def padB_def)
text ‹The Skolem witness ‹wF› / ‹wS› realizes its demand whenever one
exists in ‹(D,E)›: membership in ‹D› / ‹E› plus the truth on the
padded assignment. Direct from ‹someI_ex›.›
lemma wF_realizes:
assumes "∃d. D d ∧
⟨I,D,E⟩,(padA d0 xs)[y←d],(padB S0 Ss) ⊨⇧d ψ"
shows "D (wF I D E d0 S0 ψ y xs Ss)
∧ (⟨I,D,E⟩,(padA d0 xs)[y←wF I D E d0 S0 ψ y xs Ss],
(padB S0 Ss) ⊨⇧d ψ)"
using someI_ex[OF assms] assms unfolding wF_def by simp
lemma wS_realizes:
assumes "∃S. E S ∧
⟨I,D,E⟩,(padA d0 xs),(padB S0 Ss)⟨Y←S⟩ ⊨⇧d ψ"
shows "E (wS I D E d0 S0 ψ Y xs Ss)
∧ (⟨I,D,E⟩,(padA d0 xs),
(padB S0 Ss)⟨Y←wS I D E d0 S0 ψ Y xs Ss⟩
⊨⇧d ψ)"
using someI_ex[OF assms] assms unfolding wS_def by simp
text ‹Full Tarski--Vaught step (FO / SO): from an existential over
‹(D,E)› reachable through ‹a›, ‹b›, the ‹wF› / ‹wS› witness lives
in ‹D› / ‹E› and satisfies the formula relative to ‹a›, ‹b›. Core
lemma for the ‹TVfo› / ‹TVso› of ‹skolem_hull›.›
lemma skolem_step_FO:
assumes "∃d. D d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ"
shows "D (wF I D E d⇩0 S⇩0 ψ y
(map a [0..<fresh ψ]) (map b [0..<fresh2 ψ]))
∧ (⟨I,D,E⟩, a[y←wF I D E d⇩0 S⇩0 ψ y
(map a [0..<fresh ψ])
(map b [0..<fresh2 ψ])],
b ⊨⇧d ψ)"
proof -
let ?xs = "map a [0..<fresh ψ]"
and ?Ss = "map b [0..<fresh2 ψ]"
have "∃d. D d ∧ ⟨I,D,E⟩,(padA d⇩0 ?xs)[y←d],(padB S⇩0 ?Ss) ⊨⇧d ψ"
using assms by (simp add: pad_truth_eq_FO)
from wF_realizes[OF this] show ?thesis
by (simp add: pad_truth_eq_FO)
qed
lemma skolem_step_SO:
assumes "∃S. E S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ"
shows "E (wS I D E d⇩0 S⇩0 ψ Y
(map a [0..<fresh ψ]) (map b [0..<fresh2 ψ]))
∧ (⟨I,D,E⟩, a,
b⟨Y←wS I D E d⇩0 S⇩0 ψ Y
(map a [0..<fresh ψ])
(map b [0..<fresh2 ψ])⟩
⊨⇧d ψ)"
proof -
let ?xs = "map a [0..<fresh ψ]"
and ?Ss = "map b [0..<fresh2 ψ]"
have "∃S. E S ∧ ⟨I,D,E⟩,(padA d⇩0 ?xs),(padB S⇩0 ?Ss)⟨Y←S⟩ ⊨⇧d ψ"
using assms by (simp add: pad_truth_eq_SO)
from wS_realizes[OF this] show ?thesis
by (simp add: pad_truth_eq_SO)
qed
text ‹The ‹(Suc n)›-stage is contained in the ‹n›-stage plus the image
of ‹wF› / ‹wS› over the four-fold product ‹ℱ × V × Lists⇩𝒟(n) ×
Lists⇩𝒫(n)›, where the first two factors range over all formulas and
all binder variables, and the last two over lists of FO domain elements
resp.\ SO predicates that already live in the ‹n›-th stage. Used to
derive countability of each stage by induction.›
lemma fst_stage_Suc_subset:
"{d. fst (stage I D E g G (Suc n)) d}
⊆ {d. fst (stage I D E g G n) d}
∪ (λ(ψ, y, xs, Ss). wF I D E (g 0) (G 0) ψ y xs Ss) `
(UNIV × UNIV
× {xs. set xs ⊆ {d. fst (stage I D E g G n) d}}
× {Ss. set Ss ⊆ {S. snd (stage I D E g G n) S}})"
(is "_ ⊆ ?R")
proof (rule subsetI, simp only: mem_Collect_eq)
fix d assume "fst (stage I D E g G (Suc n)) d"
then consider
"fst (stage I D E g G n) d"
| ψ y xs Ss
where "∀x∈set xs. fst (stage I D E g G n) x"
"∀S∈set Ss. snd (stage I D E g G n) S"
"d = wF I D E (g 0) (G 0) ψ y xs Ss"
by auto
thus "d ∈ ?R"
by cases (auto intro!: rev_image_eqI[where x="(_, _, _, _)"])
qed
lemma snd_stage_Suc_subset:
"{S. snd (stage I D E g G (Suc n)) S}
⊆ {S. snd (stage I D E g G n) S}
∪ (λ(ψ, Y, xs, Ss). wS I D E (g 0) (G 0) ψ Y xs Ss) `
(UNIV × UNIV
× {xs. set xs ⊆ {d. fst (stage I D E g G n) d}}
× {Ss. set Ss ⊆ {S. snd (stage I D E g G n) S}})"
(is "_ ⊆ ?R")
proof (rule subsetI, simp only: mem_Collect_eq)
fix S assume "snd (stage I D E g G (Suc n)) S"
then consider
"snd (stage I D E g G n) S"
| ψ Y xs Ss
where "∀x∈set xs. fst (stage I D E g G n) x"
"∀S'∈set Ss. snd (stage I D E g G n) S'"
"S = wS I D E (g 0) (G 0) ψ Y xs Ss"
by auto
thus "S ∈ ?R"
by cases (auto intro!: rev_image_eqI[where x="(_, _, _, _)"])
qed
text ‹Monotonicity of the ‹stage› chain: a single-step extension lifts
to arbitrary suffixes.›
lemma fst_stage_mono:
"m ≤ n ⟹ fst (stage I D E g G m) d ⟹ fst (stage I D E g G n) d"
by (induct n) (auto simp del: stage.simps simp: stage.simps(2) le_Suc_eq)
lemma snd_stage_mono:
"m ≤ n ⟹ snd (stage I D E g G m) S ⟹ snd (stage I D E g G n) S"
by (induct n) (auto simp del: stage.simps simp: stage.simps(2) le_Suc_eq)
text ‹Finitely many parameters in the omega-union all share a common
stage.›
lemma common_stage_lifted:
assumes hx: "∀x∈set xs. ∃n. fst (stage I D E g G n) x"
and hS: "∀S∈set Ss. ∃n. snd (stage I D E g G n) S"
shows "∃N. (∀x∈set xs. fst (stage I D E g G N) x)
∧ (∀S∈set Ss. snd (stage I D E g G N) S)"
proof -
obtain fX where fX: "∀x∈set xs. fst (stage I D E g G (fX x)) x"
using hx by metis
obtain fS where fS: "∀S∈set Ss. snd (stage I D E g G (fS S)) S"
using hS by metis
let ?N = "Max (insert 0 (fX ` set xs ∪ fS ` set Ss))"
have bX: "fX x ≤ ?N" if "x ∈ set xs" for x
using that by (simp add: Max_ge)
have bS: "fS S ≤ ?N" if "S ∈ set Ss" for S
using that by (simp add: Max_ge)
from bX fX fst_stage_mono
have "∀x∈set xs. fst (stage I D E g G ?N) x" by blast
moreover from bS fS snd_stage_mono
have "∀S∈set Ss. snd (stage I D E g G ?N) S" by blast
ultimately show ?thesis by blast
qed
text ‹A ‹wF› / ‹wS› witness built from hull-valued parameters is itself
in the hull. Combines ‹common_stage_lifted› with the single-Suc-step
intros.›
lemma wF_in_omega_union:
assumes "∀x∈set xs. ∃n. fst (stage I D E g G n) x"
and "∀S∈set Ss. ∃n. snd (stage I D E g G n) S"
shows "∃n. fst (stage I D E g G n)
(wF I D E (g 0) (G 0) ψ y xs Ss)"
using common_stage_lifted[OF assms]
by (meson fst_stage_Suc_intro)
lemma wS_in_omega_union:
assumes "∀x∈set xs. ∃n. fst (stage I D E g G n) x"
and "∀S∈set Ss. ∃n. snd (stage I D E g G n) S"
shows "∃n. snd (stage I D E g G n)
(wS I D E (g 0) (G 0) ψ Y xs Ss)"
using common_stage_lifted[OF assms]
by (meson snd_stage_Suc_intro)
text ‹Tarski--Vaught closure of the omega-union: combines
‹skolem_step_FO› / ‹skolem_step_SO› with
‹wF_in_omega_union› / ‹wS_in_omega_union›.›
lemma stage_TV_FO:
assumes "a into (λd. ∃n. fst (stage I D E g G n) d)"
and "b into (λS. ∃n. snd (stage I D E g G n) S)"
and "∃d. D d ∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ"
shows "∃d. (∃n. fst (stage I D E g G n) d)
∧ ⟨I,D,E⟩,a[y←d],b ⊨⇧d ψ"
using skolem_step_FO[OF assms(3), of "g 0" "G 0"]
wF_in_omega_union[of "map a [0..<fresh ψ]" I D E g G
"map b [0..<fresh2 ψ]" ψ y]
assms(1,2)
by auto
lemma stage_TV_SO:
assumes "a into (λd. ∃n. fst (stage I D E g G n) d)"
and "b into (λS. ∃n. snd (stage I D E g G n) S)"
and "∃S. E S ∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ"
shows "∃S. (∃n. snd (stage I D E g G n) S)
∧ ⟨I,D,E⟩,a,b⟨Y←S⟩ ⊨⇧d ψ"
using skolem_step_SO[OF assms(3), of "g 0" "G 0"]
wS_in_omega_union[of "map a [0..<fresh ψ]" I D E g G
"map b [0..<fresh2 ψ]" ψ Y]
assms(1,2)
by auto
text ‹Inductive step for stage countability: each ‹Suc›-stage is
countable provided both ‹n›-stages are.›
lemma cntDE_step:
assumes cD: "countable {d. fst (stage I D E g G n) d}"
and cE: "countable {S. snd (stage I D E g G n) S}"
shows "countable {d. fst (stage I D E g G (Suc n)) d}"
and "countable {S. snd (stage I D E g G (Suc n)) S}"
proof -
let ?A = "{xs. set xs ⊆ {d. fst (stage I D E g G n) d}}"
let ?B = "{Ss. set Ss ⊆ {S. snd (stage I D E g G n) S}}"
have lDE: "countable ?A" "countable ?B"
apply (metis cD countable_lists lists_eq_set)
by (metis cE countable_lists lists_eq_set)
hence cT:
"countable ((UNIV::ℱ set) × (UNIV::V set) × ?A × ?B)"
"countable ((UNIV::ℱ set) × (UNIV::V2 set) × ?A × ?B)"
by (auto intro!: countable_Times2)
hence prods:
"countable ((λ(ψ,y,xs,Ss). wF I D E (g 0) (G 0) ψ y xs Ss) `
((UNIV::ℱ set) × (UNIV::V set) × ?A × ?B))"
"countable ((λ(ψ,Y,xs,Ss). wS I D E (g 0) (G 0) ψ Y xs Ss) `
((UNIV::ℱ set) × (UNIV::V2 set) × ?A × ?B))"
by (auto intro: countable_image)
from prods(1) cD fst_stage_Suc_subset[of I D E g G n]
show "countable {d. fst (stage I D E g G (Suc n)) d}"
by (meson countable_Un countable_subset)
from prods(2) cE snd_stage_Suc_subset[of I D E g G n]
show "countable {S. snd (stage I D E g G (Suc n)) S}"
by (meson countable_Un countable_subset)
qed
text ‹Stage carriers stay inside ‹D› / ‹E› (by induction on the stage;
‹wF_mem_seed› / ‹wS_mem_seed› handle the witness case).›
lemma fst_stage_subD:
"g into D ⟹ fst (stage I D E g G n) d ⟹ D d"
by (induct n arbitrary: d) (auto simp: wF_mem_seed)
lemma snd_stage_subE:
"G into E ⟹ snd (stage I D E g G n) S ⟹ E S"
by (induct n arbitrary: S) (auto simp: wS_mem_seed)
text ‹Every stage is countable; hence so is the omega-union of stages.
Pure consequence of ‹cntDE_step›.›
lemma stage_countable:
"countable {d. fst (stage I D E g G n) d}
∧ countable {S. snd (stage I D E g G n) S}"
proof (induct n)
case 0
have "{d. fst (stage I D E g G 0) d} = range g"
"{S. snd (stage I D E g G 0) S} = range G"
by auto
thus ?case by simp
next
case (Suc n) thus ?case
using cntDE_step[of I D E g G n] by simp
qed
lemma stage_omega_countable:
"countable {d. ∃n. fst (stage I D E g G n) d}"
"countable {S. ∃n. snd (stage I D E g G n) S}"
proof -
have eqs:
"{d. ∃n. fst (stage I D E g G n) d}
= (⋃n. {d. fst (stage I D E g G n) d})"
"{S. ∃n. snd (stage I D E g G n) S}
= (⋃n. {S. snd (stage I D E g G n) S})"
by auto
show "countable {d. ∃n. fst (stage I D E g G n) d}"
"countable {S. ∃n. snd (stage I D E g G n) S}"
unfolding eqs using stage_countable by (auto intro: countable_UN)
qed
text ‹Reindex one sort onto a countable nonempty sub-domain, keeping the
values on a finite ``guarded'' prefix specified by a predicate
‹free› bounded by ‹fr›.›
lemma reindex_one:
fixes free :: "nat ⇒ bool" and fr :: nat
and D⇩0 :: "'a ⇒ bool" and g :: "nat ⇒ 'a"
assumes "countable {x. D⇩0 x}" and "D⇩0 d⇩0"
and "Range g ❙⊆ D⇩0"
and bound: "⋀x. free x ⟹ x < fr"
obtains g' where "Range g' = D⇩0"
and "⋀x. free x ⟹ g' x = g x"
proof -
let ?D = "{x. D⇩0 x}"
have hD: "?D ≠ {}"
and re: "range (from_nat_into ?D) = ?D"
and mem: "D⇩0 (from_nat_into ?D k)" for k
using assms(2) range_from_nat_into[OF _ assms(1)]
from_nat_into
by auto
define g' where
"g' n = (if free n then g n else from_nat_into ?D (n - fr))"
for n
have "Range g' = D⇩0"
proof (rule ext, rule iffI)
fix d assume "Range g' d"
thus "D⇩0 d"
using assms(3) mem
by (auto simp: g'_def split: if_split_asm)
next
fix d assume "D⇩0 d"
hence "d ∈ range (from_nat_into ?D)" using re by simp
then obtain k where "from_nat_into ?D k = d" by auto
moreover have "¬ free (fr + k)" using bound by force
ultimately have "g' (fr + k) = d" by (simp add: g'_def)
thus "Range g' d" by auto
qed
moreover have "⋀x. free x ⟹ g' x = g x"
by (simp add: g'_def)
ultimately show ?thesis using that by blast
qed
text ‹Reindex (both sorts): reindex the (countably many) variables to
surject onto the countable @{text "D0, E0"}, while agreeing with the
originals on the finitely many free variables of ‹φ›. Two
applications of ‹reindex_one›.›
lemma reindex:
assumes "countable {d. D⇩0 d}" and "D⇩0 d⇩0"
and "countable {S. E⇩0 S}" and "E⇩0 S⇩0"
and "Range g ❙⊆ D⇩0" and "Range G ❙⊆ E⇩0"
obtains g' G'
where "Range g' = D⇩0" and "Range G' = E⇩0"
and "⋀x. x free_in φ ⟹ g' x = g x"
and "⋀X. X free2_in φ ⟹ G' X = G X"
proof -
obtain g' where g':
"Range g' = D⇩0"
"⋀x. x free_in φ ⟹ g' x = g x"
using reindex_one[OF assms(1,2,5),
of "λx. x free_in φ" "fresh φ"]
L6
by blast
obtain G' where G':
"Range G' = E⇩0"
"⋀X. X free2_in φ ⟹ G' X = G X"
using reindex_one[OF assms(3,4,6),
of "λX. X free2_in φ" "fresh2 φ"]
N6
by blast
show ?thesis using that g' G' by blast
qed
text ‹Reindex + coincidence in one step: obtain @{text "g'/G'"}
surjecting onto the countable @{text "D0/E0"} whose induced truth on
‹φ› coincides with the original.›
lemma reindex_coincide:
assumes "countable {d. D⇩0 d}" and "countable {S. E⇩0 S}"
and "Range g ❙⊆ D⇩0" and "Range G ❙⊆ E⇩0"
obtains g' G'
where "Range g' = D⇩0" and "Range G' = E⇩0"
and "(⟨I,D⇩0,E⇩0⟩,g,G ⊨⇧d φ)
= (⟨I,D⇩0,E⇩0⟩,g',G' ⊨⇧d φ)"
proof -
have nD: "D⇩0 (g 0)" and nE: "E⇩0 (G 0)"
using assms(3,4) by auto
obtain g' G' where rg: "Range g' = D⇩0" and rG: "Range G' = E⇩0"
and ag: "⋀x. x free_in φ ⟹ g' x = g x"
and aG: "⋀X. X free2_in φ ⟹ G' X = G X"
using reindex[OF assms(1) nD assms(2) nE assms(3,4)] by blast
have "(⟨I,D⇩0,E⇩0⟩,g,G ⊨⇧d φ) = (⟨I,D⇩0,E⇩0⟩,g',G' ⊨⇧d φ)"
by (rule coincidence) (simp_all add: ag aG)
thus thesis using that rg rG by blast
qed
end