# HG changeset patch
# User berghofe
# Date 1056914848 -7200
# Node ID 9a50427d7165814805ac2f98a9b4cfdbff16d996
# Parent  1c22e5499eeba9d8124242d0f59bf206fdd5b5b4
Added split_paired_All rule for splitting variables bound by
object-level universal quantifiers.

diff -r 1c22e5499eeb -r 9a50427d7165 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sun Jun 29 21:25:34 2003 +0200
+++ b/src/HOL/Record.thy	Sun Jun 29 21:27:28 2003 +0200
@@ -61,6 +61,22 @@
   thus "PROP P x" by (simp only: surjective_pairing [symmetric])
 qed
 
+lemma (in product_type) split_paired_All:
+  "(ALL x. P x) = (ALL a b. P (pair a b))"
+proof
+  fix a b
+  assume "ALL x. P x"
+  thus "ALL a b. P (pair a b)" by rules
+next
+  assume P: "ALL a b. P (pair a b)"
+  show "ALL x. P x"
+  proof
+    fix x
+    from P have "P (pair (dest1 x) (dest2 x))" by rules
+    thus "P x" by (simp only: surjective_pairing [symmetric])
+  qed
+qed
+
 
 subsection {* Concrete record syntax *}