summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 24 Apr 2012 12:36:27 +0200 | |

changeset 47727 | 027c7f8cef22 |

parent 47720 | b11dac707c78 |

child 47728 | 6ee015f6ea4b |

child 47731 | 39c5a1a80acc |

doc update

doc-src/ProgProve/Thys/Logic.thy | file | annotate | diff | comparison | revisions | |

doc-src/ProgProve/Thys/document/Logic.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/ProgProve/Thys/Logic.thy Tue Apr 24 11:07:50 2012 +0200 +++ b/doc-src/ProgProve/Thys/Logic.thy Tue Apr 24 12:36:27 2012 +0200 @@ -244,6 +244,19 @@ but we will not enlarge on that here. +\subsubsection{Trying them all} + +If you want to try all of the above automatic proof methods you simply type +\begin{isabelle} +\isacom{try} +\end{isabelle} +You can also add specific simplification and introduction rules: +\begin{isabelle} +\isacom{try} @{text"simp: \<dots> intro: \<dots>"} +\end{isabelle} +There is also a lightweight variant \isacom{try0} that does not call +sledgehammer. + \subsection{Single step proofs} Although automation is nice, it often fails, at least initially, and you need @@ -410,11 +423,19 @@ text{* In this particular example we could have backchained with @{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination. +\subsubsection{Finding theorems} + +Command \isacom{find\_theorems} searches for specific theorems in the current +theory. Search criteria include pattern matching on terms and on names. +For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}. +\bigskip + \begin{warn} To ease readability we will drop the question marks in front of unknowns from now on. \end{warn} + \section{Inductive definitions} \label{sec:inductive-defs}

--- a/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 24 11:07:50 2012 +0200 +++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 24 12:36:27 2012 +0200 @@ -347,6 +347,19 @@ but we will not enlarge on that here. +\subsubsection{Trying them all} + +If you want to try all of the above automatic proof methods you simply type +\begin{isabelle} +\isacom{try} +\end{isabelle} +You can also add specific simplification and introduction rules: +\begin{isabelle} +\isacom{try} \isa{simp{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ intro{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}} +\end{isabelle} +There is also a lightweight variant \isacom{try0} that does not call +sledgehammer. + \subsection{Single step proofs} Although automation is nice, it often fails, at least initially, and you need @@ -541,11 +554,19 @@ In this particular example we could have backchained with \isa{Suc{\isaliteral{5F}{\isacharunderscore}}leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination. +\subsubsection{Finding theorems} + +Command \isacom{find\_theorems} searches for specific theorems in the current +theory. Search criteria include pattern matching on terms and on names. +For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}. +\bigskip + \begin{warn} To ease readability we will drop the question marks in front of unknowns from now on. \end{warn} + \section{Inductive definitions} \label{sec:inductive-defs}