# Theory Pseudo_Term

chapter ‹Pseudo-Terms›

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

text ‹Pseudo-terms are formulas that satisfy the exists-unique property
on one of their variables.›

section ‹Basic Setting›

context Generic_Syntax
begin

text ‹We choose a specific variable, out, that will represent the
"output" of pseudo-terms, i.e., the variable on which the exists-unique property holds:›
abbreviation "out ≡ Variable 0"
text ‹Many facts will involve pseudo-terms with only one additional "input" variable, inp:›
abbreviation "inp ≡ Variable (Suc 0)"

(* These facts can speed up simplification: *)
lemma out_inp_distinct[simp]:
"out ≠ inp" "inp ≠ out"
"out ≠ xx" "out ≠ yy" "yy ≠ out" "out ≠ zz" "zz ≠ out" "out ≠ xx'" "xx' ≠ out"
"out ≠ yy'" "yy' ≠ out" "out ≠ zz'" "zz' ≠ out"
"inp ≠ xx" "inp ≠ yy" "yy ≠ inp" "inp ≠ zz" "zz ≠ inp" "inp ≠ xx'" "xx' ≠ inp"
"inp ≠ yy'" "yy' ≠ inp" "inp ≠ zz'" "zz' ≠ inp"
by auto

end (* context Generic_Syntax *)

context Deduct_with_False_Disj_Rename
begin

text ‹Pseudo-terms over the first $n+1$ variables, i.e.,
having $n$ input variables (Variable $1$ to Variable $n$), and an output variable, out (which is
an abbreviation for Variable $0$).›
definition ptrm :: "nat ⇒ 'fmla set" where
"ptrm n ≡ {σ ∈ fmla . Fvars σ = Variable  {0..n} ∧ prv (exu out σ)}"

lemma ptrm[intro,simp]: "σ ∈ ptrm n ⟹ σ ∈ fmla"
unfolding ptrm_def by auto

lemma ptrm_1_Fvars[simp]: "σ ∈ ptrm (Suc 0) ⟹ Fvars σ = {out,inp}"
unfolding ptrm_def by auto

lemma ptrm_prv_exu: "σ ∈ ptrm n ⟹ prv (exu out σ)"
unfolding ptrm_def by auto

lemma ptrm_prv_exi: "σ ∈ ptrm n ⟹ prv (exi out σ)"
by (simp add: ptrm_prv_exu prv_exu_exi)

lemma nprv_ptrmE_exi:
"σ ∈ ptrm n ⟹ nprv (insert σ F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹
ψ ∈ fmla ⟹ out ∉ Fvars ψ ⟹ out ∉ ⋃ (Fvars  F) ⟹ nprv F ψ"
apply (frule ptrm_prv_exu, drule ptrm)
apply(rule nprv_exuE_exi[of _ out σ])
by (auto intro!: prv_nprvI)

