# Theory Deduction

chapter ‹Deduction›

(*<*)
theory Deduction imports Syntax
begin
(*>*)

text ‹We formalize deduction in a logical system that (shallowly) embeds
intuitionistic logic connectives and quantifiers over a signature containing
the numerals.›

section ‹Positive Logic Deduction›

locale Deduct =
Syntax_with_Numerals_and_Connectives
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
+
fixes
― ‹Provability of numeric formulas:›
prv :: "'fmla ⇒ bool"
― ‹Hilbert-style system for intuitionistic logic over $\longrightarrow$,$\land$,$\forall$,$\exists$.
($\bot$, $\lnot$ and $\lor$ will be included later.)
Hilbert-style is preferred since it requires the least amount of infrastructure.
(Later, natural deduction rules will also be defined.)›
assumes
― ‹Propositional rules and axioms. There is a single propositional rule, modus ponens.›
― ‹The modus ponens rule:›
prv_imp_mp:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ χ) ⟹ prv φ ⟹ prv χ"
and
― ‹The propositional intuitionitic axioms:›
prv_imp_imp_triv:
"⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ (imp χ φ))"
and
prv_imp_trans:
"⋀ φ χ ψ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp (imp φ (imp χ ψ))
(imp (imp φ χ) (imp φ ψ)))"
and
prv_imp_cnjL:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp (cnj φ χ) φ)"
and
prv_imp_cnjR:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp (cnj φ χ) χ)"
and
prv_imp_cnjI:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ (imp χ (cnj φ χ)))"
and
(*   *)
― ‹Predicate calculus (quantifier) rules and axioms›
― ‹The rules of universal and existential generalization:›
prv_all_imp_gen:
"⋀ x φ χ. x ∉ Fvars φ ⟹ prv (imp φ χ) ⟹ prv (imp φ (all x χ))"
and
prv_exi_imp_gen:
"⋀ x φ χ. x ∈ var ⟹ φ ∈ fmla ⟹ χ ∈ fmla ⟹
x ∉ Fvars χ ⟹ prv (imp φ χ) ⟹ prv (imp (exi x φ) χ)"
and
― ‹Two quantifier instantiation axioms:›
prv_all_inst:
"⋀ x φ t.
x ∈ var ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹
prv (imp (all x φ) (subst φ t x))"
and
prv_exi_inst:
"⋀ x φ t.
x ∈ var ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹
prv (imp (subst φ t x) (exi x φ))"
and
― ‹The equality axioms:›
prv_eql_refl:
"⋀ x. x ∈ var ⟹
prv (eql (Var x) (Var x))"
and
prv_eql_subst:
"⋀ φ x y.
x ∈ var ⟹ y ∈ var ⟹ φ ∈ fmla ⟹
prv ((imp (eql (Var x) (Var y))
(imp φ (subst φ (Var y) x))))"
begin

subsection ‹Properties of the propositional fragment›

lemma prv_imp_triv:
assumes phi: "φ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv ψ ⟹ prv (imp φ ψ)"
by (meson prv_imp_imp_triv prv_imp_mp imp phi psi)

lemma prv_imp_refl:
assumes phi: "φ ∈ fmla"
shows "prv (imp φ φ)"
by (metis prv_imp_imp_triv prv_imp_mp prv_imp_trans imp phi)

lemma prv_imp_refl2: "φ ∈ fmla ⟹ ψ ∈ fmla ⟹ φ = ψ ⟹ prv (imp φ ψ)"
using prv_imp_refl by auto

lemma prv_cnjI:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv φ ⟹ prv χ ⟹ prv (cnj φ χ)"
by (meson cnj prv_imp_cnjI prv_imp_mp imp phi chi)

lemma prv_cnjEL:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv (cnj φ χ) ⟹ prv φ"
using chi phi prv_imp_cnjL prv_imp_mp by blast

lemma prv_cnjER:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla"
shows "prv (cnj φ χ) ⟹ prv χ"
using chi phi prv_imp_cnjR prv_imp_mp by blast

lemma prv_prv_imp_trans:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
assumes 1: "prv (imp φ χ)" and 2: "prv (imp χ ψ)"
shows "prv (imp φ ψ)"
proof-
have "prv (imp φ (imp χ ψ))" by (simp add: 2 chi prv_imp_triv phi psi)
thus ?thesis by (metis 1 chi prv_imp_mp prv_imp_trans imp phi psi)
qed

lemma prv_imp_trans1:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv (imp (imp χ ψ) (imp (imp φ χ) (imp φ ψ)))"
by (meson chi prv_prv_imp_trans prv_imp_imp_triv prv_imp_trans imp phi psi)

lemma prv_imp_com:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
assumes "prv (imp φ (imp χ ψ))"
shows "prv (imp χ (imp φ ψ))"
by (metis (no_types) assms prv_prv_imp_trans prv_imp_imp_triv prv_imp_mp prv_imp_trans imp)

lemma prv_imp_trans2:
assumes phi: "φ ∈ fmla" and chi: "χ ∈ fmla" and psi: "ψ ∈ fmla"
shows "prv (imp (imp φ χ) (imp (imp χ ψ) (imp φ ψ)))"
using prv_imp_mp prv_imp_trans prv_imp_trans1 prv_imp_imp_triv
by (meson chi prv_imp_com imp phi psi)

lemma prv_imp_cnj:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp φ ψ) ⟹ prv (imp φ χ) ⟹ prv (imp φ (cnj ψ χ))"
proof -
assume "prv (imp φ ψ)"
moreover
assume "prv (imp φ χ)"
then have "prv (imp φ (imp ψ f))" if "prv (imp χ f)" "f ∈ fmla" for f
using that by (metis (no_types) assms imp prv_imp_imp_triv prv_prv_imp_trans)
moreover have "prv (imp φ (imp ψ ψ)) ⟹ prv (imp φ (imp φ ψ))"
using ‹prv (imp φ ψ)› by (metis (no_types) assms(1,3) imp prv_imp_com prv_prv_imp_trans)
ultimately show ?thesis
by (metis (no_types) assms cnj imp prv_imp_cnjI prv_imp_com prv_imp_mp prv_imp_trans)
qed

lemma prv_imp_imp_com:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ))
(imp χ (imp φ ψ)))"
by (metis (no_types) assms
prv_prv_imp_trans prv_imp_com prv_imp_imp_triv prv_imp_trans imp)

lemma prv_cnj_imp_monoR2:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
assumes "prv (imp φ (imp χ ψ))"
shows "prv (imp (cnj φ χ) ψ)"
proof -
have "prv (imp (cnj φ χ) (cnj φ χ))"
using prv_imp_refl by (blast intro: assms(1-3))
then have "prv (imp (imp (cnj φ χ) (imp (cnj φ χ) ψ)) (imp (cnj φ χ) ψ))"
by (metis (no_types) cnj imp assms(1-3) prv_imp_com prv_imp_mp prv_imp_trans)
then show ?thesis
by (metis (no_types) imp cnj assms prv_imp_cnjL prv_imp_cnjR prv_imp_com prv_imp_mp prv_prv_imp_trans)
qed

lemma prv_imp_imp_imp_cnj:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ))
(imp (cnj φ χ) ψ))"
proof-
have "prv (imp φ (imp (imp φ (imp χ ψ)) (imp χ ψ)))"
by (simp add: assms prv_imp_com prv_imp_refl)
hence "prv (imp φ (imp χ (imp (imp φ (imp χ ψ)) ψ)))"
by (metis (no_types, lifting) assms prv_prv_imp_trans prv_imp_imp_com imp)
hence "prv (imp (cnj φ χ)
(imp (imp φ (imp χ ψ)) ψ))"
thus ?thesis using assms prv_imp_com prv_imp_mp by (meson cnj imp)
qed

lemma prv_imp_cnj_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows
"prv (imp (imp (cnj φ χ) ψ)
(imp φ (imp χ ψ)))"
by (metis (no_types) assms cnj prv_prv_imp_trans prv_imp_cnjI prv_imp_com prv_imp_trans2 imp)

lemma prv_cnj_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
assumes "prv (imp (cnj φ χ) ψ)"
shows "prv (imp φ (imp χ ψ))"
using assms prv_imp_cnj_imp prv_imp_mp by (meson cnj imp)

text ‹Monotonicy of conjunction w.r.t. implication:›

lemma prv_cnj_imp_monoR:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (imp φ χ) (imp (imp φ ψ) (imp φ (cnj χ ψ))))"
by (meson assms cnj imp prv_cnj_imp prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_imp_cnj3L:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (imp φ1 χ) (imp (cnj φ1 φ2) χ))"
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2
by (metis cnj imp)

lemma prv_imp_cnj3R:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (imp φ2 χ) (imp (cnj φ1 φ2) χ))"
using prv_imp_cnjR prv_imp_mp prv_imp_trans2
by (metis assms cnj imp)

lemma prv_cnj_imp_mono:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
proof-
have "prv (imp (imp (cnj φ1 φ2) χ1) (imp (imp (cnj φ1 φ2) χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_cnj_imp_monoR[of "cnj φ1 φ2" χ1 χ2] assms by auto
hence "prv (imp (imp φ1 χ1) (imp (imp (cnj φ1 φ2) χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
by (metis (no_types) imp cnj assms prv_imp_cnj3L prv_prv_imp_trans)
hence "prv (imp (imp (cnj φ1 φ2) χ2) (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_imp_com assms by (meson cnj imp)
hence "prv (imp (imp φ2 χ2) (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_imp_cnj3R prv_imp_mp prv_imp_trans1
by (metis (no_types) assms cnj prv_prv_imp_trans imp)
thus ?thesis using prv_imp_com assms
by (meson cnj imp)
qed

