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