76 \index{*"| symbol} |
76 \index{*"| symbol} |
77 \index{*"-"-"> symbol} |
77 \index{*"-"-"> symbol} |
78 \begin{tabular}{rrrr} |
78 \begin{tabular}{rrrr} |
79 \it symbol & \it meta-type & \it priority & \it description \\ |
79 \it symbol & \it meta-type & \it priority & \it description \\ |
80 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & |
80 \sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & |
81 Right 50 & composition ($\circ$) \\ |
81 Left 55 & composition ($\circ$) \\ |
82 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ |
82 \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ |
83 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ |
83 \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ |
84 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & |
84 \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & |
85 less than or equals ($\leq$)\\ |
85 less than or equals ($\leq$)\\ |
86 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ |
86 \tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ |
920 \item |
920 \item |
921 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the |
921 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the |
922 simplification set for higher-order logic. Equality~($=$), which also |
922 simplification set for higher-order logic. Equality~($=$), which also |
923 expresses logical equivalence, may be used for rewriting. See the file |
923 expresses logical equivalence, may be used for rewriting. See the file |
924 {\tt HOL/simpdata.ML} for a complete listing of the simplification |
924 {\tt HOL/simpdata.ML} for a complete listing of the simplification |
925 rules. |
925 rules. |
926 \item |
926 \item |
927 It instantiates the classical reasoner, as described below. |
927 It instantiates the classical reasoner, as described below. |
928 \end{itemize} |
928 \end{itemize} |
|
929 \begin{warn}\index{simplification!of conjunctions} |
|
930 The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$ |
|
931 to \verb$a = b & ...b...$: it does not use the left part of a conjunction |
|
932 while simplifying the right part. This can be changed by including |
|
933 \ttindex{conj_cong} in a simpset: \verb$addcongs [conj_cong]$. It can slow |
|
934 down rewriting and is therefore not included by default. |
|
935 \end{warn} |
|
936 |
929 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as |
937 \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as |
930 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
938 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
931 rule; recall Fig.\ts\ref{hol-lemmas2} above. |
939 rule; recall Fig.\ts\ref{hol-lemmas2} above. |
932 |
940 |
933 The classical reasoner is set up as the structure |
941 The classical reasoner is set up as the structure |