--- a/src/HOL/Set.ML Mon Sep 06 18:18:49 1999 +0200
+++ b/src/HOL/Set.ML Mon Sep 06 18:19:01 1999 +0200
@@ -463,6 +463,14 @@
AddSIs [insertCI];
AddSEs [insertE];
+Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)";
+by (case_tac "x:A" 1);
+by (Fast_tac 2);
+br disjI2 1;
+by (res_inst_tac [("x","A-{x}")] exI 1);
+by (Fast_tac 1);
+qed "subset_insertD";
+
section "Singletons, using insert";
Goal "a : {a}";
@@ -488,6 +496,15 @@
AddSDs [singleton_inject];
AddSEs [singletonE];
+Goal "{b} = insert a A = (a = b & A <= {a})";
+by (safe_tac (claset() addSEs [equalityE]));
+by (ALLGOALS Blast_tac);
+qed "singleton_insert_inj_eq";
+
+Goal "A <= {x} ==> A={} | A = {x}";
+by (Fast_tac 1);
+qed "subset_singletonD";
+
Goal "{x. x=a} = {a}";
by (Blast_tac 1);
qed "singleton_conv";