equal
deleted
inserted
replaced
1002 by (induct xss) auto |
1002 by (induct xss) auto |
1003 |
1003 |
1004 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" |
1004 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" |
1005 by (induct xs) auto |
1005 by (induct xs) auto |
1006 |
1006 |
1007 lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs" |
1007 lemma concat_map_singleton[simp, code unfold]: "concat(map (%x. [f x]) xs) = map f xs" |
1008 by (induct xs) auto |
1008 by (induct xs) auto |
1009 |
1009 |
1010 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" |
1010 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" |
1011 by (induct xs) auto |
1011 by (induct xs) auto |
1012 |
1012 |