Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ex/Ntree.thy
author nipkow
Thu, 29 Apr 1999 18:33:31 +0200
changeset 6539 2e7d2fba9f6c
parent 6117 f9aad8ccd590
child 8125 df502e820d07
permissions -rw-r--r--
Eta contraction is now performed all the time during rewriting.

(*  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 = InfDatatype +
consts
  ntree    :: i=>i
  maptree  :: i=>i
  maptree2 :: [i,i] => i

datatype
  "ntree(A)" = Branch ("a: A", "h: (UN n: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: A", "h: maptree(A) -||> maptree(A)")
  monos        FiniteFun_mono1         (*Use monotonicity in BOTH args*)
  type_intrs  "[FiniteFun_univ1 RS subsetD]"

datatype
  "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
  monos       "[subset_refl RS FiniteFun_mono]"
  type_intrs   FiniteFun_in_univ'

end
isabelle