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 χ ψ)) ψ))"
    by (simp add: assms prv_cnj_imp_monoR2)
  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
    by (simp add: assms prv_cnj_imp)
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))))"
    by(simp add: assms prv_cnj_imp_monoR2)
  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))))"
    by(simp add: assms prv_cnj_imp_monoR2)
  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 χ φ))"
  by (simp add: prv_cnj_com_imp prv_eqvI)

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))"
  by (simp add: prv_allE prv_all_gen)

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)"
  by (simp add: prv_eqvI prv_imp_cnjL)

lemma prv_cnjL_fls: "φ ∈ fmla ⟹ prv (eqv (cnj φ fls) fls)"
  by (simp add: prv_eqvI prv_imp_cnjR)


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"
  by (simp add: prv_eqv_eqv_neg_prv_fls prv_eqv_sym)

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)
qed(simp add: yx prv_imp_refl)

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))"
  by (simp add: prv_eqv_refl tru_def)

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
qed(simp add: prv_imp_refl)

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
  qed(simp add: prv_imp_refl)
  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 φ ψ) (imp (imp χ ψ) (imp (dsj φ χ) ψ)))"
begin

lemma prv_imp_dsjEE:
  assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
  assumes " prv (imp φ ψ)" and "prv (imp χ ψ)"
  shows "prv (imp (dsj φ χ) ψ)"
  by (metis assms dsj imp prv_imp_dsjE prv_imp_mp)

lemma prv_dsj_cases:
  assumes "φ1 ∈ fmla" "φ2 ∈ fmla" "χ ∈ fmla"
    and "prv (dsj φ1 φ2)" and "prv (imp φ1 χ)" and "prv (imp φ2 χ)"
  shows "prv χ"
  by (meson assms  dsj prv_imp_dsjEE prv_imp_mp)


subsection ‹Disjunction vs. disjunction›

lemma prv_dsj_com_imp:
  assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
  shows "prv (imp (dsj φ χ) (dsj χ φ))"
  by (metis χ φ dsj imp prv_dsj_impL prv_dsj_impR prv_imp_dsjE prv_imp_mp)

lemma prv_dsj_com:
  assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla"
  shows "prv (eqv (dsj φ χ) (dsj χ φ))"
  by (simp add: prv_dsj_com_imp prv_eqvI)

lemma prv_dsj_assoc_imp1:
  assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
  shows "prv (imp (dsj φ (dsj χ ψ)) (dsj (dsj φ χ) ψ))"
proof -
  have f1: "⋀f fa fb. f ∉ fmla ∨ ¬ prv (imp fa fb) ∨ fb ∉ fmla ∨ fa ∉ fmla ∨ prv (imp fa (dsj fb f))"
    by (meson dsj prv_dsj_impL prv_prv_imp_trans)
  have "prv (imp φ (dsj φ χ))"
    by (simp add: prv_dsj_impL)
  then show ?thesis
    using f1 χ φ ψ dsj prv_dsj_impR prv_imp_dsjEE by presburger
qed

lemma prv_dsj_assoc_imp2:
 assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
 shows "prv (imp (dsj (dsj φ χ) ψ) (dsj φ (dsj χ ψ)))"
proof -
  have f1: "∀f fa fb. (((prv (imp f (dsj fa fb)) ∨ ¬ prv (imp f (dsj fb fa))) ∨ f ∉ fmla) ∨ fa ∉ fmla) ∨ fb ∉ fmla"
    by (meson dsj prv_dsj_com_imp prv_prv_imp_trans)
  have "∀f fa fb. (((prv (imp f (dsj fa fb)) ∨ ¬ prv (imp f fa)) ∨ fa ∉ fmla) ∨ f ∉ fmla) ∨ fb ∉ fmla"
    by (meson dsj prv_dsj_impL prv_prv_imp_trans)
  then show ?thesis
    using f1 by (metis χ φ ψ dsj prv_dsj_impR prv_imp_dsjEE)
qed

lemma prv_dsj_assoc:
 assumes φ[simp]: "φ ∈ fmla" and χ[simp]: "χ ∈ fmla" and ψ[simp]: "ψ ∈ fmla"
 shows "prv (eqv (dsj φ (dsj χ ψ)) (dsj (dsj φ χ) ψ))"
  by (simp add: prv_dsj_assoc_imp1 prv_dsj_assoc_imp2 prv_eqvI)

