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.11    by (simp add: Ball_def)
    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