src/ZF/ROOT.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@1461
     1
(*  Title:      ZF/ROOT
lcp@6
     2
    ID:         $Id$
clasohm@1461
     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
lcp@14
    14
(*For Pure/tactic??  A crude way of adding structure to rules*)
paulson@1512
    15
fun CHECK_SOLVED tac st =
paulson@1512
    16
    case Sequence.pull (tac st) of
clasohm@1461
    17
        None => error"DO_GOAL: tactic list failed"
lcp@5
    18
      | Some(x,_) => 
clasohm@1461
    19
                if has_fewer_prems 1 x then
clasohm@1461
    20
                    Sequence.cons(x, Sequence.null)
clasohm@1461
    21
                else (writeln"DO_GOAL: unsolved goals!!";
clasohm@1461
    22
                      writeln"Final proof state was ...";
clasohm@1461
    23
                      print_goals (!goals_limit) x;
paulson@1512
    24
                      raise ERROR);
lcp@5
    25
lcp@5
    26
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
lcp@5
    27
clasohm@0
    28
print_depth 1;
clasohm@0
    29
lcp@516
    30
(*Add user sections for inductive/datatype definitions*)
lcp@578
    31
use     "../Pure/section_utils.ML";
lcp@803
    32
use     "thy_syntax.ML";
lcp@516
    33
lcp@1069
    34
use_thy "Let";
lcp@488
    35
use_thy "InfDatatype";
lcp@516
    36
use_thy "List";
lcp@532
    37
use_thy "EquivClass";
clasohm@0
    38
clasohm@0
    39
(*printing functions are inherited from FOL*)
clasohm@0
    40
print_depth 8;
clasohm@0
    41
clasohm@1461
    42
val ZF_build_completed = ();    (*indicate successful build*)