author  paulson 
Thu, 09 Dec 2004 16:45:46 +0100  
changeset 15391  797ed46d724b 
parent 14981  e73f8140af78 
child 15457  1fbd4aba46e3 
permissions  rwrr 
5177  1 
(* Title: HOL/Tools/datatype_rep_proofs.ML 
2 
ID: $Id$ 

11539  3 
Author: Stefan Berghofer, TU Muenchen 
5177  4 

5 
Definitional introduction of datatypes 

6 
Proof of characteristic theorems: 

7 

8 
 injectivity of constructors 

7228  9 
 distinctness of constructors 
5177  10 
 induction theorem 
11 

12 
*) 

13 

14 
signature DATATYPE_REP_PROOFS = 

15 
sig 

5661  16 
val representation_proofs : bool > DatatypeAux.datatype_info Symtab.table > 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

17 
string list > DatatypeAux.descr list > (string * sort) list > 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

18 
(string * mixfix) list > (string * mixfix) list list > theory attribute 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

19 
> theory > theory * thm list list * thm list list * thm list list * 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

20 
DatatypeAux.simproc_dist list * thm 
5177  21 
end; 
22 

23 
structure DatatypeRepProofs : DATATYPE_REP_PROOFS = 

24 
struct 

25 

26 
open DatatypeAux; 

27 

28 
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); 

29 

11435  30 

31 
(** theory context references **) 

5177  32 

11435  33 
val f_myinv_f = thm "f_myinv_f"; 
34 
val myinv_f_f = thm "myinv_f_f"; 

35 

5177  36 

37 
fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = 

38 
#exhaustion (the (Symtab.lookup (dt_info, tname))); 

39 

40 
(******************************************************************************) 

41 

5661  42 
fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) 
8436  43 
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = 
5177  44 
let 
12922  45 
val Datatype_thy = 
46 
if PureThy.get_name thy = "Datatype" then thy 

47 
else theory "Datatype"; 

11957  48 
val node_name = "Datatype_Universe.node"; 
49 
val In0_name = "Datatype_Universe.In0"; 

50 
val In1_name = "Datatype_Universe.In1"; 

51 
val Scons_name = "Datatype_Universe.Scons"; 

52 
val Leaf_name = "Datatype_Universe.Leaf"; 

53 
val Numb_name = "Datatype_Universe.Numb"; 

54 
val Lim_name = "Datatype_Universe.Lim"; 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

55 
val Suml_name = "Datatype.Suml"; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

56 
val Sumr_name = "Datatype.Sumr"; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

57 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

58 
val [In0_inject, In1_inject, Scons_inject, Leaf_inject, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

59 
In0_eq, In1_eq, In0_not_In1, In1_not_In0, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

60 
Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

61 
["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

62 
"In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

63 
"Lim_inject", "Suml_inject", "Sumr_inject"]; 
5177  64 

65 
val descr' = flat descr; 

66 

5661  67 
val big_name = space_implode "_" new_type_names; 
68 
val thy1 = add_path flat_names big_name thy; 

69 
val big_rec_name = big_name ^ "_rep_set"; 

6394  70 
val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) 
5177  71 
(if length descr' = 1 then [big_rec_name] else 
72 
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) 

73 
(1 upto (length descr')))); 

74 

5661  75 
val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); 
76 
val leafTs' = get_nonrec_types descr' sorts; 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

77 
val branchTs = get_branching_types descr' sorts; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

78 
val branchT = if null branchTs then HOLogic.unitT 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

79 
else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

80 
val arities = get_arities descr' \ 0; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

81 
val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []); 
5661  82 
val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars); 
5177  83 
val recTs = get_rec_types descr' sorts; 
84 
val newTs = take (length (hd descr), recTs); 

85 
val oldTs = drop (length (hd descr), recTs); 

86 
val sumT = if null leafTs then HOLogic.unitT 

87 
else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs; 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

88 
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); 
5177  89 
val UnivT = HOLogic.mk_setT Univ_elT; 
90 

91 
val In0 = Const (In0_name, Univ_elT > Univ_elT); 

