Basic properties of partial evaluation of terms

This file proves basic lemmas about the Factory functions on terms when applied to literal (concrete) inputs.

PE for Factory.not

@[simp]

theorem Cedar.Thm.pe_not_true : SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool true)) = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_not_false : SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool false)) = SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.pe_not_lit {b : Bool} : SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool b)) = SymCC.Term.prim (SymCC.TermPrim.bool !b)

theorem Cedar.Thm.pe_not_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bool → (SymCC.Factory.not t).isLiteral = true

PE for Factory.and

theorem Cedar.Thm.pe_and_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bool → (SymCC.Factory.and t₁ t₂).isLiteral = true

@[simp]

theorem Cedar.Thm.pe_and_false_left {t : SymCC.Term} : SymCC.Factory.and (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_and_false_right {t : SymCC.Term} : SymCC.Factory.and t (SymCC.Term.prim (SymCC.TermPrim.bool false)) = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_and_true_left {t : SymCC.Term} : SymCC.Factory.and (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t

@[simp]

theorem Cedar.Thm.pe_and_true_right {t : SymCC.Term} : SymCC.Factory.and t (SymCC.Term.prim (SymCC.TermPrim.bool true)) = t

@[simp]

theorem Cedar.Thm.pe_and_true_iff_true {t₁ t₂ : SymCC.Term} : SymCC.Factory.and t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool true) ↔ t₁ = SymCC.Term.prim (SymCC.TermPrim.bool true) ∧ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool true)

PE for Factory.or

theorem Cedar.Thm.pe_or_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bool → (SymCC.Factory.or t₁ t₂).isLiteral = true

@[simp]

