src/HOL/List.thy
changeset 50134 13211e07d931
parent 50027 7747a9f4c358
child 50422 ee729dbd1b7f
equal deleted inserted replaced
50133:5b43abaf8415 50134:13211e07d931
  4716 by auto
  4716 by auto
  4717 
  4717 
  4718 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  4718 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  4719 by auto
  4719 by auto
  4720 
  4720 
       
  4721 lemma lists_image: "lists (f`A) = map f ` lists A"
       
  4722 proof -
       
  4723   { fix xs have "\<forall>x\<in>set xs. x \<in> f ` A \<Longrightarrow> xs \<in> map f ` lists A"
       
  4724       by (induct xs) (auto simp del: map.simps simp add: map.simps[symmetric] intro!: imageI) }
       
  4725   then show ?thesis by auto
       
  4726 qed
  4721 
  4727 
  4722 subsubsection {* Inductive definition for membership *}
  4728 subsubsection {* Inductive definition for membership *}
  4723 
  4729 
  4724 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  4730 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  4725 where
  4731 where