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
clasohm@1478
     1
(*  Title:      ZF/ex/Ntree.ML
lcp@515
     2
    ID:         $Id$
clasohm@1478
     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
lcp@515
     9
Based upon ex/Term.thy
lcp@515
    10
*)
lcp@515
    11
lcp@515
    12
Ntree = InfDatatype +
lcp@515
    13
consts
clasohm@1401
    14
  ntree    :: i=>i
clasohm@1401
    15
  maptree  :: i=>i
clasohm@1401
    16
  maptree2 :: [i,i] => i
lcp@515
    17
lcp@515
    18
datatype
lcp@515
    19
  "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
clasohm@1478
    20
  monos       "[[subset_refl, Pi_mono] MRS UN_mono]"    (*MUST have this form*)
lcp@515
    21
  type_intrs  "[nat_fun_univ RS subsetD]"
lcp@515
    22
  type_elims  "[UN_E]"
lcp@515
    23
lcp@539
    24
datatype
lcp@539
    25
  "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
clasohm@1478
    26
  monos       "[FiniteFun_mono1]"       (*Use monotonicity in BOTH args*)
lcp@539
    27
  type_intrs  "[FiniteFun_univ1 RS subsetD]"
lcp@539
    28
lcp@539
    29
datatype
lcp@539
    30
  "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
clasohm@1478
    31
  monos       "[subset_refl RS FiniteFun_mono]"
lcp@539
    32
  type_intrs  "[FiniteFun_in_univ']"
lcp@539
    33
lcp@515
    34
end