map and prefix
authorkleing
Wed Nov 07 03:51:17 2007 +0100 (2007-11-07)
changeset 25322e2eac0c30ff5
parent 25321 e34b2265698a
child 25323 50d4c8257d06
map and prefix
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Tue Nov 06 22:50:39 2007 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Nov 07 03:51:17 2007 +0100
     1.3 @@ -162,6 +162,10 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 +lemma map_prefixI: 
     1.8 +  "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
     1.9 +  by (clarsimp simp: prefix_def)
    1.10 +
    1.11  lemma prefix_length_less:
    1.12    "xs < ys \<Longrightarrow> length xs < length ys"
    1.13    apply (clarsimp simp: strict_prefix_def)