# Theory Natural_Deduction

```chapter ‹Natural Deduction›

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

text ‹We develop a natural deduction system based on the Hilbert system.›

context Deduct_with_False_Disj
begin

section ‹Natural Deduction from the Hilbert System›

definition nprv :: "'fmla set ⇒ 'fmla ⇒ bool" where
"nprv F φ ≡ prv (imp (scnj F) φ)"

lemma nprv_hyp[simp,intro]:
"φ ∈ F ⟹ F ⊆ fmla ⟹ finite F ⟹ nprv F φ"
unfolding nprv_def

section ‹Structural Rules for the Natural Deduction Relation›

lemma prv_nprv0I: "prv φ ⟹ φ ∈ fmla ⟹ nprv {} φ"
unfolding nprv_def by (simp add: prv_imp_triv)

lemma prv_nprv_emp: "φ ∈ fmla ⟹ prv φ ⟷ nprv {} φ"
using prv_nprv0I unfolding nprv_def
by (metis asList eqv finite.simps insert_not_empty lcnj.simps(1) ldsj.cases
list.simps(15) prv_eqvI prv_imp_mp prv_imp_tru scnj_def tru)

lemma nprv_mono:
assumes "nprv G φ"
and "F ⊆ fmla" "finite F" "G ⊆ F" "φ ∈ fmla"
shows "nprv F φ"
using assms unfolding nprv_def
by (meson order_trans prv_prv_imp_trans prv_scnj_mono rev_finite_subset scnj)

lemma nprv_cut:
assumes "nprv F φ" and "nprv (insert φ F) ψ"
and "F ⊆ fmla" "finite F"  "φ ∈ fmla"  "ψ ∈ fmla"
shows "nprv F ψ"
using assms unfolding nprv_def
by (metis (full_types) cnj finite.insertI
insert_subset prv_imp_cnj prv_imp_cnj_scnj prv_imp_refl prv_prv_imp_trans scnj)

lemma nprv_strong_cut2:
"nprv F φ1 ⟹ nprv (insert φ1 F) φ2 ⟹ nprv (insert φ2 (insert φ1 F)) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F ψ"
by (meson finite.insertI insert_subsetI nprv_cut)

lemma nprv_cut2:
"nprv F φ1 ⟹ nprv F φ2 ⟹
F ⊆ fmla ⟹ finite F ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv (insert φ2 (insert φ1 F)) ψ ⟹ nprv F ψ"
by (meson finite.insertI insert_subsetI nprv_mono nprv_strong_cut2 subset_insertI)

text ‹Useful for fine control of the eigenformula:›

lemma nprv_insertShiftI:
"nprv (insert φ1 (insert φ2 F)) ψ ⟹ nprv (insert φ2 (insert φ1 F)) ψ"

lemma nprv_insertShift2I:
"nprv (insert φ3 (insert φ1 (insert φ2 F))) ψ ⟹ nprv (insert φ1 (insert φ2 (insert φ3 F))) ψ"

section ‹Back and Forth between Hilbert and Natural Deduction›

text ‹This is now easy, thanks to the large number of facts we have
proved for Hilbert-style deduction›

lemma prv_nprvI: "prv φ ⟹ φ ∈ fmla ⟹ F ⊆ fmla ⟹ finite F ⟹ nprv F φ"
using prv_nprv0I

thm prv_nprv0I

lemma prv_nprv1I:
assumes "φ ∈ fmla" "ψ ∈ fmla" and "prv (imp φ ψ)"
shows "nprv {φ} ψ"
using assms unfolding nprv_def by (simp add: prv_scnj_imp)

lemma prv_nprv2I:
assumes "prv (imp φ1 (imp φ2 ψ))" "φ1 ∈ fmla" "φ2 ∈ fmla" "ψ ∈ fmla"
shows "nprv {φ1,φ2} ψ"
using assms unfolding nprv_def
by (meson cnj empty_subsetI finite.simps insert_subsetI prv_cnj_imp_monoR2 prv_prv_imp_trans prv_scnj2_imp_cnj scnj)

lemma nprv_prvI: "nprv {} φ ⟹ φ ∈ fmla ⟹ prv φ"
using prv_nprv_emp by auto

section ‹More Structural Properties›

lemma nprv_clear: "nprv {} φ ⟹ F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ nprv F φ"
by (rule nprv_mono) auto

lemma nprv_cut_set:
assumes F:  "finite F" "F ⊆ fmla" and G: "finite G" "G ⊆ fmla" "χ ∈ fmla"
and n1: "⋀ ψ. ψ ∈ G ⟹ nprv F ψ" and n2: "nprv (G ∪ F) χ"
shows "nprv F χ"
using G F n1 n2 proof(induction arbitrary: F χ)
case (insert ψ G F χ)
hence 0: "nprv F ψ" by auto
have 1: "nprv (insert ψ F) χ"
using insert.prems  apply- apply(rule insert.IH)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (meson finite.simps insert_subset nprv_mono subsetD subset_insertI)
by auto
show ?case using insert.prems by (intro nprv_cut[OF 0 1]) auto
qed(insert nprv_clear, auto)

lemma nprv_clear2_1:
"nprv {φ2} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2} ψ"
by (rule nprv_mono) auto

lemma nprv_clear2_2:
"nprv {φ1} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2} ψ"
by (rule nprv_mono) auto

lemma nprv_clear3_1:
"nprv {φ2,φ3} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3} ψ"
by (rule nprv_mono) auto

lemma nprv_clear3_2:
"nprv {φ1,φ3} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3} ψ"
by (rule nprv_mono) auto

lemma nprv_clear3_3:
"nprv {φ1,φ2} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3} ψ"
by (rule nprv_mono) auto

lemma nprv_clear4_1:
"nprv {φ2,φ3,φ4} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4} ψ"
by (rule nprv_mono) auto

lemma nprv_clear4_2:
"nprv {φ1,φ3,φ4} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4} ψ"
by (rule nprv_mono) auto

lemma nprv_clear4_3:
"nprv {φ1,φ2,φ4} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4} ψ"
by (rule nprv_mono) auto

lemma nprv_clear4_4:
"nprv {φ1,φ2,φ3} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4} ψ"
by (rule nprv_mono) auto

lemma nprv_clear5_1:
"nprv {φ2,φ3,φ4,φ5} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ φ5 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4,φ5} ψ"
by (rule nprv_mono) auto

lemma nprv_clear5_2:
"nprv {φ1,φ3,φ4,φ5} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ φ5 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4,φ5} ψ"
by (rule nprv_mono) auto

lemma nprv_clear5_3:
"nprv {φ1,φ2,φ4,φ5} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ φ5 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4,φ5} ψ"
by (rule nprv_mono) auto

lemma nprv_clear5_4:
"nprv {φ1,φ2,φ3,φ5} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ φ5 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4,φ5} ψ"
by (rule nprv_mono) auto

lemma nprv_clear5_5:
"nprv {φ1,φ2,φ3,φ4} ψ ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ φ3 ∈ fmla ⟹ φ4 ∈ fmla ⟹ φ5 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv {φ1,φ2,φ3,φ4,φ5} ψ"
by (rule nprv_mono) auto

section ‹Properties Involving Substitution›

lemma nprv_subst:
assumes "x ∈ var" "t ∈ trm" "ψ ∈ fmla" "finite F" "F ⊆ fmla"
and 1: "nprv F ψ"
shows "nprv ((λφ. subst φ t x) ` F) (subst ψ t x)"
using assms using prv_subst[OF _ _ _ 1[unfolded nprv_def]]  unfolding nprv_def
by (intro prv_prv_imp_trans[OF _ _ _ prv_subst_scnj_imp]) auto

