src/ZF/ROOT.ML
author wenzelm
Thu Nov 20 16:24:05 1997 +0100 (1997-11-20)
changeset 4262 e4113a682883
parent 2469 b50b8c0eec01
child 4271 3a82492e70c5
permissions -rw-r--r--
$ISABELLE_HOME/src;
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
paulson@2469
    14
eta_contract:=false;
paulson@2469
    15
lcp@14
    16
(*For Pure/tactic??  A crude way of adding structure to rules*)
paulson@1512
    17
fun CHECK_SOLVED tac st =
paulson@1512
    18
    case Sequence.pull (tac st) of
clasohm@1461
    19
        None => error"DO_GOAL: tactic list failed"
lcp@5
    20
      | Some(x,_) => 
clasohm@1461
    21
                if has_fewer_prems 1 x then
clasohm@1461
    22
                    Sequence.cons(x, Sequence.null)
clasohm@1461
    23
                else (writeln"DO_GOAL: unsolved goals!!";
clasohm@1461
    24
                      writeln"Final proof state was ...";
clasohm@1461
    25
                      print_goals (!goals_limit) x;
paulson@1512
    26
                      raise ERROR);
lcp@5
    27
lcp@5
    28
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
lcp@5
    29
clasohm@0
    30
print_depth 1;
clasohm@0
    31
lcp@516
    32
(*Add user sections for inductive/datatype definitions*)
wenzelm@4262
    33
use     "$ISABELLE_HOME/src/Pure/section_utils.ML";
lcp@803
    34
use     "thy_syntax.ML";
lcp@516
    35
lcp@1069
    36
use_thy "Let";
paulson@2469
    37
use_thy "func";
paulson@2469
    38
use     "typechk.ML";
lcp@488
    39
use_thy "InfDatatype";
lcp@516
    40
use_thy "List";
lcp@532
    41
use_thy "EquivClass";
clasohm@0
    42
clasohm@0
    43
(*printing functions are inherited from FOL*)
clasohm@0
    44
print_depth 8;
clasohm@0
    45
clasohm@1461
    46
val ZF_build_completed = ();    (*indicate successful build*)