author  wenzelm 
Wed, 31 Dec 2008 18:53:16 +0100  
changeset 29270  0eade173f77e 
parent 28965  1de908189869 
child 29389  0a49f940d729 
permissions  rwrr 
5177  1 
(* Title: HOL/Tools/datatype_rep_proofs.ML 
11539  2 
Author: Stefan Berghofer, TU Muenchen 
5177  3 

4 
Definitional introduction of datatypes 

5 
Proof of characteristic theorems: 

6 

7 
 injectivity of constructors 

7228  8 
 distinctness of constructors 
5177  9 
 induction theorem 
10 
*) 

11 

12 
signature DATATYPE_REP_PROOFS = 

13 
sig 

27002
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

14 
val distinctness_limit : int Config.T 
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

15 
val distinctness_limit_setup : theory > theory 
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 > 
18728  18 
(string * mixfix) list > (string * mixfix) list list > attribute 
18314  19 
> theory > (thm list list * thm list list * thm list list * 
20 
DatatypeAux.simproc_dist list * thm) * theory 

5177  21 
end; 
22 

23 
structure DatatypeRepProofs : DATATYPE_REP_PROOFS = 

24 
struct 

25 

26 
open DatatypeAux; 

27 

27002
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

28 
(*the kind of distinctiveness axioms depends on number of constructors*) 
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

29 
val (distinctness_limit, distinctness_limit_setup) = 
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

30 
Attrib.config_int "datatype_distinctness_limit" 7; 
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

31 

5177  32 
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); 
33 

21021  34 
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; 
35 

11435  36 

37 
(** theory context references **) 

5177  38 

11435  39 
val f_myinv_f = thm "f_myinv_f"; 
40 
val myinv_f_f = thm "myinv_f_f"; 

41 

5177  42 

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

17412  44 
#exhaustion (the (Symtab.lookup dt_info tname)); 
5177  45 

46 
(******************************************************************************) 

47 

5661  48 
fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) 
8436  49 
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = 
5177  50 
let 
19540  51 
val Datatype_thy = ThyInfo.the_theory "Datatype" thy; 
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

52 
val node_name = "Datatype.node"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

53 
val In0_name = "Datatype.In0"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

54 
val In1_name = "Datatype.In1"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

55 
val Scons_name = "Datatype.Scons"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

56 
val Leaf_name = "Datatype.Leaf"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

57 
val Numb_name = "Datatype.Numb"; 
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20071
diff
changeset

58 
val Lim_name = "Datatype.Lim"; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

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

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

61 

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

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

63 
In0_eq, In1_eq, In0_not_In1, In1_not_In0, 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

64 
Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy) 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

65 
["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

66 
"In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", 
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

67 
"Lim_inject", "Suml_inject", "Sumr_inject"]; 
5177  68 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

69 
val descr' = flat descr; 
5177  70 

5661  71 
val big_name = space_implode "_" new_type_names; 
72 
val thy1 = add_path flat_names big_name thy; 

73 
val big_rec_name = big_name ^ "_rep_set"; 

21021  74 
val rep_set_names' = 
5177  75 
(if length descr' = 1 then [big_rec_name] else 
76 
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) 

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

28965  78 
val rep_set_names = map (Sign.full_bname thy1) rep_set_names'; 
5177  79 

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

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

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

83 
val branchT = if null branchTs then HOLogic.unitT 
23419  84 
else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

85 
val arities = get_arities descr' \ 0; 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

86 
val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs); 
17521  87 
val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars); 
5177  88 
val recTs = get_rec_types descr' sorts; 
15570  89 
val newTs = Library.take (length (hd descr), recTs); 
90 
val oldTs = Library.drop (length (hd descr), recTs); 

5177  91 
val sumT = if null leafTs then HOLogic.unitT 
23419  92 
else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