theorem Cedar.Thm.pe_or_true_left {t : SymCC.Term} : SymCC.Factory.or (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_or_true_right {t : SymCC.Term} : SymCC.Factory.or t (SymCC.Term.prim (SymCC.TermPrim.bool true)) = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_or_false_left {t : SymCC.Term} : SymCC.Factory.or (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = t

@[simp]

theorem Cedar.Thm.pe_or_false_right {t : SymCC.Term} : SymCC.Factory.or t (SymCC.Term.prim (SymCC.TermPrim.bool false)) = t

theorem Cedar.Thm.pe_or_bool {a b : Bool} : SymCC.Factory.or (SymCC.Term.prim (SymCC.TermPrim.bool a)) (SymCC.Term.prim (SymCC.TermPrim.bool b)) = SymCC.Term.prim (SymCC.TermPrim.bool (a || b))

theorem Cedar.Thm.pe_foldl_or {α : Type u_1} (g : α → Bool) (mk : α → SymCC.Term) (st : SymCC.Term → SymCC.Term) (l : List α) (hstep : ∀ (a : α), st (mk a) = SymCC.Term.prim (SymCC.TermPrim.bool (g a))) (s : Bool) : List.foldl (fun (acc t₂ : SymCC.Term) => SymCC.Factory.or acc (st t₂)) (SymCC.Term.prim (SymCC.TermPrim.bool s)) (List.map mk l) = SymCC.Term.prim (SymCC.TermPrim.bool (s || l.any g))

Left-folding Factory.or over a mapped list, where each element reduces (via hstep) to a boolean literal, yields the boolean literal of the disjunction accumulated over the list (List.any).

PE for Factory.implies

@[simp]

theorem Cedar.Thm.pe_implies_false_left {t : SymCC.Term} : SymCC.Factory.implies (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_implies_true_left {t : SymCC.Term} : SymCC.Factory.implies (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t

PE for Factory.ite

@[simp]

theorem Cedar.Thm.pe_ite_true {t₁ t₂ : SymCC.Term} : SymCC.Factory.ite (SymCC.Term.prim (SymCC.TermPrim.bool true)) t₁ t₂ = t₁

@[simp]

theorem Cedar.Thm.pe_ite_false {t₁ t₂ : SymCC.Term} : SymCC.Factory.ite (SymCC.Term.prim (SymCC.TermPrim.bool false)) t₁ t₂ = t₂

theorem Cedar.Thm.pe_ite_wfl {εs : SymCC.SymEntities} {t₁ t₂ t₃ : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t₁ → SymCC.Term.WellFormedLiteral εs t₂ → SymCC.Term.WellFormedLiteral εs t₃ → t₁.typeOf = SymCC.TermType.bool → (SymCC.Factory.ite t₁ t₂ t₃).isLiteral = true

PE for Factory.eq

theorem Cedar.Thm.pe_eq_simplify_same {t : SymCC.Term} : SymCC.Factory.eq.simplify t t = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_eq_same {t : SymCC.Term} : SymCC.Factory.eq t t = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_eq_some_none {t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Factory.eq t.some (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_eq_none_some {t : SymCC.Term} {ty : SymCC.TermType} : SymCC.Factory.eq (SymCC.Term.none ty) t.some = SymCC.Term.prim (SymCC.TermPrim.bool false)

theorem Cedar.Thm.pe_eq_some_some {t₁ t₂ : SymCC.Term} : SymCC.Factory.eq t₁.some t₂.some = SymCC.Factory.eq.simplify t₁ t₂

@[simp]

theorem Cedar.Thm.pe_eq_simplify_lit {t₁ t₂ : SymCC.Term} : t₁.isLiteral = true → t₂.isLiteral = true → (SymCC.Factory.eq.simplify t₁ t₂).isLiteral = true ∧ SymCC.Factory.eq.simplify t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool (t₁ == t₂))

theorem Cedar.Thm.pe_eq_lit {t₁ t₂ : SymCC.Term} : t₁.isLiteral = true → t₂.isLiteral = true → (SymCC.Factory.eq t₁ t₂).isLiteral = true ∧ SymCC.Factory.eq t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool (t₁ == t₂))

theorem Cedar.Thm.pe_eq_prim {p₁ p₂ : SymCC.TermPrim} : SymCC.Factory.eq (SymCC.Term.prim p₁) (SymCC.Term.prim p₂) = SymCC.Term.prim (SymCC.TermPrim.bool (p₁ == p₂))

PE for Factory.option.get and Factory.option.get'

@[simp]

theorem Cedar.Thm.pe_option_get_some {t : SymCC.Term} : SymCC.Factory.option.get t.some = t

@[simp]

theorem Cedar.Thm.pe_option_get'_some {I : SymCC.Interpretation} {t : SymCC.Term} : SymCC.Factory.option.get' I t.some = t

theorem Cedar.Thm.pe_option_get'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.option → (SymCC.Factory.option.get' I t).isLiteral = true

PE for Factory.isNone and Factory.isSome

@[simp]

theorem Cedar.Thm.pe_isNone_none {ty : SymCC.TermType} : SymCC.Factory.isNone (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_isNone_some {t : SymCC.Term} : SymCC.Factory.isNone t.some = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_isSome_none {ty : SymCC.TermType} : SymCC.Factory.isSome (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_isSome_some {t : SymCC.Term} : SymCC.Factory.isSome t.some = SymCC.Term.prim (SymCC.TermPrim.bool true)

PE for Factory.ifSome

theorem Cedar.Thm.pe_ifSome_none {t : SymCC.Term} {gty tty : SymCC.TermType} : t.typeOf = tty.option → SymCC.Factory.ifSome (SymCC.Term.none gty) t = SymCC.Term.none tty

theorem Cedar.Thm.pe_ifSome_some {g t : SymCC.Term} {tty : SymCC.TermType} : t.typeOf = tty.option → SymCC.Factory.ifSome g.some t = t

theorem Cedar.Thm.pe_ifSome_none_body {g : SymCC.Term} {ty : SymCC.TermType} : SymCC.Factory.ifSome g (SymCC.Term.none ty) = SymCC.Term.none ty

ifSome with a none body always reduces to that none.

theorem Cedar.Thm.pe_foldr_ifSome_all_some {l : List SymCC.Term} {P : SymCC.Term} {ty : SymCC.TermType} (hP : P.typeOf = ty.option) (hall : ∀ (t : SymCC.Term), t ∈ l → ∃ (g : SymCC.Term), t = g.some) : List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) P l = P

If every guard is a some, folding ifSome collapses to the body.

theorem Cedar.Thm.pe_ifSome_get_eq_get' {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t : SymCC.Term} {ty ty' : SymCC.TermType} (f : SymCC.Term → SymCC.Term) : SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.option → (f (SymCC.Factory.option.get t)).typeOf = ty'.option → (f (SymCC.Factory.option.get' I t)).typeOf = ty'.option → SymCC.Factory.ifSome t (f (SymCC.Factory.option.get t)) = SymCC.Factory.ifSome t (f (SymCC.Factory.option.get' I t))

