Jon, 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 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
