784 @{ML_response_fake [display, gray] |
784 @{ML_response_fake [display, gray] |
785 "subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})] |
785 "subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})] |
786 @{term \"(\<lambda>x::nat. x)\"}" |
786 @{term \"(\<lambda>x::nat. x)\"}" |
787 "Free (\"x\", \"nat\")"} |
787 "Free (\"x\", \"nat\")"} |
788 |
788 |
789 \begin{readmore} |
|
790 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
791 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
792 and types easier.\end{readmore} |
|
793 |
|
794 Have a look at these files and try to solve the following two exercises: |
|
795 |
|
796 \begin{exercise}\label{fun:revsum} |
|
797 Write a function @{text "rev_sum : term -> term"} that takes a |
|
798 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
|
799 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
800 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
801 associates to the left. Try your function on some examples. |
|
802 \end{exercise} |
|
803 |
|
804 \begin{exercise}\label{fun:makesum} |
|
805 Write a function which takes two terms representing natural numbers |
|
806 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
807 number representing their sum. |
|
808 \end{exercise} |
|
809 |
|
810 There are a few subtle issues with constants. They usually crop up when |
789 There are a few subtle issues with constants. They usually crop up when |
811 pattern matching terms or types, or when constructing them. While it is perfectly ok |
790 pattern matching terms or types, or when constructing them. While it is perfectly ok |
812 to write the function @{text is_true} as follows |
791 to write the function @{text is_true} as follows |
813 *} |
792 *} |
814 |
793 |
888 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
867 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true |
889 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
868 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true |
890 | is_nil_or_all _ = false *} |
869 | is_nil_or_all _ = false *} |
891 |
870 |
892 text {* |
871 text {* |
|
872 \begin{readmore} |
|
873 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and |
|
874 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms |
|
875 and types easier.\end{readmore} |
|
876 |
|
877 Have a look at these files and try to solve the following two exercises: |
|
878 |
|
879 \begin{exercise}\label{fun:revsum} |
|
880 Write a function @{text "rev_sum : term -> term"} that takes a |
|
881 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
|
882 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
|
883 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
|
884 associates to the left. Try your function on some examples. |
|
885 \end{exercise} |
|
886 |
|
887 \begin{exercise}\label{fun:makesum} |
|
888 Write a function which takes two terms representing natural numbers |
|
889 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the |
|
890 number representing their sum. |
|
891 \end{exercise} |
|
892 |
893 Occasionally you have to calculate what the ``base'' name of a given |
893 Occasionally you have to calculate what the ``base'' name of a given |
894 constant is. For this you can use the function @{ML Sign.extern_const} or |
894 constant is. For this you can use the function @{ML Sign.extern_const} or |
895 @{ML Long_Name.base_name}. For example: |
895 @{ML Long_Name.base_name}. For example: |
896 |
896 |
897 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
897 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |