src/HOL/Product_Type.thy
changeset 15481 fc075ae929e4
parent 15422 cbdddc0efadf
child 15531 08c8dad8e399
equal deleted inserted replaced
15480:cb3612cc41a3 15481:fc075ae929e4
   449 lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   449 lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   450   by (subst surjective_pairing, rule split_conv)
   450   by (subst surjective_pairing, rule split_conv)
   451 
   451 
   452 lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   452 lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   453   -- {* For use with @{text split} and the Simplifier. *}
   453   -- {* For use with @{text split} and the Simplifier. *}
   454   apply (subst surjective_pairing)
   454   by (insert surj_pair [of p], clarify, simp)
   455   apply (subst split_conv, blast)
       
   456   done
       
   457 
   455 
   458 text {*
   456 text {*
   459   @{thm [source] split_split} could be declared as @{text "[split]"}
   457   @{thm [source] split_split} could be declared as @{text "[split]"}
   460   done after the Splitter has been speeded up significantly;
   458   done after the Splitter has been speeded up significantly;
   461   precompute the constants involved and don't do anything unless the
   459   precompute the constants involved and don't do anything unless the