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`