# HG changeset patch
# User nipkow
# Date 1020670940 -7200
# Node ID 66659a4b16f6fff6550c389c7b22629fc9fa2f25
# Parent  b6f8aae5f152329e464fd069855c609fbd053c1a
Added insert_disjoint and disjoint_insert [simp], and simplified proofs

diff -r b6f8aae5f152 -r 66659a4b16f6 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Sat May 04 15:47:21 2002 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon May 06 09:42:20 2002 +0200
@@ -1,4 +1,3 @@
-
 header {* \section{Examples} *}
 
 theory RG_Examples = RG_Syntax:
@@ -340,12 +339,7 @@
        apply simp+
      apply(erule_tac x=j in allE)
      apply force
-    apply simp
-    apply clarify
-    apply(rule conjI)
-     apply clarify  
-     apply simp
-     apply(erule not_sym)
+    apply clarsimp
     apply force
 apply force+
 done
diff -r b6f8aae5f152 -r 66659a4b16f6 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat May 04 15:47:21 2002 +0200
+++ b/src/HOL/Set.thy	Mon May 06 09:42:20 2002 +0200
@@ -1049,6 +1049,13 @@
 lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
   by blast
 
+lemma insert_disjoint[simp]:
+ "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
+by blast
+
+lemma disjoint_insert[simp]:
+ "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
+by blast
 
 text {* \medskip @{text image}. *}