530 *} |
530 *} |
531 |
531 |
532 section {* Terms and Types *} |
532 section {* Terms and Types *} |
533 |
533 |
534 text {* |
534 text {* |
535 One way to construct terms of Isabelle is by using the antiquotation |
535 One way to construct Isabelle terms, is by using the antiquotation |
536 \mbox{@{text "@{term \<dots>}"}}. For example: |
536 \mbox{@{text "@{term \<dots>}"}}. For example: |
537 |
537 |
538 @{ML_response [display,gray] |
538 @{ML_response [display,gray] |
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 This will show the term @{term "(a::nat) + b = c"}, but printed using the internal |
543 will show the term @{term "(a::nat) + b = c"}, but printed using an internal |
544 representation of this term. This internal representation corresponds to the |
544 representation corresponding to the datatype @{ML_type "term"}. |
545 datatype @{ML_type "term"}. |
|
546 |
545 |
547 The internal representation of terms uses the usual de Bruijn index mechanism where bound |
546 This internal representation uses the usual de Bruijn index mechanism---where |
548 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to |
547 bound variables are represented by the constructor @{ML Bound}. The index in |
549 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that |
548 @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip |
550 binds the corresponding variable. However, in Isabelle the names of bound variables are |
549 until we hit the @{ML Abs} that binds the corresponding variable. Note that |
551 kept at abstractions for printing purposes, and so should be treated only as ``comments''. |
550 the names of bound variables are kept at abstractions for printing purposes, |
552 Application in Isabelle is realised with the term-constructor @{ML $}. |
551 and so should be treated only as ``comments''. Application in Isabelle is |
|
552 realised with the term-constructor @{ML $}. |
553 |
553 |
554 \begin{readmore} |
554 \begin{readmore} |
555 Terms are described in detail in \isccite{sec:terms}. Their |
555 Terms are described in detail in \isccite{sec:terms}. Their |
556 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
556 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}. |
557 \end{readmore} |
557 \end{readmore} |
883 \begin{exercise} |
883 \begin{exercise} |
884 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
884 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
885 result that type-checks. |
885 result that type-checks. |
886 \end{exercise} |
886 \end{exercise} |
887 |
887 |
888 Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains |
888 Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains |
889 enough typing information (constants, free variables and abstractions all have typing |
889 enough typing information (constants, free variables and abstractions all have typing |
890 information) so that it is always clear what the type of a term is. |
890 information) so that it is always clear what the type of a term is. |
891 Given a well-typed term, the function @{ML type_of} returns the |
891 Given a well-typed term, the function @{ML type_of} returns the |
892 type of a term. Consider for example: |
892 type of a term. Consider for example: |
893 |
893 |
894 @{ML_response [display,gray] |
894 @{ML_response [display,gray] |
895 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
895 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"} |
896 |
896 |
897 To calculate the type, this function traverses the whole term and will |
897 To calculate the type, this function traverses the whole term and will |
898 detect any typing inconsistency. For examle changing the type of the variable |
898 detect any typing inconsistency. For example changing the type of the variable |
899 @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: |
899 @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: |
900 |
900 |
901 @{ML_response_fake [display,gray] |
901 @{ML_response_fake [display,gray] |
902 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
902 "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" |
903 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
903 "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"} |
933 end" |
933 end" |
934 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
934 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $ |
935 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
935 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} |
936 |
936 |
937 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
937 Instead of giving explicitly the type for the constant @{text "plus"} and the free |
938 variable @{text "x"}, the type-inference filles in the missing information. |
938 variable @{text "x"}, the type-inference fills in the missing information. |
939 |
939 |
940 \begin{readmore} |
940 \begin{readmore} |
941 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
941 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading, |
942 checking and pretty-printing of terms are defined. Fuctions related to the |
942 checking and pretty-printing of terms are defined. Functions related to the |
943 type inference are implemented in @{ML_file "Pure/type.ML"} and |
943 type inference are implemented in @{ML_file "Pure/type.ML"} and |
944 @{ML_file "Pure/type_infer.ML"}. |
944 @{ML_file "Pure/type_infer.ML"}. |
945 \end{readmore} |
945 \end{readmore} |
946 |
946 |
947 (FIXME: say something about sorts) |
947 (FIXME: say something about sorts) |
1019 Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text |
1019 Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text |
1020 "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags |
1020 "[symmetric]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags |
1021 annotated to theorems, but functions that do further processing once a |
1021 annotated to theorems, but functions that do further processing once a |
1022 theorem is proven. In particular, it is not possible to find out |
1022 theorem is proven. In particular, it is not possible to find out |
1023 what are all theorems that have a given attribute in common, unless of course |
1023 what are all theorems that have a given attribute in common, unless of course |
1024 the function behind the attribute stores the theorems in a retrivable |
1024 the function behind the attribute stores the theorems in a retrievable |
1025 datastructure. |
1025 data structure. |
1026 |
1026 |
1027 If you want to print out all currently known attributes a theorem |
1027 If you want to print out all currently known attributes a theorem |
1028 can have, you can use the function: |
1028 can have, you can use the function: |
1029 |
1029 |
1030 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
1030 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |