1.1 --- a/doc-src/TutorialI/CTL/Base.thy Mon Oct 30 18:28:00 2000 +0100
1.2 +++ b/doc-src/TutorialI/CTL/Base.thy Tue Oct 31 08:53:12 2000 +0100
1.3 @@ -2,7 +2,7 @@
1.4
1.5 section{*Case study: Verified model checking*}
1.6
1.7 -text{*
1.8 +text{*\label{sec:VMC}
1.9 Model checking is a very popular technique for the verification of finite
1.10 state systems (implementations) w.r.t.\ temporal logic formulae
1.11 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
2.1 --- a/doc-src/TutorialI/CTL/document/Base.tex Mon Oct 30 18:28:00 2000 +0100
2.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex Tue Oct 31 08:53:12 2000 +0100
2.3 @@ -5,6 +5,7 @@
2.4 \isamarkupsection{Case study: Verified model checking}
2.5 %
2.6 \begin{isamarkuptext}%
2.7 +\label{sec:VMC}
2.8 Model checking is a very popular technique for the verification of finite
2.9 state systems (implementations) w.r.t.\ temporal logic formulae
2.10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
3.1 --- a/doc-src/TutorialI/IsaMakefile Mon Oct 30 18:28:00 2000 +0100
3.2 +++ b/doc-src/TutorialI/IsaMakefile Tue Oct 31 08:53:12 2000 +0100
3.3 @@ -142,7 +142,7 @@
3.4
3.5 HOL-Types: HOL $(LOG)/HOL-Types.gz
3.6
3.7 -$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
3.8 +$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML Types/Typedef.thy \
3.9 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
3.10 Types/Overloading.thy Types/Axioms.thy
3.11 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Types
4.1 --- a/doc-src/TutorialI/Misc/Itrev.thy Mon Oct 30 18:28:00 2000 +0100
4.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Oct 31 08:53:12 2000 +0100
4.3 @@ -35,7 +35,7 @@
4.4 gradually, using only @{text"#"}:
4.5 *}
4.6
4.7 -consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
4.8 +consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
4.9 primrec
4.10 "itrev [] ys = ys"
4.11 "itrev (x#xs) ys = itrev xs (x#ys)";
4.12 @@ -75,7 +75,7 @@
4.13 *};
4.14 (*<*)oops;(*>*)
4.15 lemma "itrev xs ys = rev xs @ ys";
4.16 -
4.17 +(*<*)apply(induct_tac xs, simp_all)(*>*)
4.18 txt{*\noindent
4.19 If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
4.20 @{term"rev xs"}, just as required.
4.21 @@ -87,11 +87,7 @@
4.22 Although we now have two variables, only @{term"xs"} is suitable for
4.23 induction, and we repeat our above proof attempt. Unfortunately, we are still
4.24 not there:
4.25 -\begin{isabelle}\makeatother
4.26 -~1.~{\isasymAnd}a~list.\isanewline
4.27 -~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
4.28 -~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
4.29 -\end{isabelle}
4.30 +@{subgoals[display,indent=0,goals_limit=1]}
4.31 The induction hypothesis is still too weak, but this time it takes no
4.32 intuition to generalize: the problem is that @{term"ys"} is fixed throughout
4.33 the subgoal, but the induction hypothesis needs to be applied with
4.34 @@ -99,7 +95,7 @@
4.35 for all @{term"ys"} instead of a fixed one:
4.36 *};
4.37 (*<*)oops;(*>*)
4.38 -lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
4.39 +lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
4.40 (*<*)
4.41 by(induct_tac xs, simp_all);
4.42 (*>*)
5.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Oct 30 18:28:00 2000 +0100
5.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Oct 31 08:53:12 2000 +0100
5.3 @@ -84,10 +84,10 @@
5.4 Although we now have two variables, only \isa{xs} is suitable for
5.5 induction, and we repeat our above proof attempt. Unfortunately, we are still
5.6 not there:
5.7 -\begin{isabelle}\makeatother
5.8 -~1.~{\isasymAnd}a~list.\isanewline
5.9 -~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
5.10 -~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
5.11 +\begin{isabelle}%
5.12 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
5.13 +\ \ \ \ \ \ \ itrev\ list\ ys\ {\isacharequal}\ rev\ list\ {\isacharat}\ ys\ {\isasymLongrightarrow}\isanewline
5.14 +\ \ \ \ \ \ \ itrev\ list\ {\isacharparenleft}a\ {\isacharhash}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ ys%
5.15 \end{isabelle}
5.16 The induction hypothesis is still too weak, but this time it takes no
5.17 intuition to generalize: the problem is that \isa{ys} is fixed throughout
6.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Mon Oct 30 18:28:00 2000 +0100
6.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Oct 31 08:53:12 2000 +0100
6.3 @@ -151,8 +151,8 @@
6.4 \begin{isamarkuptxt}%
6.5 \noindent
6.6 In this particular case, the resulting goal
6.7 -\begin{isabelle}
6.8 -~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
6.9 +\begin{isabelle}%
6.10 +\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ {\isasymnot}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ A\ {\isasymand}\ {\isasymnot}\ A%
6.11 \end{isabelle}
6.12 can be proved by simplification. Thus we could have proved the lemma outright by%
6.13 \end{isamarkuptxt}%
6.14 @@ -227,15 +227,14 @@
6.15 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
6.16 \begin{isamarkuptxt}%
6.17 \noindent
6.18 -can be split into
6.19 -\begin{isabelle}
6.20 -~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
6.21 -\end{isabelle}
6.22 -by a degenerate form of simplification%
6.23 +can be split by a degenerate form of simplification%
6.24 \end{isamarkuptxt}%
6.25 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
6.26 -\begin{isamarkuptext}%
6.27 +\begin{isamarkuptxt}%
6.28 \noindent
6.29 +\begin{isabelle}%
6.30 +\ {\isadigit{1}}{\isachardot}\ {\isasymforall}xs{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}%
6.31 +\end{isabelle}
6.32 where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
6.33 empty list of theorems) but the rule \isaindexbold{split_if} for
6.34 splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
6.35 @@ -244,25 +243,20 @@
6.36 on the initial goal above.
6.37
6.38 This splitting idea generalizes from \isa{if} to \isaindex{case}:%
6.39 -\end{isamarkuptext}%
6.40 -\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
6.41 +\end{isamarkuptxt}%
6.42 +\isanewline
6.43 +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
6.44 +\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
6.45 \begin{isamarkuptxt}%
6.46 -\noindent
6.47 -becomes
6.48 -\begin{isabelle}\makeatother
6.49 -~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
6.50 -~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
6.51 +\begin{isabelle}%
6.52 +\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
6.53 +\ \ \ \ {\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}%
6.54 \end{isabelle}
6.55 -by typing%
6.56 -\end{isamarkuptxt}%
6.57 -\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
6.58 -\begin{isamarkuptext}%
6.59 -\noindent
6.60 In contrast to \isa{if}-expressions, the simplifier does not split
6.61 \isa{case}-expressions by default because this can lead to nontermination
6.62 in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
6.63 dropped, the above goal is solved,%
6.64 -\end{isamarkuptext}%
6.65 +\end{isamarkuptxt}%
6.66 \isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
6.67 \begin{isamarkuptext}%
6.68 \noindent%
6.69 @@ -292,13 +286,13 @@
6.70 \end{isamarkuptext}%
6.71 \isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
6.72 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
6.73 -\begin{isamarkuptext}%
6.74 +\begin{isamarkuptxt}%
6.75 \noindent
6.76 In contrast to splitting the conclusion, this actually creates two
6.77 separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
6.78 -\begin{isabelle}
6.79 -\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
6.80 -\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
6.81 +\begin{isabelle}%
6.82 +\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
6.83 +\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
6.84 \end{isabelle}
6.85 If you need to split both in the assumptions and the conclusion,
6.86 use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
6.87 @@ -314,7 +308,7 @@
6.88 \end{warn}
6.89
6.90 \index{*split|)}%
6.91 -\end{isamarkuptext}%
6.92 +\end{isamarkuptxt}%
6.93 %
6.94 \isamarkupsubsubsection{Arithmetic}
6.95 %
7.1 --- a/doc-src/TutorialI/Misc/simp.thy Mon Oct 30 18:28:00 2000 +0100
7.2 +++ b/doc-src/TutorialI/Misc/simp.thy Tue Oct 31 08:53:12 2000 +0100
7.3 @@ -154,9 +154,7 @@
7.4
7.5 txt{*\noindent
7.6 In this particular case, the resulting goal
7.7 -\begin{isabelle}
7.8 -~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
7.9 -\end{isabelle}
7.10 +@{subgoals[display,indent=0]}
7.11 can be proved by simplification. Thus we could have proved the lemma outright by
7.12 *}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
7.13 apply(simp add: exor_def)
7.14 @@ -237,17 +235,13 @@
7.15 lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
7.16
7.17 txt{*\noindent
7.18 -can be split into
7.19 -\begin{isabelle}
7.20 -~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
7.21 -\end{isabelle}
7.22 -by a degenerate form of simplification
7.23 +can be split by a degenerate form of simplification
7.24 *}
7.25
7.26 apply(simp only: split: split_if);
7.27 -(*<*)oops;(*>*)
7.28
7.29 -text{*\noindent
7.30 +txt{*\noindent
7.31 +@{subgoals[display,indent=0]}
7.32 where no simplification rules are included (@{text"only:"} is followed by the
7.33 empty list of theorems) but the rule \isaindexbold{split_if} for
7.34 splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
7.35 @@ -256,28 +250,19 @@
7.36 on the initial goal above.
7.37
7.38 This splitting idea generalizes from @{text"if"} to \isaindex{case}:
7.39 -*}
7.40 +*}(*<*)oops;(*>*)
7.41
7.42 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
7.43 -txt{*\noindent
7.44 -becomes
7.45 -\begin{isabelle}\makeatother
7.46 -~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
7.47 -~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
7.48 -\end{isabelle}
7.49 -by typing
7.50 -*}
7.51 +apply(simp only: split: list.split);
7.52
7.53 -apply(simp only: split: list.split);
7.54 -(*<*)oops;(*>*)
7.55 -
7.56 -text{*\noindent
7.57 +txt{*
7.58 +@{subgoals[display,indent=0]}
7.59 In contrast to @{text"if"}-expressions, the simplifier does not split
7.60 @{text"case"}-expressions by default because this can lead to nontermination
7.61 in case of recursive datatypes. Again, if the @{text"only:"} modifier is
7.62 dropped, the above goal is solved,
7.63 *}
7.64 -(*<*)
7.65 +(*<*)oops;
7.66 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
7.67 (*>*)
7.68 apply(simp split: list.split);
7.69 @@ -317,17 +302,11 @@
7.70
7.71 lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
7.72 apply(simp only: split: split_if_asm);
7.73 -(*<*)
7.74 -by(simp_all)
7.75 -(*>*)
7.76
7.77 -text{*\noindent
7.78 +txt{*\noindent
7.79 In contrast to splitting the conclusion, this actually creates two
7.80 separate subgoals (which are solved by @{text"simp_all"}):
7.81 -\begin{isabelle}
7.82 -\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
7.83 -\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
7.84 -\end{isabelle}
7.85 +@{subgoals[display,indent=0]}
7.86 If you need to split both in the assumptions and the conclusion,
7.87 use $t$@{text".splits"} which subsumes $t$@{text".split"} and
7.88 $t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
7.89 @@ -343,6 +322,9 @@
7.90
7.91 \index{*split|)}
7.92 *}
7.93 +(*<*)
7.94 +by(simp_all)
7.95 +(*>*)
7.96
7.97
7.98 subsubsection{*Arithmetic*}
8.1 --- a/doc-src/TutorialI/Recdef/Induction.thy Mon Oct 30 18:28:00 2000 +0100
8.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Oct 31 08:53:12 2000 +0100
8.3 @@ -31,13 +31,7 @@
8.4 txt{*\noindent
8.5 The resulting proof state has three subgoals corresponding to the three
8.6 clauses for @{term"sep"}:
8.7 -\begin{isabelle}
8.8 -~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
8.9 -~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
8.10 -~3.~{\isasymAnd}a~x~y~zs.\isanewline
8.11 -~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
8.12 -~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
8.13 -\end{isabelle}
8.14 +@{subgoals[display,indent=0]}
8.15 The rest is pure simplification:
8.16 *}
8.17
9.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Oct 30 18:28:00 2000 +0100
9.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Oct 31 08:53:12 2000 +0100
9.3 @@ -29,12 +29,12 @@
9.4 \noindent
9.5 The resulting proof state has three subgoals corresponding to the three
9.6 clauses for \isa{sep}:
9.7 -\begin{isabelle}
9.8 -~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
9.9 -~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
9.10 -~3.~{\isasymAnd}a~x~y~zs.\isanewline
9.11 -~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
9.12 -~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
9.13 +\begin{isabelle}%
9.14 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
9.15 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
9.16 +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
9.17 +\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
9.18 +\ \ \ \ \ \ \ map\ f\ {\isacharparenleft}sep\ {\isacharparenleft}a{\isacharcomma}\ x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharcomma}\ map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
9.19 \end{isabelle}
9.20 The rest is pure simplification:%
9.21 \end{isamarkuptxt}%
10.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex Mon Oct 30 18:28:00 2000 +0100
10.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Oct 31 08:53:12 2000 +0100
10.3 @@ -64,7 +64,7 @@
10.4 \end{isamarkuptext}%
10.5 \isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
10.6 \isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
10.7 -\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
10.8 +\ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline
10.9 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
10.10 \begin{isamarkuptext}%
10.11 Because of its pattern-matching syntax, \isacommand{recdef} is also useful
11.1 --- a/doc-src/TutorialI/Recdef/examples.thy Mon Oct 30 18:28:00 2000 +0100
11.2 +++ b/doc-src/TutorialI/Recdef/examples.thy Tue Oct 31 08:53:12 2000 +0100
11.3 @@ -69,7 +69,7 @@
11.4 *}
11.5 consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
11.6 recdef sep2 "measure length"
11.7 - "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 zs a)"
11.8 + "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
11.9 "sep2 xs = (\<lambda>a. xs)";
11.10
11.11 text{*
12.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy Mon Oct 30 18:28:00 2000 +0100
12.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Oct 31 08:53:12 2000 +0100
12.3 @@ -248,13 +248,10 @@
12.4 apply(auto);
12.5
12.6 txt{*
12.7 -\begin{isabelle}
12.8 -~1.~rev~ys~=~rev~ys~@~[]\isanewline
12.9 -~2. \dots
12.10 -\end{isabelle}
12.11 -Again, we need to abandon this proof attempt and prove another simple lemma first.
12.12 -In the future the step of abandoning an incomplete proof before embarking on
12.13 -the proof of a lemma usually remains implicit.
12.14 +@{subgoals[display,indent=0,goals_limit=1]}
12.15 +Again, we need to abandon this proof attempt and prove another simple lemma
12.16 +first. In the future the step of abandoning an incomplete proof before
12.17 +embarking on the proof of a lemma usually remains implicit.
12.18 *}
12.19 (*<*)
12.20 oops
12.21 @@ -273,11 +270,7 @@
12.22 txt{*
12.23 \noindent
12.24 leads to the desired message @{text"No subgoals!"}:
12.25 -\begin{isabelle}
12.26 -xs~@~[]~=~xs\isanewline
12.27 -No~subgoals!
12.28 -\end{isabelle}
12.29 -
12.30 +@{goals[display,indent=0]}
12.31 We still need to confirm that the proof is now finished:
12.32 *}
12.33
12.34 @@ -306,11 +299,7 @@
12.35 \noindent
12.36 we find that this time @{text"auto"} solves the base case, but the
12.37 induction step merely simplifies to
12.38 -\begin{isabelle}
12.39 -~1.~{\isasymAnd}a~list.\isanewline
12.40 -~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
12.41 -~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
12.42 -\end{isabelle}
12.43 +@{subgoals[display,indent=0,goals_limit=1]}
12.44 Now we need to remember that @{text"@"} associates to the right, and that
12.45 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
12.46 in their \isacommand{infixr} annotation). Thus the conclusion really is
13.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Oct 30 18:28:00 2000 +0100
13.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Oct 31 08:53:12 2000 +0100
13.3 @@ -234,13 +234,12 @@
13.4 \end{isamarkuptxt}%
13.5 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
13.6 \begin{isamarkuptxt}%
13.7 -\begin{isabelle}
13.8 -~1.~rev~ys~=~rev~ys~@~[]\isanewline
13.9 -~2. \dots
13.10 +\begin{isabelle}%
13.11 +\ {\isadigit{1}}{\isachardot}\ rev\ ys\ {\isacharequal}\ rev\ ys\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}%
13.12 \end{isabelle}
13.13 -Again, we need to abandon this proof attempt and prove another simple lemma first.
13.14 -In the future the step of abandoning an incomplete proof before embarking on
13.15 -the proof of a lemma usually remains implicit.%
13.16 +Again, we need to abandon this proof attempt and prove another simple lemma
13.17 +first. In the future the step of abandoning an incomplete proof before
13.18 +embarking on the proof of a lemma usually remains implicit.%
13.19 \end{isamarkuptxt}%
13.20 %
13.21 \isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
13.22 @@ -254,11 +253,10 @@
13.23 \begin{isamarkuptxt}%
13.24 \noindent
13.25 leads to the desired message \isa{No\ subgoals{\isacharbang}}:
13.26 -\begin{isabelle}
13.27 -xs~@~[]~=~xs\isanewline
13.28 -No~subgoals!
13.29 +\begin{isabelle}%
13.30 +xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
13.31 +No\ subgoals{\isacharbang}%
13.32 \end{isabelle}
13.33 -
13.34 We still need to confirm that the proof is now finished:%
13.35 \end{isamarkuptxt}%
13.36 \isacommand{done}%
13.37 @@ -284,10 +282,10 @@
13.38 \noindent
13.39 we find that this time \isa{auto} solves the base case, but the
13.40 induction step merely simplifies to
13.41 -\begin{isabelle}
13.42 -~1.~{\isasymAnd}a~list.\isanewline
13.43 -~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
13.44 -~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
13.45 +\begin{isabelle}%
13.46 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
13.47 +\ \ \ \ \ \ \ rev\ {\isacharparenleft}list\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isasymLongrightarrow}\isanewline
13.48 +\ \ \ \ \ \ \ {\isacharparenleft}rev\ ys\ {\isacharat}\ rev\ list{\isacharparenright}\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ ys\ {\isacharat}\ rev\ list\ {\isacharat}\ a\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}%
13.49 \end{isabelle}
13.50 Now we need to remember that \isa{{\isacharat}} associates to the right, and that
13.51 \isa{{\isacharhash}} and \isa{{\isacharat}} have the same priority (namely the \isa{{\isadigit{6}}{\isadigit{5}}}
14.1 --- a/doc-src/TutorialI/Types/Axioms.thy Mon Oct 30 18:28:00 2000 +0100
14.2 +++ b/doc-src/TutorialI/Types/Axioms.thy Tue Oct 31 08:53:12 2000 +0100
14.3 @@ -59,7 +59,7 @@
14.4 txt{*\noindent
14.5 This time @{text intro_classes} leaves us with the four axioms,
14.6 specialized to type @{typ bool}, as subgoals:
14.7 -@{goals[display,show_types,indent=0]}
14.8 +@{subgoals[display,show_types,indent=0]}
14.9 Fortunately, the proof is easy for blast, once we have unfolded the definitions
14.10 of @{text"<<"} and @{text"<<="} at @{typ bool}:
14.11 *}
15.1 --- a/doc-src/TutorialI/Types/ROOT.ML Mon Oct 30 18:28:00 2000 +0100
15.2 +++ b/doc-src/TutorialI/Types/ROOT.ML Tue Oct 31 08:53:12 2000 +0100
15.3 @@ -1,4 +1,5 @@
15.4 use "../settings.ML";
15.5 +use_thy "Typedef";
15.6 use_thy "Overloading0";
15.7 use_thy "Overloading2";
15.8 use_thy "Axioms";
16.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Oct 30 18:28:00 2000 +0100
16.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Tue Oct 31 08:53:12 2000 +0100
16.3 @@ -59,7 +59,6 @@
16.4 This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
16.5 specialized to type \isa{bool}, as subgoals:
16.6 \begin{isabelle}%
16.7 -OFCLASS{\isacharparenleft}bool{\isacharcomma}\ parord{\isacharunderscore}class{\isacharparenright}\isanewline
16.8 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
16.9 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
16.10 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
17.1 --- a/doc-src/TutorialI/Types/types.tex Mon Oct 30 18:28:00 2000 +0100
17.2 +++ b/doc-src/TutorialI/Types/types.tex Tue Oct 31 08:53:12 2000 +0100
17.3 @@ -9,11 +9,13 @@
17.4 ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
17.5 about them.
17.6 \item Introducing your own types: how to introduce your own new types that
17.7 - cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
17.8 + cannot be constructed with any of the basic methods ({\S}\ref{sec:adv-typedef}).
17.9 \item Type classes: how to specify and reason about axiomatic collections of
17.10 types ({\S}\ref{sec:axclass}).
17.11 \end{itemize}
17.12
17.13 +\input{Types/document/Typedef}
17.14 +
17.15 \section{Axiomatic type classes}
17.16 \label{sec:axclass}
17.17 \index{axiomatic type class|(}
17.18 @@ -42,7 +44,7 @@
17.19
17.20 \index{overloading|)}
17.21
17.22 -\input{Types/document/Axioms0}
17.23 +\input{Types/document/Axioms}
17.24
17.25 \index{axiomatic type class|)}
17.26 \index{*axclass|)}