def TLA.ProofMode.mapHypPreds {σ : Type u} (f : pred σ → pred σ) (hyps : List (NamedPred σ)) : List (NamedPred σ)

Map a function over the predicates of a hypothesis list.

Equations

• TLA.ProofMode.mapHypPreds f hyps = List.map (fun (h : TLA.ProofMode.NamedPred σ) => { name := h.name, pred := f h.pred }) hyps

theorem TLA.ProofMode.mapHypPreds_preds {σ : Type u} (f : pred σ → pred σ) (hyps : List (NamedPred σ)) : List.map NamedPred.pred (mapHypPreds f hyps) = List.map f (List.map NamedPred.pred hyps)

theorem TLA.ProofMode.repeatedAnd_map_later {σ : Type u} (ps : List (pred σ)) : ((repeatedAnd (List.map later ps))) =tla= (◯(repeatedAnd ps))

theorem TLA.ProofMode.repeatedAnd_map_always {σ : Type u} (ps : List (pred σ)) : ((repeatedAnd (List.map always ps))) =tla= (□(repeatedAnd ps))

theorem TLA.ProofMode.repeatedAnd_map_eventually_always {σ : Type u} (ps : List (pred σ)) : ((repeatedAnd (List.map (fun (p : pred σ) => [tlafml|◇□p]) ps))) =tla= (◇□(repeatedAnd ps))

theorem TLA.ProofMode.Entails_later_monotone {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} : Entails hyps goal → Entails (mapHypPreds later hyps) [tlafml|◯goal]

theorem TLA.ProofMode.Entails_always_monotone {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} : Entails hyps goal → Entails (mapHypPreds always hyps) [tlafml|□goal]

theorem TLA.ProofMode.Entails_eventually_always_monotone {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} : Entails hyps goal → Entails (mapHypPreds (fun (p : pred σ) => [tlafml|◇□p]) hyps) [tlafml|◇□goal]

theorem TLA.ProofMode.Entails_eventually_monotone_single {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} {name : String} {p : pred σ} (h : hyps = [{ name := name, pred := p }]) : Entails hyps goal → Entails (mapHypPreds eventually hyps) [tlafml|◇goal]

theorem TLA.ProofMode.Entails_always_eventually_monotone_single {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} {name : String} {p : pred σ} (h : hyps = [{ name := name, pred := p }]) : Entails hyps goal → Entails (mapHypPreds (fun (p : pred σ) => [tlafml|□◇p]) hyps) [tlafml|□◇goal]

def TLA.ProofMode.tlaMonotoneTac : Lean.ParserDescr

tla_monotone removes a common monotone temporal prefix from the proof-mode context and goal.

For example, if every temporal hypothesis and the goal are prefixed by □, then

tla_monotone

turns a context such as hp : □ p, hq : □ q with goal □ r into hp : p, hq : q with goal r.

It also supports ◯ and ◇□ over multiple hypotheses, and the single-hypothesis cases for ◇ and □◇. Outside proof mode it applies the corresponding raw monotonicity theorem:

tla_monotone

changes a raw goal □ p |-tla- □ q to p |-tla- q.

Equations

• TLA.ProofMode.tlaMonotoneTac = Lean.ParserDescr.node `TLA.ProofMode.tlaMonotoneTac 1024 (Lean.ParserDescr.nonReservedSymbol "tla_monotone" false)