Theory E

section ‹The type-erasure translation from many-typed to untyped FOL›
theory E imports Mono CU
begin

(* This is the only development that uses UFOL *)


subsection‹Preliminaries›


(* Problem:
sublocale M.Signature < U.Signature
where arOf = "length o arOf" and parOf = "length o parOf"
yields error:
*** Duplicate constant declaration "local.wt_graph" vs. "local.wt_graph"
*)


(* Temporary solution: Isomorphic copy of the MFOL hierarchy: *)
locale M_Signature = M? : Sig.Signature
locale M_Problem = M? : M.Problem
locale M_MonotModel = M? : MonotModel wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and intT and intF and intP and Φ
locale M_FullStruct = M? : FullStruct
locale M_FullModel = M? : FullModel

sublocale M_FullStruct < M_Signature ..
sublocale M_Problem < M_Signature ..
sublocale M_FullModel < M_FullStruct ..
sublocale M_MonotModel < M_FullStruct where
intT = intTF and intF = intFF and intP = intPF ..
sublocale M_MonotModel < M_FullModel where
intT = intTF and intF = intFF and intP = intPF ..


context Sig.Signature begin

end (* context Signature.Signature *)


subsection‹The translation›

sublocale M_Signature < U.Signature
where arOf = "length o arOf" and parOf = "length o parOf"
by standard (auto simp: countable_wtFsym countable_wtPsym)


(* In our implicitly-typed setting, ``e" is just the identity. *)

context M_Signature begin

(* Well-typedness of the translation: *)
lemma wt[simp]: "M.wt T ⟹ wt T"
by (induct T, auto simp add: list_all_iff)

lemma wtA[simp]: "M.wtA at ⟹ wtA at"
apply(cases at) by (auto simp add: list_all_iff)

lemma wtL[simp]: "M.wtL l ⟹ wtL l"
apply(cases l) by auto

lemma wtC[simp]: "M.wtC c ⟹ wtC c"
unfolding M.wtC_def wtC_def by (induct c, auto)

lemma wtPB[simp]: "M.wtPB Φ ⟹ wtPB Φ"
unfolding M.wtPB_def wtPB_def by auto

end (* context M_Signature *)


subsection‹Completeness›

(* In our implicitly-typed setting, ``e" is just the identity. *)

text‹The next puts together an M$\_$signature with a structure for its U.flattened signature:›

locale UM_Struct =
M? : M_Signature wtFsym wtPsym arOf resOf parOf +
U? : CU.Struct wtFsym wtPsym "length o arOf" "length o parOf" D intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and D and intF and intP

sublocale UM_Struct < M? : M.Struct where intT = "λ σ. D"
  apply standard
  apply(rule NE_D)
  unfolding list_all2_list_all apply(rule intF) by auto

context UM_Struct begin

lemma wtE[simp]: "M.wtE ξ ⟹ U.wtE ξ"
unfolding U.wtE_def M.wtE_def by auto

lemma int_e[simp]: "U.int ξ T = M.int ξ T"
by (induct T, simp_all add: list_all_iff) (metis map_eq_conv)

lemma int_o_e[simp]: "U.int ξ = M.int ξ"
unfolding int_e fun_eq_iff by simp

lemma satA_e[simp]: "U.satA ξ at ⟷ M.satA ξ at"
by (cases at) auto

lemma satL_e[simp]: "U.satL ξ l ⟷ M.satL ξ l"
apply(cases l) by auto

lemma satC_e[simp]: "U.satC ξ c ⟷ M.satC ξ c"
unfolding M.satC_def U.satC_def by (induct c, simp_all)

lemma satPB_e[simp]: "U.satPB ξ Φ ⟷ M.satPB ξ Φ"
unfolding M.satPB_def U.satPB_def by auto

theorem completeness:
assumes "U.SAT Φ"  shows "M.SAT Φ"
using assms unfolding M.SAT_def satPB_e U.SAT_def by auto

end (* context UM_Struct *)

locale UM_Model =
  M_Problem wtFsym wtPsym arOf resOf parOf Φ +
  UM_Struct wtFsym wtPsym arOf resOf parOf D intF intP +
  CU.Model wtFsym wtPsym  "length o arOf" "length o parOf" Φ
          D intF intP
for wtFsym :: "'fsym ⇒ bool" and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and D and intF and intP
begin

theorem M_U_completeness: "MModel (λσ::'tp. D) intF intP"
apply standard apply(rule completeness[OF SAT]) .

end (* context UM_Model *)

text‹Global statement of completeness : UM$\_$Model consists
of an M.problem and an U.model satisfying the U.translation of this problem.
It is stated that it yields a model for the M.problem.›
sublocale UM_Model < CM.Model where intT = "λ σ. D"
using M_U_completeness .


subsection‹Soundness for monotonic problems›

sublocale M_FullStruct < U? : CU.Struct
where arOf = "length o arOf" and parOf = "length o parOf" and D = "intT any"
apply standard
  apply(rule NE_intT)
  apply (rule full2)
  unfolding full_True list_all2_list_all by auto


context M_FullModel begin

lemma wtE[simp]: "U.wtE ξ ⟹ F.wtE ξ"
unfolding U.wtE_def F.wtE_def by auto

lemma int_e[simp]: "U.int ξ T = F.int ξ T"
by (induct T, simp_all add: list_all_iff) (metis map_eq_conv)

lemma int_o_e[simp]: "U.int ξ = F.int ξ"
unfolding fun_eq_iff by auto

lemma satA_e[simp]: "U.satA ξ at ⟷ F.satA ξ at"
by (cases at) auto

lemma satL_e[simp]: "U.satL ξ l ⟷ F.satL ξ l"
by (cases l) auto

lemma satC_e[simp]: "U.satC ξ c ⟷ F.satC ξ c"
unfolding F.satC_def U.satC_def by (induct c, simp_all)

lemma satPB_e[simp]: "U.satPB ξ Φ ⟷ F.satPB ξ Φ"
unfolding F.satPB_def U.satPB_def by auto

theorem soundness: "U.SAT Φ"
unfolding U.SAT_def using sat_Φ satPB_e by auto

lemma U_Model:
"CU.Model wtFsym wtPsym (length ∘ arOf) (length ∘ parOf) Φ (intT any) intF intP"
by standard (rule wtPB[OF wt_Φ], rule soundness)

end (* context M_FullModel *)


sublocale M_FullModel < CU.Model
where arOf = "length o arOf" and parOf = "length o parOf" and D = "intT any"
using U_Model .

context M_MonotModel begin

theorem M_U_soundness:
"CU.Model wtFsym wtPsym (length ∘ arOf) (length ∘ parOf) Φ
  (InfModel.intTF (any::'tp))
  (InfModel.intFF arOf resOf intTI intFI) (InfModel.intPF parOf intTI intPI)"
apply(rule M_FullModel.U_Model)
unfolding M_FullModel_def apply(rule InfModel.FullModel)
apply(rule MonotModel.InfModelI) ..

end (* context M_MonotModel *)


text‹Global statement of the soundness theorem: M$\_$MonotModel consists
of a monotonic F.problem satisfied by an F.model.
It is stated that this yields an U.Model for the translated problem.›

sublocale M_MonotModel < CU.Model
where arOf = "length o arOf" and parOf = "length o parOf"
and Φ = Φ and D = "intTF (any::'tp)" and intF = intFF and intP = intPF
using M_U_soundness .


end