equal
deleted
inserted
replaced
697 be easily folded over a list of terms. Similarly for all functions |
697 be easily folded over a list of terms. Similarly for all functions |
698 named @{text "add_*"} in @{ML_file "Pure/term.ML"}. |
698 named @{text "add_*"} in @{ML_file "Pure/term.ML"}. |
699 |
699 |
700 \begin{exercise}\label{fun:revsum} |
700 \begin{exercise}\label{fun:revsum} |
701 Write a function @{text "rev_sum : term -> term"} that takes a |
701 Write a function @{text "rev_sum : term -> term"} that takes a |
702 term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one) |
702 term of the form @{text "t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n"} (whereby @{text "n"} might be one) |
703 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume |
703 and returns the reversed sum @{text "t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1"}. Assume |
704 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} |
704 the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"} |
705 associates to the left. Try your function on some examples. |
705 associates to the left. Try your function on some examples. |
706 \end{exercise} |
706 \end{exercise} |
707 |
707 |
708 \begin{exercise}\label{fun:makesum} |
708 \begin{exercise}\label{fun:makesum} |
709 Write a function that takes two terms representing natural numbers |
709 Write a function that takes two terms representing natural numbers |
1512 To see theorems in ``action'', let us give a proof on the ML-level for the following |
1512 To see theorems in ``action'', let us give a proof on the ML-level for the following |
1513 statement: |
1513 statement: |
1514 *} |
1514 *} |
1515 |
1515 |
1516 lemma |
1516 lemma |
1517 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" |
1517 assumes assm\<^sub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" |
1518 and assm\<^isub>2: "P t" |
1518 and assm\<^sub>2: "P t" |
1519 shows "Q t"(*<*)oops(*>*) |
1519 shows "Q t"(*<*)oops(*>*) |
1520 |
1520 |
1521 text {* |
1521 text {* |
1522 The corresponding ML-code is as follows: |
1522 The corresponding ML-code is as follows: |
1523 *} |
1523 *} |