514 |
514 |
515 section {* Storing Theorems *} |
515 section {* Storing Theorems *} |
516 |
516 |
517 section {* Theorem Attributes *} |
517 section {* Theorem Attributes *} |
518 |
518 |
|
519 section {* Printing Terms, CTerms and Theorems\label{sec:printing} *} |
|
520 |
|
521 text {* |
|
522 It will often be necesseary to inspect terms, cterms or theorems. Isabelle |
|
523 contains elaborate pretty-printing functions for that, but for quick-and-dirty |
|
524 solutions they are too unwieldy. A term can be transformed into a string using |
|
525 the function @{ML Syntax.string_of_term} |
|
526 |
|
527 @{ML_response_fake [display,gray] |
|
528 "Syntax.string_of_term @{context} @{term \"1::nat\"}" |
|
529 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} |
|
530 |
|
531 This produces a string, though with printing directions encoded in it. This |
|
532 can be properly printed, when enclosed in a @{ML warning} |
|
533 |
|
534 @{ML_response_fake [display,gray] |
|
535 "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})" |
|
536 "\"1\""} |
|
537 |
|
538 A @{ML_type cterm} can be transformed into a string by the function: |
|
539 *} |
|
540 |
|
541 ML{*fun str_of_cterm ctxt t = |
|
542 Syntax.string_of_term ctxt (term_of t)*} |
|
543 |
|
544 text {* |
|
545 If there are more than one @{ML_type cterm} to be printed, we can use the function |
|
546 @{ML commas} to conveniently separate them. |
|
547 *} |
|
548 |
|
549 ML{*fun str_of_cterms ctxt ts = |
|
550 commas (map (str_of_cterm ctxt) ts)*} |
|
551 |
|
552 text {* |
|
553 The easiest way to get the string of a theorem, is to transform it |
|
554 into a @{ML_type cterm} using the function @{ML crep_thm}. |
|
555 *} |
|
556 |
|
557 ML{*fun str_of_thm ctxt thm = |
|
558 let |
|
559 val {prop, ...} = crep_thm thm |
|
560 in |
|
561 str_of_cterm ctxt prop |
|
562 end*} |
|
563 |
|
564 text {* |
|
565 For more than one theorem, the following function adds commas in between them. |
|
566 *} |
|
567 |
|
568 ML{*fun str_of_thms ctxt thms = |
|
569 commas (map (str_of_thm ctxt) thms)*} |
|
570 |
|
571 |
519 section {* Operations on Constants (Names) *} |
572 section {* Operations on Constants (Names) *} |
520 |
573 |
521 text {* |
574 text {* |
522 |
575 |
523 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
576 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
587 which increments the argument @{text x} by 5. It does this by first incrementing |
640 which increments the argument @{text x} by 5. It does this by first incrementing |
588 the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking |
641 the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking |
589 the first component of the pair (Line 4) and finally incrementing the first |
642 the first component of the pair (Line 4) and finally incrementing the first |
590 component by 4 (Line 5). This kind of cascading manipulations of values is quite |
643 component by 4 (Line 5). This kind of cascading manipulations of values is quite |
591 common when dealing with theories (for example by adding a definition, followed by |
644 common when dealing with theories (for example by adding a definition, followed by |
592 lemmas and so on). It should also be familiar to anyone who has used Haskell's |
645 lemmas and so on). The reverse application allows you to read what happens inside |
593 do-notation. Writing the function @{ML inc_by_five} using the reverse |
646 the function in a top-down manner. This kind of codeing should also be familiar, |
594 application is much clearer than writing |
647 if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using |
|
648 the reverse application is much clearer than writing |
595 *} |
649 *} |
596 |
650 |
597 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} |
651 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} |
598 |
652 |
599 text {* or *} |
653 text {* or *} |
646 |
700 |
647 text {* increments the argument first by one and then by two. In the middle (Line 3), |
701 text {* increments the argument first by one and then by two. In the middle (Line 3), |
648 however, it uses @{ML tap} for printing the ``plus-one'' intermediate |
702 however, it uses @{ML tap} for printing the ``plus-one'' intermediate |
649 result inside the tracing buffer. The function @{ML tap} can only |
703 result inside the tracing buffer. The function @{ML tap} can only |
650 be used for side-calculations, because any value that is computed cannot |
704 be used for side-calculations, because any value that is computed cannot |
651 be merged back into the ``main waterfall''. To do this, the next combinator |
705 be merged back into the ``main waterfall''. To do this, you can use the next |
652 can be used. |
706 combinator. |
653 |
707 |
654 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
708 The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value |
655 and returns the result together with the value (as a pair). For example |
709 and returns the result together with the value (as a pair). For example |
656 the function |
710 the function |
657 *} |
711 *} |
659 ML{*fun inc_as_pair x = |
713 ML{*fun inc_as_pair x = |
660 x |> `(fn x => x + 1) |
714 x |> `(fn x => x + 1) |
661 |> (fn (x, y) => (x, y + 1))*} |
715 |> (fn (x, y) => (x, y + 1))*} |
662 |
716 |
663 text {* |
717 text {* |
664 takes @{text x} as argument, and then first |
718 takes @{text x} as argument, and then increments @{text x}, but also keeps |
665 increments @{text x}, but also keeps @{text x}. The intermediate result is |
719 @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)" |
666 therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the |
720 for x}. After that, the function increments the right-hand component of the |
667 right-hand component of the pair. So finally the result will be |
721 pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}. |
668 @{ML "(x + 1, x + 1)" for x}. |
|
669 |
722 |
670 The combinators @{ML "|>>"} and @{ML "||>"} are defined for |
723 The combinators @{ML "|>>"} and @{ML "||>"} are defined for |
671 functions manipulating pairs. The first applies the function to |
724 functions manipulating pairs. The first applies the function to |
672 the first component of the pair, defined as: |
725 the first component of the pair, defined as: |
673 *} |
726 *} |