# HG changeset patch
# User nipkow
# Date 1399010063 -7200
# Node ID 7fbed439b8d364e084030a652afbbaa018617aaa
# Parent  ad1bbed53788d1fd6451bb8d7a73dc0bea740f73
new documentation: How to Prove it

diff -r ad1bbed53788 -r 7fbed439b8d3 src/Doc/How_to_Prove_it/How_to_Prove_it.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/How_to_Prove_it.thy	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,134 @@
+(*<*)
+theory How_to_Prove_it
+imports Complex_Main
+begin
+(*>*)
+text{*
+\chapter{@{theory Main}}
+
+\section{Natural numbers}
+
+%Tobias Nipkow
+\paragraph{Induction rules}~\\
+In addition to structural induction there is the induction rule
+@{thm[source] less_induct}:
+\begin{quote}
+@{thm less_induct}
+\end{quote}
+This is often called ``complete induction''. It is applied like this:
+\begin{quote}
+(@{text"induction n rule: less_induct"})
+\end{quote}
+In fact, it is not restricted to @{typ nat} but works for any wellfounded
+order @{text"<"}.
+
+There are many more special induction rules. You can find all of them
+via the Find button (in Isabelle/jedit) with the following search criteria:
+\begin{quote}
+\texttt{name: Nat name: induct}
+\end{quote}
+
+
+\paragraph{How to convert numerals into @{const Suc} terms}~\\
+Solution: simplify with the lemma @{thm[source] numeral_eq_Suc}.
+
+\noindent
+Example:
+*}
+
+lemma fixes x :: int shows "x ^ 3 = x * x * x"
+by (simp add: numeral_eq_Suc)
+
+text{* This is a typical situation: function ``@{text"^"}'' is defined
+by pattern matching on @{const Suc} but is applied to a numeral.
+
+Note: simplification with @{thm[source] numeral_eq_Suc} will convert all numerals.
+One can be more specific with the lemmas @{thm [source] numeral_2_eq_2}
+(@{thm numeral_2_eq_2}) and @{thm[source] numeral_3_eq_3} (@{thm numeral_3_eq_3}).
+
+
+\section{Lists}
+
+%Tobias Nipkow
+\paragraph{Induction rules}~\\
+In addition to structural induction there are a few more induction rules
+that come in handy at times:
+\begin{itemize}
+\item
+Structural induction where the new element is appended to the end
+of the list (@{thm[source] rev_induct}):
+
+@{thm rev_induct}
+
+\item Induction on the length of a list (@{thm [source] length_induct}):
+
+@{thm length_induct}
+
+\item Simultaneous induction on two lists of the same length (@{thm [source] list_induct2}):
+
+@{thm[display,margin=60] list_induct2}
+
+\end{itemize}
+
+%Tobias Nipkow
+\section{Algebraic simplification}
+
+On the numeric types @{typ nat}, @{typ int} and @{typ real},
+proof method @{text simp} and friends can deal with a limited amount of linear
+arithmetic (no multiplication except by numerals) and method @{text arith} can
+handle full linear arithmetic (on @{typ nat}, @{typ int} including quantifiers).
+But what to do when proper multiplication is involved?
+At this point it can be helpful to simplify with the lemma list
+@{thm [source] algebra_simps}. Examples:
+*}
+
+lemma fixes x :: int
+  shows "(x + y) * (y - z) = (y - z) * x + y * (y-z)"
+by(simp add: algebra_simps)
+
+lemma fixes x :: "'a :: comm_ring"
+  shows "(x + y) * (y - z) = (y - z) * x + y * (y-z)"
+by(simp add: algebra_simps)
+
+text{*
+Rewriting with @{thm[source] algebra_simps} has the following effect:
+terms are rewritten into a normal form by multiplying out,
+rearranging sums and products into some canonical order.
+In the above lemma the normal form will be something like
+@{term"x*y + y*y - x*z - y*z"}.
+This works for concrete types like @{typ int} as well as for classes like
+@{class comm_ring} (commutative rings). For some classes (e.g.\ @{class ring}
+and @{class comm_ring}) this yields a decision procedure for equality.
+
+Additional function and predicate symbols are not a problem either:
+*}
+
+lemma fixes f :: "int \<Rightarrow> int" shows "2 * f(x*y) - f(y*x) < f(y*x) + 1"
+by(simp add: algebra_simps)
+
+text{* Here @{thm[source]algebra_simps} merely has the effect of rewriting
+@{term"y*x"} to @{term"x*y"} (or the other way around). This yields
+a problem of the form @{prop"2*t - t < t + (1::int)"} and we are back in the
+realm of linear arithmetic.
+
+Because @{thm[source]algebra_simps} multiplies out, terms can explode.
+If one merely wants to bring sums or products into a canonical order
+it suffices to rewrite with @{thm [source] add_ac} or @{thm [source] mult_ac}: *}
+
+lemma fixes f :: "int \<Rightarrow> int" shows "f(x*y*z) - f(z*x*y) = 0"
+by(simp add: mult_ac)
+
+text{* The lemmas @{thm[source]algebra_simps} take care of addition, subtraction
+and multiplication (algebraic structures up to rings) but ignore division (fields).
+The lemmas @{thm[source]field_simps} also deal with division:
+*}
+
+lemma fixes x :: real shows "x+z \<noteq> 0 \<Longrightarrow> 1 + y/(x+z) = (x+y+z)/(x+z)"
+by(simp add: field_simps)
+
+text{* Warning: @{thm[source]field_simps} can blow up your terms
+beyond recognition. *}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r ad1bbed53788 -r 7fbed439b8d3 src/Doc/How_to_Prove_it/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/ROOT	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,9 @@
+session How_to_Prove_it = HOL +
+  options [document = pdf, show_question_marks = false]
+  theories
+    How_to_Prove_it
+  document_files
+    "root.tex"
+    "root.bib"
+    "prelude.tex"
+
diff -r ad1bbed53788 -r 7fbed439b8d3 src/Doc/How_to_Prove_it/document/prelude.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/document/prelude.tex	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,69 @@
+\usepackage{makeidx}         % allows index generation
+\usepackage{graphicx}        % standard LaTeX graphics tool
+                             % when including figure files
+\usepackage{multicol}        % used for the two-column index
+\usepackage[bottom]{footmisc}% places footnotes at page bottom
+\usepackage{alltt}
+
+\usepackage[T1]{fontenc}
+
+\usepackage{isabelle,isabellesym}
+%\usepackage{amssymb}
+
+\renewcommand*\descriptionlabel[1]{\hspace\labelsep \textbf{#1}\hfil}
+
+% this should be the last package used
+\usepackage{xcolor}
+\definecolor{linkcolor}{rgb}{0,0,0.4}
+\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
+            filecolor=linkcolor,pagecolor=linkcolor,
+            urlcolor=linkcolor]{hyperref}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{tt}
+\isabellestyle{it}
+
+\renewcommand{\isadigit}[1]{\ensuremath{#1}}
+
+% font size
+\renewcommand{\isastyle}{\isastyleminor}
+
+% indexing
+\usepackage{ifthen}
+\newcommand{\indexdef}[3]%
+{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}}
+
+\renewcommand{\isamarkupheader}[1]{{\rmfamily\subsection{#1}}}
+\renewcommand{\isamarkupsection}[1]{{\rmfamily\subsection{#1}}}
+\renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
+% isabelle in-text command font
+\newcommand{\isacom}[1]{\isa{\isacommand{#1}}}
+
+\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
+\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
+% isabelle keyword, adapted from isabelle.sty
+\renewcommand{\isakeyword}[1]
+{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textsf{\textbf{#1}}}}
+
+% add \noindent to text blocks automatically
+\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
+\renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
+
+\newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
+\newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}
+
+%index
+\newcommand{\conceptnoidx}[1]{\textbf{#1}}
+\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
+\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
+\newcommand{\indexed}[2]{#1\index{#2@\protect#1}}
+
+\chardef\isachardoublequote=`\"%
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+
+\renewcommand{\isacharbackquoteopen}{\isacharbackquote}
+\renewcommand{\isacharbackquoteclose}{\isacharbackquote}
+
+\hyphenation{Isa-belle}
diff -r ad1bbed53788 -r 7fbed439b8d3 src/Doc/How_to_Prove_it/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/document/root.bib	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,14 @@
+@string{CUP="Cambridge University Press"}
+@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
+@string{Springer="Springer-Verlag"}
+
+@manual{Main,author={Tobias Nipkow},title={What's in Main},
+note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
+
+@manual{ProgProve,author={Tobias Nipkow},
+title={Programming and Proving in Isabelle/HOL},
+note={\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}}
+
+@manual{IsarRef,author={Makarius Wenzel},
+title={The Isabelle/Isar Reference Manual},
+note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
diff -r ad1bbed53788 -r 7fbed439b8d3 src/Doc/How_to_Prove_it/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/How_to_Prove_it/document/root.tex	Fri May 02 07:54:23 2014 +0200
@@ -0,0 +1,43 @@
+\documentclass[11pt,a4paper]{report}
+
+\input{prelude}
+
+\begin{document}
+
+\title{How to Prove it in Isabelle/HOL}
+%\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
+\author{Tobias Nipkow}
+\maketitle
+
+
+\begin{abstract}
+  How does one perform induction on the length of a list? How are numerals
+  converted into \isa{Suc} terms? How does one prove equalities in rings
+  and other algebraic structures?
+
+  This document is a collection of practical hints and techniques for dealing
+  with specific frequently occurring situations in proofs in Isabelle/HOL.
+  Not arbitrary proofs but proofs that refer to material that is part of
+  \isa{Main} or \isa{Complex\_Main}.
+
+  This is \emph{not} an introduction to
+\begin{itemize}
+\item proofs in general; for that see mathematics or logic books.
+\item Isabelle/HOL and its proof language; for that see the tutorial
+  \cite{ProgProve} or the reference manual~\cite{IsarRef}.
+\item the contents of theory \isa{Main}; for that see the overview
+  \cite{Main}.
+\end{itemize}
+\end{abstract}
+
+\setcounter{tocdepth}{1}
+\tableofcontents
+
+\input{How_to_Prove_it.tex}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+%\printindex
+
+\end{document}