theorem Cedar.Thm.pe_ifSome_get_eq_get'₂ {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ : SymCC.Term} {ty₁ ty₂ ty₃ : SymCC.TermType} (f : SymCC.Term → SymCC.Term → SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hwφ₂ : SymCC.Term.WellFormedLiteral εs t₂ ∧ t₂.typeOf = ty₂.option) (hty₁ : (f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).typeOf = ty₃.option) (hty₂ : (f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂)).typeOf = ty₃.option) : SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂))) = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂)))

theorem Cedar.Thm.pe_foldr_ifSome_get_eq_get' {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {ty : SymCC.TermType} (gs : List SymCC.Term) (F : List SymCC.Term → SymCC.Term) : (∀ (g : SymCC.Term), g ∈ gs → SymCC.Term.WellFormedLiteral εs g ∧ ∃ (ty' : SymCC.TermType), g.typeOf = ty'.option) → (F (List.map SymCC.Factory.option.get gs)).typeOf = ty.option → (F (List.map (SymCC.Factory.option.get' I) gs)).typeOf = ty.option → List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) (F (List.map SymCC.Factory.option.get gs)) gs = List.foldr (fun (tᵢ acc : SymCC.Term) => SymCC.Factory.ifSome tᵢ acc) (F (List.map (SymCC.Factory.option.get' I) gs)) gs

Under a foldr ifSome over well-formed-literal option guards, replacing option.get of each guard with option.get' I leaves the folded term unchanged (when a guard is none both sides collapse to none; when all guards are some the two gets agree).

theorem Cedar.Thm.pe_ifSome_ok_get_eq_get' {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ t₃ : SymCC.Term} {ty₁ ty₂ : SymCC.TermType} (f : SymCC.Term → SymCC.Result SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hty₂ : t₂.typeOf = ty₂.option) (hty₃ : t₃.typeOf = ty₂.option) (hok₂ : f (SymCC.Factory.option.get' I t₁) = Except.ok t₂) (hok₃ : f (SymCC.Factory.option.get t₁) = Except.ok t₃) : SymCC.Factory.ifSome t₁ t₃ = SymCC.Factory.ifSome t₁ t₂

theorem Cedar.Thm.pe_ifSome_ok_get_eq_get'₂ {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ t₃ t₄ : SymCC.Term} {ty₁ ty₂ ty₃ : SymCC.TermType} (f : SymCC.Term → SymCC.Term → SymCC.Result SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hwφ₂ : SymCC.Term.WellFormedLiteral εs t₂ ∧ t₂.typeOf = ty₂.option) (hty₃ : t₃.typeOf = ty₃.option) (hty₄ : t₄.typeOf = ty₃.option) (hok₃ : f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂) = Except.ok t₃) (hok₄ : f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂) = Except.ok t₄) : SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ t₄) = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ t₃)

PE for Factory.anyNone and Factory.ifAllSome

theorem Cedar.Thm.pe_wfls_of_type_option {εs : SymCC.SymEntities} {ts : List SymCC.Term} (hwφ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormedLiteral εs t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option) : (∃ (ty : SymCC.TermType), SymCC.Term.none ty ∈ ts) ∨ ∃ (ts' : List SymCC.Term), ts = List.map SymCC.Term.some ts'

theorem Cedar.Thm.pe_anyTrue_true {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} {t : SymCC.Term} : t ∈ ts → f t = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.anyTrue f ts = SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.pe_anyTrue_false {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} : (∀ (t : SymCC.Term), t ∈ ts → f t = SymCC.Term.prim (SymCC.TermPrim.bool false)) → SymCC.Factory.anyTrue f ts = SymCC.Term.prim (SymCC.TermPrim.bool false)

theorem Cedar.Thm.pe_anyNone_true {ts : List SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.none ty ∈ ts → SymCC.Factory.anyNone ts = SymCC.Term.prim (SymCC.TermPrim.bool true)

theorem Cedar.Thm.pe_anyNone_false {ts : List SymCC.Term} : SymCC.Factory.anyNone (List.map SymCC.Term.some ts) = SymCC.Term.prim (SymCC.TermPrim.bool false)

theorem Cedar.Thm.pe_ifAllSome_none {ts : List SymCC.Term} {t : SymCC.Term} {ty₁ ty₂ : SymCC.TermType} : SymCC.Term.none ty₁ ∈ ts → t.typeOf = ty₂.option → SymCC.Factory.ifAllSome ts t = SymCC.Term.none ty₂

theorem Cedar.Thm.pe_ifAllSome_some {ts : List SymCC.Term} {t : SymCC.Term} {ty : SymCC.TermType} : t.typeOf = ty.option → SymCC.Factory.ifAllSome (List.map SymCC.Term.some ts) t = t

PE for Factory.ifFalse and Factory.ifTrue

@[simp]

theorem Cedar.Thm.pe_ifFalse_true {t : SymCC.Term} : SymCC.Factory.ifFalse (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = SymCC.Term.none t.typeOf

@[simp]

theorem Cedar.Thm.pe_ifFalse_false {t : SymCC.Term} : SymCC.Factory.ifFalse (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = t.some

@[simp]

theorem Cedar.Thm.pe_ifTrue_true {t : SymCC.Term} : SymCC.Factory.ifTrue (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t.some

@[simp]

theorem Cedar.Thm.pe_ifTrue_false {t : SymCC.Term} : SymCC.Factory.ifTrue (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.none t.typeOf

PE for Factory.app

theorem Cedar.Thm.pe_app_wfl {εs : SymCC.SymEntities} {f : SymCC.UDF} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → SymCC.UDF.WellFormed εs f → (SymCC.Factory.app (SymCC.UnaryFunction.udf f) t).isLiteral = true

PE for Factory bitvector operators

theorem Cedar.Thm.pe_bvneg_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvneg t).isLiteral = true

theorem Cedar.Thm.pe_bvnego_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvnego t).isLiteral = true

theorem Cedar.Thm.pe_zero_extend_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n m : Nat} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec m → (SymCC.Factory.zero_extend n t).isLiteral = true

theorem Cedar.Thm.pe_bvadd_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvadd t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsub_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsub t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvmul_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvmul t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsdiv_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsdiv t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvudiv_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvudiv t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsrem_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsrem t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsmod_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsmod t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvurem_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvurem t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvshl_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvshl t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvlshr_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvlshr t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvslt_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvslt t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsle_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsle t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvult_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvult t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvule_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvule t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsaddo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsaddo t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvssubo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvssubo t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsmulo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsmulo t₁ t₂).isLiteral = true

@[simp]

theorem Cedar.Thm.pe_bvadd {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvadd (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.add bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsub {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsub (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.sub bv₂))

@[simp]

theorem Cedar.Thm.pe_bvmul {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvmul (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.mul bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsdiv {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsdiv (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smtSDiv bv₂))

@[simp]

theorem Cedar.Thm.pe_bvudiv {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvudiv (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smtUDiv bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsrem {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsrem (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.srem bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsmod {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsmod (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smod bv₂))

@[simp]

theorem Cedar.Thm.pe_bvurem {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvurem (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.umod bv₂))

@[simp]

theorem Cedar.Thm.pe_bvlshr {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvlshr (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁ >>> bv₂))

@[simp]

theorem Cedar.Thm.pe_bvshl {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvshl (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁ <<< bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsaddo {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt + bv₂.toInt)))

@[simp]

theorem Cedar.Thm.pe_bvssubo {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt - bv₂.toInt)))

@[simp]

theorem Cedar.Thm.pe_bvsmulo {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt * bv₂.toInt)))

theorem Cedar.Thm.pe_zero_extend {k n : Nat} {bv : BitVec k} : k ≤ n → SymCC.Factory.zero_extend (n - k) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (BitVec.zeroExtend n bv))

@[simp]

theorem Cedar.Thm.pe_bvslt {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvslt (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.slt bv₂))

@[simp]

theorem Cedar.Thm.pe_bvsle {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsle (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.sle bv₂))

@[simp]

theorem Cedar.Thm.pe_bvule {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvule (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.ule bv₂))

theorem Cedar.Thm.pe_bvaddChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvaddChecked t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvsubChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsubChecked t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvmulChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvmulChecked t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_bvaddChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvaddChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))

theorem Cedar.Thm.pe_bvaddChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvaddChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.add bv₂))).some

theorem Cedar.Thm.pe_bvsubChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvsubChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))

