author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47231  3ff8c79a9e2f 
child 48123  104e5fccea12 
permissions  rwrr 
31596  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26348  2 

3 
header {* Finite types as explicit enumerations *} 

4 

5 
theory Enum 

40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
40649
diff
changeset

6 
imports Map String 
26348  7 
begin 
8 

9 
subsection {* Class @{text enum} *} 

10 

29797  11 
class enum = 
26348  12 
fixes enum :: "'a list" 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

13 
fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

14 
fixes enum_ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" 
33635  15 
assumes UNIV_enum: "UNIV = set enum" 
26444  16 
and enum_distinct: "distinct enum" 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

17 
assumes enum_all : "enum_all P = (\<forall> x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

18 
assumes enum_ex : "enum_ex P = (\<exists> x. P x)" 
26348  19 
begin 
20 

29797  21 
subclass finite proof 
22 
qed (simp add: UNIV_enum) 

26444  23 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

24 
lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum .. 
26444  25 

40683  26 
lemma in_enum: "x \<in> set enum" 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

27 
unfolding enum_UNIV by auto 
26348  28 

29 
lemma enum_eq_I: 

30 
assumes "\<And>x. x \<in> set xs" 

31 
shows "set enum = set xs" 

32 
proof  

33 
from assms UNIV_eq_I have "UNIV = set xs" by auto 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

34 
with enum_UNIV show ?thesis by simp 
26348  35 
qed 
36 

37 
end 

38 

39 

40 
subsection {* Equality and order on functions *} 

41 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

42 
instantiation "fun" :: (enum, equal) equal 
26513  43 
begin 
26348  44 

26513  45 
definition 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

46 
"HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)" 
26513  47 

31464  48 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

49 
qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff) 
26513  50 

51 
end 

26348  52 

40898
882e860a1e83
changed order of lemmas to overwrite the general code equation with the nbespecific one
bulwahn
parents:
40683
diff
changeset

53 
lemma [code]: 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

54 
"HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

55 
by (auto simp add: equal enum_all fun_eq_iff) 
40898
882e860a1e83
changed order of lemmas to overwrite the general code equation with the nbespecific one
bulwahn
parents:
40683
diff
changeset

56 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

57 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

58 
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

59 
by (fact equal_refl) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

60 

28562  61 
lemma order_fun [code]: 
26348  62 
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order" 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

63 
shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

64 
and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

65 
by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le) 
26968  66 

67 

68 
subsection {* Quantifiers *} 

69 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

70 
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

71 
by (simp add: enum_all) 
26968  72 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

73 
lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

74 
by (simp add: enum_ex) 
26348  75 

40652  76 
lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum" 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

77 
unfolding list_ex1_iff enum_UNIV by auto 
40652  78 

26348  79 

80 
subsection {* Default instances *} 

81 

26444  82 
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where 
83 
"n_lists 0 xs = [[]]" 

84 
 "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))" 

85 

86 
lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])" 

87 
by (induct n) simp_all 

88 

89 
lemma length_n_lists: "length (n_lists n xs) = length xs ^ n" 

33639
603320b93668
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
hoelzl
parents:
33635
diff
changeset

90 
by (induct n) (auto simp add: length_concat o_def listsum_triv) 
26444  91 

92 
lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" 

93 
by (induct n arbitrary: ys) auto 

94 

95 
lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

96 
proof (rule set_eqI) 
26444  97 
fix ys :: "'a list" 
98 
show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}" 

99 
proof  

100 
have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n" 

101 
by (induct n arbitrary: ys) auto 

102 
moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs" 

103 
by (induct n arbitrary: ys) auto 

104 
moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)" 

105 
by (induct ys) auto 

106 
ultimately show ?thesis by auto 

107 
qed 

108 
qed 

109 

110 
lemma distinct_n_lists: 

111 
assumes "distinct xs" 

112 
shows "distinct (n_lists n xs)" 

113 
proof (rule card_distinct) 

114 
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card) 

115 
have "card (set (n_lists n xs)) = card (set xs) ^ n" 

