src/ZF/ROOT.ML

Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.

(*  Title: 	ZF/ROOT
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.

This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
*)

val banner = "ZF Set Theory (in FOL)";
writeln banner;

(*For Pure/drule??  Multiple resolution infixes*)
infix 0 MRS MRL;

(*Resolve a list of rules against bottom_rl from right to left*)
fun rls MRS bottom_rl = 
  let fun rs_aux i [] = bottom_rl
	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
  in  rs_aux 1 rls  end;

fun rlss MRL bottom_rls = 
  let fun rs_aux i [] = bottom_rls
	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
  in  rs_aux 1 rlss  end;

fun CHECK_SOLVED (Tactic tf) = 
  Tactic (fn state => 
    case Sequence.pull (tf state) of
	None => error"DO_GOAL: tactic list failed"
      | Some(x,_) => 
		if has_fewer_prems 1 x then
		    Sequence.cons(x, Sequence.null)
		else (writeln"DO_GOAL: unsolved goals!!";
		      writeln"Final proof state was ...";
		      print_goals (!goals_limit) x;
		      raise ERROR));

fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));

print_depth 1;
use_thy "zf";

use     "upair.ML";
use     "subset.ML";
use     "pair.ML";
use     "domrange.ML";
use     "func.ML";
use     "equalities.ML";
use     "simpdata.ML";  

(*further development*)
use_thy "bool";
use_thy "sum";
use_thy "qpair";
use     "mono.ML";
use_thy "fixedpt";

(*Inductive/co-inductive definitions*)
use     "ind-syntax.ML";
use     "intr-elim.ML";
use     "indrule.ML";
use     "inductive.ML";
use     "co-inductive.ML";

use_thy "perm";
use_thy "trancl";
use_thy "wf";
use_thy "ordinal";
use_thy "nat";
use_thy "epsilon";
use_thy "arith";

(*Datatype/co-datatype definitions*)
use_thy "univ";
use_thy "quniv";
use     "constructor.ML";
use     "datatype.ML";

use     "fin.ML";
use     "list.ML";
use_thy "list-fn";

(*printing functions are inherited from FOL*)
print_depth 8;

val ZF_build_completed = ();	(*indicate successful build*)