author  berghofe 
Thu, 03 Apr 2008 17:49:39 +0200  
changeset 26531  96e82c7861fa 
parent 26475  3cc1e48d0ce1 
child 26626  c6231d64d264 
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 > 
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 

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

29 

21021  30 
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; 
31 

11435  32 

33 
(** theory context references **) 

5177  34 

11435  35 
val f_myinv_f = thm "f_myinv_f"; 
36 
val myinv_f_f = thm "myinv_f_f"; 

37 

5177  38 

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

17412  40 
#exhaustion (the (Symtab.lookup dt_info tname)); 
5177  41 

42 
(******************************************************************************) 

43 

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

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

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

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

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

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

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

54 
val Lim_name = "Datatype.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, 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

60 
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

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

62 
"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

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

15570  65 
val descr' = List.concat descr; 
5177  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"; 

21021  70 
val rep_set_names' = 
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')))); 

22578  74 
val rep_set_names = map (Sign.full_name thy1) rep_set_names'; 
5177  75 

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

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

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

79 
val branchT = if null branchTs then HOLogic.unitT 
23419  80 
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

81 
val arities = get_arities descr' \ 0; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

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

5177  87 
val sumT = if null leafTs then HOLogic.unitT 
23419  88 
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

89 
val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); 
5177  90 
val UnivT = HOLogic.mk_setT Univ_elT; 
21021  91 
val UnivT' = Univ_elT > HOLogic.boolT; 
92 
val Collect = Const ("Collect", UnivT' > UnivT); 

5177  93 

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

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

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

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

97 
val Lim = Const (Lim_name, (branchT > Univ_elT) > Univ_elT); 
5177  98 

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

100 

101 
fun mk_inj T' x = 

102 
let 

103 
fun mk_inj' T n i = 

104 
if n = 1 then x else 

105 
let val n2 = n div 2; 

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

107 
in 

108 
if i <= n2 then 

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

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

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

114 
end; 

115 

116 
(* make injections for constructors *) 

117 

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

120 
right = fn t => In1 $ t, 

121 
init = 

122 
if ts = [] then Const ("arbitrary", Univ_elT) 

123 
else foldr1 (HOLogic.mk_binop Scons_name) ts}; 

5177  124 

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

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

126 

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

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

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

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

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

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

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

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

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

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

136 
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

137 
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

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

139 
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

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

141 

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

142 
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

143 

5177  144 
(************** generate introduction rules for representing set **********) 
145 

6427  146 
val _ = message "Constructing representing sets ..."; 
5177  147 

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

149 

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

151 
let 

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

152 
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

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

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

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

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

157 
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

