doc-src/TutorialI/Types/Axioms.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10420 ef006735bee8 child 10654 458068404143 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: "\ x <<= y; y <<= z \ \ x <<= z"  nipkow@10328  22 antisym: "\ x <<= y; y <<= x \ \ x = y"  nipkow@10328  23 less_le: "x << y = (x <<= y \ x \ 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 \ (\ y << x) = True";  nipkow@10328  43 nipkow@10328  44 txt{*\noindent  nipkow@10328  45 The conclusion is not simply @{prop"\ 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 \ \(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 \ 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 "\x::'a::linord. x< x=y \ y< x << x"  nipkow@10328  129 less_trans: "\ x << y; y << z \ \ x << z"  nipkow@10328  130 le_less: "x <<= y = (x << y \ 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"\"} 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 \ 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(*>*)