116 
proof (induct n) 

117 
case 0 then show ?case by simp 

118 
next 

119 
case (Suc n) 

120 
moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs) 

121 
= (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))" 

122 
by (rule card_UN_disjoint) auto 

123 
moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)" 

124 
by (rule card_image) (simp add: inj_on_def) 

125 
ultimately show ?case by auto 

126 
qed 

127 
also have "\<dots> = length xs ^ n" by (simp add: card_length) 

128 
finally show "card (set (n_lists n xs)) = length (n_lists n xs)" 

129 
by (simp add: length_n_lists) 

130 
qed 

131 

132 
lemma map_of_zip_enum_is_Some: 

133 
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)" 

134 
shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y" 

135 
proof  

136 
from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow> 

137 
(\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)" 

138 
by (auto intro!: map_of_zip_is_Some) 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

139 
then show ?thesis using enum_UNIV by auto 
26444  140 
qed 
141 

142 
lemma map_of_zip_enum_inject: 

143 
fixes xs ys :: "'b\<Colon>enum list" 

144 
assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)" 

145 
"length ys = length (enum \<Colon> 'a\<Colon>enum list)" 

146 
and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)" 

147 
shows "xs = ys" 

148 
proof  

149 
have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)" 

150 
proof 

151 
fix x :: 'a 

152 
from length map_of_zip_enum_is_Some obtain y1 y2 

153 
where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1" 

154 
and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast 

47230  155 
moreover from map_of 
156 
have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)" 

26444  157 
by (auto dest: fun_cong) 
158 
ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x" 

159 
by simp 

160 
qed 

161 
with length enum_distinct show "xs = ys" by (rule map_of_zip_inject) 

162 
qed 

163 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

164 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

165 
all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

166 
where 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

167 
"all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

168 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

169 
lemma [code]: 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

170 
"all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n  1)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

171 
unfolding all_n_lists_def enum_all 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

172 
by (cases n) (auto simp add: enum_UNIV) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

173 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

174 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

175 
ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

176 
where 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

177 
"ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

178 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

179 
lemma [code]: 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

180 
"ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n  1)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

181 
unfolding ex_n_lists_def enum_ex 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

182 
by (cases n) (auto simp add: enum_UNIV) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

183 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

184 

26444  185 
instantiation "fun" :: (enum, enum) enum 
186 
begin 

187 

188 
definition 

37765  189 
"enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)" 
26444  190 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

191 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

192 
"enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

193 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

194 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

195 
"enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

196 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

197 

26444  198 
instance proof 
199 
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)" 

200 
proof (rule UNIV_eq_I) 

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

202 
have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))" 

40683  203 
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
26444  204 
then show "f \<in> set enum" 
40683  205 
by (auto simp add: enum_fun_def set_n_lists intro: in_enum) 
26444  206 
qed 
207 
next 

208 
from map_of_zip_enum_inject 

209 
show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)" 

210 
by (auto intro!: inj_onI simp add: enum_fun_def 

211 
distinct_map distinct_n_lists enum_distinct set_n_lists enum_all) 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

212 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

213 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

214 
show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

215 
proof 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

216 
assume "enum_all P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

217 
show "\<forall>x. P x" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

218 
proof 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

219 
fix f :: "'a \<Rightarrow> 'b" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

220 
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

221 
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

222 
from `enum_all P` have "P (the \<circ> map_of (zip enum (map f enum)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

223 
unfolding enum_all_fun_def all_n_lists_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

224 
apply (simp add: set_n_lists) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

225 
apply (erule_tac x="map f enum" in allE) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

226 
apply (auto intro!: in_enum) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

227 
done 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

228 
from this f show "P f" by auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

229 
qed 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

230 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

231 
assume "\<forall>x. P x" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

232 
from this show "enum_all P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

233 
unfolding enum_all_fun_def all_n_lists_def by auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

234 
qed 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

235 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

236 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

237 
show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

238 
proof 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

239 
assume "enum_ex P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

240 
from this show "\<exists>x. P x" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

