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