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

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

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

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

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

theorem TLA.ProofMode.Entails_duplicate_one_hyp_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (newHypName : String) {newHyp : pred σ} (oldHypName : String) (hpred : List.find? (fun (h : NamedPred σ) => h.name == oldHypName) hyps = some { name := oldHypName, pred := newHyp }) : Entails (hyps ++ [{ name := newHypName, pred := newHyp }]) goal → Entails hyps goal

def TLA.ProofMode.tlaHaveTerm (newHypName : String) (tm : Lean.Term) : Lean.Elab.Tactic.TacticM Nat

Introduce a new proof-mode hypothesis proved by the given term.

Equations

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

def TLA.ProofMode.tlaHaveTerm.specializeByIdx (idx : Nat) (args : Array Lean.Term) : Lean.Elab.Tactic.TacticM Unit

Specialize the hypothesis at the given index with the supplied arguments.

Equations

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

def Lean.Parser.Category.tlaHaveClause : Category

Syntax category for the clause of a tla_have.

Equations

• Lean.Parser.Category.tlaHaveClause = { }

def TLA.ProofMode.tlaHaveClause.quot : Lean.ParserDescr

Equations

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

def TLA.ProofMode.«tlaHaveClause:_By_» : Lean.ParserDescr

A tla_have clause stating a formula proved by a tactic block.

Equations

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

def TLA.ProofMode.«tlaHaveClause:=_» : Lean.ParserDescr

A tla_have clause assigning a term.

Equations

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

def TLA.ProofMode.tlaHaveTac : Lean.ParserDescr

tla_have h : p by tac adds a new temporal hypothesis h : p to the proof-mode context, after tac proves p from the current context.

For example, if the current context can prove p, then

tla_have hp : p by
  exact pred_implies_refl _

adds hp : p to the proof-mode context and returns to the original goal.

tla_have h := t adds the temporal fact obtained from t. For example,

tla_have hq := lemma hp

adds the result of applying lemma to the temporal hypothesis hp.

Equations

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

def TLA.ProofMode.tlaHaveAnonTac : Lean.ParserDescr

tla_have := t adds the temporal fact obtained from t under the default proof-mode name "this".

For example,

tla_have := lemma hp

adds a new hypothesis named this containing the result of lemma hp.

Equations

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

def TLA.ProofMode.tlaReplaceTac : Lean.ParserDescr

tla_replace h := t replaces the named proof-mode hypothesis h by the temporal fact obtained from t.

For example, if hp : p and lem : (p) |-tla- (q), then

tla_replace hp := lem hp

removes hp : p and adds hp : q. The replacement is appended at the end of the proof-mode context, as if tla_have, tla_clear, and tla_rename had been used in sequence.

Equations

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

def TLA.ProofMode.tlaSufficesTac : Lean.ParserDescr

tla_suffices h : p by tac changes the main goal to proving p. The block tac must show that the original goal follows after adding h : p to the proof-mode context.

For example,

tla_suffices h : p ∧ q by
  tla_rcases h with ⟨hp, hq⟩

leaves the new main goal p ∧ q; inside the by block, the original goal is available with an extra temporal hypothesis h : p ∧ q.

Equations

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