46 ; |
46 ; |
47 repset: term ('morphisms' name name)? |
47 repset: term ('morphisms' name name)? |
48 ; |
48 ; |
49 \end{rail} |
49 \end{rail} |
50 |
50 |
51 \begin{descr} |
51 \begin{description} |
52 |
52 |
53 \item [\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of |
53 \item \hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} is similar |
54 Isabelle/Pure (see \secref{sec:types-pure}), but also declares type |
54 to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see |
55 arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an |
55 \secref{sec:types-pure}), but also declares type arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an actual HOL type |
56 actual HOL type constructor. %FIXME check, update |
56 constructor. %FIXME check, update |
57 |
57 |
58 \item [\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}] sets up a goal stating non-emptiness of the set \isa{A}. |
58 \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}} sets up |
59 After finishing the proof, the theory will be augmented by a |
59 a goal stating non-emptiness of the set \isa{A}. After finishing |
60 Gordon/HOL-style type definition, which establishes a bijection |
60 the proof, the theory will be augmented by a Gordon/HOL-style type |
61 between the representing set \isa{A} and the new type \isa{t}. |
61 definition, which establishes a bijection between the representing |
|
62 set \isa{A} and the new type \isa{t}. |
62 |
63 |
63 Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base |
64 Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base |
64 name may be given in parentheses). The injection from type to set |
65 name may be given in parentheses). The injection from type to set |
65 is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be |
66 is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be |
66 changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration). |
67 changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration). |
479 explicitly as well. |
478 explicitly as well. |
480 |
479 |
481 The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following |
480 The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following |
482 options. |
481 options. |
483 |
482 |
484 \begin{descr} |
483 \begin{description} |
485 |
484 |
486 \item [\isa{sequential}] enables a preprocessor which |
485 \item \isa{sequential} enables a preprocessor which disambiguates |
487 disambiguates overlapping patterns by making them mutually disjoint. |
486 overlapping patterns by making them mutually disjoint. Earlier |
488 Earlier equations take precedence over later ones. This allows to |
487 equations take precedence over later ones. This allows to give the |
489 give the specification in a format very similar to functional |
488 specification in a format very similar to functional programming. |
490 programming. Note that the resulting simplification and induction |
489 Note that the resulting simplification and induction rules |
491 rules correspond to the transformed specification, not the one given |
490 correspond to the transformed specification, not the one given |
492 originally. This usually means that each equation given by the user |
491 originally. This usually means that each equation given by the user |
493 may result in several theroems. Also note that this automatic |
492 may result in several theroems. Also note that this automatic |
494 transformation only works for ML-style datatype patterns. |
493 transformation only works for ML-style datatype patterns. |
495 |
494 |
496 \item [\isa{domintros}] enables the automated generation of |
495 \item \isa{domintros} enables the automated generation of |
497 introduction rules for the domain predicate. While mostly not |
496 introduction rules for the domain predicate. While mostly not |
498 needed, they can be helpful in some proofs about partial functions. |
497 needed, they can be helpful in some proofs about partial functions. |
499 |
498 |
500 \item [\isa{tailrec}] generates the unconstrained recursive |
499 \item \isa{tailrec} generates the unconstrained recursive |
501 equations even without a termination proof, provided that the |
500 equations even without a termination proof, provided that the |
502 function is tail-recursive. This currently only works |
501 function is tail-recursive. This currently only works |
503 |
502 |
504 \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a |
503 \item \isa{{\isachardoublequote}default\ d{\isachardoublequote}} allows to specify a default value for a |
505 (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}} |
504 (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}} |
506 whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}. |
505 whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}. |
507 |
506 |
508 \end{descr}% |
507 \end{description}% |
509 \end{isamarkuptext}% |
508 \end{isamarkuptext}% |
510 \isamarkuptrue% |
509 \isamarkuptrue% |
511 % |
510 % |
512 \isamarkupsubsection{Proof methods related to recursive definitions% |
511 \isamarkupsubsection{Proof methods related to recursive definitions% |
513 } |
512 } |
514 \isamarkuptrue% |
513 \isamarkuptrue% |
515 % |
514 % |
516 \begin{isamarkuptext}% |
515 \begin{isamarkuptext}% |
517 \begin{matharray}{rcl} |
516 \begin{matharray}{rcl} |
518 \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\ |
517 \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\ |
519 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\ |
518 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\ |
520 \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\ |
519 \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\ |
521 \end{matharray} |
520 \end{matharray} |
522 |
521 |
523 \begin{rail} |
522 \begin{rail} |
524 'relation' term |
523 'relation' term |
525 ; |
524 ; |
526 'lexicographic\_order' (clasimpmod *) |
525 'lexicographic\_order' (clasimpmod *) |
527 ; |
526 ; |
528 \end{rail} |
527 \end{rail} |
529 |
528 |
530 \begin{descr} |
529 \begin{description} |
531 |
530 |
532 \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to |
531 \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}} is a specialized method to |
533 solve goals regarding the completeness of pattern matching, as |
532 solve goals regarding the completeness of pattern matching, as |
534 required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\ |
533 required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\ |
535 \cite{isabelle-function}). |
534 \cite{isabelle-function}). |
536 |
535 |
537 \item [\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R}] introduces a termination |
536 \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination |
538 proof using the relation \isa{R}. The resulting proof state will |
537 proof using the relation \isa{R}. The resulting proof state will |
539 contain goals expressing that \isa{R} is wellfounded, and that the |
538 contain goals expressing that \isa{R} is wellfounded, and that the |
540 arguments of recursive calls decrease with respect to \isa{R}. |
539 arguments of recursive calls decrease with respect to \isa{R}. |
541 Usually, this method is used as the initial proof step of manual |
540 Usually, this method is used as the initial proof step of manual |
542 termination proofs. |
541 termination proofs. |
543 |
542 |
544 \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully |
543 \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}} attempts a fully |
545 automated termination proof by searching for a lexicographic |
544 automated termination proof by searching for a lexicographic |
546 combination of size measures on the arguments of the function. The |
545 combination of size measures on the arguments of the function. The |
547 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method, |
546 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method, |
548 which it uses internally to prove local descents. The same context |
547 which it uses internally to prove local descents. The same context |
549 modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see |
548 modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see |
550 \secref{sec:clasimp}. |
549 \secref{sec:clasimp}. |
551 |
550 |
552 In case of failure, extensive information is printed, which can help |
551 In case of failure, extensive information is printed, which can help |
553 to analyse the situation (cf.\ \cite{isabelle-function}). |
552 to analyse the situation (cf.\ \cite{isabelle-function}). |
554 |
553 |
555 \end{descr}% |
554 \end{description}% |
556 \end{isamarkuptext}% |
555 \end{isamarkuptext}% |
557 \isamarkuptrue% |
556 \isamarkuptrue% |
558 % |
557 % |
559 \isamarkupsubsection{Old-style recursive function definitions (TFL)% |
558 \isamarkupsubsection{Old-style recursive function definitions (TFL)% |
560 } |
559 } |
579 ; |
578 ; |
580 tc: nameref ('(' nat ')')? |
579 tc: nameref ('(' nat ')')? |
581 ; |
580 ; |
582 \end{rail} |
581 \end{rail} |
583 |
582 |
584 \begin{descr} |
583 \begin{description} |
585 |
584 |
586 \item [\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}] defines general well-founded |
585 \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded |
587 recursive functions (using the TFL package), see also |
586 recursive functions (using the TFL package), see also |
588 \cite{isabelle-HOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells |
587 \cite{isabelle-HOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells |
589 TFL to recover from failed proof attempts, returning unfinished |
588 TFL to recover from failed proof attempts, returning unfinished |
590 results. The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal |
589 results. The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal |
591 automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} |
590 automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} |
592 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the |
591 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the |
593 context of the Simplifier (cf.\ \secref{sec:simplifier}) and |
592 context of the Simplifier (cf.\ \secref{sec:simplifier}) and |
594 Classical reasoner (cf.\ \secref{sec:classical}). |
593 Classical reasoner (cf.\ \secref{sec:classical}). |
595 |
594 |
596 \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the |
595 \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} recommences the |
597 proof for leftover termination condition number \isa{i} (default |
596 proof for leftover termination condition number \isa{i} (default |
598 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of |
597 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of |
599 constant \isa{c}. |
598 constant \isa{c}. |
600 |
599 |
601 Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish |
600 Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish |
602 its internal proofs without manual intervention. |
601 its internal proofs without manual intervention. |
603 |
602 |
604 \end{descr} |
603 \end{description} |
605 |
604 |
606 \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared |
605 \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared |
607 globally, using the following attributes. |
606 globally, using the following attributes. |
608 |
607 |
609 \begin{matharray}{rcl} |
608 \begin{matharray}{rcl} |
610 \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\ |
609 \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isa{attribute} \\ |
611 \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\ |
610 \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isa{attribute} \\ |
612 \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\ |
611 \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isa{attribute} \\ |
613 \end{matharray} |
612 \end{matharray} |
614 |
613 |
615 \begin{rail} |
614 \begin{rail} |
616 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') |
615 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') |
617 ; |
616 ; |
662 ; |
661 ; |
663 'mono' (() | 'add' | 'del') |
662 'mono' (() | 'add' | 'del') |
664 ; |
663 ; |
665 \end{rail} |
664 \end{rail} |
666 |
665 |
667 \begin{descr} |
666 \begin{description} |
668 |
667 |
669 \item [\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}] define (co)inductive predicates from the |
668 \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the |
670 introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The |
669 introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The |
671 optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the |
670 optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the |
672 (co)inductive predicates that remain fixed throughout the |
671 (co)inductive predicates that remain fixed throughout the |
673 definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains |
672 definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains |
674 \emph{monotonicity theorems}, which are required for each operator |
673 \emph{monotonicity theorems}, which are required for each operator |
675 applied to a recursive set in the introduction rules. There |
674 applied to a recursive set in the introduction rules. There |
676 \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, |
675 \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, |
677 for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule! |
676 for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule! |
678 |
677 |
679 \item [\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}] are wrappers for to the previous commands, |
678 \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}} are wrappers for to the previous commands, |
680 allowing the definition of (co)inductive sets. |
679 allowing the definition of (co)inductive sets. |
681 |
680 |
682 \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules. These |
681 \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These |
683 rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}. |
682 rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}. |
684 |
683 |
685 \end{descr}% |
684 \end{description}% |
686 \end{isamarkuptext}% |
685 \end{isamarkuptext}% |
687 \isamarkuptrue% |
686 \isamarkuptrue% |
688 % |
687 % |
689 \isamarkupsubsection{Derived rules% |
688 \isamarkupsubsection{Derived rules% |
690 } |
689 } |
809 Moreover, rechecking Isabelle proof texts with already specified |
808 Moreover, rechecking Isabelle proof texts with already specified |
810 auxiliary facts is much faster than performing fully automated |
809 auxiliary facts is much faster than performing fully automated |
811 search over and over again. |
810 search over and over again. |
812 |
811 |
813 \begin{matharray}{rcl} |
812 \begin{matharray}{rcl} |
814 \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\ |
813 \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\ |
815 \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
814 \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
816 \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
815 \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
817 \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\ |
816 \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
818 \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\ |
817 \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\ |
819 \end{matharray} |
818 \end{matharray} |
820 |
819 |
821 \begin{rail} |
820 \begin{rail} |
822 'sledgehammer' (nameref *) |
821 'sledgehammer' (nameref *) |
823 ; |
822 ; |
824 |
823 |
825 'metis' thmrefs |
824 'metis' thmrefs |
826 ; |
825 ; |
827 \end{rail} |
826 \end{rail} |
828 |
827 |
829 \begin{descr} |
828 \begin{description} |
830 |
829 |
831 \item [\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}] invokes the specified automated theorem provers on |
830 \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}} |
832 the first subgoal. Provers are run in parallel, the first |
831 invokes the specified automated theorem provers on the first |
833 successful result is displayed, and the other attempts are |
832 subgoal. Provers are run in parallel, the first successful result |
834 terminated. |
833 is displayed, and the other attempts are terminated. |
835 |
834 |
836 Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as |
835 Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as |
837 ``ATP provers'' preference by the user interface. |
836 ``ATP provers'' preference by the user interface. |
838 |
837 |
839 There are additional preferences for timeout (default: 60 seconds), |
838 There are additional preferences for timeout (default: 60 seconds), |
840 and the maximum number of independent prover processes (default: 5); |
839 and the maximum number of independent prover processes (default: 5); |
841 excessive provers are automatically terminated. |
840 excessive provers are automatically terminated. |
842 |
841 |
843 \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated |
842 \item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated |
844 theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} |
843 theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} |
845 command. |
844 command. |
846 |
845 |
847 \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently |
846 \item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently |
848 running provers, including elapsed runtime, and the remaining time |
847 running provers, including elapsed runtime, and the remaining time |
849 until timeout. |
848 until timeout. |
850 |
849 |
851 \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running |
850 \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running |
852 provers. |
851 provers. |
853 |
852 |
854 \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis |
853 \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover |
855 prover with the given facts. Metis is an automated proof tool of |
854 with the given facts. Metis is an automated proof tool of medium |
856 medium strength, but is fully integrated into Isabelle/HOL, with |
855 strength, but is fully integrated into Isabelle/HOL, with explicit |
857 explicit inferences going through the kernel. Thus its results are |
856 inferences going through the kernel. Thus its results are |
858 guaranteed to be ``correct by construction''. |
857 guaranteed to be ``correct by construction''. |
859 |
858 |
860 Note that all facts used with Metis need to be specified as explicit |
859 Note that all facts used with Metis need to be specified as explicit |
861 arguments. There are no rule declarations as for other Isabelle |
860 arguments. There are no rule declarations as for other Isabelle |
862 provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}. |
861 provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}. |
863 |
862 |
864 \end{descr}% |
863 \end{description}% |
865 \end{isamarkuptext}% |
864 \end{isamarkuptext}% |
866 \isamarkuptrue% |
865 \isamarkuptrue% |
867 % |
866 % |
868 \isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}% |
867 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}% |
869 } |
868 } |
870 \isamarkuptrue% |
869 \isamarkuptrue% |
871 % |
870 % |
872 \begin{isamarkuptext}% |
871 \begin{isamarkuptext}% |
873 The following tools of Isabelle/HOL support cases analysis and |
872 The following tools of Isabelle/HOL support cases analysis and |
874 induction in unstructured tactic scripts; see also |
873 induction in unstructured tactic scripts; see also |
875 \secref{sec:cases-induct} for proper Isar versions of similar ideas. |
874 \secref{sec:cases-induct} for proper Isar versions of similar ideas. |
876 |
875 |
877 \begin{matharray}{rcl} |
876 \begin{matharray}{rcl} |
878 \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
877 \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\ |
879 \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
878 \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\ |
880 \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ |
879 \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\ |
881 \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{theory} \\ |
880 \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
882 \end{matharray} |
881 \end{matharray} |
883 |
882 |
884 \begin{rail} |
883 \begin{rail} |
885 'case\_tac' goalspec? term rule? |
884 'case\_tac' goalspec? term rule? |
886 ; |
885 ; |
893 |
892 |
894 rule: ('rule' ':' thmref) |
893 rule: ('rule' ':' thmref) |
895 ; |
894 ; |
896 \end{rail} |
895 \end{rail} |
897 |
896 |
898 \begin{descr} |
897 \begin{description} |
899 |
898 |
900 \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}] |
899 \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} admit |
901 admit to reason about inductive types. Rules are selected according |
900 to reason about inductive types. Rules are selected according to |
902 to the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} attributes, cf.\ \secref{sec:cases-induct}. The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this. |
901 the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} |
|
902 attributes, cf.\ \secref{sec:cases-induct}. The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this. |
903 |
903 |
904 These unstructured tactics feature both goal addressing and dynamic |
904 These unstructured tactics feature both goal addressing and dynamic |
905 instantiation. Note that named rule cases are \emph{not} provided |
905 instantiation. Note that named rule cases are \emph{not} provided |
906 as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof |
906 as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof |
907 methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} does not handle structured rule |
907 methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} does not handle structured rule |
908 statements, only the compact object-logic conclusion of the subgoal |
908 statements, only the compact object-logic conclusion of the subgoal |
909 being addressed. |
909 being addressed. |
910 |
910 |
911 \item [\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}] provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted |
911 \item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted |
912 forward manner. |
912 forward manner. |
913 |
913 |
914 While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the |
914 While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the |
915 result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level |
915 result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level |
916 for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should |
916 for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should |
917 be generalized before applying the resulting rule. |
917 be generalized before applying the resulting rule. |
918 |
918 |
919 \end{descr}% |
919 \end{description}% |
920 \end{isamarkuptext}% |
920 \end{isamarkuptext}% |
921 \isamarkuptrue% |
921 \isamarkuptrue% |
922 % |
922 % |
923 \isamarkupsection{Executable code% |
923 \isamarkupsection{Executable code% |
924 } |
924 } |
995 abstract executable view and \emph{serialization} to a specific |
995 abstract executable view and \emph{serialization} to a specific |
996 \emph{target language}. See \cite{isabelle-codegen} for an |
996 \emph{target language}. See \cite{isabelle-codegen} for an |
997 introduction on how to use it. |
997 introduction on how to use it. |
998 |
998 |
999 \begin{matharray}{rcl} |
999 \begin{matharray}{rcl} |
1000 \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1000 \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
1001 \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1001 \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
1002 \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1002 \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
1003 \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\ |
1003 \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1004 \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\ |
1004 \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1005 \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\ |
1005 \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1006 \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\ |
1006 \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1007 \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\ |
1007 \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1008 \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\ |
1008 \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1009 \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\ |
1009 \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1010 \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\ |
1010 \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1011 \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\ |
1011 \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1012 \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isartrans{theory}{theory} \\ |
1012 \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1013 \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ |
1013 \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
1014 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\ |
1014 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\ |
1015 \end{matharray} |
1015 \end{matharray} |
1016 |
1016 |
1017 \begin{rail} |
1017 \begin{rail} |
1018 'export\_code' ( constexpr + ) ? \\ |
1018 'export\_code' ( constexpr + ) ? \\ |
1019 ( ( 'in' target ( 'module\_name' string ) ? \\ |
1019 ( ( 'in' target ( 'module\_name' string ) ? \\ |
1109 |
1109 |
1110 Serializers take an optional list of arguments in parentheses. For |
1110 Serializers take an optional list of arguments in parentheses. For |
1111 \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype |
1111 \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype |
1112 declaration. |
1112 declaration. |
1113 |
1113 |
1114 \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems |
1114 \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems |
1115 representing the corresponding program containing all given |
1115 representing the corresponding program containing all given |
1116 constants; if no constants are given, the currently cached code |
1116 constants; if no constants are given, the currently cached code |
1117 theorems are printed. |
1117 theorems are printed. |
1118 |
1118 |
1119 \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of |
1119 \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of |
1120 theorems representing the corresponding program containing all given |
1120 theorems representing the corresponding program containing all given |
1121 constants; if no constants are given, the currently cached code |
1121 constants; if no constants are given, the currently cached code |
1122 theorems are visualized. |
1122 theorems are visualized. |
1123 |
1123 |
1124 \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set |
1124 \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set |
1125 for a logical type. |
1125 for a logical type. |
1126 |
1126 |
1127 \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants |
1127 \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants |
1128 with target-specific serializations; omitting a serialization |
1128 with target-specific serializations; omitting a serialization |
1129 deletes an existing serialization. |
1129 deletes an existing serialization. |
1130 |
1130 |
1131 \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type |
1131 \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type |
1132 constructors with target-specific serializations; omitting a |
1132 constructors with target-specific serializations; omitting a |
1133 serialization deletes an existing serialization. |
1133 serialization deletes an existing serialization. |
1134 |
1134 |
1135 \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes |
1135 \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes |
1136 with target-specific class names; omitting a |
1136 with target-specific class names; omitting a serialization deletes |
1137 serialization deletes an existing serialization. |
1137 an existing serialization. This applies only to \emph{Haskell}. |
1138 This applies only to \emph{Haskell}. |
1138 |
1139 |
1139 \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type |
1140 \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type |
|
1141 constructor / class instance relations as ``already present'' for a |
1140 constructor / class instance relations as ``already present'' for a |
1142 given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing |
1141 given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing |
1143 ``already present'' declaration. This applies only to |
1142 ``already present'' declaration. This applies only to |
1144 \emph{Haskell}. |
1143 \emph{Haskell}. |
1145 |
1144 |
1146 \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary |
1145 \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism |
1147 mechanism to generate monadic code for Haskell. |
1146 to generate monadic code for Haskell. |
1148 |
1147 |
1149 \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as |
1148 \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as |
1150 reserved for a given target, preventing it to be shadowed by any |
1149 reserved for a given target, preventing it to be shadowed by any |
1151 generated code. |
1150 generated code. |
1152 |
1151 |
1153 \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content |
1152 \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content |
1154 (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument |
1153 (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument |
1155 will remove an already added ``include''. |
1154 will remove an already added ``include''. |
1156 |
1155 |
1157 \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from |
1156 \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one |
1158 one module name onto another. |
1157 module name onto another. |
1159 |
1158 |
1160 \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which |
1159 \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not |
1161 are not required to have a definition by means of defining equations; |
1160 required to have a definition by means of defining equations; if |
1162 if needed these are implemented by program abort instead. |
1161 needed these are implemented by program abort instead. |
1163 |
1162 |
1164 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or |
1163 \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option |
1165 with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for |
1164 ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for code |
1166 code generation. Usually packages introducing defining equations |
1165 generation. Usually packages introducing defining equations provide |
1167 provide a reasonable default setup for selection. |
1166 a reasonable default setup for selection. |
1168 |
1167 |
1169 \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with |
1168 \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with |
1170 option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are |
1169 option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are |
1171 applied as rewrite rules to any defining equation during |
1170 applied as rewrite rules to any defining equation during |
1172 preprocessing. |
1171 preprocessing. |
1173 |
1172 |
1174 \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on |
1173 \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on |
1175 selected defining equations, code generator datatypes and |
1174 selected defining equations, code generator datatypes and |
1176 preprocessor setup. |
1175 preprocessor setup. |
1177 |
1176 |
1178 \end{descr}% |
1177 \end{description}% |
1179 \end{isamarkuptext}% |
1178 \end{isamarkuptext}% |
1180 \isamarkuptrue% |
1179 \isamarkuptrue% |
1181 % |
1180 % |
1182 \isamarkupsection{Definition by specification \label{sec:hol-specification}% |
1181 \isamarkupsection{Definition by specification \label{sec:hol-specification}% |
1183 } |
1182 } |
1184 \isamarkuptrue% |
1183 \isamarkuptrue% |
1185 % |
1184 % |
1186 \begin{isamarkuptext}% |
1185 \begin{isamarkuptext}% |
1187 \begin{matharray}{rcl} |
1186 \begin{matharray}{rcl} |
1188 \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\ |
1187 \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\ |
1189 \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\ |
1188 \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\ |
1190 \end{matharray} |
1189 \end{matharray} |
1191 |
1190 |
1192 \begin{rail} |
1191 \begin{rail} |
1193 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
1192 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) |
1194 ; |
1193 ; |
1195 decl: ((name ':')? term '(' 'overloaded' ')'?) |
1194 decl: ((name ':')? term '(' 'overloaded' ')'?) |
1196 \end{rail} |
1195 \end{rail} |
1197 |
1196 |
1198 \begin{descr} |
1197 \begin{description} |
1199 |
1198 |
1200 \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a |
1199 \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up a |
1201 goal stating the existence of terms with the properties specified to |
1200 goal stating the existence of terms with the properties specified to |
1202 hold for the constants given in \isa{decls}. After finishing the |
1201 hold for the constants given in \isa{decls}. After finishing the |
1203 proof, the theory will be augmented with definitions for the given |
1202 proof, the theory will be augmented with definitions for the given |
1204 constants, as well as with theorems stating the properties for these |
1203 constants, as well as with theorems stating the properties for these |
1205 constants. |
1204 constants. |
1206 |
1205 |
1207 \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets |
1206 \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up |
1208 up a goal stating the existence of terms with the properties |
1207 a goal stating the existence of terms with the properties specified |
1209 specified to hold for the constants given in \isa{decls}. After |
1208 to hold for the constants given in \isa{decls}. After finishing |
1210 finishing the proof, the theory will be augmented with axioms |
1209 the proof, the theory will be augmented with axioms expressing the |
1211 expressing the properties given in the first place. |
1210 properties given in the first place. |
1212 |
1211 |
1213 \item [\isa{decl}] declares a constant to be defined by the |
1212 \item \isa{decl} declares a constant to be defined by the |
1214 specification given. The definition for the constant \isa{c} is |
1213 specification given. The definition for the constant \isa{c} is |
1215 bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in |
1214 bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in |
1216 the declaration. Overloaded constants should be declared as such. |
1215 the declaration. Overloaded constants should be declared as such. |
1217 |
1216 |
1218 \end{descr} |
1217 \end{description} |
1219 |
1218 |
1220 Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style. \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by |
1219 Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style. \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by |
1221 construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the |
1220 construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the |
1222 user has explicitly proven it to be safe. A practical issue must be |
1221 user has explicitly proven it to be safe. A practical issue must be |
1223 considered, though: After introducing two constants with the same |
1222 considered, though: After introducing two constants with the same |