241 
unfolding enum_ex_fun_def ex_n_lists_def by auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

242 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

243 
assume "\<exists>x. P x" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

244 
from this obtain f where "P f" .. 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

245 
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

246 
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

247 
from `P f` this have "P (the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

248 
by auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

249 
from this show "enum_ex P" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

250 
unfolding enum_ex_fun_def ex_n_lists_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

251 
apply (auto simp add: set_n_lists) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

252 
apply (rule_tac x="map f enum" in exI) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

253 
apply (auto intro!: in_enum) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

254 
done 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

255 
qed 
26444  256 
qed 
257 

258 
end 

259 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37765
diff
changeset

260 
lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list) 
28245
9767dd8e1e54
celver code lemma avoid type ambiguity problem with Haskell
haftmann
parents:
27487
diff
changeset

261 
in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))" 
9767dd8e1e54
celver code lemma avoid type ambiguity problem with Haskell
haftmann
parents:
27487
diff
changeset

262 
by (simp add: enum_fun_def Let_def) 
26444  263 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

264 
lemma enum_all_fun_code [code]: 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

265 
"enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

266 
in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

267 
by (simp add: enum_all_fun_def Let_def) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

268 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

269 
lemma enum_ex_fun_code [code]: 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

270 
"enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

271 
in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

272 
by (simp add: enum_ex_fun_def Let_def) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

273 

26348  274 
instantiation unit :: enum 
275 
begin 

276 

277 
definition 

278 
"enum = [()]" 

279 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

280 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

281 
"enum_all P = P ()" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

282 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

283 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

284 
"enum_ex P = P ()" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

285 

31464  286 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

287 
qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust) 
26348  288 

289 
end 

290 

291 
instantiation bool :: enum 

292 
begin 

293 

294 
definition 

295 
"enum = [False, True]" 

296 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

297 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

298 
"enum_all P = (P False \<and> P True)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

299 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

300 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

301 
"enum_ex P = (P False \<or> P True)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

302 

31464  303 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

304 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

305 
show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

306 
unfolding enum_all_bool_def by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

307 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

308 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

309 
show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

310 
unfolding enum_ex_bool_def by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

311 
qed (auto simp add: enum_bool_def UNIV_bool) 
26348  312 

313 
end 

314 

315 
primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where 

316 
"product [] _ = []" 

317 
 "product (x#xs) ys = map (Pair x) ys @ product xs ys" 

318 

319 
lemma product_list_set: 

320 
"set (product xs ys) = set xs \<times> set ys" 

321 
by (induct xs) auto 

322 

26444  323 
lemma distinct_product: 
324 
assumes "distinct xs" and "distinct ys" 

325 
shows "distinct (product xs ys)" 

326 
using assms by (induct xs) 

327 
(auto intro: inj_onI simp add: product_list_set distinct_map) 

328 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37601
diff
changeset

329 
instantiation prod :: (enum, enum) enum 
26348  330 
begin 
331 

332 
definition 

333 
"enum = product enum enum" 

334 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

335 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

336 
"enum_all P = enum_all (%x. enum_all (%y. P (x, y)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

337 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

338 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

339 
"enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

340 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

341 

26348  342 
instance by default 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

343 
(simp_all add: enum_prod_def product_list_set distinct_product 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

344 
enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex) 
26348  345 

346 
end 

347 

37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37601
diff
changeset

348 
instantiation sum :: (enum, enum) enum 
26348  349 
begin 
350 

351 
definition 

352 
"enum = map Inl enum @ map Inr enum" 

353 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

354 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

355 
"enum_all P = (enum_all (%x. P (Inl x)) \<and> enum_all (%x. P (Inr x)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

356 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

357 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

358 
"enum_ex P = (enum_ex (%x. P (Inl x)) \<or> enum_ex (%x. P (Inr x)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

359 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

360 
instance proof 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

361 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

362 
show "enum_all (P :: ('a + 'b) \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

363 
unfolding enum_all_sum_def enum_all 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

364 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

365 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

366 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

367 
show "enum_ex (P :: ('a + 'b) \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

