908 qed "distinct_lemma"; |
908 qed "distinct_lemma"; |
909 |
909 |
910 |
910 |
911 (** Miniscoping: pushing in big Unions and Intersections **) |
911 (** Miniscoping: pushing in big Unions and Intersections **) |
912 local |
912 local |
913 fun prover s = prove_goal (the_context ()) s (fn _ => [Blast_tac 1]) |
913 fun prover s = prove_goal (the_context ()) s |
|
914 (fn _ => [Simp_tac 1, ALLGOALS Blast_tac]) |
914 in |
915 in |
915 val UN_simps = map prover |
916 val UN_simps = map prover |
916 ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)", |
917 ["(UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))", |
917 "!!C. c: C ==> (UN x:C. A x Un B) = ((UN x:C. A x) Un B)", |
918 "(UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))", |
918 "!!C. c: C ==> (UN x:C. A Un B x) = (A Un (UN x:C. B x))", |
919 "(UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))", |
919 "(UN x:C. A x Int B) = ((UN x:C. A x) Int B)", |
920 "(UN x:C. A x Int B) = ((UN x:C. A x) Int B)", |
920 "(UN x:C. A Int B x) = (A Int (UN x:C. B x))", |
921 "(UN x:C. A Int B x) = (A Int (UN x:C. B x))", |
921 "(UN x:C. A x - B) = ((UN x:C. A x) - B)", |
922 "(UN x:C. A x - B) = ((UN x:C. A x) - B)", |
922 "(UN x:C. A - B x) = (A - (INT x:C. B x))", |
923 "(UN x:C. A - B x) = (A - (INT x:C. B x))", |
923 "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)", |
924 "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)", |
924 "(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)", |
925 "(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)", |
925 "(UN x:f`A. B x) = (UN a:A. B(f a))"]; |
926 "(UN x:f`A. B x) = (UN a:A. B(f a))"]; |
926 |
927 |
927 val INT_simps = map prover |
928 val INT_simps = map prover |
928 ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)", |
929 ["(INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)", |
929 "!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))", |
930 "(INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))", |
930 "!!C. c: C ==> (INT x:C. A x - B) = ((INT x:C. A x) - B)", |
931 "(INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)", |
931 "!!C. c: C ==> (INT x:C. A - B x) = (A - (UN x:C. B x))", |
932 "(INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))", |
932 "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)", |
933 "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)", |
933 "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", |
934 "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)", |
934 "(INT x:C. A Un B x) = (A Un (INT x:C. B x))", |
935 "(INT x:C. A Un B x) = (A Un (INT x:C. B x))", |
935 "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)", |
936 "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)", |
936 "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)", |
937 "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)", |
937 "(INT x:f`A. B x) = (INT a:A. B(f a))"]; |
938 "(INT x:f`A. B x) = (INT a:A. B(f a))"]; |
938 |
939 |
939 |
940 |
940 val ball_simps = map prover |
941 val ball_simps = map prover |
941 ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)", |
942 ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)", |
942 "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))", |
943 "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))", |