lemma nprv_ptrmE_uni:
"σ ∈ ptrm n ⟹ nprv F (subst σ t1 out) ⟹ nprv F (subst σ t2 out) ⟹
nprv (insert (eql t1 t2) F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ ψ ∈ fmla ⟹ t1 ∈ trm ⟹ t2 ∈ trm
⟹ nprv F ψ"
apply (frule ptrm_prv_exu, drule ptrm)
apply(rule nprv_exuE_uni[of _ out σ t1 t2])
by (auto intro!: prv_nprvI)

lemma nprv_ptrmE_uni0:
"σ ∈ ptrm n ⟹ nprv F σ ⟹ nprv F (subst σ t out) ⟹
nprv (insert (eql (Var out) t) F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ ψ ∈ fmla ⟹ t ∈ trm
⟹ nprv F ψ"
by (rule nprv_ptrmE_uni[of σ _ _ "Var out" t]) auto

lemma nprv_ptrmE0_uni0:
"σ ∈ ptrm n ⟹ σ ∈ F ⟹ nprv F (subst σ t out) ⟹
nprv (insert (eql (Var out) t) F) ψ ⟹
F ⊆ fmla ⟹ finite F ⟹ ψ ∈ fmla ⟹ t ∈ trm
⟹ nprv F ψ"
by (rule nprv_ptrmE_uni0[of σ n _ t]) auto

section ‹The $\forall$-$\exists$ Equivalence›

text ‹There are two natural ways to state that (unique) "output" of a pseudo-term @{term σ}
satisfies a property @{term φ}:
(1) using $\exists$: there exists an "out" such that @{term σ} and @{term φ} hold for it;
(2) using $\forall$: for all "out" such that @{term σ} holds for it, @{term φ} holds for it as well.

We prove the well-known fact that these two ways are equivalent. (Intuitionistic
logic suffice to prove that.)›

lemma ptrm_nprv_exi:
assumes σ: "σ ∈ ptrm n" and [simp]: "φ ∈ fmla"
shows "nprv {σ, exi out (cnj σ φ)} φ"
proof-
have [simp]: "σ ∈ fmla" using σ by simp
define z where "z ≡ getFr [out] [] [σ,φ]"
have z_facts[simp]: "z ∈ var" "z ≠ out" "z ∉ Fvars σ" "z ∉ Fvars φ"
using getFr_FvarsT_Fvars[of "[out]" "[]" "[σ,φ]"] unfolding z_def[symmetric] by auto
have 0: "exi out (cnj σ φ) = exi z (subst (cnj σ φ) (Var z) out)"
by(rule exi_rename, auto)
show ?thesis
unfolding 0
apply(nrule r: nprv_exiE0[of z "subst (cnj σ φ) (Var z) out"])
apply(nrule2 r: nprv_ptrmE0_uni0[OF σ, of _ "Var z"])
subgoal by (nrule r: nprv_cnjE0)
subgoal
apply(nrule r: nprv_clear4_4)
apply(nrule r: nprv_clear3_3)
apply (nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear4_4)
apply(nrule r: nprv_clear3_1)
apply(nrule r: nprv_eql_substE012[of "Var out" "Var z" _ φ out φ]) . .
qed

lemma ptrm_nprv_exi_all:
assumes σ: "σ ∈ ptrm n" and [simp]: "φ ∈ fmla"
shows "nprv {exi out (cnj σ φ)} (all out (imp σ φ))"
proof-
have [simp]: "σ ∈ fmla" using σ by simp
show ?thesis
apply(nrule r: nprv_allI)
apply(nrule r: nprv_impI)
apply(nrule r: ptrm_nprv_exi[OF σ]) .
qed

lemma ptrm_prv_exi_imp_all:
assumes σ: "σ ∈ ptrm n" and [simp]: "φ ∈ fmla"
shows "prv (imp (exi out (cnj σ φ)) (all out (imp σ φ)))"
proof-
have [simp]: "σ ∈ fmla" using σ by simp
show ?thesis
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_impI)
apply(nrule r: ptrm_nprv_exi_all[OF σ]) .
qed

lemma ptrm_nprv_all_imp_exi:
assumes σ: "σ ∈ ptrm n" and [simp]: "φ ∈ fmla"
shows "nprv {all out (imp σ φ)} (exi out (cnj σ φ))"
proof-
have [simp]: "σ ∈ fmla" using σ by simp
define z where "z ≡ getFr [out] [] [σ,φ]"
have z_facts[simp]: "z ∈ var" "z ≠ out" "z ∉ Fvars σ" "z ∉ Fvars φ"
using getFr_FvarsT_Fvars[of "[out]" "[]" "[σ,φ]"] unfolding z_def[symmetric] by auto
show ?thesis
apply(nrule r: nprv_ptrmE_exi[OF σ])
apply(nrule r: nprv_exiI[of _ "cnj σ φ" "Var out" out])
apply(nrule r: nprv_allE0[of out "imp σ φ" _ "Var out"])
apply(nrule r: nprv_clear3_3)
apply(nrule r: nprv_cnjI)
apply(nrule r: nprv_impE01) .
qed

lemma ptrm_prv_all_imp_exi:
assumes σ: "σ ∈ ptrm n" and [simp]: "φ ∈ fmla"
shows "prv (imp (all out (imp σ φ)) (exi out (cnj σ φ)))"
proof-
have [simp]: "σ ∈ fmla" using σ by simp
define z where "z ≡ getFr [out] [] [σ,φ]"
have z_facts[simp]: "z ∈ var" "z ≠ out" "z ∉ Fvars σ" "z ∉ Fvars φ"
using getFr_FvarsT_Fvars[of "[out]" "[]" "[σ,φ]"] unfolding z_def[symmetric] by auto
show ?thesis
apply(nrule r: nprv_prvI)
apply(nrule r: nprv_impI)
apply(nrule r: ptrm_nprv_all_imp_exi[OF σ]) .
qed

end ― ‹context @{locale Deduct_with_False_Disj_Rename }›

section ‹Instantiation›

text ‹We define the notion of instantiating the "inp" variable of a formula
(in particular, of a pseudo-term):
-- first with a term);
-- then with a pseudo-term.
›

