Re: [ProofPower] Schemas and Operations
Thank you, Roger. Regards, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Schemas and Operations
Artur, After my last post I remembered the previous conversation and realised that you were reducing the width of your schemas and then having a problem translating the theta expressions in the original. I've been a bit busier than usual so I didn't get back. In fact I forgot. To use a theta term you have to contrive to get the required signature variables into scope. One way to do this is to use a quantifier. Here's one way to do this how for your original example: =TEX =SML open_theory "z_reals"; new_theory "temp"; =TEX %SZS% State %BH%%BH%%BH%%BH% %BV% a: %bbR%; %BV% b: %bbB% %EZ%%BH%%BH%%BH%%BH%%BH% %SZS% OpState %BH%%BH%%BH%%BH% %BV% %Delta%State %BT%%BH%%BH%%BH%%BH% %BV% a = real 0; %BV% %theta%(State \%down%s (a))' = %theta%(State \%down%s (a)) %EZ%%BH%%BH%%BH%%BH%%BH% %SFT%Z %BV% NewState %def% [OldState : State] %EFT% %SZS% OpNewState %BH%%BH%%BH%%BH% %BV% %Delta%NewState %BT%%BH%%BH%%BH%%BH% %BV% %exists%OpState%spot% %theta%(State) = OldState %and% %theta%(State)' = OldState' %EZ%%BH%%BH%%BH%%BH%%BH% =TEX regards, Rpger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Schemas and Operations
Hi Roger, This is a simple example to try to explain what I have now. My current problem is bigger than that. I have a state with many components. To load any operation over that state, ProofPower takes a long time without response. Few months ago, I sent a doc file to Rob Arthan and he suggested to use %SFT%Z %V% St %def% [St : State] %EFT% That is what I am using so far, every operation is similar to %SZS% OpNewState %BH%%BH%%BH%%BH% %BV% %Delta%NewState %BT%%BH%%BH%%BH%%BH% %BV% Old.a = real 0; %EZ%%BH%%BH%%BH%%BH%%BH% and it works fine, loading quickly. >For a similar predicate to work you would need the signature >of NewState to be the same as for State. Is there any other solution for my problem? Thanks, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Schemas and Operations
Artur, On Monday 09 February 2009 14:58:17 Artur Oliveira Gomes wrote: > To represent that everything except "a" is unchanged in State, we use: > > %BV% %theta%(State \%down%s (a))' = > %BV% %theta%(State \%down%s (a)) > > But, using this, > > %SFT%Z > %BV% NewState %def% [OldState : State] > %EFT% > > In a new operation, the predicate presented before is not accepted in > ProofPower. For a similar predicate to work you would need the signature of NewState to be the same as for State. But NewState has a single component called OldState, a completely different signature. Hard to say how to fix the problem without knowing more about what you are truing to do. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com