Properties of Terms

This file contains lemmas about the typeOf function on Terms.

@[simp]

theorem Cedar.Thm.typeOf_bool {b : Bool} : (SymCC.Term.prim (SymCC.TermPrim.bool b)).typeOf = SymCC.TermType.bool

@[simp]

theorem Cedar.Thm.typeOf_bv {n : Nat} {bv : BitVec n} : (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)).typeOf = SymCC.TermType.bitvec n

@[simp]

theorem Cedar.Thm.typeOf_term_none (ty : SymCC.TermType) : (SymCC.Term.none ty).typeOf = ty.option

@[simp]

theorem Cedar.Thm.typeOf_term_some {t : SymCC.Term} : t.some.typeOf = t.typeOf.option

theorem Cedar.Thm.typeOf_term_some_iff {t : SymCC.Term} {ty : SymCC.TermType} : t.typeOf = ty ↔ t.some.typeOf = ty.option

theorem Cedar.Thm.typeOf_term_prim_isPrimType (p : SymCC.TermPrim) : (SymCC.Term.prim p).typeOf.isPrimType = true

@[simp]

theorem Cedar.Thm.typeOf_term_prim_entity {uid : Spec.EntityUID} : (SymCC.Term.entity uid).typeOf = SymCC.TermType.entity uid.ty

@[simp]

theorem Cedar.Thm.typeOf_term_prim_string {s : String} : (SymCC.Term.string s).typeOf = SymCC.TermType.string

@[simp]

theorem Cedar.Thm.typeOf_term_prim_ext_decimal {d : Spec.Ext.Decimal} : (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.decimal d))).typeOf = SymCC.TermType.ext Validation.ExtType.decimal

@[simp]

theorem Cedar.Thm.typeOf_term_prim_ext_ipaddr {ip : Spec.Ext.IPAddr.IPNet} : (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr ip))).typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr

@[simp]

theorem Cedar.Thm.typeOf_term_prim_ext_datetime {d : Spec.Ext.Datetime} : (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))).typeOf = SymCC.TermType.ext Validation.ExtType.datetime

@[simp]

theorem Cedar.Thm.typeOf_term_prim_ext_duration {d : Spec.Ext.Datetime.Duration} : (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))).typeOf = SymCC.TermType.ext Validation.ExtType.duration

@[simp]

theorem Cedar.Thm.typeOf_term_var (v : SymCC.TermVar) : (SymCC.Term.var v).typeOf = v.ty

@[simp]

theorem Cedar.Thm.typeOf_term_set {elts : Data.Set SymCC.Term} {eltsTy : SymCC.TermType} : (SymCC.Term.set elts eltsTy).typeOf = eltsTy.set

@[simp]

theorem Cedar.Thm.typeOf_term_record_eq {r : Data.Map Spec.Attr SymCC.Term} : (SymCC.Term.record r).typeOf = SymCC.TermType.record (Data.Map.mapOnValues SymCC.Term.typeOf r)

theorem Cedar.Thm.typeOf_term_record_is_record_type {r : Data.Map Spec.Attr SymCC.Term} : ∃ (rty : Data.Map Spec.Attr SymCC.TermType), (SymCC.Term.record r).typeOf = SymCC.TermType.record rty

theorem Cedar.Thm.typeOf_term_record_attr_value {r : Data.Map Spec.Attr SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} {a : Spec.Attr} {ty : SymCC.TermType} (h₁ : (SymCC.Term.record r).typeOf = SymCC.TermType.record rty) (h₂ : rty.find? a = some ty) : ∃ (t : SymCC.Term), r.find? a = some t ∧ t.typeOf = ty

theorem Cedar.Thm.typeOf_term_record_attr_value_none {r : Data.Map Spec.Attr SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} {a : Spec.Attr} (h₁ : (SymCC.Term.record r).typeOf = SymCC.TermType.record rty) (h₂ : rty.find? a = none) : r.find? a = none

theorem Cedar.Thm.typeOf_term_record_attr_value_typeOf {rty : Data.Map Spec.Attr SymCC.TermType} {r : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} {t : SymCC.Term} (h₁ : (SymCC.Term.record r).typeOf = SymCC.TermType.record rty) (h₂ : r.find? a = some t) : rty.find? a = some t.typeOf