368 
unfolding enum_ex_sum_def enum_ex 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

369 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

370 
qed (auto simp add: enum_UNIV enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct) 
26348  371 

372 
end 

373 

374 
instantiation nibble :: enum 

375 
begin 

376 

377 
definition 

378 
"enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, 

379 
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" 

380 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

381 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

382 
"enum_all P = (P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

383 
\<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

384 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

385 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

386 
"enum_ex P = (P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

387 
\<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

388 

31464  389 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

390 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

391 
show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

392 
unfolding enum_all_nibble_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

393 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

394 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

395 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

396 
show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

397 
unfolding enum_ex_nibble_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

398 
by (auto, case_tac x) auto 
31464  399 
qed (simp_all add: enum_nibble_def UNIV_nibble) 
26348  400 

401 
end 

402 

403 
instantiation char :: enum 

404 
begin 

405 

406 
definition 

37765  407 
"enum = map (split Char) (product enum enum)" 
26444  408 

31482  409 
lemma enum_chars [code]: 
410 
"enum = chars" 

411 
unfolding enum_char_def chars_def enum_nibble_def by simp 

26348  412 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

413 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

414 
"enum_all P = list_all P chars" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

415 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

416 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

417 
"enum_ex P = list_ex P chars" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

418 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

419 
lemma set_enum_char: "set (enum :: char list) = UNIV" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

420 
by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric]) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

421 

31464  422 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

423 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

424 
show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

425 
unfolding enum_all_char_def enum_chars[symmetric] 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

426 
by (auto simp add: list_all_iff set_enum_char) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

427 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

428 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

429 
show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

430 
unfolding enum_ex_char_def enum_chars[symmetric] 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

431 
by (auto simp add: list_ex_iff set_enum_char) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

432 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

433 
show "distinct (enum :: char list)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

434 
by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct) 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

435 
qed (auto simp add: set_enum_char) 
26348  436 

437 
end 

438 

29024  439 
instantiation option :: (enum) enum 
440 
begin 

441 

442 
definition 

443 
"enum = None # map Some enum" 

444 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

445 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

446 
"enum_all P = (P None \<and> enum_all (%x. P (Some x)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

447 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

448 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

449 
"enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

450 

31464  451 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

452 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

453 
show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

454 
unfolding enum_all_option_def enum_all 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

455 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

456 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

457 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

458 
show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

459 
unfolding enum_ex_option_def enum_ex 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

460 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

461 
qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct) 
45963
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

462 
end 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

463 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

464 
primrec sublists :: "'a list \<Rightarrow> 'a list list" where 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

465 
"sublists [] = [[]]" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

466 
 "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

467 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

468 
lemma length_sublists: 
47221
7205eb4a0a05
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
huffman
parents:
46361
diff
changeset

469 
"length (sublists xs) = 2 ^ length xs" 
45963
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

470 
by (induct xs) (simp_all add: Let_def) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

471 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

472 
lemma sublists_powset: 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

473 
"set ` set (sublists xs) = Pow (set xs)" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

474 
proof  
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

475 
have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

476 
by (auto simp add: image_def) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

477 
have "set (map set (sublists xs)) = Pow (set xs)" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

478 
by (induct xs) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

479 
(simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

480 
then show ?thesis by simp 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

481 
qed 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

482 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

483 
lemma distinct_set_sublists: 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

484 
assumes "distinct xs" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

485 
shows "distinct (map set (sublists xs))" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

486 
proof (rule card_distinct) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

487 
have "finite (set xs)" by rule 
47221
7205eb4a0a05
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
huffman
parents:
46361
diff
changeset

488 
then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow) 
45963
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

489 
with assms distinct_card [of xs] 
47221
7205eb4a0a05
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
huffman
parents:
46361
diff
changeset

490 
have "card (Pow (set xs)) = 2 ^ length xs" by simp 
45963
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

491 
then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

492 
by (simp add: sublists_powset length_sublists) 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

493 
qed 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

494 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

495 
instantiation set :: (enum) enum 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

496 
begin 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

497 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