lemma prv_cnj_mono:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ1 χ1)" and "prv (imp φ2 χ2)"
shows "prv (imp (cnj φ1 φ2) (cnj χ1 χ2))"
using assms prv_cnj_imp_mono prv_imp_mp
by (metis (mono_tags) cnj prv_prv_imp_trans prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_cnj_imp_monoR4:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ1 ∈ fmla" and "ψ2 ∈ fmla"
shows
"prv (imp (imp φ (imp χ ψ1))
(imp (imp φ (imp χ ψ2)) (imp φ (imp χ (cnj ψ1 ψ2)))))"
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_cnj_imp_monoR2)

lemma prv_imp_cnj4:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ1 ∈ fmla" and "ψ2 ∈ fmla"
shows "prv (imp φ (imp χ ψ1)) ⟹ prv (imp φ (imp χ ψ2)) ⟹ prv (imp φ (imp χ (cnj ψ1 ψ2)))"
by (simp add: assms prv_cnj_imp prv_imp_cnj prv_cnj_imp_monoR2)

lemma prv_cnj_imp_monoR5:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp φ1 (imp φ2 (cnj χ1 χ2)))))"
proof-
have "prv (imp (imp φ1 χ1) (imp (imp φ2 χ2) (imp (cnj φ1 φ2) (cnj χ1 χ2))))"
using prv_cnj_imp_mono[of φ1 φ2  χ1 χ2] assms by auto
hence "prv (imp (imp φ1 χ1) (imp (cnj φ1 φ2) (imp (imp φ2 χ2) (cnj χ1 χ2))))"
by (metis (no_types, lifting) assms cnj imp prv_imp_imp_com prv_prv_imp_trans)
hence "prv (imp (imp φ1 χ1) (imp φ1 (imp φ2 (imp (imp φ2 χ2) (cnj χ1 χ2)))))"
using prv_imp_cnj_imp prv_imp_mp prv_imp_trans2
by (metis (mono_tags) assms cnj prv_prv_imp_trans imp)
hence 1: "prv (imp (imp φ1 χ1) (imp φ1 (imp (imp φ2 χ2) (imp φ2  (cnj χ1 χ2)))))"
using prv_cnj_imp prv_imp_cnjR prv_imp_mp prv_imp_trans1
by (metis (no_types) assms cnj prv_cnj_imp_monoR prv_prv_imp_trans prv_imp_imp_triv imp)
thus ?thesis
by (metis (no_types, lifting) assms cnj imp prv_prv_imp_trans prv_imp_imp_com)
qed

lemma prv_imp_cnj5:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ1 χ1)" and "prv (imp φ2 χ2)"
shows "prv (imp φ1 (imp φ2 (cnj χ1 χ2)))"
by (simp add: assms prv_cnj_imp prv_cnj_mono)

text ‹Properties of formula equivalence:›

lemma prv_eqv_imp:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ χ) (eqv χ φ))"
by (simp add: assms prv_imp_cnj prv_imp_cnjL prv_imp_cnjR eqv_def)

lemma prv_eqv_eqv:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (eqv (eqv φ χ) (eqv χ φ))"
using assms prv_cnjI prv_eqv_imp eqv_def by auto

lemma prv_imp_eqvEL:
"φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ prv (eqv φ1 φ2) ⟹ prv (imp φ1 φ2)"
unfolding eqv_def by (meson cnj imp prv_imp_cnjL prv_imp_mp)

lemma prv_imp_eqvER:
"φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ prv (eqv φ1 φ2) ⟹ prv (imp φ2 φ1)"
unfolding eqv_def by (meson cnj imp prv_imp_cnjR prv_imp_mp)

lemma prv_eqv_imp_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (eqv φ χ) (imp (eqv χ ψ) (eqv φ ψ)))"
proof-
have "prv (imp (eqv φ χ) (imp (imp χ ψ) (imp φ ψ)))"
using assms prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
by (metis prv_imp_cnj3L eqv imp)
hence "prv (imp (eqv φ χ) (imp (eqv χ ψ) (imp φ ψ)))"
using prv_imp_cnjL prv_imp_mp prv_imp_trans2 eqv_def
by (metis (no_types) assms prv_imp_cnj3L prv_imp_com eqv imp)
hence 1: "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (imp φ ψ))"
using prv_cnj_imp_monoR2
by (simp add: assms(1) assms(2) assms(3))
have "prv (imp (eqv φ χ) (imp (imp ψ χ) (imp ψ φ)))"
using prv_imp_cnjR prv_imp_mp prv_imp_trans1 eqv_def
by (metis assms prv_cnj_imp_monoR2 prv_imp_triv imp)
hence "prv (imp (eqv φ χ) (imp (eqv χ ψ) (imp ψ φ)))"
by (metis assms cnj eqv_def imp prv_imp_cnj3R prv_prv_imp_trans)
hence 2: "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (imp ψ φ))"
using prv_cnj_imp_monoR2
by (metis (no_types, lifting) assms eqv imp)
have "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (eqv φ ψ))"
using 1 2  using assms prv_imp_cnj by (auto simp: eqv_def[of φ ψ])
thus ?thesis
qed

lemma prv_eqv_cnj_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (imp (cnj (eqv φ χ) (eqv χ ψ)) (eqv φ ψ))"
by (simp add: assms prv_eqv_imp_trans prv_cnj_imp_monoR2)

lemma prv_eqvI:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv (imp φ χ)" and "prv (imp χ φ)"
shows "prv (eqv φ χ)"
by (simp add: assms eqv_def prv_cnjI)

text ‹Formula equivalence is a congruence (i.e., an equivalence that
is compatible with the other connectives):›

lemma prv_eqv_refl: "φ ∈ fmla ⟹ prv (eqv φ φ)"
by (simp add: prv_cnjI prv_imp_refl eqv_def)

lemma prv_eqv_sym:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (eqv φ χ) ⟹ prv (eqv χ φ)"
using assms prv_cnjI prv_imp_cnjL prv_imp_cnjR prv_imp_mp eqv_def
by (meson prv_eqv_imp eqv)

lemma prv_eqv_trans:
assumes "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (eqv φ χ) ⟹ prv (eqv χ ψ) ⟹ prv (eqv φ ψ)"
using assms prv_cnjI prv_cnj_imp_monoR2 prv_imp_mp prv_imp_trans1 prv_imp_imp_triv eqv_def
by (metis prv_prv_imp_trans prv_imp_cnjL prv_imp_cnjR eqv imp)

lemma imp_imp_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (eqv (imp φ1 χ) (imp φ2 χ)))"
proof -
have f: "prv (imp (eqv φ1 φ2) (eqv (imp φ1 χ) (imp φ2 χ)))"
if "prv (imp (eqv φ1 φ2) (imp (imp φ2 χ) (imp φ1 χ)))" "prv (imp (eqv φ1 φ2) (imp (imp φ1 χ) (imp φ2 χ)))"
using assms that prv_imp_cnj by (auto simp: eqv_def)
moreover have "(prv (imp (eqv φ1 φ2) (imp φ1 φ2)) ∧ prv (imp (eqv φ1 φ2) (imp φ2 φ1)))"
by (simp add: assms eqv_def prv_imp_cnjL prv_imp_cnjR)
ultimately show ?thesis
by (metis (no_types) assms eqv imp prv_imp_trans2 prv_prv_imp_trans)
qed

lemma imp_imp_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv χ1 χ2) (eqv (imp φ χ1) (imp φ χ2)))"
by (simp add: assms prv_cnj_mono prv_imp_trans1 eqv_def)

lemma imp_imp_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (eqv (imp φ1 χ1) (imp φ2 χ2))))"
proof-
have "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (cnj (eqv (imp φ1 χ1) (imp φ2 χ1))
(eqv (imp φ2 χ1) (imp φ2 χ2)))))"
using prv_imp_cnj5
[OF _ _ _ _ imp_imp_compat_eqvL[of φ1 φ2 χ1] imp_imp_compat_eqvR[of φ2 χ1 χ2]] assms by auto
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (cnj (eqv (imp φ1 χ1) (imp φ2 χ1))
(eqv (imp φ2 χ1) (imp φ2 χ2))))"
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (eqv (imp φ1 χ1) (imp φ2 χ2)))"
using assms prv_eqv_cnj_trans[of "imp φ1 χ1" "imp φ2 χ1" "imp φ2 χ2"]
using prv_imp_mp prv_imp_trans2
by (metis (no_types) cnj prv_prv_imp_trans eqv imp)
thus ?thesis using assms prv_cnj_imp by auto
qed

lemma imp_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)"
shows "prv (eqv (imp φ1 χ) (imp φ2 χ))"
using assms prv_imp_mp imp_imp_compat_eqvL by (meson eqv imp)

lemma imp_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv χ1 χ2)"
shows "prv (eqv (imp φ χ1) (imp φ χ2))"
using assms prv_imp_mp imp_imp_compat_eqvR by (meson eqv imp)

lemma imp_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (eqv χ1 χ2)"
shows "prv (eqv (imp φ1 χ1) (imp φ2 χ2))"
using assms prv_imp_mp imp_imp_compat_eqv by (metis eqv imp)

(*  *)

