Theory Incompleteness.Pf_Predicates

chapter‹Formalizing Provability›

theory Pf_Predicates
imports Coding_Predicates
begin

section ‹Section 4 Predicates (Leading up to Pf)›

subsection ‹The predicate ‹SentP›, for the Sentiential (Boolean) Axioms›

definition Sent_axioms :: "hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool" where
 "Sent_axioms x y z w ≡
             x = q_Imp y y ∨
             x = q_Imp y (q_Disj y z) ∨
             x = q_Imp (q_Disj y y) y ∨
             x = q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) ∨
             x = q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w))"

definition Sent :: "hf set" where
 "Sent ≡ {x. ∃y z w. Form y ∧ Form z ∧ Form w ∧ Sent_axioms x y z w}"

nominal_function SentP :: "tm ⇒ fm"
  where "⟦atom y ♯ (z,w,x); atom z ♯ (w,x); atom w ♯ x⟧ ⟹
    SentP x = Ex y (Ex z (Ex w (FormP (Var y) AND FormP (Var z) AND FormP (Var w) AND
               ( (x EQ Q_Imp (Var y) (Var y)) OR
                 (x EQ Q_Imp (Var y) (Q_Disj (Var y) (Var z)) OR
                 (x EQ Q_Imp (Q_Disj (Var y) (Var y)) (Var y)) OR
                 (x EQ Q_Imp (Q_Disj (Var y) (Q_Disj (Var z) (Var w))) 
                             (Q_Disj (Q_Disj (Var y) (Var z)) (Var w))) OR
                 (x EQ Q_Imp (Q_Disj (Var y) (Var z))
                             (Q_Imp (Q_Disj (Q_Neg (Var y)) (Var w)) (Q_Disj (Var z) (Var w)))))))))"
  by (auto simp: eqvt_def SentP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows SentP_fresh_iff [simp]: "a ♯ SentP x ⟷ a ♯ x"                  (is ?thesis1)
   and eval_fm_SentP [simp]:   "eval_fm e (SentP x) ⟷ ⟦x⟧e ∈ Sent"    (is ?thesis2)
   and SentP_sf [iff]:         "Sigma_fm (SentP x)"                     (is ?thsf)
proof -
  obtain y::name and z::name and w::name  where "atom y ♯ (z,w,x)" "atom z ♯ (w,x)" "atom w ♯ x"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thsf
    by (auto simp: Sent_def Sent_axioms_def q_defs)
qed

subsection ‹The predicate ‹Equality_axP›, for the Equality Axioms›

definition Equality_ax :: "hf set" where
 "Equality_ax ≡ { ⟦«refl_ax»⟧e0, ⟦«eq_cong_ax»⟧e0, ⟦«mem_cong_ax»⟧e0, ⟦«eats_cong_ax»⟧e0 }"

function Equality_axP :: "tm ⇒ fm"
  where "Equality_axP x =
    x EQ «refl_ax» OR x EQ «eq_cong_ax» OR x EQ «mem_cong_ax» OR x EQ «eats_cong_ax»"
by auto

termination
  by lexicographic_order

lemma eval_fm_Equality_axP [simp]: "eval_fm e (Equality_axP x) ⟷ ⟦x⟧e ∈ Equality_ax"
  by (auto simp: Equality_ax_def intro: eval_quot_fm_ignore)

subsection ‹The predicate ‹HF_axP›, for the HF Axioms›

definition HF_ax :: "hf set" where
  "HF_ax ≡ {⟦«HF1»⟧e0, ⟦«HF2»⟧e0}"

function HF_axP :: "tm ⇒ fm"
  where "HF_axP x = x EQ «HF1» OR x EQ «HF2»"
by auto

termination
  by lexicographic_order

lemma eval_fm_HF_axP [simp]: "eval_fm e (HF_axP x) ⟷ ⟦x⟧e ∈ HF_ax"
  by (auto simp: HF_ax_def intro: eval_quot_fm_ignore)

lemma HF_axP_sf [iff]: "Sigma_fm (HF_axP t)"
  by auto


subsection ‹The specialisation axioms›

inductive_set Special_ax :: "hf set" where
  I: "⟦AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y⟧
      ⟹ q_Imp sx (q_Ex ax) ∈ Special_ax"

subsubsection ‹Defining the syntax›

nominal_function Special_axP :: "tm ⇒ fm" where
  "⟦atom v ♯ (p,sx,y,ax,x); atom x ♯ (p,sx,y,ax);
    atom ax ♯ (p,sx,y); atom y ♯ (p,sx); atom sx ♯ p⟧ ⟹
  Special_axP p = Ex v (Ex x (Ex ax (Ex y (Ex sx
                   (FormP (Var x) AND VarP (Var v) AND TermP (Var y) AND
                    AbstFormP (Var v) Zero (Var x) (Var ax) AND
                    SubstFormP (Var v) (Var y) (Var x) (Var sx) AND
                    p EQ Q_Imp (Var sx) (Q_Ex (Var ax)))))))"
  by (auto simp: eqvt_def Special_axP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows Special_axP_fresh_iff [simp]: "a ♯ Special_axP p ⟷ a ♯ p" (is ?thesis1)
   and eval_fm_Special_axP [simp]: "eval_fm e (Special_axP p) ⟷ ⟦p⟧e ∈ Special_ax" (is ?thesis2)
   and Special_axP_sf [iff]:       "Sigma_fm (Special_axP p)" (is ?thesis3)
proof -
  obtain v::name and x::name and ax::name and y::name and sx::name
    where "atom v ♯ (p,sx,y,ax,x)" "atom x ♯ (p,sx,y,ax)"
          "atom ax ♯ (p,sx,y)" "atom y ♯ (p,sx)" "atom sx ♯ p"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thesis3
    apply auto
    apply (metis q_Disj_def q_Ex_def q_Imp_def q_Neg_def Special_ax.intros)
    apply (metis q_Disj_def q_Ex_def q_Imp_def q_Neg_def Special_ax.cases)
    done
qed

subsubsection ‹Correctness (or, correspondence)›

lemma Special_ax_imp_special_axioms:
  assumes "x ∈ Special_ax" shows "∃A. x = ⟦«A»⟧e ∧ A ∈ special_axioms"
using assms
proof (induction rule: Special_ax.induct)
  case (I v x ax y sx)
  obtain fm::fm and u::tm where fm: "x = ⟦«fm»⟧e" and  u: "y = ⟦«u»⟧e"
    using I  by (auto elim!: Form_imp_is_fm Term_imp_is_tm)
  obtain B where x: "x  = ⟦quot_dbfm B⟧e"
            and ax: "ax = ⟦quot_dbfm (abst_dbfm (decode_Var v) 0 B)⟧e"
    using I AbstForm_imp_abst_dbfm  by force
  obtain B' where x': "x = ⟦quot_dbfm B'⟧e"
             and sx: "sx = ⟦quot_dbfm (subst_dbfm (trans_tm [] u) (decode_Var v) B')⟧e"
    using I  by (metis u SubstForm_imp_subst_dbfm_lemma quot_tm_def)
  have eq: "B'=B"
    by (metis quot_dbfm_inject_lemma x x')
  have "fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm ∈ special_axioms"
    by (metis special_axioms.intros)
  thus ?case using eq
    apply (auto simp: quot_simps q_defs 
                intro!: exI [where x = "fm((decode_Var v)::=u) IMP (Ex (decode_Var v) fm)"])
    apply (metis fm quot_dbfm_inject_lemma quot_fm_def subst_fm_trans_commute sx x')
    apply (metis abst_trans_fm ax fm quot_dbfm_inject_lemma quot_fm_def x)
    done
qed

lemma special_axioms_into_Special_ax: "A ∈ special_axioms ⟹ ⟦«A»⟧e ∈ Special_ax"
proof (induct rule: special_axioms.induct)
  case (I A i t)
  have "⟦«A(i::=t) IMP SyntaxN.Ex i A»⟧e =
        q_Imp ⟦quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))⟧e
              (q_Ex ⟦quot_dbfm (trans_fm [i] A)⟧e)"
    by (simp add: quot_fm_def q_defs)
  also have "... ∈ Special_ax"
    apply (rule Special_ax.intros [OF AbstForm_trans_fm])
    apply (auto simp: quot_fm_def [symmetric] intro: SubstForm_quot [unfolded eval_Var_q])
    done
  finally show ?case .
qed

text‹We have precisely captured the codes of the specialisation axioms.›
corollary Special_ax_eq_special_axioms: "Special_ax = (⋃A ∈ special_axioms. { ⟦«A»⟧e })"
  by (force dest: special_axioms_into_Special_ax Special_ax_imp_special_axioms)


subsection ‹The induction axioms›

inductive_set Induction_ax :: "hf set" where
  I: "⟦SubstForm v 0 x x0;
       SubstForm v w x xw;
       SubstForm v (q_Eats v w) x xevw;
       AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw;
       AbstForm v 0 (q_All allw) allvw;
       AbstForm v 0 x ax;
       v ≠ w; VarNonOccForm w x⟧
      ⟹ q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) ∈ Induction_ax"

subsubsection ‹Defining the syntax›

nominal_function Induction_axP :: "tm ⇒ fm" where
  "⟦atom ax ♯ (p,v,w,x,x0,xw,xevw,allw,allvw);
    atom allvw ♯ (p,v,w,x,x0,xw,xevw,allw); atom allw ♯ (p,v,w,x,x0,xw,xevw);
    atom xevw ♯ (p,v,w,x,x0,xw); atom xw ♯ (p,v,w,x,x0);
    atom x0 ♯ (p,v,w,x); atom x ♯ (p,v,w);
    atom w ♯ (p,v); atom v ♯ p⟧ ⟹
  Induction_axP p = Ex v (Ex w (Ex x (Ex x0 (Ex xw (Ex xevw (Ex allw (Ex allvw (Ex ax
               ((Var v NEQ Var w) AND VarNonOccFormP (Var w) (Var x) AND
                SubstFormP (Var v) Zero (Var x) (Var x0) AND
                SubstFormP (Var v) (Var w) (Var x) (Var xw) AND
                SubstFormP (Var v) (Q_Eats (Var v) (Var w)) (Var x) (Var xevw) AND
                AbstFormP (Var w) Zero (Q_Imp (Var x) (Q_Imp (Var xw) (Var xevw))) (Var allw) AND
                AbstFormP (Var v) Zero (Q_All (Var allw)) (Var allvw) AND
                AbstFormP (Var v) Zero (Var x) (Var ax) AND
                p EQ Q_Imp (Var x0) (Q_Imp (Q_All (Var allvw)) (Q_All (Var ax))))))))))))"
  by (auto simp: eqvt_def Induction_axP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows Induction_axP_fresh_iff [simp]: "a ♯ Induction_axP p ⟷ a ♯ p" (is ?thesis1)
   and eval_fm_Induction_axP [simp]:
      "eval_fm e (Induction_axP p) ⟷ ⟦p⟧e ∈ Induction_ax"    (is ?thesis2)
   and Induction_axP_sf [iff]: "Sigma_fm (Induction_axP p)" (is ?thesis3)
proof -
  obtain v::name and w::name and x::name and x0::name and xw::name and xevw::name
                 and allw::name and allvw::name and ax::name
    where atoms: "atom ax ♯ (p,v,w,x,x0,xw,xevw,allw,allvw)"
                 "atom allvw ♯ (p,v,w,x,x0,xw,xevw,allw)" "atom allw ♯ (p,v,w,x,x0,xw,xevw)"
                 "atom xevw ♯ (p,v,w,x,x0,xw)" "atom xw ♯ (p,v,w,x,x0)" "atom x0 ♯ (p,v,w,x)"
                 "atom x ♯ (p,v,w)" "atom w ♯ (p,v)" "atom v ♯ p"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis3
    by auto
  show ?thesis2
    proof
      assume "eval_fm e (Induction_axP p)"
      thus "⟦p⟧e ∈ Induction_ax" using atoms
        by (auto intro!: Induction_ax.I [unfolded q_defs])
    next
      assume "⟦p⟧e ∈ Induction_ax"
      thus "eval_fm e (Induction_axP p)"
        apply (rule Induction_ax.cases) using atoms
        apply (force simp: q_defs htuple_minus_1 intro!: AbstForm_imp_Ord)
        done
    qed
qed

subsubsection ‹Correctness (or, correspondence)›

lemma Induction_ax_imp_induction_axioms:
  assumes "x ∈ Induction_ax" shows "∃A. x = ⟦«A»⟧e ∧ A ∈ induction_axioms"
using assms
proof (induction rule: Induction_ax.induct)
  case (I v x x0 w xw xevw allw allvw ax)
  then have v: "is_Var v" and w: "is_Var w"
        and dvw [simp]: "decode_Var v ≠ decode_Var w"  "atom (decode_Var w) ♯ [decode_Var v]" 
    by (auto simp: AbstForm_def fresh_Cons)
  obtain A::fm where A: "x = ⟦«A»⟧e" and wfresh: "atom (decode_Var w) ♯ A"
    using I VarNonOccForm_imp_fresh  by blast
  then obtain A' A'' where A': "q_Imp (⟦«A»⟧e) (q_Imp xw xevw) = ⟦quot_dbfm A'⟧e"
                       and A'': "q_All allw = ⟦quot_dbfm A''⟧e"
    using I VarNonOccForm_imp_fresh by (auto dest!: AbstForm_imp_abst_dbfm)
  define Aw where "Aw = A(decode_Var v::=Var (decode_Var w))"
  define Ae where "Ae = A(decode_Var v::= Eats (Var (decode_Var v)) (Var (decode_Var w)))"
  have x0: "x0 = ⟦«A(decode_Var v::=Zero)»⟧e"  using I SubstForm_imp_subst_fm 
    by (metis A Form_quot_fm eval_fm_inject eval_tm.simps(1) quot_Zero)
  have xw: "xw = ⟦«Aw»⟧e"  using I SubstForm_imp_subst_fm
    by (metis A Form_quot_fm eval_fm_inject is_Var_imp_decode_Var w Aw_def)
  have "SubstForm v (⟦«Eats (Var (decode_Var v)) (Var (decode_Var w))»⟧e) x xevw"
    using I  by (simp add: quot_simps q_defs) (metis is_Var_iff v w)
  hence xevw: "xevw = ⟦«Ae»⟧e"
    by (metis A Ae_def Form_quot_fm SubstForm_imp_subst_fm eval_fm_inject)
  have ax: "ax = ⟦quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))⟧e"
    using I  by (metis A AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma quot_fm_def)
  have evw: "q_Imp x (q_Imp xw xevw) =
             ⟦quot_dbfm (trans_fm [] (A IMP (Aw IMP Ae)))⟧e"
    using A xw xevw  by (auto simp: quot_simps q_defs quot_fm_def)
  hence allw: "allw = ⟦quot_dbfm (abst_dbfm (decode_Var w) 0
                                    (trans_fm [] (A IMP (Aw IMP Ae))))⟧e"
    using I  by (metis AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma)
  then have evw: "q_All allw = ⟦quot_dbfm (trans_fm [] (All (decode_Var w) (A IMP (Aw IMP Ae))))⟧e"
    by (auto simp: q_defs abst_trans_fm)
  hence allvw: "allvw = ⟦quot_dbfm (abst_dbfm (decode_Var v) 0
                                     (trans_fm [] (All (decode_Var w) (A IMP (Aw IMP Ae)))))⟧e"
    using I  by (metis AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma)
  define ind_ax
    where "ind_ax =
        A(decode_Var v::=Zero) IMP
        ((All (decode_Var v) (All (decode_Var w) (A IMP (Aw IMP Ae)))) IMP
        (All (decode_Var v) A))"
  have "atom (decode_Var w) ♯ (decode_Var v, A)" using I wfresh v w
    by (metis atom_eq_iff decode_Var_inject fresh_Pair fresh_ineq_at_base)
  hence "ind_ax ∈ induction_axioms"
    by (auto simp: ind_ax_def Aw_def Ae_def induction_axioms.intros)
  thus ?case
    by (force simp: quot_simps q_defs ind_ax_def allvw ax x0 abst_trans_fm2 abst_trans_fm)
