src/HOL/Set.thy
 changeset 16636 1ed737a98198 parent 15950 5c067c956a20 child 16773 33c4d8fe6f78
```     1.1 --- a/src/HOL/Set.thy	Fri Jul 01 13:56:34 2005 +0200
1.2 +++ b/src/HOL/Set.thy	Fri Jul 01 13:57:53 2005 +0200
1.3 @@ -444,16 +444,26 @@
1.4
1.5  subsubsection {* Congruence rules *}
1.6
1.7 -lemma ball_cong [cong]:
1.8 +lemma ball_cong:
1.9    "A = B ==> (!!x. x:B ==> P x = Q x) ==>
1.10      (ALL x:A. P x) = (ALL x:B. Q x)"
1.12
1.13 -lemma bex_cong [cong]:
1.14 +lemma strong_ball_cong [cong]:
1.15 +  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>
1.16 +    (ALL x:A. P x) = (ALL x:B. Q x)"
1.17 +  by (simp add: simp_implies_def Ball_def)
1.18 +
1.19 +lemma bex_cong:
1.20    "A = B ==> (!!x. x:B ==> P x = Q x) ==>
1.21      (EX x:A. P x) = (EX x:B. Q x)"
1.22    by (simp add: Bex_def cong: conj_cong)
1.23
1.24 +lemma strong_bex_cong [cong]:
1.25 +  "A = B ==> (!!x. x:B =simp=> P x = Q x) ==>
1.26 +    (EX x:A. P x) = (EX x:B. Q x)"
1.27 +  by (simp add: simp_implies_def Bex_def cong: conj_cong)
1.28 +
1.29
1.30  subsubsection {* Subsets *}
1.31
```