src/ZF/ROOT.ML
author lcp
Thu, 25 Aug 1994 12:09:21 +0200
changeset 578 efc648d29dd0
parent 532 851df239ac8b
child 803 4c8333ab3eae
permissions -rw-r--r--
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/ROOT
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 5
diff changeset
     2
    ID:         $Id$
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val banner = "ZF Set Theory (in FOL)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    14
(*For Pure/tactic??  A crude way of adding structure to rules*)
5
75e163863e16 test commit
lcp
parents: 0
diff changeset
    15
fun CHECK_SOLVED (Tactic tf) = 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    16
  Tactic (fn state => 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    17
    case Sequence.pull (tf state) of
75e163863e16 test commit
lcp
parents: 0
diff changeset
    18
	None => error"DO_GOAL: tactic list failed"
75e163863e16 test commit
lcp
parents: 0
diff changeset
    19
      | Some(x,_) => 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    20
		if has_fewer_prems 1 x then
75e163863e16 test commit
lcp
parents: 0
diff changeset
    21
		    Sequence.cons(x, Sequence.null)
75e163863e16 test commit
lcp
parents: 0
diff changeset
    22
		else (writeln"DO_GOAL: unsolved goals!!";
75e163863e16 test commit
lcp
parents: 0
diff changeset
    23
		      writeln"Final proof state was ...";
75e163863e16 test commit
lcp
parents: 0
diff changeset
    24
		      print_goals (!goals_limit) x;
75e163863e16 test commit
lcp
parents: 0
diff changeset
    25
		      raise ERROR));
75e163863e16 test commit
lcp
parents: 0
diff changeset
    26
75e163863e16 test commit
lcp
parents: 0
diff changeset
    27
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
75e163863e16 test commit
lcp
parents: 0
diff changeset
    28
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
print_depth 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    31
(*Add user sections for inductive/datatype definitions*)
578
efc648d29dd0 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents: 532
diff changeset
    32
use     "../Pure/section_utils.ML";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    33
use_thy "Datatype";
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    34
structure ThySyn = ThySynFun
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    35
 (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    36
		       "and", "|", "<=", "domains", "intrs", "monos", 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    37
		       "con_defs", "type_intrs", "type_elims"] 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    38
  and user_sections = [("inductive",  inductive_decl ""),
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    39
		       ("coinductive",  inductive_decl "Co"),
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    40
		       ("datatype",  datatype_decl ""),
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    41
		       ("codatatype",  datatype_decl "Co")]);
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    42
init_thy_reader ();
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    43
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
    44
use_thy "InfDatatype";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
    45
use_thy "List";
532
851df239ac8b ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp
parents: 516
diff changeset
    46
use_thy "EquivClass";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
(*printing functions are inherited from FOL*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
print_depth 8;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val ZF_build_completed = ();	(*indicate successful build*)