Theory Encodings

section‹End Results in Locale-Free Form›
theory Encodings
imports G T E
begin

text‹This section contains the outcome of our type-encoding results,
presented in a locale-free fashion. It is not very useful
from an Isabelle development point of view, where the locale theorems are fine.

Rather, this is aimed as a quasi-self-contained formal documentation of
the overall results for the non-Isabelle-experts.›


subsection ‹Soundness›

text‹In the soundness theorems below, we employ the following Isabelle types:
\\- type variables (parameters):
\\--- ‹'tp›, of types
\\--- ‹'fsym›, of function symbols
\\--- ‹'psym›, of predicate symbols
%
\\- a fixed countable universe ‹univ› for the carrier of the models
%
\\
and various operators on these types:

(1) the constitutive parts of FOL signatures:
\\---- the boolean predicates
‹wtFsym› and ‹wtPsym›, indicating the ``well-typed'' function and predicate
symbols; these are just means to select only subsets of these symbols
for consideration in the signature
\\---- the operators arOf and resOf, giving the arity and the result type
of function symbols
\\---- the operator parOf, giving the arity of predicate symbols

(2) the problem, ‹Φ›, which is a set of clauses over the considered signature

(3) a partition of the types in:
\\--- ‹tpD›, the types that should be decorated in any case
\\--- ‹tpFD›, the types that should be decorated in a featherweight fashion
\\--- for guards only, a further refinement of ‹tpD›, indicating, as ‹tpCD›,
the types that should be classically (i.e., traditionally) decorated
(these partitionings are meant to provide a uniform treatment of the
three styles of encodings:
traditional, lightweight and featherweight)

(4) the constitutive parts of a structure over the considered signature:
\\---- ‹intT›, the interpretation of each type as a unary predicate (essentially, a set)
over an arbitrary type 'univ
\\---- ‹intF› and ‹intP›, the interpretations of the function and predicate symbols
as actual functions and predicates over ‹univ›.


›


text‹\ \\ \bf Soundness of the tag encodings: \ \\›

text‹The assumptions of the tag soundness theorems are the following:

(a)  ‹ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD›,
stating that:
\\--- ‹(wtFsym, wtPsym, arOf, resOf, parOf)› form a countable signature
\\--- ‹Φ› is a well-typed problem over this signature
\\--- ‹infTp› is an indication of the types that the problem guarantees as infinite
in all models
\\--- ‹tpD› and ‹tpFD› are disjoint and all types that are not
 marked as ‹tpD› or ‹tpFD›
are deemed safe by the monotonicity calculus from ‹Mcalc›

(b) ‹CM.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP›
says that ‹(intT, intF, intP)› is a model for ‹Φ› (hence ‹Φ› is satisfiable)

The conclusion says that we obtain a model of the untyped version of the problem
(after suitable tags and axioms have been added):›


text‹Because of the assumptions on tpD and tpFD, we have the following particular cases
of our parameterized tag encoding:
\\-- if ‹tpD› is taked to be everywhere true (hence ‹tpFD› becomes everywhere false), we
obtain the traditional tag encoding
\\-- if ‹tpD› is taken to be true precisely when the monotonicity calculus fails,
we obtain the lightweight tag encoding
\\-- if ‹tpFD› is taken to be true precisely when the monotonicity calculus fails,
we obtain the featherweight tag encoding
›

theorem tags_soundness:
fixes wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list" and resOf :: "'fsym ⇒ 'tp" and parOf :: "'psym ⇒ 'tp list"
and Φ :: "('fsym, 'psym) prob" and infTp :: "'tp ⇒ bool"
and tpD :: "'tp ⇒ bool" and tpFD :: "'tp ⇒ bool"
and intT :: "'tp ⇒ univ ⇒ bool"
and intF :: "'fsym ⇒ univ list ⇒ univ" and intP :: "'psym ⇒ univ list ⇒ bool"
― ‹The problem translation:›
― ‹First the addition of tags (``TE'' stands for ``tag encoding''):›
defines "TE_wtFsym ≡ ProblemIkTpart.TE_wtFsym wtFsym resOf"
and "TE_arOf ≡ ProblemIkTpart.TE_arOf arOf"
and "TE_resOf ≡ ProblemIkTpart.TE_resOf resOf"
defines "TE_Φ ≡ ProblemIkTpart.tPB wtFsym arOf resOf Φ tpD tpFD"
― ‹Then the deletion of types (``U'' stands for ``untyped''):›
and "U_arOf ≡ length ∘ TE_arOf"
and "U_parOf ≡ length ∘ parOf"
defines "U_Φ ≡ TE_Φ"
― ‹The forward model translation:›
― ‹First, using monotonicity, we build an infinite model of @{text"Φ"}
  (``I'' stands for ``infinite''):›
