author | wenzelm |
Sun, 29 Nov 1998 13:16:47 +0100 | |
changeset 5989 | 9670dae0143d |
parent 5529 | 4a54acae6a15 |
child 6053 | 8a1059aa01f0 |
permissions | -rw-r--r-- |
1461 | 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 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic. |
|
7 |
||
8 |
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. |
|
9 |
*) |
|
10 |
||
11 |
val banner = "ZF Set Theory (in FOL)"; |
|
12 |
writeln banner; |
|
13 |
||
2469 | 14 |
eta_contract:=false; |
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 | 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 | 19 |
None => error"DO_GOAL: tactic list failed" |
5 | 20 |
| Some(x,_) => |
1461 | 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 | 23 |
else (writeln"DO_GOAL: unsolved goals!!"; |
24 |
writeln"Final proof state was ..."; |
|
25 |
print_goals (!goals_limit) x; |
|
1512 | 26 |
raise ERROR); |
5 | 27 |
|
28 |
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
|
29 |
||
0 | 30 |
print_depth 1; |
31 |
||
516 | 32 |
(*Add user sections for inductive/datatype definitions*) |
4262 | 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 | 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 | 37 |
use_thy "func"; |
38 |
use "typechk.ML"; |
|
488 | 39 |
use_thy "InfDatatype"; |
516 | 40 |
use_thy "List"; |
0 | 41 |
|
5529 | 42 |
(*Integers & binary integer arithmetic*) |
43 |
cd "Integ"; |
|
44 |
use_thy "Bin"; |
|
45 |
cd ".."; |
|
46 |
||
47 |
(*the all-in-one theory*) |
|
48 |
use_thy "Main"; |
|
49 |
||
0 | 50 |
print_depth 8; |
51 |
||
5511 | 52 |
Goal "True"; (*leave subgoal package empty*) |
53 |
||
1461 | 54 |
val ZF_build_completed = (); (*indicate successful build*) |