Theory Prenex_Normal_Form
theory Prenex_Normal_Form
imports
Ground_FOL_Compactness
begin
inductive is_prenex :: "form ⇒ bool" where
‹qfree φ ⟹ is_prenex φ›
| ‹is_prenex φ ⟹ is_prenex (❙∀x❙. φ)›
| ‹is_prenex φ ⟹ is_prenex (❙∃x❙. φ)›
inductive_simps is_prenex_simps [simp]:
"is_prenex Bot"
"is_prenex (Atom p ts)"
"is_prenex (φ ❙⟶ ψ)"
"is_prenex (❙∀ x❙. φ)"
lemma prenex_formsubst1: ‹is_prenex φ ⟹ is_prenex (φ ⋅⇩f⇩m σ)›
proof (induction φ arbitrary: σ rule: is_prenex.induct)
case 1
then show ?case using is_prenex.intros(1) qfree_formsubst
by blast
next
case (2 φ x)
then show ?case
using formsubst_def_switch by (metis (no_types, lifting) formsubst.simps(4) is_prenex.intros(2))
next
case (3 φ x)
then show ?case
using formsubst_def_switch is_prenex.intros(3)
by (smt (verit, del_insts) formsubst.simps(1) formsubst.simps(3) formsubst.simps(4))
qed
lemma prenex_formsubst2: ‹is_prenex (φ ⋅⇩f⇩m σ) ⟹ is_prenex φ›
proof (induction ‹φ ⋅⇩f⇩m σ› arbitrary: φ σ rule: is_prenex.induct)
case 1
then show ?case
using is_prenex.intros(1) qfree_formsubst by auto
next
case (2 ψ x φ)
then obtain y φ' where phi_is: ‹φ = ❙∀y❙. φ'›
using formsubst_structure_all by metis
then have ‹∃σ'. ψ = φ'⋅⇩f⇩m σ'›
using 2(3) by (metis (no_types, lifting) form.sel(6) formsubst.simps(4))
then obtain σ' where ‹ψ = φ'⋅⇩f⇩m σ'›
by blast
then have ‹is_prenex φ'›
using 2(2) by blast
then show ?case
using phi_is by (simp add: is_prenex.intros(2))
next
case (3 ψ x φ)
then obtain y φ' where phi_is: ‹φ = ❙∃y❙. φ'›
using formsubst_structure_ex by metis
then have ‹∃σ'. ψ = φ'⋅⇩f⇩m σ'›
using 3(3) by (smt (verit, ccfv_threshold) form.inject(2) form.inject(3) formsubst.simps(3)
formsubst.simps(4))
then obtain σ' where ‹ψ = φ'⋅⇩f⇩m σ'›
by blast
then have ‹is_prenex φ'›
using 3(2) by blast
then show ?case
using phi_is by (simp add: is_prenex.intros(3))
qed
lemma prenex_formsubst: ‹is_prenex (φ ⋅⇩f⇩m σ) ≡ is_prenex φ›
using prenex_formsubst1 prenex_formsubst2 by (smt (verit, ccfv_threshold))
lemma prenex_imp: ‹is_prenex (φ ❙⟶ ψ) ⟹
qfree (φ ❙⟶ ψ) ∨ (ψ = ❙⊥ ∧ (∃x φ'. is_prenex φ' ∧ φ = (❙∀x❙. φ' ❙⟶ ❙⊥)))›
by (metis form.distinct(11) form.inject(2) is_prenex.cases)
inductive universal :: "form ⇒ bool" where
‹qfree φ ⟹ universal φ›
| ‹universal φ ⟹ universal (❙∀x❙. φ)›
inductive_simps universal_simps [simp]:
"universal Bot"
"universal (Atom p ts)"
"universal (φ ❙⟶ ψ)"
"universal (❙∀ x❙. φ)"
fun size :: "form ⇒ nat" where
‹size ❙⊥ = 1›
| ‹size (Atom p ts) = 1›
| ‹size (φ ❙⟶ ψ) = size φ + size ψ›
| ‹size (❙∀ x❙. φ) = 1 + size φ›
lemma wf_size: ‹wfP (λφ ψ. size φ < size ψ)›
by (simp add: wfp_if_convertible_to_nat)
lemma size_indep_subst: ‹size (φ ⋅⇩f⇩m σ) = size φ›
proof (induction φ arbitrary: σ)
case (Forall x φ)
have ‹∃z σ'.(❙∀x❙. φ) ⋅⇩f⇩m σ = ❙∀z❙. (φ ⋅⇩f⇩m σ')›
by (meson formsubst.simps(4))
then obtain z σ' where ‹(❙∀x❙. φ) ⋅⇩f⇩m σ = ❙∀z❙. (φ ⋅⇩f⇩m σ')›
by blast
then have ‹size ((❙∀x❙. φ) ⋅⇩f⇩m σ) = size (❙∀z❙. (φ ⋅⇩f⇩m σ'))›
by argo
also have ‹... = size (❙∀x❙. φ)›
using Forall by auto
finally show ?case .
qed auto
lemma prenex_distinct: ‹(❙∀x❙. φ) ≠ (❙∃y❙. ψ)›
by auto
lemma uniq_all_x: "Uniq (λx. ∃p. r = ❙∀x❙. p)"
using Uniq_def by blast
lemma uniq_all_p: ‹Uniq ((λp. r = ❙∀(THE x. ∃p. r = ❙∀x❙. p)❙. p))›
using uniq_all_x Uniq_def
by (smt (verit, ccfv_threshold) form.inject(3))
lemma uniq_ex_x: "Uniq (λx. ∃p. r = ❙∃x❙. p)"
using Uniq_def by blast
lemma uniq_ex_p: ‹Uniq ((λp. r = ❙∃(THE x. ∃p. r = ❙∃x❙. p)❙. p))›
using uniq_ex_x Uniq_def
by (smt (verit, best) form.inject(2) form.inject(3))
definition ppat :: "(nat ⇒ form ⇒ form) ⇒ (nat ⇒ form ⇒ form) ⇒ (form ⇒ form) ⇒ form ⇒ form" where
‹ppat A B C r = (if (∃x p. r = ❙∀x❙. p) then
A (THE x. ∃p. r = ❙∀x❙. p) (THE p. r = ❙∀(THE x. ∃p. r = ❙∀x❙. p)❙. p)
else (if ∃x p. r = ❙∃x❙. p then
B (THE x. ∃p. r = ❙∃x❙. p) (THE p. r = ❙∃(THE x. ∃p. r = ❙∃x❙. p)❙. p)
else C r))›
lemma ppat_simpA: ‹∀x p. ppat A B C (❙∀x❙. p) = A x p›
unfolding ppat_def by simp
lemma ppat_simpB: ‹∀x p. ppat A B C (❙∃x❙. p) = B x p›
unfolding ppat_def by simp
lemma ppat_last: ‹(∀r. ¬(∃x p. r = ❙∀x❙. p) ∧ ¬(∃x p. r = ❙∃x❙. p)) ⟹ ppat A B C r = C r›
by blast
lemma ppat_last_qfree: ‹qfree r ⟹ ppat A B C r = C r›
using qfree_no_quantif ppat_last by (simp add: ppat_def)
lemma ppat_to_ex_qfree:
‹(∃f. (∀x p q. f p (❙∀x❙. q) = ((A :: form ⇒ nat ⇒ form ⇒ form) p) x q) ∧
(∀x p q. f p (❙∃x❙. q) = (B p) x q) ∧
(∀p q. qfree q ⟶ f p q = (C p) q))›
proof
define f where ‹f = (λp q. ppat (A p) (B p) (C p) q)›
have A_eq: ‹(∀x p q. ppat (A p) (B p) (C p) (❙∀x❙. q) = (A p) x q)› and
B_eq: ‹(∀x p q. ppat (A p) (B p) (C p) (❙∃x❙. q) = (B p) x q)›
unfolding ppat_def by simp+
have C_eq: ‹(∀p q. qfree q ⟶ ppat (A p) (B p) (C p) q = (C p) q)›
using ppat_last_qfree by blast
show ‹(∀x p q. f p (❙∀ x❙. q) = A p x q) ∧ (∀x p q. f p (❙∃x❙. q) = B p x q) ∧ (∀p q. qfree q ⟶ f p q = (C p) q)›
using A_eq B_eq C_eq unfolding f_def by blast
qed
lemma size_rec:
‹∀f g x. (∀(z::form). size z < size x ⟶ (f z = g z)) ⟶ (H f x = H g x) ⟹ (∃f. ∀x. f x = H f x)›
using wfrec [of "measure size" H] by (metis cut_apply in_measure wf_measure)
abbreviation prenex_right_forall :: "(form ⇒ form ⇒ form) ⇒ form ⇒ nat ⇒ form ⇒ form" where
‹prenex_right_forall ≡
(λp φ x ψ. (let y = variant(FV φ ∪ FV (❙∀x❙. ψ)) in (❙∀y❙. p φ (ψ ⋅⇩f⇩m (subst x (Var y))))))›
abbreviation prenex_right_exists :: "(form ⇒ form ⇒ form) ⇒ form ⇒ nat ⇒ form ⇒ form" where
‹prenex_right_exists ≡
(λp φ x ψ. (let y = variant(FV φ ∪ FV (❙∃x❙. ψ)) in (❙∃y❙. p φ (ψ ⋅⇩f⇩m (subst x (Var y))))))›
lemma prenex_right_ex:
‹∃prenex_right. (∀φ x ψ. prenex_right φ (❙∀x❙. ψ) = prenex_right_forall prenex_right φ x ψ)
∧ (∀φ x ψ. prenex_right φ (❙∃x❙. ψ) = prenex_right_exists prenex_right φ x ψ)
∧ (∀φ ψ. qfree ψ ⟶ prenex_right φ ψ = (φ ❙⟶ ψ))›
proof -
have ‹∀φ. ∃prenex_right_only. ∀ψ. prenex_right_only ψ = ppat
(λx ψ. (let y = variant(FV φ ∪ FV (❙∀x❙. ψ)) in (❙∀y❙. prenex_right_only (ψ ⋅⇩f⇩m (subst x (Var y))))))
(λx ψ. (let y = variant(FV φ ∪ FV (❙∃x❙. ψ)) in (❙∃y❙. prenex_right_only (ψ ⋅⇩f⇩m (subst x (Var y))))))
(λψ. (φ ❙⟶ ψ)) ψ›
proof
fix φ
define A where ‹A = (λg x ψ. (let y = variant(FV φ ∪ FV (❙∀x❙. ψ)) in (❙∀y❙. g (ψ ⋅⇩f⇩m (subst x (Var y))))))›
define B where ‹B = (λp x ψ. (let y = variant(FV φ ∪ FV (❙∃x❙. ψ)) in (❙∃y❙. p (ψ ⋅⇩f⇩m (subst x (Var y))))))›
show ‹∃prenex_right_only. ∀ψ. prenex_right_only ψ =
ppat (A prenex_right_only) (B prenex_right_only) (λψ. (φ ❙⟶ ψ)) ψ›
proof (rule size_rec, (rule allI)+, (rule impI))
fix prenex_right_only g:: "form ⇒ form" and ψ
assume IH: ‹∀z. size z < size ψ ⟶ prenex_right_only z = g z›
show ‹ppat (A prenex_right_only) (B prenex_right_only) (λψ. (φ ❙⟶ ψ)) ψ =
ppat (A g) (B g) (λψ. (φ ❙⟶ ψ)) ψ›
proof (cases "∃x ψ'. ψ = ❙∀x❙. ψ'")
case True
then obtain x ψ' where psi_is: "ψ = ❙∀x❙. ψ'"
by blast
then have smaller: ‹size (ψ' ⋅⇩f⇩m σ) < size ψ› for σ
using size_indep_subst by simp
have ‹ppat (A prenex_right_only) (B prenex_right_only) (λψ. (φ ❙⟶ ψ)) ψ =
A prenex_right_only x ψ'›
unfolding ppat_def by (simp add: psi_is)
also have ‹... = A g x ψ'›
unfolding A_def using IH smaller by presburger
also have ‹... = ppat (A g) (B g) (λψ. (φ ❙⟶ ψ)) ψ›
unfolding ppat_def by (simp add: psi_is)
finally show ?thesis .
next
case False
assume falseAll: ‹¬(∃x ψ'. ψ = ❙∀ x❙. ψ')›
then show ?thesis
proof (cases "∃x ψ'. ψ = ❙∃x❙. ψ'")
case True
then obtain x ψ' where psi_is: "ψ = ❙∃x❙. ψ'"
by blast
then have smaller: ‹size (ψ' ⋅⇩f⇩m σ) < size ψ› for σ
using size_indep_subst by simp
have ‹ppat (A prenex_right_only) (B prenex_right_only) (λψ. (φ ❙⟶ ψ)) ψ =
B prenex_right_only x ψ'›
unfolding ppat_def by (simp add: psi_is)
also have ‹... = B g x ψ'›
unfolding B_def using IH smaller by presburger
also have ‹... = ppat (A g) (B g) (λψ. (φ ❙⟶ ψ)) ψ›
unfolding ppat_def by (simp add: psi_is)
finally show ?thesis .
next
case False
then show ?thesis
using falseAll ppat_last unfolding ppat_def by argo
qed
qed
qed
qed
then have ‹∃prenex_right. ∀φ ψ. prenex_right φ ψ = ppat
(prenex_right_forall prenex_right φ)
(prenex_right_exists prenex_right φ)
((❙⟶) φ) ψ›
using choice[of "λφ p. ∀ψ. p ψ =
ppat (λx ψ. let y = variant (FV φ ∪ FV (❙∀x❙. ψ)) in ❙∀y❙. p (ψ ⋅⇩f⇩m subst x (Var y)))
(λx ψ. let y = variant (FV φ ∪ FV (❙∃x❙. ψ)) in (❙∃y❙. p (ψ ⋅⇩f⇩m subst x (Var y))))
((❙⟶) φ) ψ"] by blast
then obtain prenex_right where prenex_right_is: ‹∀φ ψ. prenex_right φ ψ =
ppat (prenex_right_forall prenex_right φ) (prenex_right_exists prenex_right φ) ((❙⟶) φ) ψ›
by blast
have ‹∀φ x ψ. prenex_right φ (❙∀x❙. ψ) = prenex_right_forall prenex_right φ x ψ›
using prenex_right_is unfolding ppat_def by simp
moreover have ‹∀φ x ψ. prenex_right φ (❙∃x❙. ψ) = prenex_right_exists prenex_right φ x ψ›
using prenex_right_is unfolding ppat_def by simp
moreover have ‹∀φ ψ. qfree ψ ⟶ prenex_right φ ψ = (φ ❙⟶ ψ)›
using prenex_right_is by (metis (no_types, lifting) ppat_last_qfree)
ultimately show ?thesis
by blast
qed
consts prenex_right :: "form ⇒ form ⇒ form"
specification (prenex_right) ‹
(∀φ x ψ. prenex_right φ (❙∀x❙. ψ) = prenex_right_forall prenex_right φ x ψ) ∧
(∀φ x ψ. prenex_right φ (❙∃x❙. ψ) = prenex_right_exists prenex_right φ x ψ) ∧
(∀φ ψ. qfree ψ ⟶ prenex_right φ ψ = (φ ❙⟶ ψ))›
using prenex_right_ex by blast
lemma prenex_right_qfree_case: ‹qfree ψ ⟹ prenex_right φ ψ = (φ ❙⟶ ψ)›
proof -
assume qfree_psi: "qfree ψ"
have ‹((∀φ x ψ. p φ (❙∀x❙. ψ) = prenex_right_forall p φ x ψ) ∧
(∀φ x ψ. p φ (❙∃x❙. ψ) = prenex_right_exists p φ x ψ) ∧
(∀φ ψ. qfree ψ ⟶ p φ ψ = (φ ❙⟶ ψ))) ⟹ (∀φ ψ. qfree ψ ⟶ p φ ψ = (φ ❙⟶ ψ))› (is "?P p ⟹ ?Q p") for p
by argo
then have ‹(∀φ ψ. qfree ψ ⟶ prenex_right φ ψ = (φ ❙⟶ ψ))›
using someI2_ex[of ?P ?Q] prenex_right_def prenex_right_ex by presburger
then show ?thesis
using qfree_psi by blast
qed
lemma prenex_right_all_case: ‹prenex_right φ (❙∀x❙. ψ) = prenex_right_forall prenex_right φ x ψ›
proof -
have all_cases_imp_all_case: ‹((∀φ x ψ. p φ (❙∀x❙. ψ) = prenex_right_forall p φ x ψ) ∧
(∀φ x ψ. p φ (❙∃x❙. ψ) = prenex_right_exists p φ x ψ) ∧
(∀φ ψ. qfree ψ ⟶ p φ ψ = (φ ❙⟶ ψ))) ⟹
(p φ (❙∀x❙. ψ) = prenex_right_forall p φ x ψ)› (is "?P p ⟹ ?Q p") for p
by meson
then have ‹prenex_right φ (❙∀x❙. ψ) = prenex_right_forall prenex_right φ x ψ›
using someI2_ex[of ?P ?Q] prenex_right_def prenex_right_ex by presburger
then show ?thesis .
qed
lemma prenex_right_exist_case: ‹prenex_right φ (❙∃x❙. ψ) = prenex_right_exists prenex_right φ x ψ›
proof -
have ex_cases_imp_ex_case: ‹((∀φ x ψ. p φ (❙∀x❙. ψ) = prenex_right_forall p φ x ψ) ∧
(∀φ x ψ. p φ (❙∃x❙. ψ) = prenex_right_exists p φ x ψ) ∧
(∀φ ψ. qfree ψ ⟶ p φ ψ = (φ ❙⟶ ψ))) ⟹
(p φ (❙∃x❙. ψ) = prenex_right_exists p φ x ψ)› (is "?P p ⟹ ?Q p") for p
by meson
then have ‹prenex_right φ (❙∃x❙. ψ) = prenex_right_exists prenex_right φ x ψ›
using someI2_ex[of ?P ?Q] prenex_right_def prenex_right_ex by presburger
then show ?thesis .
qed
lemma prenex_right_exists_shape_case:
‹∃x2 σ. prenex_right φ (❙∃x❙. ψ) = ❙∃x2❙. prenex_right φ (ψ ⋅⇩f⇩m σ)›
proof -
have all_cases_imp_all_case: ‹((∀φ x ψ. p φ (❙∀x❙. ψ) = prenex_right_forall p φ x ψ) ∧
(∀φ x ψ. p φ (❙∃x❙. ψ) = prenex_right_exists p φ x ψ) ∧
(∀φ ψ. qfree ψ ⟶ p φ ψ = (φ ❙⟶ ψ))) ⟹
(∃x2 σ. p φ (❙∃x❙. ψ) = ❙∃x2❙. p φ (ψ ⋅⇩f⇩m σ))› (is "?P p ⟹ ?Q p") for p
by meson
then have ‹∃x2 σ. prenex_right φ (❙∃x❙. ψ) = ❙∃x2❙. prenex_right φ (ψ ⋅⇩f⇩m σ)›
using someI2_ex[of ?P ?Q] prenex_right_def prenex_right_ex by presburger
then show ?thesis .
qed
abbreviation prenex_left_forall :: "(form ⇒ form ⇒ form) ⇒ form ⇒ nat ⇒ form ⇒ form" where
‹prenex_left_forall ≡
(λp φ x ψ. (let y = variant(FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. p (φ ⋅⇩f⇩m (subst x (Var y))) ψ)))›
abbreviation prenex_left_exists :: "(form ⇒ form ⇒ form) ⇒ form ⇒ nat ⇒ form ⇒ form" where
‹prenex_left_exists ≡
(λp φ x ψ. (let y = variant(FV (❙∃x❙. φ) ∪ FV ψ) in (❙∀y❙. p (φ ⋅⇩f⇩m (subst x (Var y))) ψ)))›
lemma prenex_left_ex:
‹∃prenex_left. (∀φ x ψ. prenex_left (❙∀x❙. φ) ψ = prenex_left_forall prenex_left φ x ψ)
∧ (∀φ x ψ. prenex_left (❙∃x❙. φ) ψ = prenex_left_exists prenex_left φ x ψ)
∧ (∀φ ψ. qfree φ ⟶ prenex_left φ ψ = prenex_right φ ψ)›
proof -
have ‹∀ψ. ∃prenex_left_only. ∀φ. prenex_left_only φ = ppat
(λx φ. (let y = variant(FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. prenex_left_only (φ ⋅⇩f⇩m (subst x (Var y))))))
(λx φ. (let y = variant(FV (❙∃x❙. φ) ∪ FV ψ) in (❙∀y❙. prenex_left_only (φ ⋅⇩f⇩m (subst x (Var y))))))
(λφ. prenex_right φ ψ) φ›
proof
fix ψ
define A where ‹A = (λg x φ. (let y = variant(FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. g (φ ⋅⇩f⇩m (subst x (Var y))))))›
define B where ‹B = (λp x φ. (let y = variant(FV (❙∃x❙. φ) ∪ FV ψ) in (❙∀y❙. p (φ ⋅⇩f⇩m (subst x (Var y))))))›
show ‹∃prenex_left_only. ∀φ. prenex_left_only φ =
ppat (A prenex_left_only) (B prenex_left_only) (λφ. prenex_right φ ψ) φ›
proof (rule size_rec, (rule allI)+, (rule impI))
fix prenex_left_only g:: "form ⇒ form" and φ
assume IH: ‹∀z. size z < size φ ⟶ prenex_left_only z = g z›
show ‹ppat (A prenex_left_only) (B prenex_left_only) (λφ. prenex_right φ ψ) φ =
ppat (A g) (B g) (λφ. prenex_right φ ψ) φ›
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 (A prenex_left_only) (B prenex_left_only) (λφ. prenex_right φ ψ) φ =
A prenex_left_only x φ'›
unfolding ppat_def by (simp add: phi_is)
also have ‹... = A g x φ'›
unfolding A_def using IH smaller by presburger
also have ‹... = ppat (A g) (B g) (λφ. prenex_right φ ψ) φ›
unfolding ppat_def by (simp add: phi_is)
finally show ?thesis .
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 (A prenex_left_only) (B prenex_left_only) (λφ. prenex_right φ ψ) φ =
B prenex_left_only x φ'›
unfolding ppat_def by (simp add: phi_is)
also have ‹... = B g x φ'›
unfolding B_def using IH smaller by presburger
also have ‹... = ppat (A g) (B g) (λφ. prenex_right φ ψ) φ›
unfolding ppat_def by (simp add: phi_is)
finally show ?thesis .
next
case False
then show ?thesis
using falseAll ppat_last unfolding ppat_def by argo
qed
qed
qed
qed
then have ‹∃prenex_left_argswap. ∀ψ φ. prenex_left_argswap ψ φ = ppat
(λx φ. let y = variant (FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. prenex_left_argswap ψ (φ ⋅⇩f⇩m subst x (Var y))))
(λx φ. let y = variant (FV (❙∃x❙. φ) ∪ FV ψ) in ❙∀ y❙. prenex_left_argswap ψ (φ ⋅⇩f⇩m subst x (Var y)))
(λφ. prenex_right φ ψ) φ›
using choice[of "λψ p. ∀φ. p φ =
ppat (λx φ. let y = variant (FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. p (φ ⋅⇩f⇩m subst x (Var y))))
(λx φ. let y = variant (FV (❙∃x❙. φ) ∪ FV ψ) in ❙∀y❙. p (φ ⋅⇩f⇩m subst x (Var y)))
(λφ. prenex_right φ ψ) φ"] by blast
then have ‹∃prenex_left. ∀φ ψ. prenex_left φ ψ = ppat
(λx φ. let y = variant (FV (❙∀x❙. φ) ∪ FV ψ) in (❙∃y❙. prenex_left (φ ⋅⇩f⇩m subst x (Var y)) ψ))
(λx φ. let y = variant (FV (❙∃x❙. φ) ∪ FV ψ) in ❙∀ y❙. prenex_left (φ ⋅⇩f⇩m subst x (Var y)) ψ)
(λφ. prenex_right φ ψ) φ›
by force
then obtain prenex_left where prenex_left_is: ‹∀φ ψ. prenex_left φ ψ = ppat
(λx φ. prenex_left_forall prenex_left φ x ψ)
(λx φ. prenex_left_exists prenex_left φ x ψ)
(λφ. prenex_right φ ψ) φ›
by blast
have ‹∀φ x ψ. prenex_left (❙∀x❙. φ) ψ = prenex_left_forall prenex_left φ x ψ›
using prenex_left_is unfolding ppat_def by simp
moreover have ‹∀φ x ψ. prenex_left (❙∃x❙. φ) ψ = prenex_left_exists prenex_left φ x ψ›
using prenex_left_is unfolding ppat_def by simp
moreover have ‹∀φ ψ. qfree φ ⟶ prenex_left φ ψ = prenex_right φ ψ›
using prenex_left_is by (metis (no_types, lifting) ppat_last_qfree)
ultimately show ?thesis
by blast
qed
definition prenex_left where ‹prenex_left = (SOME prenex_left.
(∀φ x ψ. prenex_left (❙∀x❙. φ) ψ = prenex_left_forall prenex_left φ x ψ) ∧
(∀φ x ψ. prenex_left (❙∃x❙. φ) ψ = prenex_left_exists prenex_left φ x ψ) ∧
(∀φ ψ. qfree φ ⟶ prenex_left φ ψ = prenex_right φ ψ))›
lemma prenex_left_forall_case: ‹prenex_left (❙∀x❙. φ) ψ = prenex_left_forall prenex_left φ x ψ›
unfolding prenex_left_def by (smt (verit, del_insts) prenex_left_ex some_eq_ex)
lemma prenex_left_qfree_case: ‹qfree φ ⟹ prenex_left φ ψ = prenex_right φ ψ›
unfolding prenex_left_def by (smt (verit, del_insts) prenex_left_ex some_eq_ex)
lemma prenex_left_exists_case: ‹prenex_left (❙∃x❙. φ) ψ = prenex_left_exists prenex_left φ x ψ›
unfolding prenex_left_def by (smt (verit, del_insts) prenex_left_ex some_eq_ex)
lemma prenex_left_exists_shape_case:
‹∃x2 σ. prenex_left (❙∃x❙. φ) ψ = ❙∀x2❙. prenex_left (φ ⋅⇩f⇩m σ) ψ›
using prenex_left_exists_case by metis
fun prenex where
‹prenex ❙⊥ = ❙⊥›
| ‹prenex (Atom p ts) = Atom p ts›
| ‹prenex (φ ❙⟶ ψ) = prenex_left (prenex φ) (prenex ψ)›
| ‹prenex (❙∀x❙. φ) = ❙∀x❙. (prenex φ)›
lemma holds_indep_forall:
assumes y_notin: ‹y ∉ FV (❙∀x❙. φ)›
shows ‹(I❙,β ⊨ (❙∀x❙. φ) ⟷ I❙,β ⊨ (❙∀y❙. φ ⋅⇩f⇩m (subst x (Var y))))›
proof (cases ‹y = x›)
case False
then have y_notin_phi: ‹y ∉ FV φ› using y_notin by simp
have beta_equiv: ‹∀w ∈ FV φ. (λv. termsubst I (β(y := a)) (subst x (Var y)) v) w = (β(x := a)) w› for a
proof
fix w
assume w_in: ‹w ∈ FV φ›
have ‹w = x ⟹ (λv. termsubst I (β(y := a)) (subst x (Var y)) v) w = (β(x := a)) w›
by simp
moreover have ‹w ≠ x ⟹ (λv. termsubst I (β(y := a)) (subst x (Var y)) v) w = (β(x := a)) w›
using y_notin_phi by (metis w_in eval.simps(1) fun_upd_other subst_def)
ultimately show ‹(λv. termsubst I (β(y := a)) (subst x (Var y)) v) w = (β(x := a)) w›
by argo
qed
have ‹I❙,β ⊨ (❙∀x❙. φ) ≡ (∀a ∈ dom I. I❙,β(x := a) ⊨ φ)›
by simp
also have ‹... ≡ (∀a ∈ dom I. I❙,(λv. termsubst I (β(y := a)) (subst x (Var y)) v) ⊨ φ)›
using holds_indep_β_if[OF beta_equiv] by presburger
also have ‹... ≡ (∀a ∈ dom I. I❙,β(y := a) ⊨ (φ ⋅⇩f⇩m (subst x (Var y))))›
using swap_subst_eval[of I _ φ "subst x (Var y)"] by presburger
also have ‹... ≡ (I❙,β ⊨ (❙∀y❙. φ ⋅⇩f⇩m (subst x (Var y))))›
by simp
finally show ?thesis
by argo
qed auto
lemma forall_imp_commute:
assumes y_notin: ‹y ∉ FV φ›
shows ‹((I :: 'a intrp)❙, β ⊨ (φ ❙⟶ (❙∀y❙. ψ)) ⟷ I❙, β ⊨ (❙∀y❙. φ ❙⟶ ψ))›
proof -
have ‹((I❙, β ⊨ φ) ⟶ (∀a ∈ dom I. I❙,β(y := a) ⊨ ψ)) ⟷
(∀a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β(y := a) ⊨ ψ))›
by (smt (verit, del_insts) fun_upd_other holds_indep_β_if assms)
then show ?thesis
by simp
qed
lemma forall_imp_exists:
assumes y_notin: ‹y ∉ FV ψ›
shows ‹((I :: 'a intrp)❙, β ⊨ ((❙∀y❙.φ) ❙⟶ ψ) ⟷ I❙, β ⊨ (❙∃y❙. (φ ❙⟶ ψ)))›
proof -
have ‹((∀a ∈ dom I. I❙,β(y := a) ⊨ φ) ⟶ (I❙, β ⊨ ψ)) ⟷ (∃a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β ⊨ ψ))›
using empty_iff list.set(1)
by (smt (verit, best) equals0I intrp_is_struct struct_def)
also have ‹... ⟷ (∃a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β(y := a) ⊨ ψ))›
using holds_indep_β_if by (smt (verit, del_insts) fun_upd_other y_notin)
finally show ?thesis
by simp
qed
lemma exists_imp_forall:
assumes y_notin: ‹y ∉ FV ψ›
shows ‹(I❙, β ⊨ ((❙∃y❙.φ) ❙⟶ ψ) ⟷ I❙, β ⊨ (❙∀y❙. (φ ❙⟶ ψ)))›
proof -
have ‹(∃a ∈ dom I. I❙,β(y := a) ⊨ φ) ⟶ (I❙, β ⊨ ψ) ≡
(∀a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β ⊨ ψ))›
using empty_iff list.set(1) by (smt (verit, ccfv_threshold))
also have ‹... ≡ (∀a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β(y := a) ⊨ ψ))›
using holds_indep_β_if by (smt (verit, del_insts) fun_upd_other y_notin)
finally show ?thesis
by simp
qed
lemma exists_imp_commute:
assumes y_notin: ‹y ∉ FV φ›
shows ‹((I :: 'a intrp)❙, β ⊨ (φ ❙⟶ (❙∃y❙. ψ)) ⟷ I❙, β ⊨ (❙∃y❙. φ ❙⟶ ψ))›
proof -
have ‹((I❙, β ⊨ φ) ⟶ (∃a ∈ dom I. I❙,β(y := a) ⊨ ψ)) ⟷
(∃a ∈ dom I. (I❙, β ⊨ φ) ⟶ (I❙,β(y := a) ⊨ ψ))›
by (smt (verit) equals0I intrp_is_struct struct_def)
also have ‹... ⟷ (∃a ∈ dom I. (I❙,β(y := a) ⊨ φ ⟶ I❙,β(y := a) ⊨ ψ))›
using y_notin by (smt (verit, ccfv_threshold) fun_upd_other holds_indep_β_if)
finally show ?thesis
using holds_exists by simp
qed
lemma holds_indep_exists:
‹y ∉ FV (❙∃x❙. φ) ⟹ (I❙,β ⊨ (❙∃x❙. φ) ⟷ I❙,β ⊨ (❙∃y❙. φ ⋅⇩f⇩m (subst x (Var y))))›
by (metis FV.simps(1,3) formsubst.simps(1,3) holds.simps(3) holds_indep_forall sup_bot.right_neutral)
lemma prenex_right_forall_is:
assumes ‹dom I ≠ {}›
shows ‹((I❙, β ⊨ φ ❙⟶ (❙∀x❙. ψ)) ⟷
(I❙, β ⊨ (❙∀(variant (FV φ ∪ FV (❙∀x❙. ψ)))❙.
(φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∀x❙. ψ))))))))))› (is "?lhs = ?rhs")
proof -
define y where ‹y = variant (FV φ ∪ FV (❙∀x❙. ψ))›
then have y_notin1: ‹y ∉ FV φ› and y_notin2: ‹y ∉ FV (❙∀x❙. ψ)›
using variant_finite finite_FV by (meson UnCI finite_UnI)+
have ‹?lhs ⟷ I❙, β ⊨ (φ ❙⟶ (❙∀y❙. ψ ⋅⇩f⇩m (subst x (Var y))))›
using holds_indep_forall y_notin2
by (smt (verit, ccfv_SIG) holds.simps(3))
also have ‹... ⟷ I❙, β ⊨ (❙∀y❙. φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var y))))›
using forall_imp_commute[OF y_notin1, of I β "ψ ⋅⇩f⇩m (subst x (Var y))"] .
finally show ?thesis
unfolding y_def .
qed
lemma prenex_right_exists_is:
assumes ‹dom I ≠ {}›
shows ‹((I❙, β ⊨ φ ❙⟶ (❙∃x❙. ψ)) ⟷
(I❙, β ⊨ (❙∃(variant (FV φ ∪ FV (❙∃x❙. ψ)))❙.
(φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∃x❙. ψ))))))))))› (is "?lhs = ?rhs")
proof -
define y where ‹y = variant (FV φ ∪ FV (❙∃x❙. ψ))›
then have y_notin1: ‹y ∉ FV φ› and y_notin2: ‹y ∉ FV (❙∃x❙. ψ)›
using variant_finite finite_FV by (meson UnCI finite_UnI)+
have ‹?lhs ⟷ I❙, β ⊨ (φ ❙⟶ (❙∃y❙. ψ ⋅⇩f⇩m (subst x (Var y))))›
using holds_indep_exists y_notin2 holds_exists by (smt (verit) holds.simps(3))
also have ‹... ⟷ I❙, β ⊨ (❙∃y❙. φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var y))))›
using exists_imp_commute[OF y_notin1, of I β "ψ ⋅⇩f⇩m (subst x (Var y))"] .
finally show ?thesis
unfolding y_def .
qed
lemma prenex_left_forall_is:
assumes ‹dom I ≠ {}›
shows ‹(I❙, β ⊨ ((❙∀x❙. φ) ❙⟶ ψ)) ≡ (I❙, β ⊨ (❙∃(variant (FV (❙∀x❙. φ) ∪ FV ψ))❙.
((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∀x❙. φ) ∪ FV ψ))))) ❙⟶ ψ)))›
using forall_imp_exists holds_indep_forall holds.simps(3)
by (smt (verit, del_insts) FV.simps(3) UnI2 sup.commute variant_form)
lemma prenex_left_exists_is:
assumes ‹dom I ≠ {}›
shows ‹(I❙, β ⊨ ((❙∃x❙. φ) ❙⟶ ψ)) ≡ (I❙, β ⊨ (❙∀(variant (FV (❙∃x❙. φ) ∪ FV ψ))❙.
((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∃x❙. φ) ∪ FV ψ))))) ❙⟶ ψ)))›
using exists_imp_forall holds_indep_exists holds.simps(3)
by (smt (verit, ccfv_SIG) FV.simps(3) UnCI finite_FV variant_finite)
lemma prenex_right_forall_FV: ‹FV (φ ❙⟶ (❙∀x❙. ψ)) =
FV (❙∀(variant (FV φ ∪ FV (❙∀x❙. ψ)))❙. (φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∀x❙. ψ))))))))›
using formsubst_rename
by (metis Diff_empty Diff_insert0 FV.simps(3) FV.simps(4) Un_Diff finite_FV variant_finite)
lemma prenex_right_exists_FV: ‹FV (φ ❙⟶ (❙∃x❙. ψ)) =
FV (❙∀(variant (FV φ ∪ FV (❙∃x❙. ψ)))❙. (φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∃x❙. ψ))))))))›
using formsubst_rename prenex_right_forall_FV by force
lemma prenex_left_forall_FV: ‹FV ((❙∀x❙. φ) ❙⟶ ψ) =
FV (❙∃(variant (FV (❙∀x❙. φ) ∪ FV ψ))❙. ((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∀x❙. φ) ∪ FV ψ))))) ❙⟶ ψ))›
using formsubst_rename
by (metis Diff_idemp Diff_insert_absorb FV.simps(3) FV.simps(4) Un_Diff finite_FV variant_finite FV_exists)
lemma prenex_left_exists_FV: ‹FV ((❙∃x❙. φ) ❙⟶ ψ) =
FV (❙∀(variant (FV (❙∃x❙. φ) ∪ FV ψ))❙. ((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∃x❙. φ) ∪ FV ψ))))) ❙⟶ ψ))›
using formsubst_rename FV_exists prenex_left_forall_FV by auto
lemma prenex_right_forall_language: ‹language {φ ❙⟶ (❙∀x❙. ψ)} =
language {❙∀(variant (FV φ ∪ FV (❙∀x❙. ψ)))❙. (φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∀x❙. ψ)))))))}›
using lang_singleton formsubst_functions_form formsubst_predicates formsubst_language_rename by auto
lemma prenex_right_exists_language: ‹language {φ ❙⟶ (❙∃x❙. ψ)} =
language {❙∃(variant (FV φ ∪ FV (❙∃x❙. ψ)))❙. (φ ❙⟶ (ψ ⋅⇩f⇩m (subst x (Var (variant (FV φ ∪ FV (❙∃x❙. ψ)))))))}›
using lang_singleton formsubst_functions_form formsubst_predicates formsubst_language_rename by auto
lemma prenex_left_forall_language: ‹language {(❙∀x❙. φ) ❙⟶ ψ} =
language {❙∃(variant (FV (❙∀x❙. φ) ∪ FV ψ))❙. ((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∀x❙. φ) ∪ FV ψ))))) ❙⟶ ψ)}›
using lang_singleton formsubst_functions_form formsubst_predicates formsubst_language_rename by auto
lemma prenex_left_exists_language: ‹language {(❙∃x❙. φ) ❙⟶ ψ} =
language {❙∀(variant (FV (❙∃x❙. φ) ∪ FV ψ))❙. ((φ ⋅⇩f⇩m (subst x (Var (variant (FV (❙∃x❙. φ) ∪ FV ψ))))) ❙⟶ ψ)}›
using lang_singleton formsubst_functions_form formsubst_predicates formsubst_language_rename by auto
lemma prenex_props_forall: ‹P ∧ FV φ = FV ψ ∧ language {φ} = language {ψ} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ φ ⟷ I❙,β ⊨ ψ)) ⟹
P ∧ FV (❙∀x❙. φ) = FV (❙∀x❙. ψ) ∧ language {(❙∀x❙. φ)} = language {(❙∀x❙. ψ)} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ (❙∀x❙. φ) ⟷ I❙,β ⊨ (❙∀x❙. ψ)))
›
using lang_singleton by simp
lemma prenex_props_exists: ‹P ∧ FV φ = FV ψ ∧ language {φ} = language {ψ} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ φ ⟷ I❙,β ⊨ ψ)) ⟹
P ∧ FV (❙∃x❙. φ) = FV (❙∃x❙. ψ) ∧ language {(❙∃x❙. φ)} = language {(❙∃x❙. ψ)} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ (❙∃x❙. φ) ⟷ I❙,β ⊨ (❙∃x❙. ψ)))
›
using lang_singleton by simp
lemma prenex_right_props_imp0:
assumes ‹qfree φ›
shows ‹is_prenex ψ ⟹ is_prenex (prenex_right φ ψ)›
proof (induction ψ rule: measure_induct_rule [of size])
case (less ψ)
show ?case
proof (cases rule: is_prenex.cases[OF ‹is_prenex ψ›])
case (1 ξ)
then show ?thesis
by (simp add: assms prenex_right_qfree_case)
next
case (2 ξ x)
then have ‹prenex_right φ ψ = prenex_right_forall prenex_right φ x ξ›
using prenex_right_all_case by blast
then show ‹is_prenex (prenex_right φ ψ)›
using less 2 by (auto simp: Let_def prenex_formsubst1 size_indep_subst)
next
case (3 ξ x)
then have ‹∃y σ. prenex_right φ ψ = ❙∃y❙. prenex_right φ (ξ ⋅⇩f⇩m σ)›
using prenex_right_exists_shape_case by presburger
then obtain y σ where pr_is: ‹prenex_right φ ψ = ❙∃y❙. prenex_right φ (ξ ⋅⇩f⇩m σ)›
by blast
have size_xp: ‹size (ξ ⋅⇩f⇩m σ) < size ψ›
using 3(1) size_indep_subst by auto
have ‹is_prenex (ξ ⋅⇩f⇩m σ)›
using 3(2) prenex_formsubst1 by blast
then have ‹is_prenex (prenex_right φ (ξ ⋅⇩f⇩m σ))›
using less size_xp by blast
then show ?thesis
using is_prenex.intros(3) pr_is by presburger
qed
qed
lemma prenex_right_props_imp:
assumes ‹qfree φ›
shows ‹is_prenex ψ ⟹
is_prenex (prenex_right φ ψ) ∧
FV (prenex_right φ ψ) = FV (φ ❙⟶ ψ) ∧
language {prenex_right φ ψ} = language {(φ ❙⟶ ψ)} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ ((I❙,β ⊨ (prenex_right φ ψ)) ⟷ (I❙,β ⊨ (φ ❙⟶ ψ))))›
(is ‹is_prenex ψ ⟹ ?P ψ›)
proof (induction ψ rule: measure_induct_rule [of size])
case (less ψ)
show ?case
proof (cases rule: is_prenex.cases[OF ‹is_prenex ψ›])
case (1 ξ)
then show ?thesis
using prenex_right_qfree_case ‹qfree φ› is_prenex.intros(1) qfree.simps(3) by presburger
next
case (2 ξ x)
have pr_is1:‹prenex_right φ ψ = prenex_right_forall prenex_right φ x ξ›
using 2 prenex_right_all_case by blast
define y where ‹y = variant (FV φ ∪ FV (❙∀ x❙. ξ))›
then have pr_is2: ‹prenex_right φ ψ = ❙∀y❙. prenex_right φ (ξ ⋅⇩f⇩m subst x (Var y))›
using ‹qfree φ› 2(2) pr_is1 unfolding y_def by meson
have ‹is_prenex (ξ ⋅⇩f⇩m subst x (Var y))›
using prenex_formsubst1 2(2) by presburger
then have p_xps: ‹?P (ξ ⋅⇩f⇩m subst x (Var y))›
using less 2(1) less_Suc_eq plus_1_eq_Suc size.simps(4) size_indep_subst by presburger
have ‹is_prenex (prenex_right φ ψ)›
using prenex_right_props_imp0 ‹is_prenex ψ› ‹qfree φ› by blast
moreover have ‹FV (prenex_right φ ψ) = FV (φ ❙⟶ ψ)›
using prenex_right_forall_FV[of φ x ξ] by (metis 2(1) FV.simps(4) p_xps pr_is1 y_def)
moreover have ‹language {prenex_right φ ψ} = language {φ ❙⟶ ψ}›
using prenex_right_forall_language
by (metis "2"(1) functions_form.simps(4) lang_singleton p_xps pr_is1 predicates_form.simps(4) y_def)
moreover have ‹(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ I❙,β ⊨ prenex_right φ ψ = I❙,β ⊨ φ ❙⟶ ψ)›
by (metis "2"(1) holds.simps(4) p_xps pr_is2 prenex_right_forall_is y_def)
ultimately show ?thesis
by blast
next
case (3 ξ x)
have pr_is1:‹prenex_right φ ψ = prenex_right_exists prenex_right φ x ξ›
using 3 prenex_right_exist_case by blast
define y where ‹y = variant (FV φ ∪ FV (❙∃ x❙. ξ))›
then have pr_is2: ‹prenex_right φ ψ = ❙∃y❙. prenex_right φ (ξ ⋅⇩f⇩m subst x (Var y))›
using ‹qfree φ› 3(2) pr_is1 unfolding y_def by meson
have ‹is_prenex (ξ ⋅⇩f⇩m subst x (Var y))›
using prenex_formsubst1 3(2) by presburger
then have p_xps: ‹?P (ξ ⋅⇩f⇩m subst x (Var y))›
using less 3(1) less_Suc_eq plus_1_eq_Suc size.simps size_indep_subst by simp
have ‹is_prenex (prenex_right φ ψ)›
using prenex_right_props_imp0 ‹is_prenex ψ› ‹qfree φ› by blast
moreover have ‹FV (prenex_right φ ψ) = FV (φ ❙⟶ ψ)›
using prenex_right_exists_FV[of φ x ξ] by (metis 3(1) FV.simps(4) FV_exists p_xps
pr_is1 y_def)
moreover have ‹language {prenex_right φ ψ} = language {φ ❙⟶ ψ}›
using prenex_right_forall_language by (smt (verit) "3"(1) p_xps pr_is1
prenex_props_exists prenex_right_exists_language y_def)
moreover have ‹(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ I❙,β ⊨ prenex_right φ ψ = I❙,β ⊨ φ ❙⟶ ψ)›
by (smt (verit, best) "3"(1) p_xps pr_is2 prenex_props_exists prenex_right_exists_is y_def)
ultimately show ?thesis
by blast
qed
qed
lemma prenex_right_props:
‹qfree φ ∧ is_prenex ψ ⟹
is_prenex (prenex_right φ ψ) ∧
FV (prenex_right φ ψ) = FV (φ ❙⟶ ψ) ∧
language {prenex_right φ ψ} = language {(φ ❙⟶ ψ)} ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ ((I❙,β ⊨ (prenex_right φ ψ)) ⟷ (I❙,β ⊨ (φ ❙⟶ ψ))))›
using prenex_right_props_imp by meson
lemma prenex_left_props_imp0:
assumes ‹is_prenex ψ›
shows ‹is_prenex φ ⟹ is_prenex (prenex_left φ ψ)›
proof (induction φ rule: measure_induct_rule [of size])
case (less φ)
show ?case
proof (cases rule: is_prenex.cases[OF ‹is_prenex φ›])
case (1 ξ)
then show ?thesis
using ‹is_prenex φ› prenex_right_props prenex_left_qfree_case ‹is_prenex ψ› by presburger
next
case (2 ξ x)
then have ‹prenex_left φ ψ = prenex_left_forall prenex_left ξ x ψ›
using prenex_left_forall_case by blast
then show ‹is_prenex (prenex_left φ ψ)›
using less 2 by (metis is_prenex.intros(3) lessI plus_1_eq_Suc prenex_formsubst1 size.simps(4) size_indep_subst)
next
case (3 ξ x)
then have ‹∃y σ. prenex_left φ ψ = ❙∀y❙. prenex_left (ξ ⋅⇩f⇩m σ) ψ›
using prenex_left_exists_shape_case by presburger
then obtain y σ where pr_is: ‹prenex_left φ ψ = ❙∀y❙. prenex_left (ξ ⋅⇩f⇩m σ) ψ›
by blast
have size_xp: ‹size (ξ ⋅⇩f⇩m σ) < size φ›
using 3(1) size_indep_subst by auto
have ‹is_prenex (ξ ⋅⇩f⇩m σ)›
using 3(2) prenex_formsubst1 by blast
then have ‹is_prenex (prenex_left (ξ ⋅⇩f⇩m σ) ψ)›
using less size_xp by blast
then show ?thesis
using is_prenex.intros pr_is by presburger
qed
qed
lemma prenex_left_props_imp:
assumes ‹is_prenex ψ›
shows ‹is_prenex φ ⟹
is_prenex (prenex_left φ ψ) ∧
FV (prenex_left φ ψ) = FV (φ ❙⟶ ψ) ∧
(language {(prenex_left φ ψ)} = language {(φ ❙⟶ ψ)}) ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ prenex_left φ ψ ⟷ I❙,β ⊨ φ ❙⟶ ψ))›
(is ‹is_prenex φ ⟹ ?P φ›)
proof (induction φ rule: measure_induct_rule [of size])
case (less ξ)
show ?case
proof (cases rule: is_prenex.cases[OF ‹is_prenex ξ›])
case (1 ξ')
then show ?thesis
using prenex_right_qfree_case ‹is_prenex ψ›
by (simp add: prenex_left_qfree_case prenex_right_props)
next
case (2 ξ' x)
have pr_is1:‹prenex_left ξ ψ = prenex_left_forall prenex_left ξ' x ψ›
using 2 prenex_left_forall_case by blast
define y where ‹y = variant (FV (❙∀x❙. ξ') ∪ FV ψ)›
then have pr_is2: ‹prenex_left ξ ψ = ❙∃y❙. prenex_left (ξ' ⋅⇩f⇩m subst x (Var y)) ψ›
using ‹is_prenex ψ› 2(2) pr_is1 unfolding y_def by meson
have ‹is_prenex (ξ' ⋅⇩f⇩m subst x (Var y))›
using prenex_formsubst1 2(2) by presburger
then have p_xps: ‹?P (ξ' ⋅⇩f⇩m subst x (Var y))›
using less 2(1) less_Suc_eq plus_1_eq_Suc size.simps(4) size_indep_subst by presburger
have ‹is_prenex (prenex_left ξ ψ)›
using prenex_left_props_imp0 ‹is_prenex ξ› ‹is_prenex ψ› by blast
moreover have ‹FV (prenex_left ξ ψ) = FV (ξ ❙⟶ ψ)›
using prenex_left_forall_FV[of x ξ' ψ] by (metis 2(1) FV_exists p_xps pr_is1 y_def)
moreover have ‹language {prenex_left ξ ψ} = language {ξ ❙⟶ ψ}›
using prenex_left_forall_language
by (smt (verit, ccfv_threshold) 2(1) p_xps pr_is1 prenex_props_exists y_def)
moreover have ‹(⋀(I :: 'a intrp) β. dom I ≠ {} ⟹ I❙,β ⊨ prenex_left ξ ψ = I❙,β ⊨ ξ ❙⟶ ψ)›
by (metis "2"(1) holds_exists p_xps pr_is2 prenex_left_forall_is y_def)
ultimately show ‹?P ξ›
by blast
next
case (3 ξ' x)
have pr_is1:‹prenex_left ξ ψ = prenex_left_exists prenex_left ξ' x ψ›
using 3 prenex_left_exists_case by blast
define y where ‹y = variant (FV (❙∃ x❙. ξ') ∪ FV ψ)›
then have pr_is2: ‹prenex_left ξ ψ = ❙∀y❙. prenex_left (ξ' ⋅⇩f⇩m subst x (Var y)) ψ›
using ‹is_prenex ψ› 3(2) pr_is1 unfolding y_def by meson
have ‹is_prenex (ξ' ⋅⇩f⇩m subst x (Var y))›
using prenex_formsubst1 3(2) by presburger
then have p_xps: ‹?P (ξ' ⋅⇩f⇩m subst x (Var y))›
using less 3(1) less_Suc_eq plus_1_eq_Suc size.simps size_indep_subst by simp
have ‹is_prenex (prenex_left ξ ψ)›
using prenex_left_props_imp0 ‹is_prenex ξ› ‹is_prenex ψ› by blast
moreover have ‹FV (prenex_left ξ ψ) = FV (ξ ❙⟶ ψ)›
using prenex_left_exists_FV[of x ξ' ψ] by (metis 3(1) FV.simps(4) p_xps
pr_is1 y_def)
moreover have ‹language {prenex_left ξ ψ} = language {ξ ❙⟶ ψ}›
using prenex_left_exists_language[of x ξ' ψ]
by (smt (verit) 3(1) p_xps pr_is2 prenex_props_forall y_def)
moreover have ‹(∀(I :: 'a intrp) β. dom I ≠ {} ⟶
I❙,β ⊨ prenex_left ξ ψ = I❙,β ⊨ ξ ❙⟶ ψ)›
by (metis "3"(1) holds.simps(4) p_xps pr_is2 prenex_left_exists_is y_def)
ultimately show ‹?P ξ›
by blast
qed
qed
lemma prenex_left_props:
‹is_prenex φ ∧ is_prenex ψ ⟹
is_prenex (prenex_left φ ψ) ∧
FV (prenex_left φ ψ) = FV (φ ❙⟶ ψ) ∧
(language {(prenex_left φ ψ)} = language {(φ ❙⟶ ψ)}) ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙,β ⊨ prenex_left φ ψ ⟷ I❙,β ⊨ φ ❙⟶ ψ))›
using prenex_left_props_imp by meson
theorem prenex_props: ‹is_prenex (prenex φ) ∧ (FV (prenex φ) = FV φ) ∧
(language {prenex φ} = language {φ}) ∧
(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ (I❙, β ⊨ (prenex φ)) ⟷ (I❙, β ⊨ φ))›
proof (induction φ rule: form.induct)
case Bot
then show ?case
by (metis is_prenex.simps prenex.simps(1) qfree.simps(1))
next
case (Atom p ts)
then show ?case
using is_prenex.intros(1) prenex.simps(2) qfree.simps(2) by presburger
next
case (Implies φ ψ)
have ‹is_prenex (prenex (φ ❙⟶ ψ))›
using Implies prenex_left_props prenex.simps(3) by presburger
moreover have ‹FV (prenex (φ ❙⟶ ψ)) = FV (φ ❙⟶ ψ)›
using Implies prenex_left_props prenex.simps(3) FV.simps(3) by presburger
moreover have ‹language {prenex (φ ❙⟶ ψ)} = language {φ ❙⟶ ψ}›
using Implies prenex_left_props prenex.simps(3) lang_singleton
functions_form.simps(3) predicates_form.simps(3) by (metis prod.inject)
moreover have ‹∀(I::'a intrp) β. FOL_Semantics.dom I ≠ {} ⟶
I❙,β ⊨ prenex (φ ❙⟶ ψ) = I❙,β ⊨ φ ❙⟶ ψ›
using Implies prenex_left_props holds.simps(3) prenex.simps(3) by metis
ultimately show ?case by blast
next
case (Forall x φ)
have ‹is_prenex (prenex (❙∀x❙. φ))›
using Forall using is_prenex.intros(2) prenex.simps(4) by presburger
moreover have fv_indep_prenex: ‹FV (prenex (❙∀x❙. φ)) = FV (❙∀x❙. φ)›
using Forall FV.simps(4) prenex.simps(4) by presburger
moreover have ‹language {prenex (❙∀x❙. φ)} = language {❙∀x❙. φ}›
using Forall prenex.simps(4) functions_form.simps(4) predicates_form.simps(4)
unfolding language_def functions_forms_def predicates_def by simp
moreover have ‹(∀(I :: 'a intrp) β. dom I ≠ {} ⟶ I❙,β ⊨ prenex (❙∀x❙. φ) = I❙,β ⊨ (❙∀x❙. φ))›
using Forall holds.simps(4) by simp
ultimately show ?case by blast
qed
corollary is_prenex_prenex [simp]: ‹is_prenex (prenex φ)›
and FV_prenex [simp]: ‹FV (prenex φ) = FV φ›
and language_prenex [simp]: ‹language {prenex φ} = language {φ}›
by (auto simp: prenex_props)
corollary prenex_holds [simp]: ‹dom I ≠ {} ⟹ (I❙,β ⊨ (prenex φ)) ⟷ (I❙,β ⊨ φ)›
by (simp add: prenex_props)
lemma prenex_satisfies [simp]:
assumes "dom M ≠ {}"
shows "satisfies M {prenex φ} ⟷ satisfies M {φ}"
using assms prenex_holds by (fastforce simp: satisfies_def)
end