author  wenzelm 
Wed, 03 Oct 2012 16:59:20 +0200  
changeset 49689  b8a710806de9 
parent 48176  3d9c1ddb9f47 
child 49948  744934b818c7 
permissions  rwrr 
37653  1 
(* Title: HOL/Library/Cardinality.thy 
48051  2 
Author: Brian Huffman, Andreas Lochbihler 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

3 
*) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

4 

37653  5 
header {* Cardinality of types *} 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

6 

37653  7 
theory Cardinality 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

8 
imports Phantom_Type 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

9 
begin 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

10 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

11 
subsection {* Preliminary lemmas *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

12 
(* These should be moved elsewhere *) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

13 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

14 
lemma (in type_definition) univ: 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

15 
"UNIV = Abs ` A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

16 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

17 
show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

18 
show "UNIV \<subseteq> Abs ` A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

19 
proof 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

20 
fix x :: 'b 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

21 
have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

22 
moreover have "Rep x \<in> A" by (rule Rep) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

23 
ultimately show "x \<in> Abs ` A" by (rule image_eqI) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

24 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

25 
qed 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

26 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

27 
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

28 
by (simp add: univ card_image inj_on_def Abs_inject) 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

29 

48060  30 
lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)" 
31 
by(auto dest: finite_imageD intro: inj_Some) 

32 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

33 
lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

34 
proof  
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

35 
have "inj STR" by(auto intro: injI) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

36 
thus ?thesis 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

37 
by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

38 
qed 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

39 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

40 
subsection {* Cardinalities of types *} 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

41 

e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

42 
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") 
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

43 

35431  44 
translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)" 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

45 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

46 
typed_print_translation (advanced) {* 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

47 
let 
49689
b8a710806de9
recovered print translation after 'a => bool to 'a set change;
wenzelm
parents:
48176
diff
changeset

48 
fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] = 
b8a710806de9
recovered print translation after 'a => bool to 'a set change;
wenzelm
parents:
48176
diff
changeset

49 
Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

50 
in [(@{const_syntax card}, card_univ_tr')] end 
24407  51 
*} 
52 

48058  53 
lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)" 
26153  54 
unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

55 

48060  56 
lemma card_UNIV_sum: "CARD('a + 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 then CARD('a) + CARD('b) else 0)" 
57 
unfolding UNIV_Plus_UNIV[symmetric] 

58 
by(auto simp add: card_eq_0_iff card_Plus simp del: UNIV_Plus_UNIV) 

59 

30001  60 
lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" 
48060  61 
by(simp add: card_UNIV_sum) 
62 

63 
lemma card_UNIV_option: "CARD('a option) = (if CARD('a) = 0 then 0 else CARD('a) + 1)" 

64 
proof  

65 
have "(None :: 'a option) \<notin> range Some" by clarsimp 

66 
thus ?thesis 

67 
by(simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_insert_disjoint card_image) 

68 
qed 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

69 

30001  70 
lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)" 
48060  71 
by(simp add: card_UNIV_option) 
72 

73 
lemma card_UNIV_set: "CARD('a set) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))" 

74 
by(simp add: Pow_UNIV[symmetric] card_eq_0_iff card_Pow del: Pow_UNIV) 

24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

75 

30001  76 
lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" 
48060  77 
by(simp add: card_UNIV_set) 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
diff
changeset

78 

30001  79 
lemma card_nat [simp]: "CARD(nat) = 0" 
44142  80 
by (simp add: card_eq_0_iff) 
30001  81 

48060  82 
lemma card_fun: "CARD('a \<Rightarrow> 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)" 
83 
proof  

84 
{ assume "0 < CARD('a)" and "0 < CARD('b)" 

85 
hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)" 

86 
by(simp_all only: card_ge_0_finite) 

87 
from finite_distinct_list[OF finb] obtain bs 

88 
where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast 

89 
from finite_distinct_list[OF fina] obtain as 

90 
where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast 

91 
have cb: "CARD('b) = length bs" 

92 
unfolding bs[symmetric] distinct_card[OF distb] .. 

93 
have ca: "CARD('a) = length as" 

94 
unfolding as[symmetric] distinct_card[OF dista] .. 

95 
let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)" 

96 
have "UNIV = set ?xs" 

97 
proof(rule UNIV_eq_I) 

98 
fix f :: "'a \<Rightarrow> 'b" 

99 
from as have "f = the \<circ> map_of (zip as (map f as))" 

100 
by(auto simp add: map_of_zip_map) 

101 
thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists) 

102 
qed 