lemma nprv_subst_fresh:
assumes 0: "x ∈ var" "t ∈ trm" "ψ ∈ fmla" "finite F" "F ⊆ fmla"
"nprv F ψ" and 1: "x ∉ ⋃ (Fvars ` F)"
shows "nprv F (subst ψ t x)"
proof-
have 2: "(λφ. subst φ t x) ` F = F" unfolding image_def using assms by force
show ?thesis using nprv_subst[OF 0] unfolding 2 .
qed

lemma nprv_subst_rev:
assumes 0: "x ∈ var" "y ∈ var" "ψ ∈ fmla" "finite F" "F ⊆ fmla"
and f: "y = x ∨ (y ∉ Fvars ψ ∧ y ∉ ⋃ (Fvars ` F))"
and 1: "nprv ((λφ. subst φ (Var y) x) ` F) (subst ψ (Var y) x)"
shows "nprv F ψ"
proof-
have 0: "subst (subst ψ (Var y) x) (Var x) y = ψ"
using assms by (auto simp: subst_compose_eq_or)
have "nprv ((λφ. subst φ (Var x) y) ` (λφ. subst φ (Var y) x) ` F) ψ"
using assms apply(subst 0[symmetric]) by (rule nprv_subst) auto
moreover
have "prv (imp (scnj F)
(scnj ((λφ. subst φ (Var x) y) ` (λφ. subst φ (Var y) x) ` F)))"
using assms apply(intro prv_scnj_mono_imp)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal apply clarify
subgoal for _ _ φ
by (auto simp: subst_compose_eq_or intro!: bexI[of _ φ] prv_imp_refl2) . .
ultimately show ?thesis
unfolding nprv_def using assms
apply- by(rule prv_prv_imp_trans) auto
qed

