Theory ECR
theory ECR imports Static Dynamic begin
consts
HasTyRel :: i
coinductive
domains "HasTyRel" ⊆ "Val * Ty"
intros
htr_constI [intro!]:
"⟦c ∈ Const; t ∈ Ty; isof(c,t)⟧ ⟹ <v_const(c),t> ∈ HasTyRel"
htr_closI [intro]:
"⟦x ∈ ExVar; e ∈ Exp; t ∈ Ty; ve ∈ ValEnv; te ∈ TyEnv;
<te,e_fn(x,e),t> ∈ ElabRel;
ve_dom(ve) = te_dom(te);
{<ve_app(ve,y),te_app(te,y)>.y ∈ ve_dom(ve)} ∈ Pow(HasTyRel)⟧
⟹ <v_clos(x,e,ve),t> ∈ HasTyRel"
monos Pow_mono
type_intros Val_ValEnv.intros
definition
hastyenv :: "[i,i] ⇒ o" where
"hastyenv(ve,te) ≡
ve_dom(ve) = te_dom(te) ∧
(∀x ∈ ve_dom(ve). <ve_app(ve,x),te_app(te,x)> ∈ HasTyRel)"
lemma htr_closCI [intro]:
"⟦x ∈ ExVar; e ∈ Exp; t ∈ Ty; ve ∈ ValEnv; te ∈ TyEnv;
<te, e_fn(x, e), t> ∈ ElabRel; ve_dom(ve) = te_dom(te);
{<ve_app(ve,y),te_app(te,y)>.y ∈ ve_dom(ve)} ∈
Pow({<v_clos(x,e,ve),t>} ∪ HasTyRel)⟧
⟹ <v_clos(x, e, ve),t> ∈ HasTyRel"
apply (rule singletonI [THEN HasTyRel.coinduct], auto)
done
inductive_cases
htr_constE [elim!]: "<v_const(c),t> ∈ HasTyRel"
and htr_closE [elim]: "<v_clos(x,e,ve),t> ∈ HasTyRel"
lemmas HasTyRel_non_zero =
HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]
lemma hastyenv_owr:
"⟦ve ∈ ValEnv; te ∈ TyEnv; hastyenv(ve,te); ⟨v,t⟩ ∈ HasTyRel⟧
⟹ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)
lemma basic_consistency_lem:
"⟦ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve,te)⟧ ⟹ hastyenv(ve,te)"
unfolding isofenv_def hastyenv_def
apply (force intro: te_appI ve_domI)
done
lemma consistency_const:
"⟦c ∈ Const; hastyenv(ve,te);<te,e_const(c),t> ∈ ElabRel⟧
⟹ <v_const(c), t> ∈ HasTyRel"
by blast
lemma consistency_var:
"⟦x ∈ ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> ∈ ElabRel⟧ ⟹
<ve_app(ve,x),t> ∈ HasTyRel"
by (unfold hastyenv_def, blast)
lemma consistency_fn:
"⟦ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; hastyenv(ve,te);
<te,e_fn(x,e),t> ∈ ElabRel
⟧ ⟹ <v_clos(x, e, ve), t> ∈ HasTyRel"
by (unfold hastyenv_def, blast)
declare ElabRel.dom_subset [THEN subsetD, dest]
declare Ty.intros [simp, intro!]
declare TyEnv.intros [simp, intro!]
declare Val_ValEnv.intros [simp, intro!]
lemma consistency_fix:
"⟦ve ∈ ValEnv; x ∈ ExVar; e ∈ Exp; f ∈ ExVar; cl ∈ Val;
v_clos(x,e,ve_owr(ve,f,cl)) = cl;
hastyenv(ve,te); <te,e_fix(f,x,e),t> ∈ ElabRel⟧ ⟹
⟨cl,t⟩ ∈ HasTyRel"
unfolding hastyenv_def
apply (erule elab_fixE, safe)
apply hypsubst_thin
apply (rule subst, assumption)
apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
apply simp_all
apply (blast intro: ve_owrI)
apply (rule ElabRel.fnI)
apply (simp_all add: ValNEE, force)
done
lemma consistency_app1:
"⟦ve ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; c1 ∈ Const; c2 ∈ Const;
<ve,e1,v_const(c1)> ∈ EvalRel;
∀t te.
hastyenv(ve,te) ⟶ <te,e1,t> ∈ ElabRel ⟶ <v_const(c1),t> ∈ HasTyRel;
<ve, e2, v_const(c2)> ∈ EvalRel;
∀t te.
hastyenv(ve,te) ⟶ <te,e2,t> ∈ ElabRel ⟶ <v_const(c2),t> ∈ HasTyRel;
hastyenv(ve, te);
<te,e_app(e1,e2),t> ∈ ElabRel⟧
⟹ <v_const(c_app(c1, c2)),t> ∈ HasTyRel"
by (blast intro!: c_appI intro: isof_app)
lemma consistency_app2:
"⟦ve ∈ ValEnv; vem ∈ ValEnv; e1 ∈ Exp; e2 ∈ Exp; em ∈ Exp; xm ∈ ExVar;
v ∈ Val;
<ve,e1,v_clos(xm,em,vem)> ∈ EvalRel;
∀t te. hastyenv(ve,te) ⟶
<te,e1,t> ∈ ElabRel ⟶ <v_clos(xm,em,vem),t> ∈ HasTyRel;
<ve,e2,v2> ∈ EvalRel;
∀t te. hastyenv(ve,te) ⟶ <te,e2,t> ∈ ElabRel ⟶ ⟨v2,t⟩ ∈ HasTyRel;
<ve_owr(vem,xm,v2),em,v> ∈ EvalRel;
∀t te. hastyenv(ve_owr(vem,xm,v2),te) ⟶
<te,em,t> ∈ ElabRel ⟶ ⟨v,t⟩ ∈ HasTyRel;
hastyenv(ve,te); <te,e_app(e1,e2),t> ∈ ElabRel⟧
⟹ ⟨v,t⟩ ∈ HasTyRel"
apply (erule elab_appE)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
apply (erule htr_closE)
apply (erule elab_fnE, simp)
apply clarify
apply (drule spec [THEN spec, THEN mp, THEN mp])
prefer 2 apply assumption+
apply (rule hastyenv_owr, assumption)
apply assumption
apply (simp add: hastyenv_def, blast+)
done
lemma consistency [rule_format]:
"<ve,e,v> ∈ EvalRel
⟹ (∀t te. hastyenv(ve,te) ⟶ <te,e,t> ∈ ElabRel ⟶ ⟨v,t⟩ ∈ HasTyRel)"
apply (erule EvalRel.induct)
apply (simp_all add: consistency_const consistency_var consistency_fn
consistency_fix consistency_app1)
apply (blast intro: consistency_app2)
done
lemma basic_consistency:
"⟦ve ∈ ValEnv; te ∈ TyEnv; isofenv(ve,te);
<ve,e,v_const(c)> ∈ EvalRel; <te,e,t> ∈ ElabRel⟧
⟹ isof(c,t)"
by (blast dest: consistency intro!: basic_consistency_lem)
end