subsection ‹Instantiation with terms›

text ‹Instantiation with terms is straightforward using substitution.
In the name of the operator, the suffix "Inp" is a reminder that we instantiate @{term φ}
on its variable "inp".›

context Generic_Syntax
begin

definition instInp :: "'fmla ⇒ 'trm ⇒ 'fmla" where
"instInp φ t ≡ subst φ t inp"

lemma instInp_fmla[simp,intro]:
assumes "φ ∈ fmla" and "t ∈ trm"
shows "instInp φ t ∈ fmla"
using assms instInp_def by auto

lemma Fvars_instInp[simp,intro]:
assumes "φ ∈ fmla" and "t ∈ trm" "Fvars φ = {inp}"
shows "Fvars (instInp φ t) = FvarsT t"
using assms instInp_def by auto

end ― ‹context @{locale Generic_Syntax }›

context Deduct_with_False_Disj_Rename
begin

lemma Fvars_instInp_ptrm_1[simp,intro]:
assumes τ: "τ ∈ ptrm (Suc 0)" and "t ∈ trm"
shows "Fvars (instInp τ t) = insert out (FvarsT t)"
using assms instInp_def by auto

lemma instInp:
assumes τ: "τ ∈ ptrm (Suc 0)" and [simp]: "t ∈ trm"
and [simp]: "FvarsT t = Variable  {(Suc 0)..n}"
shows "instInp τ t ∈ ptrm n"
proof-
note Let_def[simp]
have [simp]: "τ ∈ fmla" "Fvars τ = {out,inp}"
using assms unfolding ptrm_def by auto
have [simp]: "Fvars (instInp τ t) = insert out (FvarsT t)"
using τ by (subst Fvars_instInp_ptrm_1) auto
have 0: "exu out (instInp τ t) = subst (exu out τ) t inp"
unfolding instInp_def by (subst subst_exu) auto
have 1: "prv (exu out τ)" using τ unfolding ptrm_def by auto
have "prv (exu out (instInp τ t))"
unfolding 0 by (rule prv_subst[OF _ _ _ 1], auto)
thus ?thesis using assms unfolding ptrm_def[of n] by auto
qed

lemma instInp_0:
assumes τ: "τ ∈ ptrm (Suc 0)" and "t ∈ trm" and "FvarsT t = {}"
shows "instInp τ t ∈ ptrm 0"
using assms by (intro instInp) auto

lemma instInp_1:
assumes τ: "τ ∈ ptrm (Suc 0)" and "t ∈ trm" and "FvarsT t = {inp}"
shows "instInp τ t ∈ ptrm (Suc 0)"
using assms by (intro instInp) auto

subsection ‹Instantiation with pseudo-terms›

text ‹Instantiation of a formula @{term φ} with a pseudo-term @{term τ} yields a formula that
could be casually written @{term [source] "φ(τ)"}. It states the existence of an output @{term zz} of @{term τ} on which @{term φ} holds.
Instead of @{term [source] "φ(τ)"}, we write @{term "instInpP φ n τ"} where @{term n} is the number of input variables of @{term τ}.
In the name @{term "instInpP"}, @{term "Inp"} is as before a reminder that we instantiate @{term φ} on its variable
"inp" and the suffix "P" stands for "Pseudo".›

