Added insert_disjoint and disjoint_insert [simp], and simplified proofs
authornipkow
Mon May 06 09:42:20 2002 +0200 (2002-05-06)
changeset 1310366659a4b16f6
parent 13102 b6f8aae5f152
child 13104 df7aac8543c9
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Sat May 04 15:47:21 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon May 06 09:42:20 2002 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  header {* \section{Examples} *}
     1.6  
     1.7  theory RG_Examples = RG_Syntax:
     1.8 @@ -340,12 +339,7 @@
     1.9         apply simp+
    1.10       apply(erule_tac x=j in allE)
    1.11       apply force
    1.12 -    apply simp
    1.13 -    apply clarify
    1.14 -    apply(rule conjI)
    1.15 -     apply clarify  
    1.16 -     apply simp
    1.17 -     apply(erule not_sym)
    1.18 +    apply clarsimp
    1.19      apply force
    1.20  apply force+
    1.21  done
     2.1 --- a/src/HOL/Set.thy	Sat May 04 15:47:21 2002 +0200
     2.2 +++ b/src/HOL/Set.thy	Mon May 06 09:42:20 2002 +0200
     2.3 @@ -1049,6 +1049,13 @@
     2.4  lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
     2.5    by blast
     2.6  
     2.7 +lemma insert_disjoint[simp]:
     2.8 + "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
     2.9 +by blast
    2.10 +
    2.11 +lemma disjoint_insert[simp]:
    2.12 + "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
    2.13 +by blast
    2.14  
    2.15  text {* \medskip @{text image}. *}
    2.16