defines "intTI ≡ MonotProblem.intTI TE_wtFsym wtPsym TE_arOf TE_resOf parOf TE_Φ"
and "intFI ≡ MonotProblem.intFI TE_wtFsym wtPsym TE_arOf TE_resOf parOf TE_Φ"
and "intPI ≡ MonotProblem.intPI TE_wtFsym wtPsym TE_arOf TE_resOf parOf TE_Φ"
― ‹Then, by isomorphic transfer of the lattter model, we build a model of @{text"Φ"}
 that has all types interpeted as @{text "univ"} (``F'' stands for ``full"):›
defines "intFF ≡ InfModel.intFF TE_arOf TE_resOf intTI intFI"
and "intPF ≡ InfModel.intPF parOf intTI intPI"
― ‹Then we build a model of @{text "U_Φ"}:›
defines "U_intT ≡ InfModel.intTF (any::'tp)"

― ‹Assumptions of the theorem:›
assumes
P: "ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD"
and M: "CM.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"

― ‹Conclusion of the theorem:›
shows "CU.Model TE_wtFsym wtPsym U_arOf U_parOf U_Φ U_intT intFF intPF"

unfolding U_arOf_def U_parOf_def U_Φ_def
unfolding U_intT_def intTI_def intFI_def intPI_def intFF_def intPF_def
apply(rule M_MonotModel.M_U_soundness)
unfolding M_MonotModel_def MonotModel_def apply safe
  unfolding TE_wtFsym_def TE_arOf_def TE_resOf_def TE_Φ_def
  apply(rule ProblemIkTpart.T_monotonic)
   apply(rule P)
   apply(rule ModelIkTpart.T_soundness) unfolding ModelIkTpart_def apply safe
     apply(rule P)
     apply(rule M)
done


text‹\ \\ \bf Soundness of the guard encodings: \ \\›

text‹Here the assumptions and conclusion have a similar shapes as those
for the tag encodings. The difference is in the first assumption,
‹ProblemIkTpartG wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD tpCD›,
which consists of ‹ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD› together
with the following assumptions about ‹tpCD›:
\\-- ‹tpCD› is included in ‹tpD›
\\-- if a result type of an operation symbol is in ‹tpD›, then so are all the types in its arity
›

text‹We have the following particular cases of our parameterized guard encoding:
\\-- if ‹tpD› and ‹tpCD› are taked to be everywhere true
(hence ‹tpFD› becomes everywhere false),
we obtain the traditional guard encoding
\\-- if ‹tpCD› is taken to be false and ‹tpD› is taken to be true precisely when the
monotonicity calculus fails,
we obtain the lightweight tag encoding
\\-- if ‹tpFD› is taken to be true precisely when the monotonicity calculus fails,
we obtain the featherweight tag encoding
›

theorem guards_soundness:
fixes wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list" and resOf :: "'fsym ⇒ 'tp" and parOf :: "'psym ⇒ 'tp list"
and Φ :: "('fsym, 'psym) prob" and infTp :: "'tp ⇒ bool"
and tpD :: "'tp ⇒ bool" and tpFD :: "'tp ⇒ bool" and tpCD :: "'tp ⇒ bool"
and intT :: "'tp ⇒ univ ⇒ bool"
and intF :: "'fsym ⇒ univ list ⇒ univ"
and intP :: "'psym ⇒ univ list ⇒ bool"
― ‹The problem translation:›
defines "GE_wtFsym ≡ ProblemIkTpartG.GE_wtFsym wtFsym resOf tpCD"
and "GE_wtPsym ≡ ProblemIkTpartG.GE_wtPsym wtPsym tpD tpFD"
and "GE_arOf ≡ ProblemIkTpartG.GE_arOf arOf"
and "GE_resOf ≡ ProblemIkTpartG.GE_resOf resOf"
and "GE_parOf ≡ ProblemIkTpartG.GE_parOf parOf"

defines "GE_Φ ≡ ProblemIkTpartG.gPB wtFsym arOf resOf Φ tpD tpFD tpCD"
and "U_arOf ≡ length ∘ GE_arOf"
and "U_parOf ≡ length ∘ GE_parOf"

defines "U_Φ ≡ GE_Φ"

― ‹The model forward translation:›
defines "intTI ≡ MonotProblem.intTI GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf GE_Φ"
and "intFI ≡ MonotProblem.intFI GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf GE_Φ"
and "intPI ≡ MonotProblem.intPI GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf GE_Φ"

defines "intFF ≡ InfModel.intFF GE_arOf GE_resOf intTI intFI"
and "intPF ≡ InfModel.intPF GE_parOf intTI intPI"

defines "U_intT ≡ InfModel.intTF (any::'tp)"

assumes
P: "ProblemIkTpartG wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD tpCD"
and M: "CM.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"

shows "CU.Model GE_wtFsym GE_wtPsym U_arOf U_parOf U_Φ U_intT intFF intPF"

unfolding U_arOf_def U_parOf_def U_Φ_def
unfolding U_intT_def intTI_def intFI_def intPI_def intFF_def intPF_def
apply(rule M_MonotModel.M_U_soundness)
unfolding M_MonotModel_def MonotModel_def apply safe
  unfolding GE_wtFsym_def GE_wtPsym_def GE_arOf_def GE_resOf_def GE_parOf_def GE_Φ_def
  apply(rule ProblemIkTpartG.G_monotonic)
   apply(rule P)
   apply(rule ModelIkTpartG.G_soundness)
   unfolding ModelIkTpartG_def ModelIkTpart_def apply safe
     apply(rule P)
     using P unfolding ProblemIkTpartG_def apply fastforce
     apply(rule M)
done


subsection ‹Completeness›

text‹The setting is similar to the one for completeness, except for the following point:

(3) The constitutive parts of a structure over the untyped signature
resulted from the addition of the tags or guards followed by
the deletion of the types: ‹(D, eintF, eintP)›
›


text‹\ \\ \bf Completeness of the tag encodings \ \\›


theorem tags_completeness:
fixes wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list" and resOf :: "'fsym ⇒ 'tp" and parOf :: "'psym ⇒ 'tp list"
and Φ :: "('fsym, 'psym) prob" and infTp :: "'tp ⇒ bool"
and tpD :: "'tp ⇒ bool" and tpFD :: "'tp ⇒ bool"

and D :: "univ ⇒ bool"
and eintF :: "('fsym,'tp) T.efsym ⇒ univ list ⇒ univ"
and eintP :: "'psym ⇒ univ list ⇒ bool"

― ‹The problem translation (the same as in the case of soundness):›
defines "TE_wtFsym ≡ ProblemIkTpart.TE_wtFsym wtFsym resOf"
and "TE_arOf ≡ ProblemIkTpart.TE_arOf arOf"
and "TE_resOf ≡ ProblemIkTpart.TE_resOf resOf"
defines "TE_Φ ≡ ProblemIkTpart.tPB wtFsym arOf resOf Φ tpD tpFD"
and "U_arOf ≡ length ∘ TE_arOf"
and "U_parOf ≡ length ∘ parOf"
defines "U_Φ ≡ TE_Φ"

― ‹The backward model translation:›
defines "intT ≡ ProblemIkTpart_TEModel.intT tpD tpFD (λσ::'tp. D) eintF"
and "intF ≡ ProblemIkTpart_TEModel.intF arOf resOf tpD tpFD (λσ::'tp. D) eintF"
and "intP ≡ ProblemIkTpart_TEModel.intP parOf tpD tpFD (λσ::'tp. D) eintF eintP"

assumes
P: "ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD" and
M: "CU.Model TE_wtFsym wtPsym (length o TE_arOf)
            (length o parOf) TE_Φ D eintF eintP"

shows "CM.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"
proof-
  have UM: "UM_Model TE_wtFsym wtPsym TE_arOf TE_resOf parOf TE_Φ D eintF eintP"
  unfolding UM_Model_def UM_Struct_def
  using M unfolding CU.Model_def CU.Struct_def U.Model_def
  using ProblemIkTpart.T_monotonic[OF P,
  unfolded TE_wtFsym_def[symmetric] TE_arOf_def[symmetric]
           TE_resOf_def[symmetric] TE_Φ_def[symmetric]]
  by (auto simp: MonotProblem_def M_Problem_def M_Signature_def M.Problem_def)
  show ?thesis
  unfolding intT_def intF_def intP_def
  apply(rule ProblemIkTpart_TEModel.T_completeness)
  unfolding ProblemIkTpart_TEModel_def apply safe
  apply(rule P)
  apply(rule UM_Model.M_U_completeness)
  apply(rule UM[unfolded TE_wtFsym_def TE_arOf_def TE_resOf_def TE_Φ_def])
  done
qed

text‹\ \\ \bf Completeness of the guard encodings \ \\›

theorem guards_completeness:
fixes wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list" and resOf :: "'fsym ⇒ 'tp" and parOf :: "'psym ⇒ 'tp list"
and Φ :: "('fsym, 'psym) prob" and infTp :: "'tp ⇒ bool"
and tpD :: "'tp ⇒ bool" and tpFD :: "'tp ⇒ bool" and tpCD :: "'tp ⇒ bool"

and D :: "univ ⇒ bool"
and eintF :: "('fsym,'tp) G.efsym ⇒ univ list ⇒ univ"
and eintP :: "('psym,'tp) G.epsym ⇒ univ list ⇒ bool"

― ‹The problem translation (the same as in the case of soundness):›
defines "GE_wtFsym ≡ ProblemIkTpartG.GE_wtFsym wtFsym resOf tpCD"
and "GE_wtPsym ≡ ProblemIkTpartG.GE_wtPsym wtPsym tpD tpFD"
and "GE_arOf ≡ ProblemIkTpartG.GE_arOf arOf"
and "GE_resOf ≡ ProblemIkTpartG.GE_resOf resOf"
and "GE_parOf ≡ ProblemIkTpartG.GE_parOf parOf"
defines "GE_Φ ≡ ProblemIkTpartG.gPB wtFsym arOf resOf Φ tpD tpFD tpCD"
and "U_arOf ≡ length ∘ GE_arOf"
and "U_parOf ≡ length ∘ GE_parOf"
defines "U_Φ ≡ GE_Φ"

― ‹The backward model translation:›
defines "intT ≡ ProblemIkTpartG_GEModel.intT tpD tpFD (λσ::'tp. D) eintP"
and "intF ≡ ProblemIkTpartG_GEModel.intF eintF"
and "intP ≡ ProblemIkTpartG_GEModel.intP eintP"

assumes
P: "ProblemIkTpartG wtFsym wtPsym arOf resOf parOf Φ infTp tpD tpFD tpCD" and
M: "CU.Model GE_wtFsym GE_wtPsym (length o GE_arOf)
            (length o GE_parOf) GE_Φ D eintF eintP"

shows "CM.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"
proof-
  have UM: "UM_Model GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf GE_Φ D eintF eintP"
  unfolding UM_Model_def UM_Struct_def
  using M unfolding CU.Model_def CU.Struct_def U.Model_def
  using ProblemIkTpartG.G_monotonic[OF P,
  unfolded GE_wtFsym_def[symmetric] GE_arOf_def[symmetric]
           GE_wtPsym_def[symmetric] GE_parOf_def[symmetric]
           GE_resOf_def[symmetric] GE_Φ_def[symmetric]]
  by (auto simp: MonotProblem_def M_Problem_def M_Signature_def M.Problem_def)
  show ?thesis
  unfolding intT_def intF_def intP_def
  apply(rule ProblemIkTpartG_GEModel.G_completeness)
  unfolding ProblemIkTpartG_GEModel_def apply safe
  apply(rule P)
  apply(rule UM_Model.M_U_completeness)
  apply(rule UM[unfolded GE_wtFsym_def GE_wtPsym_def GE_parOf_def
             GE_arOf_def GE_resOf_def GE_Φ_def])
  done
qed

end