tuned (in particular bold fonts)
Sat, 16 Mar 2013 17:22:05 +0100
changeset 51436 790310525e97
parent 51435 c22bd20b0d63
child 51437 8739f8abbecb
tuned (in particular bold fonts)
--- 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 @@
-\section{Logic and proof beyond equality}
 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.
 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.
 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.
 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
@@ -260,7 +257,7 @@
 There is also a lightweight variant \isacom{try0} that does not call
-\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 @@
 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 @@
 Of course this is just an example and could be proved by @{text arith}, too.
-\subsubsection{Forward proof}
+\subsection{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 @@
-\def\bfdefault{sbc} % make sans serif the default bold font
@@ -63,7 +60,7 @@
 % isabelle keyword, adapted from isabelle.sty
 % add \noindent to text blocks automatically
--- 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 @@
+\chapter{Logic and proof beyond equality}
--- 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)"