498 
definition 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

499 
"enum = map set (sublists enum)" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

500 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

501 
definition 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

502 
"enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

503 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

504 
definition 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

505 
"enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

506 

1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

507 
instance proof 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

508 
qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

509 
enum_distinct enum_UNIV) 
29024  510 

511 
end 

512 

45963
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

513 

40647  514 
subsection {* Small finite types *} 
515 

516 
text {* We define small finite types for the use in Quickcheck *} 

517 

518 
datatype finite_1 = a\<^isub>1 

519 

40900
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

520 
notation (output) a\<^isub>1 ("a\<^isub>1") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

521 

40647  522 
instantiation finite_1 :: enum 
523 
begin 

524 

525 
definition 

526 
"enum = [a\<^isub>1]" 

527 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

528 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

529 
"enum_all P = P a\<^isub>1" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

530 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

531 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

532 
"enum_ex P = P a\<^isub>1" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

533 

40647  534 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

535 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

536 
show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

537 
unfolding enum_all_finite_1_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

538 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

539 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

540 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

541 
show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

542 
unfolding enum_ex_finite_1_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

543 
by (auto, case_tac x) auto 
40647  544 
qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust) 
545 

29024  546 
end 
40647  547 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

548 
instantiation finite_1 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

549 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

550 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

551 
definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

552 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

553 
"less_eq_finite_1 x y = True" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

554 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

555 
definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

556 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

557 
"less_finite_1 x y = False" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

558 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

559 
instance 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

560 
apply (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

561 
apply (auto simp add: less_finite_1_def less_eq_finite_1_def) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

562 
apply (metis finite_1.exhaust) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

563 
done 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

564 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

565 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

566 

41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
41078
diff
changeset

567 
hide_const (open) a\<^isub>1 
40657  568 

40647  569 
datatype finite_2 = a\<^isub>1  a\<^isub>2 
570 

40900
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

571 
notation (output) a\<^isub>1 ("a\<^isub>1") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

572 
notation (output) a\<^isub>2 ("a\<^isub>2") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

573 

40647  574 
instantiation finite_2 :: enum 
575 
begin 

576 

577 
definition 

578 
"enum = [a\<^isub>1, a\<^isub>2]" 

579 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

580 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

581 
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

582 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

583 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

584 
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

585 

40647  586 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

587 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

588 
show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

589 
unfolding enum_all_finite_2_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

590 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

591 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

592 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

593 
show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

594 
unfolding enum_ex_finite_2_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

595 
by (auto, case_tac x) auto 
40647  596 
qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust) 
597 

598 
end 

599 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

600 
instantiation finite_2 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

601 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

602 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

603 
definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

604 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

605 
"less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

606 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

607 
definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

608 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

609 
"less_eq_finite_2 x y = ((x = y) \<or> (x < y))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

610 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

611 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

612 
instance 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

613 
apply (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

614 
apply (auto simp add: less_finite_2_def less_eq_finite_2_def) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

615 
apply (metis finite_2.distinct finite_2.nchotomy)+ 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

616 
done 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

617 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

618 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

619 

41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
41078
diff
changeset

620 
hide_const (open) a\<^isub>1 a\<^isub>2 
40657  621 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

622 

40647  623 
datatype finite_3 = a\<^isub>1  a\<^isub>2  a\<^isub>3 
624 

40900
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

625 
notation (output) a\<^isub>1 ("a\<^isub>1") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

626 
notation (output) a\<^isub>2 ("a\<^isub>2") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

627 
notation (output) a\<^isub>3 ("a\<^isub>3") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

628 

40647  629 
instantiation finite_3 :: enum 
630 
begin 

631 

632 
definition 

633 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]" 

634 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

635 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

636 
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

637 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

638 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

639 
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

640 

40647  641 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

642 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

643 
show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

644 
unfolding enum_all_finite_3_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

645 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

646 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

647 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

648 
show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

649 
unfolding enum_ex_finite_3_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

650 
by (auto, case_tac x) auto 
40647  651 
qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust) 
652 