lemma imp_cnj_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (eqv (cnj φ1 χ) (cnj φ2 χ)))"
proof -
have "prv (imp (imp (imp φ2 φ1) (imp (cnj φ2 χ) (cnj φ1 χ)))
(imp (cnj (imp φ1 φ2) (imp φ2 φ1)) (cnj (imp (cnj φ1 χ) (cnj φ2 χ))
(imp (cnj φ2 χ) (cnj φ1 χ)))))"
by (metis (no_types) imp cnj assms prv_imp_mp assms prv_cnj_imp_mono prv_imp_com prv_imp_refl)
then show ?thesis
by (metis (no_types) imp cnj assms prv_imp_mp assms eqv_def prv_cnj_imp_mono prv_imp_com prv_imp_refl)
qed

lemma imp_cnj_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv χ1 χ2) (eqv (cnj φ χ1) (cnj φ χ2)))"
by (simp add: assms prv_cnj_mono prv_imp_cnj3R prv_imp_cnj4 prv_imp_cnjL prv_imp_triv eqv_def)

lemma imp_cnj_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
shows "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (eqv (cnj φ1 χ1) (cnj φ2 χ2))))"
proof-
have "prv (imp (eqv φ1 φ2) (imp (eqv χ1 χ2) (cnj (eqv (cnj φ1 χ1) (cnj φ2 χ1))
(eqv (cnj φ2 χ1) (cnj φ2 χ2)))))"
using prv_imp_cnj5
[OF _ _ _ _ imp_cnj_compat_eqvL[of φ1 φ2 χ1] imp_cnj_compat_eqvR[of φ2 χ1 χ2]] assms by auto
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (cnj (eqv (cnj φ1 χ1) (cnj φ2 χ1))
(eqv (cnj φ2 χ1) (cnj φ2 χ2))))"
hence "prv (imp (cnj (eqv φ1 φ2) (eqv χ1 χ2)) (eqv (cnj φ1 χ1) (cnj φ2 χ2)))"
using assms prv_eqv_cnj_trans[of "cnj φ1 χ1" "cnj φ2 χ1" "cnj φ2 χ2"]
using prv_imp_mp prv_imp_trans2
by (metis (no_types) cnj prv_prv_imp_trans eqv)
thus ?thesis using assms prv_cnj_imp by auto
qed

lemma cnj_compat_eqvL:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)"
shows "prv (eqv (cnj φ1 χ) (cnj φ2 χ))"
using assms prv_imp_mp imp_cnj_compat_eqvL by (meson eqv cnj)

lemma cnj_compat_eqvR:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv χ1 χ2)"
shows "prv (eqv (cnj φ χ1) (cnj φ χ2))"
using assms prv_imp_mp imp_cnj_compat_eqvR by (meson eqv cnj)

lemma cnj_compat_eqv:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (eqv χ1 χ2)"
shows "prv (eqv (cnj φ1 χ1) (cnj φ2 χ2))"
using assms prv_imp_mp imp_cnj_compat_eqv by (metis eqv imp cnj)

lemma prv_eqv_prv:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv φ" and "prv (eqv φ χ)"
shows "prv χ"
by (metis assms prv_imp_cnjL prv_imp_mp eqv eqv_def imp)

lemma prv_eqv_prv_rev:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv φ" and "prv (eqv χ φ)"
shows "prv χ"
using assms prv_eqv_prv prv_eqv_sym by blast

lemma prv_imp_eqv_transi:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ χ1)" and "prv (eqv χ1 χ2)"
shows "prv (imp φ χ2)"
by (meson assms imp imp_compat_eqvR prv_eqv_prv)

lemma prv_imp_eqv_transi_rev:
assumes "φ ∈ fmla" and "χ1 ∈ fmla" and "χ2 ∈ fmla"
assumes "prv (imp φ χ2)" and "prv (eqv χ1 χ2)"
shows "prv (imp φ χ1)"
by (meson assms prv_eqv_sym prv_imp_eqv_transi)

lemma prv_eqv_imp_transi:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (imp φ2 χ)"
shows "prv (imp φ1 χ)"
by (meson assms prv_imp_eqv_transi prv_imp_refl prv_prv_imp_trans)

lemma prv_eqv_imp_transi_rev:
assumes "φ1 ∈ fmla" and "φ2 ∈ fmla" and "χ ∈ fmla"
assumes "prv (eqv φ1 φ2)" and "prv (imp φ1 χ)"
shows "prv (imp φ2 χ)"
by (meson assms prv_eqv_imp_transi prv_eqv_sym)

lemma prv_imp_monoL: "φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp χ ψ) ⟹ prv (imp (imp φ χ) (imp φ ψ))"
by (meson imp prv_imp_mp prv_imp_trans1)

lemma prv_imp_monoR: "φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp ψ χ) ⟹ prv (imp (imp χ φ) (imp ψ φ))"
by (meson imp prv_imp_mp prv_imp_trans2)

text ‹More properties involving conjunction:›

lemma prv_cnj_com_imp:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
shows "prv (imp (cnj φ χ) (cnj χ φ))"
by (simp add: prv_imp_cnj prv_imp_cnjL prv_imp_cnjR)

lemma prv_cnj_com:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
shows "prv (eqv (cnj φ χ) (cnj χ φ))"

lemma prv_cnj_assoc_imp1:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (imp (cnj φ (cnj χ ψ)) (cnj (cnj φ χ) ψ))"
by (simp add: prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_cnjR prv_imp_triv)

lemma prv_cnj_assoc_imp2:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (imp (cnj (cnj φ χ) ψ) (cnj φ (cnj χ ψ)))"
proof -
have "prv (imp (cnj φ χ) (imp ψ φ)) ∧ cnj χ ψ ∈ fmla ∧ cnj φ χ ∈ fmla"
by (meson χ φ ψ cnj imp prv_cnj_imp_monoR2 prv_imp_imp_triv prv_prv_imp_trans)
then show ?thesis
using χ φ ψ cnj imp prv_cnj_imp_monoR2 prv_imp_cnj4 prv_imp_cnjI prv_imp_triv by presburger
qed

lemma prv_cnj_assoc:
assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
shows "prv (eqv (cnj φ (cnj χ ψ)) (cnj (cnj φ χ) ψ))"
by (simp add: prv_cnj_assoc_imp1 prv_cnj_assoc_imp2 prv_eqvI)

lemma prv_cnj_com_imp3:
assumes "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla"
shows "prv (imp (cnj φ1 (cnj φ2 φ3))
(cnj φ2 (cnj φ1 φ3)))"
by (simp add: assms prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_cnjL prv_imp_refl prv_imp_triv)

subsection ‹Properties involving quantifiers›

text ‹Fundamental properties:›

lemma prv_allE:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv (all x φ) ⟹ prv (subst φ t x)"
using assms prv_all_inst prv_imp_mp by (meson subst all)

lemma prv_exiI:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv (subst φ t x) ⟹ prv (exi x φ)"
using assms prv_exi_inst prv_imp_mp by (meson subst exi)

lemma prv_imp_imp_exi:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars φ"
shows "prv (imp (exi x (imp φ χ)) (imp φ (exi x χ)))"
using assms imp exi Fvars_exi Fvars_imp Un_iff assms prv_exi_imp_gen prv_exi_inst prv_imp_mp
prv_imp_trans1 member_remove remove_def subst_same_Var by (metis (full_types) Var)

lemma prv_imp_exi:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
shows "x ∉ Fvars φ ⟹ prv (exi x (imp φ χ)) ⟹ prv (imp φ (exi x χ))"
using assms prv_imp_imp_exi prv_imp_mp by (meson exi imp)

lemma prv_exi_imp:
assumes x: "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars χ" and d: "prv (all x (imp φ χ))"
shows "prv (imp (exi x φ) χ)"
proof-
have "prv (imp φ χ)" using prv_allE[of x _ "Var x", of "imp φ χ"] assms by simp
thus ?thesis using assms prv_exi_imp_gen by blast
qed

lemma prv_all_imp:
assumes x: "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla"
assumes "x ∉ Fvars φ" and "prv (all x (imp φ χ))"
shows "prv (imp φ (all x χ))"
proof-
have "prv (imp φ χ)" using prv_allE[of x _ "Var x", of "imp φ χ"] assms by simp
thus ?thesis using assms prv_all_imp_gen by blast
qed

lemma prv_exi_inst_same:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
shows "prv (imp φ (exi x φ))"
proof-
have 0: "φ = subst φ (Var x) x" using assms by simp
show ?thesis
apply(subst 0)
using assms by (intro prv_exi_inst) auto
qed

lemma prv_exi_cong:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)"
shows "prv (imp (exi x φ) (exi x χ))"
proof-
have 0: "prv (imp χ (exi x χ))" using assms prv_exi_inst_same by auto
show ?thesis
using assms apply(intro prv_exi_imp_gen)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using "0" exi prv_prv_imp_trans by blast .
qed

lemma prv_exi_congW:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)" "prv (exi x φ)"
shows "prv (exi x χ)"
by (meson exi assms prv_exi_cong prv_imp_mp)

lemma prv_all_cong:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)"
shows "prv (imp (all x φ) (all x χ))"
proof-
have 0: "prv (imp (all x φ) χ)" using assms
by (metis Var all prv_all_inst prv_prv_imp_trans subst_same_Var)
show ?thesis by (simp add: "0" assms prv_all_imp_gen)
qed

lemma prv_all_congW:
assumes "φ ∈ fmla" "χ ∈ fmla" "x ∈ var"
and "prv (imp φ χ)" "prv (all x φ)"
shows "prv (all x χ)"
by (meson all assms prv_all_cong prv_imp_mp)

text ‹Quantifiers versus free variables and substitution:›

