src/ZF/ROOT.ML
author lcp
Fri Sep 17 12:53:53 1993 +0200 (1993-09-17)
changeset 5 75e163863e16
parent 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
test commit
     1 (*  Title: 	ZF/ROOT
     2     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
     6 
     7 This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
     8 *)
     9 
    10 val banner = "ZF Set Theory (in FOL)";
    11 writeln banner;
    12 
    13 (*For Pure/drule??  Multiple resolution infixes*)
    14 infix 0 MRS MRL;
    15 
    16 (*Resolve a list of rules against bottom_rl from right to left*)
    17 fun rls MRS bottom_rl = 
    18   let fun rs_aux i [] = bottom_rl
    19 	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
    20   in  rs_aux 1 rls  end;
    21 
    22 fun rlss MRL bottom_rls = 
    23   let fun rs_aux i [] = bottom_rls
    24 	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
    25   in  rs_aux 1 rlss  end;
    26 
    27 fun CHECK_SOLVED (Tactic tf) = 
    28   Tactic (fn state => 
    29     case Sequence.pull (tf state) of
    30 	None => error"DO_GOAL: tactic list failed"
    31       | Some(x,_) => 
    32 		if has_fewer_prems 1 x then
    33 		    Sequence.cons(x, Sequence.null)
    34 		else (writeln"DO_GOAL: unsolved goals!!";
    35 		      writeln"Final proof state was ...";
    36 		      print_goals (!goals_limit) x;
    37 		      raise ERROR));
    38 
    39 fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
    40 
    41 print_depth 1;
    42 use_thy "zf";
    43 
    44 use     "upair.ML";
    45 use     "subset.ML";
    46 use     "pair.ML";
    47 use     "domrange.ML";
    48 use     "func.ML";
    49 use     "equalities.ML";
    50 use     "simpdata.ML";  
    51 
    52 (*further development*)
    53 use_thy "bool";
    54 use_thy "sum";
    55 use_thy "qpair";
    56 use     "mono.ML";
    57 use_thy "fixedpt";
    58 
    59 (*Inductive/co-inductive definitions*)
    60 use     "ind-syntax.ML";
    61 use     "intr-elim.ML";
    62 use     "indrule.ML";
    63 use     "inductive.ML";
    64 use     "co-inductive.ML";
    65 
    66 use_thy "perm";
    67 use_thy "trancl";
    68 use_thy "wf";
    69 use_thy "ordinal";
    70 use_thy "nat";
    71 use_thy "epsilon";
    72 use_thy "arith";
    73 
    74 (*Datatype/co-datatype definitions*)
    75 use_thy "univ";
    76 use_thy "quniv";
    77 use     "constructor.ML";
    78 use     "datatype.ML";
    79 
    80 use     "fin.ML";
    81 use     "list.ML";
    82 use_thy "list-fn";
    83 
    84 (*printing functions are inherited from FOL*)
    85 print_depth 8;
    86 
    87 val ZF_build_completed = ();	(*indicate successful build*)