src/ZF/ROOT.ML
 author clasohm Thu Nov 04 14:11:59 1993 +0100 (1993-11-04) changeset 90 a90653dabebc parent 75 144ec40f2650 child 120 09287f26bfb8 permissions -rw-r--r--
renamed some files
 clasohm@0 1 (* Title: ZF/ROOT lcp@6 2 ID: \$Id\$ clasohm@0 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0 4 Copyright 1993 University of Cambridge clasohm@0 5 clasohm@0 6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic. clasohm@0 7 clasohm@0 8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. clasohm@0 9 *) clasohm@0 10 clasohm@0 11 val banner = "ZF Set Theory (in FOL)"; clasohm@0 12 writeln banner; clasohm@0 13 clasohm@75 14 set_loadpath [".", "ex", "../FOL"]; clasohm@75 15 lcp@14 16 (*For Pure/tactic?? A crude way of adding structure to rules*) lcp@5 17 fun CHECK_SOLVED (Tactic tf) = lcp@5 18 Tactic (fn state => lcp@5 19 case Sequence.pull (tf state) of lcp@5 20 None => error"DO_GOAL: tactic list failed" lcp@5 21 | Some(x,_) => lcp@5 22 if has_fewer_prems 1 x then lcp@5 23 Sequence.cons(x, Sequence.null) lcp@5 24 else (writeln"DO_GOAL: unsolved goals!!"; lcp@5 25 writeln"Final proof state was ..."; lcp@5 26 print_goals (!goals_limit) x; lcp@5 27 raise ERROR)); lcp@5 28 lcp@5 29 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); lcp@5 30 clasohm@0 31 print_depth 1; clasohm@0 32 use_thy "zf"; clasohm@0 33 clasohm@0 34 use "upair.ML"; clasohm@0 35 use "subset.ML"; clasohm@0 36 use "pair.ML"; clasohm@0 37 use "domrange.ML"; clasohm@0 38 use "func.ML"; clasohm@0 39 use "equalities.ML"; clasohm@0 40 use "simpdata.ML"; clasohm@0 41 clasohm@0 42 (*further development*) clasohm@0 43 use_thy "bool"; clasohm@0 44 use_thy "sum"; clasohm@0 45 use_thy "qpair"; clasohm@0 46 use "mono.ML"; clasohm@0 47 use_thy "fixedpt"; clasohm@0 48 clasohm@0 49 (*Inductive/co-inductive definitions*) clasohm@90 50 use "ind_syntax.ML"; clasohm@90 51 use "intr_elim.ML"; clasohm@0 52 use "indrule.ML"; clasohm@0 53 use "inductive.ML"; clasohm@90 54 use "coinductive.ML"; clasohm@0 55 clasohm@0 56 use_thy "perm"; clasohm@0 57 use_thy "trancl"; clasohm@0 58 use_thy "wf"; clasohm@50 59 use_thy "ord"; clasohm@0 60 use_thy "nat"; clasohm@0 61 use_thy "epsilon"; clasohm@0 62 use_thy "arith"; clasohm@0 63 clasohm@0 64 (*Datatype/co-datatype definitions*) clasohm@0 65 use_thy "univ"; clasohm@0 66 use_thy "quniv"; clasohm@0 67 use "constructor.ML"; clasohm@0 68 use "datatype.ML"; clasohm@0 69 clasohm@0 70 use "fin.ML"; clasohm@75 71 use_thy "List"; clasohm@32 72 use_thy "listfn"; clasohm@0 73 clasohm@0 74 (*printing functions are inherited from FOL*) clasohm@0 75 print_depth 8; clasohm@0 76 clasohm@0 77 val ZF_build_completed = (); (*indicate successful build*)