src/ZF/ROOT.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 32 a8f1cdbbc5b8
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val banner = "ZF Set Theory (in FOL)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
writeln banner;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
75e163863e16 test commit
lcp
parents: 0
diff changeset
    15
fun CHECK_SOLVED (Tactic tf) = 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    16
  Tactic (fn state => 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    17
    case Sequence.pull (tf state) of
75e163863e16 test commit
lcp
parents: 0
diff changeset
    18
	None => error"DO_GOAL: tactic list failed"
75e163863e16 test commit
lcp
parents: 0
diff changeset
    19
      | Some(x,_) => 
75e163863e16 test commit
lcp
parents: 0
diff changeset
    20
		if has_fewer_prems 1 x then
75e163863e16 test commit
lcp
parents: 0
diff changeset
    21
		    Sequence.cons(x, Sequence.null)
75e163863e16 test commit
lcp
parents: 0
diff changeset
    22
		else (writeln"DO_GOAL: unsolved goals!!";
75e163863e16 test commit
lcp
parents: 0
diff changeset
    23
		      writeln"Final proof state was ...";
75e163863e16 test commit
lcp
parents: 0
diff changeset
    24
		      print_goals (!goals_limit) x;
75e163863e16 test commit
lcp
parents: 0
diff changeset
    25
		      raise ERROR));
75e163863e16 test commit
lcp
parents: 0
diff changeset
    26
75e163863e16 test commit
lcp
parents: 0
diff changeset
    27
fun DO_GOAL tfs = SELECT_GOAL (CHECK_SOLVED (EVERY1 tfs));
75e163863e16 test commit
lcp
parents: 0
diff changeset
    28
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
print_depth 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
use_thy "zf";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
use     "upair.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
use     "subset.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
use     "pair.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
use     "domrange.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
use     "func.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
use     "equalities.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
use     "simpdata.ML";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
(*further development*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
use_thy "bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
use_thy "sum";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
use_thy "qpair";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
use     "mono.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
use_thy "fixedpt";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*Inductive/co-inductive definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
use     "ind-syntax.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
use     "intr-elim.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
use     "indrule.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
use     "inductive.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
use     "co-inductive.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
use_thy "perm";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
use_thy "trancl";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
use_thy "wf";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
use_thy "ordinal";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
use_thy "nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
use_thy "epsilon";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
use_thy "arith";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
(*Datatype/co-datatype definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
use_thy "univ";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
use_thy "quniv";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
use     "constructor.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
use     "datatype.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
use     "fin.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
use     "list.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
use_thy "list-fn";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(*printing functions are inherited from FOL*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
print_depth 8;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val ZF_build_completed = ();	(*indicate successful build*)