Hey Guys,

So I got an actual proof question this time, and I can't seem to find any
that I can use successfully from the reference document to solve my current
question.

I am currently trying to prove some statements about my specification, and
in this case I am working on trying to prove the preconditions of one of
the portions of the spec. After setting the goal and dong  *a (rewrite_tac
(map z_get_spec* "spec I want to use"*));  *and doing *a (REPEAT
z_stip_tac); *I was given three subgoals to prove. I have gotten the first
two using just *a (asm_prove_tac []);* but the last one none of the tactics
seem to work for. Most of the tactics return the exact same goal and the
comment printed with the goal is that it is alpha-convertible to its goal.
I am assuming it is saying that this subgoal is alpha-convertible to the
main goal I am trying to prove. Now I looked at the reference manual and
there appears to be some commands that I can use to eliminate
alpha-convertible components and that this is what I should use for
simplifying the sub goal and thus proving it and the main goal.
Unfortunately I can't seem to get to any of the commands working with
Goals, i.e. I am having trouble accessing the goals to use them.

So based on the scenario above and where I am at does anyone have any
suggestions on what commands I should use to handle the alpha-conversion
and completing the proof of the subgoal?

Thanks,
Jon

On Mon, Sep 3, 2012 at 2:55 PM, Jon Lockhart <jal...@bucknell.edu> wrote:

> Phil,
>
> After resetting the command window and rerunning the commands today, I was
> able to run my specification to the point where I was running into the
> exception with no problems. I must of somehow changed the proof context I
> guess, though the print status was coming up that is was ok. Not sure, but
> it was probably on my typing in a command wrong.
>
> Thanks for the help. I am sure I will be back with more questions today as
> I try to prove portions of my specification.
>
> Regards,
> Jon
>
>
>
> On Sun, Sep 2, 2012 at 9:00 PM, Phil Clayton <phil.clay...@lineone.net>wrote:
>
>> Hi John,
>>
>> That sounds strange.  It's probably easiest if you can cut your example
>> down to a short script that produces the error, say containing just a
>> single paragraph, and send a zipped version of that to the list.
>>
>> Phil
>>
>>
>>
>> On 03/09/12 01:47, Jon Lockhart wrote:
>>
>>> Phil,
>>>
>>> Thanks for the reply. I have set it so up like that where the parent
>>> theory is z_library and my new theory is named something else. Just ran
>>> the print status again and that is what it says as well.
>>>
>>> Could it be one more minor thing is not loaded?
>>>
>>> Regards,
>>> Jon
>>>
>>> On Sep 2, 2012 8:43 PM, "Phil Clayton" <phil.clay...@lineone.net
>>> <mailto:phil.clayton@lineone.**net <phil.clay...@lineone.net>>> wrote:
>>>
>>>     Hi John,
>>>
>>>     On 02/09/12 23:59, Jon Lockhart wrote:
>>>
>>>         The problem I am having is this. I am trying to use the union
>>>         operator
>>>         in my specification. More specifically I am trying to and a
>>>         individual
>>>         item to a set in the predicate of a specification paragraph in
>>>         z, which
>>>         is allowed by the rules of the language. The PP system comes
>>>         back with
>>>         expection 62000 of the Z-Parser, saying that the union symbol
>>>         from the
>>>         palette is a free variable and those are not permitted in Z
>>>         paragraphs.
>>>
>>>
>>>     If ProofPower says that ∪ is a variable then the Z toolkit theory
>>>     "z_sets" that defines the Z global variable (_ ∪ _) is not in scope,
>>>     i.e. "z_sets" is not an ancestor theory of your current theory.
>>>
>>>     Generally, Z specifications should always have the theory
>>>     "z_library" as an ancestor, which brings all Z toolkit theories into
>>>     scope.  Typically your theory would start
>>>
>>>        open_theory "z_library";
>>>        new_theory "some_new_theory";
>>>        ...
>>>
>>>     If you need other theories in scope, add them as parents e.g.
>>>
>>>        new_parent "z_reals";
>>>
>>>     Phil
>>>
>>>
>>>
>>> ______________________________**_________________
>>> Proofpower mailing list
>>> Proofpower@lemma-one.com
>>> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>>>
>>>
>>
>
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to