qed


lemma induction_axioms_into_Induction_ax:
  "A ∈ induction_axioms ⟹ ⟦«A»⟧e ∈ Induction_ax"
proof (induct rule: induction_axioms.induct)
  case (ind j i A)
  hence eq: "⟦«A(i::=Zero) IMP All i (All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP All i A»⟧e =
            q_Imp ⟦quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))⟧e
            (q_Imp (q_All (q_All
                  (q_Imp ⟦quot_dbfm (trans_fm [j, i] A)⟧e
                    (q_Imp
                      ⟦quot_dbfm (trans_fm [j, i] (A(i::=Var j)))⟧e
                      ⟦quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))⟧e))))
              (q_All ⟦quot_dbfm (trans_fm [i] A)⟧e))"
    by (simp add: quot_simps q_defs quot_subst_eq fresh_Cons fresh_Pair)
  have [simp]: "atom j ♯ [i]" using ind
    by (metis fresh_Cons fresh_Nil fresh_Pair)
  show ?case
  proof (simp only: eq, rule Induction_ax.intros [where v = "q_Var i" and w = "q_Var j"])
    show "SubstForm (q_Var i) 0 ⟦«A»⟧e
           ⟦quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))⟧e"
     by (metis SubstForm_subst_dbfm_eq Term_quot_tm eval_tm.simps(1) quot_Zero quot_fm_def quot_tm_def)
  next
    show "SubstForm (q_Var i) (q_Var j) ⟦«A»⟧e ⟦quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))⟧e"
      by (auto simp: quot_fm_def intro!: SubstForm_subst_dbfm_eq Term_Var)
         (metis q_Var_def)
  next
    show "SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) ⟦«A»⟧e
              ⟦quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))⟧e"
      unfolding quot_fm_def
        by (auto intro!: SubstForm_subst_dbfm_eq Term_Eats Term_Var) (simp add: q_defs)
  next
    show "AbstForm (q_Var j) 0
           (q_Imp ⟦«A»⟧e
              (q_Imp ⟦quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))⟧e
                     ⟦quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))⟧e))
           ⟦quot_dbfm (trans_fm [j] (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))))⟧e"
      by (rule AbstForm_trans_fm_eq [where A = "(A IMP A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))"])
         (auto simp: quot_simps q_defs quot_fm_def subst_fm_trans_commute_eq)
  next
    show "AbstForm (q_Var i) 0
     (q_All ⟦quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))⟧e)
     (q_All
       (q_Imp ⟦quot_dbfm (trans_fm [j, i] A)⟧e
         (q_Imp ⟦quot_dbfm (trans_fm [j, i] (A(i::=Var j)))⟧e
                ⟦quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))⟧e)))"
      apply (rule AbstForm_trans_fm_eq
               [where A = "All j (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j))))"])
      apply (auto simp: q_defs quot_fm_def)
      done
  next
    show "AbstForm (q_Var i) 0 (⟦«A»⟧e) ⟦quot_dbfm (trans_fm [i] A)⟧e"
      by (metis AbstForm_trans_fm)
  next
    show "q_Var i ≠ q_Var j" using ind
      by (simp add: q_Var_def)
  next
    show "VarNonOccForm (q_Var j) (⟦«A»⟧e)"
      by (metis fresh_Pair fresh_imp_VarNonOccForm ind)
  qed
