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