The main lemma in this file, concretize?_some_same, proves that succesful concretization results in a concrete environment that corresponds to the given literal symbolic environment.

theorem Cedar.Thm.term_entityUID?_some_iff_eq {t : SymCC.Term} {uid : Spec.EntityUID} : t.entityUID? = some uid ↔ t = SymCC.Term.prim (SymCC.TermPrim.entity uid)

theorem Cedar.Thm.term_recordValue?_some_same {t : SymCC.Term} {r : Data.Map Spec.Attr Spec.Value} : t.recordValue? = some r → Spec.Value.record r ∼ t

theorem Cedar.Thm.term_tag?_some_iff_eq {t : SymCC.Term} {s : String} : t.tag? = some s ↔ t = SymCC.Term.string s

theorem Cedar.Thm.concretize?_taggedValueFor_some_implies {tuid : SymCC.Term} {tag tag' : Spec.Tag} {v : Spec.Value} {τs : SymCC.SymTags} : SymCC.SymEntityData.concretize?.taggedValueFor τs tuid tag = some (tag', v) → tag = tag' ∧ (τs.getTag! tuid (SymCC.Term.string tag)).value? = some v

theorem Cedar.Thm.concretize?_some_same {x : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} : εnv.WellFormedFor x → SymCC.SymEnv.concretize? x εnv = some env → env ∼ εnv