src/ZF/ROOT.ML
 author paulson Fri Jan 03 15:01:55 1997 +0100 (1997-01-03) changeset 2469 b50b8c0eec01 parent 1512 ce37c64244c0 child 4262 e4113a682883 permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
 clasohm@1461 ` 1` ```(* Title: ZF/ROOT ``` lcp@6 ` 2` ``` ID: \$Id\$ ``` clasohm@1461 ` 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` paulson@2469 ` 14` ```eta_contract:=false; ``` paulson@2469 ` 15` lcp@14 ` 16` ```(*For Pure/tactic?? A crude way of adding structure to rules*) ``` paulson@1512 ` 17` ```fun CHECK_SOLVED tac st = ``` paulson@1512 ` 18` ``` case Sequence.pull (tac st) of ``` clasohm@1461 ` 19` ``` None => error"DO_GOAL: tactic list failed" ``` lcp@5 ` 20` ``` | Some(x,_) => ``` clasohm@1461 ` 21` ``` if has_fewer_prems 1 x then ``` clasohm@1461 ` 22` ``` Sequence.cons(x, Sequence.null) ``` clasohm@1461 ` 23` ``` else (writeln"DO_GOAL: unsolved goals!!"; ``` clasohm@1461 ` 24` ``` writeln"Final proof state was ..."; ``` clasohm@1461 ` 25` ``` print_goals (!goals_limit) x; ``` paulson@1512 ` 26` ``` raise ERROR); ``` lcp@5 ` 27` lcp@5 ` 28` ```fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs)); ``` lcp@5 ` 29` clasohm@0 ` 30` ```print_depth 1; ``` clasohm@0 ` 31` lcp@516 ` 32` ```(*Add user sections for inductive/datatype definitions*) ``` lcp@578 ` 33` ```use "../Pure/section_utils.ML"; ``` lcp@803 ` 34` ```use "thy_syntax.ML"; ``` lcp@516 ` 35` lcp@1069 ` 36` ```use_thy "Let"; ``` paulson@2469 ` 37` ```use_thy "func"; ``` paulson@2469 ` 38` ```use "typechk.ML"; ``` lcp@488 ` 39` ```use_thy "InfDatatype"; ``` lcp@516 ` 40` ```use_thy "List"; ``` lcp@532 ` 41` ```use_thy "EquivClass"; ``` clasohm@0 ` 42` clasohm@0 ` 43` ```(*printing functions are inherited from FOL*) ``` clasohm@0 ` 44` ```print_depth 8; ``` clasohm@0 ` 45` clasohm@1461 ` 46` ```val ZF_build_completed = (); (*indicate successful build*) ```