lemma exists_no_Fvars: "∃ φ. φ ∈ fmla ∧ prv φ ∧ Fvars φ = {}"
proof-
obtain n where [simp]: "n ∈ num" using numNE by blast
show ?thesis
by (intro exI[of _ "imp (eql n n) (eql n n)"]) (simp add: prv_imp_refl)
qed

lemma prv_all_gen:
assumes "x ∈ var" and "φ ∈ fmla"
assumes "prv φ" shows "prv (all x φ)"
using assms prv_all_imp_gen prv_imp_mp prv_imp_triv exists_no_Fvars by blast

lemma all_subst_rename_prv:
"φ ∈ fmla ⟹ x ∈ var ⟹ y ∈ var ⟹
y ∉ Fvars φ ⟹ prv (all x φ) ⟹ prv (all y (subst φ (Var y) x))"

lemma allE_id:
assumes "y ∈ var" and "φ ∈ fmla"
assumes "prv (all y φ)"
shows "prv φ"
using assms prv_allE by (metis Var subst_same_Var)

lemma prv_subst:
assumes "x ∈ var" and "φ ∈ fmla" and "t ∈ trm"
shows "prv φ ⟹ prv (subst φ t x)"
by (simp add: assms prv_allE prv_all_gen)

lemma prv_rawpsubst:
assumes "φ ∈ fmla" and "snd  (set txs) ⊆ var" and "fst  (set txs) ⊆ trm"
and "prv φ"
shows "prv (rawpsubst φ txs)"
using assms apply (induct txs arbitrary: φ)
subgoal by auto
subgoal for tx txs φ by (cases tx) (auto intro: prv_subst) .

lemma prv_psubst:
assumes "φ ∈ fmla" and "snd  (set txs) ⊆ var" and "fst  (set txs) ⊆ trm"
and "prv φ"
shows "prv (psubst φ txs)"
proof-
define us where us: "us ≡ getFrN (map snd txs) (map fst txs) [φ] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ Fvars φ = {}"
"set us ∩ ⋃ (FvarsT  (fst  (set txs))) = {}"
"set us ∩ snd  (set txs) = {}"
"length us = length txs"
"distinct us"
using assms unfolding us
using getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
apply -
subgoal by auto
subgoal by fastforce
subgoal by auto
subgoal by (fastforce simp: image_iff)
by auto
show ?thesis using assms us_facts unfolding psubst_def
by (auto simp: Let_def us[symmetric] intro!: prv_rawpsubst rawpsubst dest!: set_zip_D)
qed

lemma prv_eqv_rawpsubst:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ snd  set txs ⊆ var ⟹ fst  set txs ⊆ trm ⟹ prv (eqv φ ψ) ⟹
prv (eqv (rawpsubst φ txs) (rawpsubst ψ txs))"
by (metis eqv prv_rawpsubst rawpsubst_eqv)

lemma prv_eqv_psubst:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ snd  set txs ⊆ var ⟹ fst  set txs ⊆ trm ⟹ prv (eqv φ ψ) ⟹
distinct (map snd txs) ⟹
prv (eqv (psubst φ txs) (psubst ψ txs))"
by (metis eqv prv_psubst psubst_eqv)

lemma prv_all_imp_trans:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (all x (imp φ χ)) ⟹ prv (all x (imp χ ψ)) ⟹ prv (all x (imp φ ψ))"
by (metis Var assms prv_allE prv_all_gen prv_prv_imp_trans imp subst_same_Var)

lemma prv_all_imp_cnj:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (all x (imp φ (imp ψ χ))) ⟹ prv (all x (imp (cnj ψ φ) χ))"
by (metis Var assms cnj prv_allE prv_all_gen prv_imp_com prv_cnj_imp_monoR2 imp subst_same_Var)

lemma prv_all_imp_cnj_rev:
assumes "x ∈ var" and "φ ∈ fmla" and "χ ∈ fmla" and "ψ ∈ fmla"
shows "prv (all x (imp (cnj φ ψ) χ)) ⟹ prv (all x (imp φ (imp ψ χ)))"
by (metis (full_types) Var assms cnj prv_allE prv_all_gen prv_cnj_imp imp subst_same_Var)

subsection ‹Properties concerning equality›

lemma prv_eql_reflT:
assumes t: "t ∈ trm"
shows "prv (eql t t)"
proof-
obtain x where x: "x ∈ var" using var_NE by auto
show ?thesis using prv_subst[OF x _ t prv_eql_refl[OF x]] x t by simp
qed

lemma prv_eql_subst_trm:
assumes xx: "x ∈ var" and φ: "φ ∈ fmla" and "t1 ∈ trm" and "t2 ∈ trm"
shows "prv ((imp (eql t1 t2)
(imp (subst φ t1 x) (subst φ t2 x))))"
proof-
have "finite ({x} ∪ FvarsT t1 ∪ FvarsT t2 ∪ Fvars φ)" (is "finite ?A")
by (simp add: assms finite_FvarsT finite_Fvars)
then obtain y where y: "y ∈ var" and "y ∉ ?A"
by (meson finite_subset infinite_var subset_iff)
hence xy: "x ≠ y" and yt1: "y ∉ FvarsT t1" and yt2: "y ∉ FvarsT t2" and yφ: "y ∉ Fvars φ" by auto
have x: "x ∉ Fvars (subst φ (Var y) x)" using xy y assms by simp
hence 1: "prv (imp (eql t1 (Var y)) (imp (subst φ t1 x) (subst φ (Var y) x)))"
using xy y assms prv_subst[OF xx _ _ prv_eql_subst[OF xx y φ]] by simp
have yy: "y ∉ Fvars (subst φ t1 x)" using yt1 yφ assms by simp
from prv_subst[OF y _ _ 1, of t2]
show ?thesis using xy yt1 yt2 yφ x xx y yy assms by auto
qed

lemma prv_eql_subst_trm2:
assumes "x ∈ var" and "φ ∈ fmla" and "t1 ∈ trm" and "t2 ∈ trm"
assumes "prv (eql t1 t2)"
shows "prv (imp (subst φ t1 x) (subst φ t2 x))"
by (meson assms eql imp local.subst prv_eql_subst_trm prv_imp_mp)

lemma prv_eql_sym:
assumes [simp]: "t1 ∈ trm" "t2 ∈ trm"
shows "prv (imp (eql t1 t2) (eql t2 t1))"
proof-
obtain x where x[simp]: "x ∈ var" "x ∉ FvarsT t1"
by (meson assms finite_FvarsT finite_subset infinite_var subsetI)
thus ?thesis using prv_eql_subst_trm[of x "eql (Var x) t1" t1 t2, simplified]
by (meson assms eql imp prv_eql_reflT prv_imp_com prv_imp_mp)
qed

lemma prv_prv_eql_sym: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ prv (eql t1 t2) ⟹ prv (eql t2 t1)"
by (meson eql prv_eql_sym prv_imp_mp)

lemma prv_all_eql:
assumes "x ∈ var" and "y ∈ var" and "φ ∈ fmla" and "t1 ∈ trm" and "t2 ∈ trm"
shows "prv (all x ((imp (eql t1 t2)
(imp (subst φ t2 y) (subst φ t1 y)))))"
by (meson subst assms prv_all_gen prv_prv_imp_trans prv_eql_subst_trm prv_eql_sym eql imp)

lemma prv_eql_subst_trm_rev:
assumes "t1 ∈ trm" and "t2 ∈ trm" and "φ ∈ fmla" and "y ∈ var"
shows
"prv ((imp (eql t1 t2)
(imp (subst φ t2 y) (subst φ t1 y))))"
using assms prv_all_eql prv_all_inst prv_imp_mp subst_same_Var
by (meson subst prv_prv_imp_trans prv_eql_subst_trm prv_eql_sym eql imp)

lemma prv_eql_subst_trm_rev2:
assumes "x ∈ var" and "φ ∈ fmla" and "t1 ∈ trm" and "t2 ∈ trm"
assumes "prv (eql t1 t2)"
shows "prv (imp (subst φ t2 x) (subst φ t1 x))"
by (meson assms eql imp local.subst prv_eql_subst_trm_rev prv_imp_mp)

lemma prv_eql_subst_trm_eqv:
assumes "x ∈ var" and "φ ∈ fmla" and "t1 ∈ trm" and "t2 ∈ trm"
assumes "prv (eql t1 t2)"
shows "prv (eqv (subst φ t1 x) (subst φ t2 x))"
using assms prv_eql_subst_trm2[OF assms] prv_eql_subst_trm_rev2[OF assms]
prv_eqvI by auto

lemma prv_eql_subst_trm_id:
assumes "y ∈ var" "φ ∈ fmla" and "n ∈ num"
shows "prv (imp (eql (Var y) n) (imp φ (subst φ n y)))"
using assms prv_eql_subst_trm
by (metis Var in_num subst_same_Var)

lemma prv_eql_subst_trm_id_back:
assumes "y ∈ var" "φ ∈ fmla" and "n ∈ num"
shows "prv (imp (eql (Var y) n) (imp (subst φ n y) φ))"
by (metis Var assms in_num prv_eql_subst_trm_rev subst_same_Var)

lemma prv_eql_subst_trm_id_rev:
assumes "y ∈ var" "φ ∈ fmla" and "n ∈ num"
shows "prv (imp (eql n (Var y)) (imp φ (subst φ n y)))"
using assms prv_eql_subst_trm_rev by (metis Var in_num subst_same_Var)

lemma prv_eql_subst_trm_id_back_rev:
assumes "y ∈ var" "φ ∈ fmla" and "n ∈ num"
shows "prv (imp (eql n (Var y)) (imp (subst φ n y) φ))"
by (metis (full_types) Var assms in_num prv_eql_subst_trm subst_same_Var)