definition instInpP :: "'fmla ⇒ nat ⇒ 'fmla ⇒ 'fmla" where
"instInpP φ n τ ≡ let zz = Variable (Suc (Suc n)) in
exi zz (cnj (subst τ (Var zz) out) (subst φ (Var zz) inp))"

lemma instInpP_fmla[simp, intro]:
assumes "φ ∈ fmla" and "τ ∈ fmla"
shows "instInpP φ n τ ∈ fmla"
using assms unfolding instInpP_def by (auto simp: Let_def)

lemma Fvars_instInpP[simp]:
assumes "φ ∈ fmla" and τ: "τ ∈ ptrm n"  "Variable (Suc (Suc n)) ∉ Fvars φ"
shows "Fvars (instInpP φ n τ) = Fvars φ - {inp} ∪ Variable  {(Suc 0)..n}"
using assms unfolding instInpP_def Let_def ptrm_def by auto

lemma Fvars_instInpP2[simp]:
assumes "φ ∈ fmla" and τ: "τ ∈ ptrm n" and "Fvars φ ⊆ {inp}"
shows "Fvars (instInpP φ n τ) = Fvars φ - {inp} ∪ Variable  {(Suc 0)..n}"
using assms by (subst Fvars_instInpP) auto

subsection ‹Closure and compositionality properties of instantiation›

text ‹Instantiating a 1-pseudo-term with an n-pseudo-term yields an n pseudo-term:›
(* This could be generalized, of course. *)
lemma instInpP1[simp,intro]:
assumes σ: "σ ∈ ptrm (Suc 0)" and τ: "τ ∈ ptrm n"
shows "instInpP σ n τ ∈ ptrm n"
proof-
note Let_def[simp]
have [simp]: "σ ∈ fmla" "τ ∈ fmla" "Fvars σ = {out,inp}"
"Fvars τ = Variable  {0..n}"
using assms unfolding ptrm_def by auto
define zz where "zz ≡ Variable (Suc (Suc n))"
have zz_facts[simp]: "zz ∈ var" "⋀i. i ≤ n ⟹ Variable i ≠ zz ∧ zz ≠ Variable i"
"out ≠ zz" "zz ≠ out" "inp ≠ zz" "zz ≠ inp"
unfolding zz_def by auto

define x where "x ≡ getFr [out,inp,zz] [] [σ,τ]"
have x_facts[simp]: "x ∈ var" "x ≠ out" "x ≠ inp"
"x ≠ zz" "zz ≠ x" "x ∉ Fvars σ" "x ∉ Fvars τ"
using getFr_FvarsT_Fvars[of "[out,inp,zz]" "[]" "[σ,τ]"] unfolding x_def[symmetric] by auto
have [simp]: "x ≠ Variable (Suc (Suc n))"
using x_facts(4) zz_def by auto
define z where "z ≡ getFr [out,inp,zz,x] [] [σ,τ]"
have z_facts[simp]: "z ∈ var" "z ≠ out" "z ≠ inp" "z ≠ x" "z ≠ zz" "z ∉ Fvars σ" "z ∉ Fvars τ"
using getFr_FvarsT_Fvars[of "[out,inp,zz,x]" "[]" "[σ,τ]"] unfolding z_def[symmetric] by auto

have [simp]: "⋀i. z = Variable i ⟹ ¬ i ≤ n"
and [simp]: "⋀i. x = Variable i ⟹ ¬ i ≤ n"
using ‹Fvars τ = Variable  {0..n}› atLeastAtMost_iff z_facts(7) x_facts(7)
by blast+

have [simp]: "Fvars (instInpP σ n τ) = Variable  {0..n}"
unfolding instInpP_def by auto
have tt: "exi out τ = exi zz (subst τ (Var zz) out)"
by (rule exi_rename) auto

