Interpretation preserves well-formedness of Terms #
This file proves that interpretation preserves well-formedness: interpreting a well-formed term of a given type produces a well-formed term of the same type. #
def
Cedar.Thm.InterpretTermWF
(εs : SymCC.SymEntities)
(I : SymCC.Interpretation)
(t : SymCC.Term)
:
Equations
- Cedar.Thm.InterpretTermWF εs I t = (Cedar.SymCC.Term.WellFormed εs (Cedar.SymCC.Term.interpret I t) ∧ (Cedar.SymCC.Term.interpret I t).typeOf = t.typeOf)
Instances For
theorem
Cedar.Thm.interpret_term_prim_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{p : SymCC.TermPrim}
(h : SymCC.Term.WellFormed εs (SymCC.Term.prim p))
:
InterpretTermWF εs I (SymCC.Term.prim p)
theorem
Cedar.Thm.interpret_term_var_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{v : SymCC.TermVar}
(h₁ : I.WellFormed εs)
(h₂ : SymCC.Term.WellFormed εs (SymCC.Term.var v))
:
InterpretTermWF εs I (SymCC.Term.var v)
theorem
Cedar.Thm.interpret_term_none_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{ty : SymCC.TermType}
(h : SymCC.Term.WellFormed εs (SymCC.Term.none ty))
:
InterpretTermWF εs I (SymCC.Term.none ty)
theorem
Cedar.Thm.interpret_term_some_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(ih : InterpretTermWF εs I t)
:
InterpretTermWF εs I t.some
theorem
Cedar.Thm.interpret_term_set_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{s : Data.Set SymCC.Term}
{ty : SymCC.TermType}
(h₁ : SymCC.Term.WellFormed εs (SymCC.Term.set s ty))
(ih : ∀ (t : SymCC.Term), t ∈ s → InterpretTermWF εs I t)
:
InterpretTermWF εs I (SymCC.Term.set s ty)
theorem
Cedar.Thm.interpret_term_record_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{r : Data.Map Spec.Attr SymCC.Term}
(h₁ : SymCC.Term.WellFormed εs (SymCC.Term.record r))
(ih : ∀ (a : Spec.Attr) (t : SymCC.Term), (a, t) ∈ r.toList → InterpretTermWF εs I t)
:
InterpretTermWF εs I (SymCC.Term.record r)
theorem
Cedar.Thm.interpret_term_app_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{op : SymCC.Op}
{ts : List SymCC.Term}
{ty : SymCC.TermType}
(h₀ : I.WellFormed εs)
(h₁ : SymCC.Term.WellFormed εs (SymCC.Term.app op ts ty))
(ih : ∀ (t : SymCC.Term), t ∈ ts → InterpretTermWF εs I t)
:
InterpretTermWF εs I (SymCC.Term.app op ts ty)
@[irreducible]
theorem
Cedar.Thm.interpret_term_wf
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : I.WellFormed εs)
(h₂ : SymCC.Term.WellFormed εs t)
:
theorem
Cedar.Thm.interpret_term_isEntityType
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : I.WellFormed εs)
(h₂ : SymCC.Term.WellFormed εs t)
:
theorem
Cedar.Thm.interpret_term_isRecordType
{εs : SymCC.SymEntities}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(h₁ : I.WellFormed εs)
(h₂ : SymCC.Term.WellFormed εs t)
: