# HG changeset patch
# User huffman
# Date 1291154509 28800
# Node ID 10aeee1d5b711cb238bd614855bdbb9e76280e09
# Parent  158d18502378099ebba59788d1c2a3a77f73ca3e
add continuity lemma for List.map

diff -r 158d18502378 -r 10aeee1d5b71 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 14:01:25 2010 -0800
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Tue Nov 30 14:01:49 2010 -0800
@@ -233,6 +233,19 @@
     done
 qed
 
+text {* Continuity rule for map *}
+
+lemma cont2cont_map [simp, cont2cont]:
+  assumes f: "cont (\<lambda>(x, y). f x y)"
+  assumes g: "cont (\<lambda>x. g x)"
+  shows "cont (\<lambda>x. map (\<lambda>y. f x y) (g x))"
+using f
+apply (simp add: prod_cont_iff)
+apply (rule cont_apply [OF g])
+apply (rule list_contI, rule map.simps, simp, simp, simp)
+apply (induct_tac y, simp, simp)
+done
+
 text {* There are probably lots of other list operations that also
 deserve to have continuity lemmas.  I'll add more as they are
 needed. *}