src/ZF/simpdata.ML
 changeset 14 1c0926788772 parent 6 8ce8c4d13d4d child 279 7738aed3f84d
```--- a/src/ZF/simpdata.ML	Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/simpdata.ML	Thu Sep 30 10:10:21 1993 +0100
@@ -10,15 +10,21 @@
(writeln s;  prove_goal ZF.thy s
(fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));

+(*INCLUDED IN ZF_ss*)
val mem_simps = map prove_fun
- [ "a:0 <-> False",
-   "a : A Un B <-> a:A | a:B",
-   "a : A Int B <-> a:A & a:B",
-   "a : A-B <-> a:A & ~a:B",
-   "a : cons(b,B) <-> a=b | a:B",
-   "i : succ(j) <-> i=j | i:j",
+ [ "a : 0             <-> False",
+   "a : A Un B        <-> a:A | a:B",
+   "a : A Int B       <-> a:A & a:B",
+   "a : A-B           <-> a:A & ~a:B",
"<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
-   "a : Collect(A,P) <-> a:A & P(a)" ];
+   "a : Collect(A,P)  <-> a:A & P(a)" ];
+
+(*INCLUDED: should be??*)
+val bquant_simps = map prove_fun
+ [ "(ALL x:0.P(x)) <-> True",
+   "(EX  x:0.P(x)) <-> False",
+   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
+   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];

(** Tactics for type checking -- from CTT **)

@@ -83,7 +89,7 @@
fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);

-val ZF_simps = [empty_subsetI, ball_simp, if_true, if_false,
+val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split];

(*Sigma_cong, Pi_cong NOT included by default since they cause
@@ -94,5 +100,5 @@

val ZF_ss = FOL_ss
setmksimps ZF_mk_rew_rules