theorem Cedar.Thm.pe_bvsubChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvsubChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.sub bv₂))).some

theorem Cedar.Thm.pe_bvmulChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvmulChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))

theorem Cedar.Thm.pe_bvmulChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} : SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvmulChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.mul bv₂))).some

PE for Factory string, set, and record operators

theorem Cedar.Thm.pe_string_like_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {p : Spec.Pattern} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.string → (SymCC.Factory.string.like t p).isLiteral = true

@[simp]

theorem Cedar.Thm.pe_set_isEmpty {s : Data.Set SymCC.Term} {ty : SymCC.TermType} : SymCC.Factory.set.isEmpty (SymCC.Term.set s ty) = SymCC.Term.prim (SymCC.TermPrim.bool s.isEmpty)

theorem Cedar.Thm.pe_set_member {t : SymCC.Term} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set s ty).isLiteral = true → t.isLiteral = true → SymCC.Factory.set.member t (SymCC.Term.set s ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s.contains t))

theorem Cedar.Thm.pe_set_member_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t₁ → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.member t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_set_subset {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.subset (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s₁.subset s₂))

theorem Cedar.Thm.pe_set_subset_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = ty.set → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.subset t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_set_inter_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = ty.set → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.inter t₁ t₂).isLiteral = true

