lemmas about card (set xs)
authorkleing
Mon Feb 16 03:25:52 2004 +0100 (2004-02-16)
changeset 1438804f04408b99b
parent 14387 e96d5c42c4b0
child 14389 57c2d90936ba
lemmas about card (set xs)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Feb 15 10:46:37 2004 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Feb 16 03:25:52 2004 +0100
     1.3 @@ -601,6 +601,8 @@
     1.4  apply (rule_tac x="x#l" in exI, auto)
     1.5  done
     1.6  
     1.7 +lemma card_length: "card (set xs) \<le> length xs"
     1.8 +by (induct xs) (auto simp add: card_insert_if)
     1.9  
    1.10  subsection {* @{text mem} *}
    1.11  
    1.12 @@ -1337,6 +1339,27 @@
    1.13  apply (erule_tac x = "Suc j" in allE, simp)
    1.14  done
    1.15  
    1.16 +lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
    1.17 +  by (induct xs) auto
    1.18 +
    1.19 +lemma card_distinct: "card (set xs) = size xs \<Longrightarrow> distinct xs"
    1.20 +proof (induct xs)
    1.21 +  case Nil thus ?case by simp
    1.22 +next
    1.23 +  case (Cons x xs)
    1.24 +  show ?case
    1.25 +  proof (cases "x \<in> set xs")
    1.26 +    case False with Cons show ?thesis by simp
    1.27 +  next
    1.28 +    case True with Cons.prems
    1.29 +    have "card (set xs) = Suc (length xs)" 
    1.30 +      by (simp add: card_insert_if split: split_if_asm)
    1.31 +    moreover have "card (set xs) \<le> length xs" by (rule card_length)
    1.32 +    ultimately have False by simp
    1.33 +    thus ?thesis ..
    1.34 +  qed
    1.35 +qed
    1.36 +
    1.37  
    1.38  subsection {* @{text replicate} *}
    1.39  
    1.40 @@ -1528,6 +1551,30 @@
    1.41                  nth_Cons'[of _ _ "number_of v",standard]
    1.42  
    1.43  
    1.44 +lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
    1.45 +  by (induct xs) auto
    1.46 +
    1.47 +lemma card_length: "card (set xs) \<le> length xs"
    1.48 +  by (induct xs) (auto simp add: card_insert_if)
    1.49 +
    1.50 +lemma "card (set xs) = size xs \<Longrightarrow> distinct xs"
    1.51 +proof (induct xs)
    1.52 +  case Nil thus ?case by simp
    1.53 +next
    1.54 +  case (Cons x xs)
    1.55 +  show ?case
    1.56 +  proof (cases "x \<in> set xs")
    1.57 +    case False with Cons show ?thesis by simp
    1.58 +  next
    1.59 +    case True with Cons.prems
    1.60 +    have "card (set xs) = Suc (length xs)" 
    1.61 +      by (simp add: card_insert_if split: split_if_asm)
    1.62 +    moreover have "card (set xs) \<le> length xs" by (rule card_length)
    1.63 +    ultimately have False by simp
    1.64 +    thus ?thesis ..
    1.65 +  qed
    1.66 +qed
    1.67 +
    1.68  subsection {* Characters and strings *}
    1.69  
    1.70  datatype nibble =