653 
end 

654 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

655 
instantiation finite_3 :: linorder 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

656 
begin 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

657 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

658 
definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

659 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

660 
"less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

661 
 a\<^isub>2 => (y = a\<^isub>3) a\<^isub>3 => False)" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

662 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

663 
definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

664 
where 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

665 
"less_eq_finite_3 x y = ((x = y) \<or> (x < y))" 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

666 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

667 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

668 
instance proof (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

669 
qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

670 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

671 
end 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

672 

41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
41078
diff
changeset

673 
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 
40657  674 

40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

675 

40647  676 
datatype finite_4 = a\<^isub>1  a\<^isub>2  a\<^isub>3  a\<^isub>4 
677 

40900
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

678 
notation (output) a\<^isub>1 ("a\<^isub>1") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

679 
notation (output) a\<^isub>2 ("a\<^isub>2") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

680 
notation (output) a\<^isub>3 ("a\<^isub>3") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

681 
notation (output) a\<^isub>4 ("a\<^isub>4") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

682 

40647  683 
instantiation finite_4 :: enum 
684 
begin 

685 

686 
definition 

687 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]" 

688 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

689 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

690 
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

691 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

692 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

693 
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

694 

40647  695 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

696 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

697 
show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

698 
unfolding enum_all_finite_4_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

699 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

700 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

701 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

702 
show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

703 
unfolding enum_ex_finite_4_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

704 
by (auto, case_tac x) auto 
40647  705 
qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust) 
706 

707 
end 

708 

41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
41078
diff
changeset

709 
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 
40651
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

710 

9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

711 

40647  712 
datatype finite_5 = a\<^isub>1  a\<^isub>2  a\<^isub>3  a\<^isub>4  a\<^isub>5 
713 

40900
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

714 
notation (output) a\<^isub>1 ("a\<^isub>1") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

715 
notation (output) a\<^isub>2 ("a\<^isub>2") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

716 
notation (output) a\<^isub>3 ("a\<^isub>3") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

717 
notation (output) a\<^isub>4 ("a\<^isub>4") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

718 
notation (output) a\<^isub>5 ("a\<^isub>5") 
1d5f76d79856
adding shorter output syntax for the finite types of quickcheck
bulwahn
parents:
40898
diff
changeset

719 

40647  720 
instantiation finite_5 :: enum 
721 
begin 

722 

723 
definition 

724 
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]" 

725 

41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

726 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

727 
"enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

728 

051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

729 
definition 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

730 
"enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

731 

40647  732 
instance proof 
41078
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

733 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

734 
show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

735 
unfolding enum_all_finite_5_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

736 
by (auto, case_tac x) auto 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

737 
next 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

738 
fix P 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

739 
show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)" 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

740 
unfolding enum_ex_finite_5_def 
051251fde456
adding more efficient implementations for quantifiers in Enum
bulwahn
parents:
40900
diff
changeset

741 
by (auto, case_tac x) auto 
40647  742 
qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust) 
743 

744 
end 

745 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

746 
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

747 

41115
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

748 
subsection {* An executable THE operator on finite types *} 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

749 

2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

750 
definition 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

751 
[code del]: "enum_the P = The P" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

752 

2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

753 
lemma [code]: 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

754 
"The P = (case filter P enum of [x] => x  _ => enum_the P)" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

755 
proof  
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

756 
{ 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

757 
fix a 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

758 
assume filter_enum: "filter P enum = [a]" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

759 
have "The P = a" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

760 
proof (rule the_equality) 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

761 
fix x 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

762 
assume "P x" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

763 
show "x = a" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

764 
proof (rule ccontr) 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

765 
assume "x \<noteq> a" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

766 
from filter_enum obtain us vs 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

767 
where enum_eq: "enum = us @ [a] @ vs" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

768 
and "\<forall> x \<in> set us. \<not> P x" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

769 
and "\<forall> x \<in> set vs. \<not> P x" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

770 
and "P a" 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

771 
by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric]) 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

772 
with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

773 
qed 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

774 
next 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

775 
from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff) 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

