The Theory xl-mm1

The Theory xl-mm1

Parents

gst

Constants

	GS
InferProp	GS
ProgProp	GS
DocProp	GS
Specification	GS
Program	GS
Language	GS
Document	GS
mk_ip	GS → GS → GS → GS
mk_pp	GS → GS → GS
mk_dp	GS → GS → GS
mk_spec	GS → GS → GS
ip_out	GS → GS
ip_in	GS → GS
ip_prog	GS → GS
pp_prog	GS → GS
pp_spec	GS → GS
dp_doc	GS → GS
dp_lang	GS → GS
out_lang	GS → GS
in_lang	GS → GS
TrueDocP	GS → BOOL
DocInferP	GS → BOOL
SoundProgP	GS → BOOL

Definitions

Document Language Program Specification DocProp ProgProp InferProp	⊢ ¬ ∈_g Document ∧ Language = ℘_g Document ∧ Program = Document _g Document ∧ Specification = Language ×_g Language ∧ DocProp = Language ×_g Document ∧ ProgProp = Specification ×_g Program ∧ InferProp = Program ×_g Document ×_g Document
mk_spec mk_dp mk_pp mk_ip	⊢ mk_spec = $↦_g ∧ mk_dp = $↦_g ∧ mk_pp = $↦_g ∧ mk_ip = (λ pr inp out• pr ↦_g inp ↦_g out)
in_lang out_lang dp_lang dp_doc pp_spec pp_prog ip_prog ip_in ip_out	⊢ in_lang = fst ∧ out_lang = snd ∧ dp_lang = fst ∧ dp_doc = snd ∧ pp_spec = fst ∧ pp_prog = snd ∧ ip_prog = fst ∧ ip_in = (λ d• fst (snd d)) ∧ ip_out = (λ d• snd (snd d))
TrueDocP	⊢ ∀ dp • TrueDocP dp ⇔ dp ∈_g DocProp ∧ dp_doc dp ∈_g dp_lang dp
DocInferP	⊢ ∀ ip • DocInferP ip ⇔ ip ∈_g InferProp ∧ ip_in ip ↦_g ip_out ip ∈_g ip_prog ip
SoundProgP	⊢ ∀ pp • SoundProgP pp ⇔ pp ∈_g ProgProp ∧ (∀ ind oud • TrueDocP (mk_dp (in_lang (pp_spec pp)) ind) ∧ DocInferP (mk_ip (pp_prog pp) ind oud) ⇒ TrueDocP (mk_dp (out_lang (pp_spec pp)) oud))

Theorems

id_spec_thm	⊢ ∀ l• l ∈_g Language ⇒ SoundProgP ((l ↦_g l) ↦_g id l)
mm1_mp_thm	⊢ ∀ in_doc in_lan p out_doc out_lan • TrueDocP (mk_dp in_lan in_doc) ∧ SoundProgP (mk_pp (mk_spec in_lan out_lan) p) ∧ DocInferP (mk_ip p in_doc out_doc) ⇒ TrueDocP (mk_dp out_lan out_doc)
mm1_mpc_thm	⊢ ∀ d1 l1 d2 l2 d3 l3 p1 p2 • TrueDocP (mk_dp l1 d1) ∧ SoundProgP (mk_pp (mk_spec l1 l2) p1) ∧ SoundProgP (mk_pp (mk_spec l2 l3) p2) ∧ DocInferP (mk_ip p1 d1 d2) ∧ DocInferP (mk_ip p2 d2 d3) ⇒ TrueDocP (mk_dp l3 d3)

privacy policy

Created:

V