Added split_paired_All rule for splitting variables bound by
object-level universal quantifiers.
--- 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 *}