Theory CM

(* Countable version of MFOL structures: *)
theory CM
imports M
begin

(* Countable Versions of the locales from M
that assume a fixed countable carrier univ
instead of an arbitrary one 'univ: *)
locale Tstruct = M.Tstruct intT
for intT :: "'tp ⇒ univ ⇒ bool"

locale Struct = M.Struct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf :: "'psym ⇒ 'tp list"
and intT :: "'tp ⇒ univ ⇒ bool"
and intF and intP

locale Model = M.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym and wtPsym
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf :: "'psym ⇒ 'tp list" and Φ
and intT :: "'tp ⇒ univ ⇒ bool"
and intF and intP

sublocale Struct < Tstruct ..
sublocale Model < Struct ..


end