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
(*>*)