author  bulwahn 
Mon, 30 Jan 2012 13:55:20 +0100  
changeset 46357  2795607a1f40 
parent 46352  73b03235799a 
child 46358  b2a936486685 
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 

155 
moreover from map_of 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)" 

156 
by (auto dest: fun_cong) 

157 
ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x" 

158 
by simp 

159 
qed 

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

161 
qed 

162 

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

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

164 
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

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

166 
"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

167 

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

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

169 
"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

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

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

172 

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

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

174 
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

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

176 
"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

177 

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

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

179 
"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

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

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

182 

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

183 

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

186 

187 
definition 

37765  188 
"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  189 

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

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

191 
"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

192 

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

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

194 
"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

195 

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

196 

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

199 
proof (rule UNIV_eq_I) 

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

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

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

207 
from map_of_zip_enum_inject 

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

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

210 
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

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

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

213 
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

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

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

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

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

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

219 
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

220 
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

221 
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

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

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

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

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

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

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

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

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

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

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

232 
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

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

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

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

236 
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

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

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

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

240 
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

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

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

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

244 
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

245 
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

246 
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

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

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

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

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

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

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

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

254 
qed 
26444  255 
qed 
256 

257 
end 

258 

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

259 
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

260 
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

261 
by (simp add: enum_fun_def Let_def) 
26444  262 

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

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

264 
"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

265 
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

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

267 

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

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

269 
"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

270 
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

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

272 

26348  273 
instantiation unit :: enum 
274 
begin 

275 

276 
definition 

277 
"enum = [()]" 

278 

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

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

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

281 

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

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

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

284 

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

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

288 
end 

289 

290 
instantiation bool :: enum 

291 
begin 

292 

293 
definition 

294 
"enum = [False, True]" 

295 

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

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

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

298 

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

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

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

301 

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

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

304 
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

305 
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

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

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

308 
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

309 
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

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

312 
end 

313 

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

315 
"product [] _ = []" 

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

317 

318 
lemma product_list_set: 

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

320 
by (induct xs) auto 

321 

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

324 
shows "distinct (product xs ys)" 

325 
using assms by (induct xs) 

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

327 

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

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

331 
definition 

332 
"enum = product enum enum" 

333 

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

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

335 
"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

336 

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

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

338 
"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

339 

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

340 

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

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

343 
enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex) 
26348  344 

345 
end 

346 

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

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

350 
definition 

351 
"enum = map Inl enum @ map Inr enum" 

352 

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

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

354 
"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

355 

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

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

357 
"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

358 

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

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

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

361 
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

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

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

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

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

366 
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

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

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

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

371 
end 

372 

373 
instantiation nibble :: enum 

374 
begin 

375 

376 
definition 

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

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

379 

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

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

381 
"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

382 
\<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

383 

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

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

385 
"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

386 
\<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

387 

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

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

390 
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

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

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

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

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

395 
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

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

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

400 
end 

401 

402 
instantiation char :: enum 

403 
begin 

404 

405 
definition 

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

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

410 
unfolding enum_char_def chars_def enum_nibble_def by simp 

26348  411 

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

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

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

414 

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

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

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

417 

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

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

419 
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

420 

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

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

423 
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

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

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

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

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

428 
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

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

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

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

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

433 
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

434 
qed (auto simp add: set_enum_char) 
26348  435 

436 
end 

437 

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

440 

441 
definition 

442 
"enum = None # map Some enum" 

443 

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

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

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

446 

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

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

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

449 

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

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

452 
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

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

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

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

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

457 
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

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

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

460 
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

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

462 

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

463 
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

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

465 
 "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

466 

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

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

468 
"length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

469 
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

470 

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

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

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

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

474 
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

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

476 
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

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

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

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

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

481 

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

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

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

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

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

486 
have "finite (set xs)" by rule 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

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

488 
with assms distinct_card [of xs] 
1c7e6454883e
enum type class instance for `set`; dropped misfitting code lemma for trancl
haftmann
parents:
45144
diff
changeset

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

490 
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

491 
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

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

493 

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

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

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

496 

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

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

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

499 

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

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

501 
"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

502 

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

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

504 
"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

505 

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

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

507 
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

508 
enum_distinct enum_UNIV) 
29024  509 

510 
end 

511 

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

512 

40647  513 
subsection {* Small finite types *} 
514 

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

516 

517 
datatype finite_1 = a\<^isub>1 

518 

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

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

520 

40647  521 
instantiation finite_1 :: enum 
522 
begin 

523 

524 
definition 

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

526 

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

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

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

529 

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

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

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

532 

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

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

535 
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

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

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

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

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

540 
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

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

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

