The Theory xl-mm1
Parents

gst
Constants
'a GS
InferProp
'a GS
ProgProp
'a GS
DocProp
'a GS
Specification
'a GS
Program
'a GS
Language
'a GS
Document
'a GS
mk_ip
'a GS 'a GS 'a GS 'a GS
mk_pp
'a GS 'a GS 'a GS
mk_dp
'a GS 'a GS 'a GS
mk_spec
'a GS 'a GS 'a GS
ip_out
'a GS 'a GS
ip_in
'a GS 'a GS
ip_prog
'a GS 'a GS
pp_prog
'a GS 'a GS
pp_spec
'a GS 'a GS
dp_doc
'a GS 'a GS
dp_lang
'a GS 'a GS
out_lang
'a GS 'a GS
in_lang
'a GS 'a GS
TrueDocP
'a GS BOOL
DocInferP
'a GS BOOL
SoundProgP
'a GS BOOL
Definitions
Document
Language
Program
Specification
DocProp
ProgProp
InferProp
Document
Language = Document
Program = Document Document
Specification = Language Language
DocProp = Language Document
ProgProp = Specification Program
InferProp = Program Document Document
mk_spec
mk_dp
mk_pp
mk_ip
mk_spec = $
mk_dp = $
mk_pp = $
mk_ip = ( pr inp out pr inp 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 DocProp dp_doc dp dp_lang dp
DocInferP
ip
DocInferP ip
ip InferProp
ip_in ip ip_out ip ip_prog ip
SoundProgP
pp
SoundProgP pp
pp 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 Language SoundProgP ((l l) 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)

up quick index © RBJ