src/ZF/ROOT.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 5 75e163863e16
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ROOT
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val banner = "ZF Set Theory (in FOL)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*For Pure/drule??  Multiple resolution infixes*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
infix 0 MRS MRL;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
(*Resolve a list of rules against bottom_rl from right to left*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
fun rls MRS bottom_rl = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  let fun rs_aux i [] = bottom_rl
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  in  rs_aux 1 rls  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
fun rlss MRL bottom_rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  let fun rs_aux i [] = bottom_rls
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  in  rs_aux 1 rlss  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
print_depth 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
use_thy "zf";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
use     "upair.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
use     "subset.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
use     "pair.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
use     "domrange.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
use     "func.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
use     "equalities.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
use     "simpdata.ML";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(*further development*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
use_thy "bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
use_thy "sum";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
use_thy "qpair";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
use     "mono.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
use_thy "fixedpt";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
(*Inductive/co-inductive definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
use     "ind-syntax.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
use     "intr-elim.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
use     "indrule.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
use     "inductive.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
use     "co-inductive.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
use_thy "perm";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
use_thy "trancl";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
use_thy "wf";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
use_thy "ordinal";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
use_thy "nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
use_thy "epsilon";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
use_thy "arith";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*Datatype/co-datatype definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
use_thy "univ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
use_thy "quniv";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
use     "constructor.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
use     "datatype.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
use     "fin.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
use     "list.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
use_thy "list-fn";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
(*printing functions are inherited from FOL*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
print_depth 8;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val ZF_build_completed = ();	(*indicate successful build*)