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.

Attached is the spec and the output of the goal where I am at. Also the
original proof is in there for now, please just disregard I am leaving it
in there for the moment to show what I originally did to what I am now
going to with these "there exists" proofs. I am currently working on


Thank you for the catch, and I apologize about that. I am using pushed and
pushed everywhere else, I believe. I guess if I missed any they will come
up when I am trying to prove.


On Mon, Sep 24, 2012 at 9:05 AM, Roger Bishop Jones <> wrote:

> Jon,
> On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote:
> > I tried adding the exclamation point to the end of the
> > pushed' line, but if gave me a paser error saying free
> > types here not allowed. I have provided exactly the what
> > the paragraph looked like I tried to parse and the error
> > that was reported in the errorEncountered document.
> The perils of not carefully quoting!
> The exclamation mark was not intended to be in the formal
> text, it was just my exclamation.
> The point I was making was just that you had said "push'={}"
> and it should have been "pushed'={}"!
> > I went back to just having the two exclamation points on
> > pushed and Button_State, in the predicate and
> > declaration section of the schema box respectively, and
> > this generated a monster of subgoals when I tried the
> > provided proof strategy. Obviously there should not be
> > that much to prove, especially when everything is the
> > same, except for push just being set to the empty set.
> Should be "pushed"!
> Make sure you have no occurrences of "push" and if you still
> have a problem with the proof post it.
> > I
> > have also gone back and reviewed Jacky's "The Way of
> > Zed" and he uses the delta operator to signify there are
> > changes being made to the states, though he never
> > discusses initialization, but there appears to be some
> > disconnect between the authors, though I know Spivey and
> > Woodcock should probably be followed so I like to stick
> > with what they say is best practice.
> I don't have access to Jacky's book so I can't comment.
> > As for the Init and State blocks that I am trying to and
> > have proven, should there be a change there so that the
> > proof is not of precondition but of consistency? As you
> > have mentioned, and I have agreed with, it is really
> > pointless to do the precondition proofs for the states
> > when they are static and not changing, everything
> > remains the same, and they are only showing the
> > information provided is consistent.
> Yes, try proving:
>         ∃ Init ∙ true
> and
>         ∃ State ∙ true
> Both should be trivial proofs.
> Roger

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Attachment: errorEncountered.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to