466 in the first place. The locale package does not attempt to remove |
466 in the first place. The locale package does not attempt to remove |
467 subsumed interpretations. This situation is normally harmless, but |
467 subsumed interpretations. This situation is normally harmless, but |
468 note that $blast$ gets confused by the presence of multiple axclass |
468 note that $blast$ gets confused by the presence of multiple axclass |
469 instances of a rule. |
469 instances of a rule. |
470 \end{warn} |
470 \end{warn} |
|
471 |
|
472 |
|
473 \subsubsection{Classes} |
|
474 |
|
475 A special case of locales are type classes. Type classes |
|
476 consist of a locale with \emph{exactly one} type variable |
|
477 and an corresponding axclass. |
|
478 |
|
479 \indexisarcmd{class}\indexisarcmd{print-classes} |
|
480 \begin{matharray}{rcl} |
|
481 \isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\ |
|
482 \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ |
|
483 \isarcmd{print_classes}^* & : & \isarkeep{theory~|~proof} \\ |
|
484 \end{matharray} |
|
485 |
|
486 \begin{rail} |
|
487 'class' name '=' classexpr |
|
488 ; |
|
489 'instance' (instarity | instsubsort) |
|
490 ; |
|
491 'print\_classes' |
|
492 ; |
|
493 |
|
494 classexpr: ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) |
|
495 ; |
|
496 instarity: (axmdecl)? (nameref '::' arity + 'and') (axmdecl prop +)? |
|
497 ; |
|
498 instsubsort: nameref ('<' | subseteq) sort |
|
499 ; |
|
500 superclassexpr: nameref | (nameref '+' superclassexpr) |
|
501 ; |
|
502 \end{rail} |
|
503 |
|
504 \begin{descr} |
|
505 |
|
506 \item [$\CLASS~c = superclasses~+~body$] defines a new class $c$, |
|
507 inheriting from $superclasses$. Simultaneously, a locale |
|
508 named $c$ is introduces, inheriting from the locales |
|
509 corresponding to $superclasses$; also, an axclass |
|
510 named $c$, inheriting from the axclasses corresponding to |
|
511 $superclasses$. $\FIXESNAME$ in $body$ are lifted |
|
512 to the theory toplevel, constraining |
|
513 the free type variable to sort $c$ and stripping local syntax. |
|
514 $\ASSUMESNAME$ in $body$ are also lifted, |
|
515 constraining |
|
516 the free type variable to sort $c$. |
|
517 |
|
518 \item [$\INSTANCE~a: \vec{arity}~\vec{defs}$] |
|
519 sets up a goal stating type arities. The proof would usually |
|
520 proceed by $intro_classes$, and then establish the characteristic theorems |
|
521 of the type classes involved. |
|
522 The $defs$, if given, must correspond to the class parameters |
|
523 involved in the $arities$ and are introduces in the theory |
|
524 before proof. Name and attributes given after the $\INSTANCE$ |
|
525 command refer to \emph{all} definitions as a whole. |
|
526 After finishing the proof, the theory will be |
|
527 augmented by a type signature declaration corresponding to the |
|
528 resulting theorems. |
|
529 |
|
530 \item [$\INSTANCE~c \subseteq \vec{c}$] sets up a |
|
531 goal stating |
|
532 the interpretation of the locale corresponding to $c$ |
|
533 in the merge of all locales corresponding to $\vec{c}$. |
|
534 After finishing the proof, it is automatically lifted to |
|
535 prove the additional class relation $c \subseteq \vec{c}$. |
|
536 |
|
537 \item [$\isarkeyword{print_classes}$] prints the names of all classes |
|
538 in the current theory together with some additonal data. |
|
539 |
|
540 \end{descr} |
471 |
541 |
472 |
542 |
473 \section{Derived proof schemes} |
543 \section{Derived proof schemes} |
474 |
544 |
475 \subsection{Generalized elimination}\label{sec:obtain} |
545 \subsection{Generalized elimination}\label{sec:obtain} |
1124 rules (even if these would qualify as intuitionistic ones), but only few |
1194 rules (even if these would qualify as intuitionistic ones), but only few |
1125 declarations to the rule context of Isabelle/Pure |
1195 declarations to the rule context of Isabelle/Pure |
1126 (\S\ref{sec:pure-meth-att}). |
1196 (\S\ref{sec:pure-meth-att}). |
1127 |
1197 |
1128 \item [$contradiction$] solves some goal by contradiction, deriving any result |
1198 \item [$contradiction$] solves some goal by contradiction, deriving any result |
1129 from both $\neg A$ and $A$. Chained facts, which are guaranteed to |
1199 from both $\lnot A$ and $A$. Chained facts, which are guaranteed to |
1130 participate, may appear in either order. |
1200 participate, may appear in either order. |
1131 |
1201 |
1132 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
1202 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
1133 elim-resolution, after having inserted any chained facts. Exactly the rules |
1203 elim-resolution, after having inserted any chained facts. Exactly the rules |
1134 given as arguments are taken into account; this allows fine-tuned |
1204 given as arguments are taken into account; this allows fine-tuned |
1263 |
1333 |
1264 \item [$iff$] declares logical equivalences to the Simplifier and the |
1334 \item [$iff$] declares logical equivalences to the Simplifier and the |
1265 Classical reasoner at the same time. Non-conditional rules result in a |
1335 Classical reasoner at the same time. Non-conditional rules result in a |
1266 ``safe'' introduction and elimination pair; conditional ones are considered |
1336 ``safe'' introduction and elimination pair; conditional ones are considered |
1267 ``unsafe''. Rules with negative conclusion are automatically inverted |
1337 ``unsafe''. Rules with negative conclusion are automatically inverted |
1268 (using $\neg$ elimination internally). |
1338 (using $\lnot$ elimination internally). |
1269 |
1339 |
1270 The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only, |
1340 The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only, |
1271 and omits the Simplifier declaration. |
1341 and omits the Simplifier declaration. |
1272 |
1342 |
1273 \end{descr} |
1343 \end{descr} |