lemma nprv_psubst:
assumes 0: "snd ` set txs ⊆ var" "fst ` set txs ⊆ trm" "ψ ∈ fmla" "finite F" "F ⊆ fmla"
"distinct (map snd txs)"
and 1: "nprv F ψ"
shows "nprv ((λφ. psubst φ txs) ` F) (psubst ψ txs)"
using assms  unfolding nprv_def
apply(intro prv_prv_imp_trans[OF _ _ _ prv_psubst_scnj_imp])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using prv_psubst[OF _ _ _ 1[unfolded nprv_def]]
by (metis imp psubst_imp scnj) .

section ‹Introduction and Elimination Rules›

text ‹We systematically leave the side-conditions at the end, to simplify reasoning.›

lemma nprv_impI:
"nprv (insert φ F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F (imp φ ψ)"
unfolding nprv_def
by (metis cnj finite.insertI insert_subset prv_cnj_imp prv_imp_cnj_scnj prv_imp_com prv_prv_imp_trans scnj)

lemma nprv_impI_rev:
assumes "nprv F (imp φ ψ)"
and "F ⊆ fmla" and "finite F" and "φ ∈ fmla" and "ψ ∈ fmla"
shows "nprv (insert φ F) ψ"
using assms unfolding nprv_def
by (metis cnj finite.insertI insert_subset prv_cnj_imp_monoR2 prv_eqv_imp_transi
prv_eqv_scnj_insert prv_imp_com scnj)

lemma nprv_impI_rev2:
assumes "nprv F (imp φ ψ)" and G: "insert φ F ⊆ G"
and "G ⊆ fmla" and "finite G" and "φ ∈ fmla" and "ψ ∈ fmla"
shows "nprv G ψ"
using assms apply- apply(rule nprv_mono[of "insert φ F"])
subgoal by (meson nprv_impI_rev order_trans rev_finite_subset subset_insertI)
by auto

lemma nprv_mp:
"nprv F (imp φ ψ) ⟹ nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F ψ"
unfolding nprv_def
by (metis (full_types) cnj prv_cnj_imp_monoR2 prv_imp_cnj prv_imp_refl prv_prv_imp_trans scnj)

lemma nprv_impE:
"nprv F (imp φ ψ) ⟹ nprv F φ ⟹  nprv (insert ψ F) χ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹ χ ∈ fmla ⟹
nprv F χ"
using nprv_cut nprv_mp by blast

lemmas nprv_impE0 = nprv_impE[OF nprv_hyp _ _, simped]
lemmas nprv_impE1 = nprv_impE[OF _ nprv_hyp _, simped]
lemmas nprv_impE2 = nprv_impE[OF _ _ nprv_hyp, simped]
lemmas nprv_impE01 = nprv_impE[OF nprv_hyp nprv_hyp _, simped]
lemmas nprv_impE02 = nprv_impE[OF nprv_hyp _ nprv_hyp, simped]
lemmas nprv_impE12 = nprv_impE[OF _ nprv_hyp nprv_hyp, simped]
lemmas nprv_impE012 = nprv_impE[OF nprv_hyp nprv_hyp nprv_hyp, simped]

lemma nprv_cnjI:
"nprv F φ ⟹ nprv F ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F (cnj φ ψ)"
unfolding nprv_def by (simp add: prv_imp_cnj)

lemma nprv_cnjE:
"nprv F (cnj φ1 φ2) ⟹ nprv (insert φ1 (insert φ2 F)) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F ψ"
unfolding nprv_def
by (metis cnj nprv_cut2 nprv_def prv_imp_cnjL prv_imp_cnjR prv_prv_imp_trans scnj)

lemmas nprv_cnjE0 = nprv_cnjE[OF nprv_hyp _, simped]
lemmas nprv_cnjE1 = nprv_cnjE[OF _ nprv_hyp, simped]
lemmas nprv_cnjE01 = nprv_cnjE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_dsjIL:
"nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F (dsj φ ψ)"
unfolding nprv_def by (meson dsj prv_dsj_impL prv_prv_imp_trans scnj)

lemma nprv_dsjIR:
"nprv F ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F (dsj φ ψ)"
unfolding nprv_def by (meson dsj prv_dsj_impR prv_prv_imp_trans scnj)

lemma nprv_dsjE:
assumes "nprv F (dsj φ ψ)"
and "nprv (insert φ F) χ" "nprv (insert ψ F) χ"
and "F ⊆ fmla" "finite F" "φ ∈ fmla" "ψ ∈ fmla" "χ ∈ fmla"
shows "nprv F χ"
proof-
have "nprv F (imp (dsj φ ψ) χ)"
by (meson assms dsj imp nprv_def nprv_impI prv_imp_com prv_imp_dsjEE scnj)
hence "nprv (insert (dsj φ ψ) F) χ" using assms
thus ?thesis using assms by (meson dsj nprv_cut)
qed