theorem Cedar.Thm.pe_set_inter {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.inter (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.set (s₁.intersect s₂) ty

theorem Cedar.Thm.pe_set_intersects {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} : (SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.intersects (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s₁.intersects s₂))

theorem Cedar.Thm.pe_record_get_wfl {εs : SymCC.SymEntities} {a : Spec.Attr} {t : SymCC.Term} {ty : SymCC.TermType} {rty : Data.Map Spec.Attr SymCC.TermType} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.record rty → rty.find? a = some ty → (SymCC.Factory.record.get t a).isLiteral = true

theorem Cedar.Thm.pe_record_get {rt : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} {tₐ : SymCC.Term} : rt.find? a = some tₐ → SymCC.Factory.record.get (SymCC.Term.record rt) a = tₐ

PE for Factory extension operators

theorem Cedar.Thm.pe_ext_decimal_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.decimal → (SymCC.Factory.ext.decimal.val t).isLiteral = true

theorem Cedar.Thm.pe_ext_ipaddr_isV4_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.isV4 t).isLiteral = true

theorem Cedar.Thm.pe_ext_ipaddr_addrV4'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.addrV4' I t).isLiteral = true

theorem Cedar.Thm.pe_ext_ipaddr_prefixV4'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.prefixV4' I t).isLiteral = true

