I've found a solution to my problem. Instead of directly using the proof stack, I proved some rules and wrote helper functions, and the helper functions generate proofs for a number of small theorems (corresponding to the subgoals in my original post). I compose my big theorem from the small theorems.
Thank you anyway. Lu [email protected] wrote: > Please give more details on your goal. > > Good Luck, > Liya > > Quoting Lu Zhao <[email protected]>: > >> Hi, >> >> I have a situation where I don't know what the best solution is. >> >> I have a goal of the form x ==> y, and after an initial rewrite on x and >> after REPEAT STRIP_TAC, I have a list of subgoals. Here's the problem. >> >> 1) According to different situations, the length of the list of subgoals >> varies; >> >> 2) For each subgoal, I need use a different concrete term to instantiate >> a variable. The term is prepared for each subgoal. >> >> I don't know if I can implement this by programming in tactics or on the >> goal stack. >> >> I appreciate any suggestions. >> >> Thanks >> Lu >> >> ------------------------------------------------------------------------------ >> >> >> >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
