src/HOL/Library/Cardinality.thy
changeset 51139 c8e3cf3520b3
parent 51116 0dac0158b8d4
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu Feb 14 17:58:28 2013 +0100
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Feb 15 09:41:25 2013 +0100
     1.3 @@ -388,65 +388,133 @@
     1.4  subsection {* Code setup for sets *}
     1.5  
     1.6  text {*
     1.7 -  Implement operations @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, and @{term "op ="} 
     1.8 -  for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}.
     1.9 +  Implement @{term "CARD('a)"} via @{term card_UNIV} and provide
    1.10 +  implementations for @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, 
    1.11 +  and @{term "op ="}if the calling context already provides @{class finite_UNIV}
    1.12 +  and @{class card_UNIV} instances. If we implemented the latter
    1.13 +  always via @{term card_UNIV}, we would require instances of essentially all 
    1.14 +  element types, i.e., a lot of instantiation proofs and -- at run time --
    1.15 +  possibly slow dictionary constructions.
    1.16  *}
    1.17  
    1.18 +definition card_UNIV' :: "'a card_UNIV"
    1.19 +where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
    1.20 +
    1.21 +lemma CARD_code [code_unfold]:
    1.22 +  "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)"
    1.23 +by(simp add: card_UNIV'_def)
    1.24 +
    1.25 +lemma card_UNIV'_code [code]:
    1.26 +  "card_UNIV' = card_UNIV"
    1.27 +by(simp add: card_UNIV card_UNIV'_def)
    1.28 +
    1.29 +hide_const (open) card_UNIV'
    1.30 +
    1.31  lemma card_Compl:
    1.32    "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
    1.33  by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
    1.34  
    1.35 -lemma card_coset_code [code]:
    1.36 -  fixes xs :: "'a :: card_UNIV list" 
    1.37 -  shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    1.38 -by(simp add: List.card_set card_Compl card_UNIV)
    1.39 -
    1.40 -lemma [code, code del]: "finite = finite" ..
    1.41 +context fixes xs :: "'a :: finite_UNIV list"
    1.42 +begin
    1.43  
    1.44 -lemma [code]:
    1.45 -  fixes xs :: "'a :: card_UNIV list" 
    1.46 -  shows finite_set_code:
    1.47 -  "finite (set xs) = True" 
    1.48 -  and finite_coset_code:
    1.49 -  "finite (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.50 +definition finite' :: "'a set \<Rightarrow> bool"
    1.51 +where [simp, code del, code_abbrev]: "finite' = finite"
    1.52 +
    1.53 +lemma finite'_code [code]:
    1.54 +  "finite' (set xs) \<longleftrightarrow> True"
    1.55 +  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.56  by(simp_all add: card_gt_0_iff finite_UNIV)
    1.57  
    1.58 -lemma coset_subset_code [code]:
    1.59 -  fixes xs :: "'a list" shows
    1.60 -  "List.coset xs \<subseteq> set ys \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card (set (xs @ ys)) = n)"
    1.61 +end
    1.62 +
    1.63 +context fixes xs :: "'a :: card_UNIV list"
    1.64 +begin
    1.65 +
    1.66 +definition card' :: "'a set \<Rightarrow> nat" 
    1.67 +where [simp, code del, code_abbrev]: "card' = card"
    1.68 + 
    1.69 +lemma card'_code [code]:
    1.70 +  "card' (set xs) = length (remdups xs)"
    1.71 +  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    1.72 +by(simp_all add: List.card_set card_Compl card_UNIV)
    1.73 +
    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  by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
    1.83    (metis finite_compl finite_set rev_finite_subset)
    1.84  
    1.85 -lemma equal_set_code [code]:
    1.86 -  fixes xs ys :: "'a :: equal list"
    1.87 +definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    1.88 +where [simp, code del, code_abbrev]: "eq_set = op ="
    1.89 +
    1.90 +lemma eq_set_code [code]:
    1.91 +  fixes ys
    1.92    defines "rhs \<equiv> 
    1.93    let n = CARD('a)
    1.94    in if n = 0 then False else 
    1.95          let xs' = remdups xs; ys' = remdups ys 
    1.96          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.97 -  shows "equal_class.equal (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
    1.98 -  and "equal_class.equal (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
    1.99 -  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.100 -  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.101 +  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   1.102 +  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   1.103 +  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.104 +  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.105  proof -
   1.106    show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   1.107    proof
   1.108      assume ?lhs thus ?rhs
   1.109 -      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.110 +      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.111    next
   1.112      assume ?rhs
   1.113      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.114      ultimately show ?lhs
   1.115 -      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.116 +      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.117    qed
   1.118 -  thus ?thesis2 unfolding equal_eq by blast
   1.119 -  show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+
   1.120 +  thus ?thesis2 unfolding eq_set_def by blast
   1.121 +  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
   1.122  qed
   1.123  
   1.124 -notepad begin (* test code setup *)
   1.125 -have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
   1.126 +end
   1.127 +
   1.128 +text {* 
   1.129 +  Provide more informative exceptions than Match for non-rewritten cases.
   1.130 +  If generated code raises one these exceptions, then a code equation calls
   1.131 +  the mentioned operator for an element type that is not an instance of
   1.132 +  @{class card_UNIV} and is therefore not implemented via @{term card_UNIV}.
   1.133 +  Constrain the element type with sort @{class card_UNIV} to change this.
   1.134 +*}
   1.135 +
   1.136 +definition card_coset_requires_card_UNIV :: "'a list \<Rightarrow> nat"
   1.137 +where [code del, simp]: "card_coset_requires_card_UNIV xs = card (List.coset xs)"
   1.138 +
   1.139 +code_abort card_coset_requires_card_UNIV
   1.140 +
   1.141 +lemma card_coset_error [code]:
   1.142 +  "card (List.coset xs) = card_coset_requires_card_UNIV xs"
   1.143 +by(simp)
   1.144 +
   1.145 +definition coset_subseteq_set_requires_card_UNIV :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   1.146 +where [code del, simp]: "coset_subseteq_set_requires_card_UNIV xs ys \<longleftrightarrow> List.coset xs \<subseteq> set ys"
   1.147 +
   1.148 +code_abort coset_subseteq_set_requires_card_UNIV
   1.149 +
   1.150 +lemma coset_subseteq_set_code [code]:
   1.151 +  "List.coset xs \<subseteq> set ys \<longleftrightarrow> 
   1.152 +  (if xs = [] \<and> ys = [] then False else coset_subseteq_set_requires_card_UNIV xs ys)"
   1.153 +by simp
   1.154 +
   1.155 +notepad begin -- "test code setup"
   1.156 +have "List.coset [True] = set [False] \<and> 
   1.157 +      List.coset [] \<subseteq> List.set [True, False] \<and> 
   1.158 +      finite (List.coset [True])"
   1.159    by eval
   1.160  end
   1.161  
   1.162 +hide_const (open) card' finite' subset' eq_set
   1.163 +
   1.164  end
   1.165