doc-src/TutorialI/Types/document/Axioms.tex
author nipkow
Wed, 15 May 2002 13:50:16 +0200
changeset 13153 4b052946b41c
parent 12815 1f073030b97a
child 13750 b5cd10cb106b
permissions -rw-r--r--
arith can now deal with div 2 and mod 2.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
     1
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
     2
\begin{isabellebody}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
     3
\def\isabellecontext{Axioms}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
     4
\isamarkupfalse%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
     5
%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
     6
\isamarkupsubsection{Axioms%
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
     7
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
     8
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
     9
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    10
\begin{isamarkuptext}%
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    11
Attaching axioms to our classes lets us reason on the
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    12
level of classes.  The results will be applicable to all types in a class,
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    13
just as in axiomatic mathematics.  These ideas are demonstrated by means of
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    14
our ordering relations.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    15
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    16
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    17
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
    18
\isamarkupsubsubsection{Partial Orders%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
    19
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    20
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    21
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    22
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    23
A \emph{partial order} is a subclass of \isa{ordrel}
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    24
where certain axioms need to hold:%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    25
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    26
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    27
\isacommand{axclass}\ parord\ {\isacharless}\ ordrel\isanewline
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    28
refl{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isanewline
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    29
trans{\isacharcolon}\ \ \ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequote}\isanewline
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    30
antisym{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    31
less{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    32
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    33
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    34
\noindent
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    35
The first three axioms are the familiar ones, and the final one
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    36
requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    37
Note that behind the scenes, Isabelle has restricted the axioms to class
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    38
\isa{parord}. For example, the axiom \isa{refl} really is
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
    39
\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    40
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10397
diff changeset
    41
We have not made \isa{less{\isacharunderscore}le} a global definition because it would
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
    42
fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
    43
never the other way around. Below you will see why we want to avoid this
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    44
asymmetry. The drawback of our choice is that
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10397
diff changeset
    45
we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
ef006735bee8 *** empty log message ***
nipkow
parents: 10397
diff changeset
    46
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    47
We can now prove simple theorems in this abstract setting, for example
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    48
that \isa{{\isacharless}{\isacharless}} is not symmetric:%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    49
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    50
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    51
\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%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    52
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    53
\begin{isamarkuptxt}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    54
\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    55
The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the 
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    56
simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    57
would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    58
a nonterminating rewrite rule.  
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    59
(It would be used to try to prove its own precondition \emph{ad
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    60
    infinitum}.)
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    61
In the form above, the rule is useful.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    62
The type constraint is necessary because otherwise Isabelle would only assume
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    63
\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), 
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    64
when the proposition is not a theorem.  The proof is easy:%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    65
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    66
\isamarkuptrue%
12815
wenzelm
parents: 12332
diff changeset
    67
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    68
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    69
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    70
We could now continue in this vein and develop a whole theory of
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    71
results about partial orders. Eventually we will want to apply these results
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    72
to concrete types, namely the instances of the class. Thus we first need to
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    73
prove that the types in question, for example \isa{bool}, are indeed
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    74
instances of \isa{parord}:%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    75
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    76
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    77
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    78
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    79
\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    80
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    81
\begin{isamarkuptxt}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    82
\noindent
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    83
This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    84
specialized to type \isa{bool}, as subgoals:
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    85
\begin{isabelle}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    86
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
10696
76d7f6c9a14c *** empty log message ***
nipkow
parents: 10668
diff changeset
    87
\ {\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
76d7f6c9a14c *** empty log message ***
nipkow
parents: 10668
diff changeset
    88
\ {\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
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    89
\ {\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}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    90
\end{isabelle}
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    91
Fortunately, the proof is easy for \isa{blast}
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    92
once we have unfolded the definitions
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    93
of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    94
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    95
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
    96
\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
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    97
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    98
\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
    99
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   100
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   101
\noindent
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   102
Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}?
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   103
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   104
We can now apply our single lemma above in the context of booleans:%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   105
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   106
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   107
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   108
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   109
\isacommand{by}\ simp\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   110
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   111
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   112
\noindent
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
   113
The effect is not stunning, but it demonstrates the principle.  It also shows
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   114
that tools like the simplifier can deal with generic rules.
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   115
The main advantage of the axiomatic method is that
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   116
theorems can be proved in the abstract and freely reused for each instance.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   117
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   118
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   119
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
   120
\isamarkupsubsubsection{Linear Orders%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
   121
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   122
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   123
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   124
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   125
If any two elements of a partial order are comparable it is a
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   126
\textbf{linear} or \textbf{total} order:%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   127
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   128
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   129
\isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   130
linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   131
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   132
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   133
\noindent
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   134
By construction, \isa{linord} inherits all axioms from \isa{parord}.
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   135
Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   136
as follows:%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   137
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   138
\isamarkuptrue%
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   139
\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
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   140
\isamarkupfalse%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   141
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   142
\isamarkupfalse%
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   143
\isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   144
\isamarkupfalse%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   145
\isacommand{apply}\ blast\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   146
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   147
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   148
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   149
\begin{isamarkuptext}%
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   150
Linear orders are an example of subclassing\index{subclasses}
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   151
by construction, which is the most
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   152
common case.  Subclass relationships can also be proved.  
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   153
This is the topic of the following
10654
458068404143 *** empty log message ***
nipkow
parents: 10645
diff changeset
   154
paragraph.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   155
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   156
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   157
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
   158
\isamarkupsubsubsection{Strict Orders%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
   159
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   160
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   161
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   162
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   163
An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   164
\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   165
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   166
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   167
\isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   168
irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   169
less{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   170
le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   171
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   172
\begin{isamarkuptext}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   173
\noindent
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   174
It is well known that partial orders are the same as strict orders. Let us
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   175
prove one direction, namely that partial orders are a subclass of strict
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   176
orders.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   177
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   178
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   179
\isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   180
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   181
\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   182
%
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   183
\begin{isamarkuptxt}%
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   184
\noindent
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   185
\begin{isabelle}%
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   186
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   187
\ {\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
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   188
\ {\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
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   189
type\ variables{\isacharcolon}\isanewline
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   190
\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   191
\end{isabelle}
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   192
Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   193
are easily proved:%
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   194
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   195
\ \ \isamarkuptrue%
12815
wenzelm
parents: 12332
diff changeset
   196
\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   197
\ \isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   198
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   199
\isamarkupfalse%
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   200
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   201
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   202
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   203
%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   204
\begin{isamarkuptext}%
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   205
The subclass relation must always be acyclic. Therefore Isabelle will
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   206
complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   207
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   208
\isamarkuptrue%
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   209
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
   210
\isamarkupsubsubsection{Multiple Inheritance and Sorts%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
   211
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   212
\isamarkuptrue%
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   213
%
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   214
\begin{isamarkuptext}%
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   215
A class may inherit from more than one direct superclass. This is called
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   216
\bfindex{multiple inheritance}.  For example, we could define
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   217
the classes of well-founded orderings and well-orderings:%
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   218
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   219
\isamarkuptrue%
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   220
\isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   221
wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   222
\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   223
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   224
\isacommand{axclass}\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   225
%
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   226
\begin{isamarkuptext}%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   227
\noindent
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   228
The last line expresses the usual definition: a well-ordering is a linear
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   229
well-founded ordering. The result is the subclass diagram in
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   230
Figure~\ref{fig:subclass}.
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   231
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   232
\begin{figure}[htbp]
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   233
\[
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   234
\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
12815
wenzelm
parents: 12332
diff changeset
   235
& & \isa{type}\\
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   236
& & |\\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   237
& & \isa{ordrel}\\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   238
& & |\\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   239
& & \isa{strord}\\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   240
& & |\\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   241
& & \isa{parord} \\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   242
& / & & \backslash \\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   243
\isa{linord} & & & & \isa{wford} \\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   244
& \backslash & & / \\
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   245
& & \isa{wellord}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   246
\end{array}
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   247
\]
10878
b254d5ad6dd4 auto update
paulson
parents: 10845
diff changeset
   248
\caption{Subclass Diagram}
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   249
\label{fig:subclass}
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   250
\end{figure}
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   251
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   252
Since class \isa{wellord} does not introduce any new axioms, it can simply
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   253
be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   254
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   255
represents the intersection of the $C@i$. Such an expression is called a
11428
332347b9b942 tidying the index
paulson
parents: 11196
diff changeset
   256
\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   257
classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
11196
bb4ede27fcb7 *** empty log message ***
nipkow
parents: 10878
diff changeset
   258
In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   259
However, we do not pursue this rarefied concept further.
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   260
10396
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   261
This concludes our demonstration of type classes based on orderings.  We
5ab08609e6c8 *** empty log message ***
nipkow
parents: 10395
diff changeset
   262
remind our readers that \isa{Main} contains a theory of
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   263
orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   264
If possible, base your own ordering relations on this theory.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   265
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   266
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   267
%
10397
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
   268
\isamarkupsubsubsection{Inconsistencies%
e2d0dda41f2c auto update
paulson
parents: 10396
diff changeset
   269
}
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   270
\isamarkuptrue%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   271
%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   272
\begin{isamarkuptext}%
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   273
The reader may be wondering what happens if we
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   274
attach an inconsistent set of axioms to a class. So far we have always
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   275
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   276
seems that we are throwing all caution to the wind. So why is there no
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   277
problem?
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   278
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   279
The point is that by construction, all type variables in the axioms of an
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   280
\isacommand{axclass} are automatically constrained with the class being
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   281
defined (as shown for axiom \isa{refl} above). These constraints are
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   282
always carried around and Isabelle takes care that they are never lost,
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   283
unless the type variable is instantiated with a type that has been shown to
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   284
belong to that class. Thus you may be able to prove \isa{False}
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   285
from your axioms, but Isabelle will remind you that this
12332
aea72a834c85 *** empty log message ***
nipkow
parents: 11866
diff changeset
   286
theorem has the hidden hypothesis that the class is non-empty.
aea72a834c85 *** empty log message ***
nipkow
parents: 11866
diff changeset
   287
aea72a834c85 *** empty log message ***
nipkow
parents: 11866
diff changeset
   288
Even if each individual class is consistent, intersections of (unrelated)
aea72a834c85 *** empty log message ***
nipkow
parents: 11866
diff changeset
   289
classes readily become inconsistent in practice. Now we know this need not
aea72a834c85 *** empty log message ***
nipkow
parents: 11866
diff changeset
   290
worry us.%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   291
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   292
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11494
diff changeset
   293
\isamarkupfalse%
10328
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   294
\end{isabellebody}%
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   295
%%% Local Variables:
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   296
%%% mode: latex
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   297
%%% TeX-master: "root"
bf33cbd76c05 *** empty log message ***
nipkow
parents:
diff changeset
   298
%%% End: