--- 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))";
--- 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