This file proves the compilation lemmas for .hasAttr and .getAttr expressions. #
theorem
Cedar.Thm.compile_evaluate_hasAttr
{x₁ : Spec.Expr}
{a : Spec.Attr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (x₁.hasAttr a))
(hwε : εnv.WellFormedFor (x₁.hasAttr a))
(hok : SymCC.compile (x₁.hasAttr a) εnv = Except.ok t)
(ih : CompileEvaluate x₁)
:
theorem
Cedar.Thm.compile_interpret_hasAttr
{x₁ : Spec.Expr}
{a : Spec.Attr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (x₁.hasAttr a))
(hok : SymCC.compile (x₁.hasAttr a) εnv = Except.ok t)
(ih : CompileInterpret x₁)
:
theorem
Cedar.Thm.compile_evaluate_getAttr
{x₁ : Spec.Expr}
{a : Spec.Attr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (x₁.getAttr a))
(hwε : εnv.WellFormedFor (x₁.getAttr a))
(hok : SymCC.compile (x₁.getAttr a) εnv = Except.ok t)
(ih : CompileEvaluate x₁)
:
theorem
Cedar.Thm.compile_interpret_getAttr
{x₁ : Spec.Expr}
{a : Spec.Attr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (x₁.getAttr a))
(hok : SymCC.compile (x₁.getAttr a) εnv = Except.ok t)
(ih : CompileInterpret x₁)
: