New rewrites for bounded quantifiers
authorpaulson
Fri Jan 17 16:17:31 1997 +0100 (1997-01-17)
changeset 2519761e3094e32f
parent 2518 bee082efaa46
child 2520 aecaa76e7eff
New rewrites for bounded quantifiers
src/HOL/equalities.ML
     1.1 --- a/src/HOL/equalities.ML	Fri Jan 17 13:21:54 1997 +0100
     1.2 +++ b/src/HOL/equalities.ML	Fri Jan 17 16:17:31 1997 +0100
     1.3 @@ -458,13 +458,16 @@
     1.4  
     1.5  section"Bounded quantifiers";
     1.6  
     1.7 -goal Set.thy "(!x:insert a A.P x) = (P a & (!x:A.P x))";
     1.8 -by (Fast_tac 1);
     1.9 -qed "Ball_insert";
    1.10 +(** These are not added to the default simpset because (a) they duplicate the
    1.11 +    body and (b) there are no similar rules for Int. **)
    1.12  
    1.13 -goal Set.thy "(!x:A Un B.P x) = ((!x:A.P x) & (!x:B.P x))";
    1.14 +goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
    1.15  by (Fast_tac 1);
    1.16 -qed "Ball_Un";
    1.17 +qed "ball_Un";
    1.18 +
    1.19 +goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
    1.20 +by (Fast_tac 1);
    1.21 +qed "bex_Un";
    1.22  
    1.23  
    1.24  section "-";