author huffman Mon, 20 Dec 2010 09:48:16 -0800 changeset 41323 ae1c227534f5 parent 41322 43a5b9a0ee8a child 41324 1383653efec3
simplify proofs
```--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Mon Dec 20 09:41:55 2010 -0800
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Mon Dec 20 09:48:16 2010 -0800
@@ -139,7 +139,7 @@
where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"

lemma list_map_ID [domain_map_ID]: "list_map ID = ID"
-by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2)

lemma deflation_list_map [domain_deflation]:
"deflation d \<Longrightarrow> deflation (list_map d)"```
```--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Mon Dec 20 09:41:55 2010 -0800
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Mon Dec 20 09:48:16 2010 -0800
@@ -338,7 +338,7 @@
where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"

lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID"
-by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2 sum_map.identity)
+by (simp add: ID_def cfun_eq_iff sum_map.identity)

lemma deflation_sum_map [domain_deflation]:
"\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"```