author  wenzelm 
Sat, 25 May 2013 15:37:53 +0200  
changeset 52143  36ffe23b25f8 
parent 51188  9b5bf1a9a710 
child 52147  9943f8067f11 
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 

52143  46 
typed_print_translation {* 
42247
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] .. 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49689
diff
changeset

95 
let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)" 
48060  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" 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49689
diff
changeset

106 
assume xs: "xs \<in> set (List.n_lists (length as) bs)" 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49689
diff
changeset

107 
and ys: "ys \<in> set (List.n_lists (length as) bs)" 
48060  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" 
51116
0dac0158b8d4
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
Andreas Lochbihler
parents:
49948
diff
changeset

202 
where "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 

48060  214 
subsection {* Instantiations for @{text "card_UNIV"} *} 
48051  215 

216 
instantiation nat :: card_UNIV begin 

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

217 
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

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

219 
instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def) 
48051  220 
end 
221 

222 
instantiation int :: card_UNIV begin 

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

223 
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

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

225 
instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int) 
48051  226 
end 
227 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

228 
instantiation natural :: card_UNIV begin 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

229 
definition "finite_UNIV = Phantom(natural) False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

230 
definition "card_UNIV = Phantom(natural) 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

231 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

232 
qed (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

233 
type_definition.univ [OF type_definition_natural] natural_eq_iff 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

234 
dest!: finite_imageD intro: inj_onI) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

235 
end 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

236 

0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

237 
instantiation integer :: card_UNIV begin 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

238 
definition "finite_UNIV = Phantom(integer) False" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

239 
definition "card_UNIV = Phantom(integer) 0" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

240 
instance proof 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

241 
qed (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

242 
type_definition.univ [OF type_definition_integer] infinite_UNIV_int 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51139
diff
changeset

243 
dest!: finite_imageD intro: inj_onI) 
48165
d07a0b9601aa
instantiate card_UNIV with nibble and code_numeral
Andreas Lochbihler
parents:
48164
diff
changeset

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

245 

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

247 
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

248 
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

249 
instance by intro_classes (simp_all add: card_UNIV_list_def finite_UNIV_list_def infinite_UNIV_listI) 
48051  250 
end 
251 

252 
instantiation unit :: card_UNIV begin 

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

253 
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

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

255 
instance by intro_classes (simp_all add: card_UNIV_unit_def finite_UNIV_unit_def) 
48051  256 
end 
257 

258 
instantiation bool :: card_UNIV begin 

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

259 
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

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

261 
instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def) 
48051  262 
end 
263 

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

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

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

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

267 
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

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

269 

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

271 
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

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

273 
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

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

275 

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

276 
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

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