776 
qed 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

777 
} 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

778 
from this show ?thesis 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

779 
unfolding enum_the_def by (auto split: list.split) 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

780 
qed 
2c362ff5daf4
adding an executable THE operator on finite types
bulwahn
parents:
41085
diff
changeset

781 

46329  782 
code_abort enum_the 
46336
39fe503602fb
evaluation of THE with a nonsingleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
bulwahn
parents:
46329
diff
changeset

783 
code_const enum_the (Eval "(fn p => raise Match)") 
46329  784 

785 
subsection {* Further operations on finite types *} 

786 

787 
lemma [code]: 

788 
"Collect P = set (filter P enum)" 

789 
by (auto simp add: enum_UNIV) 

45140  790 

46357  791 
lemma tranclp_unfold [code, no_atp]: 
792 
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" 

793 
by (simp add: trancl_def) 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

794 

46359  795 
lemma rtranclp_rtrancl_eq[code, no_atp]: 
796 
"rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})" 

797 
unfolding rtrancl_def by auto 

798 

46358  799 
lemma max_ext_eq[code]: 
800 
"max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X > (EX xa : Y. (x, xa) : R))}" 

801 
by (auto simp add: max_ext.simps) 

802 

46361  803 
lemma max_extp_eq[code]: 
804 
"max_extp r x y = ((x, y) : max_ext {(x, y). r x y})" 

805 
unfolding max_ext_def by auto 

806 

807 
lemma mlex_eq[code]: 

808 
"f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}" 

809 
unfolding mlex_prod_def by auto 

810 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

811 
subsection {* Executable accessible part *} 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

812 
(* FIXME: should be moved somewhere else !? *) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

813 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

814 
subsubsection {* Finite monotone eventually stable sequences *} 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

815 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

816 
lemma finite_mono_remains_stable_implies_strict_prefix: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

817 
fixes f :: "nat \<Rightarrow> 'a::order" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

818 
assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

819 
shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

820 
using assms 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

821 
proof  
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

822 
have "\<exists>n. f n = f (Suc n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

823 
proof (rule ccontr) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

824 
assume "\<not> ?thesis" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

825 
then have "\<And>n. f n \<noteq> f (Suc n)" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

826 
then have "\<And>n. f n < f (Suc n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

827 
using `mono f` by (auto simp: le_less mono_iff_le_Suc) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

828 
with lift_Suc_mono_less_iff[of f] 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

829 
have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

830 
then have "inj f" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

831 
by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

832 
with `finite (range f)` have "finite (UNIV::nat set)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

833 
by (rule finite_imageD) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

834 
then show False by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

835 
qed 
47230  836 
then obtain n where n: "f n = f (Suc n)" .. 
46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

837 
def N \<equiv> "LEAST n. f n = f (Suc n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

838 
have N: "f N = f (Suc N)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

839 
unfolding N_def using n by (rule LeastI) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

840 
show ?thesis 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

841 
proof (intro exI[of _ N] conjI allI impI) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

842 
fix n assume "N \<le> n" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

843 
then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

844 
proof (induct rule: dec_induct) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

845 
case (step n) then show ?case 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

846 
using eq[rule_format, of "n  1"] N 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

847 
by (cases n) (auto simp add: le_Suc_eq) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

848 
qed simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

849 
from this[of n] `N \<le> n` show "f N = f n" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

850 
next 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

851 
fix n m :: nat assume "m < n" "n \<le> N" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

852 
then show "f m < f n" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

853 
proof (induct rule: less_Suc_induct[consumes 1]) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

854 
case (1 i) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

855 
then have "i < N" by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

856 
then have "f i \<noteq> f (Suc i)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

857 
unfolding N_def by (rule not_less_Least) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

858 
with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

859 
qed auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

860 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

861 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

862 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

863 
lemma finite_mono_strict_prefix_implies_finite_fixpoint: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

864 
fixes f :: "nat \<Rightarrow> 'a set" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

865 
assumes S: "\<And>i. f i \<subseteq> S" "finite S" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

866 
and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

