# HG changeset patch
# User paulson
# Date 1061370768 -7200
# Node ID 8bf06363bbb5a5cadfb55887f665e2f3e14bcf29
# Parent  2072802ab0e385096d63f053a8dd87d0250bd0df
new example

diff -r 2072802ab0e3 -r 8bf06363bbb5 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Wed Aug 20 11:04:17 2003 +0200
+++ b/src/ZF/Induct/Binary_Trees.thy	Wed Aug 20 11:12:48 2003 +0200
@@ -65,10 +65,9 @@
   done
 
 
-subsection {* Number of nodes *}
+subsection {* Number of nodes, with an example of tail-recursion *}
 
-consts
-  n_nodes :: "i => i"
+consts  n_nodes :: "i => i"
 primrec
   "n_nodes(Lf) = 0"
   "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"
@@ -76,6 +75,23 @@
 lemma n_nodes_type [simp]: "t \<in> bt(A) ==> n_nodes(t) \<in> nat"
   by (induct_tac t) auto
 
+consts  n_nodes_aux :: "i => i"
+primrec
+  "n_nodes_aux(Lf) = (\<lambda>k \<in> nat. k)"
+  "n_nodes_aux(Br(a, l, r)) = 
+      (\<lambda>k \<in> nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"
+
+lemma n_nodes_aux_eq [rule_format]:
+     "t \<in> bt(A) ==> \<forall>k \<in> nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
+  by (induct_tac t, simp_all) 
+
+constdefs
+  n_nodes_tail :: "i => i"
+   "n_nodes_tail(t) == n_nodes_aux(t) ` 0"
+
+lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
+ by (simp add: n_nodes_tail_def n_nodes_aux_eq) 
+
 
 subsection {* Number of leaves *}