theorem TLA.ProofMode.Entails_intro_forall {σ : Type u} {hyps : List (NamedPred σ)} {α : Sort v} {p : α → pred σ} : (∀ (x : α), Entails hyps (p x)) → Entails hyps [tlafml|∀ x, (p x)]

theorem TLA.ProofMode.Entails_pure_fact_intro {σ : Type u} {hyps : List (NamedPred σ)} {q : Prop} {p : pred σ} : (q → Entails hyps p) = Entails hyps [tlafml|⌞ q ⌟ → p]

theorem TLA.ProofMode.Entails_intro_temporal {σ : Type u} {hyps : List (NamedPred σ)} {goal newHyp : pred σ} (newHypName : String) : Entails (hyps ++ [{ name := newHypName, pred := newHyp }]) goal = Entails hyps [tlafml|newHyp → goal]

def TLA.ProofMode.tlaIntroCoreStep (k : Lean.SyntaxNodeKind) (name : Lean.TSyntax k) (ident? : Lean.TSyntax k → Lean.Elab.Tactic.TacticM (Option Lean.Ident)) (errorMsgPrefix : String) (tacIntroNonTemporalHyp : Lean.TSyntax k → Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic)) : Lean.Elab.Tactic.TacticM Bool

Introduce one proof-mode hypothesis with the given name.

Equations

• One or more equations did not get rendered due to their size.

def TLA.ProofMode.tlaIntroTac : Lean.ParserDescr

tla_intro x₁ x₂ ... introduces binders from the proof-mode goal.

If the goal starts with a temporal implication p → q, then tla_intro hp adds hp : p to the proof-mode context and changes the goal to q. If the goal starts with a universal quantifier, the introduced name becomes a Lean local. If the goal starts with a pure implication ⌞P⌟ → q, the introduced name is a Lean proof of P.

Examples:

tla_intro hp    -- p → q  becomes  hp : p ⊢ q
tla_intro n hp -- ∀ n, p n → q n  introduces `n`, then `hp`

Equations

• One or more equations did not get rendered due to their size.