Documentation

Cedar.Thm.SymCC.Term.Interpret.Basic

Interpretation of Terms and Factory functions #

This file basic lemmas about the interpretation of terms and the Factory functions for creating terms. #

source
@[simp]
theorem Cedar.Thm.interpret_term_prim {I : SymCC.Interpretation} {p : SymCC.TermPrim} :
SymCC.Term.interpret I (SymCC.Term.prim p) = SymCC.Term.prim p
source
@[simp]
theorem Cedar.Thm.interpret_term_var {I : SymCC.Interpretation} {v : SymCC.TermVar} :
SymCC.Term.interpret I (SymCC.Term.var v) = I.vars v
source
@[simp]
theorem Cedar.Thm.interpret_term_none {I : SymCC.Interpretation} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.none ty) = SymCC.Term.none ty
source
@[simp]
theorem Cedar.Thm.interpret_term_some {I : SymCC.Interpretation} {t : SymCC.Term} :
SymCC.Term.interpret I t.some = (SymCC.Term.interpret I t).some
source
@[simp]
theorem Cedar.Thm.interpret_term_set {I : SymCC.Interpretation} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.set s ty) = SymCC.Term.set (Data.Set.map (SymCC.Term.interpret I) s) ty
source
@[simp]
theorem Cedar.Thm.interpret_term_set_empty {I : SymCC.Interpretation} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.set Data.Set.empty ty) = SymCC.Term.set Data.Set.empty ty
source
@[simp]
theorem Cedar.Thm.interpret_term_set_mk_nil {I : SymCC.Interpretation} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.set (Data.Set.mk []) ty) = SymCC.Term.set (Data.Set.mk []) ty
source
@[simp]
theorem Cedar.Thm.interpret_term_record {I : SymCC.Interpretation} {r : Data.Map Spec.Attr SymCC.Term} :
SymCC.Term.interpret I (SymCC.Term.record r) = SymCC.Term.record (Data.Map.mapOnValues (SymCC.Term.interpret I) r)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_not {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.not [t₁] ty) = SymCC.Factory.not (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_and {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.and [t₁, t₂] ty) = SymCC.Factory.and (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_or {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.or [t₁, t₂] ty) = SymCC.Factory.or (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_eq {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.eq [t₁, t₂] ty) = SymCC.Factory.eq (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ite {I : SymCC.Interpretation} {t₁ t₂ t₃ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.ite [t₁, t₂, t₃] ty) = SymCC.Factory.ite (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂) (SymCC.Term.interpret I t₃)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_uuf {I : SymCC.Interpretation} {f : SymCC.UUF} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.uuf f) [t₁] ty) = SymCC.Factory.app (SymCC.UnaryFunction.udf (I.funs f)) (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvneg {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvneg [t₁] ty) = SymCC.Factory.bvneg (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvadd {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvadd [t₁, t₂] ty) = SymCC.Factory.bvadd (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsub {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsub [t₁, t₂] ty) = SymCC.Factory.bvsub (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvmul {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvmul [t₁, t₂] ty) = SymCC.Factory.bvmul (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsdiv {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsdiv [t₁, t₂] ty) = SymCC.Factory.bvsdiv (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvudiv {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvudiv [t₁, t₂] ty) = SymCC.Factory.bvudiv (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsrem {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsrem [t₁, t₂] ty) = SymCC.Factory.bvsrem (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsmod {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsmod [t₁, t₂] ty) = SymCC.Factory.bvsmod (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvurem {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvurem [t₁, t₂] ty) = SymCC.Factory.bvurem (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvshl {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvshl [t₁, t₂] ty) = SymCC.Factory.bvshl (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvlshr {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvlshr [t₁, t₂] ty) = SymCC.Factory.bvlshr (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvnego {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvnego [t₁] ty) = SymCC.Factory.bvnego (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsaddo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsaddo [t₁, t₂] ty) = SymCC.Factory.bvsaddo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvssubo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvssubo [t₁, t₂] ty) = SymCC.Factory.bvssubo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsmulo {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsmulo [t₁, t₂] ty) = SymCC.Factory.bvsmulo (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvslt {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvslt [t₁, t₂] ty) = SymCC.Factory.bvslt (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvsle {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvsle [t₁, t₂] ty) = SymCC.Factory.bvsle (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvult {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvult [t₁, t₂] ty) = SymCC.Factory.bvult (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_bvule {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.bvule [t₁, t₂] ty) = SymCC.Factory.bvule (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_zero_extend {I : SymCC.Interpretation} {n : Nat} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.zero_extend n) [t₁] ty) = SymCC.Factory.zero_extend n (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_set_member {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.set.member [t₁, t₂] ty) = SymCC.Factory.set.member (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_set_subset {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.set.subset [t₁, t₂] ty) = SymCC.Factory.set.subset (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_set_inter {I : SymCC.Interpretation} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.set.inter [t₁, t₂] ty) = SymCC.Factory.set.inter (SymCC.Term.interpret I t₁) (SymCC.Term.interpret I t₂)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_option_get {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app SymCC.Op.option.get [t₁] ty) = SymCC.Factory.option.get' I (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_record_get {I : SymCC.Interpretation} {a : Spec.Attr} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.record.get a) [t₁] ty) = SymCC.Factory.record.get (SymCC.Term.interpret I t₁) a
source
@[simp]
theorem Cedar.Thm.interpret_term_app_string_like {I : SymCC.Interpretation} {p : Spec.Pattern} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.string.like p) [t₁] ty) = SymCC.Factory.string.like (SymCC.Term.interpret I t₁) p
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_decimal_val {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.decimal.val) [t₁] ty) = SymCC.Factory.ext.decimal.val (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_ipaddr_isV4 {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.isV4) [t₁] ty) = SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.interpret I t₁)
source
theorem Cedar.Thm.interpret_term_app_ext_ipaddr_addrV4 {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV4) [t₁] ty) = SymCC.Factory.ext.ipaddr.addrV4' I (SymCC.Term.interpret I t₁)
source
theorem Cedar.Thm.interpret_term_app_ext_ipaddr_prefixV4 {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV4) [t₁] ty) = SymCC.Factory.ext.ipaddr.prefixV4' I (SymCC.Term.interpret I t₁)
source
theorem Cedar.Thm.interpret_term_app_ext_ipaddr_addrV6 {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV6) [t₁] ty) = SymCC.Factory.ext.ipaddr.addrV6' I (SymCC.Term.interpret I t₁)
source
theorem Cedar.Thm.interpret_term_app_ext_ipaddr_prefixV6 {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV6) [t₁] ty) = SymCC.Factory.ext.ipaddr.prefixV6' I (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_datetime_val {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.datetime.val) [t₁] ty) = SymCC.Factory.ext.datetime.val (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_datetime_ofBitVec {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.datetime.ofBitVec) [t₁] ty) = SymCC.Factory.ext.datetime.ofBitVec (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_duration_val {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.duration.val) [t₁] ty) = SymCC.Factory.ext.duration.val (SymCC.Term.interpret I t₁)
source
@[simp]
theorem Cedar.Thm.interpret_term_app_ext_duration_ofBitVec {I : SymCC.Interpretation} {t₁ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.interpret I (SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.duration.ofBitVec) [t₁] ty) = SymCC.Factory.ext.duration.ofBitVec (SymCC.Term.interpret I t₁)