On 09/09/14 15:07, Jiaqi Tan wrote: > I tried to clear the assumption list by appending "THEN (POP_ASSUM (K > ALL_TAC))" > to my current list of tactics, but it doesn't clear any of the assumptions. I > tried using "THEN (POP_ASSUM MP_TAC)" (in place of "K ALL_TAC") as well, and > it > only adds one of the 6 assumptions as an antecedent to the goal.
If you want to get rid of them all, you will need to do REPEAT (POP_ASSUM (K ALL_TAC)) I only suggested the non-repeated version so that you could pop them off one at a time to see when METIS_TAC started to work. > The current proof steps I have are (apologies for the verbosity): ... > I'm not sure if the calls to Q.PAT_ASSUM followed > by the simplification using FULL_SIMP_TAC, and then the subsequent ASSUME_TAC > followed by the rewrites, are causing any issues (or are logically > incorrect/unsound). After (show_types := true), the instantiated inductive > hypotheses have the correct types and I am able to discharge the relevant > conjuncts in the goal. I guess you probably have found a bug in METIS_TAC. Does PROVE_TAC solve the goal? Michael ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Want excitement? Manually upgrade your production database. When you want reliability, choose Perforce. Perforce version control. Predictably reliable. http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