29024  545 
end 
40647  546 

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

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

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

549 

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

550 
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

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

552 
"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

553 

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

554 
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

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

556 
"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

557 

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

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

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

560 
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

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

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

563 

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

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

565 

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

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

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

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

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

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

572 

40647  573 
instantiation finite_2 :: enum 
574 
begin 

575 

576 
definition 

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

578 

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

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

580 
"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

581 

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

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

583 
"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

584 

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

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

587 
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

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

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

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

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

592 
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

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

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

597 
end 

598 

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

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

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

601 

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

602 
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

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

604 
"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

605 

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

606 
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

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

608 
"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

609 

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 
instance 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

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

613 
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

614 
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

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

616 

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

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

618 

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

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

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

621 

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

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

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

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

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

627 

40647  628 
instantiation finite_3 :: enum 
629 
begin 

630 

631 
definition 

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

633 

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

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

635 
"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

636 

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

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

638 
"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

639 

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

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

642 
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

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

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

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

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

647 
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

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

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

652 
end 

653 

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

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

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

656 

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

657 
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

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

659 
"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

660 
 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

661 

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

662 
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

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

664 
"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

665 

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 
instance proof (intro_classes) 
9752ba7348b5
adding code equation for function equality; adding some instantiations for the finite types
bulwahn
parents:
40650
diff
changeset

668 
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

669 

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

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

671 

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

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

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

674 

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

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

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

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

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

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

681 

40647  682 
instantiation finite_4 :: enum 
683 
begin 

684 

685 
definition 

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

687 

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

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

689 
"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

690 

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

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

692 
"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

693 

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

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

696 
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

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

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

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

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

701 
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

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

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

706 
end 

707 

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

708 
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

709 

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

710 

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

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

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

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

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

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

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

718 

40647  719 
instantiation finite_5 :: enum 
720 
begin 

721 

722 
definition 

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

724 

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

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

726 
"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

727 

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

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

729 
"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

730 

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

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

733 
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

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

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

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

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

738 
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

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

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

743 
end 

744 

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

745 
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

746 

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

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

748 

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

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

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

751 

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

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

753 
"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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

770 
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

771 
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

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

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

774 
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

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

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

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

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

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

780 

46329  781 
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

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

784 
subsection {* Further operations on finite types *} 

785 

786 
lemma [code]: 

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

788 
by (auto simp add: enum_UNIV) 

45140  789 

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

792 
by (simp add: trancl_def) 

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

793 

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

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

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

796 

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

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

798 

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

799 
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

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

801 
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

802 
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

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

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

805 
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

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

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

808 
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

809 
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

810 
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

811 
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

812 
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

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

814 
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

815 
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

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

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

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

819 
then guess n .. note n = this 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

820 
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

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

822 
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

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

824 
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

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

826 
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

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

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

829 
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

830 
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

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

832 
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

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

834 
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

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

836 
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

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

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

839 
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

840 
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

841 
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

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

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

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

845 

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

846 
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

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

848 
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

849 
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

850 
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

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

852 
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

853 

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

854 
{ 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

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

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

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

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

859 
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

860 
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

861 
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

862 
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

863 
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

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

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

866 
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

867 
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

868 
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

869 
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

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

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

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

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

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

875 

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

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

877 

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

878 
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

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

880 
"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

881 
 "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

882 

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

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

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

885 
by (induct n) (auto intro: acc.intros) 
40657  886 

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

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

888 
"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

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

890 

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

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

892 
"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

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

894 
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

895 
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

896 
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

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

898 
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

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

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

901 

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

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

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

904 
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

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

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

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

908 
from this have "\<exists> n. x : bacc r n" 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

909 
proof (induct x arbitrary: n rule: acc.induct) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

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

911 
from accI have "\<forall> y. \<exists> n. (y, x) \<in> r > y : bacc r n" by simp 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

912 
from choice[OF this] guess n .. note n = this 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

913 
have "\<exists> n. \<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

914 
proof (safe intro!: exI[of _ "Max ((%(y,x). n y)`r)"]) 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

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

916 
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

917 
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

918 
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

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

920 
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

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

922 
from this guess n .. 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

923 
from this show ?case 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

924 
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

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

926 
thus "x : (UN n. bacc r n)" by auto 
73b03235799a
an executable version of accessible part (only for finite types yet)
bulwahn
parents:
46336
diff
changeset

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

928 

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

929 
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

930 
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

931 

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

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

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

934 

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

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

936 
"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

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

938 

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

939 
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

940 

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

941 
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

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

943 

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

944 
subsection {* Closing up *} 
40657  945 

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

946 
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

947 
hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl 
40647  948 

949 
end 