lemmas nprv_dsjE0 = nprv_dsjE[OF nprv_hyp _ _, simped]
lemmas nprv_dsjE1 = nprv_dsjE[OF _ nprv_hyp _, simped]
lemmas nprv_dsjE2 = nprv_dsjE[OF _ _ nprv_hyp, simped]
lemmas nprv_dsjE01 = nprv_dsjE[OF nprv_hyp nprv_hyp _, simped]
lemmas nprv_dsjE02 = nprv_dsjE[OF nprv_hyp _ nprv_hyp, simped]
lemmas nprv_dsjE12 = nprv_dsjE[OF _ nprv_hyp nprv_hyp, simped]
lemmas nprv_dsjE012 = nprv_dsjE[OF nprv_hyp nprv_hyp nprv_hyp, simped]

lemma nprv_flsE: "nprv F fls ⟹ F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹  nprv F φ"
unfolding nprv_def using prv_prv_imp_trans scnj by blast

lemmas nprv_flsE0 = nprv_flsE[OF nprv_hyp, simped]

lemma nprv_truI: "F ⊆ fmla ⟹ finite F ⟹ nprv F tru"
unfolding nprv_def by (simp add: prv_imp_tru)

lemma nprv_negI:
"nprv (insert φ F) fls ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹
nprv F (neg φ)"
unfolding neg_def by (auto intro: nprv_impI)

lemma nprv_neg_fls:
"nprv F (neg φ) ⟹ nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F fls"
unfolding neg_def using nprv_mp by blast

lemma nprv_negE:
"nprv F (neg φ) ⟹ nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv F ψ"
using nprv_flsE nprv_neg_fls by blast

lemmas nprv_negE0 = nprv_negE[OF nprv_hyp _, simped]
lemmas nprv_negE1 = nprv_negE[OF _ nprv_hyp, simped]
lemmas nprv_negE01 = nprv_negE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_scnjI:
"(⋀ ψ. ψ ∈ G ⟹ nprv F ψ) ⟹
F ⊆ fmla ⟹ finite F ⟹ G ⊆ fmla ⟹ finite G ⟹
nprv F (scnj G)"
unfolding nprv_def by (simp add: prv_imp_scnj)

lemma nprv_scnjE:
"nprv F (scnj G) ⟹ nprv (G ∪ F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ G ⊆ fmla ⟹ finite G ⟹ ψ ∈ fmla ⟹
nprv F ψ"
apply(rule nprv_cut_set[of _ G])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (meson in_mono nprv_def prv_prv_imp_trans prv_scnj_imp_in scnj) .

lemmas nprv_scnjE0 = nprv_scnjE[OF nprv_hyp _, simped]
lemmas nprv_scnjE1 = nprv_scnjE[OF _ nprv_hyp, simped]
lemmas nprv_scnjE01 = nprv_scnjE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_lcnjI:
"(⋀ ψ. ψ ∈ set ψs ⟹ nprv F ψ) ⟹
F ⊆ fmla ⟹ finite F ⟹ set ψs ⊆ fmla ⟹
nprv F (lcnj ψs)"
unfolding nprv_def by (simp add: prv_imp_lcnj)

lemma nprv_lcnjE:
"nprv F (lcnj φs) ⟹ nprv (set φs ∪ F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ set φs ⊆ fmla ⟹ ψ ∈ fmla ⟹
nprv F ψ"
apply(rule nprv_cut_set[of _ "set φs ∪ F"])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
apply (elim UnE)
apply (meson lcnj nprv_def prv_lcnj_imp_in prv_prv_imp_trans scnj subset_code(1))
by auto
subgoal by auto .

lemmas nprv_lcnjE0 = nprv_lcnjE[OF nprv_hyp _, simped]
lemmas nprv_lcnjE1 = nprv_lcnjE[OF _ nprv_hyp, simped]
lemmas nprv_lcnjE01 = nprv_lcnjE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_sdsjI:
"nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ G ⊆ fmla ⟹ finite G ⟹ φ ∈ G ⟹
nprv F (sdsj G)"
unfolding nprv_def by (simp add: prv_imp_sdsj)

lemma nprv_sdsjE:
assumes "nprv F (sdsj G)"
and "⋀ ψ. ψ ∈ G ⟹ nprv (insert ψ F) χ"
and "F ⊆ fmla" "finite F" "G ⊆ fmla" "finite G" "χ ∈ fmla"
shows "nprv F χ"
proof-
have 0: "prv (imp (sdsj G) (imp (scnj F) χ))"
using assms apply(intro prv_sdsj_imp)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (meson nprv_def nprv_impI prv_imp_com scnj set_rev_mp) .
hence "nprv F (imp (sdsj G) χ)"
by (simp add: 0 assms nprv_def prv_imp_com)
thus ?thesis using assms nprv_mp by blast
qed

