# HG changeset patch
# User paulson
# Date 947781299 -3600
# Node ID df502e820d07a2d7e4f10da7931155bac013b2a0
# Parent  fe7d6fd68ea3c715655fa7358ec795f361ba46d7
added recursor

diff -r fe7d6fd68ea3 -r df502e820d07 src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Thu Jan 13 17:34:39 2000 +0100
+++ b/src/ZF/ex/Ntree.ML	Thu Jan 13 17:34:59 2000 +0100
@@ -63,6 +63,31 @@
 val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard;
 
 
+(** ntree recursion **)
+
+Goal "ntree_rec(b, Branch(x,h)) \
+\     = b(x, h, lam i: domain(h). ntree_rec(b, h`i))";
+by (rtac (ntree_rec_def RS def_Vrecursor RS trans) 1);
+by (Simp_tac 1);
+by (rewrite_goals_tac ntree.con_defs);
+by (asm_simp_tac (simpset() addsimps [rank_pair2 RSN (2, lt_trans), 
+				      rank_apply]) 1);;
+qed "ntree_rec_Branch";
+
+Goalw [ntree_copy_def]
+ "ntree_copy (Branch(x, h)) = Branch(x, lam i : domain(h). ntree_copy (h`i))";
+by (rtac ntree_rec_Branch 1);
+qed "ntree_copy_Branch";
+
+Addsimps [ntree_copy_Branch];
+
+Goal "z : ntree(A) ==> ntree_copy(z) = z";
+by (induct_tac "z" 1);
+by (auto_tac (claset(), simpset() addsimps [domain_of_fun, Pi_Collect_iff]));
+qed "ntree_copy_is_ident";
+
+
+
 (** maptree **)
 
 Goal "maptree(A) = A * (maptree(A) -||> maptree(A))";
diff -r fe7d6fd68ea3 -r df502e820d07 src/ZF/ex/Ntree.thy
--- a/src/ZF/ex/Ntree.thy	Thu Jan 13 17:34:39 2000 +0100
+++ b/src/ZF/ex/Ntree.thy	Thu Jan 13 17:34:59 2000 +0100
@@ -31,4 +31,14 @@
   monos       "[subset_refl RS FiniteFun_mono]"
   type_intrs   FiniteFun_in_univ'
 
+
+constdefs
+  ntree_rec  :: [[i,i,i]=>i, i] => i
+   "ntree_rec(b) == 
+    Vrecursor(%pr. ntree_case(%x h. b(x, h, lam i: domain(h). pr`(h`i))))"
+
+constdefs
+    ntree_copy     :: i=>i
+    "ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)"
+
 end