74 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
74 \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline |
75 \isacommand{oops} |
75 \isacommand{oops} |
76 \end{isabelle} |
76 \end{isabelle} |
77 \end{quote} |
77 \end{quote} |
78 |
78 |
79 However, both commands will only play minor roles in this tutorial (we will |
79 However, both commands will only play minor roles in this tutorial (we most of |
80 always arrange that the ML-code is defined outside proofs). |
80 the time make sure that the ML-code is defined outside proofs). |
81 |
81 |
82 |
82 |
83 |
83 |
84 |
84 |
85 Once a portion of code is relatively stable, you usually want to export it |
85 Once a portion of code is relatively stable, you usually want to export it |
209 end" |
209 end" |
210 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
210 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"} |
211 |
211 |
212 where now even @{term Pair} is written with its type (@{term Pair} is the |
212 where now even @{term Pair} is written with its type (@{term Pair} is the |
213 term-constructor for products). Other configuration values that influence |
213 term-constructor for products). Other configuration values that influence |
214 printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind |
214 printing of terms include |
215 show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}. |
215 |
216 *} |
216 \begin{itemize} |
217 |
217 \item @{ML_ind show_brackets in Syntax} |
218 text {* |
218 \item @{ML_ind show_sorts in Syntax} |
|
219 \item @{ML_ind eta_contract in Syntax} |
|
220 \end{itemize} |
|
221 |
219 A @{ML_type cterm} can be printed with the following function. |
222 A @{ML_type cterm} can be printed with the following function. |
220 *} |
223 *} |
221 |
224 |
222 ML{*fun pretty_cterm ctxt ctrm = |
225 ML{*fun pretty_cterm ctxt ctrm = |
223 pretty_term ctxt (term_of ctrm)*} |
226 pretty_term ctxt (term_of ctrm)*} |
687 val (one_trm, one_thm) = one_def |
690 val (one_trm, one_thm) = one_def |
688 in |
691 in |
689 pwriteln (pretty_term ctxt' one_trm); |
692 pwriteln (pretty_term ctxt' one_trm); |
690 pwriteln (pretty_thm ctxt' one_thm) |
693 pwriteln (pretty_thm ctxt' one_thm) |
691 end" |
694 end" |
692 "one |
695 "One |
693 one \<equiv> 1"} |
696 One \<equiv> 1"} |
694 Recall that @{ML "|>"} is the reverse function application. Recall also that |
697 Recall that @{ML "|>"} is the reverse function application. Recall also that |
695 the related reverse function composition is @{ML "#>"}. In fact all the |
698 the related reverse function composition is @{ML "#>"}. In fact all the |
696 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
699 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} |
697 described above have related combinators for function composition, namely |
700 described above have related combinators for function composition, namely |
698 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |
701 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in |
699 Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the |
702 Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the |
700 function @{text double} can also be written as: |
703 function @{text double} can also be written as: |
701 *} |
704 *} |
702 |
705 |
703 ML{*val double = |
706 ML{*val double = |
704 (fn x => (x, x)) |
707 (fn x => (x, x)) #-> |
705 #-> (fn x => fn y => x + y)*} |
708 (fn x => fn y => x + y)*} |
706 |
709 |
707 |
710 |
708 text {* |
711 text {* |
709 When using combinators for writing functions in waterfall fashion, it is |
712 When using combinators for writing functions in waterfall fashion, it is |
710 sometimes necessary to do some ``plumbing'' in order to fit functions |
713 sometimes necessary to do some ``plumbing'' in order to fit functions |