lemmas nprv_sdsjE0 = nprv_sdsjE[OF nprv_hyp _, simped]
lemmas nprv_sdsjE1 = nprv_sdsjE[OF _ nprv_hyp, simped]
lemmas nprv_sdsjE01 = nprv_sdsjE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_ldsjI:
"nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ set φs ⊆ fmla ⟹  φ ∈ set φs ⟹
nprv F (ldsj φs)"

lemma nprv_ldsjE:
assumes "nprv F (ldsj ψs)"
and "⋀ ψ. ψ ∈ set ψs ⟹ nprv (insert ψ F) χ"
and "F ⊆ fmla" "finite F" "set ψs ⊆ fmla"  "χ ∈ fmla"
shows "nprv F χ"
proof-
have 0: "prv (imp (ldsj ψs) (imp (scnj F) χ))"
using assms apply(intro prv_ldsj_imp)
subgoal by auto
subgoal by auto
subgoal by (meson nprv_def nprv_impI prv_imp_com scnj set_rev_mp) .
hence "nprv F (imp (ldsj ψs) χ)"
by (simp add: 0 assms nprv_def prv_imp_com)
thus ?thesis using assms nprv_mp by blast
qed

lemmas nprv_ldsjE0 = nprv_ldsjE[OF nprv_hyp _, simped]
lemmas nprv_ldsjE1 = nprv_ldsjE[OF _ nprv_hyp, simped]
lemmas nprv_ldsjE01 = nprv_ldsjE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_allI:
"nprv F φ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ x ∈ var ⟹ x ∉ ⋃ (Fvars ` F) ⟹
nprv F (all x φ)"
unfolding nprv_def by (rule prv_all_imp_gen) auto

lemma nprv_allE:
assumes "nprv F (all x φ)" "nprv (insert (subst φ t x) F) ψ"
"F ⊆ fmla" "finite F" "φ ∈ fmla" "t ∈ trm" "x ∈ var" "ψ ∈ fmla"
shows "nprv F ψ"
proof-
have "nprv F (subst φ t x)"
using assms unfolding nprv_def by (meson all subst prv_all_inst prv_prv_imp_trans scnj)
thus ?thesis by (meson assms local.subst nprv_cut)
qed

lemmas nprv_allE0 = nprv_allE[OF nprv_hyp _, simped]
lemmas nprv_allE1 = nprv_allE[OF _ nprv_hyp, simped]
lemmas nprv_allE01 = nprv_allE[OF nprv_hyp nprv_hyp, simped]

lemma nprv_exiI:
"nprv F (subst φ t x) ⟹
F ⊆ fmla ⟹ finite F ⟹ φ ∈ fmla ⟹ t ∈ trm ⟹ x ∈ var ⟹
nprv F (exi x φ)"
unfolding nprv_def by (meson exi local.subst prv_exi_inst prv_prv_imp_trans scnj)

