# 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 (\(x, y). f x y)" + assumes g: "cont (\x. g x)" + shows "cont (\x. map (\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. *}