doc-src/TutorialI/Types/Axioms.thy
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10420 ef006735bee8
child 10845 3696bc935bbd
permissions -rw-r--r--
*** empty log message ***
nipkow@10328
     1
(*<*)theory Axioms = Overloading:(*>*)
nipkow@10328
     2
nipkow@10328
     3
subsection{*Axioms*}
nipkow@10328
     4
nipkow@10328
     5
nipkow@10328
     6
text{*Now we want to attach axioms to our classes. Then we can reason on the
nipkow@10328
     7
level of classes and the results will be applicable to all types in a class,
nipkow@10328
     8
just as in axiomatic mathematics. These ideas are demonstrated by means of
nipkow@10328
     9
our above ordering relations.
nipkow@10328
    10
*}
nipkow@10328
    11
nipkow@10328
    12
subsubsection{*Partial orders*}
nipkow@10328
    13
nipkow@10328
    14
text{*
nipkow@10328
    15
A \emph{partial order} is a subclass of @{text ordrel}
nipkow@10328
    16
where certain axioms need to hold:
nipkow@10328
    17
*}
nipkow@10328
    18
nipkow@10328
    19
axclass parord < ordrel
nipkow@10328
    20
refl:    "x <<= x"
nipkow@10328
    21
trans:   "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
nipkow@10328
    22
antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
nipkow@10328
    23
less_le: "x << y = (x <<= y \<and> x \<noteq> y)"
nipkow@10328
    24
nipkow@10328
    25
text{*\noindent
nipkow@10328
    26
The first three axioms are the familiar ones, and the final one
nipkow@10328
    27
requires that @{text"<<"} and @{text"<<="} are related as expected.
nipkow@10328
    28
Note that behind the scenes, Isabelle has restricted the axioms to class
nipkow@10328
    29
@{text parord}. For example, this is what @{thm[source]refl} really looks like:
nipkow@10328
    30
@{thm[show_types]refl}.
nipkow@10328
    31
nipkow@10420
    32
We have not made @{thm[source]less_le} a global definition because it would
nipkow@10420
    33
fix once and for all that @{text"<<"} is defined in terms of @{text"<<="}.
nipkow@10420
    34
There are however situations where it is the other way around, which such a
nipkow@10420
    35
definition would complicate. The slight drawback of the above class is that
nipkow@10420
    36
we need to define both @{text"<<="} and @{text"<<"} for each instance.
nipkow@10420
    37
nipkow@10328
    38
We can now prove simple theorems in this abstract setting, for example
nipkow@10328
    39
that @{text"<<"} is not symmetric:
nipkow@10328
    40
*}
nipkow@10328
    41
nipkow@10328
    42
lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
nipkow@10328
    43
nipkow@10328
    44
txt{*\noindent
nipkow@10328
    45
The conclusion is not simply @{prop"\<not> y << x"} because the preprocessor
nipkow@10328
    46
of the simplifier would turn this into @{prop"y << x = False"}, thus yielding
nipkow@10328
    47
a nonterminating rewrite rule. In the above form it is a generally useful
nipkow@10328
    48
rule.
nipkow@10328
    49
The type constraint is necessary because otherwise Isabelle would only assume
nipkow@10328
    50
@{text"'a::ordrel"} (as required in the type of @{text"<<"}), in
nipkow@10328
    51
which case the proposition is not a theorem.  The proof is easy:
nipkow@10328
    52
*}
nipkow@10328
    53
nipkow@10328
    54
by(simp add:less_le antisym);
nipkow@10328
    55
nipkow@10328
    56
text{* We could now continue in this vein and develop a whole theory of
nipkow@10328
    57
results about partial orders. Eventually we will want to apply these results
nipkow@10328
    58
to concrete types, namely the instances of the class. Thus we first need to
nipkow@10328
    59
prove that the types in question, for example @{typ bool}, are indeed
nipkow@10328
    60
instances of @{text parord}:*}
nipkow@10328
    61
nipkow@10328
    62
instance bool :: parord
nipkow@10328
    63
apply intro_classes;
nipkow@10328
    64
nipkow@10328
    65
txt{*\noindent
nipkow@10328
    66
This time @{text intro_classes} leaves us with the four axioms,
nipkow@10328
    67
specialized to type @{typ bool}, as subgoals:
nipkow@10362
    68
@{subgoals[display,show_types,indent=0]}
nipkow@10328
    69
Fortunately, the proof is easy for blast, once we have unfolded the definitions
nipkow@10328
    70
of @{text"<<"} and @{text"<<="} at @{typ bool}:
nipkow@10328
    71
*}
nipkow@10328
    72
nipkow@10328
    73
apply(simp_all (no_asm_use) only: le_bool_def less_bool_def);
nipkow@10328
    74
by(blast, blast, blast, blast);
nipkow@10328
    75
