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
fill∧ Language = ℘g Document
fill∧ Program = Document g Document
fill∧ Specification = Language ×g Language
fill∧ DocProp = Language ×g Document
fill∧ ProgProp = Specification ×g Program
fill∧ InferProp = Program ×g Document ×g Document
mk_spec
mk_dp
mk_pp
mk_ip
⊢ mk_spec = $↦g
fill∧ mk_dp = $↦g
fill∧ mk_pp = $↦g
fill∧ 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
fill∧ out_lang = snd
fill∧ dp_lang = fst
fill∧ dp_doc = snd
fill∧ pp_spec = fst
fill∧ pp_prog = snd
fill∧ ip_prog = fst
fill∧ ip_in = (λ d• fst (snd d))
fill∧ ip_out = (λ d• snd (snd d))
TrueDocP
⊢ ∀ dp
fill• TrueDocP dp
fill⇔ dp ∈g DocProp ∧ dp_doc dp ∈g dp_lang dp
DocInferP
⊢ ∀ ip
fill• DocInferP ip
fill⇔ ip ∈g InferProp
fill∧ ip_in ip ↦g ip_out ip ∈g ip_prog ip
SoundProgP
⊢ ∀ pp
fill• SoundProgP pp
fill⇔ pp ∈g ProgProp
fill∧ (∀ ind oud
fill• TrueDocP (mk_dp (in_lang (pp_spec pp)) ind)
fill∧ DocInferP (mk_ip (pp_prog pp) ind oud)
fill⇒ TrueDocP
fill(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
fill• TrueDocP (mk_dp in_lan in_doc)
fill∧ SoundProgP (mk_pp (mk_spec in_lan out_lan) p)
fill∧ DocInferP (mk_ip p in_doc out_doc)
fill⇒ TrueDocP (mk_dp out_lan out_doc)
mm1_mpc_thm
⊢ ∀ d1 l1 d2 l2 d3 l3 p1 p2
fill• TrueDocP (mk_dp l1 d1)
fill∧ SoundProgP (mk_pp (mk_spec l1 l2) p1)
fill∧ SoundProgP (mk_pp (mk_spec l2 l3) p2)
fill∧ DocInferP (mk_ip p1 d1 d2)
fill∧ DocInferP (mk_ip p2 d2 d3)
fill⇒ TrueDocP (mk_dp l3 d3)

up quick index

privacy policy

Created:

V