Hi Jeremy, | What do these extra terms mean?
The HOL Light system of goals is a bit different from the traditional LCF one. The tradition is that a goal is a pair consisting of a list of terms (the assumptions) and another term (the desired conclusion). In HOL Light there are two differences: assumptions are actually theorems not terms, and assumptions are associated with a label, so that you can use assumptions by name (LABEL_TAC "*", USE_THEN "*" etc.). The extra terms you spotted arise because the "assumption" theorems, as theorems, may themselves have assumptions (somewhat confusingly). In practice the assumptions start life as simply "p |- p", when the assumptions end up on the assumption list as a result of ASSUME_TAC or similar tactics. But as a result of further forward inference on assumptions, their conclusions may change while retaining their original hypotheses. The original reason for this somewhat confusing arrangement was to make forward inference on assumptions really correspond to forward inference in the eventual proof prroduced by the kernel. By contrast, in the traditional style, this involves forward inference on a temporary theorem p |- p followed by discharging the assumption p by context. I don't believe this is really very important, but I've stuck with this arrangment ever since. For the most part it is invisible to the user in day-to-day tactic proofs. John. ------------------------------------------------------------------------------ Create and Deploy Rich Internet Apps outside the browser with Adobe(R)AIR(TM) software. With Adobe AIR, Ajax developers can use existing skills and code to build responsive, highly engaging applications that combine the power of local resources and data with the reach of the web. Download the Adobe AIR SDK and Ajax docs to start building applications today-http://p.sf.net/sfu/adobe-com _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
