14 val distinct_lemma: thm |
11 val distinct_lemma: thm |
15 type spec_cmd = |
12 type spec_cmd = |
16 (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list |
13 (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list |
17 val read_specs: spec_cmd list -> theory -> spec list * Proof.context |
14 val read_specs: spec_cmd list -> theory -> spec list * Proof.context |
18 val check_specs: spec list -> theory -> spec list * Proof.context |
15 val check_specs: spec list -> theory -> spec list * Proof.context |
19 val add_datatype: config -> spec list -> theory -> string list * theory |
|
20 val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory |
|
21 end; |
16 end; |
22 |
17 |
23 structure Old_Datatype : OLD_DATATYPE = |
18 structure Old_Datatype : OLD_DATATYPE = |
24 struct |
19 struct |
25 |
20 |
26 (** auxiliary **) |
|
27 |
|
28 val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover}; |
21 val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover}; |
29 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (Thm.prems_of distinct_lemma); |
|
30 |
|
31 fun exh_thm_of (dt_info : Old_Datatype_Aux.info Symtab.table) tname = |
|
32 #exhaust (the (Symtab.lookup dt_info tname)); |
|
33 |
|
34 val In0_inject = @{thm In0_inject}; |
|
35 val In1_inject = @{thm In1_inject}; |
|
36 val Scons_inject = @{thm Scons_inject}; |
|
37 val Leaf_inject = @{thm Leaf_inject}; |
|
38 val In0_eq = @{thm In0_eq}; |
|
39 val In1_eq = @{thm In1_eq}; |
|
40 val In0_not_In1 = @{thm In0_not_In1}; |
|
41 val In1_not_In0 = @{thm In1_not_In0}; |
|
42 val Lim_inject = @{thm Lim_inject}; |
|
43 val Inl_inject = @{thm Inl_inject}; |
|
44 val Inr_inject = @{thm Inr_inject}; |
|
45 val Suml_inject = @{thm Suml_inject}; |
|
46 val Sumr_inject = @{thm Sumr_inject}; |
|
47 |
|
48 val datatype_injI = |
|
49 @{lemma "(\<And>x. \<forall>y. f x = f y \<longrightarrow> x = y) \<Longrightarrow> inj f" by (simp add: inj_on_def)}; |
|
50 |
|
51 |
|
52 (** proof of characteristic theorems **) |
|
53 |
|
54 fun representation_proofs (config : Old_Datatype_Aux.config) |
|
55 (dt_info : Old_Datatype_Aux.info Symtab.table) descr types_syntax constr_syntax case_names_induct |
|
56 thy = |
|
57 let |
|
58 val descr' = flat descr; |
|
59 val new_type_names = map (Binding.name_of o fst) types_syntax; |
|
60 val big_name = space_implode "_" new_type_names; |
|
61 val thy1 = Sign.add_path big_name thy; |
|
62 val big_rec_name = "rep_set_" ^ big_name; |
|
63 val rep_set_names' = |
|
64 if length descr' = 1 then [big_rec_name] |
|
65 else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto length descr'); |
|
66 val rep_set_names = map (Sign.full_bname thy1) rep_set_names'; |
|
67 |
|
68 val tyvars = map (fn (_, (_, Ts, _)) => map Old_Datatype_Aux.dest_DtTFree Ts) (hd descr); |
|
69 val leafTs' = Old_Datatype_Aux.get_nonrec_types descr'; |
|
70 val branchTs = Old_Datatype_Aux.get_branching_types descr'; |
|
71 val branchT = |
|
72 if null branchTs then HOLogic.unitT |
|
73 else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) branchTs; |
|
74 val arities = remove (op =) 0 (Old_Datatype_Aux.get_arities descr'); |
|
75 val unneeded_vars = |
|
76 subtract (op =) (fold Term.add_tfreesT (leafTs' @ branchTs) []) (hd tyvars); |
|
77 val leafTs = leafTs' @ map TFree unneeded_vars; |
|
78 val recTs = Old_Datatype_Aux.get_rec_types descr'; |
|
79 val (newTs, oldTs) = chop (length (hd descr)) recTs; |
|
80 val sumT = |
|
81 if null leafTs then HOLogic.unitT |
|
82 else Balanced_Tree.make (fn (T, U) => Type (@{type_name Sum_Type.sum}, [T, U])) leafTs; |
|
83 val Univ_elT = HOLogic.mk_setT (Type (@{type_name Old_Datatype.node}, [sumT, branchT])); |
|
84 val UnivT = HOLogic.mk_setT Univ_elT; |
|
85 val UnivT' = Univ_elT --> HOLogic.boolT; |
|
86 val Collect = Const (@{const_name Collect}, UnivT' --> UnivT); |
|
87 |
|
88 val In0 = Const (@{const_name Old_Datatype.In0}, Univ_elT --> Univ_elT); |
|
89 val In1 = Const (@{const_name Old_Datatype.In1}, Univ_elT --> Univ_elT); |
|
90 val Leaf = Const (@{const_name Old_Datatype.Leaf}, sumT --> Univ_elT); |
|
91 val Lim = Const (@{const_name Old_Datatype.Lim}, (branchT --> Univ_elT) --> Univ_elT); |
|
92 |
|
93 (* make injections needed for embedding types in leaves *) |
|
94 |
|
95 fun mk_inj T' x = |
|
96 let |
|
97 fun mk_inj' T n i = |
|
98 if n = 1 then x |
|
99 else |
|
100 let |
|
101 val n2 = n div 2; |
|
102 val Type (_, [T1, T2]) = T; |
|
103 in |
|
104 if i <= n2 |
|
105 then Const (@{const_name Inl}, T1 --> T) $ mk_inj' T1 n2 i |
|
106 else Const (@{const_name Inr}, T2 --> T) $ mk_inj' T2 (n - n2) (i - n2) |
|
107 end; |
|
108 in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end; |
|
109 |
|
110 (* make injections for constructors *) |
|
111 |
|
112 fun mk_univ_inj ts = Balanced_Tree.access |
|
113 {left = fn t => In0 $ t, |
|
114 right = fn t => In1 $ t, |
|
115 init = |
|
116 if ts = [] then Const (@{const_name undefined}, Univ_elT) |
|
117 else foldr1 (HOLogic.mk_binop @{const_name Old_Datatype.Scons}) ts}; |
|
118 |
|
119 (* function spaces *) |
|
120 |
|
121 fun mk_fun_inj T' x = |
|
122 let |
|
123 fun mk_inj T n i = |
|
124 if n = 1 then x |
|
125 else |
|
126 let |
|
127 val n2 = n div 2; |
|
128 val Type (_, [T1, T2]) = T; |
|
129 fun mkT U = (U --> Univ_elT) --> T --> Univ_elT; |
|
130 in |
|
131 if i <= n2 then Const (@{const_name Sum_Type.Suml}, mkT T1) $ mk_inj T1 n2 i |
|
132 else Const (@{const_name Sum_Type.Sumr}, mkT T2) $ mk_inj T2 (n - n2) (i - n2) |
|
133 end; |
|
134 in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs) end; |
|
135 |
|
136 fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t; |
|
137 |
|
138 (************** generate introduction rules for representing set **********) |
|
139 |
|
140 val _ = Old_Datatype_Aux.message config "Constructing representing sets ..."; |
|
141 |
|
142 (* make introduction rule for a single constructor *) |
|
143 |
|
144 fun make_intr s n (i, (_, cargs)) = |
|
145 let |
|
146 fun mk_prem dt (j, prems, ts) = |
|
147 (case Old_Datatype_Aux.strip_dtyp dt of |
|
148 (dts, Old_Datatype_Aux.DtRec k) => |
|
149 let |
|
150 val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') dts; |
|
151 val free_t = |
|
152 Old_Datatype_Aux.app_bnds (Old_Datatype_Aux.mk_Free "x" (Ts ---> Univ_elT) j) |
|
153 (length Ts) |
|
154 in |
|
155 (j + 1, Logic.list_all (map (pair "x") Ts, |
|
156 HOLogic.mk_Trueprop |
|
157 (Free (nth rep_set_names' k, UnivT') $ free_t)) :: prems, |
|
158 mk_lim free_t Ts :: ts) |
|
159 end |
|
160 | _ => |
|
161 let val T = Old_Datatype_Aux.typ_of_dtyp descr' dt |
|
162 in (j + 1, prems, (Leaf $ mk_inj T (Old_Datatype_Aux.mk_Free "x" T j)) :: ts) end); |
|
163 |
|
164 val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []); |
|
165 val concl = HOLogic.mk_Trueprop (Free (s, UnivT') $ mk_univ_inj ts n i); |
|
166 in Logic.list_implies (prems, concl) end; |
|
167 |
|
168 val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) => |
|
169 map (make_intr rep_set_name (length constrs)) |
|
170 ((1 upto length constrs) ~~ constrs)) (descr' ~~ rep_set_names'); |
|
171 |
|
172 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = |
|
173 thy1 |
|
174 |> Sign.concealed |
|
175 |> Inductive.add_inductive_global |
|
176 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name, |
|
177 coind = false, no_elim = true, no_ind = false, skip_mono = true} |
|
178 (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] |
|
179 (map (fn x => (Binding.empty_atts, x)) intr_ts) [] |
|
180 ||> Sign.restore_naming thy1; |
|
181 |
|
182 (********************************* typedef ********************************) |
|
183 |
|
184 val (typedefs, thy3) = thy2 |
|
185 |> Sign.parent_path |
|
186 |> fold_map |
|
187 (fn (((name, mx), tvs), c) => |
|
188 Typedef.add_typedef_global {overloaded = false} (name, tvs, mx) |
|
189 (Collect $ Const (c, UnivT')) NONE |
|
190 (fn ctxt => |
|
191 resolve_tac ctxt [exI] 1 THEN |
|
192 resolve_tac ctxt [CollectI] 1 THEN |
|
193 QUIET_BREADTH_FIRST (has_fewer_prems 1) |
|
194 (resolve_tac ctxt rep_intrs 1))) |
|
195 (types_syntax ~~ tyvars ~~ take (length newTs) rep_set_names) |
|
196 ||> Sign.add_path big_name; |
|
197 |
|
198 (*********************** definition of constructors ***********************) |
|
199 |
|
200 val big_rep_name = big_name ^ "_Rep_"; |
|
201 val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr))); |
|
202 val all_rep_names = |
|
203 map (#Rep_name o #1 o #2) typedefs @ |
|
204 map (Sign.full_bname thy3) rep_names'; |
|
205 |
|
206 (* isomorphism declarations *) |
|
207 |
|
208 val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn)) |
|
209 (oldTs ~~ rep_names'); |
|
210 |
|
211 (* constructor definitions *) |
|
212 |
|
213 fun make_constr_def (typedef: Typedef.info) T n |
|
214 ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = |
|
215 let |
|
216 fun constr_arg dt (j, l_args, r_args) = |
|
217 let |
|
218 val T = Old_Datatype_Aux.typ_of_dtyp descr' dt; |
|
219 val free_t = Old_Datatype_Aux.mk_Free "x" T j; |
|
220 in |
|
221 (case (Old_Datatype_Aux.strip_dtyp dt, strip_type T) of |
|
222 ((_, Old_Datatype_Aux.DtRec m), (Us, U)) => |
|
223 (j + 1, free_t :: l_args, mk_lim |
|
224 (Const (nth all_rep_names m, U --> Univ_elT) $ |
|
225 Old_Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args) |
|
226 | _ => (j + 1, free_t :: l_args, (Leaf $ mk_inj T free_t) :: r_args)) |
|
227 end; |
|
228 |
|
229 val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []); |
|
230 val constrT = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs ---> T; |
|
231 val ({Abs_name, Rep_name, ...}, _) = typedef; |
|
232 val lhs = list_comb (Const (cname, constrT), l_args); |
|
233 val rhs = mk_univ_inj r_args n i; |
|
234 val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs); |
|
235 val def_name = Thm.def_name (Long_Name.base_name cname); |
|
236 val eqn = |
|
237 HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs)); |
|
238 val ([def_thm], thy') = |
|
239 thy |
|
240 |> Sign.add_consts [(cname', constrT, mx)] |
|
241 |> (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]; |
|
242 |
|
243 in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end; |
|
244 |
|
245 (* constructor definitions for datatype *) |
|
246 |
|
247 fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax) |
|
248 (thy, defs, eqns, rep_congs, dist_lemmas) = |
|
249 let |
|
250 val ctxt = Proof_Context.init_global thy; |
|
251 val _ $ (_ $ (cong_f $ _) $ _) = Thm.concl_of arg_cong; |
|
252 val rep_const = Thm.cterm_of ctxt (Const (#Rep_name (#1 typedef), T --> Univ_elT)); |
|
253 val cong' = infer_instantiate ctxt [(#1 (dest_Var cong_f), rep_const)] arg_cong; |
|
254 val dist = infer_instantiate ctxt [(#1 (dest_Var distinct_f), rep_const)] distinct_lemma; |
|
255 val (thy', defs', eqns', _) = |
|
256 fold (make_constr_def typedef T (length constrs)) |
|
257 (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1); |
|
258 in |
|
259 (Sign.parent_path thy', defs', eqns @ [eqns'], |
|
260 rep_congs @ [cong'], dist_lemmas @ [dist]) |
|
261 end; |
|
262 |
|
263 val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = |
|
264 fold dt_constr_defs |
|
265 (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax) |
|
266 (thy3 |> Sign.add_consts iso_decls |> Sign.parent_path, [], [], [], []); |
|
267 |
|
268 |
|
269 (*********** isomorphisms for new types (introduced by typedef) ***********) |
|
270 |
|
271 val _ = Old_Datatype_Aux.message config "Proving isomorphism properties ..."; |
|
272 |
|
273 val collect_simp = rewrite_rule (Proof_Context.init_global thy4) [mk_meta_eq mem_Collect_eq]; |
|
274 |
|
275 val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) => |
|
276 (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep)); |
|
277 |
|
278 val newT_iso_inj_thms = typedefs |> map (fn (_, (_, {Abs_inject, Rep_inject, ...})) => |
|
279 (collect_simp Abs_inject RS iffD1, Rep_inject RS iffD1)); |
|
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. Rep_dt_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *) |
|
288 (* *) |
|
289 (* also generate characteristic equations for isomorphisms *) |
|
290 (* *) |
|
291 (* e.g. Rep_dt_i (cons h t) = In1 (Scons (Rep_dt_j h) (Rep_dt_i t)) *) |
|
292 (*---------------------------------------------------------------------*) |
|
293 |
|
294 fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) = |
|
295 let |
|
296 val argTs = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs; |
|
297 val T = nth recTs k; |
|
298 val rep_const = Const (nth all_rep_names k, T --> Univ_elT); |
|
299 val constr = Const (cname, argTs ---> T); |
|
300 |
|
301 fun process_arg ks' dt (i2, i2', ts, Ts) = |
|
302 let |
|
303 val T' = Old_Datatype_Aux.typ_of_dtyp descr' dt; |
|
304 val (Us, U) = strip_type T' |
|
305 in |
|
306 (case Old_Datatype_Aux.strip_dtyp dt of |
|
307 (_, Old_Datatype_Aux.DtRec j) => |
|
308 if member (op =) ks' j then |
|
309 (i2 + 1, i2' + 1, ts @ [mk_lim (Old_Datatype_Aux.app_bnds |
|
310 (Old_Datatype_Aux.mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us], |
|
311 Ts @ [Us ---> Univ_elT]) |
|
312 else |
|
313 (i2 + 1, i2', ts @ [mk_lim |
|
314 (Const (nth all_rep_names j, U --> Univ_elT) $ |
|
315 Old_Datatype_Aux.app_bnds |
|
316 (Old_Datatype_Aux.mk_Free "x" T' i2) (length Us)) Us], Ts) |
|
317 | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (Old_Datatype_Aux.mk_Free "x" T' i2)], Ts)) |
|
318 end; |
|
319 |
|
320 val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []); |
|
321 val xs = map (uncurry (Old_Datatype_Aux.mk_Free "x")) (argTs ~~ (1 upto (i2 - 1))); |
|
322 val ys = map (uncurry (Old_Datatype_Aux.mk_Free "y")) (Ts ~~ (1 upto (i2' - 1))); |
|
323 val f = fold_rev lambda (xs @ ys) (mk_univ_inj ts n i); |
|
324 |
|
325 val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []); |
|
326 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
327 (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) |
|
328 |
|
329 in (fs @ [f], eqns @ [eqn], i + 1) end; |
|
330 |
|
331 (* define isomorphisms for all mutually recursive datatypes in list ds *) |
|
332 |
|
333 fun make_iso_defs ds (thy, char_thms) = |
|
334 let |
|
335 val ks = map fst ds; |
|
336 val (_, (tname, _, _)) = hd ds; |
|
337 val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname); |
|
338 |
|
339 fun process_dt (k, (_, _, constrs)) (fs, eqns, isos) = |
|
340 let |
|
341 val (fs', eqns', _) = fold (make_iso_def k ks (length constrs)) constrs (fs, eqns, 1); |
|
342 val iso = (nth recTs k, nth all_rep_names k); |
|
343 in (fs', eqns', isos @ [iso]) end; |
|
344 |
|
345 val (fs, eqns, isos) = fold process_dt ds ([], [], []); |
|
346 val fTs = map fastype_of fs; |
|
347 val defs = |
|
348 map (fn (rec_name, (T, iso_name)) => |
|
349 (Binding.name (Thm.def_name (Long_Name.base_name iso_name)), |
|
350 Logic.mk_equals (Const (iso_name, T --> Univ_elT), |
|
351 list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); |
|
352 val (def_thms, thy') = |
|
353 (Global_Theory.add_defs false o map Thm.no_attributes) defs thy; |
|
354 |
|
355 (* prove characteristic equations *) |
|
356 |
|
357 val rewrites = def_thms @ map mk_meta_eq rec_rewrites; |
|
358 val char_thms' = |
|
359 map (fn eqn => Goal.prove_sorry_global thy' [] [] eqn |
|
360 (fn {context = ctxt, ...} => |
|
361 EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt [refl] 1])) eqns; |
|
362 |
|
363 in (thy', char_thms' @ char_thms) end; |
|
364 |
|
365 val (thy5, iso_char_thms) = |
|
366 fold_rev make_iso_defs (tl descr) (Sign.add_path big_name thy4, []); |
|
367 |
|
368 (* prove isomorphism properties *) |
|
369 |
|
370 fun mk_funs_inv thy thm = |
|
371 let |
|
372 val prop = Thm.prop_of thm; |
|
373 val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ |
|
374 (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop; |
|
375 val used = Term.add_tfree_names a []; |
|
376 |
|
377 fun mk_thm i = |
|
378 let |
|
379 val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t")); |
|
380 val f = Free ("f", Ts ---> U); |
|
381 in |
|
382 Goal.prove_sorry_global thy [] [] |
|
383 (Logic.mk_implies |
|
384 (HOLogic.mk_Trueprop (HOLogic.list_all |
|
385 (map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)), |
|
386 HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts |
|
387 (r $ (a $ Old_Datatype_Aux.app_bnds f i)), f)))) |
|
388 (fn {context = ctxt, ...} => |
|
389 EVERY [REPEAT_DETERM_N i (resolve_tac ctxt @{thms ext} 1), |
|
390 REPEAT (eresolve_tac ctxt [allE] 1), |
|
391 resolve_tac ctxt [thm] 1, |
|
392 assume_tac ctxt 1]) |
|
393 end |
|
394 in map (fn r => r RS subst) (thm :: map mk_thm arities) end; |
|
395 |
|
396 (* prove inj Rep_dt_i and Rep_dt_i x : rep_set_dt_i *) |
|
397 |
|
398 val fun_congs = |
|
399 map (fn T => make_elim (Thm.instantiate' [SOME (Thm.global_ctyp_of thy5 T)] [] fun_cong)) branchTs; |
|
400 |
|
401 fun prove_iso_thms ds (inj_thms, elem_thms) = |
|
402 let |
|
403 val (_, (tname, _, _)) = hd ds; |
|
404 val induct = #induct (the (Symtab.lookup dt_info tname)); |
|
405 |
|
406 fun mk_ind_concl (i, _) = |
|
407 let |
|
408 val T = nth recTs i; |
|
409 val Rep_t = Const (nth all_rep_names i, T --> Univ_elT); |
|
410 val rep_set_name = nth rep_set_names i; |
|
411 val concl1 = |
|
412 HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ |
|
413 HOLogic.mk_eq (Rep_t $ Old_Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $ |
|
414 HOLogic.mk_eq (Old_Datatype_Aux.mk_Free "x" T i, Bound 0)); |
|
415 val concl2 = Const (rep_set_name, UnivT') $ (Rep_t $ Old_Datatype_Aux.mk_Free "x" T i); |
|
416 in (concl1, concl2) end; |
|
417 |
|
418 val (ind_concl1, ind_concl2) = split_list (map mk_ind_concl ds); |
|
419 |
|
420 val rewrites = map mk_meta_eq iso_char_thms; |
|
421 val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms; |
|
422 |
|
423 val inj_thm = |
|
424 Goal.prove_sorry_global thy5 [] [] |
|
425 (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj ind_concl1)) |
|
426 (fn {context = ctxt, ...} => EVERY |
|
427 [(Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW |
|
428 Object_Logic.atomize_prems_tac ctxt) 1, |
|
429 REPEAT (EVERY |
|
430 [resolve_tac ctxt [allI] 1, resolve_tac ctxt [impI] 1, |
|
431 Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1, |
|
432 REPEAT (EVERY |
|
433 [hyp_subst_tac ctxt 1, |
|
434 rewrite_goals_tac ctxt rewrites, |
|
435 REPEAT (dresolve_tac ctxt [In0_inject, In1_inject] 1), |
|
436 (eresolve_tac ctxt [In0_not_In1 RS notE, In1_not_In0 RS notE] 1) |
|
437 ORELSE (EVERY |
|
438 [REPEAT (eresolve_tac ctxt (Scons_inject :: |
|
439 map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1), |
|
440 REPEAT (cong_tac ctxt 1), resolve_tac ctxt [refl] 1, |
|
441 REPEAT (assume_tac ctxt 1 ORELSE (EVERY |
|
442 [REPEAT (resolve_tac ctxt @{thms ext} 1), |
|
443 REPEAT (eresolve_tac ctxt (mp :: allE :: |
|
444 map make_elim (Suml_inject :: Sumr_inject :: |
|
445 Lim_inject :: inj_thms') @ fun_congs) 1), |
|
446 assume_tac ctxt 1]))])])])]); |
|
447 |
|
448 val inj_thms'' = map (fn r => r RS datatype_injI) (Old_Datatype_Aux.split_conj_thm inj_thm); |
|
449 |
|
450 val elem_thm = |
|
451 Goal.prove_sorry_global thy5 [] [] |
|
452 (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj ind_concl2)) |
|
453 (fn {context = ctxt, ...} => |
|
454 EVERY [ |
|
455 (Old_Datatype_Aux.ind_tac ctxt induct [] THEN_ALL_NEW |
|
456 Object_Logic.atomize_prems_tac ctxt) 1, |
|
457 rewrite_goals_tac ctxt rewrites, |
|
458 REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW |
|
459 ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac ctxt elem_thms)) 1)]); |
|
460 |
|
461 in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end; |
|
462 |
|
463 val (iso_inj_thms_unfolded, iso_elem_thms) = |
|
464 fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms); |
|
465 val iso_inj_thms = |
|
466 map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded; |
|
467 |
|
468 (* prove rep_set_dt_i x --> x : range Rep_dt_i *) |
|
469 |
|
470 fun mk_iso_t (((set_name, iso_name), i), T) = |
|
471 let val isoT = T --> Univ_elT in |
|
472 HOLogic.imp $ |
|
473 (Const (set_name, UnivT') $ Old_Datatype_Aux.mk_Free "x" Univ_elT i) $ |
|
474 (if i < length newTs then @{term True} |
|
475 else HOLogic.mk_mem (Old_Datatype_Aux.mk_Free "x" Univ_elT i, |
|
476 Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $ |
|
477 Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T))) |
|
478 end; |
|
479 |
|
480 val iso_t = HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj (map mk_iso_t |
|
481 (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs))); |
|
482 |
|
483 (* all the theorems are proved by one single simultaneous induction *) |
|
484 |
|
485 val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq})) iso_inj_thms_unfolded; |
|
486 |
|
487 val iso_thms = |
|
488 if length descr = 1 then [] |
|
489 else |
|
490 drop (length newTs) (Old_Datatype_Aux.split_conj_thm |
|
491 (Goal.prove_sorry_global thy5 [] [] iso_t (fn {context = ctxt, ...} => EVERY |
|
492 [(Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW |
|
493 Object_Logic.atomize_prems_tac ctxt) 1, |
|
494 REPEAT (resolve_tac ctxt [TrueI] 1), |
|
495 rewrite_goals_tac ctxt (mk_meta_eq @{thm choice_eq} :: |
|
496 Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs), |
|
497 rewrite_goals_tac ctxt (map Thm.symmetric range_eqs), |
|
498 REPEAT (EVERY |
|
499 [REPEAT (eresolve_tac ctxt ([rangeE, @{thm ex1_implies_ex} RS exE] @ |
|
500 maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1), |
|
501 TRY (hyp_subst_tac ctxt 1), |
|
502 resolve_tac ctxt [sym RS range_eqI] 1, |
|
503 resolve_tac ctxt iso_char_thms 1])]))); |
|
504 |
|
505 val Abs_inverse_thms' = |
|
506 map #1 newT_iso_axms @ |
|
507 map2 (fn r_inj => fn r => @{thm f_the_inv_into_f} OF [r_inj, r RS mp]) |
|
508 iso_inj_thms_unfolded iso_thms; |
|
509 |
|
510 val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms'; |
|
511 |
|
512 (******************* freeness theorems for constructors *******************) |
|
513 |
|
514 val _ = Old_Datatype_Aux.message config "Proving freeness of constructors ..."; |
|
515 |
|
516 (* prove theorem Rep_i (Constr_j ...) = Inj_j ... *) |
|
517 |
|
518 fun prove_constr_rep_thm eqn = |
|
519 let |
|
520 val inj_thms = map fst newT_iso_inj_thms; |
|
521 val rewrites = @{thm o_def} :: constr_defs @ map (mk_meta_eq o #2) newT_iso_axms; |
|
522 in |
|
523 Goal.prove_sorry_global thy5 [] [] eqn |
|
524 (fn {context = ctxt, ...} => EVERY |
|
525 [resolve_tac ctxt inj_thms 1, |
|
526 rewrite_goals_tac ctxt rewrites, |
|
527 resolve_tac ctxt [refl] 3, |
|
528 resolve_tac ctxt rep_intrs 2, |
|
529 REPEAT (resolve_tac ctxt iso_elem_thms 1)]) |
|
530 end; |
|
531 |
|
532 (*--------------------------------------------------------------*) |
|
533 (* constr_rep_thms and rep_congs are used to prove distinctness *) |
|
534 (* of constructors. *) |
|
535 (*--------------------------------------------------------------*) |
|
536 |
|
537 val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns; |
|
538 |
|
539 val dist_rewrites = |
|
540 map (fn (rep_thms, dist_lemma) => |
|
541 dist_lemma :: (rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) |
|
542 (constr_rep_thms ~~ dist_lemmas); |
|
543 |
|
544 fun prove_distinct_thms dist_rewrites' = |
|
545 let |
|
546 fun prove [] = [] |
|
547 | prove (t :: ts) = |
|
548 let |
|
549 val dist_thm = Goal.prove_sorry_global thy5 [] [] t (fn {context = ctxt, ...} => |
|
550 EVERY [simp_tac (put_simpset HOL_ss ctxt addsimps dist_rewrites') 1]) |
|
551 in dist_thm :: Drule.zero_var_indexes (dist_thm RS not_sym) :: prove ts end; |
|
552 in prove end; |
|
553 |
|
554 val distinct_thms = |
|
555 map2 (prove_distinct_thms) dist_rewrites (Old_Datatype_Prop.make_distincts descr); |
|
556 |
|
557 (* prove injectivity of constructors *) |
|
558 |
|
559 fun prove_constr_inj_thm rep_thms t = |
|
560 let |
|
561 val inj_thms = Scons_inject :: |
|
562 map make_elim |
|
563 (iso_inj_thms @ |
|
564 [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, |
|
565 Lim_inject, Suml_inject, Sumr_inject]) |
|
566 in |
|
567 Goal.prove_sorry_global thy5 [] [] t |
|
568 (fn {context = ctxt, ...} => EVERY |
|
569 [resolve_tac ctxt [iffI] 1, |
|
570 REPEAT (eresolve_tac ctxt [conjE] 2), hyp_subst_tac ctxt 2, |
|
571 resolve_tac ctxt [refl] 2, |
|
572 dresolve_tac ctxt rep_congs 1, |
|
573 dresolve_tac ctxt @{thms box_equals} 1, |
|
574 REPEAT (resolve_tac ctxt rep_thms 1), |
|
575 REPEAT (eresolve_tac ctxt inj_thms 1), |
|
576 REPEAT (ares_tac ctxt [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1), |
|
577 REPEAT (eresolve_tac ctxt (make_elim fun_cong :: inj_thms) 1), |
|
578 assume_tac ctxt 1]))]) |
|
579 end; |
|
580 |
|
581 val constr_inject = |
|
582 map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts) |
|
583 (Old_Datatype_Prop.make_injs descr ~~ constr_rep_thms); |
|
584 |
|
585 val ((constr_inject', distinct_thms'), thy6) = |
|
586 thy5 |
|
587 |> Sign.parent_path |
|
588 |> Old_Datatype_Aux.store_thmss "inject" new_type_names constr_inject |
|
589 ||>> Old_Datatype_Aux.store_thmss "distinct" new_type_names distinct_thms; |
|
590 |
|
591 (*************************** induction theorem ****************************) |
|
592 |
|
593 val _ = Old_Datatype_Aux.message config "Proving induction rule for datatypes ..."; |
|
594 |
|
595 val Rep_inverse_thms = |
|
596 map (fn (_, iso, _) => iso RS subst) newT_iso_axms @ |
|
597 map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded; |
|
598 val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded; |
|
599 |
|
600 fun mk_indrule_lemma (i, _) T = |
|
601 let |
|
602 val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $ Old_Datatype_Aux.mk_Free "x" T i; |
|
603 val Abs_t = |
|
604 if i < length newTs then |
|
605 Const (#Abs_name (#1 (#2 (nth typedefs i))), Univ_elT --> T) |
|
606 else |
|
607 Const (@{const_name the_inv_into}, |
|
608 [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $ |
|
609 HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT); |
|
610 val prem = |
|
611 HOLogic.imp $ |
|
612 (Const (nth rep_set_names i, UnivT') $ Rep_t) $ |
|
613 (Old_Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t)); |
|
614 val concl = |
|
615 Old_Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ |
|
616 Old_Datatype_Aux.mk_Free "x" T i; |
|
617 in (prem, concl) end; |
|
618 |
|
619 val (indrule_lemma_prems, indrule_lemma_concls) = |
|
620 split_list (map2 mk_indrule_lemma descr' recTs); |
|
621 |
|
622 val indrule_lemma = |
|
623 Goal.prove_sorry_global thy6 [] [] |
|
624 (Logic.mk_implies |
|
625 (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_prems), |
|
626 HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls))) |
|
627 (fn {context = ctxt, ...} => |
|
628 EVERY |
|
629 [REPEAT (eresolve_tac ctxt [conjE] 1), |
|
630 REPEAT (EVERY |
|
631 [TRY (resolve_tac ctxt [conjI] 1), resolve_tac ctxt Rep_inverse_thms 1, |
|
632 eresolve_tac ctxt [mp] 1, resolve_tac ctxt iso_elem_thms 1])]); |
|
633 |
|
634 val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma))); |
|
635 val frees = |
|
636 if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] |
|
637 else map (Free o apfst fst o dest_Var) Ps; |
|
638 |
|
639 val dt_induct_prop = Old_Datatype_Prop.make_ind descr; |
|
640 val dt_induct = |
|
641 Goal.prove_sorry_global thy6 [] |
|
642 (Logic.strip_imp_prems dt_induct_prop) |
|
643 (Logic.strip_imp_concl dt_induct_prop) |
|
644 (fn {context = ctxt, prems, ...} => |
|
645 let |
|
646 val indrule_lemma' = |
|
647 infer_instantiate ctxt |
|
648 (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma; |
|
649 in |
|
650 EVERY |
|
651 [resolve_tac ctxt [indrule_lemma'] 1, |
|
652 (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW |
|
653 Object_Logic.atomize_prems_tac ctxt) 1, |
|
654 EVERY (map (fn (prem, r) => (EVERY |
|
655 [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1), |
|
656 simp_tac (put_simpset HOL_basic_ss ctxt |
|
657 addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1, |
|
658 DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)])) |
|
659 (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))] |
|
660 end); |
|
661 |
|
662 val ([(_, [dt_induct'])], thy7) = |
|
663 thy6 |
|
664 |> Global_Theory.note_thmss "" |
|
665 [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]), |
|
666 [([dt_induct], [])])]; |
|
667 in |
|
668 ((constr_inject', distinct_thms', dt_induct'), thy7) |
|
669 end; |
|
670 |
|
671 |
|
672 |
|
673 (** datatype definition **) |
|
674 |
|
675 (* specifications *) |
|
676 |
22 |
677 type spec_cmd = |
23 type spec_cmd = |
678 (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list; |
24 (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list; |
679 |
|
680 local |
|
681 |
25 |
682 fun parse_spec ctxt ((b, args, mx), constrs) = |
26 fun parse_spec ctxt ((b, args, mx), constrs) = |
683 ((b, map (apsnd (Typedecl.read_constraint ctxt)) args, mx), |
27 ((b, map (apsnd (Typedecl.read_constraint ctxt)) args, mx), |
684 constrs |> map (fn (c, Ts, mx') => (c, map (Syntax.parse_typ ctxt) Ts, mx'))); |
28 constrs |> map (fn (c, Ts, mx') => (c, map (Syntax.parse_typ ctxt) Ts, mx'))); |
685 |
29 |