src/HOL/Product_Type.thy
 changeset 14337 e13731554e50 parent 14208 144f45277d5a child 14359 3d9948163018
equal 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