158 
in (j + 1, list_all (map (pair "x") Ts, 
21021  159 
HOLogic.mk_Trueprop 
160 
(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

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

163 
 _ => 
5177  164 
let val T = typ_of_dtyp descr' sorts dt 
165 
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

166 
end); 
5177  167 

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

168 
val (_, prems, ts) = foldr mk_prem (1, [], []) cargs; 
21021  169 
val concl = HOLogic.mk_Trueprop 
170 
(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

171 
in Logic.list_implies (prems, concl) 
5177  172 
end; 
173 

15570  174 
val intr_ts = List.concat (map (fn ((_, (_, _, constrs)), rep_set_name) => 
5177  175 
map (make_intr rep_set_name (length constrs)) 
21021  176 
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names')); 
5177  177 

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

178 
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

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

180 
{quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, 
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

181 
alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false, 
96e82c7861fa
 use SkipProof.prove_global instead of Goal.prove_global
berghofe
parents:
26475
diff
changeset

182 
skip_mono = true} 
26128  183 
(map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') [] 
26475
3cc1e48d0ce1
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents:
26359
diff
changeset

184 
(map (fn x => (("", []), x)) intr_ts) [] thy1; 
5177  185 

186 
(********************************* typedef ********************************) 

187 

21021  188 
val (typedefs, thy3) = thy2 > 
189 
parent_path flat_names > 

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

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

191 
TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) 
21021  192 
(Collect $ Const (c, UnivT')) NONE 
193 
(rtac exI 1 THEN rtac CollectI 1 THEN 

194 
QUIET_BREADTH_FIRST (has_fewer_prems 1) 

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

195 
(resolve_tac rep_intrs 1))) 
21021  196 
(types_syntax ~~ tyvars ~~ 
197 
(Library.take (length newTs, rep_set_names)) ~~ new_type_names) > 

198 
add_path flat_names big_name; 

5177  199 

200 
(*********************** definition of constructors ***********************) 

201 

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

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

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

15570  205 
(1 upto (length (List.concat (tl descr)))); 
22578  206 
val all_rep_names = map (Sign.intern_const thy3) rep_names @ 
207 
map (Sign.full_name thy3) rep_names'; 

5177  208 

209 
(* isomorphism declarations *) 

210 

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

212 
(oldTs ~~ rep_names'); 

213 

214 
(* constructor definitions *) 

215 

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

217 
let 

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

219 
let val T = typ_of_dtyp descr' sorts dt; 

220 
val free_t = mk_Free "x" T j 

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

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

222 
((_, 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

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

224 
app_bnds free_t (length Us)) Us :: r_args) 
5177  225 
 _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) 
226 
end; 

227 

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

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

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

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

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

236 
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq 

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

18377  238 
val ([def_thm], thy') = 
239 
thy 

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

240 
> Sign.add_consts_i [(cname', constrT, mx)] 
18377  241 
> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]; 
5177  242 

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

245 
(* constructor definitions for datatype *) 

246 

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

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

249 
let 

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

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

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

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

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

261 

15570  262 
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

263 
((thy3 > Sign.add_consts_i iso_decls > parent_path flat_names, [], [], [], []), 
5177  264 
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); 
265 

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

267 

6427  268 
val _ = message "Proving isomorphism properties ..."; 
5177  269 

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

272 
collect_simp (#Rep td))) typedefs; 

5177  273 

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

5177  276 

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

278 

279 
(**) 

280 
(* isomorphisms are defined using primreccombinators: *) 

281 
(* generate appropriate functions for instantiating primreccombinator *) 

282 
(* *) 

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

283 
(* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) 
5177  284 
(* *) 
285 
(* also generate characteristic equations for isomorphisms *) 

286 
(* *) 

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

287 
(* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) 
5177  288 
(**) 
289 

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

291 
let 

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

15570  293 
val T = List.nth (recTs, k); 
294 
val rep_name = List.nth (all_rep_names, k); 

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

297 

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

298 
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

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

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

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

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

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

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

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

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

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

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

310 
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

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

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

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

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

322 

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

324 

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

326 

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

328 
let 

329 
val ks = map fst ds; 

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

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

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

334 
let 

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

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

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

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

18358  345 
val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; 
5177  346 

347 
(* prove characteristic equations *) 

348 

5553  349 
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

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

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

354 

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

355 
val (thy5, iso_char_thms) = foldr make_iso_defs 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

356 
(add_path flat_names big_name thy4, []) (tl descr); 
5177  357 

358 
(* prove isomorphism properties *) 

359 

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

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

361 
let 
22596  362 
val {thy, prop, ...} = rep_thm thm; 
21021  363 
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ 
16287  364 
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
13585
diff
changeset

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

366 

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

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

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

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

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

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

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

373 
(HOLogic.mk_Trueprop (HOLogic.list_all 
21021  374 
(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

375 
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, 
17985  376 
r $ (a $ app_bnds f i)), f)))) 
20046  377 
(fn _ => EVERY [REPEAT (rtac ext 1), 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

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

379 
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

380 

5177  381 
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) 
382 

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

384 
let 

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

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

388 
fun mk_ind_concl (i, _) = 

389 
let 

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

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

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

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

21021  396 
Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i)) 
5177  397 
end; 
398 

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

400 

5553  401 
val rewrites = map mk_meta_eq iso_char_thms; 
21021  402 
val inj_thms' = map snd newT_iso_inj_thms @ 
26359  403 
map (fn r => r RS @{thm injD}) inj_thms; 
5177  404 

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

405 
val inj_thm = SkipProof.prove_global thy5 [] [] 
17985  406 
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY 
25678  407 
[(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
5177  408 
REPEAT (EVERY 
409 
[rtac allI 1, rtac impI 1, 

410 
exh_tac (exh_thm_of dt_info) 1, 

411 
REPEAT (EVERY 

412 
[hyp_subst_tac 1, 

413 
rewrite_goals_tac rewrites, 

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

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

416 
ORELSE (EVERY 

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

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

418 
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

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

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

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

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

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

424 
Lim_inject :: fun_cong :: inj_thms')) 1), 
20046  425 
atac 1]))])])])]); 
5177  426 

26359  427 
val inj_thms'' = map (fn r => r RS @{thm datatype_injI}) 
6171  428 
(split_conj_thm inj_thm); 
5177  429 

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

431 
SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) 
20046  432 
(fn _ => 
25678  433 
EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, 
20046  434 
rewrite_goals_tac rewrites, 
435 
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW 

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

5177  437 

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

438 
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

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

440 

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

441 
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

442 
([], map #3 newT_iso_axms) (tl descr); 
21021  443 
val iso_inj_thms = map snd newT_iso_inj_thms @ 
26359  444 
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

445 

21021  446 
(* 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

447 

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

448 
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

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

450 
in HOLogic.imp $ 
21021  451 
(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

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

453 
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

454 
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

455 
Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T))) 
5177  456 
end; 
457 

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

458 
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

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

460 

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

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

462 

26359  463 
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

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

465 

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

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

468 
(SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY 
25678  469 
[(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

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

471 
rewrite_goals_tac (mk_meta_eq choice_eq :: 
26359  472 
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

473 
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

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

475 
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ 
15570  476 
List.concat (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

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

478 
rtac (sym RS range_eqI) 1, 
20046  479 
resolve_tac iso_char_thms 1])]))); 
11435  480 

481 
val Abs_inverse_thms' = 

482 
map #1 newT_iso_axms @ 

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

11435  485 

15570  486 
val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms'); 
5177  487 

488 
(******************* freeness theorems for constructors *******************) 

489 

6427  490 
val _ = message "Proving freeness of constructors ..."; 
5177  491 

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

493 

494 
fun prove_constr_rep_thm eqn = 

495 
let 

21021  496 
val inj_thms = map fst newT_iso_inj_thms; 
26359  497 
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

498 
in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY 
5177  499 
[resolve_tac inj_thms 1, 
500 
rewrite_goals_tac rewrites, 

21021  501 
rtac refl 3, 
5177  502 
resolve_tac rep_intrs 2, 
20046  503 
REPEAT (resolve_tac iso_elem_thms 1)]) 
5177  504 
end; 
505 

