src/HOL/HOLCF/Library/Sum_Cpo.thy
changeset 41323 ae1c227534f5
parent 41321 4e72b6fc9dd4
child 41392 d1ff42a70f77
equal deleted inserted replaced
41322:43a5b9a0ee8a 41323:ae1c227534f5
   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 Abs_cfun_inverse2 sum_map.identity)
   341 by (simp add: ID_def cfun_eq_iff sum_map.identity)
   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)