src/HOL/Product_Type.thy
changeset 11820 015a82d4ee96
parent 11777 b03c8a3fcc6d
child 11838 02d75712061d
     1.1 --- a/src/HOL/Product_Type.thy	Wed Oct 17 18:52:30 2001 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 17 20:24:03 2001 +0200
     1.3 @@ -115,6 +115,18 @@
     1.4  
     1.5  use "Product_Type_lemmas.ML"
     1.6  
     1.7 +lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))"   (* FIXME unused *)
     1.8 +proof
     1.9 +  fix a b
    1.10 +  assume "!!x. PROP P x"
    1.11 +  thus "PROP P (a, b)" .
    1.12 +next
    1.13 +  fix x
    1.14 +  assume "!!a b. PROP P (a, b)"
    1.15 +  hence "PROP P (fst x, snd x)" .
    1.16 +  thus "PROP P x" by simp
    1.17 +qed
    1.18 +
    1.19  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
    1.20    apply (rule_tac x = "(a, b)" in image_eqI)
    1.21     apply auto