506 
(**) 

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

508 
(* of constructors. *) 
5177  509 
(**) 
510 

511 
val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns; 

512 

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

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

515 
(constr_rep_thms ~~ dist_lemmas); 

516 

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

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

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

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

520 
val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ => 
20046  521 
EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]) 
7015
85be09eb136c
 Datatype package now also supports arbitrarily branching datatypes
berghofe
parents:
6522
diff
changeset

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

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

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

525 

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

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

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

528 

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

529 
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => 
24112  530 
if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit 
24098
f1eb34ae33af
replaced dtK ref by datatype_distinctness_limit configuration option;
wenzelm
parents:
23590
diff
changeset

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

532 
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

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

534 

5177  535 
(* prove injectivity of constructors *) 
536 

537 
fun prove_constr_inj_thm rep_thms t = 

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

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

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

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

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

545 
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

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

548 
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

549 
REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), 
20046  550 
atac 1]))]) 
5177  551 
end; 
552 

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

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

555 

18314  556 
val ((constr_inject', distinct_thms'), thy6) = 
557 
thy5 

558 
> parent_path flat_names 

559 
> store_thmss "inject" new_type_names constr_inject 

560 
>> store_thmss "distinct" new_type_names distinct_thms; 

5177  561 

562 
(*************************** induction theorem ****************************) 

563 

6427  564 
val _ = message "Proving induction rule for datatypes ..."; 
5177  565 

566 
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

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

568 
val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; 
5177  569 

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

571 
let 

15570  572 
val Rep_t = Const (List.nth (all_rep_names, i), T > Univ_elT) $ 
5177  573 
mk_Free "x" T i; 
574 

575 
val Abs_t = if i < length newTs then 

22578  576 
Const (Sign.intern_const thy6 
15570  577 
("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT > T) 
11435  578 
else Const ("Inductive.myinv", [T > Univ_elT, Univ_elT] > T) $ 
15570  579 
Const (List.nth (all_rep_names, i), T > Univ_elT) 
5177  580 

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

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

585 
end; 

586 

587 
val (indrule_lemma_prems, indrule_lemma_concls) = 

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

22578  590 
val cert = cterm_of thy6; 
5177  591 

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

592 
val indrule_lemma = SkipProof.prove_global thy6 [] [] 
5177  593 
(Logic.mk_implies 
594 
(HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), 

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

5177  597 
REPEAT (EVERY 
598 
[TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, 

20046  599 
etac mp 1, resolve_tac iso_elem_thms 1])]); 
5177  600 

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

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

605 

17985  606 
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

607 
val dt_induct = SkipProof.prove_global thy6 [] 
17985  608 
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) 
609 
(fn prems => EVERY 

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

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

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

615 
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) 
20046  616 
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); 
5177  617 

18377  618 
val ([dt_induct'], thy7) = 
619 
thy6 

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

620 
> Sign.add_path big_name 
18377  621 
> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24112
diff
changeset

622 
> Sign.parent_path; 
5177  623 

18314  624 
in 
625 
((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7) 

5177  626 
end; 
627 

628 
end; 