author  wenzelm 
Fri, 06 Mar 2015 23:57:01 +0100  
changeset 59643  f3be9235503d 
parent 59621  291934bac95e 
child 60029  b2acd5301615 
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 
58160  4 
Author: Jasmin Blanchette, TU Muenchen 
26169  5 
*) 
6 

58881  7 
section {* Encoding (almost) everything into natural numbers *} 
26169  8 

9 
theory Countable 

58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58315
diff
changeset

10 
imports Old_Datatype Rat Nat_Bijection 
26169  11 
begin 
12 

13 
subsection {* The class of countable types *} 

14 

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

18 
lemma countable_classI: 

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

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

21 
shows "OFCLASS('a, countable_class)" 

22 
proof (intro_classes, rule exI) 

23 
show "inj f" 

24 
by (rule injI [OF assms]) assumption 

25 
qed 

26 

27 

26585  28 
subsection {* Conversion functions *} 
26169  29 

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

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

32 

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

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

35 

36 
lemma inj_to_nat [simp]: "inj to_nat" 

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

38 

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

41 

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

44 

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

47 

48 
lemma from_nat_to_nat [simp]: 

49 
"from_nat (to_nat x) = x" 

50 
by (simp add: from_nat_def) 

51 

52 

58160  53 
subsection {* Finite types are countable *} 
26169  54 

55 
subclass (in finite) countable 

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

61 
then have "surj f" unfolding surj_def by auto 

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

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

64 
qed 

65 

66 

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

68 

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

69 
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

70 
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

71 
 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

72 
 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

73 
 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

74 
 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

75 

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

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

77 
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

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

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

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

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

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

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

84 
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

85 
 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

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

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

88 
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

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

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

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

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

93 

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

94 
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

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

96 

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

97 
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

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

99 

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

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

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

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

103 
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

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

105 

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

106 
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

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

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

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

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

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

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

113 
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

114 
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

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

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

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

118 
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

119 
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

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

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

122 
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

123 
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

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

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

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

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

128 
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

129 
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

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

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

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

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

134 

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

135 
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

136 
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

137 
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

138 
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

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

140 
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

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

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

143 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

162 

47432  163 
ML {* 
58161  164 
fun old_countable_datatype_tac ctxt = 
58160  165 
SUBGOAL (fn (goal, _) => 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

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

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

168 
(case goal of 
56243  169 
(_ $ 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

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

171 
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

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

173 
val pred_name = 
59582  174 
(case HOLogic.dest_Trueprop (Thm.concl_of typedef_thm) of 
58160  175 
(_ $ _ $ _ $ (_ $ Const (n, _))) => n 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

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

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

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

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

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

181 
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

182 
val vars = rev (Term.add_vars (Thm.prop_of induct_thm) []) 
59643  183 
val insts = vars > map (fn (_, T) => try (Thm.cterm_of ctxt) 
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

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

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

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

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

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

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

190 
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

191 
etac induct_thm' i, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58881
diff
changeset

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

193 
end) 
47432  194 
*} 
195 

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

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

197 

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

198 

58315  199 
subsection {* Automatically proving countability of datatypes *} 
58160  200 

201 
ML_file "bnf_lfp_countable.ML" 

202 

58161  203 
ML {* 
204 
fun countable_datatype_tac ctxt st = 

205 
HEADGOAL (old_countable_datatype_tac ctxt) st 

58164  206 
handle exn => 
207 
if Exn.is_interrupt exn then reraise exn else BNF_LFP_Countable.countable_datatype_tac ctxt st; 

58161  208 

209 
(* compatibility *) 

210 
fun countable_tac ctxt = 

211 
SELECT_GOAL (countable_datatype_tac ctxt); 

212 
*} 

213 

58160  214 
method_setup countable_datatype = {* 
58161  215 
Scan.succeed (SIMPLE_METHOD o countable_datatype_tac) 
58160  216 
*} "prove countable class instances for datatypes" 
217 

218 

219 
subsection {* More Countable types *} 

220 

221 
text {* Naturals *} 

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

222 

58160  223 
instance nat :: countable 
224 
by (rule countable_classI [of "id"]) simp 

225 

226 
text {* Pairs *} 

227 

228 
instance prod :: (countable, countable) countable 

229 
by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"]) 

230 
(auto simp add: prod_encode_eq) 

58158  231 

58160  232 
text {* Sums *} 
233 

234 
instance sum :: (countable, countable) countable 

235 
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a) 

236 
 Inr b \<Rightarrow> to_nat (True, to_nat b))"]) 

237 
(simp split: sum.split_asm) 

238 

239 
text {* Integers *} 

58158  240 

58160  241 
instance int :: countable 
242 
by (rule countable_classI [of int_encode]) (simp add: int_encode_eq) 

243 

244 
text {* Options *} 

245 

246 
instance option :: (countable) countable 

247 
by countable_datatype 

248 

249 
text {* Lists *} 

250 

251 
instance list :: (countable) countable 

252 
by countable_datatype 

253 

254 
text {* String literals *} 

255 

256 
instance String.literal :: countable 

58221  257 
by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject) 
58160  258 

259 
text {* Functions *} 

260 

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

262 
proof 

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

264 
using finite_list [OF finite_UNIV] .. 

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

266 
proof 

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

268 
by (rule injI, simp add: xs fun_eq_iff) 

269 
qed 

270 
qed 

271 

272 
text {* Typereps *} 

58158  273 

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

274 
instance typerep :: countable 
58160  275 
by countable_datatype 
276 

277 

278 
subsection {* The rationals are countably infinite *} 

279 

280 
definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where 

281 
"nat_to_rat_surj n = (let (a, b) = prod_decode n in Fract (int_decode a) (int_decode b))" 

282 

283 
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" 

284 
unfolding surj_def 

285 
proof 

286 
fix r::rat 

287 
show "\<exists>n. r = nat_to_rat_surj n" 

288 
proof (cases r) 

289 
fix i j assume [simp]: "r = Fract i j" and "j > 0" 

58161  290 
have "r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))" 
58160  291 
by (simp add: Let_def nat_to_rat_surj_def) 
58161  292 
thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp: Let_def) 
58160  293 
qed 
294 
qed 

295 

296 
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj" 

297 
by (simp add: Rats_def surj_nat_to_rat_surj) 

298 

299 
context field_char_0 

300 
begin 

301 

302 
lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: 

58221  303 
"\<rat> = range (of_rat \<circ> nat_to_rat_surj)" 
58160  304 
using surj_nat_to_rat_surj 
305 
by (auto simp: Rats_def image_def surj_def) (blast intro: arg_cong[where f = of_rat]) 

306 

307 
lemma surj_of_rat_nat_to_rat_surj: 

58221  308 
"r \<in> \<rat> \<Longrightarrow> \<exists>n. r = of_rat (nat_to_rat_surj n)" 
58160  309 
by (simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def) 
43534
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 
end 
58160  312 

313 
instance rat :: countable 

314 
proof 

315 
show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat" 

316 
proof 

317 
have "surj nat_to_rat_surj" 

318 
by (rule surj_nat_to_rat_surj) 

319 
then show "inj (inv nat_to_rat_surj)" 

320 
by (rule surj_imp_inj_inv) 

321 
qed 

322 
qed 

323 

324 
end 