92 
val In1 = Const (In1_name, Univ_elT > Univ_elT); 

93 
val Leaf = Const (Leaf_name, sumT > Univ_elT); 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

94 
val Lim = Const (Lim_name, (branchT > Univ_elT) > Univ_elT); 
5177  95 

96 
(* make injections needed for embedding types in leaves *) 

97 

98 
fun mk_inj T' x = 

99 
let 

100 
fun mk_inj' T n i = 

101 
if n = 1 then x else 

102 
let val n2 = n div 2; 

103 
val Type (_, [T1, T2]) = T 

104 
in 

105 
if i <= n2 then 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
14981
diff
changeset

106 
Const ("Sum_Type.Inl", T1 > T) $ (mk_inj' T1 n2 i) 
5177  107 
else 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
14981
diff
changeset

108 
Const ("Sum_Type.Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 
5177  109 
end 
110 
in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs) 

111 
end; 

112 

113 
(* make injections for constructors *) 

114 

7704  115 
fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then 
5177  116 
Const ("arbitrary", Univ_elT) 
117 
else 

118 
foldr1 (HOLogic.mk_binop Scons_name) ts); 

119 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

120 
(* function spaces *) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

121 

85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

122 
fun mk_fun_inj T' x = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

123 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

124 
fun mk_inj T n i = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

125 
if n = 1 then x else 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

126 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

127 
val n2 = n div 2; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

128 
val Type (_, [T1, T2]) = T; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

129 
fun mkT U = (U > Univ_elT) > T > Univ_elT 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

130 
in 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

131 
if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

132 
else Const (Sumr_name, mkT T2) $ mk_inj T2 (n  n2) (i  n2) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

133 
end 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

134 
in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

135 
end; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

136 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

137 
val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t))); 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

138 

5177  139 
(************** generate introduction rules for representing set **********) 
140 

6427  141 
val _ = message "Constructing representing sets ..."; 
5177  142 

143 
(* make introduction rule for a single constructor *) 

144 

145 
fun make_intr s n (i, (_, cargs)) = 

146 
let 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

147 
fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

148 
(dts, DtRec k) => 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

149 
let 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

150 
val Ts = map (typ_of_dtyp descr' sorts) dts; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

151 
val free_t = 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

152 
app_bnds (mk_Free "x" (Ts > Univ_elT) j) (length Ts) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

153 
in (j + 1, list_all (map (pair "x") Ts, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

154 
HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

155 
Const (nth_elem (k, rep_set_names), UnivT)))) :: prems, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

156 
mk_lim (Ts, free_t) :: ts) 
5177  157 
end 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

158 
 _ => 
5177  159 
let val T = typ_of_dtyp descr' sorts dt 
160 
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts) 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

161 
end); 
5177  162 

163 
val (_, prems, ts) = foldr mk_prem (cargs, (1, [], [])); 

164 
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem 

165 
(mk_univ_inj ts n i, Const (s, UnivT))) 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

166 
in Logic.list_implies (prems, concl) 
5177  167 
end; 
168 

169 
val consts = map (fn s => Const (s, UnivT)) rep_set_names; 

170 

171 
val intr_ts = flat (map (fn ((_, (_, _, constrs)), rep_set_name) => 

172 
map (make_intr rep_set_name (length constrs)) 

173 
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); 

174 

175 
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = 

5661  176 
setmp InductivePackage.quiet_mode (!quiet_mode) 
177 
(InductivePackage.add_inductive_i false true big_rec_name false true false 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

178 
consts (map (fn x => (("", x), [])) intr_ts) []) thy1; 
5177  179 

180 
(********************************* typedef ********************************) 

181 

5661  182 
val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => 
5696  183 
setmp TypedefPackage.quiet_mode true 
11827  184 
(TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None 
185 
(rtac exI 1 THEN 

186 
QUIET_BREADTH_FIRST (has_fewer_prems 1) 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

187 
(resolve_tac rep_intrs 1))) thy > #1) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

188 
(parent_path flat_names thy2, types_syntax ~~ tyvars ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

189 
(take (length newTs, consts)) ~~ new_type_names)); 
5177  190 