lemma prv_dsj_com_imp3:
assumes "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla"
shows "prv (imp (dsj φ1 (dsj φ2 φ3))
                (dsj φ2 (dsj φ1 φ3)))"
proof -
  have "∀f fa fb. (((prv (imp f (dsj fb fa)) ∨ ¬ prv (imp f fa)) ∨ fa ∉ fmla) ∨ f ∉ fmla) ∨ fb ∉ fmla"
    by (meson dsj prv_dsj_impR prv_prv_imp_trans)
  then show ?thesis
    by (meson assms(1) assms(2) assms(3) dsj prv_dsj_impL prv_dsj_impR prv_imp_dsjEE)
qed

lemma prv_dsj_mono:
"φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ χ1 ∈ fmla ⟹ χ2 ∈ fmla ⟹
prv (imp φ1 χ1) ⟹ prv (imp φ2 χ2) ⟹ prv (imp (dsj φ1 φ2) (dsj χ1 χ2))"
  by (meson dsj prv_dsj_impL prv_dsj_impR prv_imp_dsjEE prv_prv_imp_trans)


subsection ‹Disjunction vs. conjunction›

lemma prv_cnj_dsj_distrib1:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (imp (cnj φ (dsj χ1 χ2)) (dsj (cnj φ χ1) (cnj φ χ2)))"
  by (simp add: prv_cnj_imp prv_cnj_imp_monoR2 prv_dsj_impL prv_dsj_impR prv_imp_com prv_imp_dsjEE)

lemma prv_cnj_dsj_distrib2:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (imp (dsj (cnj φ χ1) (cnj φ χ2)) (cnj φ (dsj χ1 χ2)))"
  by (simp add: prv_cnj_mono prv_dsj_impL prv_dsj_impR prv_imp_dsjEE prv_imp_refl)

lemma prv_cnj_dsj_distrib:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (eqv (cnj φ (dsj χ1 χ2)) (dsj (cnj φ χ1) (cnj φ χ2)))"
  by (simp add: prv_cnj_dsj_distrib1 prv_cnj_dsj_distrib2 prv_eqvI)

lemma prv_dsj_cnj_distrib1:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (imp (dsj φ (cnj χ1 χ2)) (cnj (dsj φ χ1) (dsj φ χ2)))"
  by (simp add: prv_cnj_mono prv_dsj_impL prv_dsj_impR prv_imp_cnj prv_imp_dsjEE)

lemma prv_dsj_cnj_distrib2:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (imp (cnj (dsj φ χ1) (dsj φ χ2)) (dsj φ (cnj χ1 χ2)))"
proof -
  have "∀f fa fb. (((prv (imp f (imp fb fa)) ∨ ¬ prv (imp f fa)) ∨ fa ∉ fmla) ∨ f ∉ fmla) ∨ fb ∉ fmla"
    by (meson imp prv_imp_imp_triv prv_prv_imp_trans)
  then show ?thesis
    by (metis χ1 χ2 φ cnj dsj imp prv_cnj_imp prv_cnj_imp_monoR2 prv_dsj_impL prv_dsj_impR
        prv_imp_com prv_imp_dsjEE)
qed

lemma prv_dsj_cnj_distrib:
 assumes φ[simp]: "φ ∈ fmla" and χ1[simp]: "χ1 ∈ fmla" and χ2[simp]: "χ2 ∈ fmla"
 shows "prv (eqv (dsj φ (cnj χ1 χ2)) (cnj (dsj φ χ1) (dsj φ χ2)))"
  by (simp add: prv_dsj_cnj_distrib1 prv_dsj_cnj_distrib2 prv_eqvI)


subsection ‹Disjunction vs. True and False›

lemma prv_dsjR_fls: "φ ∈ fmla ⟹ prv (eqv (dsj fls φ) φ)"
  by (simp add: prv_dsj_impR prv_eqvI prv_imp_dsjEE prv_imp_refl)

lemma prv_dsjL_fls: "φ ∈ fmla ⟹ prv (eqv (dsj φ fls) φ)"
  by (simp add: prv_dsj_impL prv_eqvI prv_imp_dsjEE prv_imp_refl)

lemma prv_dsjR_tru: "φ ∈ fmla ⟹ prv (eqv (dsj tru φ) tru)"
  by (simp add: prv_dsj_impL prv_eqvI prv_imp_tru)

lemma prv_dsjL_tru: "φ ∈ fmla ⟹ prv (eqv (dsj φ tru) tru)"
  by (simp add: prv_dsj_impR prv_eqvI prv_imp_tru)