93 
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); 
5177  94 
val UnivT = HOLogic.mk_setT Univ_elT; 
21021  95 
val UnivT' = Univ_elT > HOLogic.boolT; 
96 
val Collect = Const ("Collect", UnivT' > UnivT); 

5177  97 

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

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

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

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

101 
val Lim = Const (Lim_name, (branchT > Univ_elT) > Univ_elT); 
5177  102 

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

104 

105 
fun mk_inj T' x = 

106 
let 

107 
fun mk_inj' T n i = 

108 
if n = 1 then x else 

109 
let val n2 = n div 2; 

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

111 
in 

112 
if i <= n2 then 

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

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

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

118 
end; 

119 

120 
(* make injections for constructors *) 

121 

23419  122 
fun mk_univ_inj ts = BalancedTree.access 
123 
{left = fn t => In0 $ t, 

124 
right = fn t => In1 $ t, 

125 
init = 

28524  126 
if ts = [] then Const (@{const_name undefined}, Univ_elT) 
23419  127 
else foldr1 (HOLogic.mk_binop Scons_name) ts}; 
5177  128 

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

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

130 

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

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

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

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

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

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

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

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

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

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

140 
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

141 
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

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

143 
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

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

145 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

147 

5177  148 
(************** generate introduction rules for representing set **********) 
149 

6427  150 
val _ = message "Constructing representing sets ..."; 
5177  151 

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

153 

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

155 
let 

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

156 
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

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

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

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

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

161 
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

162 
in (j + 1, list_all (map (pair "x") Ts, 
21021  163 
HOLogic.mk_Trueprop 
164 
(Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems, 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

167 
 _ => 
5177  168 
let val T = typ_of_dtyp descr' sorts dt 
169 
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

170 
end); 
5177  171 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

172 
val (_, prems, ts) = foldr mk_prem (1, [], []) cargs; 
21021  173 
val concl = HOLogic.mk_Trueprop 
174 
(Free (s, UnivT') $ mk_univ_inj ts n i) 

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

175 
in Logic.list_implies (prems, concl) 
5177  176 
end; 
177 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

178 
val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) => 
5177  179 
map (make_intr rep_set_name (length constrs)) 
28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

180 
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'); 
5177  181 

21365
4ee8e2702241
InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents:
21291
diff
changeset

182 
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = 
26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
26359
diff
changeset

183 
InductivePackage.add_inductive_global (serial_string ()) 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

184 
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, 
28965  185 
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

186 
skip_mono = true} 
28965  187 
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] 
188 
(map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1; 

5177  189 

190 
(********************************* typedef ********************************) 

191 

21021  192 
val (typedefs, thy3) = thy2 > 
193 
parent_path flat_names > 

194 
fold_map (fn ((((name, mx), tvs), c), name') => 

28662  195 
TypedefPackage.add_typedef false (SOME name') (name, tvs, mx) 
21021  196 
(Collect $ Const (c, UnivT')) NONE 
197 
(rtac exI 1 THEN rtac CollectI 1 THEN 

198 
QUIET_BREADTH_FIRST (has_fewer_prems 1) 

26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
26359
diff
changeset

199 
(resolve_tac rep_intrs 1))) 
21021  200 
(types_syntax ~~ tyvars ~~ 
201 
(Library.take (length newTs, rep_set_names)) ~~ new_type_names) > 

202 
add_path flat_names big_name; 

5177  203 

204 
(*********************** definition of constructors ***********************) 

205 

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

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

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

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

209 
(1 upto (length (flat (tl descr)))); 
22578  210 
val all_rep_names = map (Sign.intern_const thy3) rep_names @ 
28965  211 
map (Sign.full_bname thy3) rep_names'; 
5177  212 

213 
(* isomorphism declarations *) 

214 

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

216 
(oldTs ~~ rep_names'); 

217 

218 
(* constructor definitions *) 

219 

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

221 
let 

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

223 
let val T = typ_of_dtyp descr' sorts dt; 

224 
val free_t = mk_Free "x" T j 

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

225 
in (case (strip_dtyp dt, strip_type T) of 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

226 
((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

227 
(Const (List.nth (all_rep_names, m), U > Univ_elT) $ 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

228 
app_bnds free_t (length Us)) Us :: r_args) 
5177  229 
 _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) 
230 
end; 

231 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

232 
val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs; 
5177  233 
val constrT = (map (typ_of_dtyp descr' sorts) cargs) > T; 
22578  234 
val abs_name = Sign.intern_const thy ("Abs_" ^ tname); 
235 
val rep_name = Sign.intern_const thy ("Rep_" ^ tname); 

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

27330  238 
val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT > T) $ rhs); 
239 
val def_name = Sign.base_name cname ^ "_def"; 

5177  240 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 
241 
(Const (rep_name, T > Univ_elT) $ lhs, rhs)); 

18377  242 
val ([def_thm], thy') = 
243 
thy 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24112
diff
changeset

244 
> Sign.add_consts_i [(cname', constrT, mx)] 
27691
ce171cbd4b93
PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents:
27330
diff
changeset

245 
> (PureThy.add_defs false o map Thm.no_attributes) [(def_name, def)]; 
5177  246 

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

249 
(* constructor definitions for datatype *) 

250 

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

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

253 
let 

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

22578  255 
val rep_const = cterm_of thy 
256 
(Const (Sign.intern_const thy ("Rep_" ^ tname), T > Univ_elT)); 

257 
val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong); 

258 
val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); 

15570  259 
val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) 
5661  260 
((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) 
5177  261 
in 
5661  262 
(parent_path flat_names thy', defs', eqns @ [eqns'], 
5177  263 
rep_congs @ [cong'], dist_lemmas @ [dist]) 
264 
end; 

265 

15570  266 
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24112
diff
changeset

267 
((thy3 > Sign.add_consts_i iso_decls > parent_path flat_names, [], [], [], []), 
5177  268 
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); 
269 

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

271 

6427  272 
val _ = message "Proving isomorphism properties ..."; 
5177  273 

21021  274 
val newT_iso_axms = map (fn (_, td) => 
275 
(collect_simp (#Abs_inverse td), #Rep_inverse td, 

276 
collect_simp (#Rep td))) typedefs; 

5177  277 

21021  278 
val newT_iso_inj_thms = map (fn (_, td) => 
279 
(collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs; 

5177  280 

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

282 

283 
(**) 

284 
(* isomorphisms are defined using primreccombinators: *) 

285 
(* generate appropriate functions for instantiating primreccombinator *) 

286 
(* *) 

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

287 
(* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) 
5177  288 
(* *) 
289 
(* also generate characteristic equations for isomorphisms *) 

290 
(* *) 

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

291 
(* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) 
5177  292 
(**) 
293 

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

295 
let 

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

15570  297 
val T = List.nth (recTs, k); 
298 
val rep_name = List.nth (all_rep_names, k); 

5177  299 
val rep_const = Const (rep_name, T > Univ_elT); 
300 
val constr = Const (cname, argTs > T); 

301 

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

302 
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

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

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

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

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

307 
(_, DtRec j) => if j mem ks' then 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

308 
(i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

310 
Ts @ [Us > Univ_elT]) 
5177  311 
else 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

312 
(i2 + 1, i2', ts @ [mk_lim 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

313 
(Const (List.nth (all_rep_names, j), U > Univ_elT) $ 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

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

15570  318 
val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs); 
5177  319 
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

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

15570  323 
val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs); 
5177  324 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 
325 
(rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) 

326 

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

328 

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

330 

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

332 
let 

333 
val ks = map fst ds; 

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

17412  335 
val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname); 
5177  336 

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

338 
let 

15570  339 
val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs)) 
5177  340 
((fs, eqns, 1), constrs); 
15570  341 
val iso = (List.nth (recTs, k), List.nth (all_rep_names, k)) 
5177  342 
in (fs', eqns', isos @ [iso]) end; 
343 

15570  344 
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); 
5177  345 
val fTs = map fastype_of fs; 
346 
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", 

27330  347 
Logic.mk_equals (Const (iso_name, T > Univ_elT), 
348 
list_comb (Const (rec_name, fTs @ [T] > Univ_elT), fs)))) (rec_names ~~ isos); 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

349 
val (def_thms, thy') = 
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

350 
apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy); 
5177  351 

352 
(* prove characteristic equations *) 

353 

5553  354 
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

355 
val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn 
20046  356 
(fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns; 
5177  357 

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

359 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

360 
val (thy5, iso_char_thms) = apfst Theory.checkpoint (foldr make_iso_defs 
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

361 
(add_path flat_names big_name thy4, []) (tl descr)); 
5177  362 

363 
(* prove isomorphism properties *) 

364 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

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

366 
let 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26531
diff
changeset

367 
val prop = Thm.prop_of thm; 
21021  368 
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ 
16287  369 
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

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

371 

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

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

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

374 
val Ts = map (TFree o rpair HOLogic.typeS) 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20046
diff
changeset

375 
(Name.variant_list used (replicate i "'t")); 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

376 
val f = Free ("f", Ts > U) 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

377 
in SkipProof.prove_global thy [] [] (Logic.mk_implies 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

378 
(HOLogic.mk_Trueprop (HOLogic.list_all 
21021  379 
(map (pair "x") Ts, S $ app_bnds f i)), 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

380 
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, 
17985  381 
r $ (a $ app_bnds f i)), f)))) 
26806  382 
(fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1), 
383 
REPEAT (etac allE 1), rtac thm 1, atac 1]) 

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

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

385 
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

386 

5177  387 
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) 
388 

26806  389 
val fun_congs = map (fn T => make_elim (Drule.instantiate' 
390 
[SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs; 

391 

5177  392 
fun prove_iso_thms (ds, (inj_thms, elem_thms)) = 
393 
let 

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

17412  395 
val {induction, ...} = the (Symtab.lookup dt_info tname); 
5177  396 

397 
fun mk_ind_concl (i, _) = 

398 
let 

15570  399 
val T = List.nth (recTs, i); 
400 
val Rep_t = Const (List.nth (all_rep_names, i), T > Univ_elT); 

401 
val rep_set_name = List.nth (rep_set_names, i) 

5177  402 
in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ 
403 
HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ 

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

21021  405 
Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i)) 
5177  406 
end; 
407 

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

409 

5553  410 
val rewrites = map mk_meta_eq iso_char_thms; 
21021  411 
val inj_thms' = map snd newT_iso_inj_thms @ 
26359  412 
map (fn r => r RS @{thm injD}) inj_thms; 
5177  413 

26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

414 
val inj_thm = SkipProof.prove_global thy5 [] [] 
17985  415 
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY 
25678  416 
[(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
5177  417 
REPEAT (EVERY 
418 
[rtac allI 1, rtac impI 1, 

419 
exh_tac (exh_thm_of dt_info) 1, 

420 
REPEAT (EVERY 

421 
[hyp_subst_tac 1, 

422 
rewrite_goals_tac rewrites, 

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

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

425 
ORELSE (EVERY 

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

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

427 
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

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

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

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

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

432 
map make_elim (Suml_inject :: Sumr_inject :: 
26806  433 
Lim_inject :: inj_thms') @ fun_congs) 1), 
20046  434 
atac 1]))])])])]); 
5177  435 

26359  436 
val inj_thms'' = map (fn r => r RS @{thm datatype_injI}) 
6171  437 
(split_conj_thm inj_thm); 
5177  438 

6171  439 
val elem_thm = 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

440 
SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) 
20046  441 
(fn _ => 
25678  442 
EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
20046  443 
rewrite_goals_tac rewrites, 
444 
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW 

445 
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]); 

5177  446 

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

447 
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

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

449 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

450 
val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

451 
([], map #3 newT_iso_axms) (tl descr); 
21021  452 
val iso_inj_thms = map snd newT_iso_inj_thms @ 
26359  453 
map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded; 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

454 

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

456 

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

457 
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

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

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

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

462 
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

463 
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

464 
Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T))) 
5177  465 
end; 
466 

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

467 
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

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

469 

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

470 
(* 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

471 

26359  472 
val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq})) 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

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

