On 29/10/12 11:46, Tony Johnson wrote: > So, I have this.. > - prove(--`B:bool`--,MP_TAC (ASSUME ``A:bool``) THEN ACCEPT_TAC > (mk_thm([],``A ==> B``))); > > val it = [A] |- B : thm
> Which is fine and good, (as long as you think asserting theorems with mk_thm is “fine and good” :-) > but when I use the interactive prompt, > Invalid tactic > ! Uncaught exception: > ! HOL_ERR > - > I get this exception. The exception makes sense because the docs say > that the tactic isn't valid if the thm argument assumption list isn't a > subset of the goal assumption list. However if this is the case, then > why would the tactic work in the proof function? It’s simple: the prove function doesn’t perform the tactic-validity test. Tactic-validity is explicitly checked by the e function; most other tools don’t bother. The validity test can be a useful guard against errors, but these are most likely to occur as you interactively develop a proof. By the time you come to execute a proof, it’s assumed you know what you’re doing, and that your tactic really does prove the theorem you think it does. Michael ------------------------------------------------------------------------------ The Windows 8 Center - In partnership with Sourceforge Your idea - your app - 30 days. Get started! http://windows8center.sourceforge.net/ what-html-developers-need-to-know-about-coding-windows-8-metro-style-apps/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
