src/HOL/Word/Word.thy
changeset 54849 d325c7c4a4f7
parent 54848 a303daddebbf
child 54854 3324a0078636
equal deleted inserted replaced
54848:a303daddebbf 54849:d325c7c4a4f7
  4007 lemmas rotater_0 = rotater_eqs (1)
  4007 lemmas rotater_0 = rotater_eqs (1)
  4008 lemmas rotater_add = rotater_eqs (2)
  4008 lemmas rotater_add = rotater_eqs (2)
  4009 
  4009 
  4010 
  4010 
  4011 subsubsection "map, map2, commuting with rotate(r)"
  4011 subsubsection "map, map2, commuting with rotate(r)"
  4012 
       
  4013 lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
       
  4014   by (induct xs) auto
       
  4015 
  4012 
  4016 lemma butlast_map:
  4013 lemma butlast_map:
  4017   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  4014   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  4018   by (induct xs) auto
  4015   by (induct xs) auto
  4019 
  4016