1.1 --- a/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 11:59:15 2001 +0100
1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Wed Jan 24 12:29:10 2001 +0100
1.3 @@ -1,6 +1,6 @@
1.4 (*<*)theory CTL = Base:;(*>*)
1.5
1.6 -subsection{*Computation Tree Logic---CTL*};
1.7 +subsection{*Computation Tree Logic --- CTL*};
1.8
1.9 text{*\label{sec:CTL}
1.10 The semantics of PDL only needs reflexive transitive closure.
2.1 --- a/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 24 11:59:15 2001 +0100
2.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 24 12:29:10 2001 +0100
2.3 @@ -125,7 +125,7 @@
2.4
2.5 text{*
2.6 The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
2.7 -that the assumption is left unchanged---otherwise the @{text"\<forall>p"} is turned
2.8 +that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
2.9 into a @{text"\<And>p"}, which would complicate matters below. As it is,
2.10 @{thm[source]Avoid_in_lfp} is now
2.11 @{thm[display]Avoid_in_lfp[no_vars]}
3.1 --- a/doc-src/TutorialI/CTL/PDL.thy Wed Jan 24 11:59:15 2001 +0100
3.2 +++ b/doc-src/TutorialI/CTL/PDL.thy Wed Jan 24 12:29:10 2001 +0100
3.3 @@ -1,6 +1,6 @@
3.4 (*<*)theory PDL = Base:(*>*)
3.5
3.6 -subsection{*Propositional Dynamic Logic---PDL*}
3.7 +subsection{*Propositional Dynamic Logic --- PDL*}
3.8
3.9 text{*\index{PDL|(}
3.10 The formulae of PDL are built up from atomic propositions via the customary
3.11 @@ -68,7 +68,7 @@
3.12 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
3.13 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
3.14 find it hard to see that @{term"mc(EF f)"} contains exactly those states from
3.15 -which there is a path to a state where @{term f} is true, do not worry---that
3.16 +which there is a path to a state where @{term f} is true, do not worry --- that
3.17 will be proved in a moment.
3.18
3.19 First we prove monotonicity of the function inside @{term lfp}
4.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 24 11:59:15 2001 +0100
4.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Jan 24 12:29:10 2001 +0100
4.3 @@ -2,7 +2,7 @@
4.4 \begin{isabellebody}%
4.5 \def\isabellecontext{CTL}%
4.6 %
4.7 -\isamarkupsubsection{Computation Tree Logic---CTL%
4.8 +\isamarkupsubsection{Computation Tree Logic --- CTL%
4.9 }
4.10 %
4.11 \begin{isamarkuptext}%
5.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 11:59:15 2001 +0100
5.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 24 12:29:10 2001 +0100
5.3 @@ -128,7 +128,7 @@
5.4 \isacommand{done}%
5.5 \begin{isamarkuptext}%
5.6 The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
5.7 -that the assumption is left unchanged---otherwise the \isa{{\isasymforall}p} is turned
5.8 +that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
5.9 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
5.10 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
5.11 \begin{isabelle}%
6.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 11:59:15 2001 +0100
6.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Jan 24 12:29:10 2001 +0100
6.3 @@ -2,7 +2,7 @@
6.4 \begin{isabellebody}%
6.5 \def\isabellecontext{PDL}%
6.6 %
6.7 -\isamarkupsubsection{Propositional Dynamic Logic---PDL%
6.8 +\isamarkupsubsection{Propositional Dynamic Logic --- PDL%
6.9 }
6.10 %
6.11 \begin{isamarkuptext}%
6.12 @@ -68,7 +68,7 @@
6.13 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
6.14 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
6.15 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
6.16 -which there is a path to a state where \isa{f} is true, do not worry---that
6.17 +which there is a path to a state where \isa{f} is true, do not worry --- that
6.18 will be proved in a moment.
6.19
6.20 First we prove monotonicity of the function inside \isa{lfp}
7.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Jan 24 11:59:15 2001 +0100
7.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Jan 24 12:29:10 2001 +0100
7.3 @@ -49,7 +49,7 @@
7.4 @{text"exec"} that takes a list of instructions, a store (modelled as a
7.5 function from addresses to values, just like the environment for
7.6 evaluating expressions), and a stack (modelled as a list) of values,
7.7 -and returns the stack at the end of the execution---the store remains
7.8 +and returns the stack at the end of the execution --- the store remains
7.9 unchanged:
7.10 *}
7.11
7.12 @@ -110,15 +110,15 @@
7.13 apply(induct_tac xs, simp, simp split: instr.split);
7.14 (*<*)done(*>*)
7.15 text{*\noindent
7.16 -Note that because \isaindex{auto} performs simplification, it can
7.17 -also be modified in the same way @{text simp} can. Thus the proof can be
7.18 +Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
7.19 +be modified in the same way @{text simp} can. Thus the proof can be
7.20 rewritten as
7.21 *}
7.22 (*<*)
7.23 declare exec_app[simp del];
7.24 lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
7.25 (*>*)
7.26 -apply(induct_tac xs, auto split: instr.split);
7.27 +apply(induct_tac xs, simp_all split: instr.split);
7.28 (*<*)done(*>*)
7.29 text{*\noindent
7.30 Although this is more compact, it is less clear for the reader of the proof.
8.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 24 11:59:15 2001 +0100
8.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 24 12:29:10 2001 +0100
8.3 @@ -46,7 +46,7 @@
8.4 \isa{exec} that takes a list of instructions, a store (modelled as a
8.5 function from addresses to values, just like the environment for
8.6 evaluating expressions), and a stack (modelled as a list) of values,
8.7 -and returns the stack at the end of the execution---the store remains
8.8 +and returns the stack at the end of the execution --- the store remains
8.9 unchanged:%
8.10 \end{isamarkuptext}%
8.11 \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline
8.12 @@ -102,11 +102,11 @@
8.13 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
8.14 \begin{isamarkuptext}%
8.15 \noindent
8.16 -Note that because \isaindex{auto} performs simplification, it can
8.17 -also be modified in the same way \isa{simp} can. Thus the proof can be
8.18 +Note that because both \isaindex{simp_all} and \isaindex{auto} perform simplification, they can
8.19 +be modified in the same way \isa{simp} can. Thus the proof can be
8.20 rewritten as%
8.21 \end{isamarkuptext}%
8.22 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ auto\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
8.23 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
8.24 \begin{isamarkuptext}%
8.25 \noindent
8.26 Although this is more compact, it is less clear for the reader of the proof.
9.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy Wed Jan 24 11:59:15 2001 +0100
9.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy Wed Jan 24 12:29:10 2001 +0100
9.3 @@ -28,13 +28,13 @@
9.4 text{*\noindent
9.5 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
9.6 except that we have fixed the values to be of type @{typ"nat"} and that we
9.7 -have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean
9.8 +have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean
9.9 expressions can be arithmetic comparisons, conjunctions and negations.
9.10 The semantics is fixed via two evaluation functions
9.11 *}
9.12
9.13 -consts evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
9.14 - evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
9.15 +consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
9.16 + evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
9.17
9.18 text{*\noindent
9.19 that take an expression and an environment (a mapping from variables @{typ"'a"} to values
9.20 @@ -53,15 +53,15 @@
9.21 "evala (Num n) env = n"
9.22
9.23 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
9.24 - "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
9.25 - "evalb (Neg b) env = (\\<not> evalb b env)"
9.26 + "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)"
9.27 + "evalb (Neg b) env = (\<not> evalb b env)"
9.28
9.29 text{*\noindent
9.30 In the same fashion we also define two functions that perform substitution:
9.31 *}
9.32
9.33 -consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
9.34 - substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
9.35 +consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
9.36 + substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp";
9.37
9.38 text{*\noindent
9.39 The first argument is a function mapping variables to expressions, the
9.40 @@ -93,8 +93,8 @@
9.41 theorems simultaneously:
9.42 *}
9.43
9.44 -lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
9.45 - evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
9.46 +lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
9.47 + evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
9.48 apply(induct_tac a and b);
9.49
9.50 txt{*\noindent
9.51 @@ -110,7 +110,7 @@
9.52 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
9.53 where each variable $x@i$ is of type $\tau@i$. Induction is started by
9.54 \begin{isabelle}
9.55 -\isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"}
9.56 +\isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"}
9.57 \end{isabelle}
9.58
9.59 \begin{exercise}
10.1 --- a/doc-src/TutorialI/Datatype/Nested.thy Wed Jan 24 11:59:15 2001 +0100
10.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy Wed Jan 24 12:29:10 2001 +0100
10.3 @@ -9,12 +9,12 @@
10.4 where function symbols can be applied to a list of arguments:
10.5 *}
10.6 (*<*)hide const Var(*>*)
10.7 -datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
10.8 +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
10.9
10.10 text{*\noindent
10.11 Note that we need to quote @{text term} on the left to avoid confusion with
10.12 the Isabelle command \isacommand{term}.
10.13 -Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of
10.14 +Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of
10.15 function symbols.
10.16 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
10.17 [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are
10.18 @@ -41,8 +41,8 @@
10.19 *}
10.20
10.21 consts
10.22 -subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term \<Rightarrow> ('a,'b)term"
10.23 -substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list";
10.24 +subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term"
10.25 +substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list";
10.26
10.27 primrec
10.28 "subst s (Var x) = s x"
10.29 @@ -62,8 +62,8 @@
10.30 strengthened and proved as follows:
10.31 *}
10.32
10.33 -lemma "subst Var t = (t ::('a,'b)term) \<and>
10.34 - substs Var ts = (ts::('a,'b)term list)";
10.35 +lemma "subst Var t = (t ::('v,'f)term) \<and>
10.36 + substs Var ts = (ts::('v,'f)term list)";
10.37 apply(induct_tac t and ts, simp_all);
10.38 done
10.39
10.40 @@ -72,7 +72,7 @@
10.41 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also
10.42 that the type annotations are necessary because otherwise there is nothing in
10.43 the goal to enforce that both halves of the goal talk about the same type
10.44 -parameters @{text"('a,'b)"}. As a result, induction would fail
10.45 +parameters @{text"('v,'f)"}. As a result, induction would fail
10.46 because the two halves of the goal would be unrelated.
10.47
10.48 \begin{exercise}
10.49 @@ -84,7 +84,7 @@
10.50 its definition is found in theorem @{thm[source]o_def}).
10.51 \end{exercise}
10.52 \begin{exercise}\label{ex:trev-trev}
10.53 - Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}
10.54 + Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"}
10.55 that recursively reverses the order of arguments of all function symbols in a
10.56 term. Prove that @{prop"trev(trev t) = t"}.
10.57 \end{exercise}
10.58 @@ -120,7 +120,7 @@
10.59 and to define functions with \isacommand{recdef} instead.
10.60 The details are explained in \S\ref{sec:nested-recdef} below.
10.61
10.62 -Of course, you may also combine mutual and nested recursion. For example,
10.63 +Of course, you may also combine mutual and nested recursion of datatypes. For example,
10.64 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
10.65 expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.
10.66 *}
11.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 24 11:59:15 2001 +0100
11.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 24 12:29:10 2001 +0100
11.3 @@ -27,7 +27,7 @@
11.4 \noindent
11.5 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
11.6 except that we have fixed the values to be of type \isa{nat} and that we
11.7 -have fixed the two binary operations \isa{aexp{\isachardot}Sum} and \isa{Diff}. Boolean
11.8 +have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
11.9 expressions can be arithmetic comparisons, conjunctions and negations.
11.10 The semantics is fixed via two evaluation functions%
11.11 \end{isamarkuptext}%
11.12 @@ -100,7 +100,7 @@
11.13 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
11.14 where each variable $x@i$ is of type $\tau@i$. Induction is started by
11.15 \begin{isabelle}
11.16 -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isa{and} \dots\ \isa{and} $x@n$\isa{{\isacharparenright}}
11.17 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
11.18 \end{isabelle}
11.19
11.20 \begin{exercise}
12.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed Jan 24 11:59:15 2001 +0100
12.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Jan 24 12:29:10 2001 +0100
12.3 @@ -8,12 +8,12 @@
12.4 constructor. This is not the case any longer for the following model of terms
12.5 where function symbols can be applied to a list of arguments:%
12.6 \end{isamarkuptext}%
12.7 -\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
12.8 +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}%
12.9 \begin{isamarkuptext}%
12.10 \noindent
12.11 Note that we need to quote \isa{term} on the left to avoid confusion with
12.12 the Isabelle command \isacommand{term}.
12.13 -Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of
12.14 +Parameter \isa{{\isacharprime}v} is the type of variables and \isa{{\isacharprime}f} the type of
12.15 function symbols.
12.16 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
12.17 suitable values, e.g.\ numbers or strings.
12.18 @@ -38,8 +38,8 @@
12.19 lists, we need to define two substitution functions simultaneously:%
12.20 \end{isamarkuptext}%
12.21 \isacommand{consts}\isanewline
12.22 -subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
12.23 -substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}\isanewline
12.24 +subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\isanewline
12.25 +substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}\isanewline
12.26 \isanewline
12.27 \isacommand{primrec}\isanewline
12.28 \ \ {\isachardoublequote}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequote}\isanewline
12.29 @@ -58,8 +58,8 @@
12.30 the fact that the identity substitution does not change a term needs to be
12.31 strengthened and proved as follows:%
12.32 \end{isamarkuptext}%
12.33 -\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
12.34 -\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
12.35 +\isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline
12.36 +\ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline
12.37 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
12.38 \isacommand{done}%
12.39 \begin{isamarkuptext}%
12.40 @@ -68,7 +68,7 @@
12.41 leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also
12.42 that the type annotations are necessary because otherwise there is nothing in
12.43 the goal to enforce that both halves of the goal talk about the same type
12.44 -parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail
12.45 +parameters \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}}. As a result, induction would fail
12.46 because the two halves of the goal would be unrelated.
12.47
12.48 \begin{exercise}
12.49 @@ -82,7 +82,7 @@
12.50 its definition is found in theorem \isa{o{\isacharunderscore}def}).
12.51 \end{exercise}
12.52 \begin{exercise}\label{ex:trev-trev}
12.53 - Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term}
12.54 + Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term}
12.55 that recursively reverses the order of arguments of all function symbols in a
12.56 term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
12.57 \end{exercise}
12.58 @@ -118,7 +118,7 @@
12.59 and to define functions with \isacommand{recdef} instead.
12.60 The details are explained in \S\ref{sec:nested-recdef} below.
12.61
12.62 -Of course, you may also combine mutual and nested recursion. For example,
12.63 +Of course, you may also combine mutual and nested recursion of datatypes. For example,
12.64 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
12.65 expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
12.66 \end{isamarkuptext}%
13.1 --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 24 11:59:15 2001 +0100
13.2 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 24 12:29:10 2001 +0100
13.3 @@ -1,8 +1,8 @@
13.4 %
13.5 \begin{isabellebody}%
13.6 \def\isabellecontext{unfoldnested}%
13.7 -\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
13.8 -\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
13.9 +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
13.10 +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
13.11 %%% Local Variables:
13.12 %%% mode: latex
13.13 %%% TeX-master: "root"
14.1 --- a/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 11:59:15 2001 +0100
14.2 +++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 12:29:10 2001 +0100
14.3 @@ -1,8 +1,8 @@
14.4 (*<*)
14.5 theory unfoldnested = Main:;
14.6 (*>*)
14.7 -datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
14.8 -and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
14.9 +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
14.10 +and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
14.11 (*<*)
14.12 end
14.13 (*>*)
15.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 11:59:15 2001 +0100
15.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jan 24 12:29:10 2001 +0100
15.3 @@ -55,7 +55,7 @@
15.4 datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
15.5
15.6 text{*\noindent
15.7 -The evaluation if If-expressions proceeds as for @{typ"boolex"}:
15.8 +The evaluation of If-expressions proceeds as for @{typ"boolex"}:
15.9 *}
15.10
15.11 consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
16.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 24 11:59:15 2001 +0100
16.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 24 12:29:10 2001 +0100
16.3 @@ -55,7 +55,7 @@
16.4 \isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex%
16.5 \begin{isamarkuptext}%
16.6 \noindent
16.7 -The evaluation if If-expressions proceeds as for \isa{boolex}:%
16.8 +The evaluation of If-expressions proceeds as for \isa{boolex}:%
16.9 \end{isamarkuptext}%
16.10 \isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
16.11 \isacommand{primrec}\isanewline
17.1 --- a/doc-src/TutorialI/Misc/Itrev.thy Wed Jan 24 11:59:15 2001 +0100
17.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Jan 24 12:29:10 2001 +0100
17.3 @@ -26,7 +26,7 @@
17.4 The key heuristic, and the main point of this section, is to
17.5 generalize the goal before induction. The reason is simple: if the goal is
17.6 too specific, the induction hypothesis is too weak to allow the induction
17.7 -step to go through. Let us now illustrate the idea with an example.
17.8 +step to go through. Let us illustrate the idea with an example.
17.9
17.10 Function @{term"rev"} has quadratic worst-case running time
17.11 because it calls function @{text"@"} for each element of the list and
17.12 @@ -61,7 +61,7 @@
17.13
17.14 txt{*\noindent
17.15 Unfortunately, this is not a complete success:
17.16 -@{subgoals[display,indent=0,margin=65]}
17.17 +@{subgoals[display,indent=0,margin=70]}
17.18 Just as predicted above, the overall goal, and hence the induction
17.19 hypothesis, is too weak to solve the induction step because of the fixed
17.20 argument, @{term"[]"}. This suggests a heuristic:
17.21 @@ -69,7 +69,7 @@
17.22 \emph{Generalize goals for induction by replacing constants by variables.}
17.23 \end{quote}
17.24 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
17.25 -just not true---the correct generalization is
17.26 +just not true --- the correct generalization is
17.27 *};
17.28 (*<*)oops;(*>*)
17.29 lemma "itrev xs ys = rev xs @ ys";
17.30 @@ -112,13 +112,6 @@
17.31 The variables that require generalization are typically those that
17.32 change in recursive calls.
17.33
17.34 -In general, if you have tried the above heuristics and still find your
17.35 -induction does not go through, and no obvious lemma suggests itself, you may
17.36 -need to generalize your proposition even further. This requires insight into
17.37 -the problem at hand and is beyond simple rules of thumb. You
17.38 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
17.39 -to learn about some advanced techniques for inductive proofs.
17.40 -
17.41 A final point worth mentioning is the orientation of the equation we just
17.42 proved: the more complex notion (@{term itrev}) is on the left-hand
17.43 side, the simpler one (@{term rev}) on the right-hand side. This constitutes
17.44 @@ -130,6 +123,13 @@
17.45 This heuristic is tricky to apply because it is not obvious that
17.46 @{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
17.47 happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
17.48 +
17.49 +In general, if you have tried the above heuristics and still find your
17.50 +induction does not go through, and no obvious lemma suggests itself, you may
17.51 +need to generalize your proposition even further. This requires insight into
17.52 +the problem at hand and is beyond simple rules of thumb. You
17.53 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
17.54 +to learn about some advanced techniques for inductive proofs.
17.55 *}
17.56 (*<*)
17.57 end
18.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 24 11:59:15 2001 +0100
18.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 24 12:29:10 2001 +0100
18.3 @@ -28,7 +28,7 @@
18.4 The key heuristic, and the main point of this section, is to
18.5 generalize the goal before induction. The reason is simple: if the goal is
18.6 too specific, the induction hypothesis is too weak to allow the induction
18.7 -step to go through. Let us now illustrate the idea with an example.
18.8 +step to go through. Let us illustrate the idea with an example.
18.9
18.10 Function \isa{rev} has quadratic worst-case running time
18.11 because it calls function \isa{{\isacharat}} for each element of the list and
18.12 @@ -62,8 +62,7 @@
18.13 Unfortunately, this is not a complete success:
18.14 \begin{isabelle}%
18.15 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
18.16 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\isanewline
18.17 -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
18.18 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
18.19 \end{isabelle}
18.20 Just as predicted above, the overall goal, and hence the induction
18.21 hypothesis, is too weak to solve the induction step because of the fixed
18.22 @@ -72,7 +71,7 @@
18.23 \emph{Generalize goals for induction by replacing constants by variables.}
18.24 \end{quote}
18.25 Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
18.26 -just not true---the correct generalization is%
18.27 +just not true --- the correct generalization is%
18.28 \end{isamarkuptxt}%
18.29 \isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
18.30 \begin{isamarkuptxt}%
18.31 @@ -114,13 +113,6 @@
18.32 The variables that require generalization are typically those that
18.33 change in recursive calls.
18.34
18.35 -In general, if you have tried the above heuristics and still find your
18.36 -induction does not go through, and no obvious lemma suggests itself, you may
18.37 -need to generalize your proposition even further. This requires insight into
18.38 -the problem at hand and is beyond simple rules of thumb. You
18.39 -will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
18.40 -to learn about some advanced techniques for inductive proofs.
18.41 -
18.42 A final point worth mentioning is the orientation of the equation we just
18.43 proved: the more complex notion (\isa{itrev}) is on the left-hand
18.44 side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
18.45 @@ -131,7 +123,14 @@
18.46 \end{quote}
18.47 This heuristic is tricky to apply because it is not obvious that
18.48 \isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
18.49 -happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
18.50 +happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
18.51 +
18.52 +In general, if you have tried the above heuristics and still find your
18.53 +induction does not go through, and no obvious lemma suggests itself, you may
18.54 +need to generalize your proposition even further. This requires insight into
18.55 +the problem at hand and is beyond simple rules of thumb. You
18.56 +will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
18.57 +to learn about some advanced techniques for inductive proofs.%
18.58 \end{isamarkuptext}%
18.59 \end{isabellebody}%
18.60 %%% Local Variables:
19.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 11:59:15 2001 +0100
19.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 24 12:29:10 2001 +0100
19.3 @@ -69,7 +69,8 @@
19.4 For more complex goals, there is the special method \isaindexbold{arith}
19.5 (which attacks the first subgoal). It proves arithmetic goals involving the
19.6 usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
19.7 -\isa{{\isasymlongrightarrow}}), the relations \isa{{\isasymle}} and \isa{{\isacharless}}, and the operations
19.8 +\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
19.9 +and the operations
19.10 \isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
19.11 known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
19.12 For example,%
20.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 11:59:15 2001 +0100
20.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 24 12:29:10 2001 +0100
20.3 @@ -52,7 +52,7 @@
20.4 where the list of \emph{modifiers} fine tunes the behaviour and may
20.5 be empty. Most if not all of the proofs seen so far could have been performed
20.6 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
20.7 -only the first subgoal and may thus need to be repeated---use
20.8 +only the first subgoal and may thus need to be repeated --- use
20.9 \isaindex{simp_all} to simplify all subgoals.
20.10 Note that \isa{simp} fails if nothing changes.%
20.11 \end{isamarkuptext}%
20.12 @@ -109,7 +109,7 @@
20.13 \isacommand{done}%
20.14 \begin{isamarkuptext}%
20.15 \noindent
20.16 -There are three options that influence the treatment of assumptions:
20.17 +There are three modifiers that influence the treatment of assumptions:
20.18 \begin{description}
20.19 \item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
20.20 means that assumptions are completely ignored.
20.21 @@ -122,7 +122,7 @@
20.22 \end{description}
20.23 Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
20.24 the problematic subgoal above.
20.25 -Note that only one of the options is allowed, and it must precede all
20.26 +Note that only one of the modifiers is allowed, and it must precede all
20.27 other arguments.%
20.28 \end{isamarkuptext}%
20.29 %
20.30 @@ -169,13 +169,14 @@
20.31 rule because this defeats the whole purpose of an abbreviation.
20.32
20.33 \begin{warn}
20.34 - If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
20.35 - occurrences of $f$ with at least two arguments. Thus it is safer to define
20.36 - $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
20.37 + If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
20.38 + occurrences of $f$ with at least two arguments. This may be helpful for unfolding
20.39 + $f$ selectively, but it may also get in the way. Defining
20.40 + $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
20.41 \end{warn}%
20.42 \end{isamarkuptext}%
20.43 %
20.44 -\isamarkupsubsubsection{Simplifying Let-Expressions%
20.45 +\isamarkupsubsubsection{Simplifying {\tt\slshape let}-Expressions%
20.46 }
20.47 %
20.48 \begin{isamarkuptext}%
20.49 @@ -360,7 +361,7 @@
20.50 Applying instance of rewrite rule:
20.51 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
20.52 Rewriting:
20.53 -rev [x] == rev [] @ [x]
20.54 +rev [a] == rev [] @ [a]
20.55 Applying instance of rewrite rule:
20.56 rev [] == []
20.57 Rewriting:
20.58 @@ -368,11 +369,11 @@
20.59 Applying instance of rewrite rule:
20.60 [] @ ?y == ?y
20.61 Rewriting:
20.62 -[] @ [x] == [x]
20.63 +[] @ [a] == [a]
20.64 Applying instance of rewrite rule:
20.65 ?x3 \# ?t3 = ?t3 == False
20.66 Rewriting:
20.67 -[x] = [] == False
20.68 +[a] = [] == False
20.69 \end{ttbox}
20.70
20.71 In more complicated cases, the trace can be quite lenghty, especially since
21.1 --- a/doc-src/TutorialI/Misc/natsum.thy Wed Jan 24 11:59:15 2001 +0100
21.2 +++ b/doc-src/TutorialI/Misc/natsum.thy Wed Jan 24 12:29:10 2001 +0100
21.3 @@ -69,7 +69,8 @@
21.4 For more complex goals, there is the special method \isaindexbold{arith}
21.5 (which attacks the first subgoal). It proves arithmetic goals involving the
21.6 usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
21.7 -@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
21.8 +@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
21.9 +and the operations
21.10 @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
21.11 known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
21.12 For example,
22.1 --- a/doc-src/TutorialI/Misc/simp.thy Wed Jan 24 11:59:15 2001 +0100
22.2 +++ b/doc-src/TutorialI/Misc/simp.thy Wed Jan 24 12:29:10 2001 +0100
22.3 @@ -49,7 +49,7 @@
22.4 where the list of \emph{modifiers} fine tunes the behaviour and may
22.5 be empty. Most if not all of the proofs seen so far could have been performed
22.6 with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
22.7 -only the first subgoal and may thus need to be repeated---use
22.8 +only the first subgoal and may thus need to be repeated --- use
22.9 \isaindex{simp_all} to simplify all subgoals.
22.10 Note that @{text simp} fails if nothing changes.
22.11 *}
22.12 @@ -106,7 +106,7 @@
22.13 done
22.14
22.15 text{*\noindent
22.16 -There are three options that influence the treatment of assumptions:
22.17 +There are three modifiers that influence the treatment of assumptions:
22.18 \begin{description}
22.19 \item[@{text"(no_asm)"}]\indexbold{*no_asm}
22.20 means that assumptions are completely ignored.
22.21 @@ -119,7 +119,7 @@
22.22 \end{description}
22.23 Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
22.24 the problematic subgoal above.
22.25 -Note that only one of the options is allowed, and it must precede all
22.26 +Note that only one of the modifiers is allowed, and it must precede all
22.27 other arguments.
22.28 *}
22.29
22.30 @@ -165,13 +165,14 @@
22.31 rule because this defeats the whole purpose of an abbreviation.
22.32
22.33 \begin{warn}
22.34 - If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
22.35 - occurrences of $f$ with at least two arguments. Thus it is safer to define
22.36 - $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
22.37 + If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
22.38 + occurrences of $f$ with at least two arguments. This may be helpful for unfolding
22.39 + $f$ selectively, but it may also get in the way. Defining
22.40 + $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
22.41 \end{warn}
22.42 *}
22.43
22.44 -subsubsection{*Simplifying Let-Expressions*}
22.45 +subsubsection{*Simplifying {\tt\slshape let}-Expressions*}
22.46
22.47 text{*\index{simplification!of let-expressions}
22.48 Proving a goal containing \isaindex{let}-expressions almost invariably
22.49 @@ -370,7 +371,7 @@
22.50 Applying instance of rewrite rule:
22.51 rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
22.52 Rewriting:
22.53 -rev [x] == rev [] @ [x]
22.54 +rev [a] == rev [] @ [a]
22.55 Applying instance of rewrite rule:
22.56 rev [] == []
22.57 Rewriting:
22.58 @@ -378,11 +379,11 @@
22.59 Applying instance of rewrite rule:
22.60 [] @ ?y == ?y
22.61 Rewriting:
22.62 -[] @ [x] == [x]
22.63 +[] @ [a] == [a]
22.64 Applying instance of rewrite rule:
22.65 ?x3 \# ?t3 = ?t3 == False
22.66 Rewriting:
22.67 -[x] = [] == False
22.68 +[a] = [] == False
22.69 \end{ttbox}
22.70
22.71 In more complicated cases, the trace can be quite lenghty, especially since
23.1 --- a/doc-src/TutorialI/Recdef/Induction.thy Wed Jan 24 11:59:15 2001 +0100
23.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy Wed Jan 24 12:29:10 2001 +0100
23.3 @@ -8,7 +8,7 @@
23.4 equations) are simplification rules, we might like to prove something about
23.5 our function. Since the function is recursive, the natural proof principle is
23.6 again induction. But this time the structural form of induction that comes
23.7 -with datatypes is unlikely to work well---otherwise we could have defined the
23.8 +with datatypes is unlikely to work well --- otherwise we could have defined the
23.9 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
23.10 proves a suitable induction rule $f$@{text".induct"} that follows the
23.11 recursion pattern of the particular function $f$. We call this
23.12 @@ -51,7 +51,7 @@
23.13 \end{quote}\index{*induct_tac}%
23.14 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
23.15 name of a function that takes an $n$-tuple. Usually the subgoal will
23.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
23.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
23.18 induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
23.19 \begin{isabelle}
23.20 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
24.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 11:59:15 2001 +0100
24.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 12:29:10 2001 +0100
24.3 @@ -8,7 +8,7 @@
24.4 equations) are simplification rules, we might like to prove something about
24.5 our function. Since the function is recursive, the natural proof principle is
24.6 again induction. But this time the structural form of induction that comes
24.7 -with datatypes is unlikely to work well---otherwise we could have defined the
24.8 +with datatypes is unlikely to work well --- otherwise we could have defined the
24.9 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
24.10 proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
24.11 recursion pattern of the particular function $f$. We call this
24.12 @@ -53,7 +53,7 @@
24.13 \end{quote}\index{*induct_tac}%
24.14 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
24.15 name of a function that takes an $n$-tuple. Usually the subgoal will
24.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
24.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
24.18 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
24.19 \begin{isabelle}
24.20 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
25.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 11:59:15 2001 +0100
25.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 24 12:29:10 2001 +0100
25.3 @@ -30,7 +30,7 @@
25.4 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
25.5 \begin{isamarkuptxt}%
25.6 \noindent
25.7 -It was not proved automatically because of the special nature of \isa{{\isacharminus}}
25.8 +It was not proved automatically because of the special nature of subtraction
25.9 on \isa{nat}. This requires more arithmetic than is tried by default:%
25.10 \end{isamarkuptxt}%
25.11 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
26.1 --- a/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 11:59:15 2001 +0100
26.2 +++ b/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 12:29:10 2001 +0100
26.3 @@ -32,7 +32,7 @@
26.4 lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
26.5
26.6 txt{*\noindent
26.7 -It was not proved automatically because of the special nature of @{text"-"}
26.8 +It was not proved automatically because of the special nature of subtraction
26.9 on @{typ"nat"}. This requires more arithmetic than is tried by default:
26.10 *}
26.11
27.1 --- a/doc-src/TutorialI/Rules/rules.tex Wed Jan 24 11:59:15 2001 +0100
27.2 +++ b/doc-src/TutorialI/Rules/rules.tex Wed Jan 24 12:29:10 2001 +0100
27.3 @@ -71,7 +71,7 @@
27.4 like this:
27.5 \[ \infer{P\conj Q}{P & Q} \]
27.6 The rule introduces the conjunction
27.7 -symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we
27.8 +symbol~($\conj$) in its conclusion. In Isabelle proofs we
27.9 mainly reason backwards. When we apply this rule, the subgoal already has
27.10 the form of a conjunction; the proof step makes this conjunction symbol
27.11 disappear.
27.12 @@ -170,7 +170,7 @@
27.13 \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
27.14 \end{isabelle}
27.15 When we use this sort of elimination rule backwards, it produces
27.16 -a case split. (We have this before, in proofs by induction.) The following proof
27.17 +a case split. (We have seen this before, in proofs by induction.) The following proof
27.18 illustrates the use of disjunction elimination.
27.19 \begin{isabelle}
27.20 \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\
27.21 @@ -184,7 +184,7 @@
27.22 We assume \isa{P\ \isasymor\ Q} and
27.23 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
27.24 elimination rule, \isa{disjE}. The method {\isa{erule}} applies an
27.25 -elimination rule to the assumptions, searching for one that matches the
27.26 +elimination rule, searching for an assumption that matches the
27.27 rule's first premise. Deleting that assumption, it
27.28 return the subgoals for the remaining premises. Most of the
27.29 time, this is the best way to use elimination rules; only rarely is there
27.30 @@ -394,7 +394,7 @@
27.31 As we have seen, Isabelle rules involve variables that begin with a
27.32 question mark. These are called \textbf{schematic} variables and act as
27.33 placeholders for terms. \textbf{Unification} refers to the process of
27.34 -making two terms identical, possibly by replacing their variables by
27.35 +making two terms identical, possibly by replacing their schematic variables by
27.36 terms. The simplest case is when the two terms are already the same. Next
27.37 simplest is when the variables in only one of the term
27.38 are replaced; this is called \textbf{pattern-matching}. The
27.39 @@ -440,7 +440,7 @@
27.40 A typical substitution rule allows us to replace one term by
27.41 another if we know that two terms are equal.
27.42 \[ \infer{P[t/x]}{s=t & P[s/x]} \]
27.43 -The conclusion uses a notation for substitution: $P[t/x]$ is the result of
27.44 +The rule uses a notation for substitution: $P[t/x]$ is the result of
27.45 replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions
27.46 designated by~$x$. For example, it can
27.47 derive symmetry of equality from reflexivity. Using $x=s$ for~$P$
27.48 @@ -566,7 +566,7 @@
27.49 \isa{erule_tac} since above we used \isa{erule}.
27.50 \begin{isabelle}
27.51 \isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
27.52 -\isacommand{by}\ (erule_tac\ P="\isasymlambda u.\ P\ u\ u\ x"\
27.53 +\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ P\ u\ u\ x"\
27.54 \isakeyword{in}\ ssubst)
27.55 \end{isabelle}
27.56 %
27.57 @@ -580,7 +580,7 @@
27.58 An alternative to \isa{rule_tac} is to use \isa{rule} with the
27.59 \isa{of} directive, described in \S\ref{sec:forward} below. An
27.60 advantage of \isa{rule_tac} is that the instantiations may refer to
27.61 -variables bound in the current subgoal.
27.62 +\isasymAnd-bound variables in the current subgoal.
27.63
27.64
27.65 \section{Negation}
27.66 @@ -632,7 +632,7 @@
27.67 \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
27.68 \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
27.69 R"\isanewline
27.70 -\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
27.71 +\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
27.72 contrapos_np)\isanewline
27.73 \isacommand{apply}\ intro\isanewline
27.74 \isacommand{by}\ (erule\ notE)
27.75 @@ -664,7 +664,7 @@
27.76 \isa{by} command.
27.77 Now when Isabelle selects the first assumption, it tries to prove \isa{P\
27.78 \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the
27.79 -assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That
27.80 +assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That
27.81 concludes the proof.
27.82
27.83 \medskip
27.84 @@ -691,7 +691,8 @@
27.85 \end{isabelle}
27.86 Next we apply the {\isa{elim}} method, which repeatedly applies
27.87 elimination rules; here, the elimination rules given
27.88 -in the command. One of the subgoals is trivial, leaving us with one other:
27.89 +in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}),
27.90 +leaving us with one other:
27.91 \begin{isabelle}
27.92 \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
27.93 \end{isabelle}
27.94 @@ -704,8 +705,7 @@
27.95 is robust: the \isa{conjI} forces the \isa{erule} to select a
27.96 conjunction. The two subgoals are the ones we would expect from applying
27.97 conjunction introduction to
27.98 -\isa{Q\
27.99 -\isasymand\ R}:
27.100 +\isa{Q~\isasymand~R}:
27.101 \begin{isabelle}
27.102 \ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
27.103 Q\isanewline
27.104 @@ -926,10 +926,12 @@
27.105 \end{isabelle}
27.106 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
27.107 P(x)$ is also true. It is a dual of the universal elimination rule, and
27.108 -logic texts present it using the same notation for substitution. The existential
27.109 +logic texts present it using the same notation for substitution.
27.110 +
27.111 +The existential
27.112 elimination rule looks like this
27.113 in a logic text:
27.114 -\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
27.115 +\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \]
27.116 %
27.117 It looks like this in Isabelle:
27.118 \begin{isabelle}
27.119 @@ -953,17 +955,18 @@
27.120
27.121
27.122 \section{Hilbert's Epsilon-Operator}
27.123 +\label{sec:SOME}
27.124
27.125 -Isabelle/HOL provides Hilbert's
27.126 -$\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
27.127 +HOL provides Hilbert's
27.128 +$\varepsilon$-operator. The term $\varepsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
27.129 true, provided such a value exists. Using this operator, we can express an
27.130 existential destruction rule:
27.131 -\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
27.132 +\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
27.133 This rule is seldom used, for it can cause exponential blow-up.
27.134
27.135 \subsection{Definite Descriptions}
27.136
27.137 -In ASCII, we write \isa{SOME} for $\epsilon$.
27.138 +In ASCII, we write \isa{SOME} for $\varepsilon$.
27.139 \REMARK{the internal constant is \isa{Eps}}
27.140 The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
27.141 description}: when \isa{P} is satisfied by a unique value,~\isa{a}.
27.142 @@ -979,7 +982,7 @@
27.143 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
27.144 description) and proceed to prove other facts.
27.145
27.146 -Here is an example. HOL defines \isa{inv},\indexbold{*inv (constant)}
27.147 +Here is another example. Isabelle/HOL defines \isa{inv},\indexbold{*inv (constant)}
27.148 which expresses inverses of functions, as a definite
27.149 description:
27.150 \begin{isabelle}
27.151 @@ -1025,7 +1028,6 @@
27.152 \ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline
27.153 \ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
27.154 \end{isabelle}
27.155 -
27.156 As always with \isa{some_equality}, we must show existence and
27.157 uniqueness of the claimed solution,~\isa{k}. Existence, the first
27.158 subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry:
27.159 @@ -1063,6 +1065,7 @@
27.160 \ "(\isasymforall x.\ \isasymexists \ y.\ P\ x\ y)\ \isasymLongrightarrow \
27.161 \isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline
27.162 \isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline
27.163 +
27.164 \ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\
27.165 \isasymLongrightarrow \ P\ x\ (?f\ x)
27.166 \end{isabelle}
27.167 @@ -1072,6 +1075,7 @@
27.168
27.169 \begin{isabelle}
27.170 \isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline
27.171 +
27.172 \ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x)
27.173 \end{isabelle}
27.174
27.175 @@ -1141,7 +1145,8 @@
27.176 \begin{isabelle}
27.177 *** empty result sequence -- proof command failed
27.178 \end{isabelle}
27.179 -We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
27.180 +If we interact with Isabelle via the shell interface,
27.181 +we abandon a failed proof with the \isacommand{oops} command.
27.182
27.183 \medskip
27.184
27.185 @@ -1301,7 +1306,7 @@
27.186 \begin{isabelle}
27.187 \isacommand{lemma}\
27.188 [iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\
27.189 -(xs=[]\ \isacharampersand\ ys=[])"\isanewline
27.190 +(xs=[]\ \isasymand\ ys=[])"\isanewline
27.191 \isacommand{apply}\ (induct_tac\ xs)\isanewline
27.192 \isacommand{apply}\ (simp_all)\isanewline
27.193 \isacommand{done}
27.194 @@ -1314,7 +1319,7 @@
27.195 (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
27.196 \end{isabelle}
27.197 A product is zero if and only if one of the factors is zero. The
27.198 -reasoning involves a logical \textsc{or}. Proving new rules for
27.199 +reasoning involves a disjunction. Proving new rules for
27.200 disjunctive reasoning is hard, but translating to an actual disjunction
27.201 works: the classical reasoner handles disjunction properly.
27.202
27.203 @@ -1490,8 +1495,8 @@
27.204 We state it with the \isa{iff} attribute so that
27.205 Isabelle can use it to remove some occurrences of \isa{gcd}.
27.206 The theorem has a one-line
27.207 -proof using \isa{blast} supplied with four introduction
27.208 -rules: note the {\isa{intro}} attribute. The exclamation mark
27.209 +proof using \isa{blast} supplied with two additional introduction
27.210 +rules. The exclamation mark
27.211 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are
27.212 applied aggressively. Rules given without the exclamation mark
27.213 are applied reluctantly and their uses can be undone if
27.214 @@ -1519,8 +1524,8 @@
27.215
27.216 Of the latter methods, the most useful is {\isa{clarify}}. It performs
27.217 all obvious reasoning steps without splitting the goal into multiple
27.218 -parts. It does not apply rules that could render the
27.219 -goal unprovable (so-called unsafe rules). By performing the obvious
27.220 +parts. It does not apply unsafe rules that could render the
27.221 +goal unprovable. By performing the obvious
27.222 steps, {\isa{clarify}} lays bare the difficult parts of the problem,
27.223 where human intervention is necessary.
27.224
27.225 @@ -1568,7 +1573,7 @@
27.226 That makes them slower but enables them to work correctly in the
27.227 presence of the more unusual features of Isabelle rules, such
27.228 as type classes and function unknowns. For example, recall the introduction rule
27.229 -for Hilbert's epsilon-operator:
27.230 +for Hilbert's $\varepsilon$-operator:
27.231 \begin{isabelle}
27.232 ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x)
27.233 \rulename{someI}
27.234 @@ -1796,7 +1801,7 @@
27.235 instance of a rule by specifying facts for its premises. Let us try
27.236 it with this rule:
27.237 \begin{isabelle}
27.238 -\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
27.239 +\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
27.240 \isasymLongrightarrow\ ?k\ dvd\ ?m
27.241 \rulename{relprime_dvd_mult}
27.242 \end{isabelle}
27.243 @@ -1809,7 +1814,7 @@
27.244 We have evaluated an application of the \isa{gcd} function by
27.245 simplification. Expression evaluation is not guaranteed to terminate, and
27.246 certainly is not efficient; Isabelle performs arithmetic operations by
27.247 -rewriting symbolic bit strings. Here, however, the simplification takes
27.248 +rewriting symbolic bit strings. Here, however, the simplification above takes
27.249 less than one second. We can specify this new lemma to \isa{OF},
27.250 generating an instance of \isa{relprime_dvd_mult}. The expression
27.251 \begin{isabelle}
27.252 @@ -1826,7 +1831,7 @@
27.253 \isasymlbrakk?k\ dvd\ ?m;\
27.254 ?k\ dvd\ ?n\isasymrbrakk\
27.255 \isasymLongrightarrow\ ?k\ dvd\
27.256 -(?m\ +\ ?n)
27.257 +?m\ +\ ?n
27.258 \rulename{dvd_add}\isanewline
27.259 ?m\ dvd\ ?m%
27.260 \rulename{dvd_refl}
27.261 @@ -1846,7 +1851,7 @@
27.262 \end{isabelle}
27.263 The result is
27.264 \begin{isabelle}
27.265 -\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
27.266 +\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k
27.267 \end{isabelle}
27.268
27.269 You may have noticed that \isa{THEN} and \isa{OF} are based on
27.270 @@ -1933,7 +1938,7 @@
27.271 \begin{isabelle}
27.272 \isacommand{lemma}\
27.273 relprime_dvd_mult:\isanewline
27.274 -\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ (m*n)\
27.275 +\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\ k\ dvd\ m*n\
27.276 \isasymrbrakk\
27.277 \isasymLongrightarrow\ k\ dvd\
27.278 m"\isanewline
27.279 @@ -1943,11 +1948,7 @@
27.280 In the resulting subgoal, note how the equation has been
27.281 inserted:
27.282 \begin{isabelle}
27.283 -\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
27.284 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
27.285 -m\isanewline
27.286 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
27.287 -\ \ \ \ \ m\ *\ gcd\
27.288 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
27.289 (k,\ n)\
27.290 =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
27.291 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
27.292 @@ -1956,12 +1957,8 @@
27.293 utilizes the assumption \isa{gcd(k,n)\ =\
27.294 1}. Here is the result:
27.295 \begin{isabelle}
27.296 -\isasymlbrakk gcd\ (k,\
27.297 -n)\ =\ 1;\ k\
27.298 -dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
27.299 -m\isanewline
27.300 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
27.301 -\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
27.302 +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}
27.303 +\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
27.304 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
27.305 \end{isabelle}
27.306 Simplification has yielded an equation for \isa{m} that will be used to
27.307 @@ -2042,8 +2039,7 @@
27.308 \ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
27.309 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
27.310 \end{isabelle}
27.311 -
27.312 -The first subgoal is trivial, but for the second Isabelle needs help to eliminate
27.313 +The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate
27.314 the case
27.315 \isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two
27.316 subgoals:
27.317 @@ -2056,8 +2052,8 @@
27.318 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
27.319 \end{isabelle}
27.320
27.321 -Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic:
27.322 -the method {\isa{arith}}. For the second subgoal we apply the method \isa{force},
27.323 +Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
27.324 +(\isa{arith}). For the second subgoal we apply the method \isa{force},
27.325 which proceeds by assuming that \isa{z}=35 and arriving at a contradiction.
27.326
27.327
28.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Jan 24 11:59:15 2001 +0100
28.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Wed Jan 24 12:29:10 2001 +0100
28.3 @@ -28,6 +28,7 @@
28.4 \isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
28.5 the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
28.6 and not as @{text"(x # y) # z"}.
28.7 +The @{text 65} is the priority of the infix @{text"#"}.
28.8
28.9 \begin{warn}
28.10 Syntax annotations are a powerful but optional feature. You
28.11 @@ -44,9 +45,10 @@
28.12
28.13 text{*
28.14 \noindent
28.15 -In contrast to ML, Isabelle insists on explicit declarations of all functions
28.16 -(keyword \isacommand{consts}). (Apart from the declaration-before-use
28.17 -restriction, the order of items in a theory file is unconstrained.) Function
28.18 +In contrast to many functional programming languages,
28.19 +Isabelle insists on explicit declarations of all functions
28.20 +(keyword \isacommand{consts}). Apart from the declaration-before-use
28.21 +restriction, the order of items in a theory file is unconstrained. Function
28.22 @{text"app"} is annotated with concrete syntax too. Instead of the
28.23 prefix syntax @{text"app xs ys"} the infix
28.24 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
28.25 @@ -89,11 +91,11 @@
28.26 \end{warn}
28.27
28.28 A remark about syntax. The textual definition of a theory follows a fixed
28.29 -syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
28.30 -Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
28.31 +syntax with keywords like \isacommand{datatype} and \isacommand{end}.
28.32 +% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
28.33 Embedded in this syntax are the types and formulae of HOL, whose syntax is
28.34 -extensible, e.g.\ by new user-defined infix operators
28.35 -(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
28.36 +extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
28.37 +To distinguish the two levels, everything
28.38 HOL-specific (terms and types) should be enclosed in
28.39 \texttt{"}\dots\texttt{"}.
28.40 To lessen this burden, quotation marks around a single identifier can be
28.41 @@ -179,10 +181,7 @@
28.42 By default, induction acts on the first subgoal. The new proof state contains
28.43 two subgoals, namely the base case (@{term[source]Nil}) and the induction step
28.44 (@{term[source]Cons}):
28.45 -\begin{isabelle}
28.46 -~1.~rev~(rev~[])~=~[]\isanewline
28.47 -~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
28.48 -\end{isabelle}
28.49 +@{subgoals[display,indent=0,margin=65]}
28.50
28.51 The induction step is an example of the general format of a subgoal:
28.52 \begin{isabelle}
28.53 @@ -211,9 +210,7 @@
28.54 ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
28.55 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
28.56 of subgoal~2 becomes the new subgoal~1:
28.57 -\begin{isabelle}
28.58 -~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
28.59 -\end{isabelle}
28.60 +@{subgoals[display,indent=0,margin=70]}
28.61 In order to simplify this subgoal further, a lemma suggests itself.
28.62 *}
28.63 (*<*)
28.64 @@ -231,10 +228,10 @@
28.65 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
28.66
28.67 txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
28.68 -\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
28.69 -the importance we attach to a proposition. We use the words
28.70 +\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
28.71 +the importance we attach to a proposition. Therefore we use the words
28.72 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
28.73 -interchangeably.
28.74 +interchangeably, too.
28.75
28.76 There are two variables that we could induct on: @{term"xs"} and
28.77 @{term"ys"}. Because @{text"@"} is defined by recursion on
28.78 @@ -285,8 +282,8 @@
28.79
28.80 % Instead of \isacommand{apply} followed by a dot, you can simply write
28.81 % \isacommand{by}\indexbold{by}, which we do most of the time.
28.82 -Notice that in lemma @{thm[source]app_Nil2}
28.83 -(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
28.84 +Notice that in lemma @{thm[source]app_Nil2},
28.85 +as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
28.86 replaced by the unknown @{text"?xs"}, just as explained in
28.87 \S\ref{sec:variables}.
28.88
28.89 @@ -326,7 +323,7 @@
28.90 text{*
28.91 \noindent
28.92 succeeds without further ado.
28.93 -Now we can go back and prove the first lemma
28.94 +Now we can prove the first lemma
28.95 *}
28.96
28.97 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
29.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 11:59:15 2001 +0100
29.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jan 24 12:29:10 2001 +0100
29.3 @@ -30,6 +30,7 @@
29.4 \isacommand{infixr}\indexbold{*infixr} means that \isa{{\isacharhash}} associates to
29.5 the right, i.e.\ the term \isa{x\ {\isacharhash}\ y\ {\isacharhash}\ z} is read as \isa{x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ z{\isacharparenright}}
29.6 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
29.7 +The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
29.8
29.9 \begin{warn}
29.10 Syntax annotations are a powerful but optional feature. You
29.11 @@ -44,9 +45,10 @@
29.12 \ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
29.13 \begin{isamarkuptext}%
29.14 \noindent
29.15 -In contrast to ML, Isabelle insists on explicit declarations of all functions
29.16 -(keyword \isacommand{consts}). (Apart from the declaration-before-use
29.17 -restriction, the order of items in a theory file is unconstrained.) Function
29.18 +In contrast to many functional programming languages,
29.19 +Isabelle insists on explicit declarations of all functions
29.20 +(keyword \isacommand{consts}). Apart from the declaration-before-use
29.21 +restriction, the order of items in a theory file is unconstrained. Function
29.22 \isa{app} is annotated with concrete syntax too. Instead of the
29.23 prefix syntax \isa{app\ xs\ ys} the infix
29.24 \isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
29.25 @@ -87,11 +89,11 @@
29.26 \end{warn}
29.27
29.28 A remark about syntax. The textual definition of a theory follows a fixed
29.29 -syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
29.30 -Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
29.31 +syntax with keywords like \isacommand{datatype} and \isacommand{end}.
29.32 +% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
29.33 Embedded in this syntax are the types and formulae of HOL, whose syntax is
29.34 -extensible, e.g.\ by new user-defined infix operators
29.35 -(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
29.36 +extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
29.37 +To distinguish the two levels, everything
29.38 HOL-specific (terms and types) should be enclosed in
29.39 \texttt{"}\dots\texttt{"}.
29.40 To lessen this burden, quotation marks around a single identifier can be
29.41 @@ -174,9 +176,10 @@
29.42 By default, induction acts on the first subgoal. The new proof state contains
29.43 two subgoals, namely the base case (\isa{Nil}) and the induction step
29.44 (\isa{Cons}):
29.45 -\begin{isabelle}
29.46 -~1.~rev~(rev~[])~=~[]\isanewline
29.47 -~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
29.48 +\begin{isabelle}%
29.49 +\ {\isadigit{1}}{\isachardot}\ rev\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
29.50 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
29.51 +\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
29.52 \end{isabelle}
29.53
29.54 The induction step is an example of the general format of a subgoal:
29.55 @@ -204,8 +207,9 @@
29.56 ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
29.57 to the equation \isa{rev\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}) and disappears; the simplified version
29.58 of subgoal~2 becomes the new subgoal~1:
29.59 -\begin{isabelle}
29.60 -~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
29.61 +\begin{isabelle}%
29.62 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
29.63 +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
29.64 \end{isabelle}
29.65 In order to simplify this subgoal further, a lemma suggests itself.%
29.66 \end{isamarkuptxt}%
29.67 @@ -221,10 +225,10 @@
29.68 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}%
29.69 \begin{isamarkuptxt}%
29.70 \noindent The keywords \isacommand{theorem}\index{*theorem} and
29.71 -\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
29.72 -the importance we attach to a proposition. We use the words
29.73 +\isacommand{lemma}\indexbold{*lemma} are interchangeable and merely indicate
29.74 +the importance we attach to a proposition. Therefore we use the words
29.75 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
29.76 -interchangeably.
29.77 +interchangeably, too.
29.78
29.79 There are two variables that we could induct on: \isa{xs} and
29.80 \isa{ys}. Because \isa{{\isacharat}} is defined by recursion on
29.81 @@ -272,8 +276,8 @@
29.82
29.83 % Instead of \isacommand{apply} followed by a dot, you can simply write
29.84 % \isacommand{by}\indexbold{by}, which we do most of the time.
29.85 -Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}}
29.86 -(as printed out after the final \isacommand{done}) the free variable \isa{xs} has been
29.87 +Notice that in lemma \isa{app{\isacharunderscore}Nil{\isadigit{2}}},
29.88 +as printed out after the final \isacommand{done}, the free variable \isa{xs} has been
29.89 replaced by the unknown \isa{{\isacharquery}xs}, just as explained in
29.90 \S\ref{sec:variables}.
29.91
29.92 @@ -313,7 +317,7 @@
29.93 \begin{isamarkuptext}%
29.94 \noindent
29.95 succeeds without further ado.
29.96 -Now we can go back and prove the first lemma%
29.97 +Now we can prove the first lemma%
29.98 \end{isamarkuptext}%
29.99 \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
29.100 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
30.1 --- a/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 11:59:15 2001 +0100
30.2 +++ b/doc-src/TutorialI/Trie/Trie.thy Wed Jan 24 12:29:10 2001 +0100
30.3 @@ -130,7 +130,7 @@
30.4 This proof may look surprisingly straightforward. However, note that this
30.5 comes at a cost: the proof script is unreadable because the intermediate
30.6 proof states are invisible, and we rely on the (possibly brittle) magic of
30.7 -@{text auto} (@{text simp_all} will not do---try it) to split the subgoals
30.8 +@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
30.9 of the induction up in such a way that case distinction on @{term bs} makes
30.10 sense and solves the proof. Part~\ref{Isar} shows you how to write readable
30.11 and stable proofs.
31.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex Wed Jan 24 11:59:15 2001 +0100
31.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Jan 24 12:29:10 2001 +0100
31.3 @@ -120,7 +120,7 @@
31.4 This proof may look surprisingly straightforward. However, note that this
31.5 comes at a cost: the proof script is unreadable because the intermediate
31.6 proof states are invisible, and we rely on the (possibly brittle) magic of
31.7 -\isa{auto} (\isa{simp{\isacharunderscore}all} will not do---try it) to split the subgoals
31.8 +\isa{auto} (\isa{simp{\isacharunderscore}all} will not do --- try it) to split the subgoals
31.9 of the induction up in such a way that case distinction on \isa{bs} makes
31.10 sense and solves the proof. Part~\ref{Isar} shows you how to write readable
31.11 and stable proofs.%
32.1 --- a/doc-src/TutorialI/Types/Overloading2.thy Wed Jan 24 11:59:15 2001 +0100
32.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy Wed Jan 24 12:29:10 2001 +0100
32.3 @@ -23,7 +23,7 @@
32.4 text{*
32.5 HOL comes with a number of overloaded constants and corresponding classes.
32.6 The most important ones are listed in Table~\ref{tab:overloading}. They are
32.7 -defined on all numeric types and somtimes on other types as well, for example
32.8 +defined on all numeric types and sometimes on other types as well, for example
32.9 @{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
32.10
32.11 \begin{table}[htbp]
32.12 @@ -34,9 +34,13 @@
32.13 @{term 0} & @{text "'a::zero"} \\
32.14 @{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
32.15 @{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
32.16 +@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
32.17 @{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
32.18 +@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
32.19 +@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
32.20 +@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
32.21 +@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
32.22 @{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
32.23 -@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
32.24 @{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
32.25 @{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
32.26 @{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
33.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jan 24 11:59:15 2001 +0100
33.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jan 24 12:29:10 2001 +0100
33.3 @@ -25,7 +25,7 @@
33.4 \begin{isamarkuptext}%
33.5 HOL comes with a number of overloaded constants and corresponding classes.
33.6 The most important ones are listed in Table~\ref{tab:overloading}. They are
33.7 -defined on all numeric types and somtimes on other types as well, for example
33.8 +defined on all numeric types and sometimes on other types as well, for example
33.9 \isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
33.10
33.11 \begin{table}[htbp]
33.12 @@ -36,9 +36,13 @@
33.13 \isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
33.14 \isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
33.15 \isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
33.16 +\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
33.17 \isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
33.18 +\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
33.19 +\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
33.20 +\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
33.21 +\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
33.22 \isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
33.23 -\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
33.24 \isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
33.25 \isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
33.26 \isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
34.1 --- a/doc-src/TutorialI/basics.tex Wed Jan 24 11:59:15 2001 +0100
34.2 +++ b/doc-src/TutorialI/basics.tex Wed Jan 24 12:29:10 2001 +0100
34.3 @@ -2,7 +2,7 @@
34.4
34.5 \section{Introduction}
34.6
34.7 -This is a tutorial on how to use Isabelle/HOL as a specification and
34.8 +This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and
34.9 verification system. Isabelle is a generic system for implementing logical
34.10 formalisms, and Isabelle/HOL is the specialization of Isabelle for
34.11 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
34.12 @@ -15,13 +15,12 @@
34.13 misled: HOL can express most mathematical concepts, and functional
34.14 programming is just one particularly simple and ubiquitous instance.
34.15
34.16 -This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
34.17 -which is an extension of Isabelle~\cite{paulson-isa-book} with structured
34.18 -proofs.\footnote{Thus the full name of the system should be
34.19 - Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
34.20 -difference to classical Isabelle (which is the basis of another version of
34.21 -this tutorial) is the replacement of the ML level by a dedicated language for
34.22 -definitions and proofs.
34.23 +Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
34.24 +This has influenced some of HOL's concrete syntax but is otherwise
34.25 +irrelevant for us because this tutorial is based on
34.26 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle
34.27 +with structured proofs.\footnote{Thus the full name of the system should be
34.28 + Isabelle/Isar/HOL, but that is a bit of a mouthful.}
34.29
34.30 A tutorial is by definition incomplete. Currently the tutorial only
34.31 introduces the rudiments of Isar's proof language. To fully exploit the power
34.32 @@ -74,7 +73,7 @@
34.33 HOL contains a theory \isaindexbold{Main}, the union of all the basic
34.34 predefined theories like arithmetic, lists, sets, etc.
34.35 Unless you know what you are doing, always include \isa{Main}
34.36 - as a direct or indirect parent theory of all your theories.
34.37 + as a direct or indirect parent of all your theories.
34.38 \end{warn}
34.39
34.40
34.41 @@ -122,7 +121,8 @@
34.42 \end{ttbox}
34.43
34.44 \noindent
34.45 -This can be reversed by \texttt{ML "reset show_types"}. Various other flags
34.46 +This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
34.47 +which we introduce as we go along,
34.48 can be set and reset in the same manner.\indexbold{flag!(re)setting}
34.49 \end{warn}
34.50
34.51 @@ -196,7 +196,7 @@
34.52 should be familiar with to avoid certain syntactic traps. A particular
34.53 problem for novices can be the priority of operators. If you are unsure, use
34.54 additional parentheses. In those cases where Isabelle echoes your
34.55 -input, you can see which parentheses are dropped---they were superfluous. If
34.56 +input, you can see which parentheses are dropped --- they were superfluous. If
34.57 you are unsure how to interpret Isabelle's output because you don't know
34.58 where the (dropped) parentheses go, set the \rmindex{flag}
34.59 \isaindexbold{show_brackets}:
34.60 @@ -222,7 +222,7 @@
34.61 \item
34.62 Constructs with an opening but without a closing delimiter bind very weakly
34.63 and should therefore be enclosed in parentheses if they appear in subterms, as
34.64 -in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
34.65 +in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
34.66 \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
34.67 \item
34.68 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
35.1 --- a/doc-src/TutorialI/fp.tex Wed Jan 24 11:59:15 2001 +0100
35.2 +++ b/doc-src/TutorialI/fp.tex Wed Jan 24 12:29:10 2001 +0100
35.3 @@ -122,11 +122,11 @@
35.4 the files have not been modified).
35.5
35.6 If you suddenly discover that you need to modify a parent theory of your
35.7 - current theory you must first abandon your current theory\indexbold{abandon
35.8 + current theory, you must first abandon your current theory\indexbold{abandon
35.9 theory}\indexbold{theory!abandon} (at the shell
35.10 level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
35.11 - been modified you go back to your original theory. When its first line
35.12 - \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the
35.13 + been modified, you go back to your original theory. When its first line
35.14 + \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
35.15 modified parent is reloaded automatically.
35.16
35.17 The only time when you need to load a theory by hand is when you simply
35.18 @@ -291,12 +291,12 @@
35.19 \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
35.20 that it did not need to so far. However, when you go beyond toy examples, you
35.21 need to understand the ingredients of \isa{auto}. This section covers the
35.22 -method that \isa{auto} always applies first, namely simplification.
35.23 +method that \isa{auto} always applies first, simplification.
35.24
35.25 Simplification is one of the central theorem proving tools in Isabelle and
35.26 many other systems. The tool itself is called the \bfindex{simplifier}. The
35.27 purpose of this section is introduce the many features of the simplifier.
35.28 -Anybody intending to use HOL should read this section. Later on
35.29 +Anybody intending to perform proofs in HOL should read this section. Later on
35.30 ({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
35.31 little bit of how the simplifier works. The serious student should read that
35.32 section as well, in particular in order to understand what happened if things
35.33 @@ -359,7 +359,7 @@
35.34 This declaration is a real can of worms.
35.35 In HOL it must be ruled out because it requires a type
35.36 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
35.37 -same cardinality---an impossibility. For the same reason it is not possible
35.38 +same cardinality --- an impossibility. For the same reason it is not possible
35.39 to allow recursion involving the type \isa{set}, which is isomorphic to
35.40 \isa{t \isasymFun\ bool}.
35.41
35.42 @@ -380,7 +380,7 @@
35.43 \end{isabelle}
35.44 do indeed make sense. Note the different arrow,
35.45 \isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
35.46 -expressing the type of \textbf{continuous} functions.
35.47 +expressing the type of \emph{continuous} functions.
35.48 There is even a version of LCF on top of HOL,
35.49 called HOLCF~\cite{MuellerNvOS99}.
35.50
36.1 --- a/doc-src/TutorialI/todo.tobias Wed Jan 24 11:59:15 2001 +0100
36.2 +++ b/doc-src/TutorialI/todo.tobias Wed Jan 24 12:29:10 2001 +0100
36.3 @@ -89,10 +89,10 @@
36.4 ==================
36.5
36.6 Exercises
36.7 -%\begin{exercise}
36.8 -%Extend expressions by conditional expressions.
36.9 -braucht wfrec!
36.10 -%\end{exercise}
36.11 +
36.12 +For extensionality (in Sets chapter): prove
36.13 +valif o norm = valif
36.14 +in If-expression case study (Ifexpr)
36.15
36.16 Nested inductive datatypes: another example/exercise:
36.17 size(t) <= size(subst s t)?
37.1 --- a/doc-src/TutorialI/tutorial.tex Wed Jan 24 11:59:15 2001 +0100
37.2 +++ b/doc-src/TutorialI/tutorial.tex Wed Jan 24 12:29:10 2001 +0100
37.3 @@ -75,9 +75,9 @@
37.4
37.5 \subsubsection*{Acknowledgements}
37.6 This tutorial owes a lot to the constant discussions with and the valuable
37.7 -feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
37.8 +feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
37.9 Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
37.10 -and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
37.11 +and Markus Wenzel. Stephan Merz was also kind enough to
37.12 read and comment on a draft version.
37.13 \clearfirst
37.14
37.15 @@ -91,7 +91,7 @@
37.16 \chapter{Theory Presentation}
37.17 \chapter{Case Study: Verifying a Cryptographic Protocol}
37.18 \chapter{Structured Proofs}
37.19 -\chapter{Case Study: UNIX File-System Security}
37.20 +%\chapter{Case Study: UNIX File-System Security}
37.21 %\chapter{The Tricks of the Trade}
37.22 \input{appendix}
37.23