103 
moreover have "distinct ?xs" unfolding distinct_map 

104 
proof(intro conjI distinct_n_lists distb inj_onI) 

105 
fix xs ys :: "'b list" 

106 
assume xs: "xs \<in> set (Enum.n_lists (length as) bs)" 

107 
and ys: "ys \<in> set (Enum.n_lists (length as) bs)" 

108 
and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)" 

109 
from xs ys have [simp]: "length xs = length as" "length ys = length as" 

110 
by(simp_all add: length_n_lists_elem) 

111 
have "map_of (zip as xs) = map_of (zip as ys)" 

112 
proof 

113 
fix x 

114 
from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y" 

115 
by(simp_all add: map_of_zip_is_Some[symmetric]) 

116 
with eq show "map_of (zip as xs) x = map_of (zip as ys) x" 

117 
by(auto dest: fun_cong[where x=x]) 

118 
qed 

119 
with dista show "xs = ys" by(simp add: map_of_zip_inject) 

120 
qed 

121 
hence "card (set ?xs) = length ?xs" by(simp only: distinct_card) 

122 
moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists) 

123 
ultimately have "CARD('a \<Rightarrow> 'b) = CARD('b) ^ CARD('a)" using cb ca by simp } 

124 
moreover { 

125 
assume cb: "CARD('b) = 1" 

126 
then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq) 

127 
have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}" 

128 
proof(rule UNIV_eq_I) 

129 
fix x :: "'a \<Rightarrow> 'b" 

130 
{ fix y 

131 
have "x y \<in> UNIV" .. 

132 
hence "x y = b" unfolding b by simp } 

133 
thus "x \<in> {\<lambda>x. b}" by(auto) 

134 
qed 

135 
have "CARD('a \<Rightarrow> 'b) = 1" unfolding eq by simp } 

136 
ultimately show ?thesis 

137 
by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1) 

138 
qed 

139 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

140 
corollary finite_UNIV_fun: 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

141 
"finite (UNIV :: ('a \<Rightarrow> 'b) set) \<longleftrightarrow> 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

142 
finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

143 
(is "?lhs \<longleftrightarrow> ?rhs") 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

144 
proof  
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

145 
have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow> 'b) > 0" by(simp add: card_gt_0_iff) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

146 
also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

147 
by(simp add: card_fun) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

148 
also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

149 
finally show ?thesis . 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

150 
qed 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

151 

48060  152 
lemma card_nibble: "CARD(nibble) = 16" 
153 
unfolding UNIV_nibble by simp 

154 

155 
lemma card_UNIV_char: "CARD(char) = 256" 

156 
proof  

157 
have "inj (\<lambda>(x, y). Char x y)" by(auto intro: injI) 

158 
thus ?thesis unfolding UNIV_char by(simp add: card_image card_nibble) 

159 
qed 

160 

161 
lemma card_literal: "CARD(String.literal) = 0" 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

162 
by(simp add: card_eq_0_iff infinite_literal) 
30001  163 

164 
subsection {* Classes with at least 1 and 2 *} 

165 

166 
text {* Class finite already captures "at least 1" *} 

167 

168 
lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)" 

29997  169 
unfolding neq0_conv [symmetric] by simp 
170 

30001  171 
lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)" 
172 
by (simp add: less_Suc_eq_le [symmetric]) 

173 

174 
text {* Class for cardinality "at least 2" *} 

175 

176 
class card2 = finite + 

177 
assumes two_le_card: "2 \<le> CARD('a)" 

178 

179 
lemma one_less_card: "Suc 0 < CARD('a::card2)" 

180 
using two_le_card [where 'a='a] by simp 

181 

182 
lemma one_less_int_card: "1 < int CARD('a::card2)" 

183 
using one_less_card [where 'a='a] by simp 

184 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

185 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

186 
subsection {* A type class for deciding finiteness of types *} 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

187 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

188 
type_synonym 'a finite_UNIV = "('a, bool) phantom" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

189 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

190 
class finite_UNIV = 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

191 
fixes finite_UNIV :: "('a, bool) phantom" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

192 
assumes finite_UNIV: "finite_UNIV = Phantom('a) (finite (UNIV :: 'a set))" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

193 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

194 
lemma finite_UNIV_code [code_unfold]: 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

195 
"finite (UNIV :: 'a :: finite_UNIV set) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

196 
\<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

197 
by(simp add: finite_UNIV) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

198 

48051  199 
subsection {* A type class for computing the cardinality of types *} 
200 

48059  201 
definition is_list_UNIV :: "'a list \<Rightarrow> bool" 
48070
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

