author nipkow Mon May 06 09:42:20 2002 +0200 (2002-05-06) changeset 13103 66659a4b16f6 parent 13102 b6f8aae5f152 child 13104 df7aac8543c9
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
 src/HOL/HoareParallel/RG_Examples.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions
```     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.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
```