--- a/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 09:45:26 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 07:50:47 2010 -0800
@@ -143,33 +143,23 @@
"LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
by (rule liftdefl_list_def)
-subsection {* Continuous map operation for lists *}
-
-definition
- list_map :: "('a::predomain \<rightarrow> 'b::predomain) \<rightarrow> 'a list \<rightarrow> 'b list"
-where
- "list_map = (\<Lambda> f xs. map (\<lambda>x. f\<cdot>x) xs)"
+subsection {* Configuring list type to work with domain package *}
-lemma list_map_simps [simp]:
- "list_map\<cdot>f\<cdot>[] = []"
- "list_map\<cdot>f\<cdot>(x # xs) = f\<cdot>x # list_map\<cdot>f\<cdot>xs"
-unfolding list_map_def by simp_all
+abbreviation list_map :: "('a::cpo \<rightarrow> 'b::cpo) \<Rightarrow> 'a list \<rightarrow> 'b list"
+ where "list_map f \<equiv> Abs_cfun (map (Rep_cfun f))"
-lemma list_map_ID [domain_map_ID]: "list_map\<cdot>ID = ID"
-unfolding list_map_def ID_def
-by (simp add: Abs_cfun_inverse cfun_def)
+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\<cdot>d)"
+ "deflation d \<Longrightarrow> deflation (list_map d)"
apply default
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done
-subsection {* Configuring list type to work with domain package *}
-
lemma encode_list_u_map:
- "encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
+ "encode_list_u\<cdot>(u_map\<cdot>(list_map f)\<cdot>(decode_list_u\<cdot>xs))
= slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
apply (induct xs, simp, simp)
apply (case_tac a, simp, rename_tac b)
@@ -180,7 +170,7 @@
lemma isodefl_list_u [domain_isodefl]:
fixes d :: "'a::predomain \<rightarrow> 'a"
assumes "isodefl' d t"
- shows "isodefl' (list_map\<cdot>d) (list_liftdefl\<cdot>t)"
+ shows "isodefl' (list_map d) (list_liftdefl\<cdot>t)"
using assms unfolding isodefl'_def liftemb_list_def liftprj_list_def
apply (simp add: list_liftdefl_def cast_udefl cast_slist_defl cast_u_defl)
apply (simp add: cfcomp1 encode_list_u_map)