src/ZF/Induct/ROOT.ML
author wenzelm
Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456 6f79698f294d
parent 23912 039ae566a4a2
child 35762 af3ff2ba4c54
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12201
7198f403a2f9 added Term and Tree_Forest (from converted ZF/ex);
wenzelm
parents: 12190
diff changeset
     1
(*  Title:      ZF/Induct/ROOT.ML
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     2
    ID:         $Id$
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     4
    Copyright   2001  University of Cambridge
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     5
12201
7198f403a2f9 added Term and Tree_Forest (from converted ZF/ex);
wenzelm
parents: 12190
diff changeset
     6
Inductive definitions.
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     7
*)
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
     8
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
     9
use_thys [
12229
bfba0eb5124b Ntree and Brouwer converted and moved to ZF/Induct;
wenzelm
parents: 12205
diff changeset
    10
(** Datatypes **)
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    11
  "Datatypes",       (*sample datatypes*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    12
  "Binary_Trees",    (*binary trees*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    13
  "Term",            (*recursion over the list functor*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    14
  "Ntree",           (*variable-branching trees; function demo*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    15
  "Tree_Forest",     (*mutual recursion*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    16
  "Brouwer",         (*Infinite-branching trees*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    17
  "Mutil",           (*mutilated chess board*)
12190
32a9c240f225 added Datatypes, Binary_Trees (from ZF/ex);
wenzelm
parents: 12089
diff changeset
    18
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    19
(*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    20
finite sets*)
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    21
  "Multiset",
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    22
  "Rmap",            (*mapping a relation over a list*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    23
  "PropLog",         (*completeness of propositional logic*)
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    24
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    25
(*two Coq examples by Christine Paulin-Mohring*)
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    26
  "ListN",
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    27
  "Acc",
12089
34e7693271a9 Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff changeset
    28
23912
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    29
  "Comb",            (*Combinatory Logic example*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    30
  "Primrec"          (*Primitive recursive functions*)
039ae566a4a2 simultaneous use_thys;
wenzelm
parents: 12229
diff changeset
    31
];