equal
deleted
inserted
replaced
1222 Setting up the simplifier for new logics is complicated in the general case. |
1222 Setting up the simplifier for new logics is complicated in the general case. |
1223 This section describes how the simplifier is installed for intuitionistic |
1223 This section describes how the simplifier is installed for intuitionistic |
1224 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the |
1224 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the |
1225 Isabelle sources. |
1225 Isabelle sources. |
1226 |
1226 |
1227 The simplifier and the case splitting tactic, which reside on separate files, |
1227 The case splitting tactic, which resides on a separate files, is not part of |
1228 are not part of Pure Isabelle. They must be loaded explicitly by the |
1228 Pure Isabelle. It needs to be loaded explicitly by the object-logic as |
1229 object-logic as follows (below \texttt{\~\relax\~\relax} refers to |
1229 follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}): |
1230 \texttt{\$ISABELLE_HOME}): |
1230 \begin{ttbox} |
1231 \begin{ttbox} |
|
1232 use "\~\relax\~\relax/src/Provers/simplifier.ML"; |
|
1233 use "\~\relax\~\relax/src/Provers/splitter.ML"; |
1231 use "\~\relax\~\relax/src/Provers/splitter.ML"; |
1234 \end{ttbox} |
1232 \end{ttbox} |
1235 |
1233 |
1236 Simplification requires converting object-equalities to meta-level rewrite |
1234 Simplification requires converting object-equalities to meta-level rewrite |
1237 rules. This demands rules stating that equal terms and equivalent formulae |
1235 rules. This demands rules stating that equal terms and equivalent formulae |
1459 \ttbreak |
1457 \ttbreak |
1460 structure Splitter = SplitterFun(SplitterData); |
1458 structure Splitter = SplitterFun(SplitterData); |
1461 \end{ttbox} |
1459 \end{ttbox} |
1462 |
1460 |
1463 |
1461 |
1464 \subsection{Theory setup}\index{simplification!setting up the theory} |
|
1465 \begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier} |
|
1466 Simplifier.setup: (theory -> theory) list |
|
1467 \end{ttbox} |
|
1468 |
|
1469 Advanced theory related features of the simplifier (e.g.\ implicit |
|
1470 simpset support) have to be set up explicitly. The simplifier already |
|
1471 provides a suitable setup function definition. This has to be |
|
1472 installed into the base theory of any new object-logic via a |
|
1473 \texttt{setup} declaration. |
|
1474 |
|
1475 For example, this is done in \texttt{FOL/IFOL.thy} as follows: |
|
1476 \begin{ttbox} |
|
1477 setup Simplifier.setup |
|
1478 \end{ttbox} |
|
1479 |
|
1480 |
|
1481 \index{simplification|)} |
1462 \index{simplification|)} |
1482 |
1463 |
1483 |
1464 |
1484 %%% Local Variables: |
1465 %%% Local Variables: |
1485 %%% mode: latex |
1466 %%% mode: latex |