theorem Cedar.Thm.typeOf_term_record_attr_value_eq {r₁ r₂ : Data.Map Spec.Attr SymCC.Term} {rty : Data.Map Spec.Attr SymCC.TermType} {a : Spec.Attr} {t₁ t₂ : SymCC.Term} (hty₁ : (SymCC.Term.record r₁).typeOf = SymCC.TermType.record rty) (hty₂ : (SymCC.Term.record r₂).typeOf = SymCC.TermType.record rty) (ht₁ : r₁.find? a = some t₁) (ht₂ : r₂.find? a = some t₂) : t₁.typeOf = t₂.typeOf

theorem Cedar.Thm.typeOf_term_record_tail {a : Spec.Attr} {t₁ t₂ : SymCC.Term} {tl₁ tl₂ : List (Spec.Attr × SymCC.Term)} : (SymCC.Term.record (Data.Map.mk ((a, t₁) :: tl₁))).typeOf = (SymCC.Term.record (Data.Map.mk ((a, t₂) :: tl₂))).typeOf → (SymCC.Term.record (Data.Map.mk tl₁)).typeOf = (SymCC.Term.record (Data.Map.mk tl₂)).typeOf

@[simp]

theorem Cedar.Thm.typeOf_term_app {ty : SymCC.TermType} {op : SymCC.Op} {args : List SymCC.Term} : (SymCC.Term.app op args ty).typeOf = ty

theorem Cedar.Thm.typeOf_wf_term_is_wf {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormed εs t → SymCC.TermType.WellFormed εs t.typeOf

theorem Cedar.Thm.wfp_term_implies_wf_ty {εs : SymCC.SymEntities} {t : SymCC.Term} (h : SymCC.Term.WellFormedPartialApp εs t) : SymCC.TermType.WellFormed εs t.typeOf

theorem Cedar.Thm.typeOf_option_wf_terms_is_wf {εs : SymCC.SymEntities} {hd : SymCC.Term} {tl ts : List SymCC.Term} {ty : SymCC.TermType} : ts = hd :: tl → (∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t) → (∀ (t : SymCC.Term), t ∈ ts → t.typeOf = ty.option) → SymCC.TermType.WellFormed εs ty

theorem Cedar.Thm.typeOf_term_record_cedarType?_some_implies_attr_cedarType?_some {a : Spec.Attr} {t : SymCC.Term} {r : Data.Map Spec.Attr SymCC.Term} {ty : Validation.CedarType} : r.WellFormed → (SymCC.Term.record r).typeOf.cedarType? = some ty → (a, t) ∈ r.toList → ∃ (tty : SymCC.TermType), ∃ (cty : Validation.CedarType), tty.cedarType? = some cty ∧ (t.typeOf = tty ∨ t.typeOf = tty.option)

theorem Cedar.Thm.isPrimType_implies_prim_type {ty : SymCC.TermType} : ty.isPrimType = true → ∃ (pty : SymCC.TermPrimType), ty = SymCC.TermType.prim pty

theorem Cedar.Thm.isEntityType_implies_entity_type {ty : SymCC.TermType} : ty.isEntityType = true → ∃ (ety : Spec.EntityType), ty = SymCC.TermType.entity ety

theorem Cedar.Thm.isOptionEntityType_implies_option_entity_type {ty : SymCC.TermType} : ty.isOptionEntityType = true → ∃ (ety : Spec.EntityType), ty = (SymCC.TermType.entity ety).option

theorem Cedar.Thm.typeOf_ifSome_option {g t : SymCC.Term} {ty : SymCC.TermType} : t.typeOf = ty.option → (SymCC.Factory.ifSome g t).typeOf = ty.option

theorem Cedar.Thm.typeOf_ifAllSome_option_type {gs : List SymCC.Term} {t : SymCC.Term} {ty : SymCC.TermType} : t.typeOf = ty.option → (SymCC.Factory.ifAllSome gs t).typeOf = ty.option