Theory Static
theory Static imports Values Types begin
axiomatization isof :: "[i,i] ⇒ o"
where isof_app: "⟦isof(c1,t_fun(t1,t2)); isof(c2,t1)⟧ ⟹ isof(c_app(c1,c2),t2)"
definition
isofenv :: "[i,i] ⇒ o" where
"isofenv(ve,te) ≡
ve_dom(ve) = te_dom(te) ∧
(∀x ∈ ve_dom(ve).
∃c ∈ Const. ve_app(ve,x) = v_const(c) ∧ isof(c,te_app(te,x)))"
consts ElabRel :: i
inductive
domains "ElabRel" ⊆ "TyEnv * Exp * Ty"
intros
constI [intro!]:
"⟦te ∈ TyEnv; c ∈ Const; t ∈ Ty; isof(c,t)⟧ ⟹
<te,e_const(c),t> ∈ ElabRel"
varI [intro!]:
"⟦te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te)⟧ ⟹
<te,e_var(x),te_app(te,x)> ∈ ElabRel"
fnI [intro!]:
"⟦te ∈ TyEnv; x ∈ ExVar; e ∈ Exp; t1 ∈ Ty; t2 ∈ Ty;
<te_owr(te,x,t1),e,t2> ∈ ElabRel⟧ ⟹
<te,e_fn(x,e),t_fun(t1,t2)> ∈ ElabRel"
fixI [intro!]:
"⟦te ∈ TyEnv; f ∈ ExVar; x ∈ ExVar; t1 ∈ Ty; t2 ∈ Ty;
<te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> ∈ ElabRel⟧ ⟹
<te,e_fix(f,x,e),t_fun(t1,t2)> ∈ ElabRel"
appI [intro]:
"⟦te ∈ TyEnv; e1 ∈ Exp; e2 ∈ Exp; t1 ∈ Ty; t2 ∈ Ty;
<te,e1,t_fun(t1,t2)> ∈ ElabRel;
<te,e2,t1> ∈ ElabRel⟧ ⟹ <te,e_app(e1,e2),t2> ∈ ElabRel"
type_intros te_appI Exp.intros Ty.intros
inductive_cases
elab_constE [elim!]: "<te,e_const(c),t> ∈ ElabRel"
and elab_varE [elim!]: "<te,e_var(x),t> ∈ ElabRel"
and elab_fnE [elim]: "<te,e_fn(x,e),t> ∈ ElabRel"
and elab_fixE [elim!]: "<te,e_fix(f,x,e),t> ∈ ElabRel"
and elab_appE [elim]: "<te,e_app(e1,e2),t> ∈ ElabRel"
declare ElabRel.dom_subset [THEN subsetD, dest]
end