This file proves the compilation lemmas for .lit and .var expressions. #
theorem
Cedar.Thm.compile_evaluate_lit
{p : Spec.Prim}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(h₁ : SymCC.compile (Spec.Expr.lit p) εnv = Except.ok t)
:
theorem
Cedar.Thm.compile_evaluate_var
{v : Spec.Var}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(h₁ : env ∼ εnv)
(h₂ : SymCC.compile (Spec.Expr.var v) εnv = Except.ok t)
:
theorem
Cedar.Thm.compile_interpret_lit
{p : Spec.Prim}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : SymCC.compile (Spec.Expr.lit p) εnv = Except.ok t)
:
SymCC.compile (Spec.Expr.lit p) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)
theorem
Cedar.Thm.compile_interpret_var
{v : Spec.Var}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : I.WellFormed εnv.entities)
(h₂ : εnv.WellFormedFor (Spec.Expr.var v))
(h₃ : SymCC.compile (Spec.Expr.var v) εnv = Except.ok t)
:
SymCC.compile (Spec.Expr.var v) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)