--- a/doc-src/TutorialI/Types/document/Axioms.tex Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Thu Jun 09 12:06:38 2005 +0200
@@ -49,8 +49,22 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the
+simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
+would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
+a nonterminating rewrite rule.
+(It would be used to try to prove its own precondition \emph{ad
+ infinitum}.)
+In the form above, the rule is useful.
+The type constraint is necessary because otherwise Isabelle would only assume
+\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}),
+when the proposition is not a theorem. The proof is easy:%
+\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
We could now continue in this vein and develop a whole theory of
@@ -62,10 +76,26 @@
\isamarkuptrue%
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
+specialized to type \isa{bool}, as subgoals:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
+\ {\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
+\ {\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
+\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
+\end{isabelle}
+Fortunately, the proof is easy for \isa{blast}
+once we have unfolded the definitions
+of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
+\end{isamarkuptxt}%
\isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -76,7 +106,7 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -108,10 +138,13 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
\isamarkupfalse%
+\isacommand{apply}\ blast\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
Linear orders are an example of subclassing\index{subclasses}
@@ -145,12 +178,28 @@
\isamarkuptrue%
\isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline
\isamarkupfalse%
-\isamarkupfalse%
-\isamarkuptrue%
+\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
+type\ variables{\isacharcolon}\isanewline
+\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
+\end{isabelle}
+Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
+are easily proved:%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
+\ \isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
The subclass relation must always be acyclic. Therefore Isabelle will