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