next up previous contents
Next: The Proof Environment Up: The Tactic Language Previous: The Special Theorem ORDERED

The Hypothesis Facility

The hypothesis facility assigns a special role to expressions of the form ?x || ?y , ?z, which are intended to denote ?y if ?x denotes true and ?z otherwise. In other words, these are expressions defined by cases.

Expressions with infix || must have second argument a pair, or they will be rejected by the declaration checking functions of the prover (the user can create terms which violate this restriction, but they cannot appear in theorems). || now has some built-in execution behaviour: if ?x evaluates to true or false under a tactic interpreter, the case expression will evaluate to the appropriate one of ?y and ?z. The subterm ?x is handled by the tactic interpreter before the subterms ?y or ?z; conditional expressions can exhibit non-strict execution behavior.

If the subterm matching ?x is actually an equation ?a = ?b, then this equation is usable as a theorem in the context matching ?y. Moreover, any case expression with the same equation in the position matching ?x appearing in either the context matching ?y or the context matching ?z can be reduced to one of the alternatives (the left alternative inside ?y and the right alternative inside ?z).

A theorem of the form 0 |-| n, where n is a positive integer, represents the nth hypothesis from the top level of the current term, in the form of an equation applicable in the context matched by ?y in our generic case expression. A theorem of the form 1 |-| n represents the same hypothesis in a form usable to decide case expressions with the same hypothesis. A theorem of the form (2 |-| n)@parameter has the same effect as 1 |-| n, except that when applied in reverse (the only way it is likely to be applied) the parameter is used as the value in the newly introduced case. Mark2 controls what hypotheses are available in what contexts. The lookhyp and lookhyps commands can be used to look at hypotheses. Theorems with infix |-| appearing in theorems will have their numerals adjusted appropriately on application so that the theorems reference the intended hypotheses.


next up previous contents
Next: The Proof Environment Up: The Tactic Language Previous: The Special Theorem ORDERED

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997