0

1 
(* Title: ZF/ROOT


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1993 University of Cambridge


4 


5 
Adds ZermeloFraenkel Set Theory to a database containing FirstOrder 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 

5

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 

0

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/coinductive definitions*)


60 
use "indsyntax.ML";


61 
use "intrelim.ML";


62 
use "indrule.ML";


63 
use "inductive.ML";


64 
use "coinductive.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/codatatype 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 "listfn";


83 


84 
(*printing functions are inherited from FOL*)


85 
print_depth 8;


86 


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