Re: [ProofPower] Schemas and Operations

[Artur Oliveira Gomes]

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

[Roger Bishop Jones]

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