src/ZF/simpdata.ML
 changeset 1036 0d28f4bc8a44 parent 855 4c8d0ece1f95 child 1461 6bcb44e4d6e5
```--- a/src/ZF/simpdata.ML	Thu Apr 13 11:37:39 1995 +0200
+++ b/src/ZF/simpdata.ML	Thu Apr 13 11:38:48 1995 +0200
@@ -37,38 +37,39 @@

(*Should False yield False<->True, or should it solve goals some other way?*)

+(*Analyse a theorem to atomic rewrite rules*)
+fun atomize (conn_pairs, mem_pairs) th =
+  let fun tryrules pairs t =
+	      Const(a,_) =>
+		(case assoc(pairs,a) of
+		     Some rls => flat (map (atomize (conn_pairs, mem_pairs))
+				       ([th] RL rls))
+		   | None     => [th])
+	    | _ => [th]
+  in case concl_of th of
+	 Const("Trueprop",_) \$ P =>
+	    (case P of
+		 Const("op :",_) \$ a \$ b => tryrules mem_pairs b
+	       | Const("True",_)         => []
+	       | Const("False",_)        => []
+	       | A => tryrules conn_pairs A)
+       | _                       => [th]
+  end;
+
(*Analyse a rigid formula*)
-val atomize_pairs =
+val ZF_conn_pairs =
[("Ball",	[bspec]),
("All",	[spec]),
("op -->",	[mp]),
("op &",	[conjunct1,conjunct2])];

(*Analyse a:b, where b is rigid*)
-val atomize_mem_pairs =
+val ZF_mem_pairs =
[("Collect",	[CollectD1,CollectD2]),
("op -",	[DiffD1,DiffD2]),
("op Int",	[IntD1,IntD2])];

-(*Analyse a theorem to atomic rewrite rules*)
-fun atomize th =
-  let fun tryrules pairs t =
-	      Const(a,_) =>
-		(case assoc(pairs,a) of
-		     Some rls => flat (map atomize ([th] RL rls))
-		   | None     => [th])
-	    | _ => [th]
-  in case concl_of th of
-       Const("Trueprop",_) \$ P =>
-	  (case P of
-	       Const("op :",_) \$ a \$ b => tryrules atomize_mem_pairs b
-	     | Const("True",_)         => []
-	     | Const("False",_)        => []
-	     | A => tryrules atomize_pairs A)
-     | _                       => [th]
-  end;
-
val ZF_simps =
[empty_subsetI, consI1, succI1, ball_simp, if_true, if_false,
beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, singleton_iff,
@@ -80,8 +81,10 @@
val ZF_congs =
[ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];

+val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
+
val ZF_ss = FOL_ss
-      setmksimps (map mk_meta_eq o atomize o gen_all)
+      setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
addsimps (ZF_simps @ mem_simps @ bquant_simps @
Collect_simps @ UnInt_simps)