Properties of literal terms

This file proves basic lemmas about literal terms

@[simp]

theorem Cedar.Thm.isLiteral_empty (eltsTy : SymCC.TermType) : (SymCC.Term.set Data.Set.empty eltsTy).isLiteral = true

theorem Cedar.Thm.lit_term_set_implies_lit_elt {s : Data.Set SymCC.Term} {ty : SymCC.TermType} {t : SymCC.Term} : (SymCC.Term.set s ty).isLiteral = true → t ∈ s → t.isLiteral = true

theorem Cedar.Thm.lit_term_set_impliedBy_lit_elts {s : Data.Set SymCC.Term} {ty : SymCC.TermType} : (∀ (t : SymCC.Term), t ∈ s → t.isLiteral = true) → (SymCC.Term.set s ty).isLiteral = true

theorem Cedar.Thm.isLiteral_set_cons {hd : SymCC.Term} {tl : List SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set (Data.Set.mk (hd :: tl)) ty).isLiteral = true → hd.isLiteral = true ∧ (SymCC.Term.set (Data.Set.mk tl) ty).isLiteral = true

theorem Cedar.Thm.lit_term_record_implies_lit_value {r : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} {t : SymCC.Term} : (SymCC.Term.record r).isLiteral = true → (a, t) ∈ r.toList → t.isLiteral = true

theorem Cedar.Thm.isLiteral_record_mapOnValues {β : Type u_1} {m : Data.Map Spec.Attr β} {f : β → SymCC.Term} : (SymCC.Term.record (Data.Map.mapOnValues f m)).isLiteral = true ↔ ∀ (v : β), v ∈ m.values → (f v).isLiteral = true

@[simp]

theorem Cedar.Thm.isLiteral_some {t : SymCC.Term} : t.some.isLiteral = true ↔ t.isLiteral = true

@[simp]

theorem Cedar.Thm.isLiteral_none {tty : SymCC.TermType} : (SymCC.Term.none tty).isLiteral = true

@[simp]

theorem Cedar.Thm.isLiteral_prim {p : SymCC.TermPrim} : (SymCC.Term.prim p).isLiteral = true

theorem Cedar.Thm.wfl_of_type_bool_is_bool {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bool → ∃ (b : Bool), t = SymCC.Term.prim (SymCC.TermPrim.bool b)

theorem Cedar.Thm.wfl_of_type_bool_is_true_or_false {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bool → t = SymCC.Term.prim (SymCC.TermPrim.bool true) ∨ t = SymCC.Term.prim (SymCC.TermPrim.bool false)

theorem Cedar.Thm.wfl_of_type_bitvec_is_bitvec {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec n → ∃ (bv : BitVec n), t = SymCC.Term.prim (SymCC.TermPrim.bitvec bv)

theorem Cedar.Thm.wfl_of_type_datetime_is_datetime {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime → ∃ (d : Spec.Ext.Datetime), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))

theorem Cedar.Thm.wfl_of_type_duration_is_duration {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.duration → ∃ (d : Spec.Duration), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))

theorem Cedar.Thm.wfl_of_type_string_is_string {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.string → ∃ (s : String), t = SymCC.Term.prim (SymCC.TermPrim.string s)

theorem Cedar.Thm.wfl_of_type_entity_is_entity {εs : SymCC.SymEntities} {t : SymCC.Term} {ety : Spec.EntityType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.entity ety → ∃ (uid : Spec.EntityUID), t = SymCC.Term.prim (SymCC.TermPrim.entity uid) ∧ uid.ty = ety

theorem Cedar.Thm.wfl_of_type_set_is_set {εs : SymCC.SymEntities} {t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.set → ∃ (s : Data.Set SymCC.Term), t = SymCC.Term.set s ty

theorem Cedar.Thm.wfl_of_type_record_is_record {εs : SymCC.SymEntities} {t : SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.record rty → ∃ (r : Data.Map Spec.Attr SymCC.Term), t = SymCC.Term.record r

theorem Cedar.Thm.wfl_of_type_ext_decimal_is_ext_decimal {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.decimal → ∃ (d : Spec.Ext.Decimal), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.decimal d))

theorem Cedar.Thm.wfl_of_type_ext_ipaddr_is_ext_ipaddr {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → ∃ (ip : Spec.IPAddr), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr ip))

theorem Cedar.Thm.wfl_of_type_ext_datetime_is_ext_datetime {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime → ∃ (d : Spec.Ext.Datetime), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))

theorem Cedar.Thm.wfl_of_type_ext_duration_is_ext_duration {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.duration → ∃ (d : Spec.Ext.Datetime.Duration), t = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))

theorem Cedar.Thm.wfl_of_type_option_is_option {εs : SymCC.SymEntities} {t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.option → t = SymCC.Term.none ty ∨ ∃ (t' : SymCC.Term), t = t'.some ∧ t'.typeOf = ty

theorem Cedar.Thm.wfl_of_prim_type_is_prim {εs : SymCC.SymEntities} {t : SymCC.Term} {pty : SymCC.TermPrimType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.prim pty → ∃ (p : SymCC.TermPrim), t = SymCC.Term.prim p