lemma prv_eql_imp_trans_rev:
assumes t1[simp]: "t1 ∈ trm" and t2[simp]: "t2 ∈ trm" and t3[simp]: "t3 ∈ trm"
shows "prv (imp (eql t1 t2) (imp (eql t1 t3) (eql t2 t3)))"
proof-
obtain y1 where y1[simp]: "y1 ∈ var" and "y1 ∉ FvarsT t1 ∪ FvarsT t2 ∪ FvarsT t3"
using finite_FvarsT finite_subset infinite_var subsetI t1 t2 t3
by (metis (full_types) infinite_Un)
hence [simp]: "y1 ∉ FvarsT t1" "y1 ∉ FvarsT t2" "y1 ∉  FvarsT t3" by auto
obtain y2 where y2[simp]: "y2 ∈ var" and "y2 ∉ FvarsT t1 ∪ FvarsT t2 ∪ FvarsT t3 ∪ {y1}"
using finite_FvarsT finite_subset infinite_var subsetI t1 t2 t3
by (metis (full_types) finite_insert infinite_Un insert_is_Un)
hence [simp]: "y2 ∉ FvarsT t1" "y2 ∉ FvarsT t2" "y2 ∉  FvarsT t3" "y1 ≠ y2" by auto
have 0: "prv (imp (eql (Var y1) (Var y2))
(imp (eql (Var y1) t3) (eql (Var y2) t3)))"
using prv_eql_subst[OF y1 y2, of "eql (Var y1) t3"] by simp
note 1 = prv_subst[OF y1 _ t1 0, simplified]
show ?thesis using prv_subst[OF y2 _ t2 1, simplified] .
qed

lemma prv_eql_imp_trans:
assumes t1[simp]: "t1 ∈ trm" and t2[simp]: "t2 ∈ trm" and t3[simp]: "t3 ∈ trm"
shows "prv (imp (eql t1 t2) (imp (eql t2 t3) (eql t1 t3)))"
by (meson eql imp prv_eql_sym prv_eql_imp_trans_rev prv_prv_imp_trans t1 t2 t3)

lemma prv_eql_trans:
assumes t1[simp]: "t1 ∈ trm" and t2[simp]: "t2 ∈ trm" and t3[simp]: "t3 ∈ trm"
and "prv (eql t1 t2)" and "prv (eql t2 t3)"
shows "prv (eql t1 t3)"
by (meson assms cnj eql prv_cnjI prv_cnj_imp_monoR2 prv_eql_imp_trans prv_imp_mp)

subsection ‹The equivalence between soft substitution and substitution›

lemma prv_subst_imp_softSubst:
assumes [simp,intro!]: "x ∈ var" "t ∈ trm" "φ ∈ fmla" "x ∉ FvarsT t"
shows "prv (imp (subst φ t x) (softSubst φ t x))"
unfolding softSubst_def by (rule prv_imp_exi)
(auto simp: prv_eql_reflT prv_imp_cnj prv_imp_refl prv_imp_triv subst_compose_same
intro: prv_exiI[of _ _ t])

lemma prv_subst_implies_softSubst:
assumes "x ∈ var" "t ∈ trm" "φ ∈ fmla"
and "x ∉ FvarsT t"
and "prv (subst φ t x)"
shows "prv (softSubst φ t x)"
using assms prv_subst_imp_softSubst
by (metis Var cnj eql exi subst prv_imp_mp softSubst_def)

lemma prv_softSubst_imp_subst:
assumes [simp,intro!]: "x ∈ var" "t ∈ trm" "φ ∈ fmla" "x ∉ FvarsT t"
shows "prv (imp (softSubst φ t x) (subst φ t x))"
unfolding softSubst_def apply(rule prv_exi_imp_gen)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (metis Var assms(1-3) eql subst prv_cnj_imp_monoR2 prv_eql_subst_trm subst_same_Var) .

lemma prv_softSubst_implies_subst:
assumes "x ∈ var" "t ∈ trm" "φ ∈ fmla"
and "x ∉ FvarsT t"
and "prv (softSubst φ t x)"
shows "prv (subst φ t x)"
by (metis Var assms cnj eql exi local.subst prv_imp_mp prv_softSubst_imp_subst softSubst_def)

lemma prv_softSubst_eqv_subst:
assumes [simp,intro!]: "x ∈ var" "t ∈ trm" "φ ∈ fmla" "x ∉ FvarsT t"
shows "prv (eqv (softSubst φ t x) (subst φ t x))"
by (metis Var assms cnj eql exi local.subst prv_eqvI prv_softSubst_imp_subst prv_subst_imp_softSubst softSubst_def)

end ― ‹context @{locale Deduct}›

section ‹Deduction Considering False›

locale Deduct_with_False =
Syntax_with_Connectives_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
+
Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and num
and prv
+
assumes
prv_fls[simp,intro]: "⋀φ. prv (imp fls φ)"
begin

subsection ‹Basic properties of False (fls)›

lemma prv_expl:
assumes "φ ∈ fmla"
assumes "prv fls"
shows "prv φ"
using assms prv_imp_mp by blast

lemma prv_cnjR_fls: "φ ∈ fmla ⟹ prv (eqv (cnj fls φ) fls)"

lemma prv_cnjL_fls: "φ ∈ fmla ⟹ prv (eqv (cnj φ fls) fls)"

subsection ‹Properties involving negation›

text ‹Recall that negation has been defined from implication and False.›

lemma prv_imp_neg_fls:
assumes "φ ∈ fmla"
shows "prv (imp φ (imp (neg φ) fls))"
using assms prv_imp_com prv_imp_refl neg_def by auto

lemma prv_neg_fls:
assumes "φ ∈ fmla"
assumes "prv φ" and "prv (neg φ)"
shows "prv fls"
by (metis assms prv_imp_mp fls neg_def)

lemma prv_imp_neg_neg:
assumes "φ ∈ fmla"
shows "prv (imp φ (neg (neg φ)))"
using assms prv_imp_neg_fls neg_def by auto

lemma prv_neg_neg:
assumes "φ ∈ fmla"
assumes "prv φ"
shows "prv (neg (neg φ))"
by (metis assms prv_imp_mp prv_imp_neg_fls neg neg_def)

lemma prv_imp_imp_neg_rev:
assumes "φ ∈ fmla" and "χ ∈ fmla"
shows "prv (imp (imp φ χ)
(imp (neg χ) (neg φ)))"
unfolding neg_def using prv_imp_trans2[OF assms fls] .

lemma prv_imp_neg_rev:
assumes "φ ∈ fmla" and "χ ∈ fmla"
assumes "prv (imp φ χ)"
shows "prv (imp (neg χ) (neg φ))"
by (meson assms imp neg prv_imp_imp_neg_rev prv_imp_mp)

lemma prv_eqv_neg_prv_fls:
"φ ∈ fmla ⟹
prv (eqv φ (neg φ)) ⟹ prv fls"
by (metis cnj fls neg neg_def prv_cnj_imp_monoR2 prv_eqv_imp_transi prv_imp_cnj prv_imp_eqvER prv_imp_mp prv_imp_neg_rev)

lemma prv_eqv_eqv_neg_prv_fls:
"φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (eqv φ χ) ⟹ prv (eqv φ (neg χ))⟹ prv fls"
by (meson neg prv_eqv_neg_prv_fls prv_eqv_sym prv_eqv_trans)

lemma prv_eqv_eqv_neg_prv_fls2:
"φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (eqv φ χ) ⟹ prv (eqv χ (neg φ))⟹ prv fls"

lemma prv_neg_imp_imp_trans:
assumes "φ ∈ fmla" "χ ∈ fmla"  "ψ ∈ fmla"
and "prv (neg φ)"
and "prv (imp χ (imp ψ φ))"
shows "prv (imp χ (neg ψ))"
unfolding neg_def
by (metis assms cnj fls neg_def prv_cnj_imp prv_cnj_imp_monoR2 prv_prv_imp_trans)

lemma prv_imp_neg_imp_neg_imp:
assumes "φ ∈ fmla" "χ ∈ fmla"
and "prv (neg φ)"
shows "prv ((imp χ (neg (imp χ φ))))"
by (metis assms fls imp neg_def prv_imp_com prv_imp_monoL)

lemma prv_prv_neg_imp_neg:
assumes "φ ∈ fmla" "χ ∈ fmla"
and "prv φ" and "prv χ"
shows "prv (neg (imp φ (neg χ)))"
by (meson assms imp neg prv_imp_mp prv_imp_neg_imp_neg_imp prv_neg_neg)

lemma prv_imp_neg_imp_cnjL:
assumes "φ ∈ fmla" "φ1 ∈ fmla" "φ2 ∈ fmla"
and "prv (imp φ (neg φ1))"
shows "prv (imp φ (neg (cnj φ1 φ2)))"
unfolding neg_def by (metis assms cnj fls neg neg_def prv_imp_cnj3L prv_prv_imp_trans)

lemma prv_imp_neg_imp_cnjR:
assumes "φ ∈ fmla" "φ1 ∈ fmla" "φ2 ∈ fmla"
and "prv (imp φ (neg φ2))"
shows "prv (imp φ (neg (cnj φ1 φ2)))"
unfolding neg_def by (metis assms cnj fls neg neg_def prv_imp_cnj3R prv_prv_imp_trans)

text ‹Negation versus quantifiers:›

