theorem
TLA.ProofMode.Entails_apply_hyp
{σ : Type u}
{hyps : List (NamedPred σ)}
{goal : pred σ}
(hs : List (pred σ))
(h : Option.map NamedPred.pred hyps.getLast? = some (repeatedImplies hs goal))
:
Entails hyps.dropLast (repeatedAnd hs) → Entails hyps goal
theorem
TLA.ProofMode.Entails_apply_hyp_closing_goal
{σ : Type u}
{hyps : List (NamedPred σ)}
{goal : pred σ}
(h : Option.map NamedPred.pred hyps.getLast? = some goal)
:
Entails hyps goal
tla_apply t proves the current proof-mode goal using a TLA theorem or a
temporal hypothesis. If the theorem concludes the current goal but still has
unsupplied temporal premises, those premises become new proof-mode goals.
For example, if the context contains hp : p and the goal is q, then
tla_apply h hp closes the goal when h proves p |-tla- q:
tla_apply lemma hp
If the goal is r and lemma hp has type q |-tla- r, then
tla_apply lemma hp
changes the goal to q.
Equations
- One or more equations did not get rendered due to their size.