subsection ‹Set-based disjunctions›

text ‹Just like for conjunctions, these are based on properties of the auxiliary
list disjunctions.›

lemma prv_imp_ldsj_in:
  assumes "set φs ⊆ fmla"
  and "φ ∈ set φs"
  shows "prv (imp φ (ldsj φs))"
proof-
  have "φ ∈ fmla" using assms by auto
  thus ?thesis
  using assms apply(induct φs arbitrary: φ)
  subgoal by auto
  subgoal by (simp add: prv_dsj_impL)
    (meson dsj ldsj prv_dsj_impL prv_dsj_impR prv_prv_imp_trans) .
qed

lemma prv_imp_ldsj:
assumes "χ ∈ fmla" and "set φs ⊆ fmla"
and "φ ∈ set φs" and "prv (imp χ φ)"
shows "prv (imp χ (ldsj φs))"
  using assms ldsj prv_imp_ldsj_in prv_prv_imp_trans by blast

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

lemma prv_ldsj_imp_inner:
assumes "φ ∈ fmla" "set φ1s ⊆ fmla" "set φ2s ⊆ fmla"
shows "prv (imp (ldsj (φ1s @ φ # φ2s)) (dsj φ (ldsj (φ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 (dsj φ1 (dsj φ (ldsj (φ1s @ φ2s))))
                 (dsj φ (dsj φ1 (ldsj (φ1s @ φ2s)))))"
    using Cons by (intro prv_dsj_com_imp3) fastforce+
  have 1: "prv (imp (dsj φ1 (ldsj (φ1s @ φ # φ2s)))
                (dsj φ1 (dsj φ (ldsj (φ1s @ φ2s)))))"
  using Cons by (intro prv_dsj_mono) (auto simp add: prv_imp_refl)
  show ?case using prv_prv_imp_trans[OF _ _ _ 1 0] Cons by auto
qed(simp add: prv_imp_refl)

lemma prv_ldsj_imp_remdups:
assumes "set φs ⊆ fmla"
shows "prv (imp  (ldsj φs) (ldsj (remdups φs)))"
  using assms apply(induct φs)
  subgoal by auto
  subgoal by (metis ldsj prv_imp_ldsj_in prv_ldsj_imp set_remdups) .

lemma prv_ldsj_mono:
assumes φ2s: "set φ2s ⊆ fmla" and "set φ1s ⊆ set φ2s"
shows "prv (imp (ldsj φ1s) (ldsj φ2s))"
proof-
  define φ1s' where φ1s': "φ1s' = remdups φ1s"
  have A: "set φ1s' ⊆ set φ2s" "distinct φ1s'" unfolding φ1s' using assms by auto
  have B: "prv (imp (ldsj φ1s') (ldsj φ2s))"
  using φ2s A proof(induction φ2s arbitrary: φ1s')
    case (Cons φ2 φ2s φ1ss)
    show ?case proof(cases "φ2 ∈ set φ1ss")
      case True
      then obtain φ1ss1 φ1ss2 where φ1ss: "φ1ss = φ1ss1 @ φ2 # φ1ss2"
      by (meson split_list)
      define φ1s where φ1s: "φ1s ≡ φ1ss1 @ φ1ss2"
      have nin: "φ2 ∉ set φ1s" using φ1ss ‹distinct φ1ss› unfolding φ1s by auto
      have [intro!,simp]: "set φ1s ⊆ fmla" unfolding φ1s using φ1ss Cons by auto
      have 0: "prv (imp (ldsj φ1ss) (dsj φ2 (ldsj φ1s)))"
        unfolding φ1s φ1ss
        apply(rule prv_ldsj_imp_inner) using Cons φ1ss by auto
      have 1: "prv (imp (ldsj φ1s) (ldsj φ2s))" apply(rule Cons.IH) using nin Cons.prems True
      using φ1s φ1ss by  auto
      have 2: "prv (imp (dsj φ2 (ldsj φ1s)) (dsj φ2 (ldsj φ2s)))"
      using Cons φ1ss φ1s 1  apply(intro prv_dsj_mono)
      using prv_imp_refl by auto blast+
      show ?thesis using Cons by (auto intro!: prv_prv_imp_trans[OF _ _ _ 0 2])
    next
      case False
      then show ?thesis using Cons
      by (meson ldsj order.trans prv_imp_ldsj_in prv_ldsj_imp subset_code(1))
    qed
  qed(simp add: prv_imp_refl)
  have C: "prv (imp (ldsj φ1s) (ldsj φ1s'))"
    unfolding φ1s' using assms by (intro prv_ldsj_imp_remdups) auto
  show ?thesis  using A assms by (intro prv_prv_imp_trans[OF _ _ _ C B]) auto
qed

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

lemma prv_ldsj_mono_imp:
  assumes "set φ1s ⊆ fmla" "set φ2s ⊆ fmla" and "∀ φ1 ∈ set φ1s. ∃ φ2 ∈ set φ2s. prv (imp φ1 φ2)"
  shows "prv (imp (ldsj φ1s) (ldsj φ2s))"
  using assms apply(intro prv_ldsj_imp)
  subgoal by auto
  subgoal by auto
  subgoal using prv_imp_ldsj by blast .

text ‹Just like set-based conjunction, set-based disjunction commutes with substitution
only up to provably equivalence:›

lemma prv_subst_sdsj:
"F ⊆ fmla ⟹ finite F ⟹ t ∈ trm ⟹ x ∈ var ⟹
 prv (eqv (subst (sdsj F) t x) (sdsj ((λφ. subst φ t x) ` F)))"
unfolding sdsj_def by (fastforce intro!: prv_ldsj_eqv)

lemma prv_imp_sdsj_in:
  assumes "φ ∈ fmla" and "F ⊆ fmla" "finite F"
  and "φ ∈ F"
  shows "prv (imp φ (sdsj F))"
  unfolding sdsj_def using assms by (intro prv_imp_ldsj_in) auto

lemma prv_imp_sdsj:
assumes "χ ∈ fmla" and "F ⊆ fmla" "finite F"
and "φ ∈ F" and "prv (imp χ φ)"
shows "prv (imp χ (sdsj F))"
  unfolding sdsj_def using assms by (intro prv_imp_ldsj) auto

lemma prv_sdsj_imp:
  assumes "χ ∈ fmla" and "F ⊆ fmla" "finite F"
  and "⋀φ. φ ∈ F ⟹ prv (imp φ χ)"
  shows "prv (imp (sdsj F) χ)"
  unfolding sdsj_def using assms by (intro prv_ldsj_imp) auto

lemma prv_sdsj_mono:
assumes "F2 ⊆ fmla" and "F1 ⊆ F2" and "finite F2"
shows "prv (imp (sdsj F1) (sdsj F2))"
  unfolding sdsj_def using assms apply(intro prv_ldsj_mono)
  subgoal by auto
  subgoal by (metis asList infinite_super) .

lemma prv_sdsj_mono_imp:
  assumes "F1 ⊆ fmla" "F2 ⊆ fmla" "finite F1" "finite F2"
  and "∀ φ1 ∈ F1. ∃ φ2 ∈ F2. prv (imp φ1 φ2)"
  shows "prv (imp (sdsj F1) (sdsj F2))"
  unfolding sdsj_def using assms by (intro prv_ldsj_mono_imp) auto

lemma prv_sdsj_cases:
assumes "F ⊆ fmla" "finite F" "ψ ∈ fmla"
and "prv (sdsj F)" and "⋀ φ. φ ∈ F ⟹ prv (imp φ ψ)"
shows "prv ψ"
  by (meson assms prv_imp_mp prv_sdsj_imp sdsj)

lemma prv_sdsj1_imp:
"φ ∈ fmla ⟹ prv (imp (sdsj {φ}) φ)"
  using prv_imp_refl prv_sdsj_imp by fastforce

lemma prv_imp_sdsj1:
"φ ∈ fmla ⟹ prv (imp φ (sdsj {φ}))"
using prv_imp_refl prv_imp_sdsj by fastforce

lemma prv_sdsj2_imp_dsj:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ prv (imp (sdsj {φ,ψ}) (dsj φ ψ))"
  using prv_dsj_impL prv_dsj_impR prv_sdsj_imp by fastforce

lemma prv_dsj_imp_sdsj2:
"φ ∈ fmla ⟹ ψ ∈ fmla ⟹ prv (imp (dsj φ ψ) (sdsj {φ,ψ}))"
  by (simp add: prv_imp_dsjEE prv_imp_sdsj_in)

text ‹Commutation with parallel substitution:›

lemma prv_rawpsubst_sdsj:
assumes "F ⊆ fmla" "finite F"
and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
shows "prv (eqv (rawpsubst (sdsj F) txs) (sdsj ((λφ. 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 (sdsj F) t x)
                 (sdsj ((λφ. subst φ t x) ` F)))"
  using Cons.prems by (intro prv_subst_sdsj) auto
  hence "prv (eqv (rawpsubst (subst (sdsj F) t x) txs)
                  (rawpsubst (sdsj ((λφ. subst φ t x) ` F)) txs))"
  using Cons.prems by (intro prv_eqv_rawpsubst) auto
  moreover
  have "prv (eqv (rawpsubst (sdsj ((λφ. subst φ t x) ` F)) txs)
                 (sdsj ((λφ. 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_sdsj:
assumes "F ⊆ fmla" "finite F"
and "snd ` (set txs) ⊆ var" "fst ` (set txs) ⊆ trm"
and "distinct (map snd txs)"
shows "prv (eqv (psubst (sdsj F) txs) (sdsj ((λφ. psubst φ txs) ` F)))"
proof-
  define us where us: "us ≡ getFrN (map snd txs) (map fst txs) [sdsj 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" "[sdsj F]" _ "length txs"]
        getFrN_FvarsT[of "map snd txs" "map fst txs" "[sdsj F]" _ "length txs"]
        getFrN_var[of "map snd txs" "map fst txs" "[sdsj F]" _ "length txs"]
        getFrN_length[of "map snd txs" "map fst txs" "[sdsj 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 fastforce
    subgoal by (fastforce simp: image_iff)
    subgoal by (fastforce simp: image_iff)
    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 (sdsj F) ?uxs"
  have c: "prv (eqv ?c
                   (sdsj ((λφ. rawpsubst φ ?uxs) ` F)))"
  using assms us_facts
  by (intro prv_rawpsubst_sdsj) (auto intro!: rawpsubstT dest!: set_zip_D)
  hence "prv (eqv (rawpsubst ?c ?tus)
                  (rawpsubst (sdsj ((λφ. 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 (sdsj ((λφ. rawpsubst φ ?uxs) ` F)) ?tus)
                 (sdsj ((λφ. rawpsubst φ ?tus) ` ((λφ. rawpsubst φ ?uxs) ` F))))"
  using assms us_facts by (intro prv_rawpsubst_sdsj) (auto intro!: rawpsubst dest!: set_zip_D)
  ultimately
  have 0: "prv (eqv (rawpsubst ?c ?tus)
                    (sdsj ((λφ. 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 (sdsj ((λφ. rawpsubst φ ?tus) ` ((λφ. rawpsubst φ ?uxs) ` F)))
                 (sdsj ((λφ. 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_sdsj_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_sdsj_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 (sdsj F) ?uxs) ?tus)
           (sdsj ((λφ. 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

end ― ‹context @{locale Deduct_with_False_Disj}›


section ‹Deduction with Quantified Variable Renaming Included›

locale Deduct_with_False_Disj_Rename =
Deduct_with_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
+
Syntax_with_Connectives_Rename
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
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


section ‹Deduction with PseudoOrder Axioms Included›

text ‹We assume a two-variable formula Lq that satisfies two axioms
resembling the properties of the strict or nonstrict ordering on naturals.
The choice of these axioms is motivated by an abstract account of Rosser's trick
to improve on Gödel's First Incompleteness Theorem, reported in our
CADE 2019 paper~\<^cite>‹"DBLP:conf/cade/0001T19"›.›

locale Deduct_with_PseudoOrder =
Deduct_with_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
+
Syntax_PseudoOrder
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  Lq
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
and Lq
+
assumes
Lq_num:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
 ∀ φ ∈ fmla. ∀ q ∈ num. Fvars φ = {zz} ∧ (∀ p ∈ num. prv (subst φ p zz))
    ⟶ prv (all zz (imp (LLq (Var zz) q) φ))"
and
Lq_num2:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
 ∀ p ∈ num. ∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
begin

lemma LLq_num:
assumes "φ ∈ fmla" "q ∈ num" "Fvars φ = {zz}" "∀ p ∈ num. prv (subst φ p zz)"
shows "prv (all zz (imp (LLq (Var zz) q) φ))"
using assms Lq_num unfolding LLq_def by auto

lemma LLq_num2:
assumes "p ∈ num"
shows "∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
using assms Lq_num2 unfolding LLq_def by auto

end ― ‹context @{locale Deduct_with_PseudoOrder}›



(*<*)
end
(*>*)