src/ZF/ex/Ntree.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/ex/Ntree.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Datatype definition n-ary branching trees
     7 Demonstrates a simple use of function space in a datatype definition
     8 
     9 Based upon ex/Term.thy
    10 *)
    11 
    12 Ntree = InfDatatype +
    13 consts
    14   ntree    :: i=>i
    15   maptree  :: i=>i
    16   maptree2 :: [i,i] => i
    17 
    18 datatype
    19   "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
    20   monos       "[[subset_refl, Pi_mono] MRS UN_mono]"    (*MUST have this form*)
    21   type_intrs  "[nat_fun_univ RS subsetD]"
    22   type_elims  "[UN_E]"
    23 
    24 datatype
    25   "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
    26   monos       "[FiniteFun_mono1]"       (*Use monotonicity in BOTH args*)
    27   type_intrs  "[FiniteFun_univ1 RS subsetD]"
    28 
    29 datatype
    30   "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
    31   monos       "[subset_refl RS FiniteFun_mono]"
    32   type_intrs  "[FiniteFun_in_univ']"
    33 
    34 end