lemma prv_all_neg_imp_neg_exi:
assumes x: "x ∈ var" and φ: "φ ∈ fmla"
shows "prv (imp (all x (neg φ)) (neg (exi x φ)))"
proof-
have 0: "prv (imp (all x (neg φ)) (imp φ fls))"
using prv_all_inst[OF x, of "neg φ" "Var x",simplified] assms by (auto simp: neg_def)
have 1: "prv (imp φ (imp (all x (neg φ)) fls))"
using 0 by (simp add: assms  prv_imp_com)
have 2: "prv (imp (exi x φ) (imp (all x (neg φ)) fls))"
using 1 assms by (intro prv_exi_imp_gen) auto
thus ?thesis by (simp add: assms  neg_def prv_imp_com)
qed

lemma prv_neg_exi_imp_all_neg:
assumes x: "x ∈ var" and φ: "φ ∈ fmla"
shows "prv (imp (neg (exi x φ)) (all x (neg φ)))"
using assms
by (intro prv_all_imp_gen[of x "neg (exi x φ)"])
(auto simp: prv_exi_inst_same prv_imp_neg_rev)

lemma prv_neg_exi_eqv_all_neg:
assumes x: "x ∈ var" and φ: "φ ∈ fmla"
shows "prv (eqv (neg (exi x φ)) (all x (neg φ)))"
by (simp add: φ prv_all_neg_imp_neg_exi prv_eqvI prv_neg_exi_imp_all_neg x)

lemma prv_neg_exi_implies_all_neg:
assumes x: "x ∈ var" and φ: "φ ∈ fmla" and "prv (neg (exi x φ))"
shows "prv (all x (neg φ))"
by (meson φ all assms(3) exi neg prv_imp_mp prv_neg_exi_imp_all_neg x)

lemma prv_neg_neg_exi:
assumes "x ∈ var" "φ ∈ fmla"
and "prv (neg φ)"
shows "prv (neg (exi x φ))"
using assms neg_def prv_exi_imp_gen by auto

lemma prv_exi_imp_exiI:
assumes [simp]: "x ∈ var" "y ∈ var" "φ ∈ fmla" and yx: "y = x ∨ y ∉ Fvars φ"
shows "prv (imp (exi x φ) (exi y (subst φ (Var y) x)))"
proof(cases "y = x")
case [simp]: False hence [simp]: "x ≠ y" by blast
show ?thesis apply(rule prv_exi_imp_gen)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
using yx
by (auto intro!: prv_imp_exi prv_exiI[of _ _ "Var x"]
simp: prv_imp_refl2)

lemma prv_imp_neg_allI:
assumes "φ ∈ fmla" "χ ∈ fmla" "t ∈ trm" "x ∈ var"
and "prv (imp φ (neg (subst χ t x)))"
shows "prv (imp φ (neg (all x χ)))"
by (meson all assms subst neg prv_all_inst prv_imp_neg_rev prv_prv_imp_trans)

lemma prv_imp_neg_allWI:
assumes "χ ∈ fmla" "t ∈ trm" "x ∈ var"
and "prv (neg (subst χ t x))"
shows "prv (neg (all x χ))"
by (metis all assms fls subst neg_def prv_all_inst prv_prv_imp_trans)

subsection ‹Properties involving True (tru)›

lemma prv_imp_tru: "φ ∈ fmla ⟹ prv (imp φ tru)"
by (simp add: neg_def prv_imp_triv tru_def)

lemma prv_tru_imp: "φ ∈ fmla ⟹ prv (eqv (imp tru φ) φ)"
by (metis imp neg_def prv_eqvI prv_fls prv_imp_com prv_imp_imp_triv prv_imp_mp prv_imp_refl tru tru_def)

lemma prv_fls_neg_tru: "φ ∈ fmla ⟹ prv (eqv fls (neg tru))"
using neg_def prv_eqvI prv_neg_neg tru_def by auto

lemma prv_tru_neg_fls: "φ ∈ fmla ⟹ prv (eqv tru (neg fls))"

lemma prv_cnjR_tru: "φ ∈ fmla ⟹ prv (eqv (cnj tru φ) φ)"
by (simp add: prv_eqvI prv_imp_cnj prv_imp_cnjR prv_imp_refl prv_imp_tru)

lemma prv_cnjL_tru: "φ ∈ fmla ⟹ prv (eqv (cnj φ tru) φ)"
by (simp add: prv_eqvI prv_imp_cnj prv_imp_cnjL prv_imp_refl prv_imp_tru)

subsection ‹Property of set-based conjunctions›

text ‹These are based on properties of the auxiliary list conjunctions.›

lemma prv_lcnj_imp_in:
assumes "set φs ⊆ fmla"
and "φ ∈ set φs"
shows "prv (imp (lcnj φs) φ)"
proof-
have "φ ∈ fmla" using assms by auto
thus ?thesis using assms
by (induct φs arbitrary: φ)
(auto simp : prv_imp_cnjL prv_cnj_imp_monoR2 prv_imp_triv)
qed

lemma prv_lcnj_imp:
assumes "χ ∈ fmla" and "set φs ⊆ fmla"
and "φ ∈ set φs" and "prv (imp φ χ)"
shows "prv (imp (lcnj φs) χ)"
using assms lcnj prv_lcnj_imp_in prv_prv_imp_trans by blast

lemma prv_imp_lcnj:
assumes "χ ∈ fmla" and "set φs ⊆ fmla"
and "⋀φ. φ ∈ set φs ⟹ prv (imp χ φ)"
shows "prv (imp χ (lcnj φs))"
using assms
by (induct φs arbitrary: χ) (auto simp: prv_imp_tru prv_imp_com prv_imp_cnj)

