Phil,

Thank you very much for the quick response. The information you provided
was highly insightful and I will be sure to use the strategies you have
described in my current and future proofs.

You also provided me a solution with the last option you gave, as applying
the second to last tactic in a couple of my proofs generates several
subgoals that are all solvable by the "z_lin_arith" package. I will be sure
of course to make sure when I am doing my proofs in the future that this is
the case before applying the THEN_TRY link command.

Thanks again for the help and I will be sure to report whether the fix was
a success or not.

Regards,
Jon


On Tue, Jan 15, 2013 at 4:31 PM, Phil Clayton <phil.clay...@veonix.com>wrote:

> Hi Jon,
>
> To keep proof scripts maintainable, I always strictly adhere to a format
> where an SML comment is inserted each time the name of the goal changes.
>  For example:
>
> val some_thm = (
> push_goal ([], ...);
> a (REPEAT z_strip_tac);
>
> (* *** Goal "1" *** *)
> a (...);
> ...
>
> (* *** Goal "1.1" *** *)
> a (...);
> ...
>
> (* *** Goal "1.2" *** *)
> a (...);
>
> (* *** Goal "1.2.1" *** *)
> a (...);
>
> (* *** Goal "1.2.2" *** *)
> a (...);
>
> (* *** Goal "2" *** *)
> a (...);
>
> (* *** Goal "3" *** *)
> a (...);
>
> pop_thm ()
> );
>
> If a proof stops working for some reason, the comments above make it much
> easier to track down the reason because they indicate where each subgoal
> should be completed (unless set_labelled_goal was used to change goal).
>
> I wouldn't really advocate e.g.
>
> (* *** Goal "2" *** *)
> (* *** Goal "3" *** *)
> (* *** Goal "4" *** *)
> (* *** Goal "5" *** *)
> fun_pow 4 (fn () => a tac) ();
>
> even though it is fairly obvious that tac is being used to finish the
> commented subgoals.  The reason is that you can't step through the goals
> one at a time when replaying.
>
> Alternatively, if
>
>   a tac1;
>
> produces a number of subgoals that can be finished off by linear
> arithmetic, it may be preferable to stop those goals appearing in the first
> place by
>
>   a (tac1 THEN_TRY PC_T1 "z_lin_arith" asm_prove_tac []);
>
> However, this attempts lin arith on all subgoals produced by tac1 and this
> could be an issue if it does not fail quickly for subgoals that it does not
> prove.  I tend to do this but take care with how subgoals are broken down
> to avoid the issue.
>
> Regards,
>
> Phil
>
>
>
> On 15/01/13 20:55, Jon Lockhart wrote:
>
>> Dear Community,
>>
>> I was wondering if any of you knew of a command that could be used while
>> writing your ProofPower proofs for you HOL or Zed specifications that
>> would allow for the application of the apply_tactic or a command a
>> predetermined number of times? In my specifications I am running across
>> an instance where I need to repeat the same proof command for several
>> goal statements in a row. For example I could have 3 or 4 goals that all
>> require the command 'a (PC_T1 "z_lin_arith asm_prove_tac [])'. Rather
>> than repeating this multiple times I would like to encapsulate the whole
>> thing in a loop or a repeat function, similar to the use of REPEAT
>> within a goal to apply the tactic multiple times. Does such a function
>> exist within the ProofPower tool environment?
>>
>> Regards,
>> Jon Lockhart
>>
>>
>> ______________________________**_________________
>> 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<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