author  blanchet 
Wed, 03 Sep 2014 00:06:32 +0200  
changeset 58158  d2cb7cbb3aaa 
parent 58155  14dda84afbb3 
child 58160  e4965b677ba9 
permissions  rwrr 
26169  1 
(* Title: HOL/Library/Countable.thy 
26350  2 
Author: Alexander Krauss, TU Muenchen 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

3 
Author: Brian Huffman, Portland State University 
26169  4 
*) 
5 

6 
header {* Encoding (almost) everything into natural numbers *} 

7 

8 
theory Countable 

35700  9 
imports Main Rat Nat_Bijection 
26169  10 
begin 
11 

12 
subsection {* The class of countable types *} 

13 

29797  14 
class countable = 
26169  15 
assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" 
16 

17 
lemma countable_classI: 

18 
fixes f :: "'a \<Rightarrow> nat" 

19 
assumes "\<And>x y. f x = f y \<Longrightarrow> x = y" 

20 
shows "OFCLASS('a, countable_class)" 

21 
proof (intro_classes, rule exI) 

22 
show "inj f" 

23 
by (rule injI [OF assms]) assumption 

24 
qed 

25 

26 

26585  27 
subsection {* Conversion functions *} 
26169  28 

29 
definition to_nat :: "'a\<Colon>countable \<Rightarrow> nat" where 

30 
"to_nat = (SOME f. inj f)" 

31 

32 
definition from_nat :: "nat \<Rightarrow> 'a\<Colon>countable" where 

33 
"from_nat = inv (to_nat \<Colon> 'a \<Rightarrow> nat)" 

34 

35 
lemma inj_to_nat [simp]: "inj to_nat" 

36 
by (rule exE_some [OF ex_inj]) (simp add: to_nat_def) 

37 

43992  38 
lemma inj_on_to_nat[simp, intro]: "inj_on to_nat S" 
39 
using inj_to_nat by (auto simp: inj_on_def) 

40 

29910  41 
lemma surj_from_nat [simp]: "surj from_nat" 
42 
unfolding from_nat_def by (simp add: inj_imp_surj_inv) 

43 

26169  44 
lemma to_nat_split [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y" 
45 
using injD [OF inj_to_nat] by auto 

46 

47 
lemma from_nat_to_nat [simp]: 

48 
"from_nat (to_nat x) = x" 

49 
by (simp add: from_nat_def) 

50 

51 

52 
subsection {* Countable types *} 

53 

54 
instance nat :: countable 

35700  55 
by (rule countable_classI [of "id"]) simp 
26169  56 

57 
subclass (in finite) countable 

28823  58 
proof 
26169  59 
have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV) 
31992  60 
with finite_conv_nat_seg_image [of "UNIV::'a set"] 
26169  61 
obtain n and f :: "nat \<Rightarrow> 'a" 
62 
where "UNIV = f ` {i. i < n}" by auto 

63 
then have "surj f" unfolding surj_def by auto 

64 
then have "inj (inv f)" by (rule surj_imp_inj_inv) 

65 
then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj]) 

66 
qed 

67 

68 
text {* Pairs *} 

69 

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

70 
instance prod :: (countable, countable) countable 
35700  71 
by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"]) 
72 
(auto simp add: prod_encode_eq) 

26169  73 

74 

75 
text {* Sums *} 

76 

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

77 
instance sum :: (countable, countable) countable 
26169  78 
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) 
79 
 Inr b \<Rightarrow> to_nat (True, to_nat b))"]) 

35700  80 
(simp split: sum.split_asm) 
26169  81 

82 

83 
text {* Integers *} 

84 

85 
instance int :: countable 

35700  86 
by (rule countable_classI [of "int_encode"]) 
87 
(simp add: int_encode_eq) 

26169  88 

89 

90 
text {* Options *} 

91 

92 
instance option :: (countable) countable 

55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
49187
diff
changeset

93 
by (rule countable_classI [of "case_option 0 (Suc \<circ> to_nat)"]) 
35700  94 
(simp split: option.split_asm) 
26169  95 

96 

97 
text {* Lists *} 

98 

99 
instance list :: (countable) countable 

35700  100 
by (rule countable_classI [of "list_encode \<circ> map to_nat"]) 
101 
(simp add: list_encode_eq) 

26169  102 

26243  103 

37652  104 
text {* Further *} 
105 

106 
instance String.literal :: countable 

57437  107 
by (rule countable_classI [of "to_nat o String.explode"]) 
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset

108 
(auto simp add: explode_inject) 
37652  109 

26243  110 
text {* Functions *} 
111 

112 
instance "fun" :: (finite, countable) countable 

113 
proof 

114 
obtain xs :: "'a list" where xs: "set xs = UNIV" 

115 
using finite_list [OF finite_UNIV] .. 

