1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Tue Nov 07 18:38:24 2000 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Nov 08 14:38:04 2000 +0100
1.3 @@ -1,5 +1,4 @@
1.4 \chapter{Advanced Simplification, Recursion and Induction}
1.5 -\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...}
1.6
1.7 Although we have already learned a lot about simplification, recursion and
1.8 induction, there are some advanced proof techniques that we have not covered
2.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy Tue Nov 07 18:38:24 2000 +0100
2.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Wed Nov 08 14:38:04 2000 +0100
2.3 @@ -1,17 +1,17 @@
2.4 (*<*)
2.5 theory Fundata = Main:
2.6 (*>*)
2.7 -datatype ('a,'i)bigtree = Tip | Branch 'a "'i \<Rightarrow> ('a,'i)bigtree"
2.8 +datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
2.9
2.10 text{*\noindent
2.11 Parameter @{typ"'a"} is the type of values stored in
2.12 -the @{term"Branch"}es of the tree, whereas @{typ"'i"} is the index
2.13 +the @{term Br}anches of the tree, whereas @{typ"'i"} is the index
2.14 type over which the tree branches. If @{typ"'i"} is instantiated to
2.15 @{typ"bool"}, the result is a binary tree; if it is instantiated to
2.16 @{typ"nat"}, we have an infinitely branching tree because each node
2.17 has as many subtrees as there are natural numbers. How can we possibly
2.18 write down such a tree? Using functional notation! For example, the term
2.19 -@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
2.20 +@{term[display]"Br 0 (%i. Br i (%n. Tip))"}
2.21 of type @{typ"(nat,nat)bigtree"} is the tree whose
2.22 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
2.23 has merely @{term"Tip"}s as further subtrees.
2.24 @@ -21,8 +21,8 @@
2.25
2.26 consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
2.27 primrec
2.28 -"map_bt f Tip = Tip"
2.29 -"map_bt f (Branch a F) = Branch (f a) (\<lambda>i. map_bt f (F i))"
2.30 +"map_bt f Tip = Tip"
2.31 +"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
2.32
2.33 text{*\noindent This is a valid \isacommand{primrec} definition because the
2.34 recursive calls of @{term"map_bt"} involve only subtrees obtained from
2.35 @@ -37,19 +37,14 @@
2.36 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
2.37 apply(induct_tac T, simp_all)
2.38 done
2.39 -
2.40 -text{*\noindent
2.41 -%apply(induct_tac T);
2.42 -%pr(latex xsymbols symbols)
2.43 +(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
2.44 +apply(induct_tac T, rename_tac[2] F)(*>*)
2.45 +txt{*\noindent
2.46 but it is worth taking a look at the proof state after the induction step
2.47 to understand what the presence of the function type entails:
2.48 -\begin{isabelle}
2.49 -\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
2.50 -\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
2.51 -\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
2.52 -\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
2.53 -\end{isabelle}
2.54 +@{subgoals[display,indent=0]}
2.55 *}
2.56 (*<*)
2.57 +oops
2.58 end
2.59 (*>*)
3.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Nov 07 18:38:24 2000 +0100
3.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Nov 08 14:38:04 2000 +0100
3.3 @@ -1,18 +1,18 @@
3.4 %
3.5 \begin{isabellebody}%
3.6 \def\isabellecontext{Fundata}%
3.7 -\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
3.8 +\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
3.9 \begin{isamarkuptext}%
3.10 \noindent
3.11 Parameter \isa{{\isacharprime}a} is the type of values stored in
3.12 -the \isa{Branch}es of the tree, whereas \isa{{\isacharprime}i} is the index
3.13 +the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index
3.14 type over which the tree branches. If \isa{{\isacharprime}i} is instantiated to
3.15 \isa{bool}, the result is a binary tree; if it is instantiated to
3.16 \isa{nat}, we have an infinitely branching tree because each node
3.17 has as many subtrees as there are natural numbers. How can we possibly
3.18 write down such a tree? Using functional notation! For example, the term
3.19 \begin{isabelle}%
3.20 -\ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
3.21 +\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
3.22 \end{isabelle}
3.23 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
3.24 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
3.25 @@ -22,8 +22,8 @@
3.26 \end{isamarkuptext}%
3.27 \isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isanewline
3.28 \isacommand{primrec}\isanewline
3.29 -{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
3.30 -{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
3.31 +{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
3.32 +{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ Br\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
3.33 \begin{isamarkuptext}%
3.34 \noindent This is a valid \isacommand{primrec} definition because the
3.35 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from
3.36 @@ -38,19 +38,16 @@
3.37 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
3.38 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
3.39 \isacommand{done}%
3.40 -\begin{isamarkuptext}%
3.41 +\begin{isamarkuptxt}%
3.42 \noindent
3.43 -%apply(induct_tac T);
3.44 -%pr(latex xsymbols symbols)
3.45 but it is worth taking a look at the proof state after the induction step
3.46 to understand what the presence of the function type entails:
3.47 -\begin{isabelle}
3.48 -\ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
3.49 -\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
3.50 -\ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.51 -\ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
3.52 +\begin{isabelle}%
3.53 +\ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
3.54 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
3.55 +\ \ \ \ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}%
3.56 \end{isabelle}%
3.57 -\end{isamarkuptext}%
3.58 +\end{isamarkuptxt}%
3.59 \end{isabellebody}%
3.60 %%% Local Variables:
3.61 %%% mode: latex
4.1 --- a/doc-src/TutorialI/Inductive/AB.thy Tue Nov 07 18:38:24 2000 +0100
4.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Wed Nov 08 14:38:04 2000 +0100
4.3 @@ -105,7 +105,7 @@
4.4 @{thm[display]nat0_intermed_int_val[no_vars]}
4.5 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
4.6 @{term abs} is the absolute value function, and @{term"#1::int"} is the
4.7 -integer 1 (see \S\ref{sec:int}).
4.8 +integer 1 (see \S\ref{sec:numbers}).
4.9
4.10 First we show that the our specific function, the difference between the
4.11 numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every
4.12 @@ -120,7 +120,7 @@
4.13 int(size[x\<in>take (i+1) w. \<not>P x]))
4.14 -
4.15 (int(size[x\<in>take i w. P x]) -
4.16 - int(size[x\<in>take i w. \<not>P x]))) <= #1";
4.17 + int(size[x\<in>take i w. \<not>P x]))) \<le> #1";
4.18
4.19 txt{*\noindent
4.20 The lemma is a bit hard to read because of the coercion function
5.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Nov 07 18:38:24 2000 +0100
5.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 08 14:38:04 2000 +0100
5.3 @@ -101,7 +101,7 @@
5.4 \end{isabelle}
5.5 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
5.6 \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
5.7 -integer 1 (see \S\ref{sec:int}).
5.8 +integer 1 (see \S\ref{sec:numbers}).
5.9
5.10 First we show that the our specific function, the difference between the
5.11 numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every
5.12 @@ -115,7 +115,7 @@
5.13 \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
5.14 \ \ \ \ \ \ {\isacharminus}\isanewline
5.15 \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
5.16 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
5.17 +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
5.18 \begin{isamarkuptxt}%
5.19 \noindent
5.20 The lemma is a bit hard to read because of the coercion function
6.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Nov 07 18:38:24 2000 +0100
6.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Nov 08 14:38:04 2000 +0100
6.3 @@ -51,23 +51,20 @@
6.4 (*<*)oops;(*>*)
6.5 lemma hd_rev: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
6.6 (*<*)
6.7 -by(induct_tac xs, auto);
6.8 +apply(induct_tac xs);
6.9 (*>*)
6.10
6.11 -text{*\noindent
6.12 +txt{*\noindent
6.13 This time, induction leaves us with the following base case
6.14 -\begin{isabelle}
6.15 -\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
6.16 -\end{isabelle}
6.17 +@{subgoals[display,indent=0,goals_limit=1]}
6.18 which is trivial, and @{text"auto"} finishes the whole proof.
6.19
6.20 -If @{thm[source]hd_rev} is meant to be a simplification rule, you are
6.21 +If @{text hd_rev} is meant to be a simplification rule, you are
6.22 done. But if you really need the @{text"\<Longrightarrow>"}-version of
6.23 -@{thm[source]hd_rev}, for example because you want to apply it as an
6.24 +@{text hd_rev}, for example because you want to apply it as an
6.25 introduction rule, you need to derive it separately, by combining it with
6.26 modus ponens:
6.27 -*};
6.28 -
6.29 +*}(*<*)by(auto);(*>*)
6.30 lemmas hd_revI = hd_rev[THEN mp];
6.31
6.32 text{*\noindent
7.1 --- a/doc-src/TutorialI/Misc/Itrev.thy Tue Nov 07 18:38:24 2000 +0100
7.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Nov 08 14:38:04 2000 +0100
7.3 @@ -61,9 +61,7 @@
7.4
7.5 txt{*\noindent
7.6 Unfortunately, this is not a complete success:
7.7 -\begin{isabelle}\makeatother
7.8 -~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
7.9 -\end{isabelle}
7.10 +@{subgoals[display,indent=0,margin=65]}
7.11 Just as predicted above, the overall goal, and hence the induction
7.12 hypothesis, is too weak to solve the induction step because of the fixed
7.13 @{term"[]"}. The corresponding heuristic:
8.1 --- a/doc-src/TutorialI/Misc/case_exprs.thy Tue Nov 07 18:38:24 2000 +0100
8.2 +++ b/doc-src/TutorialI/Misc/case_exprs.thy Wed Nov 08 14:38:04 2000 +0100
8.3 @@ -58,10 +58,7 @@
8.4
8.5 txt{*\noindent
8.6 results in the proof state
8.7 -\begin{isabelle}
8.8 -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
8.9 -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
8.10 -\end{isabelle}
8.11 +@{subgoals[display,indent=0,margin=65]}
8.12 which is solved automatically:
8.13 *}
8.14
9.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Nov 07 18:38:24 2000 +0100
9.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Nov 08 14:38:04 2000 +0100
9.3 @@ -53,11 +53,11 @@
9.4 This means we should prove%
9.5 \end{isamarkuptxt}%
9.6 \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
9.7 -\begin{isamarkuptext}%
9.8 +\begin{isamarkuptxt}%
9.9 \noindent
9.10 This time, induction leaves us with the following base case
9.11 -\begin{isabelle}
9.12 -\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
9.13 +\begin{isabelle}%
9.14 +\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
9.15 \end{isabelle}
9.16 which is trivial, and \isa{auto} finishes the whole proof.
9.17
9.18 @@ -66,7 +66,7 @@
9.19 \isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an
9.20 introduction rule, you need to derive it separately, by combining it with
9.21 modus ponens:%
9.22 -\end{isamarkuptext}%
9.23 +\end{isamarkuptxt}%
9.24 \isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}%
9.25 \begin{isamarkuptext}%
9.26 \noindent
10.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Nov 07 18:38:24 2000 +0100
10.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Nov 08 14:38:04 2000 +0100
10.3 @@ -60,8 +60,9 @@
10.4 \begin{isamarkuptxt}%
10.5 \noindent
10.6 Unfortunately, this is not a complete success:
10.7 -\begin{isabelle}\makeatother
10.8 -~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
10.9 +\begin{isabelle}%
10.10 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
10.11 +\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
10.12 \end{isabelle}
10.13 Just as predicted above, the overall goal, and hence the induction
10.14 hypothesis, is too weak to solve the induction step because of the fixed
11.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Nov 07 18:38:24 2000 +0100
11.2 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Nov 08 14:38:04 2000 +0100
11.3 @@ -67,9 +67,10 @@
11.4 \begin{isamarkuptxt}%
11.5 \noindent
11.6 results in the proof state
11.7 -\begin{isabelle}
11.8 -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
11.9 -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
11.10 +\begin{isabelle}%
11.11 +\ {\isadigit{1}}{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs\isanewline
11.12 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
11.13 +\ \ \ \ \ \ \ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs%
11.14 \end{isabelle}
11.15 which is solved automatically:%
11.16 \end{isamarkuptxt}%
12.1 --- a/doc-src/TutorialI/Types/Axioms.thy Tue Nov 07 18:38:24 2000 +0100
12.2 +++ b/doc-src/TutorialI/Types/Axioms.thy Wed Nov 08 14:38:04 2000 +0100
12.3 @@ -29,6 +29,12 @@
12.4 @{text parord}. For example, this is what @{thm[source]refl} really looks like:
12.5 @{thm[show_types]refl}.
12.6
12.7 +We have not made @{thm[source]less_le} a global definition because it would
12.8 +fix once and for all that @{text"<<"} is defined in terms of @{text"<<="}.
12.9 +There are however situations where it is the other way around, which such a
12.10 +definition would complicate. The slight drawback of the above class is that
12.11 +we need to define both @{text"<<="} and @{text"<<"} for each instance.
12.12 +
12.13 We can now prove simple theorems in this abstract setting, for example
12.14 that @{text"<<"} is not symmetric:
12.15 *}
13.1 --- a/doc-src/TutorialI/Types/Typedef.thy Tue Nov 07 18:38:24 2000 +0100
13.2 +++ b/doc-src/TutorialI/Types/Typedef.thy Wed Nov 08 14:38:04 2000 +0100
13.3 @@ -11,7 +11,7 @@
13.4 then read on.
13.5 \begin{warn}
13.6 Types in HOL must be non-empty; otherwise the quantifier rules would be
13.7 - unsound, because $\exists x. x=x$ is a theorem.
13.8 + unsound, because $\exists x.\ x=x$ is a theorem.
13.9 \end{warn}
13.10 *}
13.11
13.12 @@ -24,8 +24,8 @@
13.13 typedecl my_new_type
13.14
13.15 text{*\noindent\indexbold{*typedecl}%
13.16 -This does not define the type at all but merely introduces its name, @{typ
13.17 -my_new_type}. Thus we know nothing about this type, except that it is
13.18 +This does not define @{typ my_new_type} at all but merely introduces its
13.19 +name. Thus we know nothing about this type, except that it is
13.20 non-empty. Such declarations without definitions are
13.21 useful only if that type can be viewed as a parameter of a theory and we do
13.22 not intend to impose any restrictions on it. A typical example is given in
13.23 @@ -43,7 +43,7 @@
13.24 *}
13.25
13.26 axioms
13.27 -just_one: "\<exists>! x::my_new_type. True"
13.28 +just_one: "\<exists>x::my_new_type. \<forall>y. x = y"
13.29
13.30 text{*\noindent
13.31 However, we strongly discourage this approach, except at explorative stages
14.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex Tue Nov 07 18:38:24 2000 +0100
14.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Nov 08 14:38:04 2000 +0100
14.3 @@ -32,6 +32,12 @@
14.4 \isa{parord}. For example, this is what \isa{refl} really looks like:
14.5 \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
14.6
14.7 +We have not made \isa{less{\isacharunderscore}le} a global definition because it would
14.8 +fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}.
14.9 +There are however situations where it is the other way around, which such a
14.10 +definition would complicate. The slight drawback of the above class is that
14.11 +we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
14.12 +
14.13 We can now prove simple theorems in this abstract setting, for example
14.14 that \isa{{\isacharless}{\isacharless}} is not symmetric:%
14.15 \end{isamarkuptext}%
15.1 --- a/doc-src/TutorialI/Types/document/Typedef.tex Tue Nov 07 18:38:24 2000 +0100
15.2 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Wed Nov 08 14:38:04 2000 +0100
15.3 @@ -15,7 +15,7 @@
15.4 then read on.
15.5 \begin{warn}
15.6 Types in HOL must be non-empty; otherwise the quantifier rules would be
15.7 - unsound, because $\exists x. x=x$ is a theorem.
15.8 + unsound, because $\exists x.\ x=x$ is a theorem.
15.9 \end{warn}%
15.10 \end{isamarkuptext}%
15.11 %
15.12 @@ -30,7 +30,8 @@
15.13 \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type%
15.14 \begin{isamarkuptext}%
15.15 \noindent\indexbold{*typedecl}%
15.16 -This does not define the type at all but merely introduces its name, \isa{my{\isacharunderscore}new{\isacharunderscore}type}. Thus we know nothing about this type, except that it is
15.17 +This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its
15.18 +name. Thus we know nothing about this type, except that it is
15.19 non-empty. Such declarations without definitions are
15.20 useful only if that type can be viewed as a parameter of a theory and we do
15.21 not intend to impose any restrictions on it. A typical example is given in
15.22 @@ -47,7 +48,7 @@
15.23 axioms. Example:%
15.24 \end{isamarkuptext}%
15.25 \isacommand{axioms}\isanewline
15.26 -just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}{\isacharbang}\ x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ True{\isachardoublequote}%
15.27 +just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}%
15.28 \begin{isamarkuptext}%
15.29 \noindent
15.30 However, we strongly discourage this approach, except at explorative stages
16.1 --- a/doc-src/TutorialI/Types/types.tex Tue Nov 07 18:38:24 2000 +0100
16.2 +++ b/doc-src/TutorialI/Types/types.tex Wed Nov 08 14:38:04 2000 +0100
16.3 @@ -22,6 +22,7 @@
16.4 \subsection{Pairs}
16.5 \label{sec:products}
16.6 % Check refs to this section to see what is expected of it.
16.7 +% Mention type unit
16.8
16.9 \subsection{Records}
16.10 \label{sec:records}