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

## Advertising

> 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
acceptable.
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.
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com