------------------------------- MODULE MinMax1 ------------------------------
EXTENDS Integers, TLAPS, FiniteSetTheorems
setMax(S) == CHOOSE t \in S : \A s \in S : t >= s
setMin(S) == CHOOSE t \in S : \A s \in S : t =< s
CONSTANTS Lo, Hi, Both, None
ASSUME Assumption == {Lo, Hi, Both, None} \cap Int = { }
VARIABLES x, turn, y
vars == <<x, turn, y>>
Init == /\ x = None
/\ turn = "input"
/\ y = {}
InputNum == /\ turn = "input"
/\ turn' = "output"
/\ x' \in Int
/\ y' = y
Respond == /\ turn = "output"
/\ turn' = "input"
/\ y' = y \cup {x}
/\ x' = IF x = setMax(y') THEN IF x = setMin(y') THEN Both ELSE Hi
ELSE IF x = setMin(y') THEN Lo ELSE None
Next == InputNum \/ Respond
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
Infinity == CHOOSE n : n \notin Int
MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})
M == INSTANCE MinMax2
WITH min <- IF y = {} THEN Infinity ELSE setMin(y),
max <- IF y = {} THEN MinusInfinity ELSE setMax(y)
TypeOK == /\ x \in Int \cup {Lo, Hi, Both, None}
/\ turn \in {"input", "output"}
/\ y \in SUBSET Int
Inv == /\ TypeOK
/\ \/ /\ turn = "output"
/\ x \in Int
\/ /\ turn = "input"
/\ x \in {Lo, Hi, Both, None}
LEMMA MaxIntegers ==
ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S)
PROVE /\ setMax(S) \in S
/\ \A yy \in S : yy <= setMax(S)
<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E xx \in T : \A yy \in T : yy <= xx
<1>1. P({})
OBVIOUS
<1>2. ASSUME NEW T, NEW xx, P(T), xx \notin T
PROVE P(T \cup {xx})
<2>. HAVE T \cup {xx} \in SUBSET Int
<2>1. CASE \A yy \in T : yy <= xx
BY <2>1, Isa
<2>2. CASE \E yy \in T : ~(yy <= xx)
<3>. T # {}
BY <2>2
<3>1. PICK yy \in T : \A zz \in T : zz <= yy
BY <1>2
<3>2. xx <= yy
BY <2>2, <3>1
<3>3. QED BY <3>1, <3>2
<2>. QED BY <2>1, <2>2
<1>. HIDE DEF P
<1>3. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast")
<1>. QED BY <1>3, Zenon DEF setMax, P
LEMMA MinIntegers ==
ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S)
PROVE /\ setMin(S) \in S
/\ \A yy \in S : yy >= setMin(S)
<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E xx \in T : \A yy \in T : yy >= xx
<1>1. P({})
OBVIOUS
<1>2. ASSUME NEW T, NEW xx, P(T), xx \notin T
PROVE P(T \cup {xx})
<2>. HAVE T \cup {xx} \in SUBSET Int
<2>1. CASE \A yy \in T : yy >= xx
BY <2>1, Isa
<2>2. CASE \E yy \in T : ~(yy >= xx)
<3>. T # {}
BY <2>2
<3>1. PICK yy \in T : \A zz \in T : zz >= yy
BY <1>2
<3>2. xx >= yy
BY <2>2, <3>1
<3>3. QED BY <3>1, <3>2
<2>. QED BY <2>1, <2>2
<1>. HIDE DEF P
<1>3. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast")
<1>. QED BY <1>3, Zenon DEF setMin, P
LEMMA IInv == Spec => []Inv
<1> USE Assumption DEF Inv
<1>1. Init => Inv
BY DEF Init, TypeOK
<1>2. Inv /\ [Next]_vars => Inv'
BY DEF Next, vars, TypeOK, InputNum, Respond, setMax, setMin
<1>3. QED
BY <1>1, <1>2, PTL
DEF Spec
THEOREM Implements == Spec => M!Spec
<1> USE Assumption, M!Assumption
<1>1. Init => M!Init
BY DEF Init, M!Init, MinusInfinity, Infinity, M!MinusInfinity, M!Infinity
<1>2. Inv /\ [Next]_vars => [M!Next]_M!vars
<2> SUFFICES ASSUME Inv,
[Next]_vars
PROVE [M!Next]_M!vars
OBVIOUS
<2>1. CASE InputNum
BY <2>1
DEF InputNum, M!Next, M!vars, M!InputNum
<2>2. CASE Respond
<3>1. CASE /\ turn = "output"
/\ turn' = "input"
/\ y' = y \cup {x}
<4>1. CASE /\ y = {}
/\ x' = Both
BY <4>1, <3>1, <2>2
DEF Respond,
Inv, TypeOK,
Next, vars, InputNum, Respond,
setMax, setMin,
Infinity, MinusInfinity,
M!Next, M!vars, M!InputNum, M!Respond,
M!Infinity, M!MinusInfinity,
M!IsLeq, M!IsGeq
<4>2. CASE /\ y = {x}
/\ x' = Both
BY <4>2, <3>1, <2>2
DEF Respond,
Inv, TypeOK,
Next, vars, InputNum, Respond,
setMax, setMin,
Infinity, MinusInfinity,
M!Next, M!vars, M!InputNum, M!Respond,
M!Infinity, M!MinusInfinity,
M!IsLeq, M!IsGeq
<4>3. CASE /\ ~(\E yy \in y : yy > x)
/\ x' = Hi
<4>4. CASE /\ ~(\E yy \in y : yy < x)
/\ x' = Lo
<4>5. CASE /\ \E yy \in y : yy > x
/\ \E yy \in y : yy > x
/\ x' = None
<4>6. QED
BY <4>1, <4>2, <4>3, <4>4, <4>5, <3>1, <2>2, MaxIntegers, MinIntegers
DEF Respond,
Inv, TypeOK,
Next, vars, InputNum, Respond,
setMax, setMin,
Infinity, MinusInfinity,
M!Next, M!vars, M!InputNum, M!Respond,
M!Infinity, M!MinusInfinity,
M!IsLeq, M!IsGeq
<3>2. QED
BY <3>1, <2>2
DEF Respond
<2>3. CASE UNCHANGED vars
BY <2>3 DEF vars, M!vars
<2>4. QED
BY <2>1, <2>2, <2>3 DEF Next
<1>3. QED
BY <1>1, <1>2, PTL, IInv
DEF Spec, M!Spec
=============================================================================