867 
shows "f (card S) = (\<Union>n. f n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

868 
proof  
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

869 
from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto 
45117
3911cf09899a
adding code equations for cardinality and (reflexive) transitive closure on finite types
bulwahn
parents:
41115
diff
changeset

870 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

871 
{ fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

872 
proof (induct i) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

873 
case 0 then show ?case by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

874 
next 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

875 
case (Suc i) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

876 
with inj[rule_format, of "Suc i" i] 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

877 
have "(f i) \<subset> (f (Suc i))" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

878 
moreover have "finite (f (Suc i))" using S by (rule finite_subset) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

879 
ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

880 
with Suc show ?case using inj by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

881 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

882 
} 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

883 
then have "N \<le> card (f N)" by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

884 
also have "\<dots> \<le> card S" using S by (intro card_mono) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

885 
finally have "f (card S) = f N" using eq by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

886 
then show ?thesis using eq inj[rule_format, of N] 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

887 
apply auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

888 
apply (case_tac "n < N") 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

889 
apply (auto simp: not_less) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

890 
done 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

891 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

892 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

893 
subsubsection {* Bounded accessible part *} 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

894 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

895 
fun bacc :: "('a * 'a) set => nat => 'a set" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

896 
where 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

897 
"bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

898 
 "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r > y : bacc r n})" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

899 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

900 
lemma bacc_subseteq_acc: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

901 
"bacc r n \<subseteq> acc r" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

902 
by (induct n) (auto intro: acc.intros) 
40657  903 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

904 
lemma bacc_mono: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

905 
"n <= m ==> bacc r n \<subseteq> bacc r m" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

906 
by (induct rule: dec_induct) auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

907 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

908 
lemma bacc_upper_bound: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

909 
"bacc (r :: ('a * 'a) set) (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

910 
proof  
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

911 
have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

912 
moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

913 
moreover have "finite (range (bacc r))" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

914 
ultimately show ?thesis 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

915 
by (intro finite_mono_strict_prefix_implies_finite_fixpoint) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

916 
(auto intro: finite_mono_remains_stable_implies_strict_prefix simp add: enum_UNIV) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

917 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

918 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

919 
lemma acc_subseteq_bacc: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

920 
assumes "finite r" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

921 
shows "acc r \<subseteq> (UN n. bacc r n)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

922 
proof 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

923 
fix x 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

924 
assume "x : acc r" 
47230  925 
then have "\<exists> n. x : bacc r n" 
926 
proof (induct x arbitrary: rule: acc.induct) 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

927 
case (accI x) 
47230  928 
then have "\<forall>y. \<exists> n. (y, x) \<in> r > y : bacc r n" by simp 
929 
from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" .. 

930 
obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n" 

931 
proof 

46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

932 
fix y assume y: "(y, x) : r" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

933 
with n have "y : bacc r (n y)" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

934 
moreover have "n y <= Max ((%(y, x). n y) ` r)" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

935 
using y `finite r` by (auto intro!: Max_ge) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

936 
note bacc_mono[OF this, of r] 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

937 
ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

938 
qed 
47230  939 
then show ?case 
46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

940 
by (auto simp add: Let_def intro!: exI[of _ "Suc n"]) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

941 
qed 
47230  942 
then show "x : (UN n. bacc r n)" by auto 
46352
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

943 
qed 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

944 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

945 
lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

946 
by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

947 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

948 
definition 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

949 
[code del]: "card_UNIV = card UNIV" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

950 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

951 
lemma [code]: 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

952 
"card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

953 
unfolding card_UNIV_def enum_UNIV .. 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

954 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

955 
declare acc_bacc_eq[folded card_UNIV_def, code] 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

956 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

957 
lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

958 
unfolding acc_def by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

959 

73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

960 
subsection {* Closing up *} 
40657  961 

41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
41078
diff
changeset

962 
hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5 
45117
3911cf09899a
adding code equations for cardinality and (reflexive) transitive closure on finite types
bulwahn
parents:
41115
diff
changeset

963 
hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl 
40647  964 

965 
end 