lemma nprv_exiE:
assumes n: "nprv F (exi x φ)"
and nn: "nprv (insert φ F) ψ"
and 0[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "x ∈ var" "ψ ∈ fmla"
and x: "x ∉ ⋃ (Fvars ` F)" "x ∉ Fvars ψ"
shows "nprv F ψ"
proof-
have "nprv F (imp (exi x φ) ψ)" unfolding nprv_def apply(rule prv_imp_com)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal apply(rule prv_exi_imp_gen)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using x by auto
subgoal apply(rule prv_imp_com)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms(3-5) assms(7) nn nprv_def nprv_impI by blast . . .
thus ?thesis using n assms nprv_mp by blast
qed

lemmas nprv_exiE0 = nprv_exiE[OF nprv_hyp _, simped]
lemmas nprv_exiE1 = nprv_exiE[OF _ nprv_hyp, simped]
lemmas nprv_exiE01 = nprv_exiE[OF nprv_hyp nprv_hyp, simped]

section ‹Adding Lemmas of Various Shapes into the Proof Context›

assumes "prv φ" "nprv (insert φ F) ψ"
and "φ ∈ fmla" "ψ ∈ fmla" and "F ⊆ fmla" and "finite F"
shows "nprv F ψ"
using assms nprv_cut prv_nprvI by blast

assumes "prv (imp φ1 φ2)"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla"
and "nprv F φ1"
shows "nprv F φ2"
by (meson assms nprv_def prv_prv_imp_trans scnj)

assumes "prv (imp φ1 φ2)" and "nprv F φ1" and "nprv ((insert φ2) F) ψ"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla" "ψ ∈ fmla"
shows "nprv F ψ"
using assms nprv_addImpLemmaI nprv_cut by blast

assumes "prv (imp φ1 (imp φ2 φ3))"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla"
and "nprv F φ1" "nprv F φ2"
shows "nprv F φ3"
by (meson assms imp nprv_addImpLemmaI nprv_mp)

assumes "prv (imp φ1 (imp φ2 φ3))" and "nprv F φ1" and "nprv F φ2" and "nprv ((insert φ3) F) ψ"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla"  "φ3 ∈ fmla" "ψ ∈ fmla"
shows "nprv F ψ"

assumes "prv (imp φ1 (imp φ2 (imp φ3 φ4)))"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla" "φ4 ∈ fmla"
and "nprv F φ1" "nprv F φ2" "nprv F φ3"
shows "nprv F φ4"
by (meson assms imp nprv_addImpLemmaI nprv_mp)

assumes "prv (imp φ1 (imp φ2 (imp φ3 φ4)))"  and "nprv F φ1" and "nprv F φ2" and "nprv F φ3"
and "nprv ((insert φ4) F) ψ"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla" "φ3 ∈ fmla" "φ4 ∈ fmla" "ψ ∈ fmla"
shows "nprv F ψ"

assumes "prv (dsj φ1 φ2)" and "nprv (insert φ1 F) ψ" and "nprv ((insert φ2) F) ψ"
and "F ⊆ fmla" "finite F" "φ1 ∈ fmla" "φ2 ∈ fmla" "ψ ∈ fmla"
shows "nprv F ψ"
by (meson assms dsj nprv_clear nprv_dsjE prv_nprv0I)

section ‹Rules for Equality›

text ‹Reflexivity:›
lemma nprv_eql_reflI: "F ⊆ fmla ⟹ finite F ⟹ t ∈ trm ⟹ nprv F (eql t t)"

lemma nprv_eq_eqlI: "t1 = t2 ⟹ F ⊆ fmla ⟹ finite F ⟹ t1 ∈ trm ⟹ nprv F (eql t1 t2)"

text ‹Symmetry:›
lemmas nprv_eql_symI =  nprv_addImpLemmaI[OF prv_eql_sym, simped, rotated 4]
lemmas nprv_eql_symE =  nprv_addImpLemmaE[OF prv_eql_sym, simped, rotated 2]

lemmas nprv_eql_symE0 =  nprv_eql_symE[OF nprv_hyp _, simped]
lemmas nprv_eql_symE1 =  nprv_eql_symE[OF _ nprv_hyp, simped]
lemmas nprv_eql_symE01 =  nprv_eql_symE[OF nprv_hyp nprv_hyp, simped]

text ‹Transitivity:›
lemmas nprv_eql_transI = nprv_addImp2LemmaI[OF prv_eql_imp_trans, simped, rotated 5]
lemmas nprv_eql_transE = nprv_addImp2LemmaE[OF prv_eql_imp_trans, simped, rotated 3]

lemmas nprv_eql_transE0 = nprv_eql_transE[OF nprv_hyp _ _, simped]
lemmas nprv_eql_transE1 = nprv_eql_transE[OF _ nprv_hyp _, simped]
lemmas nprv_eql_transE2 = nprv_eql_transE[OF _ _ nprv_hyp, simped]
lemmas nprv_eql_transE01 = nprv_eql_transE[OF nprv_hyp nprv_hyp _, simped]
lemmas nprv_eql_transE02 = nprv_eql_transE[OF nprv_hyp _ nprv_hyp, simped]
lemmas nprv_eql_transE12 = nprv_eql_transE[OF _ nprv_hyp nprv_hyp, simped]
lemmas nprv_eql_transE012 = nprv_eql_transE[OF nprv_hyp nprv_hyp nprv_hyp, simped]

text ‹Substitutivity:›
lemmas nprv_eql_substI =
lemmas nprv_eql_substE = nprv_addImp2LemmaE[OF prv_eql_subst_trm_rev, simped, rotated 4]

lemmas nprv_eql_substE0 = nprv_eql_substE[OF nprv_hyp _ _, simped]
lemmas nprv_eql_substE1 = nprv_eql_substE[OF _ nprv_hyp _, simped]
lemmas nprv_eql_substE2 = nprv_eql_substE[OF _ _ nprv_hyp, simped]
lemmas nprv_eql_substE01 = nprv_eql_substE[OF nprv_hyp nprv_hyp _, simped]
lemmas nprv_eql_substE02 = nprv_eql_substE[OF nprv_hyp _ nprv_hyp, simped]
lemmas nprv_eql_substE12 = nprv_eql_substE[OF _ nprv_hyp nprv_hyp, simped]
lemmas nprv_eql_substE012 = nprv_eql_substE[OF nprv_hyp nprv_hyp nprv_hyp, simped]

section ‹Other Rules›

lemma nprv_cnjH:
"nprv (insert φ1 (insert φ2 F)) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ φ1 ∈ fmla ⟹ φ2 ∈ fmla ⟹ ψ ∈ fmla ⟹
nprv (insert (cnj φ1 φ2) F) ψ"
apply(rule nprv_cut2[of _ φ1 φ2])
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
subgoal by (auto simp: nprv_impI_rev prv_imp_cnjL prv_imp_cnjR prv_nprvI)
by (meson cnj finite.insertI insert_iff insert_subset nprv_mono subset_insertI)

lemma nprv_exi_commute:
assumes [simp]: "x ∈ var" "y ∈ var" "φ ∈ fmla"
shows "nprv {exi x (exi y φ)} (exi y (exi x φ))"
apply(rule nprv_exiE0[of x "exi y φ"], auto)
apply(rule nprv_clear2_2, auto)
apply(rule nprv_exiE0[of y φ], auto)
apply(rule nprv_clear2_2, auto)
apply(rule nprv_exiI[of _ _ "Var y"], auto)
by (rule nprv_exiI[of _ _ "Var x"], auto)

lemma prv_exi_commute:
assumes [simp]: "x ∈ var" "y ∈ var" "φ ∈ fmla"
shows "prv (imp (exi x (exi y φ)) (exi y (exi x φ)))"
apply(rule nprv_prvI, auto)
apply(rule nprv_impI, auto)
by (rule nprv_exi_commute, auto)

end (* context Deduct_with_False_Disj *)

section ‹Natural Deduction for the Exists-Unique Quantifier›

context Deduct_with_False_Disj_Rename
begin

lemma nprv_exuI:
assumes n1: "nprv F (subst φ t x)" and n2: "nprv (insert φ F) (eql (Var x) t)"
and i[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "t ∈ trm" "x ∈ var"   "x ∉ FvarsT t"
and u: "x ∉ (⋃φ ∈ F. Fvars φ)"
shows "nprv F (exu x φ)"
proof-
define z where "z ≡ getFr [x] [t] [φ]"
have z_facts[simp]: "z ∈ var" "z ≠ x" "x ≠ z"   "z ∉ FvarsT t" "z ∉ Fvars φ"
using getFr_FvarsT_Fvars[of "[x]" "[t]" "[φ]"] unfolding z_def[symmetric] by auto
have 0: "exu x φ = cnj (exi x φ) (exi z (all x (imp φ (eql (Var x) (Var z)))))"
by (simp add: exu_def_var[of _ z])
show ?thesis
unfolding 0
apply(rule nprv_cnjI, auto)
apply(rule nprv_exiI[of _ _ t], auto)
apply(rule n1)
(**)
apply(rule nprv_exiI[of _ _ t], auto)
apply(rule nprv_allI, insert u, auto)
apply(rule nprv_impI, insert n2, auto)
done
qed

lemma nprv_exuI_var:
assumes n1: "nprv F (subst φ t x)" and n2: "nprv (insert (subst φ (Var y) x) F) (eql (Var y) t)"
and i[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "t ∈ trm" "x ∈ var"
"y ∈ var" "y ∉ FvarsT t" and u: "y ∉ (⋃φ ∈ F. Fvars φ)" and yx: "y = x ∨ y ∉ Fvars φ"
shows "nprv F (exu x φ)"
apply(subst exu_rename2[of _ _ y])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using yx by auto
subgoal apply(intro nprv_exuI[of _ _ t])
subgoal by (metis i(3) i(4) i(5) i(6) n1 subst_same_Var subst_subst yx)
using n2 u by auto .

text ‹This turned out to be the most useful introduction rule for arithmetic:›
lemma nprv_exuI_exi:
assumes n1: "nprv F (exi x φ)" and n2: "nprv (insert (subst φ (Var y) x) (insert φ F)) (eql (Var y) (Var x))"
and i[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "x ∈ var" "y ∈ var" "y ≠ x" "y ∉ Fvars φ"
and u: "x ∉ (⋃φ ∈ F. Fvars φ)" "y ∉ (⋃φ ∈ F. Fvars φ)"
shows "nprv F (exu x φ)"
proof-
have e: "nprv (insert φ F) (exu x φ)"
apply(rule nprv_exuI_var[of _ _ "Var x" _ y])
using n2 u by auto
show ?thesis
apply(rule nprv_cut[OF n1], auto)
apply(rule nprv_exiE0, insert u, auto)
apply(rule nprv_mono[OF e], auto) .
qed

lemma prv_exu_imp_exi:
assumes [simp]: "φ ∈ fmla" "x ∈ var"
shows "prv (imp (exu x φ) (exi x φ))"
proof-
define z where z: "z ≡ getFr [x] [] [φ]"
have z_facts[simp]: "z ∈ var" "z ≠ x" "x ≠ z" "z ∉ Fvars φ"
using getFr_FvarsT_Fvars[of "[x]" "[]" "[φ]"] unfolding z by auto
show ?thesis unfolding exu_def
by (simp add: Let_def z[symmetric] prv_imp_cnjL)
qed

lemma prv_exu_exi:
assumes "x ∈ var" "φ ∈ fmla" "prv (exu x φ)"
shows "prv (exi x φ)"
by (meson assms exi exu prv_exu_imp_exi prv_imp_mp)

text ‹This is just exu behaving for elimination and forward like exi:›
lemma nprv_exuE_exi:
assumes n1: "nprv F (exu x φ)" and n2: "nprv (insert φ F) ψ"
and i[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "x ∈ var" "ψ ∈ fmla" "x ∉ Fvars ψ"
and u: "x ∉ (⋃φ ∈ F. Fvars φ)"
shows "nprv F ψ"
using assms apply- apply(rule nprv_exiE[of _ x φ])
subgoal by (rule nprv_addImpLemmaI[OF prv_exu_imp_exi[of φ x]]) auto
by auto

lemma nprv_exuF_exi:
assumes n1: "exu x φ ∈ F" and n2: "nprv (insert φ F) ψ"
and i[simp]: "F ⊆ fmla" "finite F" "φ ∈ fmla" "x ∈ var" "ψ ∈ fmla" "x ∉ Fvars ψ"
and u: "x ∉ (⋃φ ∈ F. Fvars φ)"
shows "nprv F ψ"
using assms  nprv_exuE_exi nprv_hyp by metis

lemma prv_exu_uni:
assumes [simp]: "φ ∈ fmla" "x ∈ var" "t1 ∈ trm" "t2 ∈ trm"
shows "prv (imp (exu x φ) (imp (subst φ t1 x) (imp (subst φ t2 x) (eql t1 t2))))"
proof-
define z where z: "z ≡ getFr [x] [t1,t2] [φ]"
have z_facts[simp]: "z ∈ var" "z ≠ x" "x ≠ z" "z ∉ Fvars φ"  "z ∉ FvarsT t1" "z ∉ FvarsT t2"
using getFr_FvarsT_Fvars[of "[x]" "[t1,t2]" "[φ]"] unfolding z by auto
show ?thesis
apply(rule nprv_prvI, auto)
apply(rule nprv_impI, auto)
apply(rule nprv_cnjE0, auto)
apply(rule nprv_clear3_1, auto)
apply(rule nprv_clear2_2, auto)
apply(rule nprv_exiE0, auto)
apply(rule nprv_clear2_2, auto)
apply(rule nprv_allE0[of _ _ _ t1], auto)
apply(rule nprv_allE0[of _ _ _ t2], auto)
apply(rule nprv_clear3_3, auto)
apply(rule nprv_impI, auto)
apply(rule nprv_impI, auto)
apply(rule nprv_impE01, auto)
apply(rule nprv_clear5_2, auto)
apply(rule nprv_clear4_3, auto)
apply(rule nprv_impE01, auto)
apply(rule nprv_clear4_3, auto)
apply(rule nprv_clear3_3, auto)
apply(rule nprv_eql_symE0[of t2 "Var z"], auto)
apply(rule nprv_eql_transE012, auto) .
qed

lemmas nprv_exuE_uni = nprv_addImp3LemmaE[OF prv_exu_uni,simped,rotated 4]
lemmas nprv_exuF_uni = nprv_exuE_uni[OF nprv_hyp,simped]

end ― ‹context @{locale Deduct_with_False_Disj}›

section ‹Eisbach Notation for Natural Deduction Proofs›

text ‹The proof pattern will be: On a goal of the form @{term "nprv F φ"},
we apply a rule (usually an introduction, elimination, or cut/lemma-addition
rule), then discharge the side-conditions with @{method auto}, ending up with zero,
one or two goals of the same nprv-shape. This process is abstracted away in the
Eisbach nrule method:›

method nrule uses r = (rule r, auto?)
(* For future developments, in case we refine what we do
(and also for documentation): This is supposed to create two main nprv-subgoals: *)
method nrule2 uses r = (rule r, auto?)

text ‹Methods for chaining several nrule applications:›

method nprover2 uses r1 r2 =
(-,(((nrule r: r1)?, (nrule r: r2)?) ; fail))
method nprover3 uses r1 r2 r3 =
(-,(((nrule r: r1)?, (nrule r: r2)?, (nrule r: r3)?) ; fail))
method nprover4 uses r1 r2 r3 r4 =
(-,(((nrule r: r1)?, (nrule r: r2)?, (nrule r: r3)?, (nrule r: r4)?) ; fail))
method nprover5 uses r1 r2 r3 r4 r5 =
(-,((nrule r: r1)?, (nrule r: r2)?, (nrule r: r3)?,
(nrule r: r4)?, (nrule r: r5)?) ; fail)
method nprover6 uses r1 r2 r3 r4 r5 r6 =
(-,((nrule r: r1)?, (nrule r: r2)?, (nrule r: r3)?,
(nrule r: r4)?, (nrule r: r5)?, (nrule r: r6)?) ; fail)

(*<*)
end
(*>*)```