src/HOL/Product_Type.thy
changeset 14337 e13731554e50
parent 14208 144f45277d5a
child 14359 3d9948163018
equal deleted inserted replaced
14336:8f731d3cd65b 14337:e13731554e50
   482 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   482 lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   483   -- {* Allows simplifications of nested splits in case of independent predicates. *}
   483   -- {* Allows simplifications of nested splits in case of independent predicates. *}
   484   apply (rule ext, blast)
   484   apply (rule ext, blast)
   485   done
   485   done
   486 
   486 
   487 lemma split_comp_eq [simp]: 
   487 (* Do NOT make this a simp rule as it
       
   488    a) only helps in special situations
       
   489    b) can lead to nontermination in the presence of split_def
       
   490 *)
       
   491 lemma split_comp_eq: 
   488 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   492 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
   489 by (rule ext, auto)
   493 by (rule ext, auto)
   490 
   494 
   491 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   495 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   492   by blast
   496   by blast