183 section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} |
182 section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} |
184 |
183 |
185 text {* |
184 text {* |
186 While antiquotations are very convenient for constructing terms, they can |
185 While antiquotations are very convenient for constructing terms, they can |
187 only construct fixed terms (remember they are ``linked'' at compile-time). |
186 only construct fixed terms (remember they are ``linked'' at compile-time). |
188 However, you often need to construct terms dynamically. For example, a |
187 However, you often need to construct terms manually. For example, a |
189 function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking |
188 function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking |
190 @{term P} and @{term Q} as arguments can only be written as: |
189 @{term P} and @{term Q} as arguments can only be written as: |
191 |
190 |
192 *} |
191 *} |
193 |
192 |
571 |
570 |
572 |
571 |
573 section {* Type-Checking\label{sec:typechecking} *} |
572 section {* Type-Checking\label{sec:typechecking} *} |
574 |
573 |
575 text {* |
574 text {* |
576 |
|
577 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type |
|
578 typ}es, since they are just arbitrary unchecked trees. However, you |
|
579 eventually want to see if a term is well-formed, or type-checks, relative to |
|
580 a theory. Type-checking is done via the function @{ML_ind cterm_of}, which |
|
581 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} |
|
582 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are |
|
583 abstract objects that are guaranteed to be type-correct, and they can only |
|
584 be constructed via ``official interfaces''. |
|
585 |
|
586 |
|
587 Type-checking is always relative to a theory context. For now we use |
|
588 the @{ML "@{theory}"} antiquotation to get hold of the current theory. |
|
589 For example you can write: |
|
590 |
|
591 @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"} |
|
592 |
|
593 This can also be written with an antiquotation: |
|
594 |
|
595 @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} |
|
596 |
|
597 Attempting to obtain the certified term for |
|
598 |
|
599 @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"} |
|
600 |
|
601 yields an error (since the term is not typable). A slightly more elaborate |
|
602 example that type-checks is: |
|
603 |
|
604 @{ML_response_fake [display,gray] |
|
605 "let |
|
606 val natT = @{typ \"nat\"} |
|
607 val zero = @{term \"0::nat\"} |
|
608 in |
|
609 cterm_of @{theory} |
|
610 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) |
|
611 end" "0 + 0"} |
|
612 |
|
613 In Isabelle not just terms need to be certified, but also types. For example, |
|
614 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on |
|
615 the ML-level as follows: |
|
616 |
|
617 @{ML_response_fake [display,gray] |
|
618 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" |
|
619 "nat \<Rightarrow> bool"} |
|
620 |
|
621 or with the antiquotation: |
|
622 |
|
623 @{ML_response_fake [display,gray] |
|
624 "@{ctyp \"nat \<Rightarrow> bool\"}" |
|
625 "nat \<Rightarrow> bool"} |
|
626 |
|
627 \begin{readmore} |
|
628 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
|
629 the file @{ML_file "Pure/thm.ML"}. |
|
630 \end{readmore} |
|
631 |
|
632 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
575 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
633 enough typing information (constants, free variables and abstractions all have typing |
576 enough typing information (constants, free variables and abstractions all have typing |
634 information) so that it is always clear what the type of a term is. |
577 information) so that it is always clear what the type of a term is. |
635 Given a well-typed term, the function @{ML_ind type_of} returns the |
578 Given a well-typed term, the function @{ML_ind type_of} returns the |
636 type of a term. Consider for example: |
579 type of a term. Consider for example: |
687 type-inference are implemented in @{ML_file "Pure/type.ML"} and |
630 type-inference are implemented in @{ML_file "Pure/type.ML"} and |
688 @{ML_file "Pure/type_infer.ML"}. |
631 @{ML_file "Pure/type_infer.ML"}. |
689 \end{readmore} |
632 \end{readmore} |
690 |
633 |
691 \footnote{\bf FIXME: say something about sorts.} |
634 \footnote{\bf FIXME: say something about sorts.} |
|
635 \footnote{\bf FIXME: give a ``readmore''.} |
692 |
636 |
693 \begin{exercise} |
637 \begin{exercise} |
694 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
638 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
695 result that type-checks. See what happens to the solutions of this |
639 result that type-checks. See what happens to the solutions of this |
696 exercise given in Appendix \ref{ch:solutions} when they receive an |
640 exercise given in Appendix \ref{ch:solutions} when they receive an |
697 ill-typed term as input. |
641 ill-typed term as input. |
698 \end{exercise} |
642 \end{exercise} |
699 *} |
643 *} |
700 |
644 |
|
645 section {* Certified Terms and Certified Types *} |
|
646 |
|
647 text {* |
|
648 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type |
|
649 typ}es, since they are just arbitrary unchecked trees. However, you |
|
650 eventually want to see if a term is well-formed, or type-checks, relative to |
|
651 a theory. Type-checking is done via the function @{ML_ind cterm_of}, which |
|
652 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} |
|
653 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are |
|
654 abstract objects that are guaranteed to be type-correct, and they can only |
|
655 be constructed via ``official interfaces''. |
|
656 |
|
657 Certification is always relative to a theory context. For example you can |
|
658 write: |
|
659 |
|
660 @{ML_response_fake [display,gray] |
|
661 "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" |
|
662 "a + b = c"} |
|
663 |
|
664 This can also be written with an antiquotation: |
|
665 |
|
666 @{ML_response_fake [display,gray] |
|
667 "@{cterm \"(a::nat) + b = c\"}" |
|
668 "a + b = c"} |
|
669 |
|
670 Attempting to obtain the certified term for |
|
671 |
|
672 @{ML_response_fake_both [display,gray] |
|
673 "@{cterm \"1 + True\"}" |
|
674 "Type unification failed \<dots>"} |
|
675 |
|
676 yields an error (since the term is not typable). A slightly more elaborate |
|
677 example that type-checks is: |
|
678 |
|
679 @{ML_response_fake [display,gray] |
|
680 "let |
|
681 val natT = @{typ \"nat\"} |
|
682 val zero = @{term \"0::nat\"} |
|
683 in |
|
684 cterm_of @{theory} |
|
685 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) |
|
686 end" "0 + 0"} |
|
687 |
|
688 In Isabelle not just terms need to be certified, but also types. For example, |
|
689 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on |
|
690 the ML-level as follows: |
|
691 |
|
692 @{ML_response_fake [display,gray] |
|
693 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" |
|
694 "nat \<Rightarrow> bool"} |
|
695 |
|
696 or with the antiquotation: |
|
697 |
|
698 @{ML_response_fake [display,gray] |
|
699 "@{ctyp \"nat \<Rightarrow> bool\"}" |
|
700 "nat \<Rightarrow> bool"} |
|
701 |
|
702 Since certified terms are, unlike terms, abstract objects, we cannot |
|
703 pattern-match against them. However, we can construct them. For example |
|
704 the function @{ML_ind capply in Thm} produces a certified application. |
|
705 |
|
706 @{ML_response_fake [display,gray] |
|
707 "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}" |
|
708 "P 3"} |
|
709 |
|
710 Similarly @{ML_ind list_comb in Drule} applies a list of @{ML_type cterm}s. |
|
711 |
|
712 @{ML_response_fake [display,gray] |
|
713 "let |
|
714 val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"} |
|
715 val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}] |
|
716 in |
|
717 Drule.list_comb (chead, cargs) |
|
718 end" |
|
719 "P () 3"} |
|
720 |
|
721 \begin{readmore} |
|
722 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
|
723 the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and |
|
724 @{ML_file "Pure/drule.ML"}. |
|
725 \end{readmore} |
|
726 *} |
701 |
727 |
702 section {* Theorems *} |
728 section {* Theorems *} |
703 |
729 |
704 text {* |
730 text {* |
705 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |
731 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |