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



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

Reply via email to