Added split_paired_All rule for splitting variables bound by
authorberghofe
Sun Jun 29 21:27:28 2003 +0200 (2003-06-29)
changeset 140809a50427d7165
parent 14079 1c22e5499eeb
child 14081 6c0f67e2f8d5
Added split_paired_All rule for splitting variables bound by
object-level universal quantifiers.
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Sun Jun 29 21:25:34 2003 +0200
     1.2 +++ b/src/HOL/Record.thy	Sun Jun 29 21:27:28 2003 +0200
     1.3 @@ -61,6 +61,22 @@
     1.4    thus "PROP P x" by (simp only: surjective_pairing [symmetric])
     1.5  qed
     1.6  
     1.7 +lemma (in product_type) split_paired_All:
     1.8 +  "(ALL x. P x) = (ALL a b. P (pair a b))"
     1.9 +proof
    1.10 +  fix a b
    1.11 +  assume "ALL x. P x"
    1.12 +  thus "ALL a b. P (pair a b)" by rules
    1.13 +next
    1.14 +  assume P: "ALL a b. P (pair a b)"
    1.15 +  show "ALL x. P x"
    1.16 +  proof
    1.17 +    fix x
    1.18 +    from P have "P (pair (dest1 x) (dest2 x))" by rules
    1.19 +    thus "P x" by (simp only: surjective_pairing [symmetric])
    1.20 +  qed
    1.21 +qed
    1.22 +
    1.23  
    1.24  subsection {* Concrete record syntax *}
    1.25