src/ZF/ex/Ntree.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 539 01906e4644e0
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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    and also "nested" monotonicity theorems
     9 
    10 Based upon ex/Term.thy
    11 *)
    12 
    13 Ntree = InfDatatype +
    14 consts
    15   ntree :: "i=>i"
    16 
    17 datatype
    18   "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
    19   monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"
    20   type_intrs  "[nat_fun_univ RS subsetD]"
    21   type_elims  "[UN_E]"
    22 
    23 end