539 "@{term \"(a::nat) + b = c\"}" |
539 "@{term \"(a::nat) + b = c\"}" |
540 "Const (\"op =\", \<dots>) $ |
540 "Const (\"op =\", \<dots>) $ |
541 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
541 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
542 |
542 |
543 will show the term @{term "(a::nat) + b = c"}, but printed using an internal |
543 will show the term @{term "(a::nat) + b = c"}, but printed using an internal |
544 representation corresponding to the datatype @{ML_type "term"}. |
544 representation corresponding to the data type @{ML_type "term"}. |
545 |
545 |
546 This internal representation uses the usual de Bruijn index mechanism---where |
546 This internal representation uses the usual de Bruijn index mechanism---where |
547 bound variables are represented by the constructor @{ML Bound}. The index in |
547 bound variables are represented by the constructor @{ML Bound}. The index in |
548 @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip |
548 @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip |
549 until we hit the @{ML Abs} that binds the corresponding variable. Note that |
549 until we hit the @{ML Abs} that binds the corresponding variable. Note that |
748 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
748 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
749 |
749 |
750 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"} |
750 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"} |
751 |
751 |
752 the name of the constant @{text "Nil"} depends on the theory in which the |
752 the name of the constant @{text "Nil"} depends on the theory in which the |
753 term constructor is defined (@{text "List"}) and also in which datatype |
753 term constructor is defined (@{text "List"}) and also in which data type |
754 (@{text "list"}). Even worse, some constants have a name involving |
754 (@{text "list"}). Even worse, some constants have a name involving |
755 type-classes. Consider for example the constants for @{term "zero"} and |
755 type-classes. Consider for example the constants for @{term "zero"} and |
756 \mbox{@{text "(op *)"}}: |
756 \mbox{@{text "(op *)"}}: |
757 |
757 |
758 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" |
758 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" |
760 Const (\"HOL.times_class.times\", \<dots>))"} |
760 Const (\"HOL.times_class.times\", \<dots>))"} |
761 |
761 |
762 While you could use the complete name, for example |
762 While you could use the complete name, for example |
763 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
763 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or |
764 matching against @{text "Nil"}, this would make the code rather brittle. |
764 matching against @{text "Nil"}, this would make the code rather brittle. |
765 The reason is that the theory and the name of the datatype can easily change. |
765 The reason is that the theory and the name of the data type can easily change. |
766 To make the code more robust, it is better to use the antiquotation |
766 To make the code more robust, it is better to use the antiquotation |
767 @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the |
767 @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the |
768 variable parts of the constant's name. Therefore a functions for |
768 variable parts of the constant's name. Therefore a functions for |
769 matching against constants that have a polymorphic type should |
769 matching against constants that have a polymorphic type should |
770 be written as follows. |
770 be written as follows. |
866 cterm_of @{theory} |
866 cterm_of @{theory} |
867 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) |
867 (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero) |
868 end" "0 + 0"} |
868 end" "0 + 0"} |
869 |
869 |
870 In Isabelle not just terms need to be certified, but also types. For example, |
870 In Isabelle not just terms need to be certified, but also types. For example, |
871 you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on |
871 you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on |
872 the ML-level as follows: |
872 the ML-level as follows: |
873 |
873 |
874 @{ML_response_fake [display,gray] |
874 @{ML_response_fake [display,gray] |
875 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" |
875 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})" |
876 "nat \<Rightarrow> bool"} |
876 "nat \<Rightarrow> bool"} |