author | lcp |
Fri, 17 Sep 1993 16:16:38 +0200 | |
changeset 6 | 8ce8c4d13d4d |
parent 5 | 75e163863e16 |
child 14 | 1c0926788772 |
permissions | -rw-r--r-- |
0 | 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$ |
0 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
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 |
||
14 |
(*For Pure/drule?? Multiple resolution infixes*) |
|
15 |
infix 0 MRS MRL; |
|
16 |
||
17 |
(*Resolve a list of rules against bottom_rl from right to left*) |
|
18 |
fun rls MRS bottom_rl = |
|
19 |
let fun rs_aux i [] = bottom_rl |
|
20 |
| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls) |
|
21 |
in rs_aux 1 rls end; |
|
22 |
||
23 |
fun rlss MRL bottom_rls = |
|
24 |
let fun rs_aux i [] = bottom_rls |
|
25 |
| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss) |
|
26 |
in rs_aux 1 rlss end; |
|
27 |
||
5 | 28 |
fun CHECK_SOLVED (Tactic tf) = |
29 |
Tactic (fn state => |
|
30 |
case Sequence.pull (tf state) of |
|
31 |
None => error"DO_GOAL: tactic list failed" |
|
32 |
| Some(x,_) => |
|
33 |
if has_fewer_prems 1 x then |
|
34 |
Sequence.cons(x, Sequence.null) |
|
35 |
else (writeln"DO_GOAL: unsolved goals!!"; |
|
36 |
writeln"Final proof state was ..."; |
|
37 |
print_goals (!goals_limit) x; |
|
38 |
raise ERROR)); |
|
39 |
||
40 |
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); |
|
41 |
||
0 | 42 |
print_depth 1; |
43 |
use_thy "zf"; |
|
44 |
||
45 |
use "upair.ML"; |
|
46 |
use "subset.ML"; |
|
47 |
use "pair.ML"; |
|
48 |
use "domrange.ML"; |
|
49 |
use "func.ML"; |
|
50 |
use "equalities.ML"; |
|
51 |
use "simpdata.ML"; |
|
52 |
||
53 |
(*further development*) |
|
54 |
use_thy "bool"; |
|
55 |
use_thy "sum"; |
|
56 |
use_thy "qpair"; |
|
57 |
use "mono.ML"; |
|
58 |
use_thy "fixedpt"; |
|
59 |
||
60 |
(*Inductive/co-inductive definitions*) |
|
61 |
use "ind-syntax.ML"; |
|
62 |
use "intr-elim.ML"; |
|
63 |
use "indrule.ML"; |
|
64 |
use "inductive.ML"; |
|
65 |
use "co-inductive.ML"; |
|
66 |
||
67 |
use_thy "perm"; |
|
68 |
use_thy "trancl"; |
|
69 |
use_thy "wf"; |
|
70 |
use_thy "ordinal"; |
|
71 |
use_thy "nat"; |
|
72 |
use_thy "epsilon"; |
|
73 |
use_thy "arith"; |
|
74 |
||
75 |
(*Datatype/co-datatype definitions*) |
|
76 |
use_thy "univ"; |
|
77 |
use_thy "quniv"; |
|
78 |
use "constructor.ML"; |
|
79 |
use "datatype.ML"; |
|
80 |
||
81 |
use "fin.ML"; |
|
82 |
use "list.ML"; |
|
83 |
use_thy "list-fn"; |
|
84 |
||
85 |
(*printing functions are inherited from FOL*) |
|
86 |
print_depth 8; |
|
87 |
||
88 |
val ZF_build_completed = (); (*indicate successful build*) |