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)
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
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
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
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
end