202 
where [code del]: "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" 
48059  203 

204 
lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV" 

205 
by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 

206 
dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV) 

207 

48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

208 
type_synonym 'a card_UNIV = "('a, nat) phantom" 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

209 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

210 
class card_UNIV = finite_UNIV + 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

211 
fixes card_UNIV :: "'a card_UNIV" 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

212 
assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)" 
48051  213 

48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

214 
lemma card_UNIV_code [code_unfold]: 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

215 
"CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)" 
48059  216 
by(simp add: card_UNIV) 
48051  217 

48070
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

218 
lemma is_list_UNIV_code [code]: 
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

219 
"is_list_UNIV (xs :: 'a list) = 
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

220 
(let c = CARD('a :: card_UNIV) in if c = 0 then False else size (remdups xs) = c)" 
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

221 
by(rule is_list_UNIV_def) 
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48067
diff
changeset

222 

48060  223 
subsection {* Instantiations for @{text "card_UNIV"} *} 
48051  224 

225 
instantiation nat :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

226 
definition "finite_UNIV = Phantom(nat) False" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

227 
definition "card_UNIV = Phantom(nat) 0" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

228 
instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def) 
48051  229 
end 
230 

231 
instantiation int :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

232 
definition "finite_UNIV = Phantom(int) False" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

233 
definition "card_UNIV = Phantom(int) 0" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

234 
instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int) 
48051  235 
end 
236 

48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

237 
instantiation code_numeral :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

238 
definition "finite_UNIV = Phantom(code_numeral) False" 
48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

239 
definition "card_UNIV = Phantom(code_numeral) 0" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

240 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

241 
by(intro_classes)(auto simp add: card_UNIV_code_numeral_def finite_UNIV_code_numeral_def type_definition.univ[OF type_definition_code_numeral] card_eq_0_iff dest!: finite_imageD intro: inj_onI) 
48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

242 
end 
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

243 

48051  244 
instantiation list :: (type) card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

245 
definition "finite_UNIV = Phantom('a list) False" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

246 
definition "card_UNIV = Phantom('a list) 0" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

247 
instance by intro_classes (simp_all add: card_UNIV_list_def finite_UNIV_list_def infinite_UNIV_listI) 
48051  248 
end 
249 

250 
instantiation unit :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

251 
definition "finite_UNIV = Phantom(unit) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

252 
definition "card_UNIV = Phantom(unit) 1" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

253 
instance by intro_classes (simp_all add: card_UNIV_unit_def finite_UNIV_unit_def) 
48051  254 
end 
255 

256 
instantiation bool :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

257 
definition "finite_UNIV = Phantom(bool) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

258 
definition "card_UNIV = Phantom(bool) 2" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

259 
instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def) 
48051  260 
end 
261 

48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

262 
instantiation nibble :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

263 
definition "finite_UNIV = Phantom(nibble) True" 
48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

264 
definition "card_UNIV = Phantom(nibble) 16" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

265 
instance by(intro_classes)(simp_all add: card_UNIV_nibble_def card_nibble finite_UNIV_nibble_def) 
48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

266 
end 
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

267 

48051  268 
instantiation char :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

269 
definition "finite_UNIV = Phantom(char) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

270 
definition "card_UNIV = Phantom(char) 256" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

271 
instance by intro_classes (simp_all add: card_UNIV_char_def card_UNIV_char finite_UNIV_char_def) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

272 
end 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

273 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

274 
instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV begin 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

275 
definition "finite_UNIV = Phantom('a \<times> 'b) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

276 
(of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

277 
instance by intro_classes (simp add: finite_UNIV_prod_def finite_UNIV finite_prod) 
48051  278 
end 
279 

280 
instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

281 
definition "card_UNIV = Phantom('a \<times> 'b) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

282 
(of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))" 
48060  283 
instance by intro_classes (simp add: card_UNIV_prod_def card_UNIV) 
48051  284 
end 
285 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

286 
instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV begin 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

287 
definition "finite_UNIV = Phantom('a + 'b) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

