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