src/ZF/ex/Ntree.thy
author lcp
Fri Aug 12 12:28:46 1994 +0200 (1994-08-12)
changeset 515 abcc438e7c27
child 539 01906e4644e0
permissions -rw-r--r--
installation of new inductive/datatype sections
lcp@515
     1
(*  Title: 	ZF/ex/Ntree.ML
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Datatype definition n-ary branching trees
lcp@515
     7
Demonstrates a simple use of function space in a datatype definition
lcp@515
     8
   and also "nested" monotonicity theorems
lcp@515
     9
lcp@515
    10
Based upon ex/Term.thy
lcp@515
    11
*)
lcp@515
    12
lcp@515
    13
Ntree = InfDatatype +
lcp@515
    14
consts
lcp@515
    15
  ntree :: "i=>i"
lcp@515
    16
lcp@515
    17
datatype
lcp@515
    18
  "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
lcp@515
    19
  monos	      "[[subset_refl, Pi_mono] MRS UN_mono]"
lcp@515
    20
  type_intrs  "[nat_fun_univ RS subsetD]"
lcp@515
    21
  type_elims  "[UN_E]"
lcp@515
    22
lcp@515
    23
end