have exi_σ: "prv (exi out σ)" and exi_τ: "prv (exi zz (subst τ (Var zz) out))"
using σ τ ptrm_prv_exi tt by fastforce+
have exi_σ: "prv (exi out (subst σ (Var zz) inp))"
using prv_subst[OF _ _ _ exi_σ, of inp "Var zz"] by auto

have exu_σ: "prv (exu out σ)"
using σ ptrm_prv_exu by blast
have exu_σ: "prv (exu out (subst σ (Var zz) inp))"
using prv_subst[OF _ _ _ exu_σ, of inp "Var zz"] by auto

have zz_z: "exi zz (cnj (subst τ (Var zz) out) (subst σ (Var zz) inp)) =
exi z (cnj (subst τ (Var z) out) (subst σ (Var z) inp))"
by (variousSubsts2 auto s1: exi_rename[of _ zz z] s2: subst_subst)

have 0: "prv (exu out (instInpP σ n τ))"
apply(nrule r: nprv_prvI)
apply(nrule2 r: nprv_exuI_exi[of _ _ _ x])
subgoal unfolding instInpP_def Let_def
apply(nrule r: nprv_addImpLemmaI[OF prv_exi_commute])
apply(nrule r: nprv_addLemmaE[OF exi_τ])
apply(nrule r: nprv_exiE[of _ zz "subst τ (Var zz) out"])
apply(nrule r: nprv_clear2_2)
apply(nrule r: nprv_exiI[of _ _ "Var zz"])
apply(nrule r: nprv_addLemmaE[OF exi_σ])
apply(nrule r: nprv_exiE[of _ out "subst σ (Var zz) inp"])
apply(nrule r: nprv_clear3_2)
apply(nrule r: nprv_exiI[of _ _ "Var out"])
apply(variousSubsts1 auto s1: subst_subst)
apply(nrule r: nprv_cnjI) .
subgoal
unfolding instInpP_def Let_def zz_def[symmetric]
apply(nrule r: nprv_exiE0[of zz])
apply(nrule r: nprv_clear3_2)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear4_3)
unfolding zz_z
apply(nrule r: nprv_exiE0[of z])
apply(nrule r: nprv_clear4_4)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear5_3)
apply(nrule r: nprv_cut[of _ "eql (Var z) (Var zz)"])
subgoal by (nprover3 r1: nprv_clear4_2 r2: nprv_clear3_3
r3: nprv_ptrmE_uni[OF τ, of _ "Var z" "Var zz"])
subgoal
apply(nrule r: nprv_clear5_2)
apply(nrule r: nprv_clear4_3)
apply(nrule2 r: nprv_eql_substE[of _ "Var zz" "Var z" σ inp])
subgoal by (nrule r: nprv_eql_symE01)
subgoal
apply(nrule r: nprv_clear4_2)
apply(nrule r: nprv_clear3_2)
apply(nrule r: nprv_addLemmaE[OF exu_σ])
apply(nrule r: nprv_exuE_uni[of _ out "subst σ (Var zz) inp" "Var out" "Var x"])
apply(nrule r: nprv_eql_symE01) . . . .
show ?thesis using 0 unfolding ptrm_def instInpP_def Let_def by auto
qed

text ‹Term and pseudo-term instantiation compose smoothly:›
lemma instInp_instInpP:
assumes φ: "φ ∈ fmla" "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm (Suc 0)"
and "t ∈ trm" and "FvarsT t = {}"
shows "instInp (instInpP φ (Suc 0) τ) t = instInpP φ 0 (instInp τ t)"
proof-
define x1 and x2 where
x12: "x1 ≡ Variable (Suc (Suc 0))"
"x2 ≡ Variable (Suc (Suc (Suc 0)))"
have x_facts[simp]: "x1 ∈ var" "x2 ∈ var" "x1 ≠ inp" "x2 ≠ inp"
"x1 ≠ out" "out ≠ x1" "x2 ≠ out" "out ≠ x2" "x1 ≠ x2" "x2 ≠ x1"
unfolding x12 by auto
show ?thesis
using assms unfolding instInp_def instInpP_def Let_def x12[symmetric]

