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