This file proves the compilation lemmas for .set expressions. #
theorem
Cedar.Thm.interpret_terms_wfls
{ts : List SymCC.Term}
{ty : SymCC.TermType}
{I : SymCC.Interpretation}
{εs : SymCC.SymEntities}
(hI : I.WellFormed εs)
(hwφ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t)
(hty : ∀ (t : SymCC.Term), t ∈ ts → t.typeOf = ty)
(t : SymCC.Term)
:
t ∈ ts → SymCC.Term.WellFormedLiteral εs (SymCC.Term.interpret I t) ∧ (SymCC.Term.interpret I t).typeOf = ty
theorem
Cedar.Thm.pe_interpret_terms_of_type_option
{ts : List SymCC.Term}
{ty : SymCC.TermType}
{I : SymCC.Interpretation}
{εs : SymCC.SymEntities}
(hwi :
∀ (t : SymCC.Term),
t ∈ ts → SymCC.Term.WellFormedLiteral εs (SymCC.Term.interpret I t) ∧ (SymCC.Term.interpret I t).typeOf = ty.option)
:
(∃ (ty : SymCC.TermType), SymCC.Term.none ty ∈ List.map (SymCC.Term.interpret I) ts) ∨ ∃ (ts' : List SymCC.Term), List.map (SymCC.Term.interpret I) ts = List.map SymCC.Term.some ts'
theorem
Cedar.Thm.compile_interpret_set
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (Spec.Expr.set xs))
(hok : SymCC.compile (Spec.Expr.set xs) εnv = Except.ok t)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileInterpret x)
:
SymCC.compile (Spec.Expr.set xs) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)
theorem
Cedar.Thm.compile_evaluate_set
{xs : List Spec.Expr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (Spec.Expr.set xs))
(hwε : εnv.WellFormedFor (Spec.Expr.set xs))
(hok : SymCC.compile (Spec.Expr.set xs) εnv = Except.ok t)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileEvaluate x)
: