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
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@516
    31
(*Add user sections for inductive/datatype definitions*)
lcp@516
    32
use_thy "Datatype";
lcp@516
    33
structure ThySyn = ThySynFun
lcp@516
    34
 (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
lcp@516
    35
		       "and", "|", "<=", "domains", "intrs", "monos", 
lcp@516
    36
		       "con_defs", "type_intrs", "type_elims"] 
lcp@516
    37
  and user_sections = [("inductive",  inductive_decl ""),
lcp@516
    38
		       ("coinductive",  inductive_decl "Co"),
lcp@516
    39
		       ("datatype",  datatype_decl ""),
lcp@516
    40
		       ("codatatype",  datatype_decl "Co")]);
lcp@516
    41
init_thy_reader ();
lcp@516
    42
lcp@488
    43
use_thy "InfDatatype";
lcp@516
    44
use_thy "List";
lcp@532
    45
use_thy "EquivClass";
clasohm@0
    46
clasohm@0
    47
(*printing functions are inherited from FOL*)
clasohm@0
    48
print_depth 8;
clasohm@0
    49
clasohm@0
    50
val ZF_build_completed = ();	(*indicate successful build*)