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

author | sultana |

Tue, 24 Apr 2012 14:06:38 +0100 | |

changeset 47731 | 39c5a1a80acc |

parent 47730 | 15f4309bb9eb (current diff) |

parent 47727 | 027c7f8cef22 (diff) |

child 47732 | 503efdb07566 |

merged

--- a/doc-src/ProgProve/Thys/Logic.thy Tue Apr 24 13:59:29 2012 +0100 +++ b/doc-src/ProgProve/Thys/Logic.thy Tue Apr 24 14:06:38 2012 +0100 @@ -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 13:59:29 2012 +0100 +++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 24 14:06:38 2012 +0100 @@ -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}