src/ZF/ROOT.ML
 author lcp Tue Jun 21 17:20:34 1994 +0200 (1994-06-21) changeset 435 ca5356bd315a parent 364 6573122322d7 child 484 70b789956bd3 permissions -rw-r--r--
Addition of cardinals and order types, various tidying
 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` lcp@14 ` 14` ```(*For Pure/tactic?? A crude way of adding structure to rules*) ``` lcp@5 ` 15` ```fun CHECK_SOLVED (Tactic tf) = ``` lcp@5 ` 16` ``` Tactic (fn state => ``` lcp@5 ` 17` ``` case Sequence.pull (tf state) of ``` lcp@5 ` 18` ``` None => error"DO_GOAL: tactic list failed" ``` lcp@5 ` 19` ``` | Some(x,_) => ``` lcp@5 ` 20` ``` if has_fewer_prems 1 x then ``` lcp@5 ` 21` ``` Sequence.cons(x, Sequence.null) ``` lcp@5 ` 22` ``` else (writeln"DO_GOAL: unsolved goals!!"; ``` lcp@5 ` 23` ``` writeln"Final proof state was ..."; ``` lcp@5 ` 24` ``` print_goals (!goals_limit) x; ``` lcp@5 ` 25` ``` raise ERROR)); ``` lcp@5 ` 26` lcp@5 ` 27` ```fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); ``` lcp@5 ` 28` clasohm@0 ` 29` ```print_depth 1; ``` clasohm@0 ` 30` lcp@435 ` 31` ```use_thy "CardinalArith"; ``` lcp@364 ` 32` ```use_thy "Fin"; ``` clasohm@124 ` 33` ```use_thy "ListFn"; ``` clasohm@0 ` 34` clasohm@0 ` 35` ```(*printing functions are inherited from FOL*) ``` clasohm@0 ` 36` ```print_depth 8; ``` clasohm@0 ` 37` clasohm@0 ` 38` ```val ZF_build_completed = (); (*indicate successful build*) ```