src/ZF/ROOT.ML
 author lcp Fri Aug 12 12:51:34 1994 +0200 (1994-08-12) changeset 516 1957113f0d7d parent 488 52f7447d4f1b child 532 851df239ac8b permissions -rw-r--r--
installation of new inductive/datatype sections
1 (*  Title: 	ZF/ROOT
2     ID:         \$Id\$
3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1993  University of Cambridge
6 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
8 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
9 *)
11 val banner = "ZF Set Theory (in FOL)";
12 writeln banner;
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));
27 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
29 print_depth 1;
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")]);