src/HOL/Library/Cardinality.thy
changeset 51116 0dac0158b8d4
parent 49948 744934b818c7
child 51139 c8e3cf3520b3
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu Feb 14 12:24:56 2013 +0100
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Feb 14 16:01:28 2013 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4  subsection {* A type class for computing the cardinality of types *}
     1.5  
     1.6  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
     1.7 -where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     1.8 +where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     1.9  
    1.10  lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    1.11  by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    1.12 @@ -211,15 +211,6 @@
    1.13    fixes card_UNIV :: "'a card_UNIV"
    1.14    assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
    1.15  
    1.16 -lemma card_UNIV_code [code_unfold]: 
    1.17 -  "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"
    1.18 -by(simp add: card_UNIV)
    1.19 -
    1.20 -lemma is_list_UNIV_code [code]:
    1.21 -  "is_list_UNIV (xs :: 'a list) = 
    1.22 -  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
    1.23 -by(rule is_list_UNIV_def)
    1.24 -
    1.25  subsection {* Instantiations for @{text "card_UNIV"} *}
    1.26  
    1.27  instantiation nat :: card_UNIV begin
    1.28 @@ -396,80 +387,66 @@
    1.29  
    1.30  subsection {* Code setup for sets *}
    1.31  
    1.32 +text {*
    1.33 +  Implement operations @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, and @{term "op ="} 
    1.34 +  for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}.
    1.35 +*}
    1.36 +
    1.37  lemma card_Compl:
    1.38    "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
    1.39  by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
    1.40  
    1.41 -context fixes xs :: "'a :: card_UNIV list"
    1.42 -begin
    1.43 +lemma card_coset_code [code]:
    1.44 +  fixes xs :: "'a :: card_UNIV list" 
    1.45 +  shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    1.46 +by(simp add: List.card_set card_Compl card_UNIV)
    1.47  
    1.48 -definition card' :: "'a set \<Rightarrow> nat" 
    1.49 -where [simp, code del, code_abbrev]: "card' = card"
    1.50 -
    1.51 -lemma card'_code [code]:
    1.52 -  "card' (set xs) = length (remdups xs)"
    1.53 -  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    1.54 -by(simp_all add: List.card_set card_Compl card_UNIV)
    1.55 +lemma [code, code del]: "finite = finite" ..
    1.56  
    1.57 -lemma card'_UNIV [code_unfold]: 
    1.58 -  "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)"
    1.59 -by(simp add: card_UNIV)
    1.60 -
    1.61 -definition finite' :: "'a set \<Rightarrow> bool"
    1.62 -where [simp, code del, code_abbrev]: "finite' = finite"
    1.63 -
    1.64 -lemma finite'_code [code]:
    1.65 -  "finite' (set xs) \<longleftrightarrow> True"
    1.66 -  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.67 +lemma [code]:
    1.68 +  fixes xs :: "'a :: card_UNIV list" 
    1.69 +  shows finite_set_code:
    1.70 +  "finite (set xs) = True" 
    1.71 +  and finite_coset_code:
    1.72 +  "finite (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.73  by(simp_all add: card_gt_0_iff finite_UNIV)
    1.74  
    1.75 -definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.76 -where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
    1.77 -
    1.78 -lemma subset'_code [code]:
    1.79 -  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
    1.80 -  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
    1.81 -  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
    1.82 +lemma coset_subset_code [code]:
    1.83 +  fixes xs :: "'a list" shows
    1.84 +  "List.coset xs \<subseteq> set ys \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card (set (xs @ ys)) = n)"
    1.85  by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
    1.86    (metis finite_compl finite_set rev_finite_subset)
    1.87  
    1.88 -definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.89 -where [simp, code del, code_abbrev]: "eq_set = op ="
    1.90 -
    1.91 -lemma eq_set_code [code]:
    1.92 -  fixes ys
    1.93 +lemma equal_set_code [code]:
    1.94 +  fixes xs ys :: "'a :: equal list"
    1.95    defines "rhs \<equiv> 
    1.96    let n = CARD('a)
    1.97    in if n = 0 then False else 
    1.98          let xs' = remdups xs; ys' = remdups ys 
    1.99          in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"
   1.100 -  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   1.101 -  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   1.102 -  and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
   1.103 -  and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
   1.104 +  shows "equal_class.equal (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   1.105 +  and "equal_class.equal (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   1.106 +  and "equal_class.equal (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis3)
   1.107 +  and "equal_class.equal (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)" (is ?thesis4)
   1.108  proof -
   1.109    show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   1.110    proof
   1.111      assume ?lhs thus ?rhs
   1.112 -      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
   1.113 +      by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set)
   1.114    next
   1.115      assume ?rhs
   1.116      moreover have "\<lbrakk> \<forall>y\<in>set xs. y \<notin> set ys; \<forall>x\<in>set ys. x \<notin> set xs \<rbrakk> \<Longrightarrow> set xs \<inter> set ys = {}" by blast
   1.117      ultimately show ?lhs
   1.118 -      by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
   1.119 +      by(auto simp add: equal_eq rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm)
   1.120    qed
   1.121 -  thus ?thesis2 unfolding eq_set_def by blast
   1.122 -  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
   1.123 +  thus ?thesis2 unfolding equal_eq by blast
   1.124 +  show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+
   1.125  qed
   1.126  
   1.127 -end
   1.128 -
   1.129  notepad begin (* test code setup *)
   1.130  have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
   1.131    by eval
   1.132  end
   1.133  
   1.134 -hide_const (open) card' finite' subset' eq_set
   1.135 -
   1.136  end
   1.137