src/HOL/List.thy
 changeset 35510 64d2d54cbf03 parent 35296 975b34b6cf5b child 35603 c0db094d0d80
equal inserted replaced
35509:13e83ce8391b 35510:64d2d54cbf03
`   759 lemma ex_map_conv:`
`   759 lemma ex_map_conv:`
`   760   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"`
`   760   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"`
`   761 by(induct ys, auto simp add: Cons_eq_map_conv)`
`   761 by(induct ys, auto simp add: Cons_eq_map_conv)`
`   762 `
`   762 `
`   763 lemma map_eq_imp_length_eq:`
`   763 lemma map_eq_imp_length_eq:`
`   764   assumes "map f xs = map f ys"`
`   764   assumes "map f xs = map g ys"`
`   765   shows "length xs = length ys"`
`   765   shows "length xs = length ys"`
`   766 using assms proof (induct ys arbitrary: xs)`
`   766 using assms proof (induct ys arbitrary: xs)`
`   767   case Nil then show ?case by simp`
`   767   case Nil then show ?case by simp`
`   768 next`
`   768 next`
`   769   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto`
`   769   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto`
`   770   from Cons xs have "map f zs = map f ys" by simp`
`   770   from Cons xs have "map f zs = map g ys" by simp`
`   771   moreover with Cons have "length zs = length ys" by blast`
`   771   moreover with Cons have "length zs = length ys" by blast`
`   772   with xs show ?case by simp`
`   772   with xs show ?case by simp`
`   773 qed`
`   773 qed`
`   774   `
`   774   `
`   775 lemma map_inj_on:`
`   775 lemma map_inj_on:`