116 
show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat" 

117 
proof 

118 
show "inj (\<lambda>f. to_nat (map f xs))" 

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

119 
by (rule injI, simp add: xs fun_eq_iff) 
26243  120 
qed 
121 
qed 

122 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

123 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

124 
subsection {* The Rationals are Countably Infinite *} 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

125 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

126 
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where 
35700  127 
"nat_to_rat_surj n = (let (a,b) = prod_decode n 
128 
in Fract (int_decode a) (int_decode b))" 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

129 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

130 
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

131 
unfolding surj_def 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

132 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

133 
fix r::rat 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

134 
show "\<exists>n. r = nat_to_rat_surj n" 
35374  135 
proof (cases r) 
136 
fix i j assume [simp]: "r = Fract i j" and "j > 0" 

35700  137 
have "r = (let m = int_encode i; n = int_encode j 
138 
in nat_to_rat_surj(prod_encode (m,n)))" 

139 
by (simp add: Let_def nat_to_rat_surj_def) 

29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

140 
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

141 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

142 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

143 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

144 
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj" 
40702  145 
by (simp add: Rats_def surj_nat_to_rat_surj) 
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

146 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

147 
context field_char_0 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

148 
begin 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

149 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

150 
lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

151 
"\<rat> = range (of_rat o nat_to_rat_surj)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

152 
using surj_nat_to_rat_surj 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

153 
by (auto simp: Rats_def image_def surj_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

154 
(blast intro: arg_cong[where f = of_rat]) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

155 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

156 
lemma surj_of_rat_nat_to_rat_surj: 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

157 
"r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

158 
by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

159 

26169  160 
end 
29880
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

161 

3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

162 
instance rat :: countable 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

163 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

164 
show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

165 
proof 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

166 
have "surj nat_to_rat_surj" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

167 
by (rule surj_nat_to_rat_surj) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

168 
then show "inj (inv nat_to_rat_surj)" 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

169 
by (rule surj_imp_inj_inv) 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

170 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

171 
qed 
3dee8ff45d3d
move countability proof from Rational to Countable; add instance rat :: countable
huffman
parents:
29797
diff
changeset

172 

43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

173 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

174 
subsection {* Automatically proving countability of datatypes *} 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

175 

58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

176 
inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

177 
undefined: "finite_item undefined" 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

178 
 In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

179 
 In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

180 
 Leaf: "finite_item (Old_Datatype.Leaf a)" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

181 
 Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)" 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

182 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

183 
function 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

184 
nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item" 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

185 
where 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

186 
"nth_item 0 = undefined" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

187 
 "nth_item (Suc n) = 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

188 
(case sum_decode n of 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

189 
Inl i \<Rightarrow> 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

190 
(case sum_decode i of 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

191 
Inl j \<Rightarrow> Old_Datatype.In0 (nth_item j) 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

192 
 Inr j \<Rightarrow> Old_Datatype.In1 (nth_item j)) 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

193 
 Inr i \<Rightarrow> 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

194 
(case sum_decode i of 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

195 
Inl j \<Rightarrow> Old_Datatype.Leaf (from_nat j) 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

196 
 Inr j \<Rightarrow> 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

197 
(case prod_decode j of 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

198 
(a, b) \<Rightarrow> Old_Datatype.Scons (nth_item a) (nth_item b))))" 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

199 
by pat_completeness auto 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

200 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

201 
lemma le_sum_encode_Inl: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inl y)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

202 
unfolding sum_encode_def by simp 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

203 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

204 
lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

205 
unfolding sum_encode_def by simp 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

206 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

207 
termination 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

208 
by (relation "measure id") 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

209 
(auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric] 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

210 
le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

211 
le_prod_encode_1 le_prod_encode_2) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

212 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

213 
lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

214 
proof (induct set: finite_item) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

215 
case undefined 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

216 
have "nth_item 0 = undefined" by simp 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

217 
thus ?case .. 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

218 
next 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

219 
case (In0 x) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

220 
then obtain n where "nth_item n = x" by fast 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

221 
hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inl n))))) = Old_Datatype.In0 x" by simp 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

222 
thus ?case .. 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

223 
next 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

224 
case (In1 x) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

225 
then obtain n where "nth_item n = x" by fast 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

226 
hence "nth_item (Suc (sum_encode (Inl (sum_encode (Inr n))))) = Old_Datatype.In1 x" by simp 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

227 
thus ?case .. 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

228 
next 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

229 
case (Leaf a) 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

230 
have "nth_item (Suc (sum_encode (Inr (sum_encode (Inl (to_nat a)))))) = Old_Datatype.Leaf a" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

231 
by simp 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

232 
thus ?case .. 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

233 
next 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

234 
case (Scons x y) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

235 
then obtain i j where "nth_item i = x" and "nth_item j = y" by fast 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

