src/ZF/ROOT.ML
author clasohm
Thu Nov 04 14:11:59 1993 +0100 (1993-11-04)
changeset 90 a90653dabebc
parent 75 144ec40f2650
child 120 09287f26bfb8
permissions -rw-r--r--
renamed some files
     1 (*  Title: 	ZF/ROOT
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
     7 
     8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
     9 *)
    10 
    11 val banner = "ZF Set Theory (in FOL)";
    12 writeln banner;
    13 
    14 set_loadpath [".", "ex", "../FOL"];
    15 
    16 (*For Pure/tactic??  A crude way of adding structure to rules*)
    17 fun CHECK_SOLVED (Tactic tf) = 
    18   Tactic (fn state => 
    19     case Sequence.pull (tf state) of
    20 	None => error"DO_GOAL: tactic list failed"
    21       | Some(x,_) => 
    22 		if has_fewer_prems 1 x then
    23 		    Sequence.cons(x, Sequence.null)
    24 		else (writeln"DO_GOAL: unsolved goals!!";
    25 		      writeln"Final proof state was ...";
    26 		      print_goals (!goals_limit) x;
    27 		      raise ERROR));
    28 
    29 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    30 
    31 print_depth 1;
    32 use_thy "zf";
    33 
    34 use     "upair.ML";
    35 use     "subset.ML";
    36 use     "pair.ML";
    37 use     "domrange.ML";
    38 use     "func.ML";
    39 use     "equalities.ML";
    40 use     "simpdata.ML";  
    41 
    42 (*further development*)
    43 use_thy "bool";
    44 use_thy "sum";
    45 use_thy "qpair";
    46 use     "mono.ML";
    47 use_thy "fixedpt";
    48 
    49 (*Inductive/co-inductive definitions*)
    50 use     "ind_syntax.ML";
    51 use     "intr_elim.ML";
    52 use     "indrule.ML";
    53 use     "inductive.ML";
    54 use     "coinductive.ML";
    55 
    56 use_thy "perm";
    57 use_thy "trancl";
    58 use_thy "wf";
    59 use_thy "ord";
    60 use_thy "nat";
    61 use_thy "epsilon";
    62 use_thy "arith";
    63 
    64 (*Datatype/co-datatype definitions*)
    65 use_thy "univ";
    66 use_thy "quniv";
    67 use     "constructor.ML";
    68 use     "datatype.ML";
    69 
    70 use     "fin.ML";
    71 use_thy "List";
    72 use_thy "listfn";
    73 
    74 (*printing functions are inherited from FOL*)
    75 print_depth 8;
    76 
    77 val ZF_build_completed = ();	(*indicate successful build*)