# HG changeset patch # User nipkow # Date 973690684 -3600 # Node ID ef006735bee8999d406336a162843cf150089199 # Parent 1bfdd19c1d473386189d3ad9b7dbad8c39adb138 *** empty log message *** diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Nov 08 14:38:04 2000 +0100 @@ -1,5 +1,4 @@ \chapter{Advanced Simplification, Recursion and Induction} -\markboth{}{CHAPTER 4: ADVANCED SIMPLIFICATION, RECURSION ...} Although we have already learned a lot about simplification, recursion and induction, there are some advanced proof techniques that we have not covered diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Datatype/Fundata.thy --- a/doc-src/TutorialI/Datatype/Fundata.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Wed Nov 08 14:38:04 2000 +0100 @@ -1,17 +1,17 @@ (*<*) theory Fundata = Main: (*>*) -datatype ('a,'i)bigtree = Tip | Branch 'a "'i \ ('a,'i)bigtree" +datatype ('a,'i)bigtree = Tip | Br 'a "'i \ ('a,'i)bigtree" text{*\noindent Parameter @{typ"'a"} is the type of values stored in -the @{term"Branch"}es of the tree, whereas @{typ"'i"} is the index +the @{term Br}anches of the tree, whereas @{typ"'i"} is the index type over which the tree branches. If @{typ"'i"} is instantiated to @{typ"bool"}, the result is a binary tree; if it is instantiated to @{typ"nat"}, we have an infinitely branching tree because each node has as many subtrees as there are natural numbers. How can we possibly write down such a tree? Using functional notation! For example, the term -@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"} +@{term[display]"Br 0 (%i. Br i (%n. Tip))"} of type @{typ"(nat,nat)bigtree"} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and has merely @{term"Tip"}s as further subtrees. @@ -21,8 +21,8 @@ consts map_bt :: "('a \ 'b) \ ('a,'i)bigtree \ ('b,'i)bigtree" primrec -"map_bt f Tip = Tip" -"map_bt f (Branch a F) = Branch (f a) (\i. map_bt f (F i))" +"map_bt f Tip = Tip" +"map_bt f (Br a F) = Br (f a) (\i. map_bt f (F i))" text{*\noindent This is a valid \isacommand{primrec} definition because the recursive calls of @{term"map_bt"} involve only subtrees obtained from @@ -37,19 +37,14 @@ lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac T, simp_all) done - -text{*\noindent -%apply(induct_tac T); -%pr(latex xsymbols symbols) +(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; +apply(induct_tac T, rename_tac[2] F)(*>*) +txt{*\noindent but it is worth taking a look at the proof state after the induction step to understand what the presence of the function type entails: -\begin{isabelle} -\ \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 -\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline -\ \ \ \ \ \ \ {\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 -\ \ \ \ \ \ \ 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} -\end{isabelle} +@{subgoals[display,indent=0]} *} (*<*) +oops end (*>*) diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Nov 08 14:38:04 2000 +0100 @@ -1,18 +1,18 @@ % \begin{isabellebody}% \def\isabellecontext{Fundata}% -\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}% +\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}% \begin{isamarkuptext}% \noindent Parameter \isa{{\isacharprime}a} is the type of values stored in -the \isa{Branch}es of the tree, whereas \isa{{\isacharprime}i} is the index +the \isa{Br}anches of the tree, whereas \isa{{\isacharprime}i} is the index type over which the tree branches. If \isa{{\isacharprime}i} is instantiated to \isa{bool}, the result is a binary tree; if it is instantiated to \isa{nat}, we have an infinitely branching tree because each node has as many subtrees as there are natural numbers. How can we possibly write down such a tree? Using functional notation! For example, the term \begin{isabelle}% -\ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% +\ \ \ \ \ Br\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Br\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% \end{isabelle} of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and @@ -22,8 +22,8 @@ \end{isamarkuptext}% \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 \isacommand{primrec}\isanewline -{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline -{\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}% +{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline +{\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}% \begin{isamarkuptext}% \noindent This is a valid \isacommand{primrec} definition because the recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from @@ -38,19 +38,16 @@ \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 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isacommand{done}% -\begin{isamarkuptext}% +\begin{isamarkuptxt}% \noindent -%apply(induct_tac T); -%pr(latex xsymbols symbols) but it is worth taking a look at the proof state after the induction step to understand what the presence of the function type entails: -\begin{isabelle} -\ \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 -\ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline -\ \ \ \ \ \ \ {\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 -\ \ \ \ \ \ \ 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} +\begin{isabelle}% +\ {\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 +\ {\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 +\ \ \ \ \ \ \ \ \ \ 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}% \end{isabelle}% -\end{isamarkuptext}% +\end{isamarkuptxt}% \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Inductive/AB.thy Wed Nov 08 14:38:04 2000 +0100 @@ -105,7 +105,7 @@ @{thm[display]nat0_intermed_int_val[no_vars]} where @{term f} is of type @{typ"nat \ int"}, @{typ int} are the integers, @{term abs} is the absolute value function, and @{term"#1::int"} is the -integer 1 (see \S\ref{sec:int}). +integer 1 (see \S\ref{sec:numbers}). First we show that the our specific function, the difference between the numbers of @{term a}'s and @{term b}'s, does indeed only change by 1 in every @@ -120,7 +120,7 @@ int(size[x\take (i+1) w. \P x])) - (int(size[x\take i w. P x]) - - int(size[x\take i w. \P x]))) <= #1"; + int(size[x\take i w. \P x]))) \ #1"; txt{*\noindent The lemma is a bit hard to read because of the coercion function diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Nov 08 14:38:04 2000 +0100 @@ -101,7 +101,7 @@ \end{isabelle} where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers, \isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the -integer 1 (see \S\ref{sec:int}). +integer 1 (see \S\ref{sec:numbers}). First we show that the our specific function, the difference between the numbers of \isa{a}'s and \isa{b}'s, does indeed only change by 1 in every @@ -115,7 +115,7 @@ \ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline \ \ \ \ \ \ {\isacharminus}\isanewline \ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}% +\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent The lemma is a bit hard to read because of the coercion function diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Nov 08 14:38:04 2000 +0100 @@ -51,23 +51,20 @@ (*<*)oops;(*>*) lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs"; (*<*) -by(induct_tac xs, auto); +apply(induct_tac xs); (*>*) -text{*\noindent +txt{*\noindent This time, induction leaves us with the following base case -\begin{isabelle} -\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] -\end{isabelle} +@{subgoals[display,indent=0,goals_limit=1]} which is trivial, and @{text"auto"} finishes the whole proof. -If @{thm[source]hd_rev} is meant to be a simplification rule, you are +If @{text hd_rev} is meant to be a simplification rule, you are done. But if you really need the @{text"\"}-version of -@{thm[source]hd_rev}, for example because you want to apply it as an +@{text hd_rev}, for example because you want to apply it as an introduction rule, you need to derive it separately, by combining it with modus ponens: -*}; - +*}(*<*)by(auto);(*>*) lemmas hd_revI = hd_rev[THEN mp]; text{*\noindent diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Nov 08 14:38:04 2000 +0100 @@ -61,9 +61,7 @@ txt{*\noindent Unfortunately, this is not a complete success: -\begin{isabelle}\makeatother -~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% -\end{isabelle} +@{subgoals[display,indent=0,margin=65]} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed @{term"[]"}. The corresponding heuristic: diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/case_exprs.thy --- a/doc-src/TutorialI/Misc/case_exprs.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/case_exprs.thy Wed Nov 08 14:38:04 2000 +0100 @@ -58,10 +58,7 @@ txt{*\noindent results in the proof state -\begin{isabelle} -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% -\end{isabelle} +@{subgoals[display,indent=0,margin=65]} which is solved automatically: *} diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Nov 08 14:38:04 2000 +0100 @@ -53,11 +53,11 @@ This means we should prove% \end{isamarkuptxt}% \isacommand{lemma}\ hd{\isacharunderscore}rev{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}% -\begin{isamarkuptext}% +\begin{isamarkuptxt}% \noindent This time, induction leaves us with the following base case -\begin{isabelle} -\ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}% \end{isabelle} which is trivial, and \isa{auto} finishes the whole proof. @@ -66,7 +66,7 @@ \isa{hd{\isacharunderscore}rev}, for example because you want to apply it as an introduction rule, you need to derive it separately, by combining it with modus ponens:% -\end{isamarkuptext}% +\end{isamarkuptxt}% \isacommand{lemmas}\ hd{\isacharunderscore}revI\ {\isacharequal}\ hd{\isacharunderscore}rev{\isacharbrackleft}THEN\ mp{\isacharbrackright}% \begin{isamarkuptext}% \noindent diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Nov 08 14:38:04 2000 +0100 @@ -60,8 +60,9 @@ \begin{isamarkuptxt}% \noindent Unfortunately, this is not a complete success: -\begin{isabelle}\makeatother -~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\ \ \ \ \ \ \ itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}% \end{isabelle} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Misc/document/case_exprs.tex --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Nov 08 14:38:04 2000 +0100 @@ -67,9 +67,10 @@ \begin{isamarkuptxt}% \noindent results in the proof state -\begin{isabelle} -~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline -~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% +\begin{isabelle}% +\ {\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 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline +\ \ \ \ \ \ \ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymLongrightarrow}\ {\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs% \end{isabelle} which is solved automatically:% \end{isamarkuptxt}% diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Types/Axioms.thy --- a/doc-src/TutorialI/Types/Axioms.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Types/Axioms.thy Wed Nov 08 14:38:04 2000 +0100 @@ -29,6 +29,12 @@ @{text parord}. For example, this is what @{thm[source]refl} really looks like: @{thm[show_types]refl}. +We have not made @{thm[source]less_le} a global definition because it would +fix once and for all that @{text"<<"} is defined in terms of @{text"<<="}. +There are however situations where it is the other way around, which such a +definition would complicate. The slight drawback of the above class is that +we need to define both @{text"<<="} and @{text"<<"} for each instance. + We can now prove simple theorems in this abstract setting, for example that @{text"<<"} is not symmetric: *} diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Types/Typedef.thy --- a/doc-src/TutorialI/Types/Typedef.thy Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Types/Typedef.thy Wed Nov 08 14:38:04 2000 +0100 @@ -11,7 +11,7 @@ then read on. \begin{warn} Types in HOL must be non-empty; otherwise the quantifier rules would be - unsound, because $\exists x. x=x$ is a theorem. + unsound, because $\exists x.\ x=x$ is a theorem. \end{warn} *} @@ -24,8 +24,8 @@ typedecl my_new_type text{*\noindent\indexbold{*typedecl}% -This does not define the type at all but merely introduces its name, @{typ -my_new_type}. Thus we know nothing about this type, except that it is +This does not define @{typ my_new_type} at all but merely introduces its +name. Thus we know nothing about this type, except that it is non-empty. Such declarations without definitions are useful only if that type can be viewed as a parameter of a theory and we do not intend to impose any restrictions on it. A typical example is given in @@ -43,7 +43,7 @@ *} axioms -just_one: "\! x::my_new_type. True" +just_one: "\x::my_new_type. \y. x = y" text{*\noindent However, we strongly discourage this approach, except at explorative stages diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Types/document/Axioms.tex --- a/doc-src/TutorialI/Types/document/Axioms.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Nov 08 14:38:04 2000 +0100 @@ -32,6 +32,12 @@ \isa{parord}. For example, this is what \isa{refl} really looks like: \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}. +We have not made \isa{less{\isacharunderscore}le} a global definition because it would +fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}. +There are however situations where it is the other way around, which such a +definition would complicate. The slight drawback of the above class is that +we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance. + We can now prove simple theorems in this abstract setting, for example that \isa{{\isacharless}{\isacharless}} is not symmetric:% \end{isamarkuptext}% diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Types/document/Typedef.tex --- a/doc-src/TutorialI/Types/document/Typedef.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Wed Nov 08 14:38:04 2000 +0100 @@ -15,7 +15,7 @@ then read on. \begin{warn} Types in HOL must be non-empty; otherwise the quantifier rules would be - unsound, because $\exists x. x=x$ is a theorem. + unsound, because $\exists x.\ x=x$ is a theorem. \end{warn}% \end{isamarkuptext}% % @@ -30,7 +30,8 @@ \isacommand{typedecl}\ my{\isacharunderscore}new{\isacharunderscore}type% \begin{isamarkuptext}% \noindent\indexbold{*typedecl}% -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 +This does not define \isa{my{\isacharunderscore}new{\isacharunderscore}type} at all but merely introduces its +name. Thus we know nothing about this type, except that it is non-empty. Such declarations without definitions are useful only if that type can be viewed as a parameter of a theory and we do not intend to impose any restrictions on it. A typical example is given in @@ -47,7 +48,7 @@ axioms. Example:% \end{isamarkuptext}% \isacommand{axioms}\isanewline -just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}{\isacharbang}\ x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ True{\isachardoublequote}% +just{\isacharunderscore}one{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isacharcolon}{\isacharcolon}my{\isacharunderscore}new{\isacharunderscore}type{\isachardot}\ {\isasymforall}y{\isachardot}\ x\ {\isacharequal}\ y{\isachardoublequote}% \begin{isamarkuptext}% \noindent However, we strongly discourage this approach, except at explorative stages diff -r 1bfdd19c1d47 -r ef006735bee8 doc-src/TutorialI/Types/types.tex --- a/doc-src/TutorialI/Types/types.tex Tue Nov 07 18:38:24 2000 +0100 +++ b/doc-src/TutorialI/Types/types.tex Wed Nov 08 14:38:04 2000 +0100 @@ -22,6 +22,7 @@ \subsection{Pairs} \label{sec:products} % Check refs to this section to see what is expected of it. +% Mention type unit \subsection{Records} \label{sec:records}