src/ZF/ROOT.ML
 author lcp Mon Nov 15 14:41:25 1993 +0100 (1993-11-15) changeset 120 09287f26bfb8 parent 90 a90653dabebc child 124 858ab9a9b047 permissions -rw-r--r--
changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs
 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` lcp@120 ` 49` ```(*Inductive/coinductive 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` lcp@120 ` 64` ```(*Datatype/codatatype 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*) ```