--- 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 "\<le>"} 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.
--- 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}}
--- 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}
--- 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 \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
-"L (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
+"L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"