lemma prv_lcnj_imp_inner:
assumes "φ ∈ fmla" "set φ1s ⊆ fmla" "set φ2s ⊆ fmla"
shows "prv (imp (cnj φ (lcnj (φ1s @ φ2s))) (lcnj (φ1s @ φ # φ2s)))"
using assms proof(induction φ1s)
case (Cons φ1 φ1s)
have [intro!]: "set (φ1s @ φ2s) ⊆ fmla" "set (φ1s @ φ # φ2s) ⊆ fmla"  using Cons by auto
have 0: "prv (imp (cnj φ (cnj φ1 (lcnj (φ1s @ φ2s))))
(cnj φ1 (cnj φ (lcnj (φ1s @ φ2s)))))"
using Cons by (intro prv_cnj_com_imp3) fastforce+
have 1: "prv (imp (cnj φ1 (cnj φ (lcnj (φ1s @ φ2s))))
(cnj φ1 (lcnj (φ1s @ φ # φ2s))))"
using Cons by (intro prv_cnj_mono) (auto simp add: prv_imp_refl)
show ?case using prv_prv_imp_trans[OF _ _ _ 0 1] Cons by auto

lemma prv_lcnj_imp_remdups:
assumes "set φs ⊆ fmla"
shows "prv (imp (lcnj (remdups φs)) (lcnj φs))"
using assms apply(induct φs)
by (auto simp: prv_imp_cnj prv_lcnj_imp_in prv_cnj_mono prv_imp_refl)

lemma prv_lcnj_mono:
assumes φ1s: "set φ1s ⊆ fmla" and "set φ2s ⊆ set φ1s"
shows "prv (imp (lcnj φ1s) (lcnj φ2s))"
proof-
define φ2s' where φ2s': "φ2s' = remdups φ2s"
have A: "set φ2s' ⊆ set φ1s" "distinct φ2s'" unfolding  φ2s' using assms by auto
have B: "prv (imp (lcnj φ1s) (lcnj φ2s'))"
using φ1s A proof(induction φ1s arbitrary: φ2s')
case (Cons φ1 φ1s φ2ss)
show ?case proof(cases "φ1 ∈ set φ2ss")
case True
then obtain φ2ss1 φ2ss2 where φ2ss: "φ2ss = φ2ss1 @ φ1 # φ2ss2"
by (meson split_list)
define φ2s where φ2s: "φ2s ≡ φ2ss1 @ φ2ss2"
have nin: "φ1 ∉ set φ2s" using φ2ss ‹distinct φ2ss› unfolding φ2s by auto
have [intro!]: "set φ2s ⊆ fmla" unfolding φ2s using φ2ss Cons by auto
have 0: "prv (imp (cnj φ1 (lcnj φ2s)) (lcnj φ2ss))"
unfolding φ2s φ2ss using Cons φ2ss
by (intro prv_lcnj_imp_inner) auto
have 1: "prv (imp (lcnj φ1s) (lcnj φ2s))"
using nin Cons.prems True φ2s φ2ss by (intro Cons.IH) auto
have 2: "prv (imp (cnj φ1 (lcnj φ1s)) (cnj φ1 (lcnj φ2s)))"
using Cons φ2ss φ2s 1 by (intro prv_cnj_mono) (fastforce simp add: prv_imp_refl)+
show ?thesis
using Cons by (auto intro!: prv_prv_imp_trans[OF _ _ _ 2 0])
next
case False
then show ?thesis
by (meson Cons lcnj prv_imp_lcnj prv_lcnj_imp_in subset_iff)
qed
have C: "prv (imp (lcnj φ2s') (lcnj φ2s))"
unfolding φ2s' using assms by (intro prv_lcnj_imp_remdups) auto
show ?thesis using A assms by (intro prv_prv_imp_trans[OF _ _ _ B C]) auto
qed

lemma prv_lcnj_eqv:
assumes "set φ1s ⊆ fmla" and "set φ2s = set φ1s"
shows "prv (eqv (lcnj φ1s) (lcnj φ2s))"
using assms prv_lcnj_mono  by (intro prv_eqvI) auto

lemma prv_lcnj_mono_imp:
assumes "set φ1s ⊆ fmla" "set φ2s ⊆ fmla" and "∀ φ2 ∈ set φ2s. ∃ φ1 ∈ set φ1s. prv (imp φ1 φ2)"
shows "prv (imp (lcnj φ1s) (lcnj φ2s))"
using assms apply(intro prv_imp_lcnj)
subgoal by auto
subgoal by auto
subgoal using prv_lcnj_imp by blast .

text ‹Set-based conjunction commutes with substitution only up to provably equivalence:›
lemma prv_subst_scnj:
assumes "F ⊆ fmla" "finite F" "t ∈ trm" "x ∈ var"
shows "prv (eqv (subst (scnj F) t x) (scnj ((λφ. subst φ t x)  F)))"
using assms unfolding scnj_def by (fastforce intro!: prv_lcnj_eqv)

lemma prv_imp_subst_scnj:
assumes "F ⊆ fmla" "finite F" "t ∈ trm" "x ∈ var"
shows "prv (imp (subst (scnj F) t x) (scnj ((λφ. subst φ t x)  F)))"
using prv_subst_scnj[OF assms] assms by (intro prv_imp_eqvEL) auto

lemma prv_subst_scnj_imp:
assumes "F ⊆ fmla" "finite F" "t ∈ trm" "x ∈ var"
shows "prv (imp (scnj ((λφ. subst φ t x)  F)) (subst (scnj F) t x))"
using prv_subst_scnj[OF assms] assms by (intro prv_imp_eqvER) auto

lemma prv_scnj_imp_in:
assumes "F ⊆ fmla" "finite F"
and "φ ∈ F"
shows "prv (imp (scnj F) φ)"
unfolding scnj_def using assms by (intro prv_lcnj_imp_in) auto

lemma prv_scnj_imp:
assumes "χ ∈ fmla" and "F ⊆ fmla" "finite F"
and "φ ∈ F" and "prv (imp φ χ)"
shows "prv (imp (scnj F) χ)"
unfolding scnj_def using assms by (intro prv_lcnj_imp) auto

lemma prv_imp_scnj:
assumes "χ ∈ fmla" and "F ⊆ fmla" "finite F"
and "⋀φ. φ ∈ F ⟹ prv (imp χ φ)"
shows "prv (imp χ (scnj F))"
unfolding scnj_def using assms by (intro prv_imp_lcnj) auto

lemma prv_scnj_mono:
assumes "F1 ⊆ fmla" and "F2 ⊆ F1" and "finite F1"
shows "prv (imp (scnj F1) (scnj F2))"
unfolding scnj_def using assms apply (intro prv_lcnj_mono)
subgoal by auto
subgoal by (metis asList infinite_super) .

lemma prv_scnj_mono_imp:
assumes "F1 ⊆ fmla" "F2 ⊆ fmla" "finite F1" "finite F2"
and "∀ φ2 ∈ F2. ∃ φ1 ∈ F1. prv (imp φ1 φ2)"
shows "prv (imp (scnj F1) (scnj F2))"
unfolding scnj_def using assms by (intro prv_lcnj_mono_imp) auto

text ‹Commutation with parallel substitution:›

lemma prv_imp_scnj_insert:
assumes "F ⊆ fmla" and "finite F" and "φ ∈ fmla"
shows "prv (imp (scnj (insert φ F)) (cnj φ (scnj F)))"
using assms apply (intro prv_imp_cnj)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto intro: prv_imp_refl prv_scnj_imp)
subgoal by (auto intro: prv_scnj_mono) .

lemma prv_implies_scnj_insert:
assumes "F ⊆ fmla" and "finite F" and "φ ∈ fmla"
and "prv (scnj (insert φ F))"
shows "prv (cnj φ (scnj F))"
by (meson assms  cnj finite.insertI insert_subset prv_imp_mp prv_imp_scnj_insert scnj)

lemma prv_imp_cnj_scnj:
assumes "F ⊆ fmla" and "finite F" and "φ ∈ fmla"
shows "prv (imp (cnj φ (scnj F)) (scnj (insert φ F)))"
using assms
by (auto intro!: prv_imp_scnj prv_imp_cnjL
simp: prv_cnj_imp_monoR2 prv_imp_triv prv_scnj_imp_in subset_iff)

lemma prv_implies_cnj_scnj:
assumes "F ⊆ fmla" and "finite F" and "φ ∈ fmla"
and "prv (cnj φ (scnj F))"
shows "prv (scnj (insert φ F))"
by (meson assms  cnj finite.insertI insert_subset prv_imp_cnj_scnj prv_imp_mp scnj)

lemma prv_eqv_scnj_insert:
assumes "F ⊆ fmla" and "finite F" and "φ ∈ fmla"
shows "prv (eqv (scnj (insert φ F)) (cnj φ (scnj F)))"
by (simp add: assms prv_eqvI prv_imp_cnj_scnj prv_imp_scnj_insert)

lemma prv_scnj1_imp:
"φ ∈ fmla ⟹ prv (imp (scnj {φ}) φ)"
using prv_scnj_imp_in by auto

lemma prv_imp_scnj1:
"φ ∈ fmla ⟹ prv (imp φ (scnj {φ}))"
using prv_imp_refl prv_imp_scnj by fastforce

lemma prv_scnj2_imp_cnj:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ prv (imp (scnj {φ,ψ}) (cnj φ ψ))"
using prv_imp_cnj prv_scnj_imp_in by auto

lemma prv_cnj_imp_scnj2:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ prv (imp (cnj φ ψ) (scnj {φ,ψ}))"
using prv_imp_cnjL prv_imp_cnjR prv_imp_scnj by fastforce

lemma prv_imp_imp_scnj2:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ prv (imp φ (imp ψ (scnj {φ,ψ})))"
using prv_cnj_imp_scnj2 prv_cnj_imp by auto

(* *)

lemma prv_rawpsubst_scnj:
assumes "F ⊆ fmla" "finite F"
and "snd  (set txs) ⊆ var" "fst  (set txs) ⊆ trm"
shows "prv (eqv (rawpsubst (scnj F) txs) (scnj ((λφ. rawpsubst φ txs)  F)))"
using assms proof(induction txs arbitrary: F)
case (Cons tx txs)
then obtain t x where tx[simp]: "tx = (t,x)" by (cases tx) auto
hence [simp]: "t ∈ trm" "x ∈ var" using Cons.prems by auto
have 0: "(λφ. rawpsubst (subst φ t x) txs)  F =
(λφ. rawpsubst φ txs)  ((λφ. subst φ t x)  F)"
using Cons.prems by auto
have "prv (eqv (subst (scnj F) t x)
(scnj ((λφ. subst φ t x)  F)))"
using Cons.prems by (intro prv_subst_scnj) auto
hence "prv (eqv (rawpsubst (subst (scnj F) t x) txs)
(rawpsubst (scnj ((λφ. subst φ t x)  F)) txs))"
using Cons.prems by (intro prv_eqv_rawpsubst) auto
moreover
have "prv (eqv (rawpsubst (scnj ((λφ. subst φ t x)  F)) txs)
(scnj ((λφ. rawpsubst (subst φ t x) txs)  F)))"
unfolding 0 using Cons.prems by (intro Cons.IH) auto
ultimately show ?case
using Cons.prems apply - by (rule prv_eqv_trans) (auto intro!: rawpsubst)
qed(auto simp: image_def prv_eqv_refl)[]

lemma prv_psubst_scnj:
assumes "F ⊆ fmla" "finite F"
and "snd  (set txs) ⊆ var" "fst  (set txs) ⊆ trm"
and "distinct (map snd txs)"
shows "prv (eqv (psubst (scnj F) txs) (scnj ((λφ. psubst φ txs)  F)))"
proof-
define us where us: "us ≡ getFrN (map snd txs) (map fst txs) [scnj F] (length txs)"
have us_facts: "set us ⊆ var"
"set us ∩ ⋃ (Fvars  F) = {}"
"set us ∩ ⋃ (FvarsT  (fst  (set txs))) = {}"
"set us ∩ snd  (set txs) = {}"
"length us = length txs"
"distinct us"
using assms unfolding us
using getFrN_Fvars[of "map snd txs" "map fst txs" "[scnj F]" _ "length txs"]
getFrN_FvarsT[of "map snd txs" "map fst txs" "[scnj F]" _ "length txs"]
getFrN_var[of "map snd txs" "map fst txs" "[scnj F]" _ "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[scnj F]" "length txs"]
apply -
subgoal by auto
subgoal by fastforce
subgoal by (fastforce simp: image_iff)
subgoal by (fastforce simp: image_iff)
subgoal by (fastforce simp: image_iff)
by auto