qed

text‹We have captured the codes of the induction axioms.›
corollary Induction_ax_eq_induction_axioms:
  "Induction_ax = (⋃A ∈ induction_axioms. {⟦«A»⟧e})"
  by (force dest: induction_axioms_into_Induction_ax Induction_ax_imp_induction_axioms)


subsection ‹The predicate ‹AxiomP›, for any Axioms›

definition Extra_ax :: "hf set" where
 "Extra_ax ≡ {⟦«extra_axiom»⟧e0}"

definition Axiom :: "hf set" where
  "Axiom ≡ Extra_ax ∪ Sent ∪ Equality_ax ∪ HF_ax ∪ Special_ax ∪ Induction_ax"

definition AxiomP :: "tm ⇒ fm"
  where "AxiomP x ≡ x EQ «extra_axiom» OR SentP x OR Equality_axP x OR
                    HF_axP x OR Special_axP x OR Induction_axP x"

lemma AxiomP_eqvt [eqvt]: "(p ∙ AxiomP x) = AxiomP (p ∙ x)"
  by (simp add: AxiomP_def)

lemma AxiomP_fresh_iff [simp]: "a ♯ AxiomP x ⟷ a ♯ x"
  by (auto simp: AxiomP_def)

lemma eval_fm_AxiomP [simp]: "eval_fm e (AxiomP x) ⟷ ⟦x⟧e ∈ Axiom"
  unfolding AxiomP_def Axiom_def Extra_ax_def
  by (auto simp del: Equality_axP.simps HF_axP.simps intro: eval_quot_fm_ignore)

