src/HOL/List.thy
changeset 45714 ad4242285560
parent 45607 16b4f5774621
child 45789 36ea69266e61
equal deleted inserted replaced
45713:badee348c5fb 45714:ad4242285560
   503     moreover with Cons.hyps have "P xs" .
   503     moreover with Cons.hyps have "P xs" .
   504     ultimately show ?thesis by (rule cons)
   504     ultimately show ?thesis by (rule cons)
   505   qed
   505   qed
   506 qed
   506 qed
   507 
   507 
       
   508 lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
       
   509   by (auto intro!: inj_onI)
   508 
   510 
   509 subsubsection {* @{const length} *}
   511 subsubsection {* @{const length} *}
   510 
   512 
   511 text {*
   513 text {*
   512   Needs to come before @{text "@"} because of theorem @{text
   514   Needs to come before @{text "@"} because of theorem @{text
  3707   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  3709   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  3708   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  3710   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  3709   thus ?case ..
  3711   thus ?case ..
  3710 qed
  3712 qed
  3711 
  3713 
  3712 lemma finite_lists_length_eq:
  3714 lemma lists_length_Suc_eq:
  3713 assumes "finite A"
  3715   "{xs. set xs \<subseteq> A \<and> length xs = Suc n} =
  3714 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
  3716     (\<lambda>(xs, n). n#xs) ` ({xs. set xs \<subseteq> A \<and> length xs = n} \<times> A)"
  3715 proof(induct n)
  3717   by (auto simp: length_Suc_conv)
  3716   case 0 show ?case by simp
  3718 
  3717 next
  3719 lemma
  3718   case (Suc n)
  3720   assumes "finite A"
  3719   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
  3721   shows finite_lists_length_eq: "finite {xs. set xs \<subseteq> A \<and> length xs = n}"
  3720     by (auto simp:length_Suc_conv)
  3722   and card_lists_length_eq: "card {xs. set xs \<subseteq> A \<and> length xs = n} = (card A)^n"
  3721   then show ?case using `finite A`
  3723   using `finite A`
  3722     by (auto intro: Suc) (* FIXME metis? *)
  3724   by (induct n)
  3723 qed
  3725      (auto simp: card_image inj_split_Cons lists_length_Suc_eq cong: conj_cong)
  3724 
  3726 
  3725 lemma finite_lists_length_le:
  3727 lemma finite_lists_length_le:
  3726   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  3728   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  3727  (is "finite ?S")
  3729  (is "finite ?S")
  3728 proof-
  3730 proof-
  3729   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3731   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3730   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
  3732   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
       
  3733 qed
       
  3734 
       
  3735 lemma card_lists_length_le:
       
  3736   assumes "finite A" shows "card {xs. set xs \<subseteq> A \<and> length xs \<le> n} = (\<Sum>i\<le>n. card A^i)"
       
  3737 proof -
       
  3738   have "(\<Sum>i\<le>n. card A^i) = card (\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i})"
       
  3739     using `finite A`
       
  3740     by (subst card_UN_disjoint)
       
  3741        (auto simp add: card_lists_length_eq finite_lists_length_eq)
       
  3742   also have "(\<Union>i\<le>n. {xs. set xs \<subseteq> A \<and> length xs = i}) = {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
       
  3743     by auto
       
  3744   finally show ?thesis by simp
  3731 qed
  3745 qed
  3732 
  3746 
  3733 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3747 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3734 apply(rule notI)
  3748 apply(rule notI)
  3735 apply(drule finite_maxlen)
  3749 apply(drule finite_maxlen)