# HG changeset patch
# User oheimb
# Date 936634741 -7200
# Node ID 93ae11d887ffd95eb46bfc536cd3eeb8efe9cad7
# Parent  affcfd2830b7b87b4562e47f440a4bf09e878fbe
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD

diff -r affcfd2830b7 -r 93ae11d887ff src/HOL/Set.ML
--- 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";