278 
(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

279 
instance by intro_classes (simp add: finite_UNIV_prod_def finite_UNIV finite_prod) 
48051  280 
end 
281 

282 
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

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

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

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

288 
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

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

290 
(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

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

292 
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

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

294 

48051  295 
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

296 
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

297 
(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

298 
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

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

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

303 
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

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

305 
(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

306 
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

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

308 
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

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

310 

48051  311 
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

312 
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

313 
(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

314 
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

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

48051  318 

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

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

320 
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

321 
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

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

323 

48060  324 
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

325 
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

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

48051  329 

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

331 
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

332 
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

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

334 
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

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

336 

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

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

338 
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

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

342 
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

343 
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

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

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

350 

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

352 
by(auto intro: finite_2.exhaust) 

48051  353 

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

48051  356 

48060  357 
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]" 
358 
by(auto intro: finite_4.exhaust) 

359 

360 
lemma UNIV_finite_5: 

361 
"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]" 

362 
by(auto intro: finite_5.exhaust) 

48051  363 

48060  364 
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

365 
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

366 
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

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

368 
by intro_classes (simp_all add: UNIV_finite_1 card_UNIV_finite_1_def finite_UNIV_finite_1_def) 
48060  369 
end 
370 

371 
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

372 
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

373 
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

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

375 
by intro_classes (simp_all add: UNIV_finite_2 card_UNIV_finite_2_def finite_UNIV_finite_2_def) 
48060  376 
end 
48051  377 

48060  378 
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

379 
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

380 
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

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

382 
by intro_classes (simp_all add: UNIV_finite_3 card_UNIV_finite_3_def finite_UNIV_finite_3_def) 
48060  383 
end 
384 

385 
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

386 
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

387 
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

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

389 
by intro_classes (simp_all add: UNIV_finite_4 card_UNIV_finite_4_def finite_UNIV_finite_4_def) 
48060  390 
end 
391 

392 
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

393 
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

394 
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

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

396 
by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def) 
48051  397 
end 
398 

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

399 
subsection {* Code setup for sets *} 
48051  400 

51116
0dac0158b8d4
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
Andreas Lochbihler
parents:
49948
diff
changeset

401 
text {* 
51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

402 
Implement @{term "CARD('a)"} via @{term card_UNIV} and provide 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

403 
implementations for @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

404 
and @{term "op ="}if the calling context already provides @{class finite_UNIV} 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

405 
and @{class card_UNIV} instances. If we implemented the latter 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

406 
always via @{term card_UNIV}, we would require instances of essentially all 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

407 
element types, i.e., a lot of instantiation proofs and  at run time  
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

408 
possibly slow dictionary constructions. 
51116
0dac0158b8d4
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
Andreas Lochbihler
parents:
49948
diff
changeset

409 
*} 
0dac0158b8d4
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
Andreas Lochbihler
parents:
49948
diff
changeset

410 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

411 
definition card_UNIV' :: "'a card_UNIV" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

412 
where [code del]: "card_UNIV' = Phantom('a) CARD('a)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

413 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

414 
lemma CARD_code [code_unfold]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

415 
"CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

416 
by(simp add: card_UNIV'_def) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

417 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

418 
lemma card_UNIV'_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

419 
"card_UNIV' = card_UNIV" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

420 
by(simp add: card_UNIV card_UNIV'_def) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

421 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

422 
hide_const (open) card_UNIV' 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

423 

48051  424 
lemma card_Compl: 
425 
"finite A \<Longrightarrow> card ( A) = card (UNIV :: 'a set)  card (A :: 'a set)" 

426 
by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) 

427 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

428 
context fixes xs :: "'a :: finite_UNIV list" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

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

430 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

431 
definition finite' :: "'a set \<Rightarrow> bool" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

432 
where [simp, code del, code_abbrev]: "finite' = finite" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

433 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

434 
lemma finite'_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

435 
"finite' (set xs) \<longleftrightarrow> True" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

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

437 
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

438 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

439 
end 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

440 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

441 
context fixes xs :: "'a :: card_UNIV list" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

442 
begin 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

443 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

444 
definition card' :: "'a set \<Rightarrow> nat" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

445 
where [simp, code del, code_abbrev]: "card' = card" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

446 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

447 
lemma card'_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

448 
"card' (set xs) = length (remdups xs)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

449 
"card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV)  length (remdups xs)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

450 
by(simp_all add: List.card_set card_Compl card_UNIV) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

451 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

452 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

453 
definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

454 
where [simp, code del, code_abbrev]: "subset' = op \<subseteq>" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

455 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

456 
lemma subset'_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

457 
"subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

458 
"subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

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

460 
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

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

462 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

463 
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

464 
where [simp, code del, code_abbrev]: "eq_set = op =" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

465 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

466 
lemma eq_set_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

467 
fixes ys 
48051  468 
defines "rhs \<equiv> 
48059  469 
let n = CARD('a) 
48051  470 
in if n = 0 then False else 
471 
let xs' = remdups xs; ys' = remdups ys 

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

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

473 
shows "eq_set (List.coset xs) (set ys) \<longleftrightarrow> rhs" (is ?thesis1) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

474 
and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs" (is ?thesis2) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

475 
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) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

476 
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) 
48051  477 
proof  
478 
show ?thesis1 (is "?lhs \<longleftrightarrow> ?rhs") 

479 
proof 

480 
assume ?lhs thus ?rhs 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

481 
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) 
48051  482 
next 
483 
assume ?rhs 

484 
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 

485 
ultimately show ?lhs 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

486 
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) 
48051  487 
qed 
51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

488 
thus ?thesis2 unfolding eq_set_def by blast 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

489 
show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+ 
48051  490 
qed 
491 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

492 
end 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

493 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

494 
text {* 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

495 
Provide more informative exceptions than Match for nonrewritten cases. 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

496 
If generated code raises one these exceptions, then a code equation calls 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

497 
the mentioned operator for an element type that is not an instance of 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

498 
@{class card_UNIV} and is therefore not implemented via @{term card_UNIV}. 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

499 
Constrain the element type with sort @{class card_UNIV} to change this. 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

500 
*} 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

501 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

502 
definition card_coset_requires_card_UNIV :: "'a list \<Rightarrow> nat" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

503 
where [code del, simp]: "card_coset_requires_card_UNIV xs = card (List.coset xs)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

504 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

505 
code_abort card_coset_requires_card_UNIV 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

506 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

507 
lemma card_coset_error [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

508 
"card (List.coset xs) = card_coset_requires_card_UNIV xs" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

509 
by(simp) 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

510 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

511 
definition coset_subseteq_set_requires_card_UNIV :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

512 
where [code del, simp]: "coset_subseteq_set_requires_card_UNIV xs ys \<longleftrightarrow> List.coset xs \<subseteq> set ys" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

513 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

514 
code_abort coset_subseteq_set_requires_card_UNIV 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

515 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

516 
lemma coset_subseteq_set_code [code]: 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

517 
"List.coset xs \<subseteq> set ys \<longleftrightarrow> 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

518 
(if xs = [] \<and> ys = [] then False else coset_subseteq_set_requires_card_UNIV xs ys)" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

519 
by simp 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

520 

c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

521 
notepad begin  "test code setup" 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

522 
have "List.coset [True] = set [False] \<and> 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

523 
List.coset [] \<subseteq> List.set [True, False] \<and> 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

524 
finite (List.coset [True])" 
48062
9014e78ccde2
improved code setup for card, finite, subset
Andreas Lochbihler
parents:
48060
diff
changeset

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

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

527 

51139
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

528 
hide_const (open) card' finite' subset' eq_set 
c8e3cf3520b3
partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code;
Andreas Lochbihler
parents:
51116
diff
changeset

529 

48051  530 
end 
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49689
diff
changeset

531 