202 val rhs_elements = strip_bn_fun rhs |
202 val rhs_elements = strip_bn_fun rhs |
203 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
203 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
204 in |
204 in |
205 (dt_index, (bn_fun, (cnstr_head, included))) |
205 (dt_index, (bn_fun, (cnstr_head, included))) |
206 end |
206 end |
207 fun aux2 eq = |
|
208 let |
|
209 val (lhs, rhs) = eq |
|
210 |> strip_qnt_body "all" |
|
211 |> HOLogic.dest_Trueprop |
|
212 |> HOLogic.dest_eq |
|
213 val (bn_fun, [cnstr]) = strip_comb lhs |
|
214 val (_, ty) = dest_Free bn_fun |
|
215 val (ty_name, _) = dest_Type (domain_type ty) |
|
216 val dt_index = find_index (fn x => x = ty_name) dt_names |
|
217 val (cnstr_head, cnstr_args) = strip_comb cnstr |
|
218 val rhs_elements = strip_bn_fun rhs |
|
219 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
|
220 in |
|
221 (bn_fun, dt_index, (cnstr_head, included)) |
|
222 end |
|
223 fun order dts i ts = |
207 fun order dts i ts = |
224 let |
208 let |
225 val dt = nth dts i |
209 val dt = nth dts i |
226 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
210 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
227 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
211 val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts |
233 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
217 val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered |
234 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
218 val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' |
235 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
219 val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered) |
236 |
220 |
237 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
221 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
238 val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) |
222 (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*) |
239 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
223 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
240 in |
224 in |
241 ordered' |
225 ordered' |
242 end |
226 end |
243 *} |
227 *} |
244 |
228 |
|
229 ML {* add_primrec_wrapper *} |
245 ML {* |
230 ML {* |
246 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
231 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
247 let |
232 let |
248 val thy = ProofContext.theory_of lthy |
233 val thy = ProofContext.theory_of lthy |
249 val thy_name = Context.theory_name thy |
234 val thy_name = Context.theory_name thy |
269 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
254 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
270 |
255 |
271 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
256 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
272 |
257 |
273 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
258 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
274 |
|
275 val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
259 val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
276 in |
260 |
277 lthy |
261 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
278 |> add_datatype_wrapper raw_dt_names raw_dts |
262 val ((raw_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
279 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
263 |
280 ||>> pair raw_bclauses |
264 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
281 ||>> pair raw_bns |
265 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
|
266 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
|
267 in |
|
268 (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2) |
282 end |
269 end |
283 *} |
270 *} |
284 |
271 |
285 lemma equivp_hack: "equivp x" |
272 lemma equivp_hack: "equivp x" |
286 sorry |
273 sorry |
386 |
373 |
387 ML {* |
374 ML {* |
388 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
375 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
389 let |
376 let |
390 (* definition of the raw datatype and raw bn-functions *) |
377 (* definition of the raw datatype and raw bn-functions *) |
391 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
378 val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) = |
392 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
379 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
393 else raise TEST lthy |
380 else raise TEST lthy |
394 |
381 |
395 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
382 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
396 val {descr, sorts, ...} = dtinfo; |
383 val {descr, sorts, ...} = dtinfo; |
411 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
398 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
412 if get_STEPS lthy > 2 |
399 if get_STEPS lthy > 2 |
413 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
400 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
414 else raise TEST lthy1 |
401 else raise TEST lthy1 |
415 |
402 |
416 (* definition of raw fv_functions *) |
|
417 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
|
418 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
|
419 val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns; |
|
420 |
|
421 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
403 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
422 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
404 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
423 val thy = Local_Theory.exit_global lthy2a; |
405 val thy = Local_Theory.exit_global lthy2a; |
424 val thy_name = Context.theory_name thy |
406 val thy_name = Context.theory_name thy |
425 |
407 |
|
408 (* definition of raw fv_functions *) |
426 val lthy3 = Theory_Target.init NONE thy; |
409 val lthy3 = Theory_Target.init NONE thy; |
427 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
410 val raw_bn_funs = map (fn (f, _, _) => f) raw_bns; |
428 |
411 |
429 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
|
430 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
|
431 |
|
432 val ((fv, fvbn), fv_def, lthy3a) = |
412 val ((fv, fvbn), fv_def, lthy3a) = |
433 if get_STEPS lthy > 3 |
413 if get_STEPS lthy > 3 |
434 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
414 then define_raw_fv descr sorts raw_bns raw_bclauses lthy3 |
435 else raise TEST lthy3 |
415 else raise TEST lthy3 |
436 |
416 |
437 |
417 |
438 (* definition of raw alphas *) |
418 (* definition of raw alphas *) |
439 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
419 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
440 if get_STEPS lthy > 4 |
420 if get_STEPS lthy > 4 |
441 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a |
421 then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a |
442 else raise TEST lthy3a |
422 else raise TEST lthy3a |
443 |
423 |
444 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
424 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
445 |
425 |
446 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
426 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |