equal
deleted
inserted
replaced
1398 of simpsets). Another component are split-rules, which can simplify for |
1398 of simpsets). Another component are split-rules, which can simplify for |
1399 example the ``then'' and ``else'' branches of if-statements under the |
1399 example the ``then'' and ``else'' branches of if-statements under the |
1400 corresponding preconditions. |
1400 corresponding preconditions. |
1401 |
1401 |
1402 \begin{readmore} |
1402 \begin{readmore} |
1403 For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"} |
1403 For more information about the simplifier see @{ML_file "Pure/raw_simplifier.ML"} |
1404 and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in |
1404 and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in |
1405 @{ML_file "Provers/splitter.ML"}. |
1405 @{ML_file "Provers/splitter.ML"}. |
1406 \end{readmore} |
1406 \end{readmore} |
1407 |
1407 |
1408 |
1408 |
1411 |
1411 |
1412 The most common combinators for modifying simpsets are: |
1412 The most common combinators for modifying simpsets are: |
1413 |
1413 |
1414 \begin{isabelle} |
1414 \begin{isabelle} |
1415 \begin{tabular}{l@ {\hspace{10mm}}l} |
1415 \begin{tabular}{l@ {\hspace{10mm}}l} |
1416 @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\ |
1416 @{ML_ind addsimps in Raw_Simplifier} & @{ML_ind delsimps in Raw_Simplifier}\\ |
1417 @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\ |
1417 @{ML_ind addcongs in Raw_Simplifier} & @{ML_ind delcongs in Raw_Simplifier}\\ |
1418 @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\ |
1418 @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\ |
1419 \end{tabular} |
1419 \end{tabular} |
1420 \end{isabelle} |
1420 \end{isabelle} |
1421 |
1421 |
1422 \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}} |
1422 \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}} |
1423 *} |
1423 *} |
1426 \begin{figure}[t] |
1426 \begin{figure}[t] |
1427 \begin{minipage}{\textwidth} |
1427 \begin{minipage}{\textwidth} |
1428 \begin{isabelle}*} |
1428 \begin{isabelle}*} |
1429 ML{*fun print_ss ctxt ss = |
1429 ML{*fun print_ss ctxt ss = |
1430 let |
1430 let |
1431 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1431 val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss |
1432 |
1432 |
1433 fun name_thm (nm, thm) = |
1433 fun name_thm (nm, thm) = |
1434 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm] |
1434 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm] |
1435 fun name_ctrm (nm, ctrm) = |
1435 fun name_ctrm (nm, ctrm) = |
1436 Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm] |
1436 Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm] |
1443 |> pwriteln |
1443 |> pwriteln |
1444 end*} |
1444 end*} |
1445 text_raw {* |
1445 text_raw {* |
1446 \end{isabelle} |
1446 \end{isabelle} |
1447 \end{minipage} |
1447 \end{minipage} |
1448 \caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing |
1448 \caption{The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing |
1449 all printable information stored in a simpset. We are here only interested in the |
1449 all printable information stored in a simpset. We are here only interested in the |
1450 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1450 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1451 \end{figure} *} |
1451 \end{figure} *} |
1452 |
1452 |
1453 |
1453 |
1454 text {* |
1454 text {* |
1455 To see how they work, consider the function in Figure~\ref{fig:printss}, which |
1455 To see how they work, consider the function in Figure~\ref{fig:printss}, which |
1456 prints out some parts of a simpset. If you use it to print out the components of the |
1456 prints out some parts of a simpset. If you use it to print out the components of the |
1457 empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier} |
1457 empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier} |
1458 |
1458 |
1459 @{ML_response_fake [display,gray] |
1459 @{ML_response_fake [display,gray] |
1460 "print_ss @{context} empty_ss" |
1460 "print_ss @{context} empty_ss" |
1461 "Simplification rules: |
1461 "Simplification rules: |
1462 Congruences rules: |
1462 Congruences rules: |
1557 The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}. |
1557 The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}. |
1558 The simpset @{ML HOL_ss} is implemented in @{ML_file "HOL/HOL.thy"}. |
1558 The simpset @{ML HOL_ss} is implemented in @{ML_file "HOL/HOL.thy"}. |
1559 \end{readmore} |
1559 \end{readmore} |
1560 |
1560 |
1561 The simplifier is often used to unfold definitions in a proof. For this the |
1561 The simplifier is often used to unfold definitions in a proof. For this the |
1562 simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME: |
1562 simplifier implements the tactic @{ML_ind rewrite_goal_tac in Raw_Simplifier}.\footnote{\bf FIXME: |
1563 see LocalDefs infrastructure.} Suppose for example the |
1563 see LocalDefs infrastructure.} Suppose for example the |
1564 definition |
1564 definition |
1565 *} |
1565 *} |
1566 |
1566 |
1567 definition "MyTrue \<equiv> True" |
1567 definition "MyTrue \<equiv> True" |
1579 \end{isabelle} *} |
1579 \end{isabelle} *} |
1580 (*<*)oops(*>*) |
1580 (*<*)oops(*>*) |
1581 |
1581 |
1582 text {* |
1582 text {* |
1583 If you want to unfold definitions in \emph{all} subgoals, not just one, |
1583 If you want to unfold definitions in \emph{all} subgoals, not just one, |
1584 then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}. |
1584 then use the the tactic @{ML_ind rewrite_goals_tac in Raw_Simplifier}. |
1585 *} |
1585 *} |
1586 |
1586 |
1587 |
1587 |
1588 text_raw {* |
1588 text_raw {* |
1589 \begin{figure}[p] |
1589 \begin{figure}[p] |
1869 |
1869 |
1870 text {* |
1870 text {* |
1871 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1871 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1872 The function also takes a list of patterns that can trigger the simproc. |
1872 The function also takes a list of patterns that can trigger the simproc. |
1873 Now the simproc is set up and can be explicitly added using |
1873 Now the simproc is set up and can be explicitly added using |
1874 @{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever |
1874 @{ML_ind addsimprocs in Raw_Simplifier} to a simpset whenever |
1875 needed. |
1875 needed. |
1876 |
1876 |
1877 Simprocs are applied from inside to outside and from left to right. You can |
1877 Simprocs are applied from inside to outside and from left to right. You can |
1878 see this in the proof |
1878 see this in the proof |
1879 *} |
1879 *} |
2537 |
2537 |
2538 \begin{readmore} |
2538 \begin{readmore} |
2539 See @{ML_file "Pure/conv.ML"} |
2539 See @{ML_file "Pure/conv.ML"} |
2540 for more information about conversion combinators. |
2540 for more information about conversion combinators. |
2541 Some basic conversions are defined in @{ML_file "Pure/thm.ML"}, |
2541 Some basic conversions are defined in @{ML_file "Pure/thm.ML"}, |
2542 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. |
2542 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/raw_simplifier.ML"}. |
2543 \end{readmore} |
2543 \end{readmore} |
2544 |
2544 |
2545 *} |
2545 *} |
2546 |
2546 |
2547 text {* |
2547 text {* |