apply(subst subst_exi)
apply(TUF simp)

apply(variousSubsts5 auto
s1: subst_compose_same
s2: subst_compose_diff
s3: exi_rename[of _ x1 x2]
s4: subst_comp
s5: subst_notIn[of φ _ x1]
) .
qed

text ‹Pseudo-term instantiation also composes smoothly with itself:›
lemma nprv_instInpP_compose:
assumes [simp]: "χ ∈ fmla" "Fvars χ = {inp}"
and σ[simp]: "σ ∈ ptrm (Suc 0)" and τ[simp]: "τ ∈ ptrm 0"
shows "nprv {instInpP (instInpP χ (Suc 0) σ) 0 τ}
(instInpP χ 0 (instInpP σ 0 τ))" (is ?A)
and
"nprv {instInpP χ 0 (instInpP σ 0 τ)}
(instInpP (instInpP χ (Suc 0) σ) 0 τ)" (is ?B)
proof-
define χσ and στ where χσ_def: "χσ ≡ instInpP χ (Suc 0) σ" and στ_def: "στ ≡ instInpP σ 0 τ"

have [simp]: "σ ∈ fmla" "Fvars σ = {out,inp}" "τ ∈ fmla" "Fvars τ = {out}"
using σ τ unfolding ptrm_def by auto
have χσ[simp]: "χσ ∈ fmla" "Fvars χσ = {inp}"
unfolding χσ_def by auto
have στ[simp]:  "στ ∈ ptrm 0" "στ ∈ fmla" "Fvars στ = {out}" unfolding στ_def
by auto
define z where "z ≡ Variable (Suc (Suc 0))"
have z_facts[simp]: "z ∈ var"
"out ≠ z ∧ z ≠ out" "inp ≠ z ∧ z ≠ inp" "z ∉ Fvars χ" "z ∉ Fvars σ" "z ∉ Fvars τ"
unfolding z_def by auto
define zz where "zz ≡ Variable (Suc (Suc (Suc 0)))"
have zz_facts[simp]: "zz ∈ var"
"out ≠ zz ∧ zz ≠ out" "inp ≠ zz ∧ zz ≠ inp" "z ≠ zz ∧ zz ≠ z"
"zz ∉ Fvars χ" "zz ∉ Fvars σ" "zz ∉ Fvars τ"
unfolding zz_def z_def by auto
define z' where "z' ≡ getFr [out,inp,z,zz] [] [χ,σ,τ]"
have z'_facts[simp]: "z' ∈ var" "z' ≠ out" "z' ≠ inp" "z' ≠ z" "z ≠ z'" "z' ≠ zz" "zz ≠ z'"
"z' ∉ Fvars χ""z' ∉ Fvars σ" "z' ∉ Fvars τ"
using getFr_FvarsT_Fvars[of "[out,inp,z,zz]" "[]" "[χ,σ,τ]"] unfolding z'_def[symmetric] by auto