nipkow@10328
    76
text{*\noindent
nipkow@10328
    77
Can you figure out why we have to include @{text"(no_asm_use)"}?
nipkow@10328
    78
nipkow@10328
    79
We can now apply our single lemma above in the context of booleans:
nipkow@10328
    80
*}
nipkow@10328
    81
nipkow@10328
    82
lemma "(P::bool) << Q \<Longrightarrow> \<not>(Q << P)";
nipkow@10328
    83
by simp;
nipkow@10328
    84
nipkow@10328
    85
text{*\noindent
nipkow@10328
    86
The effect is not stunning but demonstrates the principle.  It also shows
nipkow@10328
    87
that tools like the simplifier can deal with generic rules as well. Moreover,
nipkow@10328
    88
it should be clear that the main advantage of the axiomatic method is that
nipkow@10328
    89
theorems can be proved in the abstract and one does not need to repeat the
nipkow@10328
    90
proof for each instance.
nipkow@10328
    91
*}
nipkow@10328
    92
nipkow@10328
    93
subsubsection{*Linear orders*}
nipkow@10328
    94
nipkow@10328
    95
text{* If any two elements of a partial order are comparable it is a
nipkow@10328
    96
\emph{linear} or \emph{total} order: *}
nipkow@10328
    97
nipkow@10328
    98
axclass linord < parord
nipkow@10328
    99
total: "x <<= y \<or> y <<= x"
nipkow@10328
   100
nipkow@10328
   101
text{*\noindent
nipkow@10328
   102
By construction, @{text linord} inherits all axioms from @{text parord}.
nipkow@10328
   103
Therefore we can show that totality can be expressed in terms of @{text"<<"}
nipkow@10328
   104
as follows:
nipkow@10328
   105
*}
nipkow@10328
   106
nipkow@10328
   107
lemma "\<And>x::'a::linord. x<<y \<or> x=y \<or> y<<x";
nipkow@10328
   108
apply(simp add: less_le);
nipkow@10328
   109
apply(insert total);
nipkow@10328
   110
apply blast;
nipkow@10328
   111
done
nipkow@10328
   112
nipkow@10328
   113
text{*
nipkow@10328
   114
Linear orders are an example of subclassing by construction, which is the most
nipkow@10328
   115
common case. It is also possible to prove additional subclass relationships
nipkow@10328
   116
later on, i.e.\ subclassing by proof. This is the topic of the following
nipkow@10654
   117
paragraph.
nipkow@10328
   118
*}
nipkow@10328
   119
nipkow@10328
   120
subsubsection{*Strict orders*}
nipkow@10328
   121
nipkow@10328
   122
text{*
nipkow@10328
   123
An alternative axiomatization of partial orders takes @{text"<<"} rather than
nipkow@10328
   124
@{text"<<="} as the primary concept. The result is a \emph{strict} order:
nipkow@10328
   125
*}
nipkow@10328
   126
nipkow@10328
   127
axclass strord < ordrel
nipkow@10328
   128
irrefl:     "\<not> x << x"
nipkow@10328
   129
less_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
nipkow@10328
   130
le_less:    "x <<= y = (x << y \<or> x = y)"
nipkow@10328
   131
nipkow@10328
   132
text{*\noindent
nipkow@10328
   133
It is well known that partial orders are the same as strict orders. Let us
nipkow@10328
   134
prove one direction, namely that partial orders are a subclass of strict
nipkow@10328
   135
orders. The proof follows the ususal pattern: *}
nipkow@10328
   136
nipkow@10328
   137
instance parord < strord
nipkow@10328
   138
apply intro_classes;
nipkow@10328
   139
apply(simp_all (no_asm_use) add:less_le);
nipkow@10328
   140
  apply(blast intro: trans antisym);
nipkow@10328
   141
 apply(blast intro: refl);
nipkow@10328
   142
done
nipkow@10328
   143
nipkow@10396
   144
text{*
nipkow@10396
   145
The subclass relation must always be acyclic. Therefore Isabelle will
nipkow@10396
   146
complain if you also prove the relationship @{text"strord < parord"}.
nipkow@10396
   147
*}
nipkow@10328
   148
nipkow@10328
   149
nipkow@10328
   150
(*
nipkow@10328
   151
instance strord < parord
nipkow@10328
   152
apply intro_classes;
nipkow@10328
   153
apply(simp_all (no_asm_use) add:le_less);
nipkow@10328
   154
apply(blast intro: less_trans);
nipkow@10328
   155
apply(erule disjE);
nipkow@10328
   156
apply(erule disjE);
nipkow@10328
   157
apply(rule irrefl[THEN notE]);
nipkow@10328
   158
apply(rule less_trans, assumption, assumption);
nipkow@10328
   159
apply blast;apply blast;
nipkow@10328
   160
apply(blast intro: irrefl[THEN notE]);
nipkow@10328
   161
done
nipkow@10328
   162
*)
nipkow@10328
   163
