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