On Wednesday 19 Sep 2012 21:10, Jon Lockhart wrote:

> I moved on to the next area of my specification, which is
> the initializations of the states declared earlier, and
> I am stuck on the first one. No errors or anything, just
> not sure how to proceed to reduce the goal any further.
> As of now I actually think what I have done is made the
> goal more complex. Was using the z_"there exists"_tac to
> try and eliminate portions so then I could feed the goal
> a tac proving the last bit which is not a precondition.
> Unfortunately using the "there exists" tactic increased
> the goal length and just added more. I have tried
> setting the values to other items with no avail either
> in reducing the goal.

z_exists_tac doesn't actually do much, it just substitutes 
in the witnesses you supplied.
You have to do something else to actually simplify the 
result, usually rewrite.
In this case asm_rewrite_tac simplifies the goal, and 
probably would have proved it if it was true.

Looks to me like you missed a clause in the precondition:
   pushed={}

Roger

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to