# HG changeset patch # User nipkow # Date 1363450925 -3600 # Node ID 790310525e974a9198c1e2421a8819582b163bba # Parent c22bd20b0d63f1ee99181de55ab52d61449eb67c tuned (in particular bold fonts) diff -r c22bd20b0d63 -r 790310525e97 src/Doc/ProgProve/Logic.thy --- a/src/Doc/ProgProve/Logic.thy Sat Mar 16 10:50:23 2013 +0100 +++ b/src/Doc/ProgProve/Logic.thy Sat Mar 16 17:22:05 2013 +0100 @@ -5,10 +5,7 @@ (*>*) text{* \vspace{-5ex} -\section{Logic and proof beyond equality} -\label{sec:Logic} - -\subsection{Formulas} +\section{Formulas} The core syntax of formulas (\textit{form} below) provides the standard logical constructs, in decreasing order of precedence: @@ -71,7 +68,7 @@ but the first one works better when using the theorem in further proofs. \end{warn} -\subsection{Sets} +\section{Sets} \label{sec:Sets} Sets of elements of type @{typ 'a} have type @{typ"'a set"}. @@ -108,7 +105,7 @@ Sets also allow bounded quantifications @{prop"ALL x : A. P"} and @{prop"EX x : A. P"}. -\subsection{Proof automation} +\section{Proof automation} So far we have only seen @{text simp} and @{text auto}: Both perform rewriting, both can also prove linear arithmetic facts (no multiplication), @@ -181,7 +178,7 @@ Because of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods. -\subsubsection{Sledgehammer} +\subsection{Sledgehammer} Command \isacom{sledgehammer} calls a number of external automatic theorem provers (ATPs) that run for up to 30 seconds searching for a @@ -221,7 +218,7 @@ incomparable. Therefore it is recommended to apply @{text simp} or @{text auto} before invoking \isacom{sledgehammer} on what is left. -\subsubsection{Arithmetic} +\subsection{Arithmetic} By arithmetic formulas we mean formulas involving variables, numbers, @{text "+"}, @{text"-"}, @{text "="}, @{text "<"}, @{text "\"} and the usual logical @@ -247,7 +244,7 @@ but we will not enlarge on that here. -\subsubsection{Trying them all} +\subsection{Trying them all} If you want to try all of the above automatic proof methods you simply type \begin{isabelle} @@ -260,7 +257,7 @@ There is also a lightweight variant \isacom{try0} that does not call sledgehammer. -\subsection{Single step proofs} +\section{Single step proofs} Although automation is nice, it often fails, at least initially, and you need to find out why. When @{text fastforce} or @{text blast} simply fail, you have @@ -273,7 +270,7 @@ \] to the proof state. We will now examine the details of this process. -\subsubsection{Instantiating unknowns} +\subsection{Instantiating unknowns} We had briefly mentioned earlier that after proving some theorem, Isabelle replaces all free variables @{text x} by so called \concept{unknowns} @@ -301,7 +298,7 @@ @{text "conjI[where ?P = \"a=b\" and ?Q = \"False\"]"}. -\subsubsection{Rule application} +\subsection{Rule application} \concept{Rule application} means applying a rule backwards to a proof state. For example, applying rule @{thm[source]conjI} to a proof state @@ -327,7 +324,7 @@ \end{quote} This is also called \concept{backchaining} with rule @{text xyz}. -\subsubsection{Introduction rules} +\subsection{Introduction rules} Conjunction introduction (@{thm[source] conjI}) is one example of a whole class of rules known as \concept{introduction rules}. They explain under which @@ -377,7 +374,7 @@ text{* Of course this is just an example and could be proved by @{text arith}, too. -\subsubsection{Forward proof} +\subsection{Forward proof} \label{sec:forward-proof} Forward proof means deriving new theorems from old theorems. We have already @@ -426,7 +423,7 @@ 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} +\subsection{Finding theorems} Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current theory. Search criteria include pattern matching on terms and on names. diff -r c22bd20b0d63 -r 790310525e97 src/Doc/ProgProve/document/prelude.tex --- a/src/Doc/ProgProve/document/prelude.tex Sat Mar 16 10:50:23 2013 +0100 +++ b/src/Doc/ProgProve/document/prelude.tex Sat Mar 16 17:22:05 2013 +0100 @@ -9,9 +9,6 @@ \usepackage{ccfonts} \usepackage[euler-digits]{eulervm} -\let\bfdefaultold=\bfdefault -\def\bfdefault{sbc} % make sans serif the default bold font - \usepackage{isabelle,isabellesym} \usepackage{mathpartir} \usepackage{amssymb} @@ -63,7 +60,7 @@ % isabelle keyword, adapted from isabelle.sty \renewcommand{\isakeyword}[1] {\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textbf{#1}}} +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\def\bfdefault{sbc}\textbf{#1}}} % add \noindent to text blocks automatically \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}} diff -r c22bd20b0d63 -r 790310525e97 src/Doc/ProgProve/document/root.tex --- a/src/Doc/ProgProve/document/root.tex Sat Mar 16 10:50:23 2013 +0100 +++ b/src/Doc/ProgProve/document/root.tex Sat Mar 16 17:22:05 2013 +0100 @@ -34,7 +34,7 @@ %\label{sec:CaseStudyExp} %\input{../generated/Expressions} -\chapter{Logic} +\chapter{Logic and proof beyond equality} \label{ch:Logic} \input{Logic} diff -r c22bd20b0d63 -r 790310525e97 src/HOL/IMP/Live_True.thy --- a/src/HOL/IMP/Live_True.thy Sat Mar 16 10:50:23 2013 +0100 +++ b/src/HOL/IMP/Live_True.thy Sat Mar 16 17:22:05 2013 +0100 @@ -8,7 +8,7 @@ fun L :: "com \ vname set \ vname set" where "L SKIP X = X" | -"L (x ::= a) X = (if x \ X then X - {x} \ vars a else X)" | +"L (x ::= a) X = (if x \ X then vars a \ (X - {x}) else X)" | "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \ L c\<^isub>2) X" | "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \ L c\<^isub>1 X \ L c\<^isub>2 X" | "L (WHILE b DO c) X = lfp(\Y. vars b \ X \ L c Y)"