52 and even those can be undone when the proof |
52 and even those can be undone when the proof |
53 script is retracted. As mentioned in the Introduction, we will drop the |
53 script is retracted. As mentioned in the Introduction, we will drop the |
54 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
54 \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we |
55 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
55 show code. The lines prefixed with @{text [quotes] ">"} are not part of the |
56 code, rather they indicate what the response is when the code is evaluated. |
56 code, rather they indicate what the response is when the code is evaluated. |
57 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf}. |
57 There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for |
58 The first evaluates the given code, but any effect on the ambient |
58 including ML-code. The first evaluates the given code, but any effect on the |
59 theory is suppressed. The second needs to be used if ML-code is defined |
59 ambient theory is suppressed. The second needs to be used if ML-code is defined |
60 inside a proof. For example |
60 inside a proof. For example |
61 |
61 |
62 \begin{isabelle} |
62 \begin{quote} |
63 \isacommand{lemma}~@{text "test:"}\isanewline |
63 \begin{isabelle} |
64 \isacommand{shows}~@{text [quotes] "True"}\isanewline |
64 \isacommand{lemma}~@{text "test:"}\isanewline |
65 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial\""}~@{text "\<verbclose>"}\isanewline |
65 \isacommand{shows}~@{text [quotes] "True"}\isanewline |
66 \isacommand{oops} |
66 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
67 \end{isabelle} |
67 \isacommand{oops} |
68 |
68 \end{isabelle} |
69 Inside a proof the \isacommand{ML} will generate an error message. |
69 \end{quote} |
70 However, both commands will not play any role in this tutorial. |
70 |
|
71 However, both commands will not play any role in this tutorial (we, for example, |
|
72 always assume the ML-code is defined outside proofs). |
71 |
73 |
72 Once a portion of code is relatively stable, you usually want to export it |
74 Once a portion of code is relatively stable, you usually want to export it |
73 to a separate ML-file. Such files can then be included somewhere inside a |
75 to a separate ML-file. Such files can then be included somewhere inside a |
74 theory by using the command \isacommand{use}. For example |
76 theory by using the command \isacommand{use}. For example |
75 |
77 |
637 |
639 |
638 will show the term @{term "(a::nat) + b = c"}, but printed using the internal |
640 will show the term @{term "(a::nat) + b = c"}, but printed using the internal |
639 representation corresponding to the datatype @{ML_type "term"} defined as follows: |
641 representation corresponding to the datatype @{ML_type "term"} defined as follows: |
640 *} |
642 *} |
641 |
643 |
642 ML_val{*datatype term = |
644 ML_val %linenosgray{*datatype term = |
643 Const of string * typ |
645 Const of string * typ |
644 | Free of string * typ |
646 | Free of string * typ |
645 | Var of indexname * typ |
647 | Var of indexname * typ |
646 | Bound of int |
648 | Bound of int |
647 | Abs of string * typ * term |
649 | Abs of string * typ * term |
648 | $ of term * term *} |
650 | $ of term * term *} |
649 |
651 |
650 text {* |
652 text {* |
651 Terms use the usual de Bruijn index mechanism---where |
653 As can be seen in Line 5, terms use the usual de Bruijn index mechanism |
652 bound variables are represented by the constructor @{ML Bound}. For |
654 for representing bound variables. For |
653 example in |
655 example in |
654 |
656 |
655 @{ML_response_fake [display, gray] |
657 @{ML_response_fake [display, gray] |
656 "@{term \"\<lambda>x y. x y\"}" |
658 "@{term \"\<lambda>x y. x y\"}" |
657 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} |
659 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"} |
684 "writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))" |
686 "writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))" |
685 "x"} |
687 "x"} |
686 |
688 |
687 When constructing terms, you are usually concerned with free variables (for example |
689 When constructing terms, you are usually concerned with free variables (for example |
688 you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). |
690 you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). |
689 If you deal with theorems, you have to observe the distinction. A similar |
691 If you deal with theorems, you have to, however, observe the distinction. A similar |
690 distinction holds for types (see below). |
692 distinction holds for types (see below). |
691 |
693 |
692 \begin{readmore} |
694 \begin{readmore} |
693 Terms and types are described in detail in \isccite{sec:terms}. Their |
695 Terms and types are described in detail in \isccite{sec:terms}. Their |
694 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
696 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
|
697 For constructing terms involving HOL constants, many helper functions are defined |
|
698 in @{ML_file "HOL/Tools/hologic.ML"}. |
695 \end{readmore} |
699 \end{readmore} |
696 |
700 |
697 Constructing terms via antiquotations has the advantage that only typable |
701 Constructing terms via antiquotations has the advantage that only typable |
698 terms can be constructed. For example |
702 terms can be constructed. For example |
699 |
703 |