--- a/src/ZF/ex/Ntree.thy Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* Title: ZF/ex/Ntree.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Datatype definition n-ary branching trees
-Demonstrates a simple use of function space in a datatype definition
-
-Based upon ex/Term.thy
-*)
-
-Ntree = Main +
-consts
- ntree :: i=>i
- maptree :: i=>i
- maptree2 :: [i,i] => i
-
-datatype
- "ntree(A)" = Branch ("a \\<in> A", "h \\<in> (\\<Union>n \\<in> nat. n -> ntree(A))")
- monos "[[subset_refl, Pi_mono] MRS UN_mono]" (*MUST have this form*)
- type_intrs "[nat_fun_univ RS subsetD]"
- type_elims UN_E
-
-datatype
- "maptree(A)" = Sons ("a \\<in> A", "h \\<in> maptree(A) -||> maptree(A)")
- monos FiniteFun_mono1 (*Use monotonicity in BOTH args*)
- type_intrs "[FiniteFun_univ1 RS subsetD]"
-
-datatype
- "maptree2(A,B)" = Sons2 ("a \\<in> A", "h \\<in> B -||> maptree2(A,B)")
- 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, \\<lambda>i \\<in> domain(h). pr`(h`i))))"
-
-constdefs
- ntree_copy :: i=>i
- "ntree_copy(z) == ntree_rec(%x h r. Branch(x,r), z)"
-
-end