This file contains helper lemmas that are shared by assumption proofs.
theorem
Cedar.Thm.interpret_option_entity_term
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
{ety : Spec.EntityType}
:
I.WellFormed εs →
SymCC.Term.WellFormed εs t →
t.typeOf = (SymCC.TermType.entity ety).option →
SymCC.Term.interpret I t = SymCC.Term.none (SymCC.TermType.entity ety) ∨ ∃ (uid : Spec.EntityUID), SymCC.Term.interpret I t = (SymCC.Term.entity uid).some ∧ uid.ty = ety
theorem
Cedar.Thm.compile_interpret_entity_implies_wf
{uid : Spec.EntityUID}
{x : Spec.Expr}
{t : SymCC.Term}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
(heq : env ∼ SymCC.SymEnv.interpret I εnv)
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor x)
(hwe : env.WellFormedFor x)
(hok : SymCC.compile x εnv = Except.ok t)
(ht : SymCC.Term.interpret I t = (SymCC.Term.entity uid).some)
:
theorem
Cedar.Thm.wfl_entity
{uid : Spec.EntityUID}
{εs : SymCC.SymEntities}
:
εs.isValidEntityUID uid = true → SymCC.Term.WellFormedLiteral εs (SymCC.Term.entity uid)
theorem
Cedar.Thm.εs_ancestors_find?_implies_ancestors
{ety : Spec.EntityType}
{δ : SymCC.SymEntityData}
{εs : SymCC.SymEntities}
:
theorem
Cedar.Thm.εs_ancestors_find?_implies_ancestorsOfType
{ety₁ ety₂ : Spec.EntityType}
{δ : SymCC.SymEntityData}
{f : SymCC.UnaryFunction}
{εs : SymCC.SymEntities}
:
Data.Map.find? εs ety₁ = some δ → δ.ancestors.find? ety₂ = some f → εs.ancestorsOfType ety₁ ety₂ = some f
theorem
Cedar.Thm.wf_term_interpret_option_entity_implies_wf_typeOf
{t : SymCC.Term}
{uid : Spec.EntityUID}
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
(hI : I.WellFormed εs)
(hwt : SymCC.Term.WellFormed εs t)
(ht : SymCC.Term.interpret I t = (SymCC.Term.entity uid).some)
:
SymCC.Term.WellFormed εs (SymCC.Term.interpret I t) ∧ t.typeOf = (SymCC.TermType.entity uid.ty).option