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

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)"
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
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)"

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)"

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

```