191 
(*********************** definition of constructors ***********************) 

192 

193 
val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; 

194 
val rep_names = map (curry op ^ "Rep_") new_type_names; 

195 
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i)) 

196 
(1 upto (length (flat (tl descr)))); 

6394  197 
val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @ 
198 
map (Sign.full_name (Theory.sign_of thy3)) rep_names'; 

5177  199 

200 
(* isomorphism declarations *) 

201 

202 
val iso_decls = map (fn (T, s) => (s, T > Univ_elT, NoSyn)) 

203 
(oldTs ~~ rep_names'); 

204 

205 
(* constructor definitions *) 

206 

207 
fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) = 

208 
let 

209 
fun constr_arg (dt, (j, l_args, r_args)) = 

210 
let val T = typ_of_dtyp descr' sorts dt; 

211 
val free_t = mk_Free "x" T j 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

212 
in (case (strip_dtyp dt, strip_type T) of 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

213 
((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

214 
Const (nth_elem (m, all_rep_names), U > Univ_elT) $ 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

215 
app_bnds free_t (length Us)) :: r_args) 
5177  216 
 _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) 
217 
end; 

218 

219 
val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], [])); 

220 
val constrT = (map (typ_of_dtyp descr' sorts) cargs) > T; 

6394  221 
val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); 
222 
val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); 

5177  223 
val lhs = list_comb (Const (cname, constrT), l_args); 
224 
val rhs = mk_univ_inj r_args n i; 

225 
val def = equals T $ lhs $ (Const (abs_name, Univ_elT > T) $ rhs); 

226 
val def_name = (Sign.base_name cname) ^ "_def"; 

227 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 

228 
(Const (rep_name, T > Univ_elT) $ lhs, rhs)); 

