--- 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
--- 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
-
--- 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 "\<not> A \<or> A"
-proof cases
- assume "A" thus ?thesis ..
-next
- assume "\<not> 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"\<not> A \<Longrightarrow> \<not> A \<or> A"} which would solve the first premise of
-@{thm[source] case_split}, instantiating @{text ?P} with @{term "\<not>
-A"}, thus making the second premise @{prop"\<not> \<not> A \<Longrightarrow> \<not> A \<or> 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 "\<not> A \<or> 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"\<not>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 * (\<Sum>i::nat\<le>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 * (\<Sum>i::nat\<le>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 * (\<Sum>i::nat \<le> 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"\<Longrightarrow>"}, for example
-*}
-
-lemma "xs \<noteq> [] \<Longrightarrow> 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"\<longrightarrow>"}.
-A further improvement is shown in the following proof:
-*}
-
-lemma "map f xs = map f ys \<Longrightarrow> 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 \<Longrightarrow> 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(\<dots>)"}.
- 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"\<And>"} or @{text"\<Longrightarrow>"}}
-
-Let us now consider abstractly the situation where the goal to be proved
-contains both @{text"\<And>"} and @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"}.
-This means that in each case of the induction,
-@{text ?case} would be of the form @{prop"\<And>x. P' x \<Longrightarrow> 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 \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
- for r :: "('a \<times> 'a)set"
-where
- refl: "(x,x) \<in> r*"
-| step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> 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) \<in> r*" shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> 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) \<in> r*" and "(y,z) \<in> r*" shows "(x,z) \<in> r*"
-using assms
-proof induct
- fix x assume "(x,z) \<in> r*" -- {*@{text B}[@{text y} := @{text x}]*}
- thus "(x,z) \<in> r*" .
-next
- fix x' x y
- assume 1: "(x',x) \<in> r" and
- IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
- B: "(y,z) \<in> r*"
- from 1 IH[OF B] show "(x',z) \<in> 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) \<in> r* \<Longrightarrow> ?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 \<Rightarrow> '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 \<noteq> [] \<Longrightarrow> 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 "\<dots> = b # tl(a # cs) @ [hd(a # cs)]" by(simp add:3)
- also have "\<dots> = 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"\<And>"}-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 \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
-by (induct xs rule: rot.induct) simp_all
-
-(*<*)end(*>*)
-(*
-lemma assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
- shows "P(n::nat)"
-proof (rule A)
- show "\<And>m. m < n \<Longrightarrow> 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 \<Longrightarrow> 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 \<noteq> n"
- with Suc have "m < n" by arith
- thus "P m" by(rule Suc)
- qed
- qed
-qed
-*)
\ No newline at end of file
--- 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 \<longrightarrow> 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 \<Longrightarrow> 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 \<longrightarrow>
-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 \<longrightarrow> 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 \<longrightarrow> 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 \<longrightarrow> A \<and> A"
-proof
- assume a: "A"
- from a and a show "A \<and> 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 \<longrightarrow> A \<and> A"
-proof
- assume a: "A"
- from a and a show "A \<and> 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 \<and> B \<longrightarrow> B \<and> A"
-proof
- assume ab: "A \<and> B"
- show "B \<and> 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 \<and> B \<longrightarrow> B \<and> A"
-proof
- assume ab: "A \<and> B"
- from ab show "B \<and> 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 \<and> B \<longrightarrow> B \<and> A"
-proof
- assume "A \<and> B"
- from this show "B \<and> 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 \<and> B \<longrightarrow> B \<and> A"
-proof
- assume ab: "A \<and> B"
- from ab have a: "A" ..
- from ab have b: "B" ..
- from b a show "B \<and> 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 "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
-proof
- assume n: "\<not> (A \<and> B)"
- show "\<not> A \<or> \<not> B"
- proof (rule ccontr)
- assume nn: "\<not> (\<not> A \<or> \<not> B)"
- have "\<not> A"
- proof
- assume a: "A"
- have "\<not> B"
- proof
- assume b: "B"
- from a and b have "A \<and> B" ..
- with n show False ..
- qed
- hence "\<not> A \<or> \<not> B" ..
- with nn show False ..
- qed
- hence "\<not> A \<or> \<not> 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"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example:
-*}
-lemma "A \<and> B \<Longrightarrow> B \<and> A"
-proof
- assume "A \<and> B" thus "B" ..
-next
- assume "A \<and> B" thus "A" ..
-qed
-text{*\noindent The \isakeyword{proof} always works on the conclusion,
-@{prop"B \<and> 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 \<and> 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 \<and> large_B \<Longrightarrow> large_B \<and> large_A"
- (is "?AB \<Longrightarrow> ?B \<and> ?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 \<and> large_B"
- shows "large_B \<and> large_A" (is "?B \<and> ?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 \<and> large_B"
- shows "large_B \<and> large_A" (is "?B \<and> ?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 \<or> 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 \<or> B" shows "B \<or> 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 \<or> B"} directly
-into the proof, thus triggering the elimination rule: *}
-lemma assumes ab: "A \<or> B" shows "B \<or> 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 \<or> B`"} (enclosing the formula in back quotes)
-refers to the fact @{text"A \<or> B"}
-without the need to name it. Here is a simple example, a revised version
-of the previous proof *}
-
-lemma assumes "A \<or> B" shows "B \<or> A"
-using `A \<or> 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 \<or> 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 \<and> B" shows "B \<and> A"
-proof -
- from `A \<and> B` have "B" ..
- moreover
- from `A \<and> B` have "A" ..
- ultimately show "B \<and> 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"\<And>"}
-(the universal quantifier at the
-meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
-@{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are
-applied implicitly: *}
-lemma assumes P: "\<forall>x. P x" shows "\<forall>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"\<exists>"} which is a bit more tricky.
-*}
-
-lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>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: "\<exists>x. P(f x)" shows "\<exists>y. P y"
-proof -
- from Pf obtain x where "P(f x)" ..
- thus "\<exists>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: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
-proof
- fix y
- from ex obtain x where "\<forall>y. P x y" ..
- hence "P x y" ..
- thus "\<exists>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 "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-proof
- let ?S = "{x. x \<notin> f x}"
- show "?S \<notin> range f"
- proof
- assume "?S \<in> range f"
- then obtain y where "?S = f y" ..
- show False
- proof cases
- assume "y \<in> ?S"
- with `?S = f y` show False by blast
- next
- assume "y \<notin> ?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 \<Longrightarrow> ?thesis"} and @{text"\<not>P \<Longrightarrow> ?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 "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-proof
- let ?S = "{x. x \<notin> f x}"
- show "?S \<notin> range f"
- proof
- assume "?S \<in> range f"
- then obtain y where "?S = f y" ..
- show False
- proof cases
- assume "y \<in> ?S"
- hence "y \<notin> f y" by simp
- hence "y \<notin> ?S" by(simp add: `?S = f y`)
- with `y \<in> ?S` show False by contradiction
- next
- assume "y \<notin> ?S"
- hence "y \<in> f y" by simp
- hence "y \<in> ?S" by(simp add: `?S = f y`)
- with `y \<notin> ?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 "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> '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 "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
-proof
- fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y"
- proof
- fix y show "A x y \<and> B x y \<longrightarrow> C x y"
- proof
- assume "A x y \<and> 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 "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
-proof -
- have "\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> 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 "\<forall>x y. A x y \<and> B x y \<longrightarrow> 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"\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> 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 \<or> P\<^isub>2 \<or> 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"\<And>"}: *}
-
-theorem "\<And>f :: 'a \<Rightarrow> 'a set. \<exists>S. S \<notin> 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 \<Rightarrow> 'a set" shows "\<exists>S. S \<notin> range f"
-(*<*)oops(*>*)
-text{* \noindent
-Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:*}
-
-lemma comm_mono:
- fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix ">" 60) and
- f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "++" 70)
- assumes comm: "\<And>x y::'a. x ++ y = y ++ x" and
- mono: "\<And>x y z::'a. x > y \<Longrightarrow> x ++ z > y ++ z"
- shows "x > y \<Longrightarrow> 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: "\<exists>x y. P x y \<and> 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"\<exists>"} 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 \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
-proof
- assume a: "A"
- show "(A \<longrightarrow>B) \<longrightarrow> 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(*>*)
--- 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"];
--- 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:
--- 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:
--- 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
--- 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.
--- 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
--- 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}}
-
--- 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}
--- 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 = <FILE>; $/ = "\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"; }
-}
--- 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