|
1 subsection \<open>Code setup for sets with cardinality type information\<close> |
|
2 |
|
3 theory Code_Cardinality imports Cardinality begin |
|
4 |
|
5 text \<open> |
|
6 Implement \<^term>\<open>CARD('a)\<close> via \<^term>\<open>card_UNIV\<close> and provide |
|
7 implementations for \<^term>\<open>finite\<close>, \<^term>\<open>card\<close>, \<^term>\<open>(\<subseteq>)\<close>, |
|
8 and \<^term>\<open>(=)\<close>if the calling context already provides \<^class>\<open>finite_UNIV\<close> |
|
9 and \<^class>\<open>card_UNIV\<close> instances. If we implemented the latter |
|
10 always via \<^term>\<open>card_UNIV\<close>, we would require instances of essentially all |
|
11 element types, i.e., a lot of instantiation proofs and -- at run time -- |
|
12 possibly slow dictionary constructions. |
|
13 \<close> |
|
14 |
|
15 context |
|
16 begin |
|
17 |
|
18 qualified definition card_UNIV' :: "'a card_UNIV" |
|
19 where [code del]: "card_UNIV' = Phantom('a) CARD('a)" |
|
20 |
|
21 lemma CARD_code [code_unfold]: |
|
22 "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)" |
|
23 by(simp add: card_UNIV'_def) |
|
24 |
|
25 lemma card_UNIV'_code [code]: |
|
26 "card_UNIV' = card_UNIV" |
|
27 by(simp add: card_UNIV card_UNIV'_def) |
|
28 |
|
29 end |
|
30 |
|
31 lemma card_Compl: |
|
32 "finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" |
|
33 by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) |
|
34 |
|
35 context fixes xs :: "'a :: finite_UNIV list" |
|
36 begin |
|
37 |
|
38 qualified definition finite' :: "'a set \<Rightarrow> bool" |
|
39 where [simp, code del, code_abbrev]: "finite' = finite" |
|
40 |
|
41 lemma finite'_code [code]: |
|
42 "finite' (set xs) \<longleftrightarrow> True" |
|
43 "finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)" |
|
44 by(simp_all add: card_gt_0_iff finite_UNIV) |
|
45 |
|
46 end |
|
47 |
|
48 context fixes xs :: "'a :: card_UNIV list" |
|
49 begin |
|
50 |
|
51 qualified definition card' :: "'a set \<Rightarrow> nat" |
|
52 where [simp, code del, code_abbrev]: "card' = card" |
|
53 |
|
54 lemma card'_code [code]: |
|
55 "card' (set xs) = length (remdups xs)" |
|
56 "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" |
|
57 by(simp_all add: List.card_set card_Compl card_UNIV) |
|
58 |
|
59 |
|
60 qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
61 where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)" |
|
62 |
|
63 lemma subset'_code [code]: |
|
64 "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" |
|
65 "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" |
|
66 "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)" |
|
67 by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) |
|
68 (metis finite_compl finite_set rev_finite_subset) |
|
69 |
|
70 qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
71 where [simp, code del, code_abbrev]: "eq_set = (=)" |
|
72 |
|
73 lemma eq_set_code [code]: |
|
74 fixes ys |
|
75 defines "rhs \<equiv> |
|
76 let n = CARD('a) |
|
77 in if n = 0 then False else |
|
78 let xs' = remdups xs; ys' = remdups ys |
|
79 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')" |
|
80 shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" |
|
81 and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" |
|
82 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)" |
|
83 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)" |
|
84 proof goal_cases |
|
85 { |
|
86 case 1 |
|
87 show ?case (is "?lhs \<longleftrightarrow> ?rhs") |
|
88 proof |
|
89 show ?rhs if ?lhs |
|
90 using that |
|
91 by (auto simp add: rhs_def Let_def List.card_set[symmetric] |
|
92 card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV |
|
93 Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) |
|
94 show ?lhs if ?rhs |
|
95 proof - |
|
96 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 |
|
97 with that show ?thesis |
|
98 by (auto simp add: rhs_def Let_def List.card_set[symmetric] |
|
99 card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] |
|
100 dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm) |
|
101 qed |
|
102 qed |
|
103 } |
|
104 moreover |
|
105 case 2 |
|
106 ultimately show ?case unfolding eq_set_def by blast |
|
107 next |
|
108 case 3 |
|
109 show ?case unfolding eq_set_def List.coset_def by blast |
|
110 next |
|
111 case 4 |
|
112 show ?case unfolding eq_set_def List.coset_def by blast |
|
113 qed |
|
114 |
|
115 end |
|
116 |
|
117 text \<open> |
|
118 Provide more informative exceptions than Match for non-rewritten cases. |
|
119 If generated code raises one these exceptions, then a code equation calls |
|
120 the mentioned operator for an element type that is not an instance of |
|
121 \<^class>\<open>card_UNIV\<close> and is therefore not implemented via \<^term>\<open>card_UNIV\<close>. |
|
122 Constrain the element type with sort \<^class>\<open>card_UNIV\<close> to change this. |
|
123 \<close> |
|
124 |
|
125 lemma card_coset_error [code]: |
|
126 "card (List.coset xs) = |
|
127 Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'') |
|
128 (\<lambda>_. card (List.coset xs))" |
|
129 by(simp) |
|
130 |
|
131 lemma coset_subseteq_set_code [code]: |
|
132 "List.coset xs \<subseteq> set ys \<longleftrightarrow> |
|
133 (if xs = [] \<and> ys = [] then False |
|
134 else Code.abort |
|
135 (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'') |
|
136 (\<lambda>_. List.coset xs \<subseteq> set ys))" |
|
137 by simp |
|
138 |
|
139 notepad begin \<comment> \<open>test code setup\<close> |
|
140 have "List.coset [True] = set [False] \<and> |
|
141 List.coset [] \<subseteq> List.set [True, False] \<and> |
|
142 finite (List.coset [True])" |
|
143 by eval |
|
144 |
|
145 end |
|
146 |
|
147 end |