8436  229 
val (thy', [def_thm]) = thy > 
5177  230 
Theory.add_consts_i [(cname', constrT, mx)] > 
9315  231 
(PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]; 
5177  232 

8436  233 
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; 
5177  234 

235 
(* constructor definitions for datatype *) 

236 

237 
fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas), 

238 
((((_, (_, _, constrs)), tname), T), constr_syntax)) = 

239 
let 

240 
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong; 

6394  241 
val sg = Theory.sign_of thy; 
5177  242 
val rep_const = cterm_of sg 
243 
(Const (Sign.intern_const sg ("Rep_" ^ tname), T > Univ_elT)); 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

244 
val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

245 
val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma); 
5177  246 
val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs)) 
5661  247 
((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) 
5177  248 
in 
5661  249 
(parent_path flat_names thy', defs', eqns @ [eqns'], 
5177  250 
rep_congs @ [cong'], dist_lemmas @ [dist]) 
251 
end; 

252 

253 
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs 

5661  254 
((thy3 > Theory.add_consts_i iso_decls > parent_path flat_names, [], [], [], []), 
5177  255 
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); 
256 

257 
(*********** isomorphisms for new types (introduced by typedef) ***********) 

258 

6427  259 
val _ = message "Proving isomorphism properties ..."; 
5177  260 

261 
(* get axioms from theory *) 

262 

263 
val newT_iso_axms = map (fn s => 

7904  264 
(get_thm thy4 ("Abs_" ^ s ^ "_inverse"), 
265 
get_thm thy4 ("Rep_" ^ s ^ "_inverse"), 

266 
get_thm thy4 ("Rep_" ^ s))) new_type_names; 

5177  267 

268 
(**) 

269 
(* prove additional theorems: *) 

270 
(* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *) 

271 
(**) 

272 

273 
fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) = 

274 
let 

6394  275 
val sg = Theory.sign_of thy4; 
5177  276 
val RepT = T > Univ_elT; 
277 
val Rep_name = Sign.intern_const sg ("Rep_" ^ s); 

278 
val AbsT = Univ_elT > T; 

279 
val Abs_name = Sign.intern_const sg ("Abs_" ^ s); 

280 

6171  281 
val inj_Abs_thm = 
282 
prove_goalw_cterm [] 

283 
(cterm_of sg 

284 
(HOLogic.mk_Trueprop 

11435  285 
(Const ("Fun.inj_on", [AbsT, UnivT] > HOLogic.boolT) $ 
6171  286 
Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))) 
5177  287 
(fn _ => [rtac inj_on_inverseI 1, etac thm1 1]); 
288 

6171  289 
val setT = HOLogic.mk_setT T 
290 

291 
val inj_Rep_thm = 

292 
prove_goalw_cterm [] 

293 
(cterm_of sg 

294 
(HOLogic.mk_Trueprop 

11435  295 
(Const ("Fun.inj_on", [RepT, setT] > HOLogic.boolT) $ 
296 
Const (Rep_name, RepT) $ Const ("UNIV", setT)))) 

5177  297 
(fn _ => [rtac inj_inverseI 1, rtac thm2 1]) 
298 

6171  299 
in (inj_Abs_thm, inj_Rep_thm) end; 
5177  300 

301 
val newT_iso_inj_thms = map prove_newT_iso_inj_thm 

302 
(new_type_names ~~ newT_iso_axms ~~ newTs ~~ 

303 
take (length newTs, rep_set_names)); 

304 

305 
(********* isomorphisms between existing types and "unfolded" types *******) 

306 

307 
(**) 

308 
(* isomorphisms are defined using primreccombinators: *) 

309 
(* generate appropriate functions for instantiating primreccombinator *) 

310 
(* *) 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

311 
(* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) 
5177  312 
(* *) 
313 
(* also generate characteristic equations for isomorphisms *) 

314 
(* *) 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

315 
(* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) 
5177  316 
(**) 
317 

318 
fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) = 

319 
let 

320 
val argTs = map (typ_of_dtyp descr' sorts) cargs; 

321 
val T = nth_elem (k, recTs); 

322 
val rep_name = nth_elem (k, all_rep_names); 

323 
val rep_const = Const (rep_name, T > Univ_elT); 

324 
val constr = Const (cname, argTs > T); 

325 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

326 
fun process_arg ks' ((i2, i2', ts, Ts), dt) = 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

327 
let 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

328 
val T' = typ_of_dtyp descr' sorts dt; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

329 
val (Us, U) = strip_type T' 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

330 
in (case strip_dtyp dt of 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

331 
(_, DtRec j) => if j mem ks' then 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

332 
(i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

333 
(mk_Free "y" (Us > Univ_elT) i2') (length Us))], 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

334 
Ts @ [Us > Univ_elT]) 
5177  335 
else 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

336 
(i2 + 1, i2', ts @ [mk_lim (Us, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

337 
Const (nth_elem (j, all_rep_names), U > Univ_elT) $ 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

338 
app_bnds (mk_Free "x" T' i2) (length Us))], Ts) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

339 
 _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) 
5177  340 
end; 
341 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

342 
val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs); 
5177  343 
val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2  1))); 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

344 
val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2'  1))); 
5177  345 
val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); 
346 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

347 
val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs); 
5177  348 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 
349 
(rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) 

350 

351 
in (fs @ [f], eqns @ [eqn], i + 1) end; 

352 

353 
(* define isomorphisms for all mutually recursive datatypes in list ds *) 

354 

355 
fun make_iso_defs (ds, (thy, char_thms)) = 

356 
let 

357 
val ks = map fst ds; 

358 
val (_, (tname, _, _)) = hd ds; 

359 
val {rec_rewrites, rec_names, ...} = the (Symtab.lookup (dt_info, tname)); 

360 

361 
fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = 

362 
let 

363 
val (fs', eqns', _) = foldl (make_iso_def k ks (length constrs)) 

364 
((fs, eqns, 1), constrs); 

365 
val iso = (nth_elem (k, recTs), nth_elem (k, all_rep_names)) 

366 
in (fs', eqns', isos @ [iso]) end; 

367 

368 
val (fs, eqns, isos) = foldl process_dt (([], [], []), ds); 

369 
val fTs = map fastype_of fs; 

370 
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", 

371 
equals (T > Univ_elT) $ Const (iso_name, T > Univ_elT) $ 

