Thanks for the input. I adjusted the predicate section of my specification
to include that precondition requirement, and everything fell right into

On Tue, Nov 6, 2012 at 3:17 PM, Roger Bishop Jones <> wrote:

> On Tuesday 06 Nov 2012 01:04, Jon Lockhart wrote:
> > Unfortunately I realized I
> > needed to show that the starting and calling floors were
> > greater than zero not greater than or equal to zero.
> However, this makes the goal false, so far as I can see.
> You need to change the specification if you want this to be
> the case.
> > I have modified my goal as such, and was able to prove the
> > first sub goal. The third sub goal should be easy to get
> > since it is exactly like what I was originally proving.
> > I am having trouble though with the second goal, which
> > the point I am at can be seen in the error encountered
> > document I have provided.
> > It looks exactly like goal one, but the linear arithmetic
> > tactic fails to solve it, and I tired introducing a
> > lemma through LEMMA_T, since I could not get lemma_tac
> > working, and I would believe that should give the system
> > enough to prove the goal, but apparently not. It
> > logically makes since in my head.
> I think the reason linear arithmetic fails is because the
> subgoal is false.
> It looks like you don't really understand what lemma_tac and
> LEMMA_T do.
> They do not do any useful proof work, they just help you to
> organise your proof by proving and then using a lemma.
> "lemma_tac" assumes you want to use the lemma by adding it
> into your assumptions using strip_asm_tac, whereas LEMMA_T
> allows you to specify how you are going to use the lemma.
> In your proof, you say "asm_tac", which is like
> "strip_asm_tac" except that it adds the lemma into the
> assumptions without stripping it.
> In both cases you have to prove the lemma yourself.
> You can do that in the same step using THEN1 if you know a
> tactic which will prove it in one step, otherwise THEN1 will
> do the first step of the proof and you have to continue on
> from there.
> In your case, you could have solved that particular subgoal
> if you had used linear arithmetic instead of just a rewrite,
> but the lemma would not help you to solve goal 2, if (as I
> suspect) its not true,
> You need to stipulate in your general operation predicate
> the necessary constraints on the allowable input values.
> Roger Jones
Proofpower mailing list

Reply via email to