diff -r 83abec907072 -r 509e2ca547db ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Tue Jul 21 11:53:41 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Tue Jul 21 11:59:09 2009 +0200 @@ -786,27 +786,6 @@ @{term \"(\x::nat. x)\"}" "Free (\"x\", \"nat\")"} - \begin{readmore} - There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and - @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms - and types easier.\end{readmore} - - Have a look at these files and try to solve the following two exercises: - - \begin{exercise}\label{fun:revsum} - Write a function @{text "rev_sum : term -> term"} that takes a - term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "n"} might be one) - and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. Assume - the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} - associates to the left. Try your function on some examples. - \end{exercise} - - \begin{exercise}\label{fun:makesum} - Write a function which takes two terms representing natural numbers - in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the - number representing their sum. - \end{exercise} - There are a few subtle issues with constants. They usually crop up when pattern matching terms or types, or when constructing them. While it is perfectly ok to write the function @{text is_true} as follows @@ -890,6 +869,27 @@ | is_nil_or_all _ = false *} text {* + \begin{readmore} + There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and + @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms + and types easier.\end{readmore} + + Have a look at these files and try to solve the following two exercises: + + \begin{exercise}\label{fun:revsum} + Write a function @{text "rev_sum : term -> term"} that takes a + term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "n"} might be one) + and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. Assume + the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} + associates to the left. Try your function on some examples. + \end{exercise} + + \begin{exercise}\label{fun:makesum} + Write a function which takes two terms representing natural numbers + in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the + number representing their sum. + \end{exercise} + Occasionally you have to calculate what the ``base'' name of a given constant is. For this you can use the function @{ML Sign.extern_const} or @{ML Long_Name.base_name}. For example: