Interpretation preserves well-formedness of Terms #
This file proves that interpretation produces literals that preserve well-formedness: interpreting a well-formed term of a given type produces a well-formed literal term of the same type. It also proves that interpreting a well-formed literal produces that same literal. #
@[irreducible]
theorem
Cedar.Thm.interpret_term_lit_id
{εs : SymCC.SymEntities}
(I : SymCC.Interpretation)
{t : SymCC.Term}
(h₁ : SymCC.Term.WellFormedLiteral εs t)
:
theorem
Cedar.Thm.interpret_term_lit
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₀ : I.WellFormed εs)
(h₁ : SymCC.Term.WellFormed εs t)
:
theorem
Cedar.Thm.interpret_term_wfl
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : I.WellFormed εs)
(h₂ : SymCC.Term.WellFormed εs t)
:
SymCC.Term.WellFormedLiteral εs (SymCC.Term.interpret I t) ∧ (SymCC.Term.interpret I t).typeOf = t.typeOf