Re: [tlaplus] ENABLED Operator Theorems

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

> On 3 May 2017, at 10:46, kacem belout <belout...@xxxxxxxxx> wrote:
> 
> Hallo,
> 
> I noticed the following theorems concerning the ENABLED Operator that I  hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules)

as I tried to explain before, in order to give a precise meaning to your notion of "formal" proof, you would need to give clear definitions.

> 
> In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements.

I don't understand why you insist on Raw TLA: the difference between RTLA and TLA only exists at the temporal level, and you don't consider any temporal formulas. Also, it would help if you used actual TLA syntax.

> Let me know if any one is not valid by giving a counterexample, thanks !.
> 
> Theorem 1 : A ==> ENABLED(A)
>                  Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables.

See my previous answer: the implication holds for the same reason why F => \E X: F is a theorem of first-order logic.

> 
> Theorem 2 : \Not ENABLED(A) ==> \Not A
>                  Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive).

Yes, so it's just a corollary to the previous theorem.

> 
> Theorem 3 : \Not A ==> \Not ENABLED(A)

Wrong. Consider A == x = 0 /\ x' = 1 and a state s that assigns 0 to x. Then the stuttering step (s,s) satisfies ~ A and ENABLED A.

> 
> Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A))

Consequence of Theorems 1 and 2.

> 
> Theorem 5 :  ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A.  (A)-1 == A ( v ' <- v , v <- v ')

Wrong, take again A == x=0 /\ x'=1. then

ENABLED A \equiv x = 0
ENABLED (A)-1 \equiv x = 1

> 
> Theorem 6 : For any state predicate P.  P <==> ENABLED(P)

Correct.

> Theorem 7 : For any state predicate P.  P ==> ENABLED((P) '), where ' == Prime operator.

Correct. (ENABLED P' is true iff P is satisfiable.)

> Theorem 8 : For any state predicate P.  P ==> ENABLED(((p)')-1)

Isn't (P')-1 = P, so this is the same as theorem 6?

Regards,
Stephan