This file proves the compilation lemmas for .binaryApp expressions. #
theorem
Cedar.Thm.interpret_compileInₑ
{t₁ t₂ : SymCC.Term}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
(hwε : εs.WellFormed)
(hI : I.WellFormed εs)
(hwφ₁ : SymCC.Term.WellFormed εs t₁)
(hwφ₂ : SymCC.Term.WellFormed εs t₂)
(hwl₁ : SymCC.Term.WellFormed εs (SymCC.Term.interpret I t₁) ∧ (SymCC.Term.interpret I t₁).typeOf = t₁.typeOf)
(hwl₂ : SymCC.Term.WellFormed εs (SymCC.Term.interpret I t₂) ∧ (SymCC.Term.interpret I t₂).typeOf = t₂.typeOf)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety₁)
(hty₂ : t₂.typeOf = SymCC.TermType.entity ety₂)
:
SymCC.Term.interpret I (SymCC.compileInₑ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂)) = SymCC.compileInₑ (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
((SymCC.SymEntities.interpret I εs).ancestorsOfType ety₁ ety₂)
theorem
Cedar.Thm.interpret_compileInₛ
{t₁ t₂ : SymCC.Term}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
(hwε : εs.WellFormed)
(hI : I.WellFormed εs)
(hwφ₁ : SymCC.Term.WellFormed εs t₁)
(hwφ₂ : SymCC.Term.WellFormed εs t₂)
(hwl₁ : SymCC.Term.WellFormed εs (SymCC.Term.interpret I t₁) ∧ (SymCC.Term.interpret I t₁).typeOf = t₁.typeOf)
(hwl₂ : SymCC.Term.WellFormed εs (SymCC.Term.interpret I t₂) ∧ (SymCC.Term.interpret I t₂).typeOf = t₂.typeOf)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety₁)
(hty₂ : t₂.typeOf = (SymCC.TermType.entity ety₂).set)
:
SymCC.Term.interpret I (SymCC.compileInₛ t₁ t₂ (εs.ancestorsOfType ety₁ ety₂)) = SymCC.compileInₛ (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
((SymCC.SymEntities.interpret I εs).ancestorsOfType ety₁ ety₂)
theorem
Cedar.Thm.interpret_hasTag
{t₁ t₂ : SymCC.Term}
{ety : Spec.EntityType}
{εs : SymCC.SymEntities}
{τs : SymCC.SymTags}
{I : SymCC.Interpretation}
(hwτ : SymCC.SymTags.WellFormed εs ety τs)
(hI : I.WellFormed εs)
(hwφ₁ : SymCC.Term.WellFormed εs t₁)
(hwφ₂ : SymCC.Term.WellFormed εs t₂)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety)
:
(SymCC.SymTags.interpret I τs).hasTag (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂) = SymCC.Term.interpret I (τs.hasTag t₁ t₂)
theorem
Cedar.Thm.interpret_getTag
{t₁ t₂ : SymCC.Term}
{ety : Spec.EntityType}
{εs : SymCC.SymEntities}
{τs : SymCC.SymTags}
{I : SymCC.Interpretation}
(hwτ : SymCC.SymTags.WellFormed εs ety τs)
(hI : I.WellFormed εs)
(hwφ₁ : SymCC.Term.WellFormed εs t₁)
(hwφ₂ : SymCC.Term.WellFormed εs t₂)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety)
(hty₂ : t₂.typeOf = SymCC.TermType.string)
:
(SymCC.SymTags.interpret I τs).getTag (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂) = SymCC.Term.interpret I (τs.getTag t₁ t₂)
theorem
Cedar.Thm.compile_interpret_binaryApp
{op₂ : Spec.BinaryOp}
{x₁ x₂ : Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (Spec.Expr.binaryApp op₂ x₁ x₂))
(hok : SymCC.compile (Spec.Expr.binaryApp op₂ x₁ x₂) εnv = Except.ok t)
(ih₁ : CompileInterpret x₁)
(ih₂ : CompileInterpret x₂)
:
SymCC.compile (Spec.Expr.binaryApp op₂ x₁ x₂) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)
theorem
Cedar.Thm.same_entities_ancestors_none_of_type
{es : Spec.Entities}
{εs : SymCC.SymEntities}
{e₁ e₂ : Spec.EntityUID}
(heq : es ∼ εs)
(hno : εs.ancestorsOfType e₁.ty e₂.ty = none)
:
theorem
Cedar.Thm.same_entities_ancestors_some_of_type
{es : Spec.Entities}
{εs : SymCC.SymEntities}
{e₁ : Spec.EntityUID}
{ety₂ : Spec.EntityType}
{ancs : SymCC.UnaryFunction}
(heq : es ∼ εs)
(hwf : Spec.Value.WellFormed es (Spec.Value.prim (Spec.Prim.entityUID e₁)))
(hso : εs.ancestorsOfType e₁.ty ety₂ = some ancs)
:
∃ (ts : Data.Set SymCC.Term), SymCC.Factory.app ancs (SymCC.Term.prim (SymCC.TermPrim.entity e₁)) = SymCC.Term.set ts (SymCC.TermType.entity ety₂) ∧ (SymCC.Term.set ts (SymCC.TermType.entity ety₂)).isLiteral = true ∧ ∀ (e₂ : Spec.EntityUID),
e₂.ty = ety₂ → (SymCC.Term.prim (SymCC.TermPrim.entity e₂) ∈ ts ↔ e₂ ∈ es.ancestorsOrEmpty e₁)
theorem
Cedar.Thm.compile_evaluate_binaryApp
{op₂ : Spec.BinaryOp}
{x₁ x₂ : Spec.Expr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (Spec.Expr.binaryApp op₂ x₁ x₂))
(hwε : εnv.WellFormedFor (Spec.Expr.binaryApp op₂ x₁ x₂))
(hok : SymCC.compile (Spec.Expr.binaryApp op₂ x₁ x₂) εnv = Except.ok t)
(ih₁ : CompileEvaluate x₁)
(ih₂ : CompileEvaluate x₂)
: