src/HOL/List.thy
changeset 50134 13211e07d931
parent 50027 7747a9f4c358
child 50422 ee729dbd1b7f
     1.1 --- a/src/HOL/List.thy	Tue Nov 20 17:49:26 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Nov 20 18:59:35 2012 +0100
     1.3 @@ -4718,6 +4718,12 @@
     1.4  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
     1.5  by auto
     1.6  
     1.7 +lemma lists_image: "lists (f`A) = map f ` lists A"
     1.8 +proof -
     1.9 +  { fix xs have "\<forall>x\<in>set xs. x \<in> f ` A \<Longrightarrow> xs \<in> map f ` lists A"
    1.10 +      by (induct xs) (auto simp del: map.simps simp add: map.simps[symmetric] intro!: imageI) }
    1.11 +  then show ?thesis by auto
    1.12 +qed
    1.13  
    1.14  subsubsection {* Inductive definition for membership *}
    1.15