656 because @{term "All"} is such a fundamental constant, which can be referenced |
656 because @{term "All"} is such a fundamental constant, which can be referenced |
657 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
657 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at |
658 |
658 |
659 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"} |
659 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"} |
660 |
660 |
661 the name of the constant depends on the theory in which the term constructor |
661 the name of the constant @{term "Nil"} depends on the theory in which the |
662 @{text "Nil"} is defined (@{text "List"}) and also in which datatype |
662 term constructor is defined (@{text "List"}) and also in which datatype |
663 (@{text "list"}). Even worse, some constants have a name involving |
663 (@{text "list"}). Even worse, some constants have a name involving |
664 type-classes. Consider for example the constants for @{term "zero"} |
664 type-classes. Consider for example the constants for @{term "zero"} and |
665 and @{text "(op *)"}: |
665 @{text "(op *)"}: |
666 |
666 |
667 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" |
667 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" |
668 "(Const (\"HOL.zero_class.zero\", \<dots>), |
668 "(Const (\"HOL.zero_class.zero\", \<dots>), |
669 Const (\"HOL.times_class.times\", \<dots>))"} |
669 Const (\"HOL.times_class.times\", \<dots>))"} |
670 |
670 |
755 |
755 |
756 @{ML_response [display,gray] |
756 @{ML_response [display,gray] |
757 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
757 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
758 |
758 |
759 To calculate the type, this function traverses the whole term and will |
759 To calculate the type, this function traverses the whole term and will |
760 detect any inconsistency. For examle changing the type of the variable |
760 detect any typing inconsistency. For examle changing the type of the variable |
761 from @{typ "nat"} to @{typ "int"} will result in the error message: |
761 from @{typ "nat"} to @{typ "int"} will result in the error message: |
762 |
762 |
763 @{ML_response_fake [display,gray] |
763 @{ML_response_fake [display,gray] |
764 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
764 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
765 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
765 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
766 |
766 |
767 Since the complete traversal might sometimes be too costly and |
767 Since the complete traversal might sometimes be too costly and |
768 not necessary, there is also the function @{ML fastype_of} which |
768 not necessary, there is also the function @{ML fastype_of} which |
769 returns a type. |
769 returns the type of a term. |
770 |
770 |
771 @{ML_response [display,gray] |
771 @{ML_response [display,gray] |
772 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
772 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
773 |
773 |
774 However, efficiency is gained on the expense of skiping some tests. You |
774 However, efficiency is gained on the expense of skiping some tests. You |
795 end" |
795 end" |
796 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
796 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
797 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
797 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
798 |
798 |
799 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
799 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
800 variable @{text "x"}, the type-inference will fill in the missing information. |
800 variable @{text "x"}, the type-inference filled in the missing information. |
801 |
801 |
802 |
802 |
803 \begin{readmore} |
803 \begin{readmore} |
804 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
804 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
805 checking and pretty-printing of terms are defined. |
805 checking and pretty-printing of terms are defined. |
862 } |
862 } |
863 \] |
863 \] |
864 |
864 |
865 However, while we obtained a theorem as result, this theorem is not |
865 However, while we obtained a theorem as result, this theorem is not |
866 yet stored in Isabelle's theorem database. So it cannot be referenced later |
866 yet stored in Isabelle's theorem database. So it cannot be referenced later |
867 on. How to store theorems will be explained in the next section. |
867 on. How to store theorems will be explained in Section~\ref{sec:storing}. |
868 |
868 |
869 \begin{readmore} |
869 \begin{readmore} |
870 For the functions @{text "assume"}, @{text "forall_elim"} etc |
870 For the functions @{text "assume"}, @{text "forall_elim"} etc |
871 see \isccite{sec:thms}. The basic functions for theorems are defined in |
871 see \isccite{sec:thms}. The basic functions for theorems are defined in |
872 @{ML_file "Pure/thm.ML"}. |
872 @{ML_file "Pure/thm.ML"}. |