88 \end{isabelle} |
88 \end{isabelle} |
89 \end{quote} |
89 \end{quote} |
90 |
90 |
91 However, both commands will only play minor roles in this tutorial (we will |
91 However, both commands will only play minor roles in this tutorial (we will |
92 always arrange that the ML-code is defined outside proofs). |
92 always arrange that the ML-code is defined outside proofs). |
|
93 |
|
94 |
|
95 |
93 |
96 |
94 Once a portion of code is relatively stable, you usually want to export it |
97 Once a portion of code is relatively stable, you usually want to export it |
95 to a separate ML-file. Such files can then be included somewhere inside a |
98 to a separate ML-file. Such files can then be included somewhere inside a |
96 theory by using the command \isacommand{use}. For example |
99 theory by using the command \isacommand{use}. For example |
97 |
100 |
540 (fn x => x + 3)*} |
543 (fn x => x + 3)*} |
541 |
544 |
542 text {* |
545 text {* |
543 which is the function composed of first the increment-by-one function and then |
546 which is the function composed of first the increment-by-one function and then |
544 increment-by-two, followed by increment-by-three. Again, the reverse function |
547 increment-by-two, followed by increment-by-three. Again, the reverse function |
545 composition allows you to read the code top-down. |
548 composition allows you to read the code top-down. This combinator is often used |
546 |
549 for setup function inside the \isacommand{setup}-command. These function have to be |
|
550 of type @{ML_type "theory -> theory"} in order to install, for example, some new |
|
551 data inside the current theory. More than one such setup function can be composed |
|
552 with @{ML "#>"}. For example |
|
553 *} |
|
554 |
|
555 setup %gray {* let |
|
556 val (ival1, setup_ival1) = Attrib.config_int "ival1" 1 |
|
557 val (ival2, setup_ival2) = Attrib.config_int "ival2" 2 |
|
558 in |
|
559 setup_ival1 #> |
|
560 setup_ival2 |
|
561 end *} |
|
562 |
|
563 text {* |
|
564 after this the configuration values @{text ival1} and @{text ival2} are known |
|
565 in the current theory and can be manipulated by the user (for more information |
|
566 about configuration values see Section~\ref{sec:storing}, for more about setup |
|
567 functions see Section~\ref{sec:theories}). |
|
568 |
547 The remaining combinators we describe in this section add convenience for the |
569 The remaining combinators we describe in this section add convenience for the |
548 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in |
570 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in |
549 Basics} allows you to get hold of an intermediate result (to do some |
571 Basics} allows you to get hold of an intermediate result (to do some |
550 side-calculations for instance). The function |
572 side-calculations for instance). The function |
551 *} |
573 *} |
812 The point of these antiquotations is that referring to theorems in this way |
834 The point of these antiquotations is that referring to theorems in this way |
813 makes your code independent from what theorems the user might have stored |
835 makes your code independent from what theorems the user might have stored |
814 under this name (this becomes especially important when you deal with |
836 under this name (this becomes especially important when you deal with |
815 theorem lists; see Section \ref{sec:storing}). |
837 theorem lists; see Section \ref{sec:storing}). |
816 |
838 |
|
839 It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"} |
|
840 whose first argument is a statement (possibly many of them separated by @{text "and"}, |
|
841 and the second is a proof. For example |
|
842 *} |
|
843 |
|
844 ML{*val foo_thm = @{lemma "True" and "True" by simp simp} *} |
|
845 |
|
846 text {* |
|
847 which can be printed out as follows |
|
848 |
|
849 @{ML_response_fake [gray,display] |
|
850 "foo_thm |> string_of_thms @{context} |
|
851 |> tracing" |
|
852 "True, True"} |
|
853 |
817 You can also refer to the current simpset via an antiquotation. To illustrate |
854 You can also refer to the current simpset via an antiquotation. To illustrate |
818 this we implement the function that extracts the theorem names stored in a |
855 this we implement the function that extracts the theorem names stored in a |
819 simpset. |
856 simpset. |
820 *} |
857 *} |
821 |
858 |