theorem Cedar.Thm.pe_ext_ipaddr_addrV6'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.addrV6' I t).isLiteral = true

theorem Cedar.Thm.pe_ext_ipaddr_prefixV6'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.prefixV6' I t).isLiteral = true

theorem Cedar.Thm.pe_ext_datetime_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime → (SymCC.Factory.ext.datetime.val t).isLiteral = true

theorem Cedar.Thm.pe_ext_datetime_ofBitVec_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64) → (SymCC.Factory.ext.datetime.ofBitVec t).isLiteral = true

theorem Cedar.Thm.pe_ext_duration_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.duration → (SymCC.Factory.ext.duration.val t).isLiteral = true

theorem Cedar.Thm.pe_ext_duration_ofBitVec_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} : SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64) → (SymCC.Factory.ext.duration.ofBitVec t).isLiteral = true

@[simp]

theorem Cedar.Thm.pe_ext_decimal_val {d : Spec.Ext.Decimal} : SymCC.Factory.ext.decimal.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.decimal d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec (Int64.toBitVec d))

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_isV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} : SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bool true)

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_isV4_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} : SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bool false)

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_addrV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} : SymCC.Factory.ext.ipaddr.addrV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bitvec cidr.addr)

theorem Cedar.Thm.pe_ext_ipaddr_addrV4'_V4 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} : SymCC.Factory.ext.ipaddr.addrV4' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Factory.ext.ipaddr.addrV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr))))

def Cedar.Thm.cidrPrefixTerm {w : Nat} (cidr : Spec.Ext.IPAddr.CIDR w) : SymCC.Term

Equations

• Cedar.Thm.cidrPrefixTerm cidr = match cidr.pre with | none => Cedar.SymCC.Term.none (Cedar.SymCC.TermType.bitvec w) | some pre => (Cedar.SymCC.Term.prim (Cedar.SymCC.TermPrim.bitvec pre)).some

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_prefixV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} : SymCC.Factory.ext.ipaddr.prefixV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = cidrPrefixTerm cidr

theorem Cedar.Thm.pe_ext_ipaddr_prefixV4'_V4 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} : SymCC.Factory.ext.ipaddr.prefixV4' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Factory.ext.ipaddr.prefixV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr))))

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_addrV6_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} : SymCC.Factory.ext.ipaddr.addrV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bitvec cidr.addr)

theorem Cedar.Thm.pe_ext_ipaddr_addrV6'_V6 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} : SymCC.Factory.ext.ipaddr.addrV6' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Factory.ext.ipaddr.addrV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr))))

@[simp]

theorem Cedar.Thm.pe_ext_ipaddr_prefixV6_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} : SymCC.Factory.ext.ipaddr.prefixV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = cidrPrefixTerm cidr

theorem Cedar.Thm.pe_ext_ipaddr_prefixV6'_V6 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} : SymCC.Factory.ext.ipaddr.prefixV6' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Factory.ext.ipaddr.prefixV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr))))

@[simp]

theorem Cedar.Thm.pe_ext_datetime_val {d : Spec.Ext.Datetime} : SymCC.Factory.ext.datetime.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec d.val.toBitVec)

@[simp]

theorem Cedar.Thm.pe_ext_datetime_ofBitVec {bv : BitVec 64} : SymCC.Factory.ext.datetime.ofBitVec (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime { val := Int64.ofInt bv.toInt }))

@[simp]

theorem Cedar.Thm.pe_ext_duration_val {d : Spec.Ext.Datetime.Duration} : SymCC.Factory.ext.duration.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec d.val.toBitVec)

@[simp]

theorem Cedar.Thm.pe_ext_duration_ofBitVec {bv : BitVec 64} : SymCC.Factory.ext.duration.ofBitVec (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration { val := Int64.ofInt bv.toInt }))