src/ZF/ROOT.ML
author paulson
Fri Sep 18 16:07:55 1998 +0200 (1998-09-18)
changeset 5511 7f52fb755581
parent 4271 3a82492e70c5
child 5529 4a54acae6a15
permissions -rw-r--r--
leaves subgoal package empty
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 =
wenzelm@4271
    18
    case Seq.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
wenzelm@4271
    22
                    Seq.cons(x, Seq.empty)
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
paulson@5511
    46
Goal "True";  (*leave subgoal package empty*)
paulson@5511
    47
clasohm@1461
    48
val ZF_build_completed = ();    (*indicate successful build*)