equal
deleted
inserted
replaced
336 |
336 |
337 abbreviation sum_map' |
337 abbreviation sum_map' |
338 where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" |
338 where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" |
339 |
339 |
340 lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" |
340 lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" |
341 by (simp add: ID_def cfun_eq_iff sum_map.identity) |
341 by (simp add: ID_def cfun_eq_iff sum_map.identity id_def) |
342 |
342 |
343 lemma deflation_sum_map [domain_deflation]: |
343 lemma deflation_sum_map [domain_deflation]: |
344 "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)" |
344 "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)" |
345 apply default |
345 apply default |
346 apply (induct_tac x, simp_all add: deflation.idem) |
346 apply (induct_tac x, simp_all add: deflation.idem) |