911 |
911 |
912 @{ML_response_fake [gray,display] |
912 @{ML_response_fake [gray,display] |
913 "writeln (Syntax.string_of_term @{context} |
913 "writeln (Syntax.string_of_term @{context} |
914 (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" |
914 (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))" |
915 "True = False"} |
915 "True = False"} |
916 |
|
917 \begin{readmore} |
|
918 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
919 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
920 and types easier.\end{readmore} |
|
921 |
|
922 Have a look at these files and try to solve the following two exercises: |
|
923 |
|
924 \begin{exercise}\label{fun:revsum} |
|
925 Write a function @{text "rev_sum : term -> term"} that takes a |
|
926 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero) |
|
927 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
928 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
929 associates to the left. Try your function on some examples. |
|
930 \end{exercise} |
|
931 |
|
932 \begin{exercise}\label{fun:makesum} |
|
933 Write a function which takes two terms representing natural numbers |
|
934 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
935 number representing their sum. |
|
936 \end{exercise} |
|
937 *} |
916 *} |
938 |
917 |
939 section {* Constants *} |
918 section {* Constants *} |
940 |
919 |
941 text {* |
920 text {* |
1020 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
999 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
1021 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
1000 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
1022 | is_nil_or_all _ = false *} |
1001 | is_nil_or_all _ = false *} |
1023 |
1002 |
1024 text {* |
1003 text {* |
1025 The antiquotation for properly referencing type constants is is @{text "@{type_name \<dots>}"}. |
1004 \begin{readmore} |
|
1005 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
1006 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
1007 and types easier.\end{readmore} |
|
1008 |
|
1009 Have a look at these files and try to solve the following two exercises: |
|
1010 |
|
1011 \begin{exercise}\label{fun:revsum} |
|
1012 Write a function @{text "rev_sum : term -> term"} that takes a |
|
1013 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
|
1014 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
1015 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
1016 associates to the left. Try your function on some examples. |
|
1017 \end{exercise} |
|
1018 |
|
1019 \begin{exercise}\label{fun:makesum} |
|
1020 Write a function which takes two terms representing natural numbers |
|
1021 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
1022 number representing their sum. |
|
1023 \end{exercise} |
|
1024 |
|
1025 The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}. |
1026 For example |
1026 For example |
1027 |
1027 |
1028 @{ML_response [display,gray] |
1028 @{ML_response [display,gray] |
1029 "@{type_name \"list\"}" "\"List.list\""} |
1029 "@{type_name \"list\"}" "\"List.list\""} |
1030 |
1030 |