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