equal
deleted
inserted
replaced
|
1 (* Title: ZF/ROOT |
|
2 ID: $Id$ |
|
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 |
|
28 print_depth 1; |
|
29 use_thy "zf"; |
|
30 |
|
31 use "upair.ML"; |
|
32 use "subset.ML"; |
|
33 use "pair.ML"; |
|
34 use "domrange.ML"; |
|
35 use "func.ML"; |
|
36 use "equalities.ML"; |
|
37 use "simpdata.ML"; |
|
38 |
|
39 (*further development*) |
|
40 use_thy "bool"; |
|
41 use_thy "sum"; |
|
42 use_thy "qpair"; |
|
43 use "mono.ML"; |
|
44 use_thy "fixedpt"; |
|
45 |
|
46 (*Inductive/co-inductive definitions*) |
|
47 use "ind-syntax.ML"; |
|
48 use "intr-elim.ML"; |
|
49 use "indrule.ML"; |
|
50 use "inductive.ML"; |
|
51 use "co-inductive.ML"; |
|
52 |
|
53 use_thy "perm"; |
|
54 use_thy "trancl"; |
|
55 use_thy "wf"; |
|
56 use_thy "ordinal"; |
|
57 use_thy "nat"; |
|
58 use_thy "epsilon"; |
|
59 use_thy "arith"; |
|
60 |
|
61 (*Datatype/co-datatype definitions*) |
|
62 use_thy "univ"; |
|
63 use_thy "quniv"; |
|
64 use "constructor.ML"; |
|
65 use "datatype.ML"; |
|
66 |
|
67 use "fin.ML"; |
|
68 use "list.ML"; |
|
69 use_thy "list-fn"; |
|
70 |
|
71 (*printing functions are inherited from FOL*) |
|
72 print_depth 8; |
|
73 |
|
74 val ZF_build_completed = (); (*indicate successful build*) |