237 |
237 |
238 text {* |
238 text {* |
239 A @{ML_type cterm} can be transformed into a string by the following function. |
239 A @{ML_type cterm} can be transformed into a string by the following function. |
240 *} |
240 *} |
241 |
241 |
242 ML{*fun string_of_cterm ctxt t = |
242 ML{*fun string_of_cterm ctxt ct = |
243 string_of_term ctxt (term_of t)*} |
243 string_of_term ctxt (term_of ct)*} |
244 |
244 |
245 text {* |
245 text {* |
246 In this example the function @{ML [index] term_of} extracts the @{ML_type term} from |
246 In this example the function @{ML [index] term_of} extracts the @{ML_type |
247 a @{ML_type cterm}. More than one @{ML_type cterm}s can again be printed |
247 term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be |
248 with @{ML [index] commas}. |
248 printed with @{ML [index] commas}. |
249 *} |
249 *} |
250 |
250 |
251 ML{*fun string_of_cterms ctxt cts = |
251 ML{*fun string_of_cterms ctxt cts = |
252 commas (map (string_of_cterm ctxt) cts)*} |
252 commas (map (string_of_cterm ctxt) cts)*} |
253 |
253 |
259 ML{*fun string_of_thm ctxt thm = |
259 ML{*fun string_of_thm ctxt thm = |
260 string_of_cterm ctxt (#prop (crep_thm thm))*} |
260 string_of_cterm ctxt (#prop (crep_thm thm))*} |
261 |
261 |
262 text {* |
262 text {* |
263 Theorems also include schematic variables, such as @{text "?P"}, |
263 Theorems also include schematic variables, such as @{text "?P"}, |
264 @{text "?Q"} and so on. |
264 @{text "?Q"} and so on. They are needed in order to able to |
|
265 instantiate theorems when they are applied. For example the theorem |
|
266 @{thm [source] conjI} shown below can be used for any (typable) |
|
267 instantiation of @{text "?P"} and @{text "?Q"} |
265 |
268 |
266 @{ML_response_fake [display, gray] |
269 @{ML_response_fake [display, gray] |
267 "tracing (string_of_thm @{context} @{thm conjI})" |
270 "tracing (string_of_thm @{context} @{thm conjI})" |
268 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
271 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"} |
269 |
272 |
270 In order to improve the readability of theorems we convert these schematic |
273 However, in order to improve the readability when printing theorems, we |
271 variables into free variables using the function @{ML [index] import in |
274 convert these schematic variables into free variables using the function |
272 Variable}. This is similar to statements like @{text "conjI[no_vars]"} |
275 @{ML [index] import in Variable}. This is similar to statements like @{text |
273 from Isabelle's user-level. |
276 "conjI[no_vars]"} from Isabelle's user-level. |
274 *} |
277 *} |
275 |
278 |
276 ML{*fun no_vars ctxt thm = |
279 ML{*fun no_vars ctxt thm = |
277 let |
280 let |
278 val ((_, [thm']), _) = Variable.import true [thm] ctxt |
281 val ((_, [thm']), _) = Variable.import true [thm] ctxt |
298 |
301 |
299 fun string_of_thms_no_vars ctxt thms = |
302 fun string_of_thms_no_vars ctxt thms = |
300 commas (map (string_of_thm_no_vars ctxt) thms) *} |
303 commas (map (string_of_thm_no_vars ctxt) thms) *} |
301 |
304 |
302 text {* |
305 text {* |
303 When printing out several parcels of information that semantically |
306 Note, that when printing out several parcels of information that |
304 belong together, like a warning message consisting for example |
307 semantically belong together, like a warning message consisting for example |
305 of a term and a type, you should try to keep this information |
308 of a term and a type, you should try to keep this information together in a |
306 together in a single string. So do not print out information as |
309 single string. So do not print out information as |
307 |
310 |
308 @{ML_response_fake [display,gray] |
311 @{ML_response_fake [display,gray] |
309 "tracing \"First half,\"; |
312 "tracing \"First half,\"; |
310 tracing \"and second half.\"" |
313 tracing \"and second half.\"" |
311 "First half, |
314 "First half, |
518 *} |
521 *} |
519 |
522 |
520 ML{*fun (x, y) ||> f = (x, f y)*} |
523 ML{*fun (x, y) ||> f = (x, f y)*} |
521 |
524 |
522 text {* |
525 text {* |
523 These two functions can be used to avoid explicit @{text "lets"} for |
526 These two functions can, for example, be used to avoid explicit @{text "lets"} for |
524 intermediate values in functions that return pairs. Suppose for example you |
527 intermediate values in functions that return pairs. As an example, suppose you |
525 want to separate a list of integers into two lists according to a |
528 want to separate a list of integers into two lists according to a |
526 treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} |
529 treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} |
527 should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be |
530 should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be |
528 implemented as |
531 implemented as |
529 *} |
532 *} |
547 if i <= x |
550 if i <= x |
548 then separate i xs ||> cons x |
551 then separate i xs ||> cons x |
549 else separate i xs |>> cons x*} |
552 else separate i xs |>> cons x*} |
550 |
553 |
551 text {* |
554 text {* |
552 avoiding the explicit @{text "let"}. While in this example the gain is only |
555 avoiding the explicit @{text "let"}. While in this example the gain in |
553 small, in more complicated situations the benefit of avoiding @{text "lets"} |
556 conciseness is only small, in more complicated situations the benefit of |
554 can be substantial. |
557 avoiding @{text "lets"} can be substantial. |
555 |
558 |
556 With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. |
559 With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. |
557 This combinator is defined as |
560 This combinator is defined as |
558 *} |
561 *} |
559 |
562 |
615 (fn x => (x, x)) |
618 (fn x => (x, x)) |
616 #-> (fn x => fn y => x + y)*} |
619 #-> (fn x => fn y => x + y)*} |
617 |
620 |
618 |
621 |
619 text {* |
622 text {* |
620 When using combinators for writing function in waterfall fashion, it is |
623 When using combinators for writing functions in waterfall fashion, it is |
621 sometimes necessary to do some ``plumbing'' in order to fit functions |
624 sometimes necessary to do some ``plumbing'' in order to fit functions |
622 together. We have already seen such plumbing in the function @{ML |
625 together. We have already seen such plumbing in the function @{ML |
623 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML |
626 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML |
624 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such |
627 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such |
625 plumbing is also needed in situations where a functions operate over lists, |
628 plumbing is also needed in situations where a functions operate over lists, |
641 |
644 |
642 text {* |
645 text {* |
643 In this example we obtain two terms with appropriate typing. However, if you |
646 In this example we obtain two terms with appropriate typing. However, if you |
644 have only a single term, then @{ML check_terms in Syntax} needs to be |
647 have only a single term, then @{ML check_terms in Syntax} needs to be |
645 adapted. This can be done with the ``plumbing'' function @{ML |
648 adapted. This can be done with the ``plumbing'' function @{ML |
646 singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax}, |
649 singleton}.\footnote{There is already a function @{ML check_term in Syntax} |
647 which however is defined in terms of @{ML singleton} and @{ML check_terms in |
650 in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML |
648 Syntax}.} For example |
651 check_terms in Syntax}.} For example |
649 |
652 |
650 @{ML_response_fake [display, gray] |
653 @{ML_response_fake [display, gray] |
651 "let |
654 "let |
652 val ctxt = @{context} |
655 val ctxt = @{context} |
653 in |
656 in |