src/ZF/ROOT.ML
author paulson
Fri, 03 Jan 1997 15:01:55 +0100
changeset 2469 b50b8c0eec01
parent 1512 ce37c64244c0
child 4262 e4113a682883
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
     1
(*  Title:      ZF/ROOT
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 5
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val banner = "ZF Set Theory (in FOL)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1512
diff changeset
    14
eta_contract:=false;
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1512
diff changeset
    15
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    16
(*For Pure/tactic??  A crude way of adding structure to rules*)
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    17
fun CHECK_SOLVED tac st =
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    18
    case Sequence.pull (tac st) of
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    19
        None => error"DO_GOAL: tactic list failed"
5
75e163863e16 test commit
lcp
parents: 0
diff changeset
    20
      | Some(x,_) => 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    21
                if has_fewer_prems 1 x then
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    22
                    Sequence.cons(x, Sequence.null)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    23
                else (writeln"DO_GOAL: unsolved goals!!";
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    24
                      writeln"Final proof state was ...";
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    25
                      print_goals (!goals_limit) x;
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1461
diff changeset
    26
                      raise ERROR);
5
75e163863e16 test commit
lcp
parents: 0
diff changeset
    27
75e163863e16 test commit
lcp
parents: 0
diff changeset
    28
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
75e163863e16 test commit
lcp
parents: 0
diff changeset
    29
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
print_depth 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    32
(*Add user sections for inductive/datatype definitions*)
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 532
diff changeset
    33
use     "../Pure/section_utils.ML";
803
4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents: 578
diff changeset
    34
use     "thy_syntax.ML";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    35
1069
66efd8f90fbd Now loads the theory "Let". Could add it to FOL, but this appears to
lcp
parents: 803
diff changeset
    36
use_thy "Let";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1512
diff changeset
    37
use_thy "func";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1512
diff changeset
    38
use     "typechk.ML";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
    39
use_thy "InfDatatype";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    40
use_thy "List";
532
851df239ac8b ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents: 516
diff changeset
    41
use_thy "EquivClass";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*printing functions are inherited from FOL*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
print_depth 8;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    46
val ZF_build_completed = ();    (*indicate successful build*)