nipkow@10396
   164
subsubsection{*Multiple inheritance and sorts*}
nipkow@10396
   165
nipkow@10396
   166
text{*
nipkow@10396
   167
A class may inherit from more than one direct superclass. This is called
nipkow@10396
   168
multiple inheritance and is certainly permitted. For example we could define
nipkow@10396
   169
the classes of well-founded orderings and well-orderings:
nipkow@10396
   170
*}
nipkow@10396
   171
nipkow@10396
   172
axclass wford < parord
nipkow@10396
   173
wford: "wf {(y,x). y << x}"
nipkow@10396
   174
nipkow@10396
   175
axclass wellord < linord, wford
nipkow@10396
   176
nipkow@10396
   177
text{*\noindent
nipkow@10396
   178
The last line expresses the usual definition: a well-ordering is a linear
nipkow@10396
   179
well-founded ordering. The result is the subclass diagram in
nipkow@10396
   180
Figure~\ref{fig:subclass}.
nipkow@10396
   181
nipkow@10396
   182
\begin{figure}[htbp]
nipkow@10396
   183
\[
nipkow@10396
   184
\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
nipkow@10396
   185
& & \isa{term}\\
nipkow@10396
   186
& & |\\
nipkow@10396
   187
& & \isa{ordrel}\\
nipkow@10396
   188
& & |\\
nipkow@10396
   189
& & \isa{strord}\\
nipkow@10396
   190
& & |\\
nipkow@10396
   191
& & \isa{parord} \\
nipkow@10396
   192
& / & & \backslash \\
nipkow@10396
   193
\isa{linord} & & & & \isa{wford} \\
nipkow@10396
   194
& \backslash & & / \\
nipkow@10396
   195
& & \isa{wellord}
nipkow@10396
   196
\end{array}
nipkow@10396
   197
\]
nipkow@10396
   198
\caption{Subclass diagramm}
nipkow@10396
   199
\label{fig:subclass}
nipkow@10396
   200
\end{figure}
nipkow@10396
   201
nipkow@10396
   202
Since class @{text wellord} does not introduce any new axioms, it can simply
nipkow@10396
   203
be viewed as the intersection of the two classes @{text linord} and @{text
nipkow@10396
   204
wford}. Such intersections need not be given a new name but can be created on
nipkow@10396
   205
the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
nipkow@10396
   206
represents the intersection of the $C@i$. Such an expression is called a
nipkow@10396
   207
\bfindex{sort}, and sorts can appear in most places where we have only shown
nipkow@10396
   208
classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
nipkow@10396
   209
In fact, @{text"'a::ord"} is short for @{text"'a::{ord}"}.
nipkow@10396
   210
However, we do not pursue this rarefied concept further.
nipkow@10396
   211
nipkow@10396
   212
This concludes our demonstration of type classes based on orderings.  We
nipkow@10396
   213
remind our readers that \isa{Main} contains a theory of
nipkow@10396
   214
orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
nipkow@10396
   215
It is recommended that, if possible,
nipkow@10396
   216
you base your own ordering relations on this theory.
nipkow@10396
   217
*}
nipkow@10396
   218
nipkow@10328
   219
subsubsection{*Inconsistencies*}
nipkow@10328
   220
nipkow@10328
   221
text{* The reader may be wondering what happens if we, maybe accidentally,
nipkow@10328
   222
attach an inconsistent set of axioms to a class. So far we have always
nipkow@10328
   223
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
nipkow@10328
   224
seems that we are throwing all caution to the wind. So why is there no
nipkow@10328
   225
problem?
nipkow@10328
   226
nipkow@10328
   227
The point is that by construction, all type variables in the axioms of an
nipkow@10328
   228
\isacommand{axclass} are automatically constrained with the class being
nipkow@10328
   229
defined (as shown for axiom @{thm[source]refl} above). These constraints are
nipkow@10328
   230
always carried around and Isabelle takes care that they are never lost,
nipkow@10328
   231
unless the type variable is instantiated with a type that has been shown to
nipkow@10328
   232
belong to that class. Thus you may be able to prove @{prop False}
nipkow@10328
   233
from your axioms, but Isabelle will remind you that this
nipkow@10328
   234
theorem has the hidden hypothesis that the class is non-empty.
nipkow@10328
   235
*}
nipkow@10328
   236
nipkow@10328
   237
(*
nipkow@10328
   238
axclass false<"term"
nipkow@10328
   239
false: "x \<noteq> x";
nipkow@10328
   240
nipkow@10328
   241
lemma "False";
nipkow@10328
   242
by(rule notE[OF false HOL.refl]);
nipkow@10328
   243
*)
nipkow@10328
   244
(*<*)end(*>*)