474 

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

475 
val iso_thms = if length descr = 1 then [] else 
15570  476 
Library.drop (length newTs, split_conj_thm 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

477 
(SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY 
25678  478 
[(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
11471
ba2c252b55ad
 Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
berghofe
parents:
11435
diff
changeset

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

480 
rewrite_goals_tac (mk_meta_eq choice_eq :: 
26359  481 
symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

482 
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

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

484 
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ 
28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

485 
maps (mk_funs_inv thy5 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

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

487 
rtac (sym RS range_eqI) 1, 
20046  488 
resolve_tac iso_char_thms 1])]))); 
11435  489 

490 
val Abs_inverse_thms' = 

491 
map #1 newT_iso_axms @ 

18330  492 
map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp]) 
493 
iso_inj_thms_unfolded iso_thms; 

11435  494 

28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

495 
val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms'; 
5177  496 

497 
(******************* freeness theorems for constructors *******************) 

498 

6427  499 
val _ = message "Proving freeness of constructors ..."; 
5177  500 

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

502 

503 
fun prove_constr_rep_thm eqn = 

504 
let 

21021  505 
val inj_thms = map fst newT_iso_inj_thms; 
26359  506 
val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

507 
in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY 
5177  508 
[resolve_tac inj_thms 1, 
509 
rewrite_goals_tac rewrites, 

21021  510 
rtac refl 3, 
5177  511 
resolve_tac rep_intrs 2, 
20046  512 
REPEAT (resolve_tac iso_elem_thms 1)]) 
5177  513 
end; 
514 

