The lemmas in this file prove key properties of well-structured and well-formed values.
theorem
Cedar.Thm.value_record_entityUIDs_def
{avs : Data.Map Spec.Attr Spec.Value}
:
(Spec.Value.record avs).entityUIDs = List.mapUnion
(fun (x : Spec.Attr × Spec.Value) =>
match x with
| (fst, v) => v.entityUIDs)
avs.toList
theorem
Cedar.Thm.value_ws_closed_implies_wf
{v : Spec.Value}
{es : Spec.Entities}
:
v.WellStructured → es.ClosedFor v.entityUIDs → Spec.Value.WellFormed es v
theorem
Cedar.Thm.term_prim_value?_some_implies_ws
{t : SymCC.TermPrim}
{v : Spec.Value}
:
t.value? = some v → v.WellStructured
theorem
Cedar.Thm.term_set_value?_some_implies
{ts : List SymCC.Term}
{ty : SymCC.TermType}
{v : Spec.Value}
:
(SymCC.Term.set (Data.Set.mk ts) ty).value? = some v →
∃ (vs : List Spec.Value), List.mapM SymCC.Term.value? ts = some vs ∧ Spec.Value.set (Data.Set.make vs) = v
theorem
Cedar.Thm.term_set_value?_some_implies_ws
{ts : List SymCC.Term}
{ty : SymCC.TermType}
{v : Spec.Value}
{εs : SymCC.SymEntities}
(hw : SymCC.Term.WellFormed εs (SymCC.Term.set (Data.Set.mk ts) ty))
(hv : (SymCC.Term.set (Data.Set.mk ts) ty).value? = some v)
(ih :
∀ (tᵢ : SymCC.Term),
tᵢ ∈ ts → ∀ {vᵢ : Spec.Value}, SymCC.Term.WellFormed εs tᵢ → tᵢ.value? = some vᵢ → vᵢ.WellStructured)
:
theorem
Cedar.Thm.term_value?_some_implies_ws
{t : SymCC.Term}
{v : Spec.Value}
{εs : SymCC.SymEntities}
:
SymCC.Term.WellFormed εs t → t.value? = some v → v.WellStructured
theorem
Cedar.Thm.term_value?_some_implies_eq_entityUIDs
{t : SymCC.Term}
{v : Spec.Value}
:
t.value? = some v → t.entityUIDs = v.entityUIDs