equal
deleted
inserted
replaced
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 |