Manual/Tutorial/logic.tex

57 For example, the \ML{} function \ml{dest\_imp} with \ML{} type \ml{term -> term * term} splits an implication into a pair of terms consisting of its antecedent and consequent, and the \ML\ function \ml{dest\_conj} of type \ml{term -> term * term} splits a conjunction into its two conjuncts.%
85 The built-in function \ml{type_of} has \ML{} type \ml{term->hol_type} and returns the logical type of a term.
118 The function \ml{mk_var} constructs a variable from a string and a type.
145 There are actually only four different kinds of term in \HOL: variables, constants, function applications (\ml{``$t_1$ $t_2$``}), and lambda abstractions (\ml{``\bs$x$.$t$``}).
201 An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function with type $\tau_1 \to \tau_2$ and $t_2$ has type $\tau_1$.
202 Contrarily, an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function:
222 \noindent or if it is a function, but $t_2$ is not in its domain:
261 Functions have types of the form \ml{$\sigma_1$->$\sigma_2$}, where $\sigma_1$ and $\sigma_2$ are the types of the domain and range of the function, respectively.
295 For example, {\small\verb|``\x. x+1``|} is a term that denotes the function $n\mapsto n{+}1$.
377 \noindent This rule is represented in \ML{} by a function \ml{SPEC},%
401 If the argument to an \ML{} function representing a rule of inference is of the wrong kind, or violates a condition of the rule, then the application fails.
403 When one of the standard \ml{HOL\_ERR} exceptions is raised, more information about the failure can often be gained by using the \ml{Raise} function.%
404 \footnote{The \ml{Raise} function passes on all of the exceptions it sees; it does not affect the semantics of the computation at all.
454 function \ml{dest\_thm} decomposes a theorem into a pair consisting of
499 The \ML{} function \ml{MP} takes argument theorems of the form
527 The hypotheses of \ml{Th6} can be inspected with the \ML{} function
762 tactic is a function that does two things.
778 \noindent In \HOL,  $\wedge$-introduction is  represented by  the \ML{} function
818 A tactic is an \ML{} function that when applied to a goal generates subgoals together with a \emph{justification function} or {\it validation\/}, which will be an \ML{} derived inference rule, that can be used to infer an achievement of the original goal from achievements of the subgoals.
820 If $T$ is a tactic (\ie\ an \ML{} function of type \ml{goal\,->\,(goal\,list\,*\,(thm\,list\,->\,thm))}) and $g$ is a goal, then applying $T$ to
823 whose second component is a justification function, \ie\ a value with
858 \noindent Applying the justification function \ml{just\_fn} to a list
884 \noindent The function \ml{dest\_conj} splits a conjunction into its
887 \ml{(asl,$t_1$)} and \ml{(asl,$t_2$)}. The justification function,
894 and whose second component is a justification function, with \ML{} type
905 applying $T$ to $g$) is an \ML{} function which when applied to the
909 $p$ is a function for converting a solution of the subgoals to a
1044 \noindent will bind $p$ to a function which when applied to the empty list
1072 The built-in function
1081 If the theorem is not to be saved, the function \ml{prove} of type
1093 (In short, the \ML{} function \ml{g} establishes a goal, and the \ML{} function \ml{e} applies a tactic to the current state of the goal.)
1098 A {\it tactical\/} is an \ML{} function that takes one or more tactics