Hello,
in short, in order to use a temporal-level theorem inside the proof of another one, your proof should be written as follows:
THEOREM ThmA == Spec => []A
THEOREM ThmB == Spec => []B
<1>1. Init (* /\ A *) => B
<1>2. B /\ [Next]_vars (* /\ A /\ A' *) => B'
<1>. QED BY <1>1, <1>2, ThmA, PTL DEF Spec
The commented parts indicate where you may make use of the invariant proved in ThmA.
As a rule of thumb, do not decompose temporal-level implications into ASSUME ... PROVE steps, but make sure that all hypotheses used for proving a fact that will be passed to the PTL proof method are constant level or [] formulas. The reason is that PTL will try to apply the necessitation rule F |- []F to promote any fact to a boxed formula, but it can do so only if there are no state- or action-level hypotheses in the context where that fact was established. For example, the steps <1>1 and <1>2 of your proof of SpecIInvB are established in the context of the assumption Spec, which is not a [] formula (due to the initial condition), and that's indicated by the "non-[]" warnings that you see in the proof obligation. As a result, the preservation of the invariant (step <1>2) cannot be "boxed" as it would need to be in order to apply temporal induction.
Regards,
Stephan
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/CAFteovJFJPvHyQObPEMHAgeLqydEbAdbVzqGvXBqbrgYcDAOFA%40mail.gmail.com.