288 
(of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

289 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

290 
by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

291 
end 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

292 

48051  293 
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

294 
definition "card_UNIV = Phantom('a + 'b) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

295 
(let ca = of_phantom (card_UNIV :: 'a card_UNIV); 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

296 
cb = of_phantom (card_UNIV :: 'b card_UNIV) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

297 
in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)" 
48060  298 
instance by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_UNIV_sum) 
48051  299 
end 
300 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

301 
instantiation "fun" :: (finite_UNIV, card_UNIV) finite_UNIV begin 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

302 
definition "finite_UNIV = Phantom('a \<Rightarrow> 'b) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

303 
(let cb = of_phantom (card_UNIV :: 'b card_UNIV) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

304 
in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

305 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

306 
by intro_classes (auto simp add: finite_UNIV_fun_def Let_def card_UNIV finite_UNIV finite_UNIV_fun card_gt_0_iff) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

307 
end 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

308 

48051  309 
instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

310 
definition "card_UNIV = Phantom('a \<Rightarrow> 'b) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

311 
(let ca = of_phantom (card_UNIV :: 'a card_UNIV); 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

312 
cb = of_phantom (card_UNIV :: 'b card_UNIV) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

313 
in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)" 
48060  314 
instance by intro_classes (simp add: card_UNIV_fun_def card_UNIV Let_def card_fun) 
315 
end 

48051  316 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

317 
instantiation option :: (finite_UNIV) finite_UNIV begin 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

318 
definition "finite_UNIV = Phantom('a option) (of_phantom (finite_UNIV :: 'a finite_UNIV))" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

319 
instance by intro_classes (simp add: finite_UNIV_option_def finite_UNIV) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

320 
end 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

321 

48060  322 
instantiation option :: (card_UNIV) card_UNIV begin 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

323 
definition "card_UNIV = Phantom('a option) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

324 
(let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c \<noteq> 0 then Suc c else 0)" 
48060  325 
instance by intro_classes (simp add: card_UNIV_option_def card_UNIV card_UNIV_option) 
326 
end 

48051  327 

48060  328 
instantiation String.literal :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

329 
definition "finite_UNIV = Phantom(String.literal) False" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

330 
definition "card_UNIV = Phantom(String.literal) 0" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

331 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

332 
by intro_classes (simp_all add: card_UNIV_literal_def finite_UNIV_literal_def infinite_literal card_literal) 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

333 
end 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

334 

3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

335 
instantiation set :: (finite_UNIV) finite_UNIV begin 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

336 
definition "finite_UNIV = Phantom('a set) (of_phantom (finite_UNIV :: 'a finite_UNIV))" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

337 
instance by intro_classes (simp add: finite_UNIV_set_def finite_UNIV Finite_Set.finite_set) 
48060  338 
end 
339 

340 
instantiation set :: (card_UNIV) card_UNIV begin 

48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

341 
definition "card_UNIV = Phantom('a set) 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

342 
(let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c = 0 then 0 else 2 ^ c)" 
48060  343 
instance by intro_classes (simp add: card_UNIV_set_def card_UNIV_set card_UNIV) 
48051  344 
end 
345 

48060  346 
lemma UNIV_finite_1: "UNIV = set [finite_1.a\<^isub>1]" 
347 
by(auto intro: finite_1.exhaust) 

348 

349 
lemma UNIV_finite_2: "UNIV = set [finite_2.a\<^isub>1, finite_2.a\<^isub>2]" 

350 
by(auto intro: finite_2.exhaust) 

48051  351 

48060  352 
lemma UNIV_finite_3: "UNIV = set [finite_3.a\<^isub>1, finite_3.a\<^isub>2, finite_3.a\<^isub>3]" 
353 
by(auto intro: finite_3.exhaust) 

48051  354 

48060  355 
lemma UNIV_finite_4: "UNIV = set [finite_4.a\<^isub>1, finite_4.a\<^isub>2, finite_4.a\<^isub>3, finite_4.a\<^isub>4]" 
356 
by(auto intro: finite_4.exhaust) 

357 

358 
lemma UNIV_finite_5: 

359 
"UNIV = set [finite_5.a\<^isub>1, finite_5.a\<^isub>2, finite_5.a\<^isub>3, finite_5.a\<^isub>4, finite_5.a\<^isub>5]" 

360 
by(auto intro: finite_5.exhaust) 

48051  361 

48060  362 
instantiation Enum.finite_1 :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

363 
definition "finite_UNIV = Phantom(Enum.finite_1) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

364 
definition "card_UNIV = Phantom(Enum.finite_1) 1" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

365 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

366 
by intro_classes (simp_all add: UNIV_finite_1 card_UNIV_finite_1_def finite_UNIV_finite_1_def) 
48060  367 
end 
368 

369 
instantiation Enum.finite_2 :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

370 
definition "finite_UNIV = Phantom(Enum.finite_2) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

371 
definition "card_UNIV = Phantom(Enum.finite_2) 2" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

372 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

373 
by intro_classes (simp_all add: UNIV_finite_2 card_UNIV_finite_2_def finite_UNIV_finite_2_def) 
48060  374 
end 
48051  375 

48060  376 
instantiation Enum.finite_3 :: card_UNIV begin 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

377 
definition "finite_UNIV = Phantom(Enum.finite_3) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

378 
definition "card_UNIV = Phantom(Enum.finite_3) 3" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

379 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

380 
by intro_classes (simp_all add: UNIV_finite_3 card_UNIV_finite_3_def finite_UNIV_finite_3_def) 
48060  381 
end 
382 

383 
instantiation Enum.finite_4 :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

384 
definition "finite_UNIV = Phantom(Enum.finite_4) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

385 
definition "card_UNIV = Phantom(Enum.finite_4) 4" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

386 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

387 
by intro_classes (simp_all add: UNIV_finite_4 card_UNIV_finite_4_def finite_UNIV_finite_4_def) 
48060  388 
end 
389 

390 
instantiation Enum.finite_5 :: card_UNIV begin 

48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

391 
definition "finite_UNIV = Phantom(Enum.finite_5) True" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

392 
definition "card_UNIV = Phantom(Enum.finite_5) 5" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

393 
instance 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

394 
by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def) 
48051  395 
end 
396 

48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

397 
subsection {* Code setup for sets *} 
48051  398 

399 
lemma card_Compl: 

400 
"finite A \<Longrightarrow> card ( A) = card (UNIV :: 'a set)  card (A :: 'a set)" 

401 
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) 

402 

48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

403 
context fixes xs :: "'a :: card_UNIV list" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

404 
begin 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

405 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

406 
definition card' :: "'a set \<Rightarrow> nat" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

407 
where [simp, code del, code_abbrev]: "card' = card" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

408 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

409 
lemma card'_code [code]: 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

410 
"card' (set xs) = length (remdups xs)" 
48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

411 
"card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV)  length (remdups xs)" 
48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

412 
by(simp_all add: List.card_set card_Compl card_UNIV) 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

413 

48164
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

414 
lemma card'_UNIV [code_unfold]: 
e97369f20c30
change card_UNIV from itself to phantom type to avoid unnecessary closures in generated code
Andreas Lochbihler
parents:
48070
diff
changeset

415 
"card' (UNIV :: 'a :: card_UNIV set) = of_phantom (card_UNIV :: 'a card_UNIV)" 
48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

416 
by(simp add: card_UNIV) 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

417 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

418 
definition finite' :: "'a set \<Rightarrow> bool" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

419 
where [simp, code del, code_abbrev]: "finite' = finite" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

420 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

421 
lemma finite'_code [code]: 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

422 
"finite' (set xs) \<longleftrightarrow> True" 
48176
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

423 
"finite' (List.coset xs) \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)" 
3d9c1ddb9f47
new type class for computing finiteness of types with instantiations
Andreas Lochbihler
parents:
48165
diff
changeset

424 
by(simp_all add: card_gt_0_iff finite_UNIV) 
48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

425 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

426 
definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

427 
where [simp, code del, code_abbrev]: "subset' = op \<subseteq>" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

428 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

429 
lemma subset'_code [code]: 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

430 
"subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

431 
"subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

432 
"subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

433 
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

434 
(metis finite_compl finite_set rev_finite_subset) 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

435 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

436 
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

437 
where [simp, code del, code_abbrev]: "eq_set = op =" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

438 

48051  439 
lemma eq_set_code [code]: 
48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

440 
fixes ys 
48051  441 
defines "rhs \<equiv> 
48059  442 
let n = CARD('a) 
48051  443 
in if n = 0 then False else 
444 
let xs' = remdups xs; ys' = remdups ys 

445 
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')" 

446 
shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1) 

447 
and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2) 

448 
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) 

449 
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) 

450 
proof  

451 
show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs") 

452 
proof 

453 
assume ?lhs thus ?rhs 

454 
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) 

455 
next 

456 
assume ?rhs 

457 
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 

458 
ultimately show ?lhs 

459 
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) 

460 
qed 

461 
thus ?thesis2 unfolding eq_set_def by blast 

462 
show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+ 

463 
qed 

464 

48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

465 
end 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

466 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

467 
notepad begin (* test code setup *) 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

468 
have "List.coset [True] = set [False] \<and> List.coset [] \<subseteq> List.set [True, False] \<and> finite (List.coset [True])" 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

469 
by eval 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

470 
end 
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

471 

9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

472 
hide_const (open) card' finite' subset' eq_set 
48051  473 

474 
end 