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
by (simp add: prv_scnj_imp_in subset_iff)


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)) ψ"
by (simp add: insert_commute)

lemma nprv_insertShift2I:
"nprv (insert φ3 (insert φ1 (insert φ2 F))) ψ ⟹ nprv (insert φ1 (insert φ2 (insert φ3 F))) ψ"
by (simp add: insert_commute)


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
by (simp add: nprv_def prv_imp_triv)

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
    by (simp add: nprv_impI_rev)
  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)"
unfolding nprv_def by(simp add: prv_imp_ldsj)

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›

lemma nprv_addLemmaE:
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

lemmas nprv_addLemmaE1 = nprv_addLemmaE[OF _ nprv_hyp, simped]

lemma nprv_addImpLemmaI:
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)

lemma nprv_addImpLemmaE:
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

lemmas nprv_addImpLemmaE1 = nprv_addImpLemmaE[OF _ nprv_hyp _, simped]
lemmas nprv_addImpLemmaE2 = nprv_addImpLemmaE[OF _ _ nprv_hyp, simped]
lemmas nprv_addImpLemmaE12 = nprv_addImpLemmaE[OF _ nprv_hyp nprv_hyp, simped]

lemma nprv_addImp2LemmaI:
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)

lemma nprv_addImp2LemmaE:
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 ψ"
by (meson assms nprv_addImp2LemmaI nprv_cut)

lemmas nprv_addImp2LemmaE1 = nprv_addImp2LemmaE[OF _ nprv_hyp _ _, simped]
lemmas nprv_addImp2LemmaE2 = nprv_addImp2LemmaE[OF _ _ nprv_hyp _, simped]
lemmas nprv_addImp2LemmaE3 = nprv_addImp2LemmaE[OF _ _ _ nprv_hyp, simped]
lemmas nprv_addImp2LemmaE12 = nprv_addImp2LemmaE[OF _ nprv_hyp nprv_hyp _, simped]
lemmas nprv_addImp2LemmaE13 = nprv_addImp2LemmaE[OF _ nprv_hyp _ nprv_hyp, simped]
lemmas nprv_addImp2LemmaE23 = nprv_addImp2LemmaE[OF _ _ nprv_hyp nprv_hyp, simped]
lemmas nprv_addImp2LemmaE123 = nprv_addImp2LemmaE[OF _ nprv_hyp nprv_hyp nprv_hyp, simped]

lemma nprv_addImp3LemmaI:
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)

lemma nprv_addImp3LemmaE:
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 ψ"
by (meson assms nprv_addImp3LemmaI nprv_cut)

lemmas nprv_addImp3LemmaE1 = nprv_addImp3LemmaE[OF _ nprv_hyp _ _ _, simped]
lemmas nprv_addImp3LemmaE2 = nprv_addImp3LemmaE[OF _ _ nprv_hyp _ _, simped]
lemmas nprv_addImp3LemmaE3 = nprv_addImp3LemmaE[OF _ _ _ nprv_hyp _, simped]
lemmas nprv_addImp3LemmaE4 = nprv_addImp3LemmaE[OF _ _ _ _ nprv_hyp, simped]
lemmas nprv_addImp3LemmaE12 = nprv_addImp3LemmaE[OF _ nprv_hyp nprv_hyp _ _, simped]
lemmas nprv_addImp3LemmaE13 = nprv_addImp3LemmaE[OF _ nprv_hyp _ nprv_hyp _, simped]
lemmas nprv_addImp3LemmaE14 = nprv_addImp3LemmaE[OF _ nprv_hyp _ _ nprv_hyp, simped]
lemmas nprv_addImp3LemmaE23 = nprv_addImp3LemmaE[OF _ _ nprv_hyp nprv_hyp _, simped]
lemmas nprv_addImp3LemmaE24 = nprv_addImp3LemmaE[OF _ _ nprv_hyp _ nprv_hyp, simped]
lemmas nprv_addImp3LemmaE34 = nprv_addImp3LemmaE[OF _ _ _ nprv_hyp nprv_hyp, simped]
lemmas nprv_addImp3LemmaE123 = nprv_addImp3LemmaE[OF _ nprv_hyp nprv_hyp nprv_hyp _, simped]
lemmas nprv_addImp3LemmaE124 = nprv_addImp3LemmaE[OF _ nprv_hyp nprv_hyp _ nprv_hyp, simped]
lemmas nprv_addImp3LemmaE134 = nprv_addImp3LemmaE[OF _ nprv_hyp _ nprv_hyp nprv_hyp, simped]
lemmas nprv_addImp3LemmaE234 = nprv_addImp3LemmaE[OF _ _ nprv_hyp nprv_hyp nprv_hyp, simped]
lemmas nprv_addImp3LemmaE1234 = nprv_addImp3LemmaE[OF _ nprv_hyp nprv_hyp nprv_hyp nprv_hyp, simped]

lemma nprv_addDsjLemmaE:
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)

lemmas nprv_addDsjLemmaE1 = nprv_addDsjLemmaE[OF _ nprv_hyp _, simped]
lemmas nprv_addDsjLemmaE2 = nprv_addDsjLemmaE[OF _ _ nprv_hyp, simped]
lemmas nprv_addDsjLemmaE12 = nprv_addDsjLemmaE[OF _ nprv_hyp nprv_hyp, simped]

section ‹Rules for Equality›

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

lemma nprv_eq_eqlI: "t1 = t2 ⟹ F ⊆ fmla ⟹ finite F ⟹ t1 ∈ trm ⟹ nprv F (eql t1 t2)"
by (simp add: prv_eql_reflT prv_nprvI)

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 =
nprv_addImp2LemmaI[OF prv_eql_subst_trm_rev, simped, rotated 6]
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(simp add: exu_def_var[of _ z])
  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
(*>*)