have χσ': "instInpP χσ 0 τ = exi z' (cnj (subst τ (Var z') out) (subst χσ (Var z') inp))"
unfolding instInpP_def Let_def z_def[symmetric]
by (auto simp: exi_rename[of _ z z'])
have χσz': "subst χσ (Var z') inp =
exi zz (cnj (subst (subst σ (Var zz) out) (Var z') inp) (subst χ (Var zz) inp))"
unfolding χσ_def instInpP_def Let_def zz_def[symmetric]
by (auto simp: subst_compose_same)
have στzz: "subst στ (Var zz) out =
exi z (cnj (subst τ (Var z) out) (subst (subst σ (Var zz) out) (Var z) inp))"
unfolding στ_def instInpP_def Let_def z_def[symmetric]
by (variousSubsts2 auto s1: subst_compose_same s2: subst_compose_diff)

have "nprv {instInpP χσ 0 τ} (instInpP χ 0 στ)"
unfolding χσ'
apply(nrule r: nprv_exiE0)
apply(nrule r: nprv_clear2_2)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear3_3)
unfolding χσz'
apply(nrule r: nprv_exiE0)
apply(nrule r: nprv_clear3_3)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear4_3)
unfolding instInpP_def Let_def z_def[symmetric]
apply(nrule r: nprv_exiI[of _ _ "Var zz"])
apply(nrule r: nprv_cnjI)
apply(nrule r: nprv_clear3_2)
unfolding στzz
apply(nrule r: nprv_exiI[of _ _ "Var z'"])
apply(nrule r: nprv_cnjI) .
thus ?A unfolding χσ_def στ_def .

have χστ: "instInpP χ 0 στ = exi z' (cnj (subst στ (Var z') out) (subst χ (Var z') inp))"
unfolding instInpP_def Let_def z_def[symmetric]
by (auto simp: exi_rename[of _ z z'])

have στz': "subst στ (Var z') out =
exi z (cnj (subst τ (Var z) out) (subst (subst σ (Var z) inp) (Var z') out))"
unfolding στ_def instInpP_def Let_def z_def[symmetric]
by (auto simp: subst_compose_same)

have χσz: "subst χσ (Var z) inp =
exi zz (cnj (subst (subst σ (Var z) inp) (Var zz) out) (subst χ (Var zz) inp))"
unfolding χσ_def instInpP_def Let_def zz_def[symmetric]
by (variousSubsts2 auto s1: subst_compose_same s2: subst_compose_diff)

have "nprv {instInpP χ 0 στ} (instInpP χσ 0 τ)"
unfolding χστ
apply(nrule r: nprv_exiE0)
apply(nrule r: nprv_clear2_2)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear3_3)
unfolding στz'
apply(nrule r: nprv_exiE0)
apply(nrule r: nprv_clear3_2)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear4_3)
unfolding instInpP_def Let_def z_def[symmetric]
apply(nrule r: nprv_exiI[of _ _ "Var z"])
apply(nrule r: nprv_cnjI)
unfolding χσz
apply(nrule r: nprv_exiI[of _ _ "Var z'"])
apply(nrule r: nprv_cnjI) .
thus ?B unfolding χσ_def στ_def .
qed

lemma prv_instInpP_compose:
assumes [simp]: "χ ∈ fmla" "Fvars χ = {inp}"
and σ[simp]: "σ ∈ ptrm (Suc 0)" and τ[simp]: "τ ∈ ptrm 0"
shows "prv (imp (instInpP (instInpP χ (Suc 0) σ) 0 τ)
(instInpP χ 0 (instInpP σ 0 τ)))" (is ?A)
and
"prv (imp (instInpP χ 0 (instInpP σ 0 τ))
(instInpP (instInpP χ (Suc 0) σ) 0 τ))" (is ?B)
and
"prv (eqv (instInpP (instInpP χ (Suc 0) σ) 0 τ)
(instInpP χ 0 (instInpP σ 0 τ)))" (is ?C)
proof-
have [simp]: "σ ∈ fmla" "Fvars σ = {out,inp}" "τ ∈ fmla" "Fvars τ = {out}"
using σ τ unfolding ptrm_def by auto
show ?A ?B by (intro nprv_prvI nprv_impI nprv_instInpP_compose, auto)+
thus ?C by (intro prv_eqvI) auto
qed

section ‹Equality between Pseudo-Terms and Terms›

text ‹Casually, the equality between a pseudo-term @{term τ} and a term @{term t} can
be written as $\vdash\tau = t$. This is in fact the (provability of)
the instantiation of @{term τ} with @{term t} on @{term τ}'s output variable out. Indeed, this
formula says that the unique entity denoted by @{term τ} is exactly @{term t}.›

definition prveqlPT :: "'fmla ⇒ 'trm ⇒ bool" where
"prveqlPT τ t ≡ prv (subst τ t out)"

text ‹We prove that term--pseudo-term equality indeed acts like an equality,
in that it satisfies the substitutivity principle (shown only in the
particular case of formula-input instantiation).›

lemma prveqlPT_nprv_instInp_instInpP:
assumes[simp]: "φ ∈ fmla" and f: "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm 0"
and [simp]: "t ∈ trm" "FvarsT t = {}"
and τt: "prveqlPT τ t"
shows "nprv {instInpP φ 0 τ} (instInp φ t)"
proof-
have [simp]: "τ ∈ fmla" "Fvars τ = {out}" using τ unfolding ptrm_def by auto
define zz where "zz ≡ Variable (Suc (Suc 0))"
have zz_facts[simp]: "zz ∈ var"
"out ≠ zz ∧ zz ≠ out" "inp ≠ zz ∧ zz ≠ inp" "zz ∉ Fvars τ" "zz ∉ Fvars φ"
unfolding zz_def using f by auto

note lemma1 = nprv_addLemmaE[OF τt[unfolded prveqlPT_def]]

show ?thesis unfolding instInpP_def Let_def zz_def[symmetric] instInp_def
apply(nrule r: lemma1)
apply(nrule r: nprv_exiE0[of zz])
apply(nrule r: nprv_clear3_3)
apply(nrule r: nprv_cnjE0)
apply(nrule r: nprv_clear4_3)
apply(nrule r: nprv_ptrmE_uni[OF τ, of _ t "Var zz"])
apply(nrule r: nprv_clear4_2)
apply(nrule r: nprv_clear3_3)
apply(nrule r: nprv_eql_substE012[of t "Var zz" _ φ inp]) .
qed

lemma prveqlPT_prv_instInp_instInpP:
assumes"φ ∈ fmla" and f: "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm 0"
and "t ∈ trm" "FvarsT t = {}"
and τt: "prveqlPT τ t"
shows "prv (imp (instInpP φ 0 τ) (instInp φ t))"
using assms by (intro nprv_prvI nprv_impI prveqlPT_nprv_instInp_instInpP) auto

lemma prveqlPT_nprv_instInpP_instInp:
assumes[simp]: "φ ∈ fmla" and f: "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm 0"
and [simp]: "t ∈ trm" "FvarsT t = {}"
and τt: "prveqlPT τ t"
shows "nprv {instInp φ t} (instInpP φ 0 τ)"
proof-
have [simp]: "τ ∈ fmla" "Fvars τ = {out}" using τ unfolding ptrm_def by auto
define zz where "zz ≡ Variable (Suc (Suc 0))"
have zz_facts[simp]: "zz ∈ var"
"out ≠ zz ∧ zz ≠ out" "inp ≠ zz ∧ zz ≠ inp" "zz ∉ Fvars τ" "zz ∉ Fvars φ"
unfolding zz_def using f by auto

note lemma1 = nprv_addLemmaE[OF τt[unfolded prveqlPT_def]]

show ?thesis unfolding instInpP_def Let_def zz_def[symmetric] instInp_def
by (nprover3 r1: lemma1 r2: nprv_exiI[of _ _ t] r3: nprv_cnjI)
qed

lemma prveqlPT_prv_instInpP_instInp:
assumes"φ ∈ fmla" and f: "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm 0"
and "t ∈ trm" "FvarsT t = {}"
and τt: "prveqlPT τ t"
shows "prv (imp (instInp φ t) (instInpP φ 0 τ))"
using assms by (intro nprv_prvI nprv_impI prveqlPT_nprv_instInpP_instInp) auto

lemma prveqlPT_prv_instInp_eqv_instInpP:
assumes"φ ∈ fmla" and f: "Fvars φ ⊆ {inp}" and τ: "τ ∈ ptrm 0"
and "t ∈ trm" "FvarsT t = {}"
and τt: "prveqlPT τ t"
shows "prv (eqv (instInpP φ 0 τ) (instInp φ t))"
using assms prveqlPT_prv_instInp_instInpP prveqlPT_prv_instInpP_instInp
by (intro prv_eqvI) auto

end ― ‹context @{locale Deduct_with_False_Disj_Rename}›

(*<*)
end
(*>*)