Hi,
I am wondering how can I prove something like this:
A large system A consists of N subsystems (B=[1..N -> Subsystem]), if each subsystem has invariant property P, a new invariant property Q of the large system A can be proved.
Take the Hour Clock (Specifying Systems, Chapter 2) for a simple example.
Here is the specification and proof of a single clock.
---------------------- MODULE HourClock ----------------------
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
--------------------------------------------------------------
THEOREM HC => []HCini
<1>1 HCini /\ [HCnxt]_hr => HCini' BY DEF HCini, HCnxt
<1> QED BY PTL, <1>1 DEF HC
==============================================================
But how can I proof:
For a larger system consists of N Hour Clocks, the maximum value M of values displayed by each clock has property M \in (1..12).
I think theorem taking parameters is need here but it isn't supported yet. So I have tried to emulate parameterized theorem by ASSUME VARIABLE var PROVE ... such as:
HCini(hr) == hr \in (1 .. 12)
HCnxt(hr) == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC(hr) == HCini(hr) /\ [][HCnxt(hr)]_hr
--------------------------------------------------------------
THEOREM T1 == ASSUME VARIABLE hr PROVE HC(hr) => []HCini(hr)
<1>1 HCini(hr) /\ [HCnxt(hr)]_hr => HCini(hr)' BY DEF HCini, HCnxt
<1> QED BY PTL, <1>1 DEF HC
VARIABLE newhr
THEOREM T2 == HC(newhr) => []HCini(newhr) BY T1 \* T2 can't be proved
In brief, I don't understand why the following THEOREM isn't OBVIOUS
THEOREM TEST == ASSUME VARIABLE A, NEW F(_),
ASSUME VARIABLE B PROVE []F(B)
PROVE []F(A