515 
(**) 

516 
(* 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

517 
(* of constructors. *) 
5177  518 
(**) 
519 

520 
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns; 

521 

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

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

524 
(constr_rep_thms ~~ dist_lemmas); 

525 

26969
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

526 
fun prove_distinct_thms _ _ (_, []) = [] 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

527 
 prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) = 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

528 
if k >= lim then [] else let 
27002
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

529 
(*number of constructors < distinctness_limit : C_i ... ~= C_j ...*) 
26969
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

530 
fun prove [] = [] 
27300
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

531 
 prove (t :: ts) = 
26969
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

532 
let 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

533 
val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ => 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

534 
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]) 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

535 
in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end; 
cf3f998d0631
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents:
26806
diff
changeset

536 
in prove ts end; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

537 

27300
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

538 
val distinct_thms = DatatypeProp.make_distincts descr sorts 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

539 
> map2 (prove_distinct_thms 
4cb3101d2bf7
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents:
27002
diff
changeset

540 
(Config.get_thy thy5 distinctness_limit)) dist_rewrites; 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

541 

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

542 
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => 
27002
215d64dc971e
moved distinctness_limit to datatype_rep_proofs.ML
haftmann
parents:
26969
diff
changeset

543 
if length constrs < Config.get_thy thy5 distinctness_limit 
24098
f1eb34ae33af
replaced dtK ref by datatype_distinctness_limit configuration option;
wenzelm
parents:
23590
diff
changeset

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

