This file contains utility lemmas for proving compilation theorems about lists of argument terms. #
theorem
Cedar.Thm.compile_wfs
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{ts : List SymCC.Term}
(hwφ : ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x)
(hok : List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x εnv = Except.ok t) xs ts)
(t : SymCC.Term)
:
t ∈ ts → SymCC.Term.WellFormed εnv.entities t
theorem
Cedar.Thm.compile_interpret_ihs
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{ts : List SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileInterpret x)
(hok : List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x εnv = Except.ok t) xs ts)
:
List.Forall₂
(fun (x : Spec.Expr) (t : SymCC.Term) =>
SymCC.compile x (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t))
xs ts
theorem
Cedar.Thm.compile_interpret_args_not_error
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{xs : List Spec.Expr}
{ts : List SymCC.Term}
{e : SymCC.Error}
:
List.Forall₂
(fun (x : Spec.Expr) (t : SymCC.Term) =>
SymCC.compile x (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t))
xs ts →
List.mapM (fun (x : Spec.Expr) => SymCC.compile x (SymCC.SymEnv.interpret I εnv)) xs = Except.error e → False
theorem
Cedar.Thm.compile_interpret_terms
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{ts ts' : List SymCC.Term}
(h₁ :
List.Forall₂
(fun (x : Spec.Expr) (t : SymCC.Term) =>
SymCC.compile x (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t))
xs ts)
(h₂ :
List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x (SymCC.SymEnv.interpret I εnv) = Except.ok t) xs
ts')
:
List.Forall₂ (fun (t t' : SymCC.Term) => SymCC.Term.interpret I t = t') ts ts'
theorem
Cedar.Thm.compile_evaluate_ihs
{ts : List SymCC.Term}
{xs : List Spec.Expr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
(heq : env ∼ εnv)
(hwe : ∀ (x : Spec.Expr), x ∈ xs → env.WellFormedFor x)
(hwε : ∀ (x : Spec.Expr), x ∈ xs → εnv.WellFormedFor x)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileEvaluate x)
(hok : List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => SymCC.compile x εnv = Except.ok t) xs ts)
:
List.Forall₂ (fun (x : Spec.Expr) (t : SymCC.Term) => Spec.evaluate x env.request env.entities ∼ t) xs ts