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 