equal
deleted
inserted
replaced
518 *} |
518 *} |
519 |
519 |
520 ML{*fun make_fun_types tys ty = tys ---> ty *} |
520 ML{*fun make_fun_types tys ty = tys ---> ty *} |
521 |
521 |
522 text {* |
522 text {* |
523 A handy function for manipulating terms is @{ML_ind map_types}: it takes a |
523 A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a |
524 function and applies it to every type in a term. You can, for example, |
524 function and applies it to every type in a term. You can, for example, |
525 change every @{typ nat} in a term into an @{typ int} using the function: |
525 change every @{typ nat} in a term into an @{typ int} using the function: |
526 *} |
526 *} |
527 |
527 |
528 ML{*fun nat_to_int ty = |
528 ML{*fun nat_to_int ty = |
607 |
607 |
608 text {* |
608 text {* |
609 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
609 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
610 enough typing information (constants, free variables and abstractions all have typing |
610 enough typing information (constants, free variables and abstractions all have typing |
611 information) so that it is always clear what the type of a term is. |
611 information) so that it is always clear what the type of a term is. |
612 Given a well-typed term, the function @{ML_ind type_of} returns the |
612 Given a well-typed term, the function @{ML_ind type_of in Term} returns the |
613 type of a term. Consider for example: |
613 type of a term. Consider for example: |
614 |
614 |
615 @{ML_response [display,gray] |
615 @{ML_response [display,gray] |
616 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
616 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
617 |
617 |
622 @{ML_response_fake [display,gray] |
622 @{ML_response_fake [display,gray] |
623 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
623 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
624 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
624 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
625 |
625 |
626 Since the complete traversal might sometimes be too costly and |
626 Since the complete traversal might sometimes be too costly and |
627 not necessary, there is the function @{ML_ind fastype_of}, which |
627 not necessary, there is the function @{ML_ind fastype_of in Term}, which |
628 also returns the type of a term. |
628 also returns the type of a term. |
629 |
629 |
630 @{ML_response [display,gray] |
630 @{ML_response [display,gray] |
631 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
631 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
632 |
632 |
680 |
680 |
681 text {* |
681 text {* |
682 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type |
682 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type |
683 typ}es, since they are just arbitrary unchecked trees. However, you |
683 typ}es, since they are just arbitrary unchecked trees. However, you |
684 eventually want to see if a term is well-formed, or type-checks, relative to |
684 eventually want to see if a term is well-formed, or type-checks, relative to |
685 a theory. Type-checking is done via the function @{ML_ind cterm_of}, which |
685 a theory. Type-checking is done via the function @{ML_ind cterm_of in Thm}, which |
686 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} |
686 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} |
687 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are |
687 term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are |
688 abstract objects that are guaranteed to be type-correct, and they can only |
688 abstract objects that are guaranteed to be type-correct, and they can only |
689 be constructed via ``official interfaces''. |
689 be constructed via ``official interfaces''. |
690 |
690 |