lemma AxiomP_sf [iff]: "Sigma_fm (AxiomP t)"
  by (auto simp: AxiomP_def)


subsection ‹The predicate ‹ModPonP›, for the inference rule Modus Ponens›

definition ModPon :: "hf ⇒ hf ⇒ hf ⇒ bool" where
  "ModPon x y z ≡ (y = q_Imp x z)"

definition ModPonP :: "tm ⇒ tm ⇒ tm ⇒ fm"
  where "ModPonP x y z = (y EQ Q_Imp x z)"

lemma ModPonP_eqvt [eqvt]: "(p ∙ ModPonP x y z) = ModPonP (p ∙ x) (p ∙ y) (p ∙ z)"
  by (simp add: ModPonP_def)

lemma ModPonP_fresh_iff [simp]: "a ♯ ModPonP x y z ⟷ a ♯ x ∧ a ♯ y ∧ a ♯ z"
  by (auto simp: ModPonP_def)

lemma eval_fm_ModPonP [simp]: "eval_fm e (ModPonP x y z) ⟷ ModPon ⟦x⟧e ⟦y⟧e ⟦z⟧e"
  by (auto simp: ModPon_def ModPonP_def q_defs)

lemma ModPonP_sf [iff]: "Sigma_fm (ModPonP t u v)"
  by (auto simp: ModPonP_def)