372 
list_comb (Const (rec_name, fTs @ [T] > Univ_elT), fs))) (rec_names ~~ isos); 

9315  373 
val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; 
5177  374 

375 
(* prove characteristic equations *) 

376 

5553  377 
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); 
5177  378 
val char_thms' = map (fn eqn => prove_goalw_cterm rewrites 
6394  379 
(cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns; 
5177  380 

381 
in (thy', char_thms' @ char_thms) end; 

382 

5661  383 
val (thy5, iso_char_thms) = foldr make_iso_defs 
384 
(tl descr, (add_path flat_names big_name thy4, [])); 

5177  385 

386 
(* prove isomorphism properties *) 

387 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

388 
fun mk_funs_inv thm = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

389 
let 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

390 
val {sign, prop, ...} = rep_thm thm; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

391 
val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $ 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

392 
(_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

393 
val used = add_term_tfree_names (a, []); 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

394 

63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

395 
fun mk_thm i = 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

396 
let 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

397 
val Ts = map (TFree o rpair HOLogic.typeS) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

398 
(variantlist (replicate i "'t", used)); 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

399 
val f = Free ("f", Ts > U) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

400 
in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

401 
(HOLogic.mk_Trueprop (HOLogic.list_all 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

402 
(map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

403 
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

404 
r $ (a $ app_bnds f i)), f))))) (fn prems => 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

405 
[cut_facts_tac prems 1, REPEAT (rtac ext 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

406 
REPEAT (etac allE 1), rtac thm 1, atac 1]) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

407 
end 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

408 
in map (fn r => r RS subst) (thm :: map mk_thm arities) end; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

409 

5177  410 
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) 
411 

412 
fun prove_iso_thms (ds, (inj_thms, elem_thms)) = 

413 
let 

414 
val (_, (tname, _, _)) = hd ds; 

415 
val {induction, ...} = the (Symtab.lookup (dt_info, tname)); 

416 

417 
fun mk_ind_concl (i, _) = 

418 
let 

419 
val T = nth_elem (i, recTs); 

420 
val Rep_t = Const (nth_elem (i, all_rep_names), T > Univ_elT); 

421 
val rep_set_name = nth_elem (i, rep_set_names) 

422 
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ 

423 
HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ 

424 
HOLogic.mk_eq (mk_Free "x" T i, Bound 0)), 

425 
HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT))) 

426 
end; 

427 

428 
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); 

429 

5553  430 
val rewrites = map mk_meta_eq iso_char_thms; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

431 
val inj_thms' = map (fn r => r RS injD) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

432 
(map snd newT_iso_inj_thms @ inj_thms); 
5177  433 

6394  434 
val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) 
5177  435 
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ => 
11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

