On Tuesday 25 Sep 2012 22:05, Jon Lockhart wrote:

> I started doing the "There Exist" proofs, and as you said
> they seem quite trivial indeed, but I seem to be stuck
> after the first two lines. So I have the goal, and it
> has been rewritten, now I am not sure what is the right
> question to ask. Do I do the z_"There Exist"_tac or
> something else? What constitutes a witness for some of
> the predicate declarations.

Ideally you would say "prove_∃_tac" and it would do it for 
you, but at present automation for existential goals in Z is 
not strong, so you normally have to supply the witness 
yourself and should use z_∃_tac.

You have to ask yourself what are the objects which belong 
to the schema (ButtonState in this case) and chose a simple 
one to use as a witness.
You then have to prove that the witness does indeed have the 
required properties.
So the question is, "what's a simple binding which satisifies
the ButtonState predicate?", i.e. what are the acceptable 
states of the buttons.
The components of ButtonState are all sets.
You have said nothing which requires any of them to be non-
empty, and the specified relationships all hold if they are 
all empty.
So the binding in which every component is the empty set 
will be your simplest witness.
If you supply that witness and then rewrite that should 
solve the goal.

At this point you might ask yourself whether "ButtonState" 
does not allow more things to vary than might be thought 
Do you really want your system to allow all the buttons to 
disappear, or even to allow that the set of buttons might 
change, or to allow that a floor button become a lift button?
I don't know your application, but I would have thought that 
the set of buttons would be fixed and only the "pushed" bit 
was actually part of the state.
In that case you could have buttons, floorButtons and 
elevatorButtons as loosely specified by an axiomatic 
paragraph, so that they are fixed in any implementation of 
the spec but not fixed by the spec, and then you would have 
only one component in ButtonState, i.e. "pushed", 
constrained to be a subset of the available buttons.


Proofpower mailing list

Reply via email to