I want to prove a meta-theorem (or induction lemma, tactic) for a specification and reuse it in other proofs, like Coq.
I wonder if its possible or not.
Consider the following spec:
----
vars == <state variables>
Act1 == ...
Act2 == ...
Next == Act1 \/ Act2
Spec == Init /\ [][Next]_vars
----
Then we expect the following lemma hold for any non-temporal formula "Invariant", and we want to use it to prove, say, its type invariance.
(I know its too simple. Actually I want to consider more complicated cases)
I was able to prove the lemma, but I could not "apply" the lemma to the type invariant theorem.
Is there anything wrong?
----
LEMMA SpecInduction ==
ASSUME
NEW Invariant,
ASSUME Init PROVE Invariant,
ASSUME Invariant, Act1 PROVE Invariant',
ASSUME Invariant, Act2 PROVE Invariant',
PROVE
Spec => []Invariant
PROOF
<1>1. Init => Invariant OBVIOUS
<1>2. Invariant /\ Next => Invariant' OBVIOUS
<1>3. Invariant /\ UNCHANGED vars => Invariant' OBVIOUS
<1> QED BY PTL, <1>1, <1>2, <1>3 DEF Spec
----