Theory Abstract_Representability

chapter ‹Representability Assumptions›

(*<*)
theory Abstract_Representability imports Abstract_Encoding
begin
(*>*)

text ‹Here we make assumptions about various functions or relations being
representable.›


section ‹Representability of Negation›

text ‹The negation function neg is assumed to be representable by a
two-variable formula N.›

locale Repr_Neg =
Deduct2_with_False
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  num
  prv bprv
+
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and num
and prv bprv
and enc (‹⟨_⟩›)
+
fixes N :: 'fmla
assumes
N[simp,intro!]: "N ∈ fmla"
and
Fvars_N[simp]: "Fvars N = {xx,yy}"
and
neg_implies_prv_N:
"⋀ φ.
  let NN = (λ t1 t2. psubst N [(t1,xx), (t2,yy)]) in
   φ ∈ fmla ⟶ Fvars φ = {} ⟶ bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
and
N_unique:
"⋀ φ.
  let NN = (λ t1 t2. psubst N [(t1,xx), (t2,yy)]) in
  φ ∈ fmla ⟶ Fvars φ = {} ⟶
  bprv (all yy (all yy'
    (imp (cnj (NN ⟨φ⟩ (Var yy)) (NN ⟨φ⟩ (Var yy')))
         (eql (Var yy) (Var yy')))))"
begin

text ‹NN is a notation for the predicate that takes terms and returns corresponding instances
of N, obtained by substituting its free variables with these terms. This is very convenient
for reasoning, and will be done for all the representing formulas we will consider.›

definition NN where "NN ≡ λ t1 t2. psubst N [(t1,xx), (t2,yy)]"

lemma NN_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
 NN t1 t2 = subst (subst N t1 xx) t2 yy"
  unfolding NN_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma NN_neg:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
  using neg_implies_prv_N unfolding Let_def NN_def by meson

lemma NN_unique:
  assumes "φ ∈ fmla" "Fvars φ = {}"
  shows "bprv (all yy (all yy'
    (imp (cnj (NN ⟨φ⟩ (Var yy)) (NN ⟨φ⟩ (Var yy')))
         (eql (Var yy) (Var yy')))))"
  using assms N_unique unfolding Let_def NN_def by meson

lemma NN[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ NN t1 t2 ∈ fmla"
unfolding NN_def by auto

lemma Fvars_NN[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (NN t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: NN_def2 subst2_fresh_switch)

(* Here and elsewhere: hard to make into one or two uniform statements,
given that we don't assume sufficiently powerful properties for trm substitution.
So such lists would need to be maintained on an ad hoc basis, keeping adding instances
when needed. *)
lemma [simp]:
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var yy)) n yy = NN m n"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var yy')) n yy = NN m (Var yy')"
"m ∈ num ⟹ subst (NN m (Var yy')) (Var yy) yy' = NN m (Var yy)"
"n ∈ num ⟹ subst (NN (Var xx) (Var yy)) n xx = NN n (Var yy)"
"n ∈ num ⟹ subst (NN (Var xx) (Var xx')) n xx = NN n (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var xx')) n zz = NN m (Var xx')"
"n ∈ num ⟹ subst (NN n (Var yy)) (Var xx') yy = NN n (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (NN m (Var xx')) n xx' = NN m n"
  by (auto simp add: NN_def2 subst2_fresh_switch)

lemma NN_unique2:
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (all yy
     (imp (NN ⟨φ⟩ (Var yy))
          (eql ⟨neg φ⟩ (Var yy))))"
proof-
  have 1: "bprv (NN ⟨φ⟩ ⟨neg φ⟩)"
    using NN_neg[OF assms] .
  have 2: "bprv (all yy' (
             imp (cnj (NN ⟨φ⟩ ⟨neg φ⟩)
                      (NN ⟨φ⟩ (Var yy')))
                 (eql ⟨neg φ⟩ (Var yy'))))"
    using B.prv_allE[of yy, OF _ _ _ NN_unique, of "φ" "⟨neg φ⟩"]
    by fastforce
  have 31: "bprv (all yy' (
             imp (NN ⟨φ⟩ ⟨neg φ⟩)
                 (imp (NN ⟨φ⟩ (Var yy'))
                      (eql ⟨neg φ⟩ (Var yy')))))"
    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
  have 32: "bprv (imp (NN ⟨φ⟩ ⟨neg φ⟩)
                      (all yy' (imp (NN ⟨φ⟩ (Var yy'))
                                    (eql ⟨neg φ⟩ (Var yy')))))"
    by (rule B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: NN_def2)
  have 33: "bprv (all yy' (imp (NN ⟨φ⟩ (Var yy'))
                              (eql ⟨neg φ⟩ (Var yy'))))"
    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
  thus ?thesis using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy] by simp
qed

lemma NN_neg_unique:
assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
shows
"bprv (imp (NN ⟨φ⟩ (Var yy))
           (eql ⟨neg φ⟩ (Var yy)))" (is "bprv ?A")
proof-
  have 0: "bprv (all yy ?A)"
    using NN_unique2[of "φ"] by simp
  show ?thesis by (rule B.allE_id[OF _ _ 0]) auto
qed

lemma NN_exi_cnj:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and χ[simp]: "χ ∈ fmla"
assumes f: "Fvars χ = {yy}"
shows "bprv (eqv (subst χ ⟨neg φ⟩ yy)
                 (exi yy (cnj χ (NN ⟨φ⟩ (Var yy)))))"
(is "bprv (eqv ?A ?B)")
proof(intro B.prv_eqvI)
  have yy: "yy ∈ var" by simp
  let ?N = "NN ⟨φ⟩ (Var yy)"
  have "bprv (imp (subst χ ⟨neg φ⟩ yy) ((subst (cnj χ ?N) ⟨neg φ⟩ yy)))" using NN_neg[OF φ]
    by (simp add: B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv)
  thus "bprv (imp ?A ?B)"
    by (elim B.prv_prv_imp_trans[rotated 3], intro B.prv_exi_inst) auto
next
  have 00: "bprv (imp (eql ⟨neg φ⟩ (Var yy)) (imp χ (subst χ ⟨neg φ⟩ yy)))"
    by (rule B.prv_eql_subst_trm_id_rev) auto
  have 11: "bprv (imp (NN ⟨φ⟩ (Var yy)) (imp χ (subst χ ⟨neg φ⟩ yy)))"
    using 00 NN_neg_unique[OF φ]
    using NN num Var Variable φ χ eql imp subst B.prv_prv_imp_trans
    by (metis (no_types, lifting) enc in_num neg)
  hence "bprv (imp (cnj χ (NN ⟨φ⟩ (Var yy))) (subst χ ⟨neg φ⟩ yy))"
    by (simp add: 11 B.prv_cnj_imp_monoR2 B.prv_imp_com)
  hence 1: "bprv (all yy (imp (cnj χ (NN ⟨φ⟩ (Var yy))) (subst χ ⟨neg φ⟩ yy)))"
    by (simp add: B.prv_all_gen)
  have 2: "Fvars (subst χ ⟨neg φ⟩ yy) = {}" using f by simp
  show "bprv (imp ?B ?A)" using 1 2
    by (simp add: B.prv_exi_imp)
qed auto

end ― ‹context @{locale Repr_Neg}›


section ‹Representability of Self-Substitution›

text ‹Self-substitution is the function that takes a formula @{term φ}
and returns $\phi[\langle\phi\rangle/\mathit{xx}]$ (for the fixed variable @{term xx}). This is all that
will be needed for the diagonalization lemma.›

locale Repr_SelfSubst =
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
+
Deduct2
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc (‹⟨_⟩›)
+
fixes S :: 'fmla
assumes
S[simp,intro!]: "S ∈ fmla"
and
Fvars_S[simp]: "Fvars S = {xx,yy}"
and
subst_implies_prv_S:
"⋀ φ.
  let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
  φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
  bprv (SS ⟨φ⟩ ⟨subst φ ⟨φ⟩ xx⟩)"
and
S_unique:
"⋀ φ.
  let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
  φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
  bprv (all yy (all yy'
     (imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
          (eql (Var yy) (Var yy')))))"
begin

text ‹SS is the instantiation combinator of S:›
definition SS where "SS ≡ λ t1 t2. psubst S [(t1,xx), (t2,yy)]"

lemma SS_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
 yy ∉ FvarsT t1 ⟹
 SS t1 t2 = subst (subst S t1 xx) t2 yy"
  unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma subst_implies_prv_SS:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ bprv (SS ⟨φ⟩ ⟨subst φ ⟨φ⟩ xx⟩)"
using subst_implies_prv_S unfolding Let_def SS_def by meson

lemma SS_unique:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹
 bprv (all yy (all yy'
      (imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
           (eql (Var yy) (Var yy')))))"
using S_unique unfolding Let_def SS_def by meson

lemma SS[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ SS t1 t2 ∈ fmla"
unfolding SS_def by auto

lemma Fvars_SS[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (SS t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: SS_def2 subst2_fresh_switch)

lemma [simp]:
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy)) p yy = SS m p"
"m ∈ num ⟹ subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy' = SS m p"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy = SS m (Var yy')"
"m ∈ num ⟹ subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
by (auto simp add: SS_def2 subst_comp_num Let_def)

end ― ‹context @{locale Repr_SelfSubst}›


section ‹Representability of Self-Soft-Substitution›

text ‹The soft substitution function performs substitution logically instead of
syntactically. In particular, its "self" version sends @{term φ} to
@{term "exi xx (cnj (eql (Var xx) (enc φ)) φ)"}. Representability of self-soft-substitution will be
an alternative assumption in the diagonalization lemma.›

locale Repr_SelfSoftSubst =
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
+
Deduct2
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc (‹⟨_⟩›)
+
fixes S :: 'fmla
assumes
S[simp,intro!]: "S ∈ fmla"
and
Fvars_S[simp]: "Fvars S = {xx,yy}"
and
softSubst_implies_prv_S:
"⋀ φ.
  let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
  φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
  bprv (SS ⟨φ⟩ ⟨softSubst φ ⟨φ⟩ xx⟩)"
and
S_unique:
"⋀ φ.
  let SS = (λ t1 t2. psubst S [(t1,xx), (t2,yy)]) in
  φ ∈ fmla ⟶ Fvars φ = {xx} ⟶
  bprv (all yy (all yy'
     (imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
          (eql (Var yy) (Var yy')))))"
begin

text ‹SS is the instantiation combinator of S:›
definition SS where "SS ≡ λ t1 t2. psubst S [(t1,xx), (t2,yy)]"

lemma SS_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹
 yy ∉ FvarsT t1 ⟹
 SS t1 t2 = subst (subst S t1 xx) t2 yy"
  unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma softSubst_implies_prv_SS:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹ bprv (SS ⟨φ⟩ ⟨softSubst φ ⟨φ⟩ xx⟩)"
using softSubst_implies_prv_S unfolding Let_def SS_def by meson

lemma SS_unique:
"φ ∈ fmla ⟹ Fvars φ = {xx} ⟹
 bprv (all yy (all yy'
     (imp (cnj (SS ⟨φ⟩ (Var yy)) (SS ⟨φ⟩ (Var yy')))
          (eql (Var yy) (Var yy')))))"
using S_unique unfolding Let_def SS_def by meson

lemma SS[simp,intro]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ SS t1 t2 ∈ fmla"
unfolding SS_def by auto

lemma Fvars_SS[simp]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ yy ∉ FvarsT t1 ⟹
Fvars (SS t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: SS_def2 subst2_fresh_switch)

lemma [simp]:
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy)) p yy = SS m p"
"m ∈ num ⟹ subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy' = SS m p"
"m ∈ num ⟹ p ∈ num ⟹ subst (SS m (Var yy')) p yy = SS m (Var yy')"
"m ∈ num ⟹ subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
by (auto simp add: SS_def2 subst_comp_num Let_def)

end ― ‹context @{locale Repr_SelfSoftSubst}›


section ‹Clean Representability of the "Proof-of" Relation›


text‹For the proof-of relation, we must assume a stronger version of
representability, namely clean representability on the first argument, which
is dedicated to encoding the proof component. The property asks that the
representation predicate is provably false on numerals that do not encode
proofs; it would hold trivially for surjective proof encodings.

Cleanness is not a standard concept in the literature -- we have
introduced it in our CADE 2019 paper~\<^cite>‹"DBLP:conf/cade/0001T19"›.›

locale CleanRepr_Proofs =
Encode_Proofs
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
  enc
  fls
  dsj
  "proof" prfOf
  encPf
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc (‹⟨_⟩›)
and fls dsj
and "proof" :: "'proof set" and prfOf
and encPf
+
fixes Pf :: 'fmla
assumes
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
prfOf_Pf:
"⋀ prf φ.
  let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
  (prf ∈ proof ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶
   prfOf prf φ
   ⟶
   bprv (PPf (encPf prf) ⟨φ⟩))"
and
not_prfOf_Pf:
"⋀ prf φ.
  let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
  (prf ∈ proof ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶
   ¬ prfOf prf φ
   ⟶
   bprv (neg (PPf (encPf prf) ⟨φ⟩)))"
and
Clean_Pf_encPf:
"⋀ p φ. let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
  p ∈ num ∧ φ ∈ fmla ∧ Fvars φ = {} ⟶ p ∉ encPf ` proof ⟶ bprv (neg (PPf p ⟨φ⟩))"
begin

text ‹PPf is the instantiation combinator of Pf:›
definition PPf where "PPf ≡ λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]"

lemma prfOf_PPf:
assumes "prf ∈ proof" "φ ∈ fmla" "Fvars φ = {}" "prfOf prf φ"
shows "bprv (PPf (encPf prf) ⟨φ⟩)"
  using assms prfOf_Pf unfolding PPf_def by auto

lemma not_prfOf_PPf:
assumes "prf ∈ proof" "φ ∈ fmla" "Fvars φ = {}" "¬ prfOf prf φ"
shows "bprv (neg (PPf (encPf prf) ⟨φ⟩))"
  using assms not_prfOf_Pf unfolding PPf_def by auto

lemma Clean_PPf_encPf:
  assumes "φ ∈ fmla" "Fvars φ = {}" and "p ∈ num" "p ∉ encPf ` proof"
  shows "bprv (neg (PPf p ⟨φ⟩))"
using assms Clean_Pf_encPf unfolding PPf_def by auto

lemma PPf[simp,intro!]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ PPf t1 t2 ∈ fmla"
  unfolding PPf_def by auto

lemma PPf_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
  PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
  unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma Fvars_PPf[simp]:
"t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
 Fvars (PPf t1 t2) = FvarsT t1 ∪ FvarsT t2"
by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma [simp]:
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var yy) m) n yy = PPf n m"
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx)) n xx = PPf m n"
"m ∈ num ⟹ subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx')) n xx' = PPf m n"
"n ∈ num ⟹ subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var zz) n) m zz = PPf m n"
by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma B_consistent_prfOf_iff_PPf:
"B.consistent ⟹ prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟶ prfOf prf φ ⟷ bprv (PPf (encPf prf) ⟨φ⟩)"
  unfolding B.consistent_def3 using not_prfOf_PPf[of "prf" φ] prfOf_PPf[of "prf" φ] by force

lemma consistent_prfOf_iff_PPf:
"consistent ⟹ prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟶ prfOf prf φ ⟷ bprv (PPf (encPf prf) ⟨φ⟩)"
  using B_consistent_prfOf_iff_PPf[OF dwf_dwfd.consistent_B_consistent] .

end ― ‹context @{locale CleanRepr_Proofs}›

(*<*)
end
(*>*)