Theory Skolem_Normal_Form
theory Skolem_Normal_Form
imports
Prenex_Normal_Form
Bumping
begin
lemma witness_imp_holds_exists:
assumes ‹is_interpretation (functions_term t, preds) (I :: (nat, nat) term intrp)› and
‹is_valuation I β› and
‹I❙, β ⊨ (φ ⋅⇩f⇩m (subst x t))›
shows ‹I❙, β ⊨ (❙∃x❙. φ)›
proof -
have ‹(λv. ⟦subst x t v⟧⇗I,β⇖) = β(x := ⟦t⟧⇗I,β⇖)›
proof -
have "∀n. ⟦subst x t n⟧⇗I,β⇖ = (β(x := ⟦t⟧⇗I,β⇖)) n"
by (simp add: subst_def)
then show ?thesis
by blast
qed
moreover have ‹⟦t⟧⇗I,β⇖ ∈ dom I›
using assms(1)
proof (induct t)
case (Var x)
then show ?case
using assms(2) by (auto simp: is_valuation_def)
next
case (Fun f ts)
then have ‹u ∈ set ts ⟹ ⟦u⟧⇗I,β⇖ ∈ dom I› for u
by (smt (verit) UN_I Un_iff fst_conv funas_term.simps(2) is_interpretation_def list.set_map)
then show ?case
using eval.simps(2) fst_conv imageE length_map list.set_map list_all_set assms(2)
unfolding is_valuation_def
by (smt (verit, best) Fun.prems Un_insert_left funas_term.simps(2) insert_iff
is_interpretation_def subsetI)
qed
ultimately have ‹∃a ∈ dom I. I❙, β(x := a) ⊨ φ›
using assms(3) swap_subst_eval[of I β φ "subst x t"] by auto
then show ?thesis
using holds_exists by blast
qed
definition skolem1 :: "nat ⇒ nat ⇒ form ⇒ form" where
‹skolem1 f x φ = φ ⋅⇩f⇩m (subst x (Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))))›
lemma fvt_var_x_simp:
‹FVT (Var x ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV φ - {x}))))) = FV φ - {x}›
proof -
have remove_list:
‹set (map Var (sorted_list_of_set (FV φ - {x}))) = Var ` (FV φ - {x})›
using set_map set_sorted_list_of_set using finite_FV by auto
have ‹FVT (Var x ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV φ - {x}))))) =
FVT (Fun f (map Var (sorted_list_of_set (FV φ - {x}))))›
by simp
also have ‹... = ⋃ (FVT ` set (map Var (sorted_list_of_set (FV φ - {x}))))›
using term.set(4) by metis
also have ‹... = ⋃ (FVT ` Var ` (FV φ - {x}))›
using remove_list by auto
also have ‹... = FV φ - {x}›
by force
finally show ?thesis .
qed
lemma holds_indep_intrp_if2:
fixes I I' :: "'a intrp"
shows
‹⟦I❙,β ⊨ φ; dom I = dom I'; ⋀p. intrp_rel I p = intrp_rel I' p;
⋀f zs. (f, length zs) ∈ functions_form φ ⟹ intrp_fn I f zs = intrp_fn I' f zs⟧ ⟹
I'❙,β ⊨ φ›
using holds_indep_intrp_if by blast
lemma fun_upds_prop: ‹length xs = length zs ⟹ ∀z∈set zs. P z ⟹ ∀v. P (g v) ⟹ ∀v. P ((foldr (λkv f. fun_upd f (fst kv) (snd kv)) (zip xs zs) g) v)›
proof (induction zs arbitrary: xs g)
case Nil
then show ?case
by simp
next
case (Cons a zs)
obtain x xsp where xs_is: ‹xs = x # xsp›
using Cons(2) by (metis length_Suc_conv)
with Cons show ?case
by auto
qed
lemma ‹{z. ∃y. y ∈ FV φ ∧ z ∈ functions_term (Var y ⋅ subst x t)} = functions_term t ∨
{z. ∃y. y ∈ FV φ ∧ z ∈ functions_term (Var y ⋅ subst x t)} = {}›
proof -
have ‹y ≠ x ⟹ functions_term (Var y ⋅ subst x t) = {}› for y
by (simp add: subst_def)
moreover have ‹y = x ⟹ functions_term (Var y ⋅ subst x t) = functions_term t› for y
by simp
ultimately show ?thesis
by blast
qed
lemma func_form_subst: ‹x ∈ FV φ ⟹ (f, length ts) ∈ functions_form (φ ⋅⇩f⇩m subst x (Fun f ts))›
proof (induction φ rule: functions_form.induct)
case 1
then show ?case by simp
next
case (2 p ts)
then show ?case
by (metis (no_types, lifting) UnCI eval_term.simps(1) formsubst_functions_form
funas_term.simps(2) mem_Collect_eq singletonI subst_simps(1))
next
case (3 φ ψ)
then show ?case
by auto
next
case (4 y φ)
then show ?case
by (metis (no_types, lifting) UnI2 Un_commute eval_term.simps(1) formsubst_functions_form
funas_term.simps(2) mem_Collect_eq singletonI subst_simps(1))
qed
lemma holds_formsubst:
"M❙,β ⊨ (p ⋅⇩f⇩m i) ⟷ M❙,(λt. ⟦t⟧⇗M,β⇖) ∘ i ⊨ p"
by (simp add: holds_indep_β_if swap_subst_eval)
lemma holds_formsubst1:
"M❙,β ⊨ (p ⋅⇩f⇩m Var(x:=t)) ⟷ M❙,β(x := ⟦t⟧⇗M,β⇖) ⊨ p"
by (simp add: holds_indep_β_if swap_subst_eval)
lemma holds_formsubst2:
"M❙,β ⊨ (p ⋅⇩f⇩m subst x t) ⟷ M❙,β(x := ⟦t⟧⇗M,β⇖) ⊨ p"
by (simp add: holds_formsubst1 subst_def)
lemma size_nonzero [simp]: "size fm > 0"
by (induction fm) auto
lemma
assumes prenex_ex_phi: ‹is_prenex (❙∃x❙. φ)›
and notin_ff: ‹¬ (f, card (FV (❙∃x❙. φ))) ∈ functions_form (❙∃x❙. φ)›
shows holds_skolem1a: "is_prenex (skolem1 f x φ)" (is "?A")
and holds_skolem1b: "FV (skolem1 f x φ) = FV (❙∃x❙. φ)" (is "?B")
and holds_skolem1c:
"Prenex_Normal_Form.size (skolem1 f x φ) < Prenex_Normal_Form.size (❙∃x❙. φ)" (is "?C")
and holds_skolem1d: "predicates_form (skolem1 f x φ) = predicates_form (❙∃x❙. φ)" (is "?D")
and holds_skolem1e: "functions_form (❙∃x❙. φ) ⊆ functions_form (skolem1 f x φ)" (is "?E")
and holds_skolem1f: "functions_form (skolem1 f x φ)
⊆ (f, card (FV (❙∃x❙. φ))) ▹ functions_form (❙∃x❙. φ)" (is "?F")
proof -
show ?A
by (metis form.inject(2) form.inject(3) prenex_ex_phi prenex_formsubst prenex_imp
qfree_no_quantif skolem1_def)
show ?B
proof
show ‹FV (skolem1 f x φ) ⊆ FV (❙∃x❙. φ)›
proof
fix z
assume ‹z ∈ FV (skolem1 f x φ)›
then obtain y where y_in: ‹y ∈ FV φ› and
z_in: ‹z ∈ FVT (Var y ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV φ - {x})))))›
unfolding skolem1_def using formsubst_fv FV_exists by auto
then have neq_x: ‹y ≠ x ⟹ z ∈ FV φ - {x}›
by (simp add: subst_def)
then show ‹z ∈ FV (❙∃x❙. φ)›
using fvt_var_x_simp z_in by force
qed
next
show ‹FV (❙∃x❙. φ) ⊆ FV (skolem1 f x φ)›
proof
fix z
assume z_in: ‹z ∈ FV (❙∃x❙. φ)›
then have ‹FVT (Var z ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ)))))) = {z}›
by (simp add: subst_def)
then show ‹z ∈ FV (skolem1 f x φ)›
unfolding skolem1_def using z_in formsubst_fv by auto
qed
qed
show ?C
by (simp add: size_indep_subst skolem1_def)
show ?D
by (simp add: formsubst_predicates skolem1_def)
show ?E
by (simp add: formsubst_functions_form skolem1_def)
show ?F
proof
fix g
assume g_in: ‹g ∈ functions_form (skolem1 f x φ)›
then have ‹g ∈ functions_form φ ∪ {g. ∃y. y ∈ FV φ ∧
g ∈ functions_term (Var y ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ)))))))}›
unfolding skolem1_def using formsubst_functions_form
by blast
moreover have ‹{g. ∃y ∈ FV φ.
g ∈ functions_term (Var y ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ)))))))}
⊆ (f, card (FV (❙∃x❙. φ))) ▹ functions_form φ›
proof
fix h
assume ‹h ∈ {g. ∃y ∈ FV φ. g ∈ functions_term (Var y ⋅ subst x (Fun f (map Var
(sorted_list_of_set (FV ((❙∃x❙. φ)))))))}›
then obtain y where y_in: ‹y ∈ FV φ› and h_in:
‹h ∈ functions_term (Var y ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ)))))))›
by blast
then have y_neq_x_case: ‹y ≠ x ⟹ h ∈ functions_form φ›
by (simp add: subst_def)
have ‹functions_term (Var x ⋅ subst x (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ))))))) =
functions_term (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ))))))›
by (simp add: subst_def)
have ‹functions_term (Fun f (map Var (sorted_list_of_set (FV ((❙∃x❙. φ)))))) =
{(f, card (FV (❙∃x❙. φ)))}›
by auto
then have y_eq_x_case: ‹y = x ⟹ h = (f, card (FV (❙∃x❙. φ)))›
using y_in h_in by auto
show ‹h ∈ (f, card (FV (❙∃x❙. φ))) ▹ functions_form φ›
using y_neq_x_case y_eq_x_case by blast
qed
ultimately show ‹g ∈ (f, card (FV (❙∃x❙. φ))) ▹ functions_form (❙∃x❙. φ)›
by auto
qed
qed
definition "define_fn ≡ λFN f n h. λg zs. if g=f ∧ length zs = n then h zs else FN g zs"
lemma holds_skolem1g:
assumes prenex_ex_phi: ‹is_prenex (❙∃x❙. φ)›
and notin_ff: ‹¬ (f, card (FV (❙∃x❙. φ))) ∈ functions_form (❙∃x❙. φ)›
fixes I :: "'a intrp"
assumes interp_I: "is_interpretation (language {φ}) I"
and nempty_I: "dom I ≠ {}"
and valid: "⋀β. is_valuation I β ⟹ I❙,β ⊨ (❙∃x❙. φ)"
obtains M where "dom M = dom I"
"intrp_rel M = intrp_rel I"
"⋀g zs. g ≠ f ∨ length zs ≠ card (FV (❙∃x❙. φ)) ⟹ intrp_fn M g zs = intrp_fn I g zs"
"is_interpretation (language {skolem1 f x φ}) M"
"⋀β. is_valuation M β ⟹ M❙,β ⊨ skolem1 f x φ"
proof -
have ex_a_mod_phi: "∃a∈dom I. I❙,β(x := a) ⊨ φ"
if "∀v. β v ∈ dom I" for β
using that FOL_Semantics.holds_exists is_valuation_def valid by blast
define intrp_f where
‹intrp_f ≡ λzs. foldr (λkv f. fun_upd f (fst kv) (snd kv))
(zip (sorted_list_of_set (FV (❙∃x❙. φ))) zs) (λz. SOME c. c ∈ dom I)›
define thex where "thex ≡ λzs. SOME a. a ∈ dom I ∧ (I❙, (intrp_f zs)(x:=a) ⊨ φ)"
define FN where "FN ≡ define_fn (intrp_fn I) f (card (FV (❙∃x❙. φ))) thex"
define M :: "'a intrp" where ‹M = Abs_intrp (dom I, FN, intrp_rel I)›
show ?thesis
proof
show dom_M_I_eq: ‹dom M = dom I›
unfolding M_def by simp
show intrp_rel_eq: ‹intrp_rel M = intrp_rel I›
unfolding M_def by simp
show intrp_fn_eq: "⋀g zs. g ≠ f ∨ length zs ≠ card (FV (❙∃x❙. φ)) ⟹
intrp_fn M g zs = intrp_fn I g zs"
unfolding M_def FN_def define_fn_def
by fastforce
have in_dom_I: ‹intrp_fn M f zs ∈ dom I›
if len_eq: ‹length zs = card (FV φ - {x})› and zs_in: ‹set zs ⊆ dom M›
for zs
proof -
have len_eq2: ‹length (sorted_list_of_set (FV (❙∃x❙. φ))) = length zs›
using len_eq by simp
have zs_in2: ‹∀z∈set zs. z ∈ dom I›
using dom_M_I_eq zs_in by force
have fn_is_thex: ‹(intrp_fn M) f zs = thex zs›
using len_eq by (auto simp: M_def FN_def define_fn_def)
have ‹∀v. (intrp_f zs) v ∈ dom I›
using fun_upds_prop[OF len_eq2 zs_in2] nempty_I some_in_eq unfolding intrp_f_def
by (metis (mono_tags))
then show ‹intrp_fn M f zs ∈ dom I›
using nempty_I ex_a_mod_phi interp_I unfolding is_interpretation_def
by (metis (mono_tags, lifting) fn_is_thex someI_ex thex_def)
qed
show ‹is_interpretation (language {skolem1 f x φ}) M›
unfolding is_interpretation_def
proof (intro strip)
fix g l
assume §: ‹(g, length l) ∈ fst (language {skolem1 f x φ}) ∧ set l ⊆ dom M›
then have ‹(g, length l) ∈ fst (language {φ}) ∨ (g, length l) = (f, card (FV φ - {x}))›
using holds_skolem1f lang_singleton notin_ff prenex_ex_phi by auto
with § show ‹intrp_fn M g l ∈ dom M›
by (metis FV_exists dom_M_I_eq in_dom_I interp_I intrp_fn_eq is_interpretation_def prod.inject)
qed
show "M❙,β ⊨ skolem1 f x φ" if "is_valuation M β" for β
proof -
have "M❙,β(x:=thex (map β (sorted_list_of_set(FV(❙∃x❙. φ))))) ⊨ φ"
proof (rule holds_indep_intrp_if2)
have "I❙, (intrp_f (map β (sorted_list_of_set(FV(❙∃x❙. φ)))))(x:=a) ⊨ φ ⟷ I❙, β(x:=a) ⊨ φ"
for a
proof (intro holds_indep_β_if strip)
fix v
assume "v ∈ FV φ"
then have "v=x ∨ v ∈ FV (❙∃x❙. φ)"
using FV_exists by blast
moreover have
"foldr (λkv f. f(fst kv := snd kv)) (zip vs (map β vs)) (λz. SOME c. c ∈ dom I) w = β w"
if "w ∈ set vs" "set vs ⊆ FV (❙∃x❙. φ)" for vs w
using that by (induction vs) auto
ultimately
show "((intrp_f (map β (sorted_list_of_set (FV (❙∃x❙. φ))))) (x := a)) v = (β(x := a)) v"
using finite_FV intrp_f_def by auto
qed
then show "I❙,β (x := thex (map β (sorted_list_of_set (FV (❙∃x❙. φ))))) ⊨ φ"
by (metis (mono_tags, lifting) dom_M_I_eq ex_a_mod_phi is_valuation_def that thex_def
verit_sko_ex')
show "dom I = dom M"
using dom_M_I_eq by auto
show "⋀p. intrp_rel I p = intrp_rel M p"
using intrp_rel_eq by auto
show "⋀f zs. (f, length zs) ∈ functions_form φ ⟹ intrp_fn I f zs = intrp_fn M f zs"
using functions_form.simps notin_ff intrp_fn_eq
by (metis sup_bot.right_neutral)
qed
moreover have "FN f (map β (sorted_list_of_set (FV φ - {x}))) =
thex (map β (sorted_list_of_set (FV φ - {x})))"
by (simp add: FN_def define_fn_def)
ultimately show ?thesis
by (simp add: holds_formsubst2 skolem1_def M_def o_def)
qed
qed
qed
lemma holds_skolem1h:
assumes prenex_ex_phi: ‹is_prenex (❙∃x❙. φ)› and ‹¬ (f, card (FV (❙∃x❙. φ))) ∈ functions_form (❙∃x❙. φ)›
assumes is_intrp: "is_interpretation (language {skolem1 f x φ}) N"
and nempty_N: "dom N ≠ {}"
and is_val: "is_valuation N β"
and skol_holds: "N❙,β ⊨ skolem1 f x φ"
shows "N❙,β ⊨ (❙∃x❙. φ)"
proof -
have ‹∃a∈dom N. N❙,β(x := a) ⊨ φ›
proof -
have ‹N❙,(λv. ⟦subst x (Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))) v⟧⇗N,β⇖) ⊨ φ›
by (metis skol_holds skolem1_def swap_subst_eval)
then have holds_eval_f: ‹N❙,β(x := ⟦Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))⟧⇗N,β⇖) ⊨ φ›
by (smt (verit, best) eval.simps(1) fun_upd_other fun_upd_same holds_indep_β_if subst_def)
show ‹∃a∈dom N. N❙,β(x := a) ⊨ φ›
proof (cases ‹x ∈ FV φ›)
case True
have eval_to_intrp: ‹⟦Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))⟧⇗N,β⇖ =
intrp_fn N f [⟦t⟧⇗N,β⇖. t ← map Var (sorted_list_of_set (FV (❙∃x❙. φ)))]›
by simp
have ‹[⟦t⟧⇗N,β⇖. t ← map Var (sorted_list_of_set (FV (❙∃x❙. φ)))] =
[β t. t ← (sorted_list_of_set (FV (❙∃x❙. φ)))]›
by auto
then have all_in_dom: ‹set [⟦t⟧⇗N,β⇖. t ← map Var (sorted_list_of_set (FV (❙∃x❙. φ)))] ⊆ dom N›
using is_val by (auto simp: is_valuation_def)
have ‹(f, length [⟦t⟧⇗N,β⇖. t ← map Var (sorted_list_of_set (FV (❙∃x❙. φ)))]) ∈
functions_form (φ ⋅⇩f⇩m subst x (Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))))›
using func_form_subst[OF True] is_intrp lang_singleton
unfolding skolem1_def is_interpretation_def by (metis length_map)
then have ‹⟦Fun f (map Var (sorted_list_of_set (FV (❙∃x❙. φ))))⟧⇗N,β⇖ ∈ dom N›
using is_intrp eval_to_intrp all_in_dom unfolding is_interpretation_def skolem1_def
by (metis fst_conv lang_singleton)
then show ?thesis
using holds_eval_f by blast
next
case False
obtain a where a_in: ‹a ∈ dom N›
using nempty_N by blast
then have ‹N❙,β(x := a) ⊨ φ›
using holds_eval_f False by (metis fun_upd_other holds_indep_β_if)
then show ?thesis
using a_in by blast
qed
qed
then show ?thesis
by simp
qed
lemma holds_skolem1:
assumes ‹is_prenex (❙∃x❙. φ)› and ‹¬ (f, card (FV (❙∃x❙. φ))) ∈ functions_form (❙∃x❙. φ)›
shows ‹is_prenex (skolem1 f x φ) ∧
FV (skolem1 f x φ) = FV (❙∃x❙. φ) ∧
size (skolem1 f x φ) < size (❙∃x❙. φ) ∧
predicates_form (skolem1 f x φ) = predicates_form (❙∃x❙. φ) ∧
functions_form (❙∃x❙. φ) ⊆ functions_form (skolem1 f x φ) ∧
functions_form (skolem1 f x φ) ⊆ insert (f, card (FV (❙∃x❙. φ))) (functions_form (❙∃x❙. φ)) ∧
(∀(I :: 'a intrp). is_interpretation (language {φ}) I ∧
¬ (dom I = {}) ∧
(∀β. is_valuation I β ⟶ (I❙, β ⊨ (❙∃x❙. φ))) ⟶
(∃(M :: 'a intrp). dom M = dom I ∧
intrp_rel M = intrp_rel I ∧
(∀g zs. ¬g=f ∨ ¬(length zs = card (FV (❙∃x❙. φ))) ⟶ intrp_fn M g zs = intrp_fn I g zs) ∧
is_interpretation (language {skolem1 f x φ}) M ∧
(∀β. is_valuation M β ⟶ (M❙, β ⊨ (skolem1 f x φ))))) ∧
(∀(N :: 'a intrp). is_interpretation (language {skolem1 f x φ}) N ∧
¬ (dom N = {}) ⟶
(∀β. is_valuation N β ∧ (N❙, β ⊨ (skolem1 f x φ)) ⟶ (N❙, β ⊨ (❙∃x❙. φ))))
›
by (smt (verit, ccfv_SIG) assms holds_skolem1a holds_skolem1b holds_skolem1c holds_skolem1d
holds_skolem1e holds_skolem1f holds_skolem1g holds_skolem1h)
lemma skolems_ex: ‹∃skolems. ∀φ. skolems φ = (λk. ppat (λx ψ. ❙∀x❙. (skolems ψ k))
(λx ψ. skolems (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ)›
proof (intro size_rec strip)
fix skolems :: "form ⇒ nat ⇒ form" and g φ
assume IH: ‹∀z. size z < size φ ⟶ skolems z = g z›
show "(λk.
ppat (λx ψ. ❙∀ x❙. skolems ψ k) (λx ψ. skolems (skolem1 (numpair J k) x ψ) (Suc k))(λψ. ψ) φ) =
(λk. ppat (λx ψ. ❙∀ x❙. g ψ k) (λx ψ. g (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ)"
proof (cases "∃x φ'. φ = ❙∀x❙. φ'")
case True
then obtain x φ' where phi_is: "φ = ❙∀x❙. φ'"
by blast
then have smaller: ‹size (φ' ⋅⇩f⇩m σ) < size φ› for σ
using size_indep_subst by simp
have ppat_to_skol: ‹(ppat (λx ψ. ❙∀x❙. (skolems ψ k))
(λx ψ. skolems (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ) = (❙∀x❙. skolems φ' k)› for k
unfolding ppat_def by (simp add: phi_is)
have skol_to_g: ‹(❙∀x❙. skolems φ' k) = (❙∀ x❙. g φ' k)› for k
using IH smaller by (simp add: phi_is)
have g_to_ppat: ‹(❙∀ x❙. g φ' k) =
ppat (λx ψ. ❙∀ x❙. g ψ k) (λx ψ. g (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ› for k
unfolding ppat_def using phi_is by simp
show ?thesis
using ppat_to_skol skol_to_g g_to_ppat by auto
next
case False
assume falseAll: ‹¬(∃x φ'. φ = ❙∀ x❙. φ')›
then show ?thesis
proof (cases "∃x φ'. φ = ❙∃x❙. φ'")
case True
then obtain x φ' where phi_is: "φ = ❙∃x❙. φ'"
by blast
then have smaller: ‹size (φ' ⋅⇩f⇩m σ) < size φ› for σ
using size_indep_subst by simp
have ppat_to_skol: ‹(ppat (λx ψ. ❙∀x❙. (skolems ψ k))
(λx ψ. skolems (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ) =
skolems (skolem1 (numpair J k) x φ') (Suc k)› for k
unfolding ppat_def using phi_is by simp
have skol_to_g: ‹skolems (skolem1 (numpair J k) x φ') (Suc k) =
g (skolem1 (numpair J k) x φ') (Suc k)› for k
using IH smaller phi_is by (simp add: skolem1_def)
have g_to_ppat: ‹g (skolem1 (numpair J k) x φ') (Suc k) =
ppat (λx ψ. ❙∀ x❙. g ψ k) (λx ψ. g (skolem1 (numpair J k) x ψ) (Suc k)) (λψ. ψ) φ› for k
unfolding ppat_def using phi_is by simp
show ?thesis
using ppat_to_skol skol_to_g g_to_ppat by simp
next
case False
then show ?thesis
using falseAll ppat_last unfolding ppat_def by auto
qed
qed
qed
consts skolems :: "nat ⇒ form ⇒ nat ⇒ form"
specification (skolems)
skolems_eq: ‹⋀J ψ k. skolems J ψ k
= ppat (λx φ'. ❙∀x❙. (skolems J φ' k)) (λx φ'. skolems J (skolem1 (numpair J k) x φ') (Suc k)) (λφ. φ) ψ›
using skolems_ex by meson
text ‹bounding the possible Skolem functions in a given formula›
definition "skolems_bounded ≡ λp J k. ∀l m. (numpair J l, m) ∈ functions_form p ⟶ l < k"
lemma skolems_bounded_mono: "⟦skolems_bounded p J k'; k'≤k⟧ ⟹ skolems_bounded p J k"
by (meson dual_order.strict_trans1 skolems_bounded_def)
lemma skolems_bounded_prenex: "skolems_bounded φ K k ⟹ skolems_bounded (prenex φ) K k"
unfolding skolems_bounded_def
by (metis Pair_inject lang_singleton prenex_props)
text ‹Basic properties proved by induction on the number of Skolemisation steps.
Harrison's gigantic conjunction broken up for more manageable proofs, at the cost of some repetition›
text ‹first, the simplest properties›
lemma holds_skolems_induction_A:
assumes "size p = n" and "is_prenex p" and "skolems_bounded p J k"
shows "universal(skolems J p k) ∧
FV(skolems J p k) = FV p ∧
predicates_form (skolems J p k) = predicates_form p ∧
functions_form p ⊆ functions_form (skolems J p k) ∧
functions_form (skolems J p k) ⊆ {(numpair J l,m) | l m. k ≤ l} ∪ functions_form p"
using assms
proof (induction n arbitrary: k p rule: less_induct)
case (less n)
show ?case
using ‹is_prenex p›
proof cases
case 1
then show ?thesis
by (metis (no_types, lifting) ppat_last_qfree skolems_eq universal.simps UnCI subsetI)
next
case (2 φ x)
then have smaller: "Prenex_Normal_Form.size φ < n" and skbo: "skolems_bounded φ J k"
using less.prems by (auto simp add: skolems_bounded_def)
have skoeq: "skolems J p k = (❙∀ x❙. skolems J φ k)"
by (metis "2"(1) ppat_simpA skolems_eq)
show ?thesis
using less.IH [OF smaller refl ‹is_prenex φ›, of k] skoeq
by (simp add: 2 is_valuation_def lang_singleton skbo)
next
case (3 φ x)
define φ' where "φ' ≡ skolem1 (numpair J k) x φ"
have smaller: "Prenex_Normal_Form.size φ' < n"
and pair_notin_ff: "(numpair J k, card (FV (❙∃x❙. φ))) ∉ functions_form (❙∃x❙. φ)"
using 3 holds_skolem1c less.prems unfolding φ'_def skolems_bounded_def by blast+
have pre: "is_prenex φ'"
using "3"(1) pair_notin_ff holds_skolem1a ‹is_prenex p› φ'_def by blast
define φ'' where "φ'' ≡ skolems J φ' (Suc k)"
have skos: "skolems J (❙∃x❙. φ) k = φ''"
by (metis φ'_def φ''_def ppat_simpB skolems_eq)
have funsub: "functions_form p ⊆ functions_form φ'"
"functions_form φ' ⊆ insert (numpair J k, card (FV (❙∃x❙. φ))) (functions_form p)"
using "3"(1) pair_notin_ff φ'_def holds_skolem1e holds_skolem1f ‹is_prenex p› by presburger+
have skbo: "skolems_bounded φ' J (Suc k)"
using ‹skolems_bounded p J k› unfolding skolems_bounded_def less_Suc_eq
using funsub(2) by fastforce
have FV: "FV φ' = FV φ - {x}"
using "3"(1) pair_notin_ff holds_skolem1b ‹is_prenex p› φ'_def by auto
have preq: "predicates_form φ' = predicates_form φ"
using φ'_def formsubst_predicates skolem1_def by presburger
show ?thesis
using less.IH [OF smaller refl pre, of "Suc k"] skolems_eq [of J p] FV funsub 3
by (force simp: preq skbo ppat_simpB simp flip: φ'_def)
qed
qed
text ‹the final conjunct of the HOL Light version›
lemma holds_skolems_induction_B:
fixes N :: "'a intrp"
assumes "size p = n" and "is_prenex p" and "skolems_bounded p J k"
and "is_interpretation (language {skolems J p k}) N" "dom N ≠ {}"
and "is_valuation N β" "N❙,β ⊨ skolems J p k"
shows "N❙,β ⊨ p"
using assms
proof (induction n arbitrary: N k p β rule: less_induct)
case (less n)
show ?case
using ‹is_prenex p›
proof cases
case 1
with less show ?thesis
by (metis (no_types, lifting) ppat_last_qfree skolems_eq)
next
case (2 φ x)
then have smaller: "Prenex_Normal_Form.size φ < n" and skbo: "skolems_bounded φ J k"
using less.prems by (auto simp add: skolems_bounded_def)
have "skolems J p k = (❙∀ x❙. skolems J φ k)"
by (metis "2"(1) ppat_simpA skolems_eq)
then show ?thesis
using less.IH [OF smaller refl ‹is_prenex φ›, of k] less.prems
by (simp add: lang_singleton skbo valuation_valmod 2)
next
case (3 φ x)
define φ' where "φ' ≡ skolem1 (numpair J k) x φ"
have smaller: "Prenex_Normal_Form.size φ' < n"
and pair_notin_ff: "(numpair J k, card (FV (❙∃x❙. φ))) ∉ functions_form (❙∃x❙. φ)"
using 3 holds_skolem1c less.prems unfolding φ'_def skolems_bounded_def by blast+
have pre: "is_prenex φ'"
using "3"(1) pair_notin_ff holds_skolem1a ‹is_prenex p› φ'_def by blast
define φ'' where "φ'' ≡ skolems J φ' (Suc k)"
have skos: "skolems J (❙∃x❙. φ) k = φ''"
by (metis φ'_def φ''_def ppat_simpB skolems_eq)
have "functions_form φ' ⊆ insert (numpair J k, card (FV (❙∃x❙. φ))) (functions_form p)"
using "3"(1) pair_notin_ff φ'_def holds_skolem1f ‹is_prenex p› by presburger
then have skbo: "skolems_bounded φ' J (Suc k)"
using ‹skolems_bounded p J k› unfolding skolems_bounded_def less_Suc_eq by fastforce
have prex: "is_prenex (❙∃x❙. φ)"
using 3 ‹is_prenex p› by blast
have "functions_form (skolem1 (numpair J k) x φ) ⊆ functions_form (skolems J φ' (Suc k))"
using φ'_def holds_skolems_induction_A pre skbo by blast
then show ?thesis
using less.IH [OF smaller refl pre, of "Suc k"] less.prems skolems_eq [of J p]
apply (simp add: skbo ppat_simpB 3)
using holds_skolem1h [of x φ "numpair J k"] pair_notin_ff ‹is_prenex φ'›
by (metis prex φ'_def holds_exists interpretation_sublanguage lang_singleton)
qed
qed
text ‹the penultimate conjunct of the HOL Light version›
lemma holds_skolems_induction_C:
fixes M :: "'a intrp"
assumes "size p = n" and "is_prenex p" and "skolems_bounded p J k"
and "is_interpretation (language {p}) M" "dom M ≠ {}" "satisfies M {p}"
shows "∃M'. dom M' = dom M ∧ intrp_rel M' = intrp_rel M ∧
(∀g zs. intrp_fn M' g zs ≠ intrp_fn M g zs
⟶ (∃l. k ≤ l ∧ g = numpair J l)) ∧
is_interpretation (language {skolems J p k}) M' ∧
satisfies M' {skolems J p k}"
using assms
proof (induction n arbitrary: M k p rule: less_induct)
case (less n)
show ?case
using ‹is_prenex p›
proof cases
case 1
with less show ?thesis
by (metis (no_types, lifting) ppat_last_qfree skolems_eq)
next
case (2 φ x)
then have smaller: "Prenex_Normal_Form.size φ < n" and skbo: "skolems_bounded φ J k"
using less.prems by (auto simp add: skolems_bounded_def)
have skoeq: "skolems J p k = (❙∀ x❙. skolems J φ k)"
by (metis "2"(1) ppat_simpA skolems_eq)
show ?thesis
using less.IH [OF smaller refl ‹is_prenex φ›, of k M] skoeq less.prems
apply (simp add: skbo 2 lang_singleton satisfies_def)
by (metis fun_upd_triv is_valuation_def valuation_valmod)
next
case (3 φ x)
define φ' where "φ' ≡ skolem1 (numpair J k) x φ"
have smaller: "Prenex_Normal_Form.size φ' < n"
and pair_notin_ff: "(numpair J k, card (FV (❙∃x❙. φ))) ∉ functions_form (❙∃x❙. φ)"
using 3 holds_skolem1c less.prems unfolding φ'_def skolems_bounded_def by blast+
have pre: "is_prenex φ'"
using "3"(1) pair_notin_ff holds_skolem1a ‹is_prenex p› φ'_def by blast
define φ'' where "φ'' ≡ skolems J φ' (Suc k)"
have skos: "skolems J (❙∃x❙. φ) k = φ''"
by (metis φ'_def φ''_def ppat_simpB skolems_eq)
have "functions_form φ' ⊆ insert (numpair J k, card (FV (❙∃x❙. φ))) (functions_form p)"
using "3"(1) pair_notin_ff φ'_def holds_skolem1f ‹is_prenex p› by presburger
then have skbo: "skolems_bounded φ' J (Suc k)"
unfolding skolems_bounded_def less_Suc_eq
by (meson insert_iff less.prems(3) old.prod.inject prod_encode_eq skolems_bounded_def subsetD)
have prex: "is_prenex (❙∃x❙. φ)"
using "3"(1) ‹is_prenex p› by blast
have **: "∃M'. dom M' = dom M ∧ intrp_rel M' = intrp_rel M
∧ (∀g. (∃zs. intrp_fn M' g zs ≠ intrp_fn M g zs) ⟶ (∃l≥k. g = numpair J l))
∧ is_interpretation (language {skolems J φ' (Suc k)}) M'
∧ satisfies M' {skolems J φ' (Suc k)}"
if "is_interpretation (language {(❙∃x❙. φ)}) M"
and "dom M ≠ {}"
and M_extend: "⋀β. is_valuation M β ⟹ (∃a ∈ dom M. M❙, β(x:=a) ⊨ φ)"
for M :: "'a intrp"
proof -
have M: "is_interpretation (language {φ}) M"
using lang_singleton that(1) by auto
with that show ?thesis
using less.IH[OF smaller refl ‹is_prenex φ'› skbo]
using holds_skolem1g [OF prex pair_notin_ff M] holds_exists
by (smt (verit) φ'_def nat_le_linear not_less_eq_eq satisfies_def singleton_iff)
qed
show ?thesis
using less.IH [OF smaller refl pre, of "Suc k"] less.prems skolems_eq [of J p] **
by (simp add: skbo ppat_simpB 3 φ'_def satisfies_def)
qed
qed
corollary holds_skolems_prenex_A:
assumes "is_prenex φ" "skolems_bounded φ K 0"
shows "universal(skolems K φ 0) ∧ (FV (skolems K φ 0) = FV φ) ∧
predicates_form (skolems K φ 0) = predicates_form φ ∧
functions_form φ ⊆ functions_form (skolems K φ 0) ∧
functions_form (skolems K φ 0) ⊆ {(numpair K l,m) | l m. True} ∪ (functions_form φ)"
using holds_skolems_induction_A [OF refl assms] by simp
corollary holds_skolems_prenex_B:
assumes "is_prenex φ" "skolems_bounded φ K 0"
and "is_interpretation (language {skolems K φ 0}) M" "dom M ≠ {}"
and "is_valuation M β" "M❙,β ⊨ skolems K φ 0"
shows "M❙,β ⊨ φ"
using holds_skolems_induction_B [OF refl assms] by simp
corollary holds_skolems_prenex_C:
assumes "is_prenex φ" "skolems_bounded φ K 0"
and "is_interpretation (language {φ}) M" "dom M ≠ {}" "satisfies M {φ}"
shows "∃M'. dom M' = dom M ∧ intrp_rel M' = intrp_rel M ∧
(∀g zs. intrp_fn M' g zs ≠ intrp_fn M g zs ⟶ (∃l. g = numpair K l)) ∧
is_interpretation (language {skolems K φ 0}) M' ∧
satisfies M' {skolems K φ 0}"
using holds_skolems_induction_C [OF refl assms] by simp
definition skopre where
‹skopre k φ = skolems k (prenex φ) 0›
corollary skopre_model_A:
assumes "skolems_bounded φ K 0"
shows "universal(skopre K φ) ∧ (FV (skopre K φ) = FV φ) ∧
predicates_form (skopre K φ) = predicates_form φ ∧
functions_form φ ⊆ functions_form (skopre K φ) ∧
functions_form (skopre K φ) ⊆ {(numpair K l,m) | l m. True} ∪ (functions_form φ)"
using skolems_bounded_prenex holds_skolems_prenex_A
by (metis (no_types, lifting) Pair_inject assms lang_singleton prenex_props skopre_def)
corollary skopre_model_B:
assumes "skolems_bounded φ K 0"
and "is_interpretation (language {skopre K φ}) M" "dom M ≠ {}"
and "is_valuation M β" "M❙,β ⊨ skopre K φ"
shows "M❙,β ⊨ φ"
using skolems_bounded_prenex holds_skolems_prenex_B
by (metis assms prenex_props skopre_def)
corollary skopre_model_C:
assumes "skolems_bounded φ K 0"
and "is_interpretation (language {φ}) M" "dom M ≠ {}" "satisfies M {φ}"
shows "∃M'. dom M' = dom M ∧ intrp_rel M' = intrp_rel M ∧
(∀g zs. intrp_fn M' g zs ≠ intrp_fn M g zs ⟶ (∃l. g = numpair K l)) ∧
is_interpretation (language {skopre K φ}) M' ∧
satisfies M' {skopre K φ}"
using holds_skolems_prenex_C skopre_def
by (metis assms prenex_props prenex_satisfies skolems_bounded_prenex)
definition skolemize where
‹skolemize φ = skopre (num_of_form (bump_form φ) + 1) (bump_form φ)›
lemma no_skolems_bump_nterm:
shows "i>0 ⟹ (numpair i l, m) ∉ functions_term (bump_nterm t)"
proof (induction t)
case (Var x)
then show ?case
by auto
next
case (Fun ff ts) then show ?case
by induction auto
qed
lemma no_skolems_bump_form: "i>0 ⟹ skolems_bounded (bump_form φ) i 0"
by (induction φ) (auto simp: skolems_bounded_def no_skolems_bump_nterm)
lemma universal_skolemize [iff]: "universal (skolemize φ)"
and FV_skolemize [simp]: "FV (skolemize φ) = FV (bump_form φ)"
and predicates_form_skolemize [simp]: "predicates_form (skolemize φ) = predicates_form (bump_form φ)"
by (simp_all add: skolemize_def no_skolems_bump_form skopre_model_A)
lemma functions_bump_form: "functions_form (bump_form φ) ⊆ functions_form (skolemize φ)"
by (simp add: skolemize_def no_skolems_bump_form skopre_model_A)
lemma functions_skolemize:
"functions_form (skolemize φ) ⊆ {(numpair (num_of_form (bump_form φ)+1) l, m) |k l m. True} ∪ functions_form (bump_form φ)"
unfolding skolemize_def
using no_skolems_bump_form skopre_model_A by auto
lemma skolemize_imp_holds_bump_form:
assumes "is_interpretation (language {skolemize φ}) N" "dom N ≠ {}"
and "is_valuation N β" "N❙,β ⊨ skolemize φ"
shows "N❙,β ⊨ bump_form φ"
using assms no_skolems_bump_form skolemize_def skopre_model_B by fastforce
lemma is_interpretation_skolemize:
assumes "is_interpretation (language {bump_form φ}) M" "dom M ≠ {}" "satisfies M {bump_form φ}"
obtains M' where "dom M' = dom M" "intrp_rel M' = intrp_rel M"
"⋀g zs. intrp_fn M' g zs ≠ intrp_fn M g zs ⟹ ∃l. g = numpair (num_of_form (bump_form φ) + 1) l"
"is_interpretation (language {skolemize φ}) M'" "satisfies M' {skolemize φ}"
by (metis add_gr_0 assms no_skolems_bump_form skolemize_def skopre_model_C zero_less_one)
lemma functions_form_skolemize:
assumes ‹(f,m) ∈ functions_form (skolemize φ)›
obtains k where ‹f = numpair 0 k› ‹(k,m) ∈ functions_form φ› | l where ‹f = numpair (num_of_form (bump_form φ) + 1) l›
using functions_skolemize assms functions_form_bumpform by (fastforce dest: that)
definition skomod1 where
‹skomod1 φ M ≡
if satisfies M {φ}
then (SOME M'. dom M' = dom (bump_intrp M) ∧
intrp_rel M' = intrp_rel (bump_intrp M) ∧
(∀g zs. intrp_fn M' g zs ≠ intrp_fn (bump_intrp M) g zs ⟶
(∃l. g = numpair (num_of_form (bump_form φ) + 1) l)) ∧
is_interpretation (language {skolemize φ}) M' ∧ satisfies M' {skolemize φ})
else (Abs_intrp (dom M, (λg zs. (SOME a. a ∈ dom M)), intrp_rel M))›
lemma skomod1_works:
assumes M: ‹is_interpretation (language {φ}) M› ‹dom M ≠ {}›
shows ‹dom (skomod1 φ M) = dom (bump_intrp M) ∧
intrp_rel (skomod1 φ M) = intrp_rel (bump_intrp M) ∧
is_interpretation (language {skolemize φ}) (skomod1 φ M) ∧
(satisfies M {φ} ⟶
(∀g zs. intrp_fn (skomod1 φ M) g zs ≠ intrp_fn (bump_intrp M) g zs ⟶
(∃l. g = numpair (num_of_form (bump_form φ) + 1) l)) ∧
satisfies (skomod1 φ M) {skolemize φ})›
proof (cases ‹satisfies M {φ}›)
case True
obtain M' where
"dom M' = dom (bump_intrp M)" "intrp_rel M' = intrp_rel (bump_intrp M)"
"⋀g zs. intrp_fn M' g zs ≠ intrp_fn (bump_intrp M) g zs ⟹ ∃l. g = numpair (num_of_form (bump_form φ) + 1) l"
"is_interpretation (language {skolemize φ}) M'" "satisfies M' {skolemize φ}"
proof (rule is_interpretation_skolemize)
show "is_interpretation (language {bump_form φ}) (bump_intrp M)"
by (simp add: assms(1) bumpform_interpretation)
next
show "dom (bump_intrp M) ≠ {}"
by (simp add: assms(2))
next
show "satisfies (bump_intrp M) {bump_form φ}"
by (metis True bump_dom bumpform is_valuation_def satisfies_def singleton_iff)
qed metis
then show ?thesis
apply (simp only: skomod1_def True)
by (smt (verit, del_insts) someI)
next
case False
then show ?thesis
by (simp add: skomod1_def assms bump_intrp_def intrp_is_struct is_interpretation_def some_in_eq)
qed
definition "skomod_FN ≡ λM g zs. if numfst g = 0 then intrp_fn M (numsnd g) zs
else intrp_fn (skomod1 (unbump_form (form_of_num (numfst g - 1))) M) g zs"
definition skomod where
‹skomod M ≡ Abs_intrp (dom M, skomod_FN M, intrp_rel M)›
lemma skomod_interpretation:
assumes ‹is_interpretation (language {φ}) M› ‹dom M ≠ {}›
shows ‹is_interpretation (language {skolemize φ}) (skomod M)›
proof -
have stM: "struct (dom M)"
by (simp add: intrp_is_struct)
have indom: "intrp_fn M f l ∈ dom M"
if "(f, length l) ∈ functions_form φ" and "set l ⊆ dom M" for f l
using assms that by (auto simp: is_interpretation_def lang_singleton)
show ?thesis
proof -
have "intrp_fn (skomod M) f l ∈ dom (skomod M)"
if fl: "(f, length l) ∈ functions_form (skolemize φ)" and "set l ⊆ dom (skomod M)" for f l
proof -
consider (0) k where ‹f = numpair 0 k› ‹(k, length l) ∈ functions_form φ›
| (1) l where ‹f = numpair (num_of_form (bump_form φ) + 1) l›
using functions_form_skolemize [OF fl] by metis
then show ?thesis
proof cases
case 0
with that show ?thesis
by (simp add: stM indom skomod_def skomod_FN_def)
next
case (1 l')
then show ?thesis
using that skomod1_works [OF assms]
by (force simp add: stM indom skomod_def skomod_FN_def lang_singleton is_interpretation_def)
qed
qed
then show ?thesis
by (auto simp: lang_singleton is_interpretation_def)
qed
qed
proposition skomod_works:
assumes ‹is_interpretation (language {φ}) M› ‹dom M ≠ {}›
shows ‹satisfies M {φ} ⟷ satisfies (skomod M) {skolemize φ}›
proof
assume φ: "satisfies M {φ}"
have "Abs_intrp (dom M, skomod_FN M, intrp_rel M)❙, β ⊨ skolemize φ"
if "is_valuation (Abs_intrp (dom M, skomod_FN M, intrp_rel M)) β"
for β :: "nat ⇒ 'a"
proof -
have "is_valuation (skomod1 φ M) β"
by (metis assms bump_dom dom_Abs_is_fst is_valuation_def skomod1_works struct.intro that)
then have "skomod1 φ M❙,β ⊨ skolemize φ"
by (meson φ assms insertCI satisfies_def skomod1_works)
then show ?thesis
proof (rule holds_indep_intrp_if2)
fix f and zs :: "'a list"
assume f: "(f, length zs) ∈ functions_form (skolemize φ)"
show "intrp_fn (skomod1 φ M) f zs = intrp_fn (Abs_intrp (dom M, skomod_FN M, intrp_rel M)) f zs"
using functions_form_skolemize [OF f]
proof cases
case (1 k)
with φ skomod1_works [OF assms] show ?thesis
apply (simp add: skomod_FN_def bump_intrp_def)
by (metis Zero_neq_Suc prod.inject prod_encode_inverse sndI)
qed (simp add: skomod_FN_def)
qed (simp_all add: assms skomod1_works)
qed
then show "satisfies (skomod M) {skolemize φ}"
by (simp add: satisfies_def skomod_def skomod_FN_def)
next
assume φ: "satisfies (skomod M) {skolemize φ}"
have "bump_intrp M❙,β ⊨ bump_form φ" if "is_valuation (bump_intrp M) β" for β :: "nat ⇒ 'a"
proof -
have "skomod M❙,β ⊨ skolemize φ"
using φ that by (simp add: satisfies_def is_valuation_def skomod_def)
with assms that skomod_interpretation [OF assms] skolemize_imp_holds_bump_form
have "skomod M❙,β ⊨ bump_form φ"
by (simp add: is_valuation_def skolemize_imp_holds_bump_form skomod_def)
then show ?thesis
proof (rule holds_indep_intrp_if2)
fix f and zs :: "'a list"
assume f: "(f, length zs) ∈ functions_form (bump_form φ)"
show "intrp_fn (skomod M) f zs = intrp_fn (bump_intrp M) f zs"
using functions_form_bumpform [OF f]
by (auto simp: skomod_FN_def skomod_def)
qed (simp_all add: skomod_def)
qed
then have "satisfies (bump_intrp M) {bump_form φ}"
by (auto simp: satisfies_def)
then show "satisfies M {φ}"
by (metis bump_dom bumpform is_valuation_def satisfies_def singleton_iff)
qed
proposition skolemize_satisfiable:
‹(∃M::'a intrp. dom M ≠ {} ∧ is_interpretation (language S) M ∧
satisfies M S) ⟷
(∃M::'a intrp. dom M ≠ {} ∧ is_interpretation (language (skolemize ` S)) M
∧ satisfies M (skolemize ` S))› (is "?lhs = ?rhs")
proof
assume ?lhs
then obtain M::"'a intrp" where "dom M ≠ {}"
and int: "is_interpretation (language S) M" and sat: "satisfies M S"
by auto
show ?rhs
proof (intro exI conjI)
show "dom (skomod M) ≠ {}"
using ‹dom M ≠ {}› by (simp add: dom_def skomod_def struct_def)
have "intrp_fn (skomod M) f l ∈ dom (skomod M)"
if l: "set l ⊆ dom (skomod M)"
and "φ ∈ S"
and f: "(f, length l) ∈ functions_form (skolemize φ)"
for f l φ
proof -
have "is_interpretation (language {φ}) M"
using ‹φ ∈ S› unfolding lang_singleton
by (metis Sup_upper functions_forms_def image_iff int interpretation_sublanguage language_def)
then have "is_interpretation (language {skolemize φ}) (skomod M)"
by (intro skomod_interpretation ‹dom M ≠ {}›)
then show ?thesis
by (simp add: f is_interpretation_def l lang_singleton)
qed
then show "is_interpretation (language (skolemize ` S)) (skomod M)"
by (auto simp add: is_interpretation_def language_def functions_forms_def)
next
have "skomod M❙,β ⊨ skolemize φ"
if "is_valuation (skomod M) β" and "φ ∈ S" for β φ
proof -
have "is_interpretation (language {φ}) M"
using ‹φ ∈ S› unfolding lang_singleton
by (metis Sup_upper functions_forms_def image_iff int interpretation_sublanguage language_def)
then show ?thesis
using that sat ‹dom M ≠ {}›
by (metis satisfies_def singleton_iff skomod_works)
qed
then show "satisfies (skomod M) (skolemize ` S)"
by (auto simp add: satisfies_def image_iff)
qed
next
assume ?rhs
then obtain M :: "'a intrp" where "dom M ≠ {}"
and int: "is_interpretation (language (skolemize ` S)) M"
and sat: "satisfies M (skolemize ` S)"
by auto
show ?lhs
proof (intro exI conjI)
show "dom (unbump_intrp M) ≠ {}"
using ‹dom M ≠ {}› struct_def by blast
next
have "functions_forms (bump_form ` S) ⊆ functions_forms (skolemize ` S)"
using functions_bump_form functions_forms_def by auto
then have *: "is_interpretation (language (bump_form ` S)) M"
by (metis int interpretation_sublanguage language_def)
have "is_interpretation (language {φ}) (unbump_intrp M)"
if "is_interpretation (language {bump_form φ}) M" for φ
using that
proof (induction φ)
case (Atom p ts)
have **: "(f,k) ∈ Union (set (map functions_term l))
⟹ (numpair 0 f, k) ∈ Union (set (map functions_term (map bump_nterm l)))" for l k f
proof (induction l)
case Nil
then show ?case by simp
next
case (Cons a l)
have "(f,k) ∈ functions_term t ⟹ (numpair 0 f, k) ∈ functions_term (bump_nterm t)" for t
by (induction t) auto
with Cons show ?case
by auto
qed
show ?case
using Atom ** by (auto simp: is_interpretation_def lang_singleton unbump_intrp_def)
qed (auto simp: is_interpretation_def lang_singleton)
with * show "is_interpretation (language S) (unbump_intrp M)"
unfolding is_interpretation_def lang_singleton
by (simp add: language_def functions_forms_def) blast
next
have "unbump_intrp M❙,β ⊨ φ"
if "is_valuation (unbump_intrp M) β" and "φ ∈ S" for β φ
proof -
have "is_interpretation (language {skolemize φ}) M"
using ‹φ ∈ S› unfolding lang_singleton
by (metis Sup_upper functions_forms_def image_eqI int interpretation_sublanguage language_def)
then show ?thesis
using that ‹dom M ≠ {}› sat unfolding satisfies_def
by (metis dom_Abs_is_fst image_eqI intrp_is_struct is_valuation_def
skolemize_imp_holds_bump_form unbump_holds unbump_intrp_def)
qed
then show "satisfies (unbump_intrp M) S"
by (auto simp add: satisfies_def image_iff)
qed
qed
fun specialize :: "form ⇒ form" where
‹specialize ❙⊥ = ❙⊥›
| ‹specialize (Atom p ts) = Atom p ts›
| ‹specialize (φ ❙⟶ ψ) = φ ❙⟶ ψ›
| ‹specialize (❙∀x❙. φ) = specialize φ›
lemma specialize_satisfies:
fixes M :: "'a intrp"
assumes ‹dom M ≠ {}›
shows ‹satisfies M (specialize ` S) ⟷ satisfies M S›
proof -
have "satisfies M {specialize φ} ⟷ satisfies M {φ}" for φ
proof (induction φ)
case (Forall x1 φ)
show ?case
proof
show "satisfies M {specialize (❙∀ x1❙. φ)} ⟹ satisfies M {❙∀ x1❙. φ}"
using Forall by (auto simp: satisfies_def valuation_valmod)
show "satisfies M {specialize (❙∀ x1❙. φ)}" if §: "satisfies M {❙∀ x1❙. φ}"
proof -
have "M❙,β ⊨ specialize φ" if "is_valuation M β" for β
using that § Forall unfolding is_valuation_def satisfies_def singleton_iff
by (metis fun_upd_triv holds.simps(4))
then show ?thesis
by (auto simp: satisfies_def)
qed
qed
qed auto
then show ?thesis
by (auto simp add: satisfies_def)
qed
lemma specialize_qfree: ‹universal φ ⟹ qfree (specialize φ)›
by (induction rule: universal.induct) (auto elim: qfree.elims)
lemma functions_form_specialize [simp]: "functions_form(specialize φ) = functions_form φ"
by (induction φ) auto
lemma predicates_form_form_specialize [simp]: "predicates_form(specialize φ) = predicates_form φ"
by (induction φ) auto
lemma specialize_language: ‹language (specialize ` S) = language S›
by (simp add: language_def functions_forms_def predicates_def)
definition skolem :: "form ⇒ form" where
‹skolem φ = specialize(skolemize φ)›
lemma skolem_qfree: ‹qfree (skolem φ)›
by (simp add: skolem_def specialize_qfree)
theorem skolem_satisfiable:
‹(∃M::'a intrp. dom M ≠ {} ∧ is_interpretation (language S) M ∧ satisfies M S)
⟷ (∃M::'a intrp. dom M ≠ {} ∧ is_interpretation (language (skolem ` S)) M ∧
satisfies M (skolem ` S))›
proof -
have "is_interpretation (language (skolemize ` S)) M ⟷ is_interpretation (language (skolem ` S)) M"
for M :: "'a intrp"
by (simp add: functions_forms_def is_interpretation_def language_def skolem_def)
moreover
have "satisfies M (skolemize ` S) ⟷ satisfies M (skolem ` S)"
if "dom M ≠ {}" for M :: "'a intrp"
by (smt (verit, del_insts) image_iff satisfies_def skolem_def specialize_satisfies that)
ultimately show ?thesis
by (metis skolemize_satisfiable)
qed
end