Dear Stephan,
Stephan Merz <stephan.merz@xxxxxxxxx> writes:
> Hello,
>
> TLAPS only supports functions of one argument. It’s probably best to replace your function of type
thanks!!! That did it.
Best regards,
Marko
> [ Elems \X SUBSET Elems -> SUBSET Elems ]
>
> by a “curried” function
>
> [ Elems -> [ SUBSET Elems -> SUBSET Elems ] ]
>
> and correspondingly write
>
> ASSUME ...
> PROVE x \in [new \in Elems |-> [set_1 \in SUBSET Elems |-> set_1 \cup {new}]][x][set]
>
> Regards,
> Stephan
>
>
>> On 20 Jun 2019, at 18:39, 'Marko Schuetz-Schmuck' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
>>
>> Dear All,
>>
>> I have a function Insert and an operator InsertOp as in the attached
>> file. When I make the definition of the operator available TLAPS proves
>> the corresponding theorem, but when I make the definition of the
>> function available the function gets rewritten leading to the goal
>>
>> ASSUME NEW CONSTANT Elems,
>> NEW CONSTANT x \in Elems,
>> NEW CONSTANT set \in SUBSET Elems
>> PROVE x
>> \in [new \in Elems, set_1 \in SUBSET Elems |-> set_1 \cup {new}][x,
>> set]
>>
>> How do I tell TLAPS to take the \beta-reduction step?
>>
>> I was unable to find this in all the TLAPS documentation I checked.
>>
>> Thanks and best regards,
>>
>> Marko
>>
>> --
>> 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+unsubscribe@xxxxxxxxxxxxxxxx.
>> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
>> Visit this group at https://groups.google.com/group/tlaplus.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736k4us6d.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
>> For more options, visit https://groups.google.com/d/optout.
>> ------------------------------- MODULE Dummy -------------------------------
>> EXTENDS TLAPS
>> CONSTANT Elems
>> ASSUME \E x : x \in Elems
>>
>> Insert[new \in Elems, set \in SUBSET Elems] ==
>> set \cup {new}
>>
>> InsertOp(new, set) ==
>> set \cup {new}
>>
>> THEOREM \A x \in Elems, set \in SUBSET Elems:
>> x \in Insert[x, set]
>> <1> SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
>> PROVE x \in Insert[x, set]
>> OBVIOUS
>> <1> QED
>> BY DEF Insert
>>
>> THEOREM \A x \in Elems, set \in SUBSET Elems:
>> x \in InsertOp(x, set)
>> <1>a SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
>> PROVE x \in InsertOp(x, set)
>> OBVIOUS
>> <1>b QED
>> BY DEF InsertOp
>> =============================================================================
>> \* Modification History
>> \* Last modified Thu Jun 20 12:30:32 AST 2019 by marko
>> \* Created Thu Jun 13 13:34:49 AST 2019 by marko
>>
>> --
>> 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+unsubscribe@xxxxxxxxxxxxxxxx.
>> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
>> Visit this group at https://groups.google.com/group/tlaplus.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8736k4us6d.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
>> For more options, visit https://groups.google.com/d/optout.
>
> --
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/944861DF-5AC1-4DEA-A37E-6D581E5A0F04%40gmail.com.
> For more options, visit https://groups.google.com/d/optout.
--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87wohgt6qr.fsf%40tpad-m.i-did-not-set--mail-host-address--so-tickle-me.
For more options, visit https://groups.google.com/d/optout.
Attachment:
signature.asc
Description: PGP signature