# HG changeset patch
# User paulson
# Date 910605587 -3600
# Node ID 829cae93f13240a8c42704e316f18f05e82a4bc5
# Parent  bacf85370ce0843aa213ed27eda1c537fbc775d9
new TIMES/Sigma rules

diff -r bacf85370ce0 -r 829cae93f132 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Mon Nov 09 10:58:49 1998 +0100
+++ b/src/HOL/Prod.ML	Mon Nov 09 10:59:47 1998 +0100
@@ -3,11 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-For prod.thy.  Ordered Pairs, the Cartesian product type, the unit type
+Ordered Pairs, the Cartesian product type, the unit type
 *)
 
-open Prod;
-
 (*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
 Goalw [Prod_def] "Pair_Rep a b : Prod";
 by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
@@ -363,6 +361,9 @@
 qed "mem_Sigma_iff";
 AddIffs [mem_Sigma_iff]; 
 
+
+(*** Complex rules for Sigma ***)
+
 val Collect_split = prove_goal Prod.thy 
 	"{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
 Addsimps [Collect_split];
@@ -373,6 +374,42 @@
 qed "UNION_Times_distrib";
 
 
+Goal "(ALL z: A Times B. P z) = (ALL x:A. ALL y: B. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Ball_Times";
+Addsimps [split_paired_Ball_Times];
+
+Goal "(EX z: A Times B. P z) = (EX x:A. EX y: B. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Bex_Times";
+Addsimps [split_paired_Bex_Times];
+
+
+Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib1";
+
+Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib2";
+
+Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib1";
+
+Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib2";
+
+Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib1";
+
+Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib2";
+
+
 (** Exhaustion rule for unit -- a degenerate form of induction **)
 
 Goalw [Unity_def]
@@ -446,3 +483,5 @@
                     |> standard;
 
 end;
+
+