380 I cannot verify 

   381 I cannot verify\ldots

   382 

   383 

   384 

   385 \newpage

   386 \section*{Isabelle Cheat-Sheet}

   387  

   388 \begin{itemize} 

   389 \item The main notion in Isabelle is a \emph{theorem}.

   390       Definitions, inductive predicates and recursive

   391       functions all have underlying theorems. If a definition

   392       is called \texttt{foo}, then the theorem will be called

   393       \texttt{foo\_def}. Take a recursive function, say

   394       \texttt{bar}, it will have a theorem that is called

   395       \texttt{bar.simps} and will be added to the simplifier.

   396       That means the simplifier will automatically 

   397       Inductive predicates called \texttt{baz} will be called

   398       \texttt{baz.intros}. For inductive predicates, there are

   399       also theorems \texttt{baz.induct} and

   400       \texttt{baz.cases}.    

   401 

   402 \item A \emph{goal-state} consists of one or more subgoals. If

   403       there are \texttt{No more subgoals!} then the theorem is

   404       proved. Each subgoal is of the form

   405   

   406       \[

   407       \llbracket \ldots{}premises\ldots \rrbracket \Longrightarrow 

   408       conclusion

   409       \]  

   410   

   411       \noindent 

   412       where $premises$ and $conclusion$ are formulas of type 

   413       \texttt{bool}.

   414       

   415 \item There are three low-level methods for applying one or

   416       more theorem to a subgoal, called \texttt{rule},

   417       \texttt{drule} and \texttt{erule}. The first applies a 

   418       theorem to a conclusion of a goal. For example

   419       

   420       \[\texttt{apply}(\texttt{rule}\;thm)

   421       \]

   422  

   423       If the conclusion is of the form $\_ \wedge \_$,

   424       $\_ \longrightarrow \_$ and $\forall\,x. \_$ the

   425       $thm$ is called

   426       

   427       \begin{center}

   428       \begin{tabular}{lcl}

   429       $\_ \wedge \_$          &  $\Rightarrow$ & $conjI$\\

   430       $\_ \longrightarrow \_$ &  $\Rightarrow$ & $impI$\\

   431       $\forall\,x.\_$        &  $\Rightarrow$ & $allI$

   432       \end{tabular}

   433       \end{center}

   434        

   435       Many of such rule are called intro-rules and end with 

   436       an ``$I$'', or in case of inductive predicates $\_.intros$.

   437       

   438       

   439        

   440        

   441 \end{itemize}

   442