lemma ModPonP_subst [simp]:
  "(ModPonP t u v)(i::=w) = ModPonP (subst i w t) (subst i w u) (subst i w v)"
  by (auto simp: ModPonP_def)


subsection ‹The predicate ‹ExistsP›, for the existential rule›
subsubsection ‹Definition›

(*  "⊢ A IMP B ⟹ atom i ♯ B ⟹  ⊢ (Ex i A) IMP B" *)
definition Exists :: "hf ⇒ hf ⇒ bool" where
 "Exists p q ≡ (∃x x' y v. Form x ∧ VarNonOccForm v y ∧ AbstForm v 0 x x' ∧
                p = q_Imp x y ∧ q = q_Imp (q_Ex x') y)"

nominal_function ExistsP :: "tm ⇒ tm ⇒ fm" where
  "⟦atom x ♯ (p,q,v,y,x'); atom x' ♯ (p,q,v,y);
    atom y ♯ (p,q,v); atom v ♯ (p,q)⟧ ⟹
  ExistsP p q = Ex x (Ex x' (Ex y (Ex v (FormP (Var x) AND
                    VarNonOccFormP (Var v) (Var y) AND
                    AbstFormP (Var v) Zero (Var x) (Var x') AND
                    p EQ Q_Imp (Var x) (Var y) AND
                    q EQ Q_Imp (Q_Ex (Var x')) (Var y)))))"
  by (auto simp: eqvt_def ExistsP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows ExistsP_fresh_iff [simp]: "a ♯ ExistsP p q ⟷ a ♯ p ∧ a ♯ q"    (is ?thesis1)
   and eval_fm_ExistsP [simp]: "eval_fm e (ExistsP p q) ⟷ Exists ⟦p⟧e ⟦q⟧e"  (is ?thesis2)
   and ExistsP_sf [iff]:       "Sigma_fm (ExistsP p q)"   (is ?thesis3)
proof -
  obtain x::name and x'::name and y::name and v::name
    where "atom x ♯ (p,q,v,y,x')"  "atom x' ♯ (p,q,v,y)" "atom y ♯ (p,q,v)"  "atom v ♯ (p,q)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thesis3
    by (auto simp: Exists_def q_defs)
qed

lemma ExistsP_subst [simp]: "(ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)"
proof -
  obtain x::name and x'::name and y::name and v::name
    where "atom x ♯ (j,w,p,q,v,y,x')"   "atom x' ♯ (j,w,p,q,v,y)"
          "atom y ♯ (j,w,p,q,v)"   "atom v ♯ (j,w,p,q)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: ExistsP.simps [of x _ _ x' y v])
qed

subsubsection ‹Correctness›

lemma Exists_imp_exists:
  assumes "Exists p q"
  shows "∃A B i. p = ⟦«A IMP B»⟧e ∧ q = ⟦«(Ex i A) IMP B»⟧e ∧ atom i ♯ B"
proof -
  obtain x ax y v
    where x:    "Form x"
      and noc:  "VarNonOccForm v y"
      and abst: "AbstForm v 0 x ax"
      and p: "p = q_Imp x y"
      and q: "q = q_Imp (q_Ex ax) y"
    using assms  by (auto simp: Exists_def)
  then obtain B::fm where B: "y = ⟦«B»⟧e" and vfresh: "atom (decode_Var v) ♯ B"
   by (metis VarNonOccForm_imp_fresh)
  obtain A::fm where A: "x = ⟦«A»⟧e" 
    by (metis Form_imp_is_fm x)
  with AbstForm_imp_abst_dbfm [OF abst, of e]
  have ax: "ax = ⟦quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))⟧e"
           "p = ⟦«A IMP B»⟧e" using p A B
    by (auto simp: quot_simps quot_fm_def q_defs)
  have "q = ⟦«(Ex (decode_Var v) A) IMP B»⟧e" using q A B ax
    by (auto simp: abst_trans_fm quot_simps q_defs)
  then show ?thesis using vfresh ax
    by blast
qed

lemma Exists_intro: "atom i ♯ B ⟹ Exists (⟦«A IMP B»⟧e) ⟦«(Ex i A) IMP B»⟧e"
  by (simp add: Exists_def quot_simps q_defs)
     (metis AbstForm_trans_fm Form_quot_fm fresh_imp_VarNonOccForm)

text‹Thus, we have precisely captured the codes of the specialisation axioms.›
corollary Exists_iff_exists:
  "Exists p q ⟷ (∃A B i. p = ⟦«A IMP B»⟧e ∧ q = ⟦«(Ex i A) IMP B»⟧e ∧ atom i ♯ B)"
  by (force dest: Exists_imp_exists Exists_intro)


subsection ‹The predicate ‹SubstP›, for the substitution rule›

text‹Although the substitution rule is derivable in the calculus, the derivation is
too complicated to reproduce within the proof function. It is much easier to
provide it as an immediate inference step, justifying its soundness in terms
of other inference rules.›

subsubsection ‹Definition›

text‹This is the inference ‹H ⊢ A ⟹ H ⊢ A (i::=x)››
definition Subst :: "hf ⇒ hf ⇒ bool" where
  "Subst p q ≡ (∃v u. SubstForm v u p q)"

nominal_function SubstP :: "tm ⇒ tm ⇒ fm" where
  "⟦atom u ♯ (p,q,v); atom v ♯ (p,q)⟧ ⟹
   SubstP p q = Ex v (Ex u (SubstFormP (Var v) (Var u) p q))"
  by (auto simp: eqvt_def SubstP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows SubstP_fresh_iff [simp]: "a ♯ SubstP p q ⟷ a ♯ p ∧ a ♯ q"        (is ?thesis1)
   and eval_fm_SubstP [simp]: "eval_fm e (SubstP p q) ⟷ Subst ⟦p⟧e ⟦q⟧e" (is ?thesis2)
   and SubstP_sf [iff]: "Sigma_fm (SubstP p q)"                           (is ?thesis3)
proof -
  obtain u::name and v::name  where "atom u ♯ (p,q,v)" "atom v ♯ (p,q)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thesis3
    by (auto simp: Subst_def q_defs)
qed

lemma SubstP_subst [simp]: "(SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)"
proof -
  obtain u::name and v::name  where "atom u ♯ (j,w,p,q,v)"  "atom v ♯ (j,w,p,q)"
    by (metis obtain_fresh)
  thus ?thesis
    by (simp add: SubstP.simps [of u _ _ v])
qed

subsubsection ‹Correctness›

lemma Subst_imp_subst:
  assumes "Subst p q" "Form p"
  shows "∃A::fm. ∃i t. p = ⟦«A»⟧e ∧ q = ⟦«A(i::=t)»⟧e"
proof -
  obtain v u where subst: "SubstForm v u p q" using assms
    by (auto simp: Subst_def)
  then obtain t::tm where substt: "SubstForm v ⟦«t»⟧e p q"
    by (metis SubstForm_def Term_imp_is_tm)
  with SubstForm_imp_subst_fm [OF substt] assms
  obtain A where "p = ⟦«A»⟧e"  "q = ⟦«A(decode_Var v::=t)»⟧e"
    by auto
  thus ?thesis
    by blast
qed


subsection ‹The predicate ‹PrfP››

(*Prf(s,k,t) ≡ LstSeq(s,k,t) ∧ (∀n∈k)[Sent (s n) ∨ (∃m,l∈n)[ModPon (s m) (s l) (s n)]]*)
definition Prf :: "hf ⇒ hf ⇒ hf ⇒ bool"
  where "Prf s k y ≡ BuildSeq (λx. x ∈ Axiom) (λu v w. ModPon v w u ∨ Exists v u ∨ Subst v u) s k y"

nominal_function PrfP :: "tm ⇒ tm ⇒ tm ⇒ fm"
  where "⟦atom l ♯ (s,sl,m,n,sm,sn); atom sl ♯ (s,m,n,sm,sn);
          atom m ♯ (s,n,sm,sn); atom n ♯ (s,k,sm,sn);
          atom sm ♯ (s,sn); atom sn ♯ (s)⟧ ⟹
    PrfP s k t =
      LstSeqP s k t AND
      All2 n (SUCC k) (Ex sn (HPair (Var n) (Var sn) IN s AND (AxiomP (Var sn) OR
                Ex m (Ex l (Ex sm (Ex sl (Var m IN Var n AND Var l IN Var n AND
                       HPair (Var m) (Var sm) IN s AND HPair (Var l) (Var sl) IN s AND
                       (ModPonP (Var sm) (Var sl) (Var sn) OR
                        ExistsP (Var sm) (Var sn) OR
                        SubstP (Var sm) (Var sn)))))))))"
  by (auto simp: eqvt_def PrfP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
  shows PrfP_fresh_iff [simp]: "a ♯ PrfP s k t ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ t"      (is ?thesis1)
  and eval_fm_PrfP [simp]:     "eval_fm e (PrfP s k t) ⟷ Prf ⟦s⟧e ⟦k⟧e ⟦t⟧e"  (is ?thesis2)
  and PrfP_imp_OrdP [simp]:    "{PrfP s k t} ⊢ OrdP k"         (is ?thord)
  and PrfP_imp_LstSeqP [simp]: "{PrfP s k t} ⊢ LstSeqP s k t"  (is ?thlstseq)
  and PrfP_sf [iff]:           "Sigma_fm (PrfP s k t)"         (is ?thsf)
proof -
  obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
    where atoms: "atom l ♯ (s,sl,m,n,sm,sn)"   "atom sl ♯ (s,m,n,sm,sn)"
        "atom m ♯ (s,n,sm,sn)"   "atom n ♯ (s,k,sm,sn)"
        "atom sm ♯ (s,sn)"   "atom sn ♯ (s)"
    by (metis obtain_fresh)
  thus ?thesis1 ?thord ?thlstseq ?thsf
    by (auto intro: LstSeqP_OrdP)
  show ?thesis2 using atoms
    by simp
       (simp cong: conj_cong add: LstSeq_imp_Ord Prf_def BuildSeq_def Builds_def
             ModPon_def Exists_def HBall_def HBex_def
             Seq_iff_app [OF LstSeq_imp_Seq_succ]
             Ord_trans [of _ _ "succ ⟦k⟧e"])
qed

lemma PrfP_subst [simp]:
     "(PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)"
proof -
  obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
    where "atom l ♯ (t,u,v,j,w,sl,m,n,sm,sn)"   "atom sl ♯ (t,u,v,j,w,m,n,sm,sn)"
          "atom m ♯ (t,u,v,j,w,n,sm,sn)"   "atom n ♯ (t,u,v,j,w,sm,sn)"
          "atom sm ♯ (t,u,v,j,w,sn)"   "atom sn ♯ (t,u,v,j,w)"
    by (metis obtain_fresh)
  thus ?thesis
    by (simp add: PrfP.simps [of l _ sl m n sm sn])
qed


subsection ‹The predicate ‹PfP››

definition Pf :: "hf ⇒ bool"
  where "Pf y ≡ (∃s k. Prf s k y)"

nominal_function PfP :: "tm ⇒ fm"
  where "⟦atom k ♯ (s,y); atom s ♯ y⟧ ⟹
    PfP y = Ex k (Ex s (PrfP (Var s) (Var k) y))"
  by (auto simp: eqvt_def PfP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)

nominal_termination (eqvt)
  by lexicographic_order

lemma
 shows PfP_fresh_iff [simp]: "a ♯ PfP y ⟷ a ♯ y"           (is ?thesis1)
   and eval_fm_PfP [simp]:  "eval_fm e (PfP y) ⟷ Pf ⟦y⟧e"  (is ?thesis2)
   and PfP_sf [iff]: "Sigma_fm (PfP y)"                      (is ?thsf)
proof -
  obtain k::name and s::name where "atom k ♯ (s,y)" "atom s ♯ y"
    by (metis obtain_fresh)
  thus ?thesis1 ?thesis2 ?thsf
    by (auto simp: Pf_def)
qed

lemma PfP_subst [simp]: "(PfP t)(j::=w) = PfP (subst j w t)"
proof -
  obtain k::name and s::name where "atom k ♯ (s,t,j,w)" "atom s ♯ (t,j,w)"
    by (metis obtain_fresh)
  thus ?thesis
    by (auto simp: PfP.simps [of k s])
qed

lemma ground_PfP [simp]: "ground_fm (PfP y) = ground y"
  by (simp add: ground_aux_def ground_fm_aux_def supp_conv_fresh)


section‹Proposition 4.4›

subsection‹Left-to-Right Proof›

lemma extra_axiom_imp_Pf: "Pf ⟦«extra_axiom»⟧e"
proof -
  have "⟦«extra_axiom»⟧e ∈ Extra_ax"
    by (simp add: Extra_ax_def) (rule eval_quot_fm_ignore)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma boolean_axioms_imp_Pf:
  assumes "α ∈ boolean_axioms" shows "Pf ⟦«α»⟧e"
proof -
  have "⟦«α»⟧e ∈ Sent" using assms
    by (rule boolean_axioms.cases)
       (auto simp: Sent_def Sent_axioms_def quot_Disj quot_Neg q_defs)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma equality_axioms_imp_Pf:
  assumes "α ∈ equality_axioms" shows "Pf ⟦«α»⟧e"
proof -
  have "⟦«α»⟧e ∈ Equality_ax" using assms [unfolded equality_axioms_def]
    by (auto simp: Equality_ax_def eval_quot_fm_ignore)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma HF_axioms_imp_Pf:
  assumes "α ∈ HF_axioms" shows "Pf ⟦«α»⟧e"
proof -
  have "⟦«α»⟧e ∈ HF_ax" using assms [unfolded HF_axioms_def]
    by (auto simp: HF_ax_def eval_quot_fm_ignore)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma special_axioms_imp_Pf:
  assumes "α ∈ special_axioms" shows "Pf ⟦«α»⟧e"
proof -
  have "⟦«α»⟧e ∈ Special_ax"
    by (metis special_axioms_into_Special_ax assms)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma induction_axioms_imp_Pf:
  assumes "α ∈ induction_axioms" shows "Pf ⟦«α»⟧e"
proof -
  have "⟦«α»⟧e ∈ Induction_ax"
    by (metis induction_axioms_into_Induction_ax assms)
  thus ?thesis
    by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
qed

lemma ModPon_imp_Pf: "⟦Pf ⟦Q_Imp x y⟧e; Pf ⟦x⟧e⟧ ⟹ Pf ⟦y⟧e"
  by (auto simp: Pf_def Prf_def ModPon_def q_defs intro: BuildSeq_combine)

lemma quot_ModPon_imp_Pf: "⟦Pf ⟦«α IMP β»⟧e; Pf ⟦«α»⟧e⟧ ⟹ Pf ⟦«β»⟧e"
  by (simp add: ModPon_imp_Pf quot_fm_def quot_simps q_defs)

lemma quot_Exists_imp_Pf: "⟦Pf ⟦«α IMP β»⟧e; atom i ♯ β⟧ ⟹ Pf ⟦«Ex i α IMP β»⟧e"
  by (force simp: Pf_def Prf_def Exists_def quot_simps q_defs 
            intro: BuildSeq_combine AbstForm_trans_fm_eq fresh_imp_VarNonOccForm)

lemma proved_imp_Pf: assumes "H ⊢ α" "H={}" shows "Pf ⟦«α»⟧e"
using assms
proof (induct)
  case (Hyp A H) thus ?case
    by auto
next
  case (Extra H) thus ?case
    by (metis extra_axiom_imp_Pf)
next
  case (Bool A H) thus ?case
    by (metis boolean_axioms_imp_Pf)
next
  case (Eq A H) thus ?case
    by (metis equality_axioms_imp_Pf)
next
  case (HF A H) thus ?case
    by (metis HF_axioms_imp_Pf)
next
  case (Spec A H) thus ?case
    by (metis special_axioms_imp_Pf)
next
  case (Ind A H) thus ?case
    by (metis induction_axioms_imp_Pf)
next
  case (MP H A B H') thus ?case
    by (metis quot_ModPon_imp_Pf Un_empty)
next
  case (Exists H A B i) thus ?case
    by (metis quot_Exists_imp_Pf)
qed

corollary proved_imp_proved_PfP: "{} ⊢ α ⟹ {} ⊢ PfP «α»"
  by (rule Sigma_fm_imp_thm [OF PfP_sf]) 
     (auto simp: ground_aux_def supp_conv_fresh proved_imp_Pf)

subsection‹Right-to-Left Proof›

lemma Sent_imp_hfthm:
  assumes "x ∈ Sent" shows "∃A. x = ⟦«A»⟧e ∧ {} ⊢ A"
proof -
  obtain y z w where "Form y" "Form z" "Form w" and axs: "Sent_axioms x y z w"
    using assms  by (auto simp: Sent_def)
  then obtain A::fm and B::fm and C::fm 
         where A: "y = ⟦«A»⟧e" and B: "z = ⟦«B»⟧e" and C: "w = ⟦«C»⟧e"
    by (metis Form_imp_is_fm)
  have "∃A. q_Imp y y = ⟦«A»⟧e ∧ {} ⊢ A"
      by (force simp add: A quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
  moreover have "∃A. q_Imp y (q_Disj y z) = ⟦«A»⟧e ∧ {} ⊢ A"
      by (force intro!: exI [where x="A IMP (A OR B)"]
                simp add: A B quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
  moreover have "∃A. q_Imp (q_Disj y y) y = ⟦«A»⟧e ∧ {} ⊢ A"
      by (force intro!: exI [where x="(A OR A) IMP A"]
                simp add: A quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
  moreover have "∃A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = ⟦«A»⟧e ∧ {} ⊢ A"
      by (force intro!: exI [where x="(A OR (B OR C)) IMP ((A OR B) OR C)"]
                simp add: A B C quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
  moreover have "∃A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = ⟦«A»⟧e ∧ {} ⊢ A"
      by (force intro!: exI [where x="(A OR B) IMP ((Neg A OR C) IMP (B OR C))"]
                simp add: A B C quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
  ultimately show ?thesis using axs [unfolded Sent_axioms_def]
    by blast
qed

lemma Extra_ax_imp_hfthm:
  assumes "x ∈ Extra_ax" obtains A where "x = ⟦«A»⟧e ∧ {} ⊢ A"
  using assms unfolding Extra_ax_def
  by (auto intro: eval_quot_fm_ignore hfthm.Extra)

lemma Equality_ax_imp_hfthm:
  assumes "x ∈ Equality_ax" obtains A where "x = ⟦«A»⟧e ∧ {} ⊢ A"
  using assms unfolding Equality_ax_def
  by (auto intro: eval_quot_fm_ignore hfthm.Eq [unfolded equality_axioms_def])

lemma HF_ax_imp_hfthm:
  assumes "x ∈ HF_ax" obtains A where "x = ⟦«A»⟧e ∧ {} ⊢ A"
  using assms unfolding HF_ax_def
  by (auto intro: eval_quot_fm_ignore hfthm.HF [unfolded HF_axioms_def])

lemma Special_ax_imp_hfthm:
  assumes "x ∈ Special_ax" obtains A where "x = ⟦«A»⟧e" "{} ⊢ A"
  by (metis Spec Special_ax_imp_special_axioms assms)

lemma Induction_ax_imp_hfthm:
  assumes "x ∈ Induction_ax" obtains A where "x = ⟦«A»⟧e" "{} ⊢ A"
  by (metis Induction_ax_imp_induction_axioms assms hfthm.Ind)

lemma Exists_imp_hfthm: "⟦Exists ⟦«A»⟧e y; {} ⊢ A⟧ ⟹ ∃B. y = ⟦«B»⟧e ∧ {} ⊢ B"
  by (drule Exists_imp_exists [where e=e]) (auto intro: anti_deduction)

lemma Subst_imp_hfthm:  "⟦Subst ⟦«A»⟧e y; {} ⊢ A⟧ ⟹ ∃B. y = ⟦«B»⟧e ∧ {} ⊢ B"
  by (drule Subst_imp_subst [where e=e], auto intro: Subst)

lemma eval_Neg_imp_Neg: "⟦«α»⟧e = q_Neg x ⟹ ∃A. α = Neg A ∧ ⟦«A»⟧e = x" 
  by (cases α rule: fm.exhaust) (auto simp: quot_simps q_defs htuple_minus_1)

lemma eval_Disj_imp_Disj: "⟦«α»⟧e = q_Disj x y ⟹ ∃A B. α = A OR B ∧ ⟦«A»⟧e = x ∧ ⟦«B»⟧e = y"
  by (cases α rule: fm.exhaust) (auto simp: quot_simps q_defs htuple_minus_1)

lemma Prf_imp_proved: assumes "Prf s k x" shows "∃A. x = ⟦«A»⟧e ∧ {} ⊢ A"
using assms [unfolded Prf_def Axiom_def]
proof (induction x rule: BuildSeq_induct)
  case (B x) thus ?case
    by (auto intro: Extra_ax_imp_hfthm Sent_imp_hfthm Equality_ax_imp_hfthm HF_ax_imp_hfthm
                    Special_ax_imp_hfthm Induction_ax_imp_hfthm)
next
  case (C x y z)
  then obtain A::fm and B::fm where "y = ⟦«A»⟧e" "{} ⊢ A" "z = ⟦«B»⟧e" "{} ⊢ B"
    by blast
  thus ?case using C.hyps ModPon_def q_Imp_def
    by (auto dest!: MP_same eval_Neg_imp_Neg eval_Disj_imp_Disj Exists_imp_hfthm Subst_imp_hfthm)
qed

corollary Pf_quot_imp_is_proved: "Pf ⟦«α»⟧e ⟹ {} ⊢ α"
  by (metis Pf_def Prf_imp_proved eval_fm_inject)

text‹Proposition 4.4!›
theorem proved_iff_proved_PfP: "{} ⊢ α ⟷ {} ⊢ PfP «α»"
  by (metis Pf_quot_imp_is_proved emptyE eval_fm_PfP hfthm_sound proved_imp_proved_PfP)

end