# HG changeset patch # User wenzelm # Date 1333530954 -7200 # Node ID 8204b1023537bcb3d07df57c74c2870c7f3f710c # Parent 360e080fd13e41f03b5a54cc4d7eeec9cb4d6520 removed obsolete isar-overview manual; diff -r 360e080fd13e -r 8204b1023537 doc-src/Dirs --- a/doc-src/Dirs Wed Apr 04 10:04:25 2012 +0100 +++ b/doc-src/Dirs Wed Apr 04 11:15:54 2012 +0200 @@ -1,1 +1,1 @@ -Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve +Intro Ref System Logics HOL ZF Inductive TutorialI IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/IsaMakefile --- a/doc-src/IsarOverview/IsaMakefile Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -## targets - -default: Isar - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log -USEDIR = $(ISABELLE_TOOL) usedir -i false -g false -d false -D document -v true - - -## Isar - -Isar: $(LOG)/HOL-Isar.gz - -$(LOG)/HOL-Isar.gz: Isar/ROOT.ML Isar/document/intro.tex \ - Isar/document/root.tex Isar/document/root.bib Isar/*.thy - @$(USEDIR) HOL Isar - @rm -f Isar/document/isabelle.sty Isar/document/isabellesym.sty \ - Isar/document/pdfsetup.sty Isar/document/session.tex - - -## clean - -clean: - @rm -f $(LOG)/HOL-Isar.gz - diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/Induction.thy --- a/doc-src/IsarOverview/Isar/Induction.thy Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,357 +0,0 @@ -(*<*)theory Induction imports Main begin -fun itrev where -"itrev [] ys = ys" | -"itrev (x#xs) ys = itrev xs (x#ys)" -(*>*) - -section{*Case distinction and induction \label{sec:Induct}*} - -text{* Computer science applications abound with inductively defined -structures, which is why we treat them in more detail. HOL already -comes with a datatype of lists with the two constructors @{text Nil} -and @{text Cons}. @{text Nil} is written @{term"[]"} and @{text"Cons x -xs"} is written @{term"x # xs"}. *} - -subsection{*Case distinction\label{sec:CaseDistinction}*} - -text{* We have already met the @{text cases} method for performing -binary case splits. Here is another example: *} -lemma "\ A \ A" -proof cases - assume "A" thus ?thesis .. -next - assume "\ A" thus ?thesis .. -qed - -text{*\noindent The two cases must come in this order because @{text -cases} merely abbreviates @{text"(rule case_split)"} where -@{thm[source] case_split} is @{thm case_split}. If we reverse -the order of the two cases in the proof, the first case would prove -@{prop"\ A \ \ A \ A"} which would solve the first premise of -@{thm[source] case_split}, instantiating @{text ?P} with @{term "\ -A"}, thus making the second premise @{prop"\ \ A \ \ A \ A"}. -Therefore the order of subgoals is not always completely arbitrary. - -The above proof is appropriate if @{term A} is textually small. -However, if @{term A} is large, we do not want to repeat it. This can -be avoided by the following idiom *} - -lemma "\ A \ A" -proof (cases "A") - case True thus ?thesis .. -next - case False thus ?thesis .. -qed - -text{*\noindent which is like the previous proof but instantiates -@{text ?P} right away with @{term A}. Thus we could prove the two -cases in any order. The phrase \isakeyword{case}~@{text True} -abbreviates \isakeyword{assume}~@{text"True: A"} and analogously for -@{text"False"} and @{prop"\A"}. - -The same game can be played with other datatypes, for example lists, -where @{term tl} is the tail of a list, and @{text length} returns a -natural number (remember: $0-1=0$): -*} -(*<*)declare length_tl[simp del](*>*) -lemma "length(tl xs) = length xs - 1" -proof (cases xs) - case Nil thus ?thesis by simp -next - case Cons thus ?thesis by simp -qed -text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates -\isakeyword{assume}~@{text"Nil:"}~@{prop"xs = []"} and -\isakeyword{case}~@{text Cons} abbreviates \isakeyword{fix}~@{text"? ??"} -\isakeyword{assume}~@{text"Cons:"}~@{text"xs = ? # ??"}, -where @{text"?"} and @{text"??"} -stand for variable names that have been chosen by the system. -Therefore we cannot refer to them. -Luckily, this proof is simple enough we do not need to refer to them. -However, sometimes one may have to. Hence Isar offers a simple scheme for -naming those variables: replace the anonymous @{text Cons} by -@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"} -\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}. -In each \isakeyword{case} the assumption can be -referred to inside the proof by the name of the constructor. In -Section~\ref{sec:full-Ind} below we will come across an example -of this. - -\subsection{Structural induction} - -We start with an inductive proof where both cases are proved automatically: *} -lemma "2 * (\i::nat\n. i) = n*(n+1)" -by (induct n) simp_all - -text{*\noindent The constraint @{text"::nat"} is needed because all of -the operations involved are overloaded. -This proof also demonstrates that \isakeyword{by} can take two arguments, -one to start and one to finish the proof --- the latter is optional. - -If we want to expose more of the structure of the -proof, we can use pattern matching to avoid having to repeat the goal -statement: *} -lemma "2 * (\i::nat\n. i) = n*(n+1)" (is "?P n") -proof (induct n) - show "?P 0" by simp -next - fix n assume "?P n" - thus "?P(Suc n)" by simp -qed - -text{* \noindent We could refine this further to show more of the equational -proof. Instead we explore the same avenue as for case distinctions: -introducing context via the \isakeyword{case} command: *} -lemma "2 * (\i::nat \ n. i) = n*(n+1)" -proof (induct n) - case 0 show ?case by simp -next - case Suc thus ?case by simp -qed - -text{* \noindent The implicitly defined @{text ?case} refers to the -corresponding case to be proved, i.e.\ @{text"?P 0"} in the first case and -@{text"?P(Suc n)"} in the second case. Context \isakeyword{case}~@{text 0} is -empty whereas \isakeyword{case}~@{text Suc} assumes @{text"?P n"}. Again we -have the same problem as with case distinctions: we cannot refer to an anonymous @{term n} -in the induction step because it has not been introduced via \isakeyword{fix} -(in contrast to the previous proof). The solution is the one outlined for -@{text Cons} above: replace @{term Suc} by @{text"(Suc i)"}: *} -lemma fixes n::nat shows "n < n*n + 1" -proof (induct n) - case 0 show ?case by simp -next - case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp -qed - -text{* \noindent Of course we could again have written -\isakeyword{thus}~@{text ?case} instead of giving the term explicitly -but we wanted to use @{term i} somewhere. - -\subsection{Generalization via @{text arbitrary}} - -It is frequently necessary to generalize a claim before it becomes -provable by induction. The tutorial~\cite{LNCS2283} demonstrates this -with @{prop"itrev xs ys = rev xs @ ys"}, where @{text ys} -needs to be universally quantified before induction succeeds.\footnote{@{thm rev.simps(1)},\quad @{thm rev.simps(2)[no_vars]},\\ @{thm itrev.simps(1)[no_vars]},\quad @{thm itrev.simps(2)[no_vars]}} But -strictly speaking, this quantification step is already part of the -proof and the quantifiers should not clutter the original claim. This -is how the quantification step can be combined with induction: *} -lemma "itrev xs ys = rev xs @ ys" -by (induct xs arbitrary: ys) simp_all -text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars} -universally quantifies all \emph{vars} before the induction. Hence -they can be replaced by \emph{arbitrary} values in the proof. - -Generalization via @{text"arbitrary"} is particularly convenient -if the induction step is a structured proof as opposed to the automatic -example above. Then the claim is available in unquantified form but -with the generalized variables replaced by @{text"?"}-variables, ready -for instantiation. In the above example, in the @{const[source] Cons} case the -induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available -under the name @{const[source] Cons}). - - -\subsection{Inductive proofs of conditional formulae} -\label{sec:full-Ind} - -Induction also copes well with formulae involving @{text"\"}, for example -*} - -lemma "xs \ [] \ hd(rev xs) = last xs" -by (induct xs) simp_all - -text{*\noindent This is an improvement over that style the -tutorial~\cite{LNCS2283} advises, which requires @{text"\"}. -A further improvement is shown in the following proof: -*} - -lemma "map f xs = map f ys \ length xs = length ys" -proof (induct ys arbitrary: xs) - case Nil thus ?case by simp -next - case (Cons y ys) note Asm = Cons - show ?case - proof (cases xs) - case Nil - hence False using Asm(2) by simp - thus ?thesis .. - next - case (Cons x xs') - with Asm(2) have "map f xs' = map f ys" by simp - from Asm(1)[OF this] `xs = x#xs'` show ?thesis by simp - qed -qed - -text{*\noindent -The base case is trivial. In the step case Isar assumes -(under the name @{text Cons}) two propositions: -\begin{center} -\begin{tabular}{l} -@{text"map f ?xs = map f ys \ length ?xs = length ys"}\\ -@{prop"map f xs = map f (y # ys)"} -\end{tabular} -\end{center} -The first is the induction hypothesis, the second, and this is new, -is the premise of the induction step. The actual goal at this point is merely -@{prop"length xs = length (y#ys)"}. The assumptions are given the new name -@{text Asm} to avoid a name clash further down. The proof procedes with a case distinction on @{text xs}. In the case @{prop"xs = []"}, the second of our two -assumptions (@{text"Asm(2)"}) implies the contradiction @{text"0 = Suc(\)"}. - In the case @{prop"xs = x#xs'"}, we first obtain -@{prop"map f xs' = map f ys"}, from which a forward step with the first assumption (@{text"Asm(1)[OF this]"}) yields @{prop"length xs' = length ys"}. Together -with @{prop"xs = x#xs"} this yields the goal -@{prop"length xs = length (y#ys)"}. - - -\subsection{Induction formulae involving @{text"\"} or @{text"\"}} - -Let us now consider abstractly the situation where the goal to be proved -contains both @{text"\"} and @{text"\"}, say @{prop"\x. P x \ Q x"}. -This means that in each case of the induction, -@{text ?case} would be of the form @{prop"\x. P' x \ Q' x"}. Thus the -first proof steps will be the canonical ones, fixing @{text x} and assuming -@{prop"P' x"}. To avoid this tedium, induction performs the canonical steps -automatically: in each step case, the assumptions contain both the -usual induction hypothesis and @{prop"P' x"}, whereas @{text ?case} is only -@{prop"Q' x"}. - -\subsection{Rule induction} - -HOL also supports inductively defined sets. See \cite{LNCS2283} -for details. As an example we define our own version of the reflexive -transitive closure of a relation --- HOL provides a predefined one as well.*} -inductive_set - rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) - for r :: "('a \ 'a)set" -where - refl: "(x,x) \ r*" -| step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" - -text{* \noindent -First the constant is declared as a function on binary -relations (with concrete syntax @{term"r*"} instead of @{text"rtc -r"}), then the defining clauses are given. We will now prove that -@{term"r*"} is indeed transitive: *} - -lemma assumes A: "(x,y) \ r*" shows "(y,z) \ r* \ (x,z) \ r*" -using A -proof induct - case refl thus ?case . -next - case step thus ?case by(blast intro: rtc.step) -qed -text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) -\in R$ piped into the proof, here \isakeyword{using}~@{text A}. The -proof itself follows the inductive definition very -closely: there is one case for each rule, and it has the same name as -the rule, analogous to structural induction. - -However, this proof is rather terse. Here is a more readable version: -*} - -lemma assumes "(x,y) \ r*" and "(y,z) \ r*" shows "(x,z) \ r*" -using assms -proof induct - fix x assume "(x,z) \ r*" -- {*@{text B}[@{text y} := @{text x}]*} - thus "(x,z) \ r*" . -next - fix x' x y - assume 1: "(x',x) \ r" and - IH: "(y,z) \ r* \ (x,z) \ r*" and - B: "(y,z) \ r*" - from 1 IH[OF B] show "(x',z) \ r*" by(rule rtc.step) -qed -text{*\noindent -This time, merely for a change, we start the proof with by feeding both -assumptions into the inductive proof. Only the first assumption is -``consumed'' by the induction. -Since the second one is left over we don't just prove @{text ?thesis} but -@{text"(y,z) \ r* \ ?thesis"}, just as in the previous proof. -The base case is trivial. In the assumptions for the induction step we can -see very clearly how things fit together and permit ourselves the -obvious forward step @{text"IH[OF B]"}. - -The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} -is also supported for inductive definitions. The \emph{constructor} is the -name of the rule and the \emph{vars} fix the free variables in the -rule; the order of the \emph{vars} must correspond to the -left-to-right order of the variables as they appear in the rule. -For example, we could start the above detailed proof of the induction -with \isakeyword{case}~\isa{(step x' x y)}. In that case we don't need -to spell out the assumptions but can refer to them by @{text"step(.)"}, -although the resulting text will be quite cryptic. - -\subsection{More induction} - -We close the section by demonstrating how arbitrary induction -rules are applied. As a simple example we have chosen recursion -induction, i.e.\ induction based on a recursive function -definition. However, most of what we show works for induction in -general. - -The example is an unusual definition of rotation: *} - -fun rot :: "'a list \ 'a list" where -"rot [] = []" | -"rot [x] = [x]" | -"rot (x#y#zs) = y # rot(x#zs)" -text{*\noindent This yields, among other things, the induction rule -@{thm[source]rot.induct}: @{thm[display]rot.induct[no_vars]} -The following proof relies on a default naming scheme for cases: they are -called 1, 2, etc, unless they have been named explicitly. The latter happens -only with datatypes and inductively defined sets, but (usually) -not with recursive functions. *} - -lemma "xs \ [] \ rot xs = tl xs @ [hd xs]" -proof (induct xs rule: rot.induct) - case 1 thus ?case by simp -next - case 2 show ?case by simp -next - case (3 a b cs) - have "rot (a # b # cs) = b # rot(a # cs)" by simp - also have "\ = b # tl(a # cs) @ [hd(a # cs)]" by(simp add:3) - also have "\ = tl (a # b # cs) @ [hd (a # b # cs)]" by simp - finally show ?case . -qed - -text{*\noindent -The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01} -for how to reason with chains of equations) to demonstrate that the -\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} notation also -works for arbitrary induction theorems with numbered cases. The order -of the \emph{vars} corresponds to the order of the -@{text"\"}-quantified variables in each case of the induction -theorem. For induction theorems produced by \isakeyword{fun} it is -the order in which the variables appear on the left-hand side of the -equation. - -The proof is so simple that it can be condensed to -*} - -(*<*)lemma "xs \ [] \ rot xs = tl xs @ [hd xs]"(*>*) -by (induct xs rule: rot.induct) simp_all - -(*<*)end(*>*) -(* -lemma assumes A: "(\n. (\m. m < n \ P m) \ P n)" - shows "P(n::nat)" -proof (rule A) - show "\m. m < n \ P m" - proof (induct n) - case 0 thus ?case by simp - next - case (Suc n) -- {*\isakeyword{fix} @{term m} \isakeyword{assume} @{text Suc}: @{text[source]"?m < n \ P ?m"} @{prop[source]"m < Suc n"}*} - show ?case -- {*@{term ?case}*} - proof cases - assume eq: "m = n" - from Suc and A have "P n" by blast - with eq show "P m" by simp - next - assume "m \ n" - with Suc have "m < n" by arith - thus "P m" by(rule Suc) - qed - qed -qed -*) \ No newline at end of file diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/Logic.thy --- a/doc-src/IsarOverview/Isar/Logic.thy Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,714 +0,0 @@ -(*<*)theory Logic imports Main begin(*>*) - -section{*Logic \label{sec:Logic}*} - -subsection{*Propositional logic*} - -subsubsection{*Introduction rules*} - -text{* We start with a really trivial toy proof to introduce the basic -features of structured proofs. *} -lemma "A \ A" -proof (rule impI) - assume a: "A" - show "A" by(rule a) -qed -text{*\noindent -The operational reading: the \isakeyword{assume}-\isakeyword{show} -block proves @{prop"A \ A"} (@{term a} is a degenerate rule (no -assumptions) that proves @{term A} outright), which rule -@{thm[source]impI} (@{thm impI}) turns into the desired @{prop"A \ -A"}. However, this text is much too detailed for comfort. Therefore -Isar implements the following principle: \begin{quote}\em Command -\isakeyword{proof} automatically tries to select an introduction rule -based on the goal and a predefined list of rules. \end{quote} Here -@{thm[source]impI} is applied automatically: *} - -lemma "A \ A" -proof - assume a: A - show A by(rule a) -qed - -text{*\noindent As you see above, single-identifier formulae such as @{term A} -need not be enclosed in double quotes. However, we will continue to do so for -uniformity. - -Instead of applying fact @{text a} via the @{text rule} method, we can -also push it directly onto our goal. The proof is then immediate, -which is formally written as ``.'' in Isar: *} -lemma "A \ A" -proof - assume a: "A" - from a show "A" . -qed - -text{* We can also push several facts towards a goal, and put another -rule in between to establish some result that is one step further -removed. We illustrate this by introducing a trivial conjunction: *} -lemma "A \ A \ A" -proof - assume a: "A" - from a and a show "A \ A" by(rule conjI) -qed -text{*\noindent Rule @{thm[source]conjI} is of course @{thm conjI}. - -Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} -can be abbreviated to ``..'' if \emph{name} refers to one of the -predefined introduction rules (or elimination rules, see below): *} - -lemma "A \ A \ A" -proof - assume a: "A" - from a and a show "A \ A" .. -qed -text{*\noindent -This is what happens: first the matching introduction rule @{thm[source]conjI} -is applied (first ``.''), the remaining problem is solved immediately (second ``.''). *} - -subsubsection{*Elimination rules*} - -text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination: -@{thm[display,indent=5]conjE} In the following proof it is applied -by hand, after its first (\emph{major}) premise has been eliminated via -@{text"[OF ab]"}: *} -lemma "A \ B \ B \ A" -proof - assume ab: "A \ B" - show "B \ A" - proof (rule conjE[OF ab]) -- {*@{text"conjE[OF ab]"}: @{thm conjE[OF ab]} *} - assume a: "A" and b: "B" - from b and a show ?thesis .. - qed -qed -text{*\noindent Note that the term @{text"?thesis"} always stands for the -``current goal'', i.e.\ the enclosing \isakeyword{show} (or -\isakeyword{have}) statement. - -This is too much proof text. Elimination rules should be selected -automatically based on their major premise, the formula or rather connective -to be eliminated. In Isar they are triggered by facts being fed -\emph{into} a proof. Syntax: -\begin{center} -\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof} -\end{center} -where \emph{fact} stands for the name of a previously proved -proposition, e.g.\ an assumption, an intermediate result or some global -theorem, which may also be modified with @{text OF} etc. -The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it -how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, -an elimination rule (from a predefined list) is applied -whose first premise is solved by the \emph{fact}. Thus the proof above -is equivalent to the following one: *} - -lemma "A \ B \ B \ A" -proof - assume ab: "A \ B" - from ab show "B \ A" - proof - assume a: "A" and b: "B" - from b and a show ?thesis .. - qed -qed - -text{* Now we come to a second important principle: -\begin{quote}\em -Try to arrange the sequence of propositions in a UNIX-like pipe, -such that the proof of each proposition builds on the previous proposition. -\end{quote} -The previous proposition can be referred to via the fact @{text this}. -This greatly reduces the need for explicit naming of propositions. We also -rearrange the additional inner assumptions into proper order for immediate use: -*} -lemma "A \ B \ B \ A" -proof - assume "A \ B" - from this show "B \ A" - proof - assume "B" "A" - from this show ?thesis .. - qed -qed - -text{*\noindent Because of the frequency of \isakeyword{from}~@{text -this}, Isar provides two abbreviations: -\begin{center} -\begin{tabular}{r@ {\quad=\quad}l} -\isakeyword{then} & \isakeyword{from} @{text this} \\ -\isakeyword{thus} & \isakeyword{then} \isakeyword{show} -\end{tabular} -\end{center} - -Here is an alternative proof that operates purely by forward reasoning: *} -lemma "A \ B \ B \ A" -proof - assume ab: "A \ B" - from ab have a: "A" .. - from ab have b: "B" .. - from b a show "B \ A" .. -qed - -text{*\noindent It is worth examining this text in detail because it -exhibits a number of new concepts. For a start, it is the first time -we have proved intermediate propositions (\isakeyword{have}) on the -way to the final \isakeyword{show}. This is the norm in nontrivial -proofs where one cannot bridge the gap between the assumptions and the -conclusion in one step. To understand how the proof works we need to -explain more Isar details: -\begin{itemize} -\item -Method @{text rule} can be given a list of rules, in which case -@{text"(rule"}~\textit{rules}@{text")"} applies the first matching -rule in the list \textit{rules}. -\item Command \isakeyword{from} can be -followed by any number of facts. Given \isakeyword{from}~@{text -f}$_1$~\dots~@{text f}$_n$, the proof step -@{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have} -or \isakeyword{show} searches \textit{rules} for a rule whose first -$n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the -given order. -\item ``..'' is short for -@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnote{or -merely @{text"(rule"}~\textit{intro-rules}@{text")"} if there are no facts -fed into the proof}, where \textit{elim-rules} and \textit{intro-rules} -are the predefined elimination and introduction rule. Thus -elimination rules are tried first (if there are incoming facts). -\end{itemize} -Hence in the above proof both \isakeyword{have}s are proved via -@{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas -in the \isakeyword{show} step no elimination rule is applicable and -the proof succeeds with @{thm[source]conjI}. The latter would fail had -we written \isakeyword{from}~@{text"a b"} instead of -\isakeyword{from}~@{text"b a"}. - -A plain \isakeyword{proof} with no argument is short for -\isakeyword{proof}~@{text"(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnotemark[1]. -This means that the matching rule is selected by the incoming facts and the goal exactly as just explained. - -Although we have only seen a few introduction and elimination rules so -far, Isar's predefined rules include all the usual natural deduction -rules. We conclude our exposition of propositional logic with an extended -example --- which rules are used implicitly where? *} -lemma "\ (A \ B) \ \ A \ \ B" -proof - assume n: "\ (A \ B)" - show "\ A \ \ B" - proof (rule ccontr) - assume nn: "\ (\ A \ \ B)" - have "\ A" - proof - assume a: "A" - have "\ B" - proof - assume b: "B" - from a and b have "A \ B" .. - with n show False .. - qed - hence "\ A \ \ B" .. - with nn show False .. - qed - hence "\ A \ \ B" .. - with nn show False .. - qed -qed -text{*\noindent -Rule @{thm[source]ccontr} (``classical contradiction'') is -@{thm ccontr[no_vars]}. -Apart from demonstrating the strangeness of classical -arguments by contradiction, this example also introduces two new -abbreviations: -\begin{center} -\begin{tabular}{l@ {\quad=\quad}l} -\isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\ -\isakeyword{with}~\emph{facts} & -\isakeyword{from}~\emph{facts} @{text this} -\end{tabular} -\end{center} -*} - - -subsection{*Avoiding duplication*} - -text{* So far our examples have been a bit unnatural: normally we want to -prove rules expressed with @{text"\"}, not @{text"\"}. Here is an example: -*} -lemma "A \ B \ B \ A" -proof - assume "A \ B" thus "B" .. -next - assume "A \ B" thus "A" .. -qed -text{*\noindent The \isakeyword{proof} always works on the conclusion, -@{prop"B \ A"} in our case, thus selecting $\land$-introduction. Hence -we must show @{prop B} and @{prop A}; both are proved by -$\land$-elimination and the proofs are separated by \isakeyword{next}: -\begin{description} -\item[\isakeyword{next}] deals with multiple subgoals. For example, -when showing @{term"A \ B"} we need to show both @{term A} and @{term -B}. Each subgoal is proved separately, in \emph{any} order. The -individual proofs are separated by \isakeyword{next}. \footnote{Each -\isakeyword{show} must prove one of the pending subgoals. If a -\isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals -contain ?-variables, the first one is proved. Thus the order in which -the subgoals are proved can matter --- see -\S\ref{sec:CaseDistinction} for an example.} - -Strictly speaking \isakeyword{next} is only required if the subgoals -are proved in different assumption contexts which need to be -separated, which is not the case above. For clarity we -have employed \isakeyword{next} anyway and will continue to do so. -\end{description} - -This is all very well as long as formulae are small. Let us now look at some -devices to avoid repeating (possibly large) formulae. A very general method -is pattern matching: *} - -lemma "large_A \ large_B \ large_B \ large_A" - (is "?AB \ ?B \ ?A") -proof - assume "?AB" thus "?B" .. -next - assume "?AB" thus "?A" .. -qed -text{*\noindent Any formula may be followed by -@{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern -to be matched against the formula, instantiating the @{text"?"}-variables in -the pattern. Subsequent uses of these variables in other terms causes -them to be replaced by the terms they stand for. - -We can simplify things even more by stating the theorem by means of the -\isakeyword{assumes} and \isakeyword{shows} elements which allow direct -naming of assumptions: *} - -lemma assumes ab: "large_A \ large_B" - shows "large_B \ large_A" (is "?B \ ?A") -proof - from ab show "?B" .. -next - from ab show "?A" .. -qed -text{*\noindent Note the difference between @{text ?AB}, a term, and -@{text ab}, a fact. - -Finally we want to start the proof with $\land$-elimination so we -don't have to perform it twice, as above. Here is a slick way to -achieve this: *} - -lemma assumes ab: "large_A \ large_B" - shows "large_B \ large_A" (is "?B \ ?A") -using ab -proof - assume "?B" "?A" thus ?thesis .. -qed -text{*\noindent Command \isakeyword{using} can appear before a proof -and adds further facts to those piped into the proof. Here @{text ab} -is the only such fact and it triggers $\land$-elimination. Another -frequent idiom is as follows: -\begin{center} -\isakeyword{from} \emph{major-facts}~ -\isakeyword{show} \emph{proposition}~ -\isakeyword{using} \emph{minor-facts}~ -\emph{proof} -\end{center} - -Sometimes it is necessary to suppress the implicit application of rules in a -\isakeyword{proof}. For example \isakeyword{show(s)}~@{prop[source]"P \ Q"} -would trigger $\lor$-introduction, requiring us to prove @{prop P}, which may -not be what we had in mind. -A simple ``@{text"-"}'' prevents this \emph{faux pas}: *} - -lemma assumes ab: "A \ B" shows "B \ A" -proof - - from ab show ?thesis - proof - assume A thus ?thesis .. - next - assume B thus ?thesis .. - qed -qed -text{*\noindent Alternatively one can feed @{prop"A \ B"} directly -into the proof, thus triggering the elimination rule: *} -lemma assumes ab: "A \ B" shows "B \ A" -using ab -proof - assume A thus ?thesis .. -next - assume B thus ?thesis .. -qed -text{* \noindent Remember that eliminations have priority over -introductions. - -\subsection{Avoiding names} - -Too many names can easily clutter a proof. We already learned -about @{text this} as a means of avoiding explicit names. Another -handy device is to refer to a fact not by name but by contents: for -example, writing @{text "`A \ B`"} (enclosing the formula in back quotes) -refers to the fact @{text"A \ B"} -without the need to name it. Here is a simple example, a revised version -of the previous proof *} - -lemma assumes "A \ B" shows "B \ A" -using `A \ B` -(*<*)oops(*>*) -text{*\noindent which continues as before. - -Clearly, this device of quoting facts by contents is only advisable -for small formulae. In such cases it is superior to naming because the -reader immediately sees what the fact is without needing to search for -it in the preceding proof text. - -The assumptions of a lemma can also be referred to via their -predefined name @{text assms}. Hence the @{text"`A \ B`"} in the -previous proof can also be replaced by @{text assms}. Note that @{text -assms} refers to the list of \emph{all} assumptions. To pick out a -specific one, say the second, write @{text"assms(2)"}. - -This indexing notation $name(.)$ works for any $name$ that stands for -a list of facts, for example $f$@{text".simps"}, the equations of the -recursively defined function $f$. You may also select sublists by writing -$name(2-3)$. - -Above we recommended the UNIX-pipe model (i.e. @{text this}) to avoid -the need to name propositions. But frequently we needed to feed more -than one previously derived fact into a proof step. Then the UNIX-pipe -model appears to break down and we need to name the different facts to -refer to them. But this can be avoided: *} -lemma assumes "A \ B" shows "B \ A" -proof - - from `A \ B` have "B" .. - moreover - from `A \ B` have "A" .. - ultimately show "B \ A" .. -qed -text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term -An} into a sequence by separating their proofs with -\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands -for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to -introduce names for all of the sequence elements. - - -\subsection{Predicate calculus} - -Command \isakeyword{fix} introduces new local variables into a -proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\"} -(the universal quantifier at the -meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to -@{text"\"}. Here is a sample proof, annotated with the rules that are -applied implicitly: *} -lemma assumes P: "\x. P x" shows "\x. P(f x)" -proof --"@{thm[source]allI}: @{thm allI}" - fix a - from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE}" -qed -text{*\noindent Note that in the proof we have chosen to call the bound -variable @{term a} instead of @{term x} merely to show that the choice of -local names is irrelevant. - -Next we look at @{text"\"} which is a bit more tricky. -*} - -lemma assumes Pf: "\x. P(f x)" shows "\y. P y" -proof - - from Pf show ?thesis - proof -- "@{thm[source]exE}: @{thm exE}" - fix x - assume "P(f x)" - thus ?thesis .. -- "@{thm[source]exI}: @{thm exI}" - qed -qed -text{*\noindent Explicit $\exists$-elimination as seen above can become -cumbersome in practice. The derived Isar language element -\isakeyword{obtain} provides a more appealing form of generalised -existence reasoning: *} - -lemma assumes Pf: "\x. P(f x)" shows "\y. P y" -proof - - from Pf obtain x where "P(f x)" .. - thus "\y. P y" .. -qed -text{*\noindent Note how the proof text follows the usual mathematical style -of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ -as a new local variable. Technically, \isakeyword{obtain} is similar to -\isakeyword{fix} and \isakeyword{assume} together with a soundness proof of -the elimination involved. - -Here is a proof of a well known tautology. -Which rule is used where? *} - -lemma assumes ex: "\x. \y. P x y" shows "\y. \x. P x y" -proof - fix y - from ex obtain x where "\y. P x y" .. - hence "P x y" .. - thus "\x. P x y" .. -qed - -subsection{*Making bigger steps*} - -text{* So far we have confined ourselves to single step proofs. Of course -powerful automatic methods can be used just as well. Here is an example, -Cantor's theorem that there is no surjective function from a set to its -powerset: *} -theorem "\S. S \ range (f :: 'a \ 'a set)" -proof - let ?S = "{x. x \ f x}" - show "?S \ range f" - proof - assume "?S \ range f" - then obtain y where "?S = f y" .. - show False - proof cases - assume "y \ ?S" - with `?S = f y` show False by blast - next - assume "y \ ?S" - with `?S = f y` show False by blast - qed - qed -qed -text{*\noindent -For a start, the example demonstrates two new constructs: -\begin{itemize} -\item \isakeyword{let} introduces an abbreviation for a term, in our case -the witness for the claim. -\item Proof by @{text"cases"} starts a proof by cases. Note that it remains -implicit what the two cases are: it is merely expected that the two subproofs -prove @{text"P \ ?thesis"} and @{text"\P \ ?thesis"} (in that order) -for some @{term P}. -\end{itemize} -If you wonder how to \isakeyword{obtain} @{term y}: -via the predefined elimination rule @{thm rangeE[no_vars]}. - -Method @{text blast} is used because the contradiction does not follow easily -by just a single rule. If you find the proof too cryptic for human -consumption, here is a more detailed version; the beginning up to -\isakeyword{obtain} stays unchanged. *} - -theorem "\S. S \ range (f :: 'a \ 'a set)" -proof - let ?S = "{x. x \ f x}" - show "?S \ range f" - proof - assume "?S \ range f" - then obtain y where "?S = f y" .. - show False - proof cases - assume "y \ ?S" - hence "y \ f y" by simp - hence "y \ ?S" by(simp add: `?S = f y`) - with `y \ ?S` show False by contradiction - next - assume "y \ ?S" - hence "y \ f y" by simp - hence "y \ ?S" by(simp add: `?S = f y`) - with `y \ ?S` show False by contradiction - qed - qed -qed -text{*\noindent Method @{text contradiction} succeeds if both $P$ and -$\neg P$ are among the assumptions and the facts fed into that step, in any order. - -As it happens, Cantor's theorem can be proved automatically by best-first -search. Depth-first search would diverge, but best-first search successfully -navigates through the large search space: -*} - -theorem "\S. S \ range (f :: 'a \ 'a set)" -by best -(* Of course this only works in the context of HOL's carefully -constructed introduction and elimination rules for set theory.*) - -subsection{*Raw proof blocks*} - -text{* Although we have shown how to employ powerful automatic methods like -@{text blast} to achieve bigger proof steps, there may still be the -tendency to use the default introduction and elimination rules to -decompose goals and facts. This can lead to very tedious proofs: -*} -lemma "\x y. A x y \ B x y \ C x y" -proof - fix x show "\y. A x y \ B x y \ C x y" - proof - fix y show "A x y \ B x y \ C x y" - proof - assume "A x y \ B x y" - show "C x y" sorry - qed - qed -qed -text{*\noindent Since we are only interested in the decomposition and not the -actual proof, the latter has been replaced by -\isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is -only allowed in quick and dirty mode, the default interactive mode. It -is very convenient for top down proof development. - -Luckily we can avoid this step by step decomposition very easily: *} - -lemma "\x y. A x y \ B x y \ C x y" -proof - - have "\x y. \ A x y; B x y \ \ C x y" - proof - - fix x y assume "A x y" "B x y" - show "C x y" sorry - qed - thus ?thesis by blast -qed - -text{*\noindent -This can be simplified further by \emph{raw proof blocks}, i.e.\ -proofs enclosed in braces: *} - -lemma "\x y. A x y \ B x y \ C x y" -proof - - { fix x y assume "A x y" "B x y" - have "C x y" sorry } - thus ?thesis by blast -qed - -text{*\noindent The result of the raw proof block is the same theorem -as above, namely @{prop"\x y. \ A x y; B x y \ \ C x y"}. Raw -proof blocks are like ordinary proofs except that they do not prove -some explicitly stated property but that the property emerges directly -out of the \isakeyword{fixe}s, \isakeyword{assume}s and -\isakeyword{have} in the block. Thus they again serve to avoid -duplication. Note that the conclusion of a raw proof block is stated with -\isakeyword{have} rather than \isakeyword{show} because it is not the -conclusion of some pending goal but some independent claim. - -The general idea demonstrated in this subsection is very -important in Isar and distinguishes it from \isa{apply}-style proofs: -\begin{quote}\em -Do not manipulate the proof state into a particular form by applying -proof methods but state the desired form explicitly and let the proof -methods verify that from this form the original goal follows. -\end{quote} -This yields more readable and also more robust proofs. - -\subsubsection{General case distinctions} - -As an important application of raw proof blocks we show how to deal -with general case distinctions --- more specific kinds are treated in -\S\ref{sec:CaseDistinction}. Imagine that you would like to prove some -goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that -the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and -that each case $P_i$ implies the goal. Taken together, this proves the -goal. The corresponding Isar proof pattern (for $n = 3$) is very handy: -*} -text_raw{*\renewcommand{\isamarkupcmt}[1]{#1}*} -(*<*)lemma "XXX"(*>*) -proof - - have "P\<^isub>1 \ P\<^isub>2 \ P\<^isub>3" (*<*)sorry(*>*) -- {*\dots*} - moreover - { assume P\<^isub>1 - -- {*\dots*} - have ?thesis (*<*)sorry(*>*) -- {*\dots*} } - moreover - { assume P\<^isub>2 - -- {*\dots*} - have ?thesis (*<*)sorry(*>*) -- {*\dots*} } - moreover - { assume P\<^isub>3 - -- {*\dots*} - have ?thesis (*<*)sorry(*>*) -- {*\dots*} } - ultimately show ?thesis by blast -qed -text_raw{*\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}*} - - -subsection{*Further refinements*} - -text{* This subsection discusses some further tricks that can make -life easier although they are not essential. *} - -subsubsection{*\isakeyword{and}*} - -text{* Propositions (following \isakeyword{assume} etc) may but need not be -separated by \isakeyword{and}. This is not just for readability -(\isakeyword{from} \isa{A} \isakeyword{and} \isa{B} looks nicer than -\isakeyword{from} \isa{A} \isa{B}) but for structuring lists of propositions -into possibly named blocks. In -\begin{center} -\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$ -\isakeyword{and} $A_4$ -\end{center} -label \isa{A} refers to the list of propositions $A_1$ $A_2$ and -label \isa{B} to $A_3$. *} - -subsubsection{*\isakeyword{note}*} -text{* If you want to remember intermediate fact(s) that cannot be -named directly, use \isakeyword{note}. For example the result of raw -proof block can be named by following it with -\isakeyword{note}~@{text"some_name = this"}. As a side effect, -@{text this} is set to the list of facts on the right-hand side. You -can also say @{text"note some_fact"}, which simply sets @{text this}, -i.e.\ recalls @{text"some_fact"}, e.g.\ in a \isakeyword{moreover} sequence. *} - - -subsubsection{*\isakeyword{fixes}*} - -text{* Sometimes it is necessary to decorate a proposition with type -constraints, as in Cantor's theorem above. These type constraints tend -to make the theorem less readable. The situation can be improved a -little by combining the type constraint with an outer @{text"\"}: *} - -theorem "\f :: 'a \ 'a set. \S. S \ range f" -(*<*)oops(*>*) -text{*\noindent However, now @{term f} is bound and we need a -\isakeyword{fix}~\isa{f} in the proof before we can refer to @{term f}. -This is avoided by \isakeyword{fixes}: *} - -theorem fixes f :: "'a \ 'a set" shows "\S. S \ range f" -(*<*)oops(*>*) -text{* \noindent -Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:*} - -lemma comm_mono: - fixes r :: "'a \ 'a \ bool" (infix ">" 60) and - f :: "'a \ 'a \ 'a" (infixl "++" 70) - assumes comm: "\x y::'a. x ++ y = y ++ x" and - mono: "\x y z::'a. x > y \ x ++ z > y ++ z" - shows "x > y \ z ++ x > z ++ y" -by(simp add: comm mono) - -text{*\noindent The concrete syntax is dropped at the end of the proof and the -theorem becomes @{thm[display,margin=60]comm_mono} -\tweakskip *} - -subsubsection{*\isakeyword{obtain}*} - -text{* The \isakeyword{obtain} construct can introduce multiple -witnesses and propositions as in the following proof fragment:*} - -lemma assumes A: "\x y. P x y \ Q x y" shows "R" -proof - - from A obtain x y where P: "P x y" and Q: "Q x y" by blast -(*<*)oops(*>*) -text{* Remember also that one does not even need to start with a formula -containing @{text"\"} as we saw in the proof of Cantor's theorem. -*} - -subsubsection{*Combining proof styles*} - -text{* Finally, whole \isa{apply}-scripts may appear in the leaves of the -proof tree, although this is best avoided. Here is a contrived example: *} - -lemma "A \ (A \ B) \ B" -proof - assume a: "A" - show "(A \B) \ B" - apply(rule impI) - apply(erule impE) - apply(rule a) - apply assumption - done -qed - -text{*\noindent You may need to resort to this technique if an -automatic step fails to prove the desired proposition. - -When converting a proof from \isa{apply}-style into Isar you can proceed -in a top-down manner: parts of the proof can be left in script form -while the outer structure is already expressed in Isar. *} - -(*<*)end(*>*) diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/ROOT.ML --- a/doc-src/IsarOverview/Isar/ROOT.ML Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -quick_and_dirty := true; - -use_thys ["Logic", "Induction"]; diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/Induction.tex --- a/doc-src/IsarOverview/Isar/document/Induction.tex Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,718 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Induction}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{Case distinction and induction \label{sec:Induct}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Computer science applications abound with inductively defined -structures, which is why we treat them in more detail. HOL already -comes with a datatype of lists with the two constructors \isa{Nil} -and \isa{Cons}. \isa{Nil} is written \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and \isa{Cons\ x\ xs} is written \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Case distinction\label{sec:CaseDistinction}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -We have already met the \isa{cases} method for performing -binary case splits. Here is another example:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ cases\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isaliteral{28}{\isacharparenleft}}rule\ case{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{29}{\isacharparenright}}} where -\isa{case{\isaliteral{5F}{\isacharunderscore}}split} is \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}. If we reverse -the order of the two cases in the proof, the first case would prove -\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A} which would solve the first premise of -\isa{case{\isaliteral{5F}{\isacharunderscore}}split}, instantiating \isa{{\isaliteral{3F}{\isacharquery}}P} with \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A}, thus making the second premise \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A}. -Therefore the order of subgoals is not always completely arbitrary. - -The above proof is appropriate if \isa{A} is textually small. -However, if \isa{A} is large, we do not want to repeat it. This can -be avoided by the following idiom% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ True\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ False\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent which is like the previous proof but instantiates -\isa{{\isaliteral{3F}{\isacharquery}}P} right away with \isa{A}. Thus we could prove the two -cases in any order. The phrase \isakeyword{case}~\isa{True} -abbreviates \isakeyword{assume}~\isa{True{\isaliteral{3A}{\isacharcolon}}\ A} and analogously for -\isa{False} and \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A}. - -The same game can be played with other datatypes, for example lists, -where \isa{tl} is the tail of a list, and \isa{length} returns a -natural number (remember: $0-1=0$):% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}length{\isaliteral{28}{\isacharparenleft}}tl\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ length\ xs\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ Nil\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ Cons\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Here \isakeyword{case}~\isa{Nil} abbreviates -\isakeyword{assume}~\isa{Nil{\isaliteral{3A}{\isacharcolon}}}~\isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and -\isakeyword{case}~\isa{Cons} abbreviates \isakeyword{fix}~\isa{{\isaliteral{3F}{\isacharquery}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{3F}{\isacharquery}}} -\isakeyword{assume}~\isa{Cons{\isaliteral{3A}{\isacharcolon}}}~\isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}\ {\isaliteral{23}{\isacharhash}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{3F}{\isacharquery}}}, -where \isa{{\isaliteral{3F}{\isacharquery}}} and \isa{{\isaliteral{3F}{\isacharquery}}{\isaliteral{3F}{\isacharquery}}} -stand for variable names that have been chosen by the system. -Therefore we cannot refer to them. -Luckily, this proof is simple enough we do not need to refer to them. -However, sometimes one may have to. Hence Isar offers a simple scheme for -naming those variables: replace the anonymous \isa{Cons} by -\isa{{\isaliteral{28}{\isacharparenleft}}Cons\ y\ ys{\isaliteral{29}{\isacharparenright}}}, which abbreviates \isakeyword{fix}~\isa{y\ ys} -\isakeyword{assume}~\isa{Cons{\isaliteral{3A}{\isacharcolon}}}~\isa{xs\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys}. -In each \isakeyword{case} the assumption can be -referred to inside the proof by the name of the constructor. In -Section~\ref{sec:full-Ind} below we will come across an example -of this. - -\subsection{Structural induction} - -We start with an inductive proof where both cases are proved automatically:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The constraint \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat} is needed because all of -the operations involved are overloaded. -This proof also demonstrates that \isakeyword{by} can take two arguments, -one to start and one to finish the proof --- the latter is optional. - -If we want to expose more of the structure of the -proof, we can use pattern matching to avoid having to repeat the goal -statement:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{5C3C6C653E}{\isasymle}}n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ n\ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent We could refine this further to show more of the equational -proof. Instead we explore the same avenue as for case distinctions: -introducing context via the \isakeyword{case} command:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}i{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n{\isaliteral{2E}{\isachardot}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ Suc\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The implicitly defined \isa{{\isaliteral{3F}{\isacharquery}}case} refers to the -corresponding case to be proved, i.e.\ \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isadigit{0}}} in the first case and -\isa{{\isaliteral{3F}{\isacharquery}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}} in the second case. Context \isakeyword{case}~\isa{{\isadigit{0}}} is -empty whereas \isakeyword{case}~\isa{Suc} assumes \isa{{\isaliteral{3F}{\isacharquery}}P\ n}. Again we -have the same problem as with case distinctions: we cannot refer to an anonymous \isa{n} -in the induction step because it has not been introduced via \isakeyword{fix} -(in contrast to the previous proof). The solution is the one outlined for -\isa{Cons} above: replace \isa{Suc} by \isa{{\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{fixes}\ n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{2A}{\isacharasterisk}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isadigit{0}}\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}Suc\ i{\isaliteral{29}{\isacharparenright}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ i\ {\isaliteral{3C}{\isacharless}}\ Suc\ i\ {\isaliteral{2A}{\isacharasterisk}}\ Suc\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Of course we could again have written -\isakeyword{thus}~\isa{{\isaliteral{3F}{\isacharquery}}case} instead of giving the term explicitly -but we wanted to use \isa{i} somewhere. - -\subsection{Generalization via \isa{arbitrary}} - -It is frequently necessary to generalize a claim before it becomes -provable by induction. The tutorial~\cite{LNCS2283} demonstrates this -with \isa{itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys}, where \isa{ys} -needs to be universally quantified before induction succeeds.\footnote{\isa{rev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}},\quad \isa{rev\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}},\\ \isa{itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys},\quad \isa{itrev\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}}} But -strictly speaking, this quantification step is already part of the -proof and the quantifiers should not clutter the original claim. This -is how the quantification step can be combined with induction:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The annotation \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}}~\emph{vars} -universally quantifies all \emph{vars} before the induction. Hence -they can be replaced by \emph{arbitrary} values in the proof. - -Generalization via \isa{arbitrary} is particularly convenient -if the induction step is a structured proof as opposed to the automatic -example above. Then the claim is available in unquantified form but -with the generalized variables replaced by \isa{{\isaliteral{3F}{\isacharquery}}}-variables, ready -for instantiation. In the above example, in the \isa{Cons} case the -induction hypothesis is \isa{itrev\ xs\ {\isaliteral{3F}{\isacharquery}}ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{3F}{\isacharquery}}ys} (available -under the name \isa{Cons}). - - -\subsection{Inductive proofs of conditional formulae} -\label{sec:full-Ind} - -Induction also copes well with formulae involving \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, for example% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ xs{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent This is an improvement over that style the -tutorial~\cite{LNCS2283} advises, which requires \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. -A further improvement is shown in the following proof:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \ {\isaliteral{22}{\isachardoublequoteopen}}map\ f\ xs\ {\isaliteral{3D}{\isacharequal}}\ map\ f\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ length\ xs\ {\isaliteral{3D}{\isacharequal}}\ length\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ ys\ arbitrary{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ Nil\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ ys{\isaliteral{29}{\isacharparenright}}\ \ \isacommand{note}\isamarkupfalse% -\ Asm\ {\isaliteral{3D}{\isacharequal}}\ Cons\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}cases\ xs{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{case}\isamarkupfalse% -\ Nil\isanewline -\ \ \ \ \isacommand{hence}\isamarkupfalse% -\ False\ \isacommand{using}\isamarkupfalse% -\ Asm{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{next}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{case}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{with}\isamarkupfalse% -\ Asm{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}map\ f\ xs{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ map\ f\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \isacommand{from}\isamarkupfalse% -\ Asm{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}OF\ this{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{60}{\isacharbackquoteopen}}xs\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{23}{\isacharhash}}xs{\isaliteral{27}{\isacharprime}}{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -The base case is trivial. In the step case Isar assumes -(under the name \isa{Cons}) two propositions: -\begin{center} -\begin{tabular}{l} -\isa{map\ f\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3D}{\isacharequal}}\ map\ f\ ys\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ length\ {\isaliteral{3F}{\isacharquery}}xs\ {\isaliteral{3D}{\isacharequal}}\ length\ ys}\\ -\isa{map\ f\ xs\ {\isaliteral{3D}{\isacharequal}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}} -\end{tabular} -\end{center} -The first is the induction hypothesis, the second, and this is new, -is the premise of the induction step. The actual goal at this point is merely -\isa{length\ xs\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}}. The assumptions are given the new name -\isa{Asm} to avoid a name clash further down. The proof procedes with a case distinction on \isa{xs}. In the case \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, the second of our two -assumptions (\isa{Asm{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}) implies the contradiction \isa{{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}}. - In the case \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{27}{\isacharprime}}}, we first obtain -\isa{map\ f\ xs{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ map\ f\ ys}, from which a forward step with the first assumption (\isa{Asm{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}OF\ this{\isaliteral{5D}{\isacharbrackright}}}) yields \isa{length\ xs{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ length\ ys}. Together -with \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ xs} this yields the goal -\isa{length\ xs\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}}. - - -\subsection{Induction formulae involving \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} or \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}} - -Let us now consider abstractly the situation where the goal to be proved -contains both \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, say \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ x}. -This means that in each case of the induction, -\isa{{\isaliteral{3F}{\isacharquery}}case} would be of the form \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{27}{\isacharprime}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}\ x}. Thus the -first proof steps will be the canonical ones, fixing \isa{x} and assuming -\isa{P{\isaliteral{27}{\isacharprime}}\ x}. To avoid this tedium, induction performs the canonical steps -automatically: in each step case, the assumptions contain both the -usual induction hypothesis and \isa{P{\isaliteral{27}{\isacharprime}}\ x}, whereas \isa{{\isaliteral{3F}{\isacharquery}}case} is only -\isa{Q{\isaliteral{27}{\isacharprime}}\ x}. - -\subsection{Rule induction} - -HOL also supports inductively defined sets. See \cite{LNCS2283} -for details. As an example we define our own version of the reflexive -transitive closure of a relation --- HOL provides a predefined one as well.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% -\isanewline -\ \ rtc\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isakeyword{for}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\isakeyword{where}\isanewline -\ \ refl{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -{\isaliteral{7C}{\isacharbar}}\ step{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}% -\begin{isamarkuptext}% -\noindent -First the constant is declared as a function on binary -relations (with concrete syntax \isa{r{\isaliteral{2A}{\isacharasterisk}}} instead of \isa{rtc\ r}), then the defining clauses are given. We will now prove that -\isa{r{\isaliteral{2A}{\isacharasterisk}}} is indeed transitive:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ A{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{using}\isamarkupfalse% -\ A\isanewline -\isacommand{proof}\isamarkupfalse% -\ induct\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ refl\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ step\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{3A}{\isacharcolon}}\ rtc{\isaliteral{2E}{\isachardot}}step{\isaliteral{29}{\isacharparenright}}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) -\in R$ piped into the proof, here \isakeyword{using}~\isa{A}. The -proof itself follows the inductive definition very -closely: there is one case for each rule, and it has the same name as -the rule, analogous to structural induction. - -However, this proof is rather terse. Here is a more readable version:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{using}\isamarkupfalse% -\ assms\isanewline -\isacommand{proof}\isamarkupfalse% -\ induct\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x\ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ % -\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]% -} -\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x{\isaliteral{27}{\isacharprime}}\ x\ y\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline -\ \ \ \ \ \ \ \ \ IH{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline -\ \ \ \ \ \ \ \ \ B{\isaliteral{3A}{\isacharcolon}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ {\isadigit{1}}\ IH{\isaliteral{5B}{\isacharbrackleft}}OF\ B{\isaliteral{5D}{\isacharbrackright}}\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ rtc{\isaliteral{2E}{\isachardot}}step{\isaliteral{29}{\isacharparenright}}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -This time, merely for a change, we start the proof with by feeding both -assumptions into the inductive proof. Only the first assumption is -``consumed'' by the induction. -Since the second one is left over we don't just prove \isa{{\isaliteral{3F}{\isacharquery}}thesis} but -\isa{{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{2C}{\isacharcomma}}z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}thesis}, just as in the previous proof. -The base case is trivial. In the assumptions for the induction step we can -see very clearly how things fit together and permit ourselves the -obvious forward step \isa{IH{\isaliteral{5B}{\isacharbrackleft}}OF\ B{\isaliteral{5D}{\isacharbrackright}}}. - -The notation \isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} -is also supported for inductive definitions. The \emph{constructor} is the -name of the rule and the \emph{vars} fix the free variables in the -rule; the order of the \emph{vars} must correspond to the -left-to-right order of the variables as they appear in the rule. -For example, we could start the above detailed proof of the induction -with \isakeyword{case}~\isa{(step x' x y)}. In that case we don't need -to spell out the assumptions but can refer to them by \isa{step{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{29}{\isacharparenright}}}, -although the resulting text will be quite cryptic. - -\subsection{More induction} - -We close the section by demonstrating how arbitrary induction -rules are applied. As a simple example we have chosen recursion -induction, i.e.\ induction based on a recursive function -definition. However, most of what we show works for induction in -general. - -The example is an unusual definition of rotation:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{fun}\isamarkupfalse% -\ rot\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}rot\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}rot\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}rot\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{23}{\isacharhash}}\ rot{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% -\begin{isamarkuptext}% -\noindent This yields, among other things, the induction rule -\isa{rot{\isaliteral{2E}{\isachardot}}induct}: \begin{isabelle}% -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ zs{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ a{\isadigit{0}}% -\end{isabelle} -The following proof relies on a default naming scheme for cases: they are -called 1, 2, etc, unless they have been named explicitly. The latter happens -only with datatypes and inductively defined sets, but (usually) -not with recursive functions.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ rot\ xs\ {\isaliteral{3D}{\isacharequal}}\ tl\ xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}hd\ xs{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ rule{\isaliteral{3A}{\isacharcolon}}\ rot{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isadigit{1}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isadigit{2}}\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{case}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ a\ b\ cs{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}rot\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ b\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ rot{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{23}{\isacharhash}}\ tl{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}hd{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ tl\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ b\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}hd\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ b\ {\isaliteral{23}{\isacharhash}}\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \isacommand{finally}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}case\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -The third case is only shown in gory detail (see \cite{BauerW-TPHOLs01} -for how to reason with chains of equations) to demonstrate that the -\isakeyword{case}~\isa{(}\emph{constructor} \emph{vars}\isa{)} notation also -works for arbitrary induction theorems with numbered cases. The order -of the \emph{vars} corresponds to the order of the -\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-quantified variables in each case of the induction -theorem. For induction theorems produced by \isakeyword{fun} it is -the order in which the variables appear on the left-hand side of the -equation. - -The proof is so simple that it can be condensed to% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}induct\ xs\ rule{\isaliteral{3A}{\isacharcolon}}\ rot{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/Logic.tex --- a/doc-src/IsarOverview/Isar/document/Logic.tex Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1688 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Logic}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\isamarkupsection{Logic \label{sec:Logic}% -} -\isamarkuptrue% -% -\isamarkupsubsection{Propositional logic% -} -\isamarkuptrue% -% -\isamarkupsubsubsection{Introduction rules% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -We start with a really trivial toy proof to introduce the basic -features of structured proofs.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -The operational reading: the \isakeyword{assume}-\isakeyword{show} -block proves \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} (\isa{a} is a degenerate rule (no -assumptions) that proves \isa{A} outright), which rule -\isa{impI} (\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}) turns into the desired \isa{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A}. However, this text is much too detailed for comfort. Therefore -Isar implements the following principle: \begin{quote}\em Command -\isakeyword{proof} automatically tries to select an introduction rule -based on the goal and a predefined list of rules. \end{quote} Here -\isa{impI} is applied automatically:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ A\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent As you see above, single-identifier formulae such as \isa{A} -need not be enclosed in double quotes. However, we will continue to do so for -uniformity. - -Instead of applying fact \isa{a} via the \isa{rule} method, we can -also push it directly onto our goal. The proof is then immediate, -which is formally written as ``.'' in Isar:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -We can also push several facts towards a goal, and put another -rule in between to establish some result that is one step further -removed. We illustrate this by introducing a trivial conjunction:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ a\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ conjI{\isaliteral{29}{\isacharparenright}}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Rule \isa{conjI} is of course \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q}. - -Proofs of the form \isakeyword{by}\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\emph{name}\isa{{\isaliteral{29}{\isacharparenright}}} -can be abbreviated to ``..'' if \emph{name} refers to one of the -predefined introduction rules (or elimination rules, see below):% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ a\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -This is what happens: first the matching introduction rule \isa{conjI} -is applied (first ``.''), the remaining problem is solved immediately (second ``.'').% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Elimination rules% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -A typical elimination rule is \isa{conjE}, $\land$-elimination: -\begin{isabelle}% -\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R% -\end{isabelle} In the following proof it is applied -by hand, after its first (\emph{major}) premise has been eliminated via -\isa{{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}rule\ conjE{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ % -\isamarkupcmt{\isa{conjE{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}}: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A{\isaliteral{3B}{\isacharsemicolon}}\ B{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R}% -} -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{from}\isamarkupfalse% -\ b\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Note that the term \isa{{\isaliteral{3F}{\isacharquery}}thesis} always stands for the -``current goal'', i.e.\ the enclosing \isakeyword{show} (or -\isakeyword{have}) statement. - -This is too much proof text. Elimination rules should be selected -automatically based on their major premise, the formula or rather connective -to be eliminated. In Isar they are triggered by facts being fed -\emph{into} a proof. Syntax: -\begin{center} -\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof} -\end{center} -where \emph{fact} stands for the name of a previously proved -proposition, e.g.\ an assumption, an intermediate result or some global -theorem, which may also be modified with \isa{OF} etc. -The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it -how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, -an elimination rule (from a predefined list) is applied -whose first premise is solved by the \emph{fact}. Thus the proof above -is equivalent to the following one:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{from}\isamarkupfalse% -\ b\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -Now we come to a second important principle: -\begin{quote}\em -Try to arrange the sequence of propositions in a UNIX-like pipe, -such that the proof of each proposition builds on the previous proposition. -\end{quote} -The previous proposition can be referred to via the fact \isa{this}. -This greatly reduces the need for explicit naming of propositions. We also -rearrange the additional inner assumptions into proper order for immediate use:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ this\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{from}\isamarkupfalse% -\ this\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations: -\begin{center} -\begin{tabular}{r@ {\quad=\quad}l} -\isakeyword{then} & \isakeyword{from} \isa{this} \\ -\isakeyword{thus} & \isakeyword{then} \isakeyword{show} -\end{tabular} -\end{center} - -Here is an alternative proof that operates purely by forward reasoning:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{have}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{have}\isamarkupfalse% -\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ b\ a\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent It is worth examining this text in detail because it -exhibits a number of new concepts. For a start, it is the first time -we have proved intermediate propositions (\isakeyword{have}) on the -way to the final \isakeyword{show}. This is the norm in nontrivial -proofs where one cannot bridge the gap between the assumptions and the -conclusion in one step. To understand how the proof works we need to -explain more Isar details: -\begin{itemize} -\item -Method \isa{rule} can be given a list of rules, in which case -\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{rules}\isa{{\isaliteral{29}{\isacharparenright}}} applies the first matching -rule in the list \textit{rules}. -\item Command \isakeyword{from} can be -followed by any number of facts. Given \isakeyword{from}~\isa{f}$_1$~\dots~\isa{f}$_n$, the proof step -\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{rules}\isa{{\isaliteral{29}{\isacharparenright}}} following a \isakeyword{have} -or \isakeyword{show} searches \textit{rules} for a rule whose first -$n$ premises can be proved by \isa{f}$_1$~\dots~\isa{f}$_n$ in the -given order. -\item ``..'' is short for -\isa{by{\isaliteral{28}{\isacharparenleft}}rule}~\textit{elim-rules intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}}\footnote{or -merely \isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}} if there are no facts -fed into the proof}, where \textit{elim-rules} and \textit{intro-rules} -are the predefined elimination and introduction rule. Thus -elimination rules are tried first (if there are incoming facts). -\end{itemize} -Hence in the above proof both \isakeyword{have}s are proved via -\isa{conjE} triggered by \isakeyword{from}~\isa{ab} whereas -in the \isakeyword{show} step no elimination rule is applicable and -the proof succeeds with \isa{conjI}. The latter would fail had -we written \isakeyword{from}~\isa{a\ b} instead of -\isakeyword{from}~\isa{b\ a}. - -A plain \isakeyword{proof} with no argument is short for -\isakeyword{proof}~\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{elim-rules intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}}\footnotemark[1]. -This means that the matching rule is selected by the incoming facts and the goal exactly as just explained. - -Although we have only seen a few introduction and elimination rules so -far, Isar's predefined rules include all the usual natural deduction -rules. We conclude our exposition of propositional logic with an extended -example --- which rules are used implicitly where?% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ n{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\ {\isaliteral{28}{\isacharparenleft}}rule\ ccontr{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ nn{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ a\ \isakeyword{and}\ b\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ n\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ nn\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{with}\isamarkupfalse% -\ nn\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -Rule \isa{ccontr} (``classical contradiction'') is -\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P}. -Apart from demonstrating the strangeness of classical -arguments by contradiction, this example also introduces two new -abbreviations: -\begin{center} -\begin{tabular}{l@ {\quad=\quad}l} -\isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\ -\isakeyword{with}~\emph{facts} & -\isakeyword{from}~\emph{facts} \isa{this} -\end{tabular} -\end{center}% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Avoiding duplication% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -So far our examples have been a bit unnatural: normally we want to -prove rules expressed with \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, not \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. Here is an example:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The \isakeyword{proof} always works on the conclusion, -\isa{B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} in our case, thus selecting $\land$-introduction. Hence -we must show \isa{B} and \isa{A}; both are proved by -$\land$-elimination and the proofs are separated by \isakeyword{next}: -\begin{description} -\item[\isakeyword{next}] deals with multiple subgoals. For example, -when showing \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B} we need to show both \isa{A} and \isa{B}. Each subgoal is proved separately, in \emph{any} order. The -individual proofs are separated by \isakeyword{next}. \footnote{Each -\isakeyword{show} must prove one of the pending subgoals. If a -\isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals -contain ?-variables, the first one is proved. Thus the order in which -the subgoals are proved can matter --- see -\S\ref{sec:CaseDistinction} for an example.} - -Strictly speaking \isakeyword{next} is only required if the subgoals -are proved in different assumption contexts which need to be -separated, which is not the case above. For clarity we -have employed \isakeyword{next} anyway and will continue to do so. -\end{description} - -This is all very well as long as formulae are small. Let us now look at some -devices to avoid repeating (possibly large) formulae. A very general method -is pattern matching:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Any formula may be followed by -\isa{{\isaliteral{28}{\isacharparenleft}}}\isakeyword{is}~\emph{pattern}\isa{{\isaliteral{29}{\isacharparenright}}} which causes the pattern -to be matched against the formula, instantiating the \isa{{\isaliteral{3F}{\isacharquery}}}-variables in -the pattern. Subsequent uses of these variables in other terms causes -them to be replaced by the terms they stand for. - -We can simplify things even more by stating the theorem by means of the -\isakeyword{assumes} and \isakeyword{shows} elements which allow direct -naming of assumptions:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Note the difference between \isa{{\isaliteral{3F}{\isacharquery}}AB}, a term, and -\isa{ab}, a fact. - -Finally we want to start the proof with $\land$-elimination so we -don't have to perform it twice, as above. Here is a slick way to -achieve this:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{using}\isamarkupfalse% -\ ab\isanewline -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Command \isakeyword{using} can appear before a proof -and adds further facts to those piped into the proof. Here \isa{ab} -is the only such fact and it triggers $\land$-elimination. Another -frequent idiom is as follows: -\begin{center} -\isakeyword{from} \emph{major-facts}~ -\isakeyword{show} \emph{proposition}~ -\isakeyword{using} \emph{minor-facts}~ -\emph{proof} -\end{center} - -Sometimes it is necessary to suppress the implicit application of rules in a -\isakeyword{proof}. For example \isakeyword{show(s)}~\isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} -would trigger $\lor$-introduction, requiring us to prove \isa{P}, which may -not be what we had in mind. -A simple ``\isa{{\isaliteral{2D}{\isacharminus}}}'' prevents this \emph{faux pas}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ab\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ A\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{next}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ B\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Alternatively one can feed \isa{A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B} directly -into the proof, thus triggering the elimination rule:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{using}\isamarkupfalse% -\ ab\isanewline -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ A\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ B\ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Remember that eliminations have priority over -introductions. - -\subsection{Avoiding names} - -Too many names can easily clutter a proof. We already learned -about \isa{this} as a means of avoiding explicit names. Another -handy device is to refer to a fact not by name but by contents: for -example, writing \isa{{\isaliteral{60}{\isacharbackquote}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquote}}} (enclosing the formula in back quotes) -refers to the fact \isa{A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B} -without the need to name it. Here is a simple example, a revised version -of the previous proof% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{using}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquoteclose}}% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent which continues as before. - -Clearly, this device of quoting facts by contents is only advisable -for small formulae. In such cases it is superior to naming because the -reader immediately sees what the fact is without needing to search for -it in the preceding proof text. - -The assumptions of a lemma can also be referred to via their -predefined name \isa{assms}. Hence the \isa{{\isaliteral{60}{\isacharbackquote}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquote}}} in the -previous proof can also be replaced by \isa{assms}. Note that \isa{assms} refers to the list of \emph{all} assumptions. To pick out a -specific one, say the second, write \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. - -This indexing notation $name(.)$ works for any $name$ that stands for -a list of facts, for example $f$\isa{{\isaliteral{2E}{\isachardot}}simps}, the equations of the -recursively defined function $f$. You may also select sublists by writing -$name(2-3)$. - -Above we recommended the UNIX-pipe model (i.e. \isa{this}) to avoid -the need to name propositions. But frequently we needed to feed more -than one previously derived fact into a proof step. Then the UNIX-pipe -model appears to break down and we need to name the different facts to -refer to them. But this can be avoided:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{moreover}\isamarkupfalse% -\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{ultimately}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with -\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands -for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}. This avoids having to -introduce names for all of the sequence elements. - - -\subsection{Predicate calculus} - -Command \isakeyword{fix} introduces new local variables into a -proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} -(the universal quantifier at the -meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to -\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}. Here is a sample proof, annotated with the rules that are -applied implicitly:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ % -\isamarkupcmt{\isa{allI}: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}% -} -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ a\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ P\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\ \ % -\isamarkupcmt{\isa{allE}: \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R}% -} -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Note that in the proof we have chosen to call the bound -variable \isa{a} instead of \isa{x} merely to show that the choice of -local names is irrelevant. - -Next we look at \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} which is a bit more tricky.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ Pf{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ Pf\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\ \ \ \ \ \ \ \ \ \ \ \ \ \ % -\isamarkupcmt{\isa{exE}: \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}% -} -\isanewline -\ \ \ \ \isacommand{fix}\isamarkupfalse% -\ x\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\ \ % -\isamarkupcmt{\isa{exI}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}% -} -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Explicit $\exists$-elimination as seen above can become -cumbersome in practice. The derived Isar language element -\isakeyword{obtain} provides a more appealing form of generalised -existence reasoning:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ Pf{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ Pf\ \isacommand{obtain}\isamarkupfalse% -\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Note how the proof text follows the usual mathematical style -of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ -as a new local variable. Technically, \isakeyword{obtain} is similar to -\isakeyword{fix} and \isakeyword{assume} together with a soundness proof of -the elimination involved. - -Here is a proof of a well known tautology. -Which rule is used where?% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ ex{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ y\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ ex\ \isacommand{obtain}\isamarkupfalse% -\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isamarkupsubsection{Making bigger steps% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -So far we have confined ourselves to single step proofs. Of course -powerful automatic methods can be used just as well. Here is an example, -Cantor's theorem that there is no surjective function from a set to its -powerset:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{let}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{then}\isamarkupfalse% -\ \isacommand{obtain}\isamarkupfalse% -\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{show}\isamarkupfalse% -\ False\isanewline -\ \ \ \ \isacommand{proof}\isamarkupfalse% -\ cases\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\ \ \ \ \isacommand{next}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -For a start, the example demonstrates two new constructs: -\begin{itemize} -\item \isakeyword{let} introduces an abbreviation for a term, in our case -the witness for the claim. -\item Proof by \isa{cases} starts a proof by cases. Note that it remains -implicit what the two cases are: it is merely expected that the two subproofs -prove \isa{P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}thesis} and \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}thesis} (in that order) -for some \isa{P}. -\end{itemize} -If you wonder how to \isakeyword{obtain} \isa{y}: -via the predefined elimination rule \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P}. - -Method \isa{blast} is used because the contradiction does not follow easily -by just a single rule. If you find the proof too cryptic for human -consumption, here is a more detailed version; the beginning up to -\isakeyword{obtain} stays unchanged.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{let}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{then}\isamarkupfalse% -\ \isacommand{obtain}\isamarkupfalse% -\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{show}\isamarkupfalse% -\ False\isanewline -\ \ \ \ \isacommand{proof}\isamarkupfalse% -\ cases\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{by}\isamarkupfalse% -\ contradiction\isanewline -\ \ \ \ \isacommand{next}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ \isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \ \ \isacommand{with}\isamarkupfalse% -\ {\isaliteral{60}{\isacharbackquoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse% -\ False\ \isacommand{by}\isamarkupfalse% -\ contradiction\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Method \isa{contradiction} succeeds if both $P$ and -$\neg P$ are among the assumptions and the facts fed into that step, in any order. - -As it happens, Cantor's theorem can be proved automatically by best-first -search. Depth-first search would diverge, but best-first search successfully -navigates through the large search space:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ best% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isamarkupsubsection{Raw proof blocks% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Although we have shown how to employ powerful automatic methods like -\isa{blast} to achieve bigger proof steps, there may still be the -tendency to use the default introduction and elimination rules to -decompose goals and facts. This can lead to very tedious proofs:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{fix}\isamarkupfalse% -\ y\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% -\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent Since we are only interested in the decomposition and not the -actual proof, the latter has been replaced by -\isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is -only allowed in quick and dirty mode, the default interactive mode. It -is very convenient for top down proof development. - -Luckily we can avoid this step by step decomposition very easily:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\ x\ y{\isaliteral{3B}{\isacharsemicolon}}\ B\ x\ y\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \ \ \isacommand{fix}\isamarkupfalse% -\ x\ y\ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% -\isanewline -\ \ \isacommand{qed}\isamarkupfalse% -\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -This can be simplified further by \emph{raw proof blocks}, i.e.\ -proofs enclosed in braces:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% -\ \isacommand{fix}\isamarkupfalse% -\ x\ y\ \isacommand{assume}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% -\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The result of the raw proof block is the same theorem -as above, namely \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ x\ y{\isaliteral{3B}{\isacharsemicolon}}\ B\ x\ y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ x\ y}. Raw -proof blocks are like ordinary proofs except that they do not prove -some explicitly stated property but that the property emerges directly -out of the \isakeyword{fixe}s, \isakeyword{assume}s and -\isakeyword{have} in the block. Thus they again serve to avoid -duplication. Note that the conclusion of a raw proof block is stated with -\isakeyword{have} rather than \isakeyword{show} because it is not the -conclusion of some pending goal but some independent claim. - -The general idea demonstrated in this subsection is very -important in Isar and distinguishes it from \isa{apply}-style proofs: -\begin{quote}\em -Do not manipulate the proof state into a particular form by applying -proof methods but state the desired form explicitly and let the proof -methods verify that from this form the original goal follows. -\end{quote} -This yields more readable and also more robust proofs. - -\subsubsection{General case distinctions} - -As an important application of raw proof blocks we show how to deal -with general case distinctions --- more specific kinds are treated in -\S\ref{sec:CaseDistinction}. Imagine that you would like to prove some -goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that -the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and -that each case $P_i$ implies the goal. Taken together, this proves the -goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:% -\end{isamarkuptext}% -\isamarkuptrue% -% -\renewcommand{\isamarkupcmt}[1]{#1} -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ % -\isamarkupcmt{\dots% -} -\isanewline -\ \ \isacommand{moreover}\isamarkupfalse% -\isanewline -\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% -\ \isacommand{assume}\isamarkupfalse% -\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isanewline -\ \ \ \ % -\isamarkupcmt{\dots% -} -\isanewline -\ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \ % -\isamarkupcmt{\dots% -} -\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{moreover}\isamarkupfalse% -\isanewline -\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% -\ \isacommand{assume}\isamarkupfalse% -\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\isanewline -\ \ \ \ % -\isamarkupcmt{\dots% -} -\isanewline -\ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \ % -\isamarkupcmt{\dots% -} -\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{moreover}\isamarkupfalse% -\isanewline -\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% -\ \isacommand{assume}\isamarkupfalse% -\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\isanewline -\ \ \ \ % -\isamarkupcmt{\dots% -} -\isanewline -\ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \ % -\isamarkupcmt{\dots% -} -\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% -\isanewline -\ \ \isacommand{ultimately}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} -% -\isamarkupsubsection{Further refinements% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -This subsection discusses some further tricks that can make -life easier although they are not essential.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{\isakeyword{and}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Propositions (following \isakeyword{assume} etc) may but need not be -separated by \isakeyword{and}. This is not just for readability -(\isakeyword{from} \isa{A} \isakeyword{and} \isa{B} looks nicer than -\isakeyword{from} \isa{A} \isa{B}) but for structuring lists of propositions -into possibly named blocks. In -\begin{center} -\isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$ -\isakeyword{and} $A_4$ -\end{center} -label \isa{A} refers to the list of propositions $A_1$ $A_2$ and -label \isa{B} to $A_3$.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{\isakeyword{note}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -If you want to remember intermediate fact(s) that cannot be -named directly, use \isakeyword{note}. For example the result of raw -proof block can be named by following it with -\isakeyword{note}~\isa{some{\isaliteral{5F}{\isacharunderscore}}name\ {\isaliteral{3D}{\isacharequal}}\ this}. As a side effect, -\isa{this} is set to the list of facts on the right-hand side. You -can also say \isa{note\ some{\isaliteral{5F}{\isacharunderscore}}fact}, which simply sets \isa{this}, -i.e.\ recalls \isa{some{\isaliteral{5F}{\isacharunderscore}}fact}, e.g.\ in a \isakeyword{moreover} sequence.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{\isakeyword{fixes}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Sometimes it is necessary to decorate a proposition with type -constraints, as in Cantor's theorem above. These type constraints tend -to make the theorem less readable. The situation can be improved a -little by combining the type constraint with an outer \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent However, now \isa{f} is bound and we need a -\isakeyword{fix}~\isa{f} in the proof before we can refer to \isa{f}. -This is avoided by \isakeyword{fixes}:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent -Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ comm{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{3A}{\isacharcolon}}\isanewline -\ \ \isakeyword{fixes}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{and}\isanewline -\ \ \ \ \ \ \ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \isakeyword{assumes}\ comm{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline -\ \ \ \ \ \ \ \ \ \ mono{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ z\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ x\ {\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ comm\ mono{\isaliteral{29}{\isacharparenright}}% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent The concrete syntax is dropped at the end of the proof and the -theorem becomes \begin{isabelle}% -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}f\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ y\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline -\isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}r\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ x\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ y\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline -{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}z\ {\isaliteral{3F}{\isacharquery}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}z\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{29}{\isacharparenright}}% -\end{isabelle} -\tweakskip% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{\isakeyword{obtain}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The \isakeyword{obtain} construct can introduce multiple -witnesses and propositions as in the following proof fragment:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ \isakeyword{assumes}\ A{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x\ y{\isaliteral{2E}{\isachardot}}\ P\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isaliteral{2D}{\isacharminus}}\isanewline -\ \ \isacommand{from}\isamarkupfalse% -\ A\ \isacommand{obtain}\isamarkupfalse% -\ x\ y\ \isakeyword{where}\ P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ Q{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isacommand{by}\isamarkupfalse% -\ blast% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -Remember also that one does not even need to start with a formula -containing \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} as we saw in the proof of Cantor's theorem.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsubsection{Combining proof styles% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Finally, whole \isa{apply}-scripts may appear in the leaves of the -proof tree, although this is best avoided. Here is a contrived example:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline -\ \ \ \ \isacommand{apply}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{apply}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}erule\ impE{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{apply}\isamarkupfalse% -{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline -\ \ \ \ \isacommand{apply}\isamarkupfalse% -\ assumption\isanewline -\ \ \ \ \isacommand{done}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent You may need to resort to this technique if an -automatic step fails to prove the desired proposition. - -When converting a proof from \isa{apply}-style into Isar you can proceed -in a top-down manner: parts of the proof can be left in script form -while the outer structure is already expressed in Isar.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/Makefile --- a/doc-src/IsarOverview/Isar/document/Makefile Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ - -## targets - -default: dvi - -## dependencies - -include ../../../Makefile.in - -dvi: ../../isar-overview.dvi - -../../isar-overview.dvi: *.tex *.bib - $(LATEX) root - $(BIBTEX) root - $(LATEX) root - $(LATEX) root - mv root.dvi ../../isar-overview.dvi - -pdf: ../../isar-overview.pdf - -../../isar-overview.pdf: *.tex *.bib - $(PDFLATEX) root - $(BIBTEX) root - $(PDFLATEX) root - $(PDFLATEX) root - mv root.pdf ../../isar-overview.pdf \ No newline at end of file diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/intro.tex --- a/doc-src/IsarOverview/Isar/document/intro.tex Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -\section{Introduction} - -This is a tutorial introduction to structured proofs in Isabelle/HOL. -It introduces the core of the proof language Isar by example. Isar is -an extension of the \isa{apply}-style proofs introduced in the -Isabelle/HOL tutorial~\cite{LNCS2283} with structured proofs in a -stylised language of mathematics. These proofs are readable for both -human and machine. - -\subsection{A first glimpse of Isar} -Below you find a simplified grammar for Isar proofs. -Parentheses are used for grouping and $^?$ indicates an optional item: -\begin{center} -\begin{tabular}{lrl} -\emph{proof} & ::= & \isakeyword{proof} \emph{method}$^?$ - \emph{statement}* - \isakeyword{qed} \\ - &$\mid$& \isakeyword{by} \emph{method}\\[1ex] -\emph{statement} &::= & \isakeyword{fix} \emph{variables} \\ - &$\mid$& \isakeyword{assume} \emph{propositions} \\ - &$\mid$& (\isakeyword{from} \emph{fact}*)$^?$ - (\isakeyword{show} $\mid$ \isakeyword{have}) - \emph{propositions} \emph{proof} \\[1ex] -\emph{proposition} &::=& (\emph{label}{\bf:})$^?$ \emph{string} \\[1ex] -\emph{fact} &::=& \emph{label} -\end{tabular} -\end{center} -A proof can be either compound (\isakeyword{proof} -- -\isakeyword{qed}) or atomic (\isakeyword{by}). A \emph{method} is a -proof method. - -This is a typical proof skeleton: -\begin{center} -\begin{tabular}{@{}ll} -\isakeyword{proof}\\ -\hspace*{3ex}\isakeyword{assume} \isa{"}\emph{the-assm}\isa{"}\\ -\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\ -\hspace*{3ex}\vdots\\ -\hspace*{3ex}\isakeyword{have} \isa{"}\dots\isa{"} & --- intermediate result\\ -\hspace*{3ex}\isakeyword{show} \isa{"}\emph{the-concl}\isa{"}\\ -\isakeyword{qed} -\end{tabular} -\end{center} -It proves \emph{the-assm}~$\Longrightarrow$~\emph{the-concl}. Text starting with -``---'' is a comment. The intermediate \isakeyword{have}s are only -there to bridge the gap between the assumption and the conclusion and -do not contribute to the theorem being proved. In contrast, -\isakeyword{show} establishes the conclusion of the theorem. - -\subsection{Background} - -Interactive theorem proving has been dominated by a model of proof -that goes back to the LCF system~\cite{LCF}: a proof is a more or less -structured sequence of commands that manipulate an implicit proof -state. Thus the proof text is only suitable for the machine; for a -human, the proof only comes alive when he can see the state changes -caused by the stepwise execution of the commands. Such proofs are like -uncommented assembly language programs. Their Isabelle incarnation are -sequences of \isa{apply}-commands. - -In contrast there is the model of a mathematics-like proof language -pioneered in the Mizar system~\cite{Rudnicki92} and followed by -Isar~\cite{WenzelW-JAR}. -The most important arguments in favour of this style are -\emph{communication} and \emph{maintainance}: structured proofs are -immensly more readable and maintainable than \isa{apply}-scripts. - -For reading this tutorial you should be familiar with natural -deduction and the basics of Isabelle/HOL~\cite{LNCS2283} although we -summarize the most important aspects of Isabelle below. The -definitive Isar reference is its manual~\cite{Isar-Ref-Man}. For an -example-based account of Isar's support for reasoning by chains of -(in)equations see~\cite{BauerW-TPHOLs01}. - - -\subsection{Bits of Isabelle} - -Isabelle's meta-logic comes with a type of \emph{propositions} with -implication $\Longrightarrow$ and a universal quantifier $\bigwedge$ for expressing -inference rules and generality. Iterated implications $A_1 \Longrightarrow \dots -A_n \Longrightarrow A$ may be abbreviated to $[\![ A_1; \dots; A_n ]\!] \Longrightarrow A$. -Applying a theorem $A \Longrightarrow B$ (named \isa{T}) to a theorem $A$ (named -\isa{U}) is written \isa{T[OF U]} and yields theorem $B$. - -Isabelle terms are simply typed. Function types are -written $\tau_1 \Rightarrow \tau_2$. - -Free variables that may be instantiated (``logical variables'' in Prolog -parlance) are prefixed with a \isa{?}. Typically, theorems are stated with -ordinary free variables but after the proof those are automatically replaced -by \isa{?}-variables. Thus the theorem can be used with arbitrary instances -of its free variables. - -Isabelle/HOL offers all the usual logical symbols like $\longrightarrow$, $\land$, -$\forall$ etc. HOL formulae are propositions, e.g.\ $\forall$ can appear below -$\Longrightarrow$, but not the other way around. Beware that $\longrightarrow$ binds more -tightly than $\Longrightarrow$: in $\forall x. P \longrightarrow Q$ the $\forall x$ covers $P \longrightarrow Q$, whereas -in $\forall x. P \Longrightarrow Q$ it covers only $P$. - -Proof methods include \isa{rule} (which performs a backwards -step with a given rule, unifying the conclusion of the rule with the -current subgoal and replacing the subgoal by the premises of the -rule), \isa{simp} (for simplification) and \isa{blast} (for predicate -calculus reasoning). - -\subsection{Advice} - -A word of warning for potential writers of Isar proofs. It -is easier to write obscure rather than readable texts. Similarly, -\isa{apply}-style proofs are sometimes easier to write than readable -ones: structure does not emerge automatically but needs to be -understood and imposed. If the precise structure of the proof is -unclear at beginning, it can be useful to start with \isa{apply} for -exploratory purposes until one has found a proof which can be -converted into a structured text in a second step. Top down conversion -is possible because Isar allows \isa{apply}-style proofs as components -of structured ones. - -Finally, do not be misled by the simplicity of the formulae being proved, -especially in the beginning. Isar has been used very successfully in -large applications, for example the formalisation of Java -dialects~\cite{KleinN-TOPLAS}. -\medskip - -The rest of this tutorial is divided into two parts. -Section~\ref{sec:Logic} introduces proofs in pure logic based on -natural deduction. Section~\ref{sec:Induct} is dedicated to induction. diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/llncs.cls --- a/doc-src/IsarOverview/Isar/document/llncs.cls Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1189 +0,0 @@ -% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002) -% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science -% -%% -%% \CharacterTable -%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z -%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z -%% Digits \0\1\2\3\4\5\6\7\8\9 -%% Exclamation \! Double quote \" Hash (number) \# -%% Dollar \$ Percent \% Ampersand \& -%% Acute accent \' Left paren \( Right paren \) -%% Asterisk \* Plus \+ Comma \, -%% Minus \- Point \. Solidus \/ -%% Colon \: Semicolon \; Less than \< -%% Equals \= Greater than \> Question mark \? -%% Commercial at \@ Left bracket \[ Backslash \\ -%% Right bracket \] Circumflex \^ Underscore \_ -%% Grave accent \` Left brace \{ Vertical bar \| -%% Right brace \} Tilde \~} -%% -\NeedsTeXFormat{LaTeX2e}[1995/12/01] -\ProvidesClass{llncs}[2002/01/28 v2.13 -^^J LaTeX document class for Lecture Notes in Computer Science] -% Options -\let\if@envcntreset\iffalse -\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue} -\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y} -\DeclareOption{oribibl}{\let\oribibl=Y} -\let\if@custvec\iftrue -\DeclareOption{orivec}{\let\if@custvec\iffalse} -\let\if@envcntsame\iffalse -\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue} -\let\if@envcntsect\iffalse -\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue} -\let\if@runhead\iffalse -\DeclareOption{runningheads}{\let\if@runhead\iftrue} - -\let\if@openbib\iffalse -\DeclareOption{openbib}{\let\if@openbib\iftrue} - -% languages -\let\switcht@@therlang\relax -\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}} -\def\ds@francais{\def\switcht@@therlang{\switcht@francais}} - -\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} - -\ProcessOptions - -\LoadClass[twoside]{article} -\RequirePackage{multicol} % needed for the list of participants, index - -\setlength{\textwidth}{12.2cm} -\setlength{\textheight}{19.3cm} -\renewcommand\@pnumwidth{2em} -\renewcommand\@tocrmarg{3.5em} -% -\def\@dottedtocline#1#2#3#4#5{% - \ifnum #1>\c@tocdepth \else - \vskip \z@ \@plus.2\p@ - {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \parindent #2\relax\@afterindenttrue - \interlinepenalty\@M - \leavevmode - \@tempdima #3\relax - \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip - {#4}\nobreak - \leaders\hbox{$\m@th - \mkern \@dotsep mu\hbox{.}\mkern \@dotsep - mu$}\hfill - \nobreak - \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}% - \par}% - \fi} -% -\def\switcht@albion{% -\def\abstractname{Abstract.} -\def\ackname{Acknowledgement.} -\def\andname{and} -\def\lastandname{\unskip, and} -\def\appendixname{Appendix} -\def\chaptername{Chapter} -\def\claimname{Claim} -\def\conjecturename{Conjecture} -\def\contentsname{Table of Contents} -\def\corollaryname{Corollary} -\def\definitionname{Definition} -\def\examplename{Example} -\def\exercisename{Exercise} -\def\figurename{Fig.} -\def\keywordname{{\bf Key words:}} -\def\indexname{Index} -\def\lemmaname{Lemma} -\def\contriblistname{List of Contributors} -\def\listfigurename{List of Figures} -\def\listtablename{List of Tables} -\def\mailname{{\it Correspondence to\/}:} -\def\noteaddname{Note added in proof} -\def\notename{Note} -\def\partname{Part} -\def\problemname{Problem} -\def\proofname{Proof} -\def\propertyname{Property} -\def\propositionname{Proposition} -\def\questionname{Question} -\def\remarkname{Remark} -\def\seename{see} -\def\solutionname{Solution} -\def\subclassname{{\it Subject Classifications\/}:} -\def\tablename{Table} -\def\theoremname{Theorem}} -\switcht@albion -% Names of theorem like environments are already defined -% but must be translated if another language is chosen -% -% French section -\def\switcht@francais{%\typeout{On parle francais.}% - \def\abstractname{R\'esum\'e.}% - \def\ackname{Remerciements.}% - \def\andname{et}% - \def\lastandname{ et}% - \def\appendixname{Appendice} - \def\chaptername{Chapitre}% - \def\claimname{Pr\'etention}% - \def\conjecturename{Hypoth\`ese}% - \def\contentsname{Table des mati\`eres}% - \def\corollaryname{Corollaire}% - \def\definitionname{D\'efinition}% - \def\examplename{Exemple}% - \def\exercisename{Exercice}% - \def\figurename{Fig.}% - \def\keywordname{{\bf Mots-cl\'e:}} - \def\indexname{Index} - \def\lemmaname{Lemme}% - \def\contriblistname{Liste des contributeurs} - \def\listfigurename{Liste des figures}% - \def\listtablename{Liste des tables}% - \def\mailname{{\it Correspondence to\/}:} - \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}% - \def\notename{Remarque}% - \def\partname{Partie}% - \def\problemname{Probl\`eme}% - \def\proofname{Preuve}% - \def\propertyname{Caract\'eristique}% -%\def\propositionname{Proposition}% - \def\questionname{Question}% - \def\remarkname{Remarque}% - \def\seename{voir} - \def\solutionname{Solution}% - \def\subclassname{{\it Subject Classifications\/}:} - \def\tablename{Tableau}% - \def\theoremname{Th\'eor\`eme}% -} -% -% German section -\def\switcht@deutsch{%\typeout{Man spricht deutsch.}% - \def\abstractname{Zusammenfassung.}% - \def\ackname{Danksagung.}% - \def\andname{und}% - \def\lastandname{ und}% - \def\appendixname{Anhang}% - \def\chaptername{Kapitel}% - \def\claimname{Behauptung}% - \def\conjecturename{Hypothese}% - \def\contentsname{Inhaltsverzeichnis}% - \def\corollaryname{Korollar}% -%\def\definitionname{Definition}% - \def\examplename{Beispiel}% - \def\exercisename{\"Ubung}% - \def\figurename{Abb.}% - \def\keywordname{{\bf Schl\"usselw\"orter:}} - \def\indexname{Index} -%\def\lemmaname{Lemma}% - \def\contriblistname{Mitarbeiter} - \def\listfigurename{Abbildungsverzeichnis}% - \def\listtablename{Tabellenverzeichnis}% - \def\mailname{{\it Correspondence to\/}:} - \def\noteaddname{Nachtrag}% - \def\notename{Anmerkung}% - \def\partname{Teil}% -%\def\problemname{Problem}% - \def\proofname{Beweis}% - \def\propertyname{Eigenschaft}% -%\def\propositionname{Proposition}% - \def\questionname{Frage}% - \def\remarkname{Anmerkung}% - \def\seename{siehe} - \def\solutionname{L\"osung}% - \def\subclassname{{\it Subject Classifications\/}:} - \def\tablename{Tabelle}% -%\def\theoremname{Theorem}% -} - -% Ragged bottom for the actual page -\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil -\global\let\@textbottom\relax}} - -\renewcommand\small{% - \@setfontsize\small\@ixpt{11}% - \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ - \abovedisplayshortskip \z@ \@plus2\p@ - \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ - \def\@listi{\leftmargin\leftmargini - \parsep 0\p@ \@plus1\p@ \@minus\p@ - \topsep 8\p@ \@plus2\p@ \@minus4\p@ - \itemsep0\p@}% - \belowdisplayskip \abovedisplayskip -} - -\frenchspacing -\widowpenalty=10000 -\clubpenalty=10000 - -\setlength\oddsidemargin {63\p@} -\setlength\evensidemargin {63\p@} -\setlength\marginparwidth {90\p@} - -\setlength\headsep {16\p@} - -\setlength\footnotesep{7.7\p@} -\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@} -\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@} - -\setcounter{secnumdepth}{2} - -\newcounter {chapter} -\renewcommand\thechapter {\@arabic\c@chapter} - -\newif\if@mainmatter \@mainmattertrue -\newcommand\frontmatter{\cleardoublepage - \@mainmatterfalse\pagenumbering{Roman}} -\newcommand\mainmatter{\cleardoublepage - \@mainmattertrue\pagenumbering{arabic}} -\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi - \@mainmatterfalse} - -\renewcommand\part{\cleardoublepage - \thispagestyle{empty}% - \if@twocolumn - \onecolumn - \@tempswatrue - \else - \@tempswafalse - \fi - \null\vfil - \secdef\@part\@spart} - -\def\@part[#1]#2{% - \ifnum \c@secnumdepth >-2\relax - \refstepcounter{part}% - \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}% - \else - \addcontentsline{toc}{part}{#1}% - \fi - \markboth{}{}% - {\centering - \interlinepenalty \@M - \normalfont - \ifnum \c@secnumdepth >-2\relax - \huge\bfseries \partname~\thepart - \par - \vskip 20\p@ - \fi - \Huge \bfseries #2\par}% - \@endpart} -\def\@spart#1{% - {\centering - \interlinepenalty \@M - \normalfont - \Huge \bfseries #1\par}% - \@endpart} -\def\@endpart{\vfil\newpage - \if@twoside - \null - \thispagestyle{empty}% - \newpage - \fi - \if@tempswa - \twocolumn - \fi} - -\newcommand\chapter{\clearpage - \thispagestyle{empty}% - \global\@topnum\z@ - \@afterindentfalse - \secdef\@chapter\@schapter} -\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne - \if@mainmatter - \refstepcounter{chapter}% - \typeout{\@chapapp\space\thechapter.}% - \addcontentsline{toc}{chapter}% - {\protect\numberline{\thechapter}#1}% - \else - \addcontentsline{toc}{chapter}{#1}% - \fi - \else - \addcontentsline{toc}{chapter}{#1}% - \fi - \chaptermark{#1}% - \addtocontents{lof}{\protect\addvspace{10\p@}}% - \addtocontents{lot}{\protect\addvspace{10\p@}}% - \if@twocolumn - \@topnewpage[\@makechapterhead{#2}]% - \else - \@makechapterhead{#2}% - \@afterheading - \fi} -\def\@makechapterhead#1{% -% \vspace*{50\p@}% - {\centering - \ifnum \c@secnumdepth >\m@ne - \if@mainmatter - \large\bfseries \@chapapp{} \thechapter - \par\nobreak - \vskip 20\p@ - \fi - \fi - \interlinepenalty\@M - \Large \bfseries #1\par\nobreak - \vskip 40\p@ - }} -\def\@schapter#1{\if@twocolumn - \@topnewpage[\@makeschapterhead{#1}]% - \else - \@makeschapterhead{#1}% - \@afterheading - \fi} -\def\@makeschapterhead#1{% -% \vspace*{50\p@}% - {\centering - \normalfont - \interlinepenalty\@M - \Large \bfseries #1\par\nobreak - \vskip 40\p@ - }} - -\renewcommand\section{\@startsection{section}{1}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {12\p@ \@plus 4\p@ \@minus 4\p@}% - {\normalfont\large\bfseries\boldmath - \rightskip=\z@ \@plus 8em\pretolerance=10000 }} -\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {8\p@ \@plus 4\p@ \@minus 4\p@}% - {\normalfont\normalsize\bfseries\boldmath - \rightskip=\z@ \@plus 8em\pretolerance=10000 }} -\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% - {-18\p@ \@plus -4\p@ \@minus -4\p@}% - {-0.5em \@plus -0.22em \@minus -0.1em}% - {\normalfont\normalsize\bfseries\boldmath}} -\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% - {-12\p@ \@plus -4\p@ \@minus -4\p@}% - {-0.5em \@plus -0.22em \@minus -0.1em}% - {\normalfont\normalsize\itshape}} -\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use - \string\subparagraph\space with this class}\vskip0.5cm -You should not use \verb|\subparagraph| with this class.\vskip0.5cm} - -\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00} -\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01} -\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02} -\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03} -\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04} -\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05} -\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06} -\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07} -\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08} -\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09} -\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A} - -\let\footnotesize\small - -\if@custvec -\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}} -{\mbox{\boldmath$\textstyle#1$}} -{\mbox{\boldmath$\scriptstyle#1$}} -{\mbox{\boldmath$\scriptscriptstyle#1$}}} -\fi - -\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}} -\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil -\penalty50\hskip1em\null\nobreak\hfil\squareforqed -\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi} - -\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip -\halign{\hfil -$\displaystyle##$\hfil\cr\gets\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets -\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets -\cr\to\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr -\gets\cr\to\cr}}}}} -\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil -$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr -\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr -\noalign{\vskip1pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr -<\cr -\noalign{\vskip0.9pt}=\cr}}}}} -\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil -$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr -\noalign{\vskip1.2pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr -\noalign{\vskip1pt}=\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr ->\cr -\noalign{\vskip0.9pt}=\cr}}}}} -\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip -\halign{\hfil -$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr ->\cr\noalign{\vskip-1pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr ->\cr\noalign{\vskip-0.8pt}<\cr}}} -{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr ->\cr\noalign{\vskip-0.3pt}<\cr}}}}} -\def\bbbr{{\rm I\!R}} %reelle Zahlen -\def\bbbm{{\rm I\!M}} -\def\bbbn{{\rm I\!N}} %natuerliche Zahlen -\def\bbbf{{\rm I\!F}} -\def\bbbh{{\rm I\!H}} -\def\bbbk{{\rm I\!K}} -\def\bbbp{{\rm I\!P}} -\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l} -{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}} -\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox -to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}} -\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm -Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise -0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}} -\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm -T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox -to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}} -\def\bbbs{{\mathchoice -{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox -to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} -{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox -to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox -to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}} -{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox -to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox -to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}} -\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} -{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} -{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}} -{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}} - -\let\ts\, - -\setlength\leftmargini {17\p@} -\setlength\leftmargin {\leftmargini} -\setlength\leftmarginii {\leftmargini} -\setlength\leftmarginiii {\leftmargini} -\setlength\leftmarginiv {\leftmargini} -\setlength \labelsep {.5em} -\setlength \labelwidth{\leftmargini} -\addtolength\labelwidth{-\labelsep} - -\def\@listI{\leftmargin\leftmargini - \parsep 0\p@ \@plus1\p@ \@minus\p@ - \topsep 8\p@ \@plus2\p@ \@minus4\p@ - \itemsep0\p@} -\let\@listi\@listI -\@listi -\def\@listii {\leftmargin\leftmarginii - \labelwidth\leftmarginii - \advance\labelwidth-\labelsep - \topsep 0\p@ \@plus2\p@ \@minus\p@} -\def\@listiii{\leftmargin\leftmarginiii - \labelwidth\leftmarginiii - \advance\labelwidth-\labelsep - \topsep 0\p@ \@plus\p@\@minus\p@ - \parsep \z@ - \partopsep \p@ \@plus\z@ \@minus\p@} - -\renewcommand\labelitemi{\normalfont\bfseries --} -\renewcommand\labelitemii{$\m@th\bullet$} - -\setlength\arraycolsep{1.4\p@} -\setlength\tabcolsep{1.4\p@} - -\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}% - {{\contentsname}}} - \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}} - \def\lastand{\ifnum\value{auco}=2\relax - \unskip{} \andname\ - \else - \unskip \lastandname\ - \fi}% - \def\and{\stepcounter{@auth}\relax - \ifnum\value{@auth}=\value{auco}% - \lastand - \else - \unskip, - \fi}% - \@starttoc{toc}\if@restonecol\twocolumn\fi} - -\def\l@part#1#2{\addpenalty{\@secpenalty}% - \addvspace{2em plus\p@}% % space above part line - \begingroup - \parindent \z@ - \rightskip \z@ plus 5em - \hrule\vskip5pt - \large % same size as for a contribution heading - \bfseries\boldmath % set line in boldface - \leavevmode % TeX command to enter horizontal mode. - #1\par - \vskip5pt - \hrule - \vskip1pt - \nobreak % Never break after part entry - \endgroup} - -\def\@dotsep{2} - -\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else -{chapter.\thechapter}\fi} - -\def\addnumcontentsmark#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline - {\thechapter}#3}{\thepage}\hyperhrefextend}} -\def\addcontentsmark#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}} -\def\addcontentsmarkwop#1#2#3{% -\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}} - -\def\@adcmk[#1]{\ifcase #1 \or -\def\@gtempa{\addnumcontentsmark}% - \or \def\@gtempa{\addcontentsmark}% - \or \def\@gtempa{\addcontentsmarkwop}% - \fi\@gtempa{toc}{chapter}} -\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}} - -\def\l@chapter#1#2{\addpenalty{-\@highpenalty} - \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip - {\large\bfseries\boldmath#1}\ifx0#2\hfil\null - \else - \nobreak - \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern - \@dotsep mu$}\hfill - \nobreak\hbox to\@pnumwidth{\hss #2}% - \fi\par - \penalty\@highpenalty \endgroup} - -\def\l@title#1#2{\addpenalty{-\@highpenalty} - \addvspace{8pt plus 1pt} - \@tempdima \z@ - \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \parfillskip -\rightskip \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip - #1\nobreak - \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern - \@dotsep mu$}\hfill - \nobreak\hbox to\@pnumwidth{\hss #2}\par - \penalty\@highpenalty \endgroup} - -\def\l@author#1#2{\addpenalty{\@highpenalty} - \@tempdima=\z@ %15\p@ - \begingroup - \parindent \z@ \rightskip \@tocrmarg - \advance\rightskip by 0pt plus 2cm - \pretolerance=10000 - \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip - \textit{#1}\par - \penalty\@highpenalty \endgroup} - -\setcounter{tocdepth}{0} -\newdimen\tocchpnum -\newdimen\tocsecnum -\newdimen\tocsectotal -\newdimen\tocsubsecnum -\newdimen\tocsubsectotal -\newdimen\tocsubsubsecnum -\newdimen\tocsubsubsectotal -\newdimen\tocparanum -\newdimen\tocparatotal -\newdimen\tocsubparanum -\tocchpnum=\z@ % no chapter numbers -\tocsecnum=15\p@ % section 88. plus 2.222pt -\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt -\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt -\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt -\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt -\def\calctocindent{% -\tocsectotal=\tocchpnum -\advance\tocsectotal by\tocsecnum -\tocsubsectotal=\tocsectotal -\advance\tocsubsectotal by\tocsubsecnum -\tocsubsubsectotal=\tocsubsectotal -\advance\tocsubsubsectotal by\tocsubsubsecnum -\tocparatotal=\tocsubsubsectotal -\advance\tocparatotal by\tocparanum} -\calctocindent - -\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}} -\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}} -\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}} -\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}} -\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}} - -\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn - \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}} - \@starttoc{lof}\if@restonecol\twocolumn\fi} -\def\l@figure{\@dottedtocline{1}{0em}{1.5em}} - -\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn - \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}} - \@starttoc{lot}\if@restonecol\twocolumn\fi} -\let\l@table\l@figure - -\renewcommand\listoffigures{% - \section*{\listfigurename - \@mkboth{\listfigurename}{\listfigurename}}% - \@starttoc{lof}% - } - -\renewcommand\listoftables{% - \section*{\listtablename - \@mkboth{\listtablename}{\listtablename}}% - \@starttoc{lot}% - } - -\ifx\oribibl\undefined -\ifx\citeauthoryear\undefined -\renewenvironment{thebibliography}[1] - {\section*{\refname} - \def\@biblabel##1{##1.} - \small - \list{\@biblabel{\@arabic\c@enumiv}}% - {\settowidth\labelwidth{\@biblabel{#1}}% - \leftmargin\labelwidth - \advance\leftmargin\labelsep - \if@openbib - \advance\leftmargin\bibindent - \itemindent -\bibindent - \listparindent \itemindent - \parsep \z@ - \fi - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{\@arabic\c@enumiv}}% - \if@openbib - \renewcommand\newblock{\par}% - \else - \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% - \fi - \sloppy\clubpenalty4000\widowpenalty4000% - \sfcode`\.=\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} -\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw - {\let\protect\noexpand\immediate - \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} -\newcount\@tempcntc -\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi - \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do - {\@ifundefined - {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries - ?}\@warning - {Citation `\@citeb' on page \thepage \space undefined}}% - {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}% - \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne - \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}% - \else - \advance\@tempcntb\@ne - \ifnum\@tempcntb=\@tempcntc - \else\advance\@tempcntb\m@ne\@citeo - \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}} -\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else - \@citea\def\@citea{,\,\hskip\z@skip}% - \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else - {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else - \def\@citea{--}\fi - \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi} -\else -\renewenvironment{thebibliography}[1] - {\section*{\refname} - \small - \list{}% - {\settowidth\labelwidth{}% - \leftmargin\parindent - \itemindent=-\parindent - \labelsep=\z@ - \if@openbib - \advance\leftmargin\bibindent - \itemindent -\bibindent - \listparindent \itemindent - \parsep \z@ - \fi - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{}}% - \if@openbib - \renewcommand\newblock{\par}% - \else - \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}% - \fi - \sloppy\clubpenalty4000\widowpenalty4000% - \sfcode`\.=\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} - \def\@cite#1{#1}% - \def\@lbibitem[#1]#2{\item[]\if@filesw - {\def\protect##1{\string ##1\space}\immediate - \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} - \fi -\else -\@cons\@openbib@code{\noexpand\small} -\fi - -\def\idxquad{\hskip 10\p@}% space that divides entry from number - -\def\@idxitem{\par\hangindent 10\p@} - -\def\subitem{\par\setbox0=\hbox{--\enspace}% second order - \noindent\hangindent\wd0\box0}% index entry - -\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third - \noindent\hangindent\wd0\box0}% order index entry - -\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax} - -\renewenvironment{theindex} - {\@mkboth{\indexname}{\indexname}% - \thispagestyle{empty}\parindent\z@ - \parskip\z@ \@plus .3\p@\relax - \let\item\par - \def\,{\relax\ifmmode\mskip\thinmuskip - \else\hskip0.2em\ignorespaces\fi}% - \normalfont\small - \begin{multicols}{2}[\@makeschapterhead{\indexname}]% - } - {\end{multicols}} - -\renewcommand\footnoterule{% - \kern-3\p@ - \hrule\@width 2truecm - \kern2.6\p@} - \newdimen\fnindent - \fnindent1em -\long\def\@makefntext#1{% - \parindent \fnindent% - \leftskip \fnindent% - \noindent - \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1} - -\long\def\@makecaption#1#2{% - \vskip\abovecaptionskip - \sbox\@tempboxa{{\bfseries #1.} #2}% - \ifdim \wd\@tempboxa >\hsize - {\bfseries #1.} #2\par - \else - \global \@minipagefalse - \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}% - \fi - \vskip\belowcaptionskip} - -\def\fps@figure{htbp} -\def\fnum@figure{\figurename\thinspace\thefigure} -\def \@floatboxreset {% - \reset@font - \small - \@setnobreak - \@setminipage -} -\def\fps@table{htbp} -\def\fnum@table{\tablename~\thetable} -\renewenvironment{table} - {\setlength\abovecaptionskip{0\p@}% - \setlength\belowcaptionskip{10\p@}% - \@float{table}} - {\end@float} -\renewenvironment{table*} - {\setlength\abovecaptionskip{0\p@}% - \setlength\belowcaptionskip{10\p@}% - \@dblfloat{table}} - {\end@dblfloat} - -\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname - ext@#1\endcsname}{#1}{\protect\numberline{\csname - the#1\endcsname}{\ignorespaces #2}}\begingroup - \@parboxrestore - \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par - \endgroup} - -% LaTeX does not provide a command to enter the authors institute -% addresses. The \institute command is defined here. - -\newcounter{@inst} -\newcounter{@auth} -\newcounter{auco} -\newdimen\instindent -\newbox\authrun -\newtoks\authorrunning -\newtoks\tocauthor -\newbox\titrun -\newtoks\titlerunning -\newtoks\toctitle - -\def\clearheadinfo{\gdef\@author{No Author Given}% - \gdef\@title{No Title Given}% - \gdef\@subtitle{}% - \gdef\@institute{No Institute Given}% - \gdef\@thanks{}% - \global\titlerunning={}\global\authorrunning={}% - \global\toctitle={}\global\tocauthor={}} - -\def\institute#1{\gdef\@institute{#1}} - -\def\institutename{\par - \begingroup - \parskip=\z@ - \parindent=\z@ - \setcounter{@inst}{1}% - \def\and{\par\stepcounter{@inst}% - \noindent$^{\the@inst}$\enspace\ignorespaces}% - \setbox0=\vbox{\def\thanks##1{}\@institute}% - \ifnum\c@@inst=1\relax - \gdef\fnnstart{0}% - \else - \xdef\fnnstart{\c@@inst}% - \setcounter{@inst}{1}% - \noindent$^{\the@inst}$\enspace - \fi - \ignorespaces - \@institute\par - \endgroup} - -\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or - {\star\star\star}\or \dagger\or \ddagger\or - \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger - \or \ddagger\ddagger \else\@ctrerr\fi}} - -\def\inst#1{\unskip$^{#1}$} -\def\fnmsep{\unskip$^,$} -\def\email#1{{\tt#1}} -\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}% -\@ifpackageloaded{babel}{% -\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}% -\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}% -\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}% -}{\switcht@@therlang}% -} -\def\homedir{\~{ }} - -\def\subtitle#1{\gdef\@subtitle{#1}} -\clearheadinfo - -\renewcommand\maketitle{\newpage - \refstepcounter{chapter}% - \stepcounter{section}% - \setcounter{section}{0}% - \setcounter{subsection}{0}% - \setcounter{figure}{0} - \setcounter{table}{0} - \setcounter{equation}{0} - \setcounter{footnote}{0}% - \begingroup - \parindent=\z@ - \renewcommand\thefootnote{\@fnsymbol\c@footnote}% - \if@twocolumn - \ifnum \col@number=\@ne - \@maketitle - \else - \twocolumn[\@maketitle]% - \fi - \else - \newpage - \global\@topnum\z@ % Prevents figures from going at top of page. - \@maketitle - \fi - \thispagestyle{empty}\@thanks -% - \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}% - \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}% - \instindent=\hsize - \advance\instindent by-\headlineindent - \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else - \addcontentsline{toc}{title}{\the\toctitle}\fi - \if@runhead - \if!\the\titlerunning!\else - \edef\@title{\the\titlerunning}% - \fi - \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}% - \ifdim\wd\titrun>\instindent - \typeout{Title too long for running head. Please supply}% - \typeout{a shorter form with \string\titlerunning\space prior to - \string\maketitle}% - \global\setbox\titrun=\hbox{\small\rm - Title Suppressed Due to Excessive Length}% - \fi - \xdef\@title{\copy\titrun}% - \fi -% - \if!\the\tocauthor!\relax - {\def\and{\noexpand\protect\noexpand\and}% - \protected@xdef\toc@uthor{\@author}}% - \else - \def\\{\noexpand\protect\noexpand\newline}% - \protected@xdef\scratch{\the\tocauthor}% - \protected@xdef\toc@uthor{\scratch}% - \fi - \addcontentsline{toc}{author}{\toc@uthor}% - \if@runhead - \if!\the\authorrunning! - \value{@inst}=\value{@auth}% - \setcounter{@auth}{1}% - \else - \edef\@author{\the\authorrunning}% - \fi - \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}% - \ifdim\wd\authrun>\instindent - \typeout{Names of authors too long for running head. Please supply}% - \typeout{a shorter form with \string\authorrunning\space prior to - \string\maketitle}% - \global\setbox\authrun=\hbox{\small\rm - Authors Suppressed Due to Excessive Length}% - \fi - \xdef\@author{\copy\authrun}% - \markboth{\@author}{\@title}% - \fi - \endgroup - \setcounter{footnote}{\fnnstart}% - \clearheadinfo} -% -\def\@maketitle{\newpage - \markboth{}{}% - \def\lastand{\ifnum\value{@inst}=2\relax - \unskip{} \andname\ - \else - \unskip \lastandname\ - \fi}% - \def\and{\stepcounter{@auth}\relax - \ifnum\value{@auth}=\value{@inst}% - \lastand - \else - \unskip, - \fi}% - \begin{center}% - \let\newline\\ - {\Large \bfseries\boldmath - \pretolerance=10000 - \@title \par}\vskip .8cm -\if!\@subtitle!\else {\large \bfseries\boldmath - \vskip -.65cm - \pretolerance=10000 - \@subtitle \par}\vskip .8cm\fi - \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}% - \def\thanks##1{}\@author}% - \global\value{@inst}=\value{@auth}% - \global\value{auco}=\value{@auth}% - \setcounter{@auth}{1}% -{\lineskip .5em -\noindent\ignorespaces -\@author\vskip.35cm} - {\small\institutename} - \end{center}% - } - -% definition of the "\spnewtheorem" command. -% -% Usage: -% -% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font} -% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font} -% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font} -% -% New is "cap_font" and "body_font". It stands for -% fontdefinition of the caption and the text itself. -% -% "\spnewtheorem*" gives a theorem without number. -% -% A defined spnewthoerem environment is used as described -% by Lamport. -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\def\@thmcountersep{} -\def\@thmcounterend{.} - -\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}} - -% definition of \spnewtheorem with number - -\def\@spnthm#1#2{% - \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}} -\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}} - -\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname - {\@definecounter{#1}\@addtoreset{#1}{#3}% - \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand - \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname - {\@definecounter{#1}% - \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@spothm#1[#2]#3#4#5{% - \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}% - {\expandafter\@ifdefinable\csname #1\endcsname - {\global\@namedef{the#1}{\@nameuse{the#2}}% - \expandafter\xdef\csname #1name\endcsname{#3}% - \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}% - \global\@namedef{end#1}{\@endtheorem}}}} - -\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@ -\refstepcounter{#1}% -\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}} - -\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}% - \ignorespaces} - -\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname - the#1\endcsname}{#5}{#3}{#4}\ignorespaces} - -\def\@spbegintheorem#1#2#3#4{\trivlist - \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4} - -\def\@spopargbegintheorem#1#2#3#4#5{\trivlist - \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5} - -% definition of \spnewtheorem* without number - -\def\@sthm#1#2{\@Ynthm{#1}{#2}} - -\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname - {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}% - \expandafter\xdef\csname #1name\endcsname{#2}% - \global\@namedef{end#1}{\@endtheorem}}} - -\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@ -\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}} - -\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces} - -\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1} - {#4}{#2}{#3}\ignorespaces} - -\def\@Begintheorem#1#2#3{#3\trivlist - \item[\hskip\labelsep{#2#1\@thmcounterend}]} - -\def\@Opargbegintheorem#1#2#3#4{#4\trivlist - \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }} - -\if@envcntsect - \def\@thmcountersep{.} - \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape} -\else - \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape} - \if@envcntreset - \@addtoreset{theorem}{section} - \else - \@addtoreset{theorem}{chapter} - \fi -\fi - -%definition of divers theorem environments -\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily} -\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily} -\if@envcntsame % alle Umgebungen wie Theorem. - \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}} -\else % alle Umgebungen mit eigenem Zaehler - \if@envcntsect % mit section numeriert - \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}} - \else % nicht mit section numeriert - \if@envcntreset - \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} - \@addtoreset{#1}{section}} - \else - \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} - \@addtoreset{#1}{chapter}}% - \fi - \fi -\fi -\spn@wtheorem{case}{Case}{\itshape}{\rmfamily} -\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily} -\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape} -\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape} -\spn@wtheorem{example}{Example}{\itshape}{\rmfamily} -\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily} -\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape} -\spn@wtheorem{note}{Note}{\itshape}{\rmfamily} -\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily} -\spn@wtheorem{property}{Property}{\itshape}{\rmfamily} -\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape} -\spn@wtheorem{question}{Question}{\itshape}{\rmfamily} -\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily} -\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily} - -\def\@takefromreset#1#2{% - \def\@tempa{#1}% - \let\@tempd\@elt - \def\@elt##1{% - \def\@tempb{##1}% - \ifx\@tempa\@tempb\else - \@addtoreset{##1}{#2}% - \fi}% - \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname - \expandafter\def\csname cl@#2\endcsname{}% - \@tempc - \let\@elt\@tempd} - -\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist - \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5} - \def\@Opargbegintheorem##1##2##3##4{##4\trivlist - \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }} - } - -\renewenvironment{abstract}{% - \list{}{\advance\topsep by0.35cm\relax\small - \leftmargin=1cm - \labelwidth=\z@ - \listparindent=\z@ - \itemindent\listparindent - \rightmargin\leftmargin}\item[\hskip\labelsep - \bfseries\abstractname]} - {\endlist} - -\newdimen\headlineindent % dimension for space between -\headlineindent=1.166cm % number and text of headings. - -\def\ps@headings{\let\@mkboth\@gobbletwo - \let\@oddfoot\@empty\let\@evenfoot\@empty - \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% - \leftmark\hfil} - \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}% - \llap{\thepage}} - \def\chaptermark##1{}% - \def\sectionmark##1{}% - \def\subsectionmark##1{}} - -\def\ps@titlepage{\let\@mkboth\@gobbletwo - \let\@oddfoot\@empty\let\@evenfoot\@empty - \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% - \hfil} - \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}% - \llap{\thepage}} - \def\chaptermark##1{}% - \def\sectionmark##1{}% - \def\subsectionmark##1{}} - -\if@runhead\ps@headings\else -\ps@empty\fi - -\setlength\arraycolsep{1.4\p@} -\setlength\tabcolsep{1.4\p@} - -\endinput -%end of file llncs.cls diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/root.bib --- a/doc-src/IsarOverview/Isar/document/root.bib Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -@string{LNCS="Lect.\ Notes in Comp.\ Sci."} -@string{Springer="Springer-Verlag"} -@string{JAR="J. Automated Reasoning"} - -@InProceedings{BauerW-TPHOLs01, -author={Gertrud Bauer and Markus Wenzel}, -title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience}, -booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001}, -editor={R. Boulton and P. Jackson}, -year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"} - -@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth", -title="Edinburgh {LCF}: a Mechanised Logic of Computation", -publisher=Springer,series=LNCS,volume=78,year=1979} - -@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel}, -title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic", -publisher=Springer,series=LNCS,volume=2283,year=2002, -note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}} - -@article{KleinN-TOPLAS,author={Gerwin Klein and Tobias Nipkow}, -title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler}, -journal=TOPLAS,volume = {28}, number = {4}, year = {2006}, pages = {619--695}, -doi = {http://doi.acm.org/10.1145/1146809.1146811}} - -@InProceedings{Rudnicki92,author={P. Rudnicki}, -title={An Overview of the {Mizar} Project}, -booktitle={Workshop on Types for Proofs and Programs}, -year=1992,organization={Chalmers University of Technology}} - -@manual{Isar-Ref-Man,author="Markus Wenzel", -title="The Isabelle/Isar Reference Manual", -organization={Technische Universit{\"a}t M{\"u}nchen},year=2002, -note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}} - -@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk}, -title={A comparison of the mathematical proof languages {Mizar} and {Isar}}, -journal=JAR,year=2002,pages={389--411}} - diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/document/root.tex --- a/doc-src/IsarOverview/Isar/document/root.tex Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -\documentclass[envcountsame]{llncs} -%\documentclass[11pt,a4paper]{article} -\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym,../../../pdfsetup} - -%for best-style documents ... -\urlstyle{rm} -%\isabellestyle{it} - -\newcommand{\tweakskip}{\vspace{-\medskipamount}} - -\pagestyle{plain} - -\begin{document} - -\title{A Tutorial Introduction to Structured Isar Proofs} -\author{Tobias Nipkow} -\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\ - {\small\url{http://www.in.tum.de/~nipkow/}}} -\date{} -\maketitle - -\input{intro.tex} -\input{Logic.tex} -\input{Induction.tex} - -\begingroup -\bibliographystyle{plain} \small\raggedright\frenchspacing -\bibliography{root} -\endgroup - -\end{document} diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Isar/makeDemo --- a/doc-src/IsarOverview/Isar/makeDemo Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -#!/usr/bin/perl -w - -sub doit { - my ($file) = @_; - - open (FILE, $file) || die $!; - undef $/; $text = ; $/ = "\n"; - close FILE || die $!; - - $_ = $text; - - s/text_raw\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here - s/text\{\*([^*]|\*[^}])*\*\}//sg; # actual work done here - s/\(\*<\*\)//sg; - s/\(\*>\*\)//sg; - s/--(\ )*"([^"])*"//sg; - s/--(\ )*\{\*([^*]|\*[^}])*\*\}//sg; - - $result = $_; - - if ($text ne $result) { - print STDERR "fixing $file\n"; -# if (! -f "$file~~") { -# rename $file, "$file~~" || die $!; -# } - open (FILE, "> Demo/$file") || die $!; - print FILE $result; - close FILE || die $!; - } -} - - -foreach $file (@ARGV) { - eval { &doit($file); }; - if ($@) { print STDERR "*** doit $file: ", $@, "\n"; } -} diff -r 360e080fd13e -r 8204b1023537 doc-src/IsarOverview/Makefile --- a/doc-src/IsarOverview/Makefile Wed Apr 04 10:04:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ - -## targets - -default: dvi - -## dependencies - -dvi: - cd Isar/document; make dvi - -pdf: - cd Isar/document; make pdf - -clean: - cd Isar/document; make clean - -mrproper: - rm -f *.pdf *.dvi - cd Isar/document; make mrproper