236 
hence "nth_item 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

237 
(Suc (sum_encode (Inr (sum_encode (Inr (prod_encode (i, j))))))) = Old_Datatype.Scons x y" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

238 
by simp 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

239 
thus ?case .. 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

240 
qed 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

241 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

242 
theorem countable_datatype: 
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

243 
fixes Rep :: "'b \<Rightarrow> ('a::countable) Old_Datatype.item" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

244 
fixes Abs :: "('a::countable) Old_Datatype.item \<Rightarrow> 'b" 
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57437
diff
changeset

245 
fixes rep_set :: "('a::countable) Old_Datatype.item \<Rightarrow> bool" 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

246 
assumes type: "type_definition Rep Abs (Collect rep_set)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

247 
assumes finite_item: "\<And>x. rep_set x \<Longrightarrow> finite_item x" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

248 
shows "OFCLASS('b, countable_class)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

249 
proof 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

250 
def f \<equiv> "\<lambda>y. LEAST n. nth_item n = Rep y" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

251 
{ 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

252 
fix y :: 'b 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

253 
have "rep_set (Rep y)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

254 
using type_definition.Rep [OF type] by simp 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

255 
hence "finite_item (Rep y)" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

256 
by (rule finite_item) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

257 
hence "\<exists>n. nth_item n = Rep y" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

258 
by (rule nth_item_covers) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

259 
hence "nth_item (f y) = Rep y" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

260 
unfolding f_def by (rule LeastI_ex) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

261 
hence "Abs (nth_item (f y)) = y" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

262 
using type_definition.Rep_inverse [OF type] by simp 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

263 
} 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

264 
hence "inj f" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

265 
by (rule inj_on_inverseI) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

266 
thus "\<exists>f::'b \<Rightarrow> nat. inj f" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

267 
by  (rule exI) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

268 
qed 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

269 

47432  270 
ML {* 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

271 
fun countable_tac ctxt = 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

272 
SUBGOAL (fn (goal, i) => 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

273 
let 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

274 
val ty_name = 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

275 
(case goal of 
56243  276 
(_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

277 
 _ => raise Match) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

278 
val typedef_info = hd (Typedef.get_info ctxt ty_name) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

279 
val typedef_thm = #type_definition (snd typedef_info) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

280 
val pred_name = 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

281 
(case HOLogic.dest_Trueprop (concl_of typedef_thm) of 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

282 
(typedef $ rep $ abs $ (collect $ Const (n, _))) => n 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

283 
 _ => raise Match) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

284 
val induct_info = Inductive.the_inductive ctxt pred_name 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

285 
val pred_names = #names (fst induct_info) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

286 
val induct_thms = #inducts (snd induct_info) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

287 
val alist = pred_names ~~ induct_thms 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

288 
val induct_thm = the (AList.lookup (op =) alist pred_name) 
49187
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

289 
val vars = rev (Term.add_vars (Thm.prop_of induct_thm) []) 
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

290 
val thy = Proof_Context.theory_of ctxt 
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

291 
val insts = vars > map (fn (_, T) => try (Thm.cterm_of thy) 
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

292 
(Const (@{const_name Countable.finite_item}, T))) 
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

293 
val induct_thm' = Drule.instantiate' [] insts induct_thm 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

294 
val rules = @{thms finite_item.intros} 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

295 
in 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

296 
SOLVED' (fn i => EVERY 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

297 
[rtac @{thm countable_datatype} i, 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

298 
rtac typedef_thm i, 
49187
6096da55d2d6
countable_datatype method: preinstantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
huffman
parents:
47432
diff
changeset

299 
etac induct_thm' i, 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

300 
REPEAT (resolve_tac rules i ORELSE atac i)]) 1 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

301 
end) 
47432  302 
*} 
303 

304 
method_setup countable_datatype = {* 

43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

305 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt)) 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

306 
*} "prove countable class instances for datatypes" 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

307 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

308 
hide_const (open) finite_item nth_item 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

309 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

310 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

311 
subsection {* Countable datatypes *} 
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

312 

58158  313 
(* TODO: automate *) 
314 

315 
primrec encode_typerep :: "typerep \<Rightarrow> nat" where 

316 
"encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))" 

317 

318 
lemma encode_typerep_injective: "\<forall>u. encode_typerep t = encode_typerep u \<longrightarrow> t = u" 

319 
apply (induct t) 

320 
apply (rule allI) 

321 
apply (case_tac u) 

322 
apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1]) 

323 
done 

324 

43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

325 
instance typerep :: countable 
58158  326 
apply default 
327 
apply (unfold inj_on_def ball_UNIV) 

328 
apply (rule exI) 

329 
apply (rule allI) 

330 
apply (rule encode_typerep_injective) 

331 
done 

43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

332 

15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

333 
end 