show sum_list defn
Tue, 02 Aug 2022 13:15:59 +0200
changeset 75715 a480964ea704
parent 75714 1635ee32e6d8
child 75717 b93ed38cef85
show sum_list defn
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Fri Jul 29 08:45:51 2022 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Aug 02 13:15:59 2022 +0200
@@ -220,7 +220,9 @@
 Then define a function \<open>sum_tree ::\<close> \<^typ>\<open>nat tree \<Rightarrow> nat\<close>
 that sums up all values in a tree of natural numbers
 and prove \<^prop>\<open>sum_tree t = sum_list(contents t)\<close>
-(where \<^const>\<open>sum_list\<close> is predefined).
+where \<^const>\<open>sum_list\<close> is predefined by the equations
+@{thm sum_list.Nil[where 'a=nat]} and
+@{thm sum_list.Cons}.
@@ -272,8 +274,7 @@
 empty. Note that \<^const>\<open>itrev\<close> is tail-recursive: it can be
 compiled into a loop; no stack is necessary for executing it.
-Naturally, we would like to show that \<^const>\<open>itrev\<close> does indeed reverse
-its first argument provided the second one is empty:
+Naturally, we would like to show that \<^const>\<open>itrev\<close> reverses its first argument:
 lemma "itrev xs [] = rev xs"
@@ -323,7 +324,7 @@
 apply(induction xs arbitrary: ys)
-txt\<open>The induction hypothesis in the induction step is now universally quantified over \<open>ys\<close>:
+txt\<open>The induction hypothesis is now universally quantified over \<open>ys\<close>:
 Thus the proof succeeds: