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