define vs where vs: "vs ≡ λ φ. getFrN (map snd txs) (map fst txs) [φ] (length txs)"
hence vss: "⋀φ. vs φ = getFrN (map snd txs) (map fst txs) [φ] (length txs)" by auto
{fix φ assume "φ ∈ F" hence "φ ∈ fmla" using assms by auto
hence "set (vs φ)  ⊆ var ∧
set (vs φ) ∩ Fvars φ = {} ∧
set (vs φ) ∩ ⋃ (FvarsT  (fst  (set txs))) = {} ∧
set (vs φ) ∩ snd  (set txs) = {} ∧
length (vs φ) = length txs ∧
distinct (vs φ)"
using assms unfolding vs
using getFrN_Fvars[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_FvarsT[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_var[of "map snd txs" "map fst txs" "[φ]" _ "length txs"]
getFrN_length[of "map snd txs" "map fst txs" "[φ]" "length txs"]
apply (intro conjI)
subgoal by auto
subgoal by auto
subgoal by fastforce
subgoal by (fastforce simp: image_iff)
by auto
} note vs_facts = this

have [simp]: "⋀ x f. f ∈ F ⟹ x ∈ set (vs f) ⟹ x ∈ var"
using vs_facts
by (meson subsetD)

let ?tus = "zip (map fst txs) us"
let ?uxs = "zip (map Var us) (map snd txs)"
let ?tvs = "λ φ. zip (map fst txs) (vs φ)"
let ?vxs = "λ φ. zip (map Var (vs φ)) (map snd txs)"

let ?c = "rawpsubst (scnj F) ?uxs"
have c: "prv (eqv ?c
(scnj ((λφ. rawpsubst φ ?uxs)  F)))"
using assms us_facts by (intro prv_rawpsubst_scnj) (auto intro!: rawpsubstT dest!: set_zip_D)
hence "prv (eqv (rawpsubst ?c ?tus)
(rawpsubst (scnj ((λφ. rawpsubst φ ?uxs)  F)) ?tus))"
using assms us_facts
by (intro prv_eqv_rawpsubst) (auto intro!: rawpsubst dest!: set_zip_D)
moreover
have "prv (eqv (rawpsubst (scnj ((λφ. rawpsubst φ ?uxs)  F)) ?tus)
(scnj ((λφ. rawpsubst φ ?tus)  ((λφ. rawpsubst φ ?uxs)  F))))"
using assms us_facts
by (intro prv_rawpsubst_scnj) (auto intro!: rawpsubst dest!: set_zip_D)
ultimately
have 0: "prv (eqv (rawpsubst ?c ?tus)
(scnj ((λφ. rawpsubst φ ?tus)  ((λφ. rawpsubst φ ?uxs)  F))))"
using assms us_facts apply - by (rule prv_eqv_trans) (auto intro!: rawpsubst dest!: set_zip_D)
moreover
have "prv (eqv (scnj ((λφ. rawpsubst φ ?tus)  ((λφ. rawpsubst φ ?uxs)  F)))
(scnj ((λφ. rawpsubst (rawpsubst φ (?vxs φ)) (?tvs φ))  F)))"
using assms us_facts vs_facts apply(intro prv_eqvI)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal apply(rule prv_scnj_mono_imp)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by auto
subgoal by auto
subgoal apply clarsimp
subgoal for φ apply(rule bexI[of _ φ]) apply(rule prv_imp_refl2)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (rule rawpsubst_compose_freshVar2)
(auto intro!: rawpsubst dest!: set_zip_D)  . . .
subgoal apply(rule prv_scnj_mono_imp)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal by (auto intro!: rawpsubst dest!: set_zip_D)
subgoal apply clarsimp
subgoal for φ apply(rule bexI[of _ φ]) apply(rule prv_imp_refl2)
apply (auto intro!: rawpsubst dest!: set_zip_D)
apply(rule rawpsubst_compose_freshVar2)
apply (auto intro!: rawpsubst dest!: set_zip_D) . . . .
ultimately
have "prv (eqv (rawpsubst (rawpsubst (scnj F) ?uxs) ?tus)
(scnj ((λφ. rawpsubst (rawpsubst φ (?vxs φ)) (?tvs φ))  F)))"
using assms us_facts
apply - by (rule prv_eqv_trans) (auto intro!: rawpsubst dest!: set_zip_D)
thus ?thesis unfolding psubst_def by (simp add: Let_def us[symmetric] vss)
qed

lemma prv_imp_psubst_scnj:
assumes "F ⊆ fmla" "finite F" "snd  set txs ⊆ var" "fst  set txs ⊆ trm"
and "distinct (map snd txs)"
shows "prv (imp (psubst (scnj F) txs) (scnj ((λφ. psubst φ txs)  F)))"
using prv_psubst_scnj[OF assms] assms apply(intro prv_imp_eqvEL) by auto

lemma prv_psubst_scnj_imp:
assumes "F ⊆ fmla" "finite F" "snd  set txs ⊆ var" "fst  set txs ⊆ trm"
and "distinct (map snd txs)"
shows "prv (imp (scnj ((λφ. psubst φ txs)  F)) (psubst (scnj F) txs))"
using prv_psubst_scnj[OF assms] assms apply(intro prv_imp_eqvER) by auto

subsection ‹Consistency and $\omega$-consistency›

definition consistent :: bool where
"consistent ≡ ¬ prv fls"

lemma consistent_def2: "consistent ⟷ (∃φ ∈ fmla. ¬ prv φ)"
unfolding consistent_def using prv_expl by blast

lemma consistent_def3: "consistent ⟷ (∀φ ∈ fmla. ¬ (prv φ ∧ prv (neg φ)))"
unfolding consistent_def using prv_neg_fls neg_def by auto

(* Omega-consistency: *)
definition ωconsistent :: bool where
"ωconsistent ≡
∀ φ ∈ fmla. ∀ x ∈ var. Fvars φ = {x} ⟶
(∀ n ∈ num. prv (neg (subst φ n x)))
⟶
¬ prv (neg (neg (exi x φ)))"

text ‹The above particularly strong version of @{term ωconsistent} is used for the sake of working without
assuming classical logic. It of course implies the more standard formulations for classical logic:›

definition ωconsistentStd1 :: bool where
"ωconsistentStd1 ≡
∀ φ ∈ fmla. ∀ x ∈ var. Fvars φ = {x} ⟶
(∀ n ∈ num. prv (neg (subst φ n x))) ⟶ ¬ prv (exi x φ)"

definition ωconsistentStd2 :: bool where
"ωconsistentStd2 ≡
∀ φ ∈ fmla. ∀ x ∈ var. Fvars φ = {x} ⟶
(∀ n ∈ num. prv (subst φ n x)) ⟶ ¬ prv (exi x (neg φ))"

lemma ωconsistent_impliesStd1:
"ωconsistent ⟹
ωconsistentStd1"
unfolding ωconsistent_def ωconsistentStd1_def using prv_neg_neg by blast

lemma ωconsistent_impliesStd2:
"ωconsistent ⟹
ωconsistentStd2"
by (auto dest!: ωconsistent_impliesStd1 bspec[of _ _ "neg _"]
simp: ωconsistentStd1_def ωconsistentStd2_def prv_neg_neg)

text ‹In the presence of classical logic deduction, the stronger condition is
equivalent to the standard ones:›

lemma ωconsistent_iffStd1:
assumes "⋀ φ. φ ∈ fmla ⟹ prv (imp (neg (neg φ)) φ)"
shows "ωconsistent ⟷ ωconsistentStd1"
apply standard
subgoal using ωconsistent_impliesStd1 by auto
subgoal unfolding ωconsistentStd1_def ωconsistent_def
by (meson assms exi neg prv_imp_mp) .

lemma ωconsistent_iffStd2:
assumes "⋀ φ. φ ∈ fmla ⟹ prv (imp (neg (neg φ)) φ)"
shows "ωconsistent ⟷ ωconsistentStd2"
unfolding ωconsistent_iffStd1[OF assms, simplified]
ωconsistentStd1_def ωconsistentStd2_def apply safe
subgoal for φ x
by (auto simp: prv_neg_neg dest: bspec[of _ _ "neg _"])
subgoal for φ x
using  prv_exi_congW prv_imp_neg_fls
by (auto simp: neg_def prv_neg_neg dest!: bspec[of _ _ "neg _"]) .

text ‹$\omega$-consistency implies consistency:›

lemma ωconsistentStd1_implies_consistent:
assumes "ωconsistentStd1"
shows "consistent"
unfolding consistent_def
proof safe
assume pf: "prv fls"
then obtain x where x: "x ∈ var" "x ∉ Fvars fls"
using finite_Fvars getFresh by auto
let ?fls = "cnj (fls) (eql (Var x) (Var x))"
have 0: "∀ n ∈ num. prv (neg (subst ?fls n x))" and 1: "prv (exi x fls)"
using x fls by (auto simp: pf prv_expl)
have 2: "¬ prv (exi x ?fls)" using 0 fls x assms
unfolding ωconsistentStd1_def by simp
show False using 1 2 consistent_def consistent_def2 pf x(1) by blast
qed

lemma ωconsistentStd2_implies_consistent:
assumes "ωconsistentStd2"
shows "consistent"
unfolding consistent_def
proof safe
assume pf: "prv fls"
then obtain x where x: "x ∈ var" "x ∉ Fvars fls"
using finite_Fvars getFresh by auto
let ?fls = "cnj (fls) (eql (Var x) (Var x))"
have 0: "∀ n ∈ num. prv (subst ?fls n x)" and 1: "prv (exi x (neg ?fls))"
using x fls  by (auto simp: pf prv_expl)
have 2: "¬ prv (exi x (neg ?fls))" using 0 fls x assms
unfolding ωconsistentStd2_def by auto
show False using 1 2 by simp
qed

corollary ωconsistent_implies_consistent:
assumes "ωconsistent"
shows "consistent"
by (simp add: ωconsistentStd2_implies_consistent ωconsistent_impliesStd2 assms)

end ― ‹context @{locale Deduct_with_False}›

section ‹Deduction Considering False and Disjunction›

locale Deduct_with_False_Disj =
Syntax_with_Connectives_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
+
Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv
+
assumes
prv_dsj_impL:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp φ (dsj φ χ))"
and
prv_dsj_impR:
"⋀ φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹
prv (imp χ (dsj φ χ))"
and
prv_imp_dsjE:
"⋀ φ χ ψ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ ψ ∈ fmla ⟹
prv (imp (imp φ ψ) <`