src/ZF/ROOT.ML
author paulson
Fri, 18 Sep 1998 16:07:55 +0200
changeset 5511 7f52fb755581
parent 4271 3a82492e70c5
child 5529 4a54acae6a15
permissions -rw-r--r--
leaves subgoal package empty
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 =
4271
3a82492e70c5 changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents: 4262
diff changeset
    18
    case Seq.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
4271
3a82492e70c5 changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents: 4262
diff changeset
    22
                    Seq.cons(x, Seq.empty)
1461
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*)
4262
e4113a682883 $ISABELLE_HOME/src;
wenzelm
parents: 2469
diff changeset
    33
use     "$ISABELLE_HOME/src/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
5511
7f52fb755581 leaves subgoal package empty
paulson
parents: 4271
diff changeset
    46
Goal "True";  (*leave subgoal package empty*)
7f52fb755581 leaves subgoal package empty
paulson
parents: 4271
diff changeset
    47
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1361
diff changeset
    48
val ZF_build_completed = ();    (*indicate successful build*)