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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
