equal
deleted
inserted
replaced
539 (* Do NOT make this a simp rule as it |
539 (* Do NOT make this a simp rule as it |
540 a) only helps in special situations |
540 a) only helps in special situations |
541 b) can lead to nontermination in the presence of split_def |
541 b) can lead to nontermination in the presence of split_def |
542 *) |
542 *) |
543 lemma split_comp_eq: |
543 lemma split_comp_eq: |
544 "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" |
544 fixes f :: "'a => 'b => 'c" and g :: "'d => 'a" |
|
545 shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" |
545 by (rule ext) auto |
546 by (rule ext) auto |
546 |
547 |
547 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)" |
548 lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)" |
548 by blast |
549 by blast |
549 |
550 |