Theory Abstract_Encoding

chapter ‹Abstract Encoding›

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

text ‹Here we simply fix some unspecified encoding functions: encoding formulas
and proofs as numerals.›

locale Encode =
Syntax_with_Numerals
  var trm fmla Var FvarsT substT Fvars subst
  num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes enc :: "'fmla ⇒ 'trm" ("⟨_⟩")
assumes
enc[simp,intro!]: "⋀ φ. φ ∈ fmla ⟹ enc φ ∈ num"
begin

end ― ‹context @{locale Encode}›

text ‹Explicit proofs (encoded as numbers), needed only for the harder half of
Goedel's first, and for both half's of Rosser's version; not needed in Goedel's
second.›

locale Encode_Proofs =
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
+
Deduct2_with_Proofs
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv bprv
  "proof" prfOf
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
+
fixes encPf :: "'proof ⇒ 'trm"
assumes
encPf[simp,intro!]: "⋀ pf. pf ∈ proof ⟹ encPf pf ∈ num"


(*<*)
end
(*>*)