545 
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

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

547 

5177  548 
(* prove injectivity of constructors *) 
549 

550 
fun prove_constr_inj_thm rep_thms t = 

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

551 
let val inj_thms = Scons_inject :: (map make_elim 
21021  552 
(iso_inj_thms @ 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

553 
[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

554 
Lim_inject, Suml_inject, Sumr_inject])) 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

555 
in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY 
5177  556 
[rtac iffI 1, 
557 
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2, 

558 
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

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

561 
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

562 
REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), 
20046  563 
atac 1]))]) 
5177  564 
end; 
565 

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

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

568 

18314  569 
val ((constr_inject', distinct_thms'), thy6) = 
570 
thy5 

571 
> parent_path flat_names 

572 
> store_thmss "inject" new_type_names constr_inject 

573 
>> store_thmss "distinct" new_type_names distinct_thms; 

5177  574 

575 
(*************************** induction theorem ****************************) 

576 

6427  577 
val _ = message "Proving induction rule for datatypes ..."; 
5177  578 

579 
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

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

581 
val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; 
5177  582 

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

584 
let 

15570  585 
val Rep_t = Const (List.nth (all_rep_names, i), T > Univ_elT) $ 
5177  586 
mk_Free "x" T i; 
587 

588 
val Abs_t = if i < length newTs then 

22578  589 
Const (Sign.intern_const thy6 
15570  590 
("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT > T) 
11435  591 
else Const ("Inductive.myinv", [T > Univ_elT, Univ_elT] > T) $ 
15570  592 
Const (List.nth (all_rep_names, i), T > Univ_elT) 
5177  593 

21021  594 
in (prems @ [HOLogic.imp $ 
595 
(Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $ 

5177  596 
(mk_Free "P" (T > HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], 
597 
concls @ [mk_Free "P" (T > HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) 

598 
end; 

599 

600 
val (indrule_lemma_prems, indrule_lemma_concls) = 

15570  601 
Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); 
5177  602 

22578  603 
val cert = cterm_of thy6; 
5177  604 

26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

605 
val indrule_lemma = SkipProof.prove_global thy6 [] [] 
5177  606 
(Logic.mk_implies 
607 
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 

17985  608 
HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY 
609 
[REPEAT (etac conjE 1), 

5177  610 
REPEAT (EVERY 
611 
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, 

20046  612 
etac mp 1, resolve_tac iso_elem_thms 1])]); 
5177  613 

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

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

618 

17985  619 
val dt_induct_prop = DatatypeProp.make_ind descr sorts; 
26531
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

620 
val dt_induct = SkipProof.prove_global thy6 [] 
17985  621 
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) 
26711  622 
(fn {prems, ...} => EVERY 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

623 
[rtac indrule_lemma' 1, 
25678  624 
(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
5177  625 
EVERY (map (fn (prem, r) => (EVERY 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

626 
[REPEAT (eresolve_tac Abs_inverse_thms 1), 
5177  627 
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

628 
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) 
20046  629 
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); 
5177  630 

18377  631 
val ([dt_induct'], thy7) = 
632 
thy6 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24112
diff
changeset

633 
> Sign.add_path big_name 
18377  634 
> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] 
28362
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

635 
> Sign.parent_path 
b0ebac91c8d5
explicit checkpoint for lowlevel (global) theory operations admits concurrent SkipProof.prove;
wenzelm
parents:
28084
diff
changeset

636 
> Theory.checkpoint; 
5177  637 

18314  638 
in 
639 
((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7) 

5177  640 
end; 
641 

642 
end; 