src/ZF/ROOT.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 516 1957113f0d7d
child 578 efc648d29dd0
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ROOT
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
     7 
     8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
     9 *)
    10 
    11 val banner = "ZF Set Theory (in FOL)";
    12 writeln banner;
    13 
    14 (*For Pure/tactic??  A crude way of adding structure to rules*)
    15 fun CHECK_SOLVED (Tactic tf) = 
    16   Tactic (fn state => 
    17     case Sequence.pull (tf state) of
    18 	None => error"DO_GOAL: tactic list failed"
    19       | Some(x,_) => 
    20 		if has_fewer_prems 1 x then
    21 		    Sequence.cons(x, Sequence.null)
    22 		else (writeln"DO_GOAL: unsolved goals!!";
    23 		      writeln"Final proof state was ...";
    24 		      print_goals (!goals_limit) x;
    25 		      raise ERROR));
    26 
    27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    28 
    29 print_depth 1;
    30 
    31 (*Add user sections for inductive/datatype definitions*)
    32 use_thy "Datatype";
    33 structure ThySyn = ThySynFun
    34  (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
    35 		       "and", "|", "<=", "domains", "intrs", "monos", 
    36 		       "con_defs", "type_intrs", "type_elims"] 
    37   and user_sections = [("inductive",  inductive_decl ""),
    38 		       ("coinductive",  inductive_decl "Co"),
    39 		       ("datatype",  datatype_decl ""),
    40 		       ("codatatype",  datatype_decl "Co")]);
    41 init_thy_reader ();
    42 
    43 use_thy "InfDatatype";
    44 use_thy "List";
    45 use_thy "EquivClass";
    46 
    47 (*printing functions are inherited from FOL*)
    48 print_depth 8;
    49 
    50 val ZF_build_completed = ();	(*indicate successful build*)