923 |
923 |
924 @{ML_response_fake [gray,display] |
924 @{ML_response_fake [gray,display] |
925 "writeln (Syntax.string_of_term @{context} |
925 "writeln (Syntax.string_of_term @{context} |
926 (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" |
926 (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" |
927 "True = False"} |
927 "True = False"} |
928 |
|
929 \begin{readmore} |
|
930 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
931 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
932 and types easier.\end{readmore} |
|
933 |
|
934 Have a look at these files and try to solve the following two exercises: |
|
935 |
|
936 \begin{exercise}\label{fun:revsum} |
|
937 Write a function @{text "rev_sum : term -> term"} that takes a |
|
938 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero) |
|
939 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
940 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
941 associates to the left. Try your function on some examples. |
|
942 \end{exercise} |
|
943 |
|
944 \begin{exercise}\label{fun:makesum} |
|
945 Write a function which takes two terms representing natural numbers |
|
946 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
947 number representing their sum. |
|
948 \end{exercise} |
|
949 *} |
928 *} |
950 |
929 |
951 section {* Constants *} |
930 section {* Constants *} |
952 |
931 |
953 text {* |
932 text {* |
966 |
945 |
967 ML{*fun is_all (@{term All} $ _) = true |
946 ML{*fun is_all (@{term All} $ _) = true |
968 | is_all _ = false*} |
947 | is_all _ = false*} |
969 |
948 |
970 text {* |
949 text {* |
971 will not correctly match the formula @{prop "\<forall>x::nat. P x"}: |
950 will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: |
972 |
951 |
973 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
952 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"} |
974 |
953 |
975 The problem is that the @{text "@term"}-antiquotation in the pattern |
954 The problem is that the @{text "@term"}-antiquotation in the pattern |
976 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |
955 fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for |
1032 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
1011 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
1033 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
1012 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
1034 | is_nil_or_all _ = false *} |
1013 | is_nil_or_all _ = false *} |
1035 |
1014 |
1036 text {* |
1015 text {* |
1037 The antiquotation for properly referencing type constants is is @{text "@{type_name \<dots>}"}. |
1016 \begin{readmore} |
|
1017 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
1018 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
1019 and types easier.\end{readmore} |
|
1020 |
|
1021 Have a look at these files and try to solve the following two exercises: |
|
1022 |
|
1023 \begin{exercise}\label{fun:revsum} |
|
1024 Write a function @{text "rev_sum : term -> term"} that takes a |
|
1025 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
|
1026 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
1027 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
1028 associates to the left. Try your function on some examples. |
|
1029 \end{exercise} |
|
1030 |
|
1031 \begin{exercise}\label{fun:makesum} |
|
1032 Write a function which takes two terms representing natural numbers |
|
1033 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
1034 number representing their sum. |
|
1035 \end{exercise} |
|
1036 |
|
1037 The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}. |
1038 For example |
1038 For example |
1039 |
1039 |
1040 @{ML_response [display,gray] |
1040 @{ML_response [display,gray] |
1041 "@{type_name \"list\"}" "\"List.list\""} |
1041 "@{type_name \"list\"}" "\"List.list\""} |
1042 |
1042 |
1181 \begin{readmore} |
1181 \begin{readmore} |
1182 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1182 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1183 the file @{ML_file "Pure/thm.ML"}. |
1183 the file @{ML_file "Pure/thm.ML"}. |
1184 \end{readmore} |
1184 \end{readmore} |
1185 |
1185 |
1186 \begin{exercise} |
1186 \begin{exercise}\label{fun:revsum typed} |
1187 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1187 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
1188 result that type-checks. |
1188 result that type-checks. |
1189 \end{exercise} |
1189 \end{exercise} |
1190 |
1190 |
1191 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1191 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |