1 (* Title: HOL/Tools/datatype_rep_proofs.ML |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 |
|
4 Definitional introduction of datatypes |
|
5 Proof of characteristic theorems: |
|
6 |
|
7 - injectivity of constructors |
|
8 - distinctness of constructors |
|
9 - induction theorem |
|
10 *) |
|
11 |
|
12 signature DATATYPE_REP_PROOFS = |
|
13 sig |
|
14 val distinctness_limit : int Config.T |
|
15 val distinctness_limit_setup : theory -> theory |
|
16 val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table -> |
|
17 string list -> DatatypeAux.descr list -> (string * sort) list -> |
|
18 (binding * mixfix) list -> (binding * mixfix) list list -> attribute |
|
19 -> theory -> (thm list list * thm list list * thm list list * |
|
20 DatatypeAux.simproc_dist list * thm) * theory |
|
21 end; |
|
22 |
|
23 structure DatatypeRepProofs : DATATYPE_REP_PROOFS = |
|
24 struct |
|
25 |
|
26 open DatatypeAux; |
|
27 |
|
28 (*the kind of distinctiveness axioms depends on number of constructors*) |
|
29 val (distinctness_limit, distinctness_limit_setup) = |
|
30 Attrib.config_int "datatype_distinctness_limit" 7; |
|
31 |
|
32 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); |
|
33 |
|
34 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; |
|
35 |
|
36 |
|
37 (** theory context references **) |
|
38 |
|
39 val f_myinv_f = thm "f_myinv_f"; |
|
40 val myinv_f_f = thm "myinv_f_f"; |
|
41 |
|
42 |
|
43 fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = |
|
44 #exhaustion (the (Symtab.lookup dt_info tname)); |
|
45 |
|
46 (******************************************************************************) |
|
47 |
|
48 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) |
|
49 new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = |
|
50 let |
|
51 val Datatype_thy = ThyInfo.the_theory "Datatype" thy; |
|
52 val node_name = "Datatype.node"; |
|
53 val In0_name = "Datatype.In0"; |
|
54 val In1_name = "Datatype.In1"; |
|
55 val Scons_name = "Datatype.Scons"; |
|
56 val Leaf_name = "Datatype.Leaf"; |
|
57 val Numb_name = "Datatype.Numb"; |
|
58 val Lim_name = "Datatype.Lim"; |
|
59 val Suml_name = "Datatype.Suml"; |
|
60 val Sumr_name = "Datatype.Sumr"; |
|
61 |
|
62 val [In0_inject, In1_inject, Scons_inject, Leaf_inject, |
|
63 In0_eq, In1_eq, In0_not_In1, In1_not_In0, |
|
64 Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy) |
|
65 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
|
66 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
|
67 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
|
68 |
|
69 val descr' = flat descr; |
|
70 |
|
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"; |
|
74 val rep_set_names' = |
|
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')))); |
|
78 val rep_set_names = map (Sign.full_bname thy1) rep_set_names'; |
|
79 |
|
80 val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr); |
|
81 val leafTs' = get_nonrec_types descr' sorts; |
|
82 val branchTs = get_branching_types descr' sorts; |
|
83 val branchT = if null branchTs then HOLogic.unitT |
|
84 else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs; |
|
85 val arities = get_arities descr' \ 0; |
|
86 val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs); |
|
87 val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars); |
|
88 val recTs = get_rec_types descr' sorts; |
|
89 val newTs = Library.take (length (hd descr), recTs); |
|
90 val oldTs = Library.drop (length (hd descr), recTs); |
|
91 val sumT = if null leafTs then HOLogic.unitT |
|
92 else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs; |
|
93 val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); |
|
94 val UnivT = HOLogic.mk_setT Univ_elT; |
|
95 val UnivT' = Univ_elT --> HOLogic.boolT; |
|
96 val Collect = Const ("Collect", UnivT' --> UnivT); |
|
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); |
|
101 val Lim = Const (Lim_name, (branchT --> Univ_elT) --> Univ_elT); |
|
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 |
|
113 Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i) |
|
114 else |
|
115 Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) |
|
116 end |
|
117 in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs) |
|
118 end; |
|
119 |
|
120 (* make injections for constructors *) |
|
121 |
|
122 fun mk_univ_inj ts = BalancedTree.access |
|
123 {left = fn t => In0 $ t, |
|
124 right = fn t => In1 $ t, |
|
125 init = |
|
126 if ts = [] then Const (@{const_name undefined}, Univ_elT) |
|
127 else foldr1 (HOLogic.mk_binop Scons_name) ts}; |
|
128 |
|
129 (* function spaces *) |
|
130 |
|
131 fun mk_fun_inj T' x = |
|
132 let |
|
133 fun mk_inj T n i = |
|
134 if n = 1 then x else |
|
135 let |
|
136 val n2 = n div 2; |
|
137 val Type (_, [T1, T2]) = T; |
|
138 fun mkT U = (U --> Univ_elT) --> T --> Univ_elT |
|
139 in |
|
140 if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i |
|
141 else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2) |
|
142 end |
|
143 in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs) |
|
144 end; |
|
145 |
|
146 val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t))); |
|
147 |
|
148 (************** generate introduction rules for representing set **********) |
|
149 |
|
150 val _ = message "Constructing representing sets ..."; |
|
151 |
|
152 (* make introduction rule for a single constructor *) |
|
153 |
|
154 fun make_intr s n (i, (_, cargs)) = |
|
155 let |
|
156 fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of |
|
157 (dts, DtRec k) => |
|
158 let |
|
159 val Ts = map (typ_of_dtyp descr' sorts) dts; |
|
160 val free_t = |
|
161 app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts) |
|
162 in (j + 1, list_all (map (pair "x") Ts, |
|
163 HOLogic.mk_Trueprop |
|
164 (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems, |
|
165 mk_lim free_t Ts :: ts) |
|
166 end |
|
167 | _ => |
|
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) |
|
170 end); |
|
171 |
|
172 val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs; |
|
173 val concl = HOLogic.mk_Trueprop |
|
174 (Free (s, UnivT') $ mk_univ_inj ts n i) |
|
175 in Logic.list_implies (prems, concl) |
|
176 end; |
|
177 |
|
178 val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) => |
|
179 map (make_intr rep_set_name (length constrs)) |
|
180 ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'); |
|
181 |
|
182 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = |
|
183 InductivePackage.add_inductive_global (serial_string ()) |
|
184 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, |
|
185 alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, |
|
186 skip_mono = true, fork_mono = false} |
|
187 (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] |
|
188 (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1; |
|
189 |
|
190 (********************************* typedef ********************************) |
|
191 |
|
192 val (typedefs, thy3) = thy2 |> |
|
193 parent_path flat_names |> |
|
194 fold_map (fn ((((name, mx), tvs), c), name') => |
|
195 TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx) |
|
196 (Collect $ Const (c, UnivT')) NONE |
|
197 (rtac exI 1 THEN rtac CollectI 1 THEN |
|
198 QUIET_BREADTH_FIRST (has_fewer_prems 1) |
|
199 (resolve_tac rep_intrs 1))) |
|
200 (types_syntax ~~ tyvars ~~ |
|
201 (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||> |
|
202 add_path flat_names big_name; |
|
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)) |
|
209 (1 upto (length (flat (tl descr)))); |
|
210 val all_rep_names = map (Sign.intern_const thy3) rep_names @ |
|
211 map (Sign.full_bname thy3) rep_names'; |
|
212 |
|
213 (* isomorphism declarations *) |
|
214 |
|
215 val iso_decls = map (fn (T, s) => (Binding.name 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 |
|
225 in (case (strip_dtyp dt, strip_type T) of |
|
226 ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim |
|
227 (Const (List.nth (all_rep_names, m), U --> Univ_elT) $ |
|
228 app_bnds free_t (length Us)) Us :: r_args) |
|
229 | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) |
|
230 end; |
|
231 |
|
232 val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs; |
|
233 val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T; |
|
234 val abs_name = Sign.intern_const thy ("Abs_" ^ tname); |
|
235 val rep_name = Sign.intern_const thy ("Rep_" ^ tname); |
|
236 val lhs = list_comb (Const (cname, constrT), l_args); |
|
237 val rhs = mk_univ_inj r_args n i; |
|
238 val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs); |
|
239 val def_name = Long_Name.base_name cname ^ "_def"; |
|
240 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
241 (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); |
|
242 val ([def_thm], thy') = |
|
243 thy |
|
244 |> Sign.add_consts_i [(cname', constrT, mx)] |
|
245 |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; |
|
246 |
|
247 in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; |
|
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; |
|
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); |
|
259 val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) |
|
260 ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) |
|
261 in |
|
262 (parent_path flat_names thy', defs', eqns @ [eqns'], |
|
263 rep_congs @ [cong'], dist_lemmas @ [dist]) |
|
264 end; |
|
265 |
|
266 val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs |
|
267 ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []), |
|
268 hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); |
|
269 |
|
270 (*********** isomorphisms for new types (introduced by typedef) ***********) |
|
271 |
|
272 val _ = message "Proving isomorphism properties ..."; |
|
273 |
|
274 val newT_iso_axms = map (fn (_, td) => |
|
275 (collect_simp (#Abs_inverse td), #Rep_inverse td, |
|
276 collect_simp (#Rep td))) typedefs; |
|
277 |
|
278 val newT_iso_inj_thms = map (fn (_, td) => |
|
279 (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs; |
|
280 |
|
281 (********* isomorphisms between existing types and "unfolded" types *******) |
|
282 |
|
283 (*---------------------------------------------------------------------*) |
|
284 (* isomorphisms are defined using primrec-combinators: *) |
|
285 (* generate appropriate functions for instantiating primrec-combinator *) |
|
286 (* *) |
|
287 (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) |
|
288 (* *) |
|
289 (* also generate characteristic equations for isomorphisms *) |
|
290 (* *) |
|
291 (* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *) |
|
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; |
|
297 val T = List.nth (recTs, k); |
|
298 val rep_name = List.nth (all_rep_names, k); |
|
299 val rep_const = Const (rep_name, T --> Univ_elT); |
|
300 val constr = Const (cname, argTs ---> T); |
|
301 |
|
302 fun process_arg ks' ((i2, i2', ts, Ts), dt) = |
|
303 let |
|
304 val T' = typ_of_dtyp descr' sorts dt; |
|
305 val (Us, U) = strip_type T' |
|
306 in (case strip_dtyp dt of |
|
307 (_, DtRec j) => if j mem ks' then |
|
308 (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds |
|
309 (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us], |
|
310 Ts @ [Us ---> Univ_elT]) |
|
311 else |
|
312 (i2 + 1, i2', ts @ [mk_lim |
|
313 (Const (List.nth (all_rep_names, j), U --> Univ_elT) $ |
|
314 app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts) |
|
315 | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) |
|
316 end; |
|
317 |
|
318 val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs); |
|
319 val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1))); |
|
320 val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1))); |
|
321 val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); |
|
322 |
|
323 val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs); |
|
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; |
|
335 val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname); |
|
336 |
|
337 fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = |
|
338 let |
|
339 val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs)) |
|
340 ((fs, eqns, 1), constrs); |
|
341 val iso = (List.nth (recTs, k), List.nth (all_rep_names, k)) |
|
342 in (fs', eqns', isos @ [iso]) end; |
|
343 |
|
344 val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); |
|
345 val fTs = map fastype_of fs; |
|
346 val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"), |
|
347 Logic.mk_equals (Const (iso_name, T --> Univ_elT), |
|
348 list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); |
|
349 val (def_thms, thy') = |
|
350 apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy); |
|
351 |
|
352 (* prove characteristic equations *) |
|
353 |
|
354 val rewrites = def_thms @ (map mk_meta_eq rec_rewrites); |
|
355 val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn |
|
356 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns; |
|
357 |
|
358 in (thy', char_thms' @ char_thms) end; |
|
359 |
|
360 val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs |
|
361 (add_path flat_names big_name thy4, []) (tl descr)); |
|
362 |
|
363 (* prove isomorphism properties *) |
|
364 |
|
365 fun mk_funs_inv thy thm = |
|
366 let |
|
367 val prop = Thm.prop_of thm; |
|
368 val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ |
|
369 (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; |
|
370 val used = OldTerm.add_term_tfree_names (a, []); |
|
371 |
|
372 fun mk_thm i = |
|
373 let |
|
374 val Ts = map (TFree o rpair HOLogic.typeS) |
|
375 (Name.variant_list used (replicate i "'t")); |
|
376 val f = Free ("f", Ts ---> U) |
|
377 in SkipProof.prove_global thy [] [] (Logic.mk_implies |
|
378 (HOLogic.mk_Trueprop (HOLogic.list_all |
|
379 (map (pair "x") Ts, S $ app_bnds f i)), |
|
380 HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts, |
|
381 r $ (a $ app_bnds f i)), f)))) |
|
382 (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1), |
|
383 REPEAT (etac allE 1), rtac thm 1, atac 1]) |
|
384 end |
|
385 in map (fn r => r RS subst) (thm :: map mk_thm arities) end; |
|
386 |
|
387 (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) |
|
388 |
|
389 val fun_congs = map (fn T => make_elim (Drule.instantiate' |
|
390 [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs; |
|
391 |
|
392 fun prove_iso_thms (ds, (inj_thms, elem_thms)) = |
|
393 let |
|
394 val (_, (tname, _, _)) = hd ds; |
|
395 val {induction, ...} = the (Symtab.lookup dt_info tname); |
|
396 |
|
397 fun mk_ind_concl (i, _) = |
|
398 let |
|
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) |
|
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)), |
|
405 Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i)) |
|
406 end; |
|
407 |
|
408 val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); |
|
409 |
|
410 val rewrites = map mk_meta_eq iso_char_thms; |
|
411 val inj_thms' = map snd newT_iso_inj_thms @ |
|
412 map (fn r => r RS @{thm injD}) inj_thms; |
|
413 |
|
414 val inj_thm = SkipProof.prove_global thy5 [] [] |
|
415 (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY |
|
416 [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, |
|
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 |
|
426 [REPEAT (eresolve_tac (Scons_inject :: |
|
427 map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1), |
|
428 REPEAT (cong_tac 1), rtac refl 1, |
|
429 REPEAT (atac 1 ORELSE (EVERY |
|
430 [REPEAT (rtac ext 1), |
|
431 REPEAT (eresolve_tac (mp :: allE :: |
|
432 map make_elim (Suml_inject :: Sumr_inject :: |
|
433 Lim_inject :: inj_thms') @ fun_congs) 1), |
|
434 atac 1]))])])])]); |
|
435 |
|
436 val inj_thms'' = map (fn r => r RS @{thm datatype_injI}) |
|
437 (split_conj_thm inj_thm); |
|
438 |
|
439 val elem_thm = |
|
440 SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) |
|
441 (fn _ => |
|
442 EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, |
|
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)]); |
|
446 |
|
447 in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) |
|
448 end; |
|
449 |
|
450 val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms |
|
451 ([], map #3 newT_iso_axms) (tl descr); |
|
452 val iso_inj_thms = map snd newT_iso_inj_thms @ |
|
453 map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded; |
|
454 |
|
455 (* prove dt_rep_set_i x --> x : range dt_Rep_i *) |
|
456 |
|
457 fun mk_iso_t (((set_name, iso_name), i), T) = |
|
458 let val isoT = T --> Univ_elT |
|
459 in HOLogic.imp $ |
|
460 (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $ |
|
461 (if i < length newTs then Const ("True", HOLogic.boolT) |
|
462 else HOLogic.mk_mem (mk_Free "x" Univ_elT i, |
|
463 Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $ |
|
464 Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T))) |
|
465 end; |
|
466 |
|
467 val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t |
|
468 (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs))); |
|
469 |
|
470 (* all the theorems are proved by one single simultaneous induction *) |
|
471 |
|
472 val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq})) |
|
473 iso_inj_thms_unfolded; |
|
474 |
|
475 val iso_thms = if length descr = 1 then [] else |
|
476 Library.drop (length newTs, split_conj_thm |
|
477 (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY |
|
478 [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, |
|
479 REPEAT (rtac TrueI 1), |
|
480 rewrite_goals_tac (mk_meta_eq choice_eq :: |
|
481 symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), |
|
482 rewrite_goals_tac (map symmetric range_eqs), |
|
483 REPEAT (EVERY |
|
484 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ |
|
485 maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1), |
|
486 TRY (hyp_subst_tac 1), |
|
487 rtac (sym RS range_eqI) 1, |
|
488 resolve_tac iso_char_thms 1])]))); |
|
489 |
|
490 val Abs_inverse_thms' = |
|
491 map #1 newT_iso_axms @ |
|
492 map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp]) |
|
493 iso_inj_thms_unfolded iso_thms; |
|
494 |
|
495 val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms'; |
|
496 |
|
497 (******************* freeness theorems for constructors *******************) |
|
498 |
|
499 val _ = message "Proving freeness of constructors ..."; |
|
500 |
|
501 (* prove theorem Rep_i (Constr_j ...) = Inj_j ... *) |
|
502 |
|
503 fun prove_constr_rep_thm eqn = |
|
504 let |
|
505 val inj_thms = map fst newT_iso_inj_thms; |
|
506 val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms) |
|
507 in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY |
|
508 [resolve_tac inj_thms 1, |
|
509 rewrite_goals_tac rewrites, |
|
510 rtac refl 3, |
|
511 resolve_tac rep_intrs 2, |
|
512 REPEAT (resolve_tac iso_elem_thms 1)]) |
|
513 end; |
|
514 |
|
515 (*--------------------------------------------------------------*) |
|
516 (* constr_rep_thms and rep_congs are used to prove distinctness *) |
|
517 (* of constructors. *) |
|
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 |
|
526 fun prove_distinct_thms _ _ (_, []) = [] |
|
527 | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) = |
|
528 if k >= lim then [] else let |
|
529 (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*) |
|
530 fun prove [] = [] |
|
531 | prove (t :: ts) = |
|
532 let |
|
533 val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ => |
|
534 EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]) |
|
535 in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end; |
|
536 in prove ts end; |
|
537 |
|
538 val distinct_thms = DatatypeProp.make_distincts descr sorts |
|
539 |> map2 (prove_distinct_thms |
|
540 (Config.get_thy thy5 distinctness_limit)) dist_rewrites; |
|
541 |
|
542 val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) => |
|
543 if length constrs < Config.get_thy thy5 distinctness_limit |
|
544 then FewConstrs dists |
|
545 else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~ |
|
546 constr_rep_thms ~~ rep_congs ~~ distinct_thms); |
|
547 |
|
548 (* prove injectivity of constructors *) |
|
549 |
|
550 fun prove_constr_inj_thm rep_thms t = |
|
551 let val inj_thms = Scons_inject :: (map make_elim |
|
552 (iso_inj_thms @ |
|
553 [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, |
|
554 Lim_inject, Suml_inject, Sumr_inject])) |
|
555 in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY |
|
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, |
|
559 REPEAT (resolve_tac rep_thms 1), |
|
560 REPEAT (eresolve_tac inj_thms 1), |
|
561 REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1), |
|
562 REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), |
|
563 atac 1]))]) |
|
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 |
|
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; |
|
574 |
|
575 (*************************** induction theorem ****************************) |
|
576 |
|
577 val _ = message "Proving induction rule for datatypes ..."; |
|
578 |
|
579 val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @ |
|
580 (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); |
|
581 val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; |
|
582 |
|
583 fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = |
|
584 let |
|
585 val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $ |
|
586 mk_Free "x" T i; |
|
587 |
|
588 val Abs_t = if i < length newTs then |
|
589 Const (Sign.intern_const thy6 |
|
590 ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T) |
|
591 else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $ |
|
592 Const (List.nth (all_rep_names, i), T --> Univ_elT) |
|
593 |
|
594 in (prems @ [HOLogic.imp $ |
|
595 (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $ |
|
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) = |
|
601 Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); |
|
602 |
|
603 val cert = cterm_of thy6; |
|
604 |
|
605 val indrule_lemma = SkipProof.prove_global thy6 [] [] |
|
606 (Logic.mk_implies |
|
607 (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), |
|
608 HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY |
|
609 [REPEAT (etac conjE 1), |
|
610 REPEAT (EVERY |
|
611 [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1, |
|
612 etac mp 1, resolve_tac iso_elem_thms 1])]); |
|
613 |
|
614 val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma))); |
|
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 |
|
619 val dt_induct_prop = DatatypeProp.make_ind descr sorts; |
|
620 val dt_induct = SkipProof.prove_global thy6 [] |
|
621 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) |
|
622 (fn {prems, ...} => EVERY |
|
623 [rtac indrule_lemma' 1, |
|
624 (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, |
|
625 EVERY (map (fn (prem, r) => (EVERY |
|
626 [REPEAT (eresolve_tac Abs_inverse_thms 1), |
|
627 simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, |
|
628 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) |
|
629 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); |
|
630 |
|
631 val ([dt_induct'], thy7) = |
|
632 thy6 |
|
633 |> Sign.add_path big_name |
|
634 |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] |
|
635 ||> Sign.parent_path |
|
636 ||> Theory.checkpoint; |
|
637 |
|
638 in |
|
639 ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7) |
|
640 end; |
|
641 |
|
642 end; |
|