src/HOL/Product_Type.thy
changeset 11820 015a82d4ee96
parent 11777 b03c8a3fcc6d
child 11838 02d75712061d
--- a/src/HOL/Product_Type.thy	Wed Oct 17 18:52:30 2001 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 17 20:24:03 2001 +0200
@@ -115,6 +115,18 @@
 
 use "Product_Type_lemmas.ML"
 
+lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))"   (* FIXME unused *)
+proof
+  fix a b
+  assume "!!x. PROP P x"
+  thus "PROP P (a, b)" .
+next
+  fix x
+  assume "!!a b. PROP P (a, b)"
+  hence "PROP P (fst x, snd x)" .
+  thus "PROP P x" by simp
+qed
+
 lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   apply (rule_tac x = "(a, b)" in image_eqI)
    apply auto