author  lcp 
Thu, 30 Sep 1993 10:10:21 +0100  
changeset 14  1c0926788772 
parent 6  8ce8c4d13d4d 
child 32  a8f1cdbbc5b8 
permissions  rwrr 
0  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  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4 
Copyright 1993 University of Cambridge 

5 

6 
Adds ZermeloFraenkel Set Theory to a database containing FirstOrder Logic. 

7 

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

9 
*) 

10 

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

12 
writeln banner; 

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  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)); 

26 

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

28 

0  29 
print_depth 1; 
30 
use_thy "zf"; 

31 

32 
use "upair.ML"; 

33 
use "subset.ML"; 

34 
use "pair.ML"; 

35 
use "domrange.ML"; 

36 
use "func.ML"; 

37 
use "equalities.ML"; 

38 
use "simpdata.ML"; 

39 

40 
(*further development*) 

41 
use_thy "bool"; 

42 
use_thy "sum"; 

43 
use_thy "qpair"; 

44 
use "mono.ML"; 

45 
use_thy "fixedpt"; 

46 

47 
(*Inductive/coinductive definitions*) 

48 
use "indsyntax.ML"; 

49 
use "intrelim.ML"; 

50 
use "indrule.ML"; 

51 
use "inductive.ML"; 

52 
use "coinductive.ML"; 

53 

54 
use_thy "perm"; 

55 
use_thy "trancl"; 

56 
use_thy "wf"; 

57 
use_thy "ordinal"; 

58 
use_thy "nat"; 

59 
use_thy "epsilon"; 

60 
use_thy "arith"; 

61 

62 
(*Datatype/codatatype definitions*) 

63 
use_thy "univ"; 

64 
use_thy "quniv"; 

65 
use "constructor.ML"; 

66 
use "datatype.ML"; 

67 

68 
use "fin.ML"; 

69 
use "list.ML"; 

70 
use_thy "listfn"; 

71 

72 
(*printing functions are inherited from FOL*) 

73 
print_depth 8; 

74 

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