implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
authorAndreas Lochbihler
Thu Feb 14 16:01:28 2013 +0100 (2013-02-14)
changeset 511160dac0158b8d4
parent 51114 3e913a575dc6
child 51117 47af65ef228e
implement code generation for finite, card, op = and op <= for sets always via finite_UNIV and card_UNIV, as fragile rewrites based on sorts are hard to find and debug
src/HOL/Codegenerator_Test/RBT_Set_Test.thy
src/HOL/Library/Cardinality.thy
     1.1 --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Thu Feb 14 12:24:56 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Thu Feb 14 16:01:28 2013 +0100
     1.3 @@ -22,23 +22,13 @@
     1.4  lemma [code, code del]:
     1.5    "pred_of_set = pred_of_set" ..
     1.6  
     1.7 -
     1.8 -lemma [code, code del]:
     1.9 -  "Cardinality.card' = Cardinality.card'" ..
    1.10 -
    1.11 -lemma [code, code del]:
    1.12 -  "Cardinality.finite' = Cardinality.finite'" ..
    1.13 -
    1.14 -lemma [code, code del]:
    1.15 -  "Cardinality.subset' = Cardinality.subset'" ..
    1.16 -
    1.17 -lemma [code, code del]:
    1.18 -  "Cardinality.eq_set = Cardinality.eq_set" ..
    1.19 -
    1.20 -
    1.21  lemma [code, code del]:
    1.22    "acc = acc" ..
    1.23  
    1.24 +lemmas [code del] =
    1.25 +  finite_set_code finite_coset_code 
    1.26 +  equal_set_code
    1.27 +
    1.28  (*
    1.29    If the code generation ends with an exception with the following message:
    1.30    '"List.set" is not a constructor, on left hand side of equation: ...',
     2.1 --- a/src/HOL/Library/Cardinality.thy	Thu Feb 14 12:24:56 2013 +0100
     2.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Feb 14 16:01:28 2013 +0100
     2.3 @@ -199,7 +199,7 @@
     2.4  subsection {* A type class for computing the cardinality of types *}
     2.5  
     2.6  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
     2.7 -where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     2.8 +where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     2.9  
    2.10  lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    2.11  by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    2.12 @@ -211,15 +211,6 @@
    2.13    fixes card_UNIV :: "'a card_UNIV"
    2.14    assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
    2.15  
    2.16 -lemma card_UNIV_code [code_unfold]: 
    2.17 -  "CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"
    2.18 -by(simp add: card_UNIV)
    2.19 -
    2.20 -lemma is_list_UNIV_code [code]:
    2.21 -  "is_list_UNIV (xs :: 'a list) = 
    2.22 -  (let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)"
    2.23 -by(rule is_list_UNIV_def)
    2.24 -
    2.25  subsection {* Instantiations for @{text "card_UNIV"} *}
    2.26  
    2.27  instantiation nat :: card_UNIV begin
    2.28 @@ -396,80 +387,66 @@
    2.29  
    2.30  subsection {* Code setup for sets *}
    2.31  
    2.32 +text {*
    2.33 +  Implement operations @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, and @{term "op ="} 
    2.34 +  for sets using @{term "finite_UNIV"} and @{term "card_UNIV"}.
    2.35 +*}
    2.36 +
    2.37  lemma card_Compl:
    2.38    "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
    2.39  by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest)
    2.40  
    2.41 -context fixes xs :: "'a :: card_UNIV list"
    2.42 -begin
    2.43 +lemma card_coset_code [code]:
    2.44 +  fixes xs :: "'a :: card_UNIV list" 
    2.45 +  shows "card (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    2.46 +by(simp add: List.card_set card_Compl card_UNIV)
    2.47  
    2.48 -definition card' :: "'a set \<Rightarrow> nat" 
    2.49 -where [simp, code del, code_abbrev]: "card' = card"
    2.50 -
    2.51 -lemma card'_code [code]:
    2.52 -  "card' (set xs) = length (remdups xs)"
    2.53 -  "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)"
    2.54 -by(simp_all add: List.card_set card_Compl card_UNIV)
    2.55 +lemma [code, code del]: "finite = finite" ..
    2.56  
    2.57 -lemma card'_UNIV [code_unfold]: 
    2.58 -  "card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)"
    2.59 -by(simp add: card_UNIV)
    2.60 -
    2.61 -definition finite' :: "'a set \<Rightarrow> bool"
    2.62 -where [simp, code del, code_abbrev]: "finite' = finite"
    2.63 -
    2.64 -lemma finite'_code [code]:
    2.65 -  "finite' (set xs) \<longleftrightarrow> True"
    2.66 -  "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    2.67 +lemma [code]:
    2.68 +  fixes xs :: "'a :: card_UNIV list" 
    2.69 +  shows finite_set_code:
    2.70 +  "finite (set xs) = True" 
    2.71 +  and finite_coset_code:
    2.72 +  "finite (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    2.73  by(simp_all add: card_gt_0_iff finite_UNIV)
    2.74  
    2.75 -definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    2.76 -where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
    2.77 -
    2.78 -lemma subset'_code [code]:
    2.79 -  "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)"
    2.80 -  "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)"
    2.81 -  "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)"
    2.82 +lemma coset_subset_code [code]:
    2.83 +  fixes xs :: "'a list" shows
    2.84 +  "List.coset xs \<subseteq> set ys \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card (set (xs @ ys)) = n)"
    2.85  by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
    2.86    (metis finite_compl finite_set rev_finite_subset)
    2.87  
    2.88 -definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    2.89 -where [simp, code del, code_abbrev]: "eq_set = op ="
    2.90 -
    2.91 -lemma eq_set_code [code]:
    2.92 -  fixes ys
    2.93 +lemma equal_set_code [code]:
    2.94 +  fixes xs ys :: "'a :: equal list"
    2.95    defines "rhs \<equiv> 
    2.96    let n = CARD('a)
    2.97    in if n = 0 then False else 
    2.98          let xs' = remdups xs; ys' = remdups ys 
    2.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')"
   2.100 -  shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   2.101 -  and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   2.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)
   2.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)
   2.104 +  shows "equal_class.equal (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1)
   2.105 +  and "equal_class.equal (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2)
   2.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)
   2.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)
   2.108  proof -
   2.109    show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs")
   2.110    proof
   2.111      assume ?lhs thus ?rhs
   2.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)
   2.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)
   2.114    next
   2.115      assume ?rhs
   2.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
   2.117      ultimately show ?lhs
   2.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)
   2.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)
   2.120    qed
   2.121 -  thus ?thesis2 unfolding eq_set_def by blast
   2.122 -  show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+
   2.123 +  thus ?thesis2 unfolding equal_eq by blast
   2.124 +  show ?thesis3 ?thesis4 unfolding equal_eq List.coset_def by blast+
   2.125  qed
   2.126  
   2.127 -end
   2.128 -
   2.129  notepad begin (* test code setup *)
   2.130  have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])"
   2.131    by eval
   2.132  end
   2.133  
   2.134 -hide_const (open) card' finite' subset' eq_set
   2.135 -
   2.136  end
   2.137