Theory 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›

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 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 ?thsf
    by auto
qed

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

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

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

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

termination
  by lexicographic_order

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


subsection ‹The specialisation axioms›

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 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 ?thesis3
    by auto
qed

subsection ‹The induction axioms›

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 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
qed

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

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_I:
  "{} ⊢ AxiomP «extra_axiom»"
  "{} ⊢ SentP x ⟹ {} ⊢ AxiomP x"
  "{} ⊢ Equality_axP x ⟹ {} ⊢ AxiomP x"
  "{} ⊢ HF_axP x ⟹ {} ⊢ AxiomP x"
  "{} ⊢ Special_axP x ⟹ {} ⊢ AxiomP x"
  "{} ⊢ Induction_axP x ⟹ {} ⊢ AxiomP x"
  unfolding AxiomP_def
  by (rule Disj_I1, rule Refl,
      rule Disj_I2, rule Disj_I1, assumption,
      rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
      rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
      rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I1, assumption,
      rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, rule Disj_I2, assumption)

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 AxiomP_sf [iff]: "Sigma_fm (AxiomP t)"
  by (auto simp: AxiomP_def)


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

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 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" *)
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 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 ?thesis3
    by auto
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

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›

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 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 ?thesis3
    by auto
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


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)]]*)
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 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)
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››

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 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 ?thsf
    by auto
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)

end