436 
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
5177  437 
REPEAT (EVERY 
438 
[rtac allI 1, rtac impI 1, 

439 
exh_tac (exh_thm_of dt_info) 1, 

440 
REPEAT (EVERY 

441 
[hyp_subst_tac 1, 

442 
rewrite_goals_tac rewrites, 

443 
REPEAT (dresolve_tac [In0_inject, In1_inject] 1), 

444 
(eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1) 

445 
ORELSE (EVERY 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

446 
[REPEAT (eresolve_tac (Scons_inject :: 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

447 
map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

448 
REPEAT (cong_tac 1), rtac refl 1, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

449 
REPEAT (atac 1 ORELSE (EVERY 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

450 
[REPEAT (rtac ext 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

451 
REPEAT (eresolve_tac (mp :: allE :: 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

452 
map make_elim (Suml_inject :: Sumr_inject :: 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

453 
Lim_inject :: fun_cong :: inj_thms')) 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

454 
atac 1]))])])])]); 
5177  455 

6171  456 
val inj_thms'' = map (fn r => r RS datatype_injI) 
457 
(split_conj_thm inj_thm); 

5177  458 

6171  459 
val elem_thm = 
460 
prove_goalw_cterm [] 

6394  461 
(cterm_of (Theory.sign_of thy5) 
6171  462 
(HOLogic.mk_Trueprop (mk_conj ind_concl2))) 
463 
(fn _ => 

11951
381135c295ef
Fixed several bugs concerning arbitrarily branching datatypes.
berghofe
parents:
11827
diff
changeset

464 
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

465 
rewrite_goals_tac rewrites, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

466 
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

467 
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]); 
5177  468 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

469 
in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

470 
end; 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

471 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

472 
val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

473 
(tl descr, ([], map #3 newT_iso_axms)); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

474 
val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded; 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

475 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

476 
(* prove x : dt_rep_set_i > x : range dt_Rep_i *) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

477 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

478 
fun mk_iso_t (((set_name, iso_name), i), T) = 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

479 
let val isoT = T > Univ_elT 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

480 
in HOLogic.imp $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

481 
HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

482 
(if i < length newTs then Const ("True", HOLogic.boolT) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

483 
else HOLogic.mk_mem (mk_Free "x" Univ_elT i, 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

484 
Const ("image", [isoT, HOLogic.mk_setT T] > UnivT) $ 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

485 
Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T))) 
5177  486 
end; 
487 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

488 
val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

489 
(rep_set_names ~~ all_rep_names ~~ (0 upto (length descr'  1)) ~~ recTs))); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

490 

ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

491 
(* all the theorems are proved by one single simultaneous induction *) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

492 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

493 
val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq)) 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

494 
iso_inj_thms_unfolded; 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

495 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

496 
val iso_thms = if length descr = 1 then [] else 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

497 
drop (length newTs, split_conj_thm 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

498 
(prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ => 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

499 
[(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

500 
REPEAT (rtac TrueI 1), 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

501 
rewrite_goals_tac (mk_meta_eq choice_eq :: 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

502 
symmetric (mk_meta_eq expand_fun_eq) :: range_eqs), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

503 
rewrite_goals_tac (map symmetric range_eqs), 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

504 
REPEAT (EVERY 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

505 
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

506 
flat (map (mk_funs_inv o #1) newT_iso_axms)) 1), 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

507 
TRY (hyp_subst_tac 1), 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

508 
rtac (sym RS range_eqI) 1, 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

509 
resolve_tac iso_char_thms 1])]))); 
11435  510 

511 
val Abs_inverse_thms' = 

512 
map #1 newT_iso_axms @ 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

513 
map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

514 
(iso_inj_thms_unfolded, iso_thms); 
11435  515 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

516 
val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms'); 
5177  517 

518 
(******************* freeness theorems for constructors *******************) 

519 

6427  520 
val _ = message "Proving freeness of constructors ..."; 
5177  521 

522 
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *) 

523 

524 
fun prove_constr_rep_thm eqn = 

525 
let 

526 
val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms; 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

527 
val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) 
6394  528 
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ => 
5177  529 
[resolve_tac inj_thms 1, 
530 
rewrite_goals_tac rewrites, 

531 
rtac refl 1, 

532 
resolve_tac rep_intrs 2, 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

533 
REPEAT (resolve_tac iso_elem_thms 1)]) 
5177  534 
end; 
535 

536 
(**) 

537 
(* constr_rep_thms and rep_congs are used to prove distinctness *) 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

538 
(* of constructors. *) 
5177  539 
(**) 
540 

541 
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns; 

542 

543 
val dist_rewrites = map (fn (rep_thms, dist_lemma) => 

544 
dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) 

545 
(constr_rep_thms ~~ dist_lemmas); 

546 

7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

547 
fun prove_distinct_thms (_, []) = [] 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

548 
 prove_distinct_thms (dist_rewrites', t::_::ts) = 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

549 
let 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

550 
val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

551 
[simp_tac (HOL_ss addsimps dist_rewrites') 1]) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

552 
in dist_thm::(standard (dist_thm RS not_sym)):: 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

553 
(prove_distinct_thms (dist_rewrites', ts)) 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

554 
end; 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

555 

85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

556 
val distinct_thms = map prove_distinct_thms (dist_rewrites ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

557 
DatatypeProp.make_distincts new_type_names descr sorts thy5); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

558 

85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

559 
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

560 
if length constrs < !DatatypeProp.dtK then FewConstrs dists 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

561 
else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~ 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

562 
constr_rep_thms ~~ rep_congs ~~ distinct_thms); 
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

563 

5177  564 
(* prove injectivity of constructors *) 
565 

566 
fun prove_constr_inj_thm rep_thms t = 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

567 
let val inj_thms = Scons_inject :: (map make_elim 
5177  568 
((map (fn r => r RS injD) iso_inj_thms) @ 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

569 
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

570 
Lim_inject, Suml_inject, Sumr_inject])) 
6394  571 
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ => 
5177  572 
[rtac iffI 1, 
573 
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2, 

574 
dresolve_tac rep_congs 1, dtac box_equals 1, 

13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

575 
REPEAT (resolve_tac rep_thms 1), 
5177  576 
REPEAT (eresolve_tac inj_thms 1), 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

577 
REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

578 
REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

579 
atac 1]))]) 
5177  580 
end; 
581 

582 
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts) 

583 
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms); 

584 

8479
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

585 
val (thy6, (constr_inject', distinct_thms'))= thy5 > parent_path flat_names > 
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

586 
store_thmss "inject" new_type_names constr_inject >>> 
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

587 
store_thmss "distinct" new_type_names distinct_thms; 
5177  588 

589 
(*************************** induction theorem ****************************) 

590 

6427  591 
val _ = message "Proving induction rule for datatypes ..."; 
5177  592 

593 
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @ 

11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

594 
(map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); 
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

595 
val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; 
5177  596 

597 
fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = 

598 
let 

599 
val Rep_t = Const (nth_elem (i, all_rep_names), T > Univ_elT) $ 

600 
mk_Free "x" T i; 

601 

602 
val Abs_t = if i < length newTs then 

6394  603 
Const (Sign.intern_const (Theory.sign_of thy6) 
5177  604 
("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT > T) 
11435  605 
else Const ("Inductive.myinv", [T > Univ_elT, Univ_elT] > T) $ 
5177  606 
Const (nth_elem (i, all_rep_names), T > Univ_elT) 
607 

608 
in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, 

609 
Const (nth_elem (i, rep_set_names), UnivT)) $ 

610 
(mk_Free "P" (T > HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], 

611 
concls @ [mk_Free "P" (T > HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) 

612 
end; 

613 

614 
val (indrule_lemma_prems, indrule_lemma_concls) = 

615 
foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); 

616 

6394  617 
val cert = cterm_of (Theory.sign_of thy6); 
5177  618 

619 
val indrule_lemma = prove_goalw_cterm [] (cert 

620 
(Logic.mk_implies 

621 
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 

622 
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems => 

623 
[cut_facts_tac prems 1, REPEAT (etac conjE 1), 

624 
REPEAT (EVERY 

625 
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, 

626 
etac mp 1, resolve_tac iso_elem_thms 1])]); 

627 

8305  628 
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma))); 
5177  629 
val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else 
630 
map (Free o apfst fst o dest_Var) Ps; 

631 
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma; 

632 

13340
9b0332344ae2
Simplified proof of induction rule for datatypes involving function types.
berghofe
parents:
12922
diff
changeset

633 
val dt_induct = prove_goalw_cterm [] (cert 
5177  634 
(DatatypeProp.make_ind descr sorts)) (fn prems => 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

635 
[rtac indrule_lemma' 1, 
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

636 
(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, 
5177  637 
EVERY (map (fn (prem, r) => (EVERY 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

638 
[REPEAT (eresolve_tac Abs_inverse_thms 1), 
5177  639 
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

640 
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

641 
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); 
5177  642 

8436  643 
val (thy7, [dt_induct']) = thy6 > 
5661  644 
Theory.add_path big_name > 
13340
9b0332344ae2
Simplified proof of induction rule for datatypes involving function types.
berghofe
parents:
12922
diff
changeset

645 
PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] >> 
5661  646 
Theory.parent_path; 
5177  647 

8479
5d327a46dc61
Now returns theorems with correct names in derivations.
berghofe
parents:
8436
diff
changeset

648 
in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct') 
5177  649 
end; 
650 

651 
end; 