src/ZF/ROOT.ML
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 5529 4a54acae6a15
child 6065 3b4a29166f26
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
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*)
paulson@6053
    33
use     "$ISABELLE_HOME/src/Pure/section_utils";
paulson@6053
    34
use     "thy_syntax";
lcp@516
    35
lcp@1069
    36
use_thy "Let";
paulson@2469
    37
use_thy "func";
paulson@6053
    38
use     "Tools/typechk";
paulson@6053
    39
use_thy "mono";
paulson@6053
    40
use     "ind_syntax";
paulson@6053
    41
use     "Tools/cartprod";
paulson@6053
    42
use_thy "Fixedpt";
paulson@6053
    43
use     "Tools/inductive_package";
paulson@6053
    44
use_thy "Inductive";
paulson@6053
    45
use_thy "QUniv";
paulson@6053
    46
use "Tools/datatype_package";
paulson@6053
    47
use "Tools/primrec_package";
paulson@6053
    48
use_thy "Datatype";
lcp@488
    49
use_thy "InfDatatype";
lcp@516
    50
use_thy "List";
clasohm@0
    51
paulson@5529
    52
(*Integers & binary integer arithmetic*)
paulson@5529
    53
cd "Integ";
paulson@5529
    54
use_thy "Bin";
paulson@5529
    55
cd "..";
paulson@5529
    56
paulson@5529
    57
(*the all-in-one theory*)
paulson@5529
    58
use_thy "Main";
paulson@5529
    59
clasohm@0
    60
print_depth 8;
clasohm@0
    61
paulson@5511
    62
Goal "True";  (*leave subgoal package empty*)
paulson@5511
    63
clasohm@1461
    64
val ZF_build_completed = ();    (*indicate successful build*)