author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63040  eb4ddd18d635 
child 65411  3c628937899d 
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 

60500  7 
section \<open>Encoding (almost) everything into natural numbers\<close> 
26169  8 

9 
theory Countable 

62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61115
diff
changeset

10 
imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection 
26169  11 
begin 
12 

60500  13 
subsection \<open>The class of countable types\<close> 
26169  14 

29797  15 
class countable = 
61076  16 
assumes ex_inj: "\<exists>to_nat :: 'a \<Rightarrow> nat. inj to_nat" 
26169  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 

60500  28 
subsection \<open>Conversion functions\<close> 
26169  29 

61076  30 
definition to_nat :: "'a::countable \<Rightarrow> nat" where 
26169  31 
"to_nat = (SOME f. inj f)" 
32 

61076  33 
definition from_nat :: "nat \<Rightarrow> 'a::countable" where 
34 
"from_nat = inv (to_nat :: 'a \<Rightarrow> nat)" 

26169  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 

60500  53 
subsection \<open>Finite types are countable\<close> 
26169  54 

55 
subclass (in finite) countable 

28823  56 
proof 
61076  57 
have "finite (UNIV::'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) 

61076  63 
then show "\<exists>to_nat :: 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj]) 
26169  64 
qed 
65 

66 

60500  67 
subsection \<open>Automatically proving countability of oldstyle datatypes\<close> 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

68 

61115
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

69 
context 
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

70 
begin 
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

71 

3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

72 
qualified 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

73 
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

74 
 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

75 
 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

76 
 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

77 
 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

78 

61115
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

79 
qualified function 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

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

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

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

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

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

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

86 
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

87 
 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

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

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

90 
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

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

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

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

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

95 

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

96 
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

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

98 

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

99 
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

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

101 

61115
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

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

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

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

105 
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

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

107 

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

108 
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

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

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

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

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

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

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

115 
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

116 
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

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

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

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

120 
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

121 
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

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

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

124 
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

125 
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

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

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

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

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

130 
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

131 
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

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

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

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

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

136 

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

137 
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

138 
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

139 
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

140 
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

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

142 
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

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

144 
proof 
63040  145 
define f where "f y = (LEAST n. nth_item n = Rep y)" for y 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

164 

60500  165 
ML \<open> 
58161  166 
fun old_countable_datatype_tac ctxt = 
58160  167 
SUBGOAL (fn (goal, _) => 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

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

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

170 
(case goal of 
56243  171 
(_ $ 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

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

173 
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

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

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

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

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

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

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

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

183 
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

184 
val vars = rev (Term.add_vars (Thm.prop_of induct_thm) []) 
59643  185 
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

186 
(Const (@{const_name Countable.finite_item}, T))) 
60801  187 
val induct_thm' = Thm.instantiate' [] insts induct_thm 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

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

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

190 
SOLVED' (fn i => EVERY 
60752  191 
[resolve_tac ctxt @{thms countable_datatype} i, 
192 
resolve_tac ctxt [typedef_thm] i, 

193 
eresolve_tac ctxt [induct_thm'] i, 

194 
REPEAT (resolve_tac ctxt rules i ORELSE assume_tac ctxt i)]) 1 

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

195 
end) 
60500  196 
\<close> 
47432  197 

61115
3a4400985780
modernized name space management  more uniform qualification;
wenzelm
parents:
61076
diff
changeset

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

199 

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

200 

60500  201 
subsection \<open>Automatically proving countability of datatypes\<close> 
58160  202 

62691
9bfcbab7cd99
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
blanchet
parents:
62087
diff
changeset

203 
ML_file "../Tools/BNF/bnf_lfp_countable.ML" 
58160  204 

60500  205 
ML \<open> 
58161  206 
fun countable_datatype_tac ctxt st = 
60029  207 
(case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of 
208 
SOME res => res 

209 
 NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st); 

58161  210 

211 
(* compatibility *) 

212 
fun countable_tac ctxt = 

213 
SELECT_GOAL (countable_datatype_tac ctxt); 

60500  214 
\<close> 
58161  215 

60500  216 
method_setup countable_datatype = \<open> 
58161  217 
Scan.succeed (SIMPLE_METHOD o countable_datatype_tac) 
60500  218 
\<close> "prove countable class instances for datatypes" 
58160  219 

220 

60500  221 
subsection \<open>More Countable types\<close> 
58160  222 

60500  223 
text \<open>Naturals\<close> 
43534
15df7bc8e93f
add countable_datatype method for proving countable class instances
huffman
parents:
40702
diff
changeset

224 

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

227 

60500  228 
text \<open>Pairs\<close> 
58160  229 

230 
instance prod :: (countable, countable) countable 

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

232 
(auto simp add: prod_encode_eq) 

58158  233 

60500  234 
text \<open>Sums\<close> 
58160  235 

236 
instance sum :: (countable, countable) countable 

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

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

239 
(simp split: sum.split_asm) 

240 

60500  241 
text \<open>Integers\<close> 
58158  242 

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

245 

60500  246 
text \<open>Options\<close> 
58160  247 

248 
instance option :: (countable) countable 

249 
by countable_datatype 

250 

60500  251 
text \<open>Lists\<close> 
58160  252 

253 
instance list :: (countable) countable 

254 
by countable_datatype 

255 

60500  256 
text \<open>String literals\<close> 
58160  257 

258 
instance String.literal :: countable 

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

60500  261 
text \<open>Functions\<close> 
58160  262 

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

264 
proof 

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

266 
using finite_list [OF finite_UNIV] .. 

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

268 
proof 

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

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

271 
qed 

272 
qed 

273 

60500  274 
text \<open>Typereps\<close> 
58158  275 

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

276 
instance typerep :: countable 
58160  277 
by countable_datatype 
278 

279 

60500  280 
subsection \<open>The rationals are countably infinite\<close> 
58160  281 

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

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

284 

285 
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj" 

286 
unfolding surj_def 

287 
proof 

288 
fix r::rat 

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

290 
proof (cases r) 

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

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

297 

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

299 
by (simp add: Rats_def surj_nat_to_rat_surj) 

300 

301 
context field_char_0 

302 
begin 

303 

304 
lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: 

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

308 

309 
lemma surj_of_rat_nat_to_rat_surj: 

58221  310 
"r \<in> \<rat> \<Longrightarrow> \<exists>n. r = of_rat (nat_to_rat_surj n)" 
58160  311 
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

312 

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

313 
end 
58160  314 

315 
instance rat :: countable 

316 
proof 

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

318 
proof 

319 
have "surj nat_to_rat_surj" 

320 
by (rule surj_nat_to_rat_surj) 

321 
then show "inj (inv nat_to_rat_surj)" 

322 
by (rule surj_imp_inj_inv) 

323 
qed 

324 
qed 

325 

326 
end 