def
Cedar.Thm.SubstituteActionPreservesEvaluation
(expr : Spec.Expr)
(request : Spec.Request)
(entities : Spec.Entities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.substitute_action_preserves_evaluation_ite
{i t e : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation i request entities)
(ih₂ : SubstituteActionPreservesEvaluation t request entities)
(ih₃ : SubstituteActionPreservesEvaluation e request entities)
:
Spec.evaluate (Validation.substituteAction request.action (i.ite t e)) request entities = Spec.evaluate (i.ite t e) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_getAttr
{e : Spec.Expr}
{attr : Spec.Attr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation e request entities)
:
Spec.evaluate (Validation.substituteAction request.action (e.getAttr attr)) request entities = Spec.evaluate (e.getAttr attr) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_hasAttr
{e : Spec.Expr}
{attr : Spec.Attr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation e request entities)
:
Spec.evaluate (Validation.substituteAction request.action (e.hasAttr attr)) request entities = Spec.evaluate (e.hasAttr attr) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_unaryApp
{op : Spec.UnaryOp}
{e : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation e request entities)
:
Spec.evaluate (Validation.substituteAction request.action (Spec.Expr.unaryApp op e)) request entities = Spec.evaluate (Spec.Expr.unaryApp op e) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_binaryApp
{op : Spec.BinaryOp}
{a b : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation a request entities)
(ih₂ : SubstituteActionPreservesEvaluation b request entities)
:
Spec.evaluate (Validation.substituteAction request.action (Spec.Expr.binaryApp op a b)) request entities = Spec.evaluate (Spec.Expr.binaryApp op a b) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_and
{a b : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation a request entities)
(ih₂ : SubstituteActionPreservesEvaluation b request entities)
:
Spec.evaluate (Validation.substituteAction request.action (a.and b)) request entities = Spec.evaluate (a.and b) request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluation_or
{a b : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : SubstituteActionPreservesEvaluation a request entities)
(ih₂ : SubstituteActionPreservesEvaluation b request entities)
:
Spec.evaluate (Validation.substituteAction request.action (a.or b)) request entities = Spec.evaluate (a.or b) request entities
theorem
Cedar.Thm.substitute_action_cons_set
(h : Spec.Expr)
(t : List Spec.Expr)
(uid : Spec.EntityUID)
:
Validation.substituteAction uid (Spec.Expr.set (h :: t)) = Spec.Expr.set (Validation.substituteAction uid h :: List.map (Validation.substituteAction uid) t)
theorem
Cedar.Thm.substitute_action_preserves_evaluation_set
{xs : List Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → SubstituteActionPreservesEvaluation xᵢ request entities)
:
Spec.evaluate (Validation.substituteAction request.action (Spec.Expr.set xs)) request entities = Spec.evaluate (Spec.Expr.set xs) request entities
theorem
Cedar.Thm.substitute_action_cons_record
(ax : Spec.Attr × Spec.Expr)
(axs : List (Spec.Attr × Spec.Expr))
(uid : Spec.EntityUID)
:
Validation.substituteAction uid (Spec.Expr.record (ax :: axs)) = Spec.Expr.record
((ax.fst, Validation.substituteAction uid ax.snd) :: List.map
(fun (x : Spec.Attr × Spec.Expr) =>
match x with
| (a, e) => (a, Validation.substituteAction uid e))
axs)
theorem
Cedar.Thm.substitute_action_preserves_evaluation_record
{axs : List (Spec.Attr × Spec.Expr)}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : ∀ (axᵢ : Spec.Attr × Spec.Expr), axᵢ ∈ axs → SubstituteActionPreservesEvaluation axᵢ.snd request entities)
:
Spec.evaluate (Validation.substituteAction request.action (Spec.Expr.record axs)) request entities = Spec.evaluate (Spec.Expr.record axs) request entities
theorem
Cedar.Thm.substitute_action_cons_call
(x : Spec.Expr)
(xs : List Spec.Expr)
(uid : Spec.EntityUID)
(xfn : Spec.ExtFun)
:
Validation.substituteAction uid (Spec.Expr.call xfn (x :: xs)) = Spec.Expr.call xfn (Validation.substituteAction uid x :: List.map (Validation.substituteAction uid) xs)
theorem
Cedar.Thm.substitute_action_preserves_evaluation_call
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
(ih₁ : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → SubstituteActionPreservesEvaluation xᵢ request entities)
:
Spec.evaluate (Validation.substituteAction request.action (Spec.Expr.call xfn xs)) request entities = Spec.evaluate (Spec.Expr.call xfn xs) request entities
@[irreducible]
theorem
Cedar.Thm.substitute_action_preserves_evaluation
(expr : Spec.Expr)
(request : Spec.Request)
(entities : Spec.Entities)
:
Spec.evaluate (Validation.substituteAction request.action expr) request entities = Spec.evaluate expr request entities
theorem
Cedar.Thm.substitute_action_preserves_evaluates_to
{expr : Spec.Expr}
{request : Spec.Request}
{entities : Spec.Entities}
{v : Spec.Value}
:
EvaluatesTo (Validation.substituteAction request.action expr) request entities v ↔ EvaluatesTo expr request entities v