201 val (_, ty) = dest_Const bn_fun |
201 val (_, ty) = dest_Const bn_fun |
202 val (ty_name, _) = dest_Type (domain_type ty) |
202 val (ty_name, _) = dest_Type (domain_type ty) |
203 val dt_index = find_index (fn x => x = ty_name) dt_names |
203 val dt_index = find_index (fn x => x = ty_name) dt_names |
204 val (cnstr_head, cnstr_args) = strip_comb cnstr |
204 val (cnstr_head, cnstr_args) = strip_comb cnstr |
205 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
205 val rhs_elements = strip_bn_fun lthy cnstr_args rhs |
206 val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements |
|
207 in |
206 in |
208 (dt_index, (bn_fun, (cnstr_head, included))) |
207 (dt_index, (bn_fun, (cnstr_head, rhs_elements))) |
209 end |
208 end |
210 fun order dts i ts = |
209 fun order dts i ts = |
211 let |
210 let |
212 val dt = nth dts i |
211 val dt = nth dts i |
213 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
212 val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) |
257 |
254 |
258 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
255 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
259 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 |
260 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
257 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
261 |
258 |
262 val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
259 val (raw_dt_full_names, lthy1) = |
263 |
260 add_datatype_wrapper raw_dt_names raw_dts lthy |
264 in |
261 in |
265 (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
262 (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
266 end |
263 end |
267 *} |
264 *} |
268 |
265 |
269 ML {* |
266 ML {* |
270 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
267 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
271 let |
268 if null raw_bn_funs |
272 val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs |
269 then ([], [], [], [], lthy) |
273 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
270 else |
274 |
271 let |
275 val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) |
272 val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs |
276 val {fs, simps, inducts, ...} = info; |
273 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
277 |
274 |
278 val raw_bn_induct = (the inducts) |
275 val (info, lthy2) = prove_termination (Local_Theory.restore lthy1) |
279 val raw_bn_eqs = the simps |
276 val {fs, simps, inducts, ...} = info; |
280 |
277 |
281 val raw_bn_info = |
278 val raw_bn_induct = (the inducts) |
282 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
279 val raw_bn_eqs = the simps |
283 |
280 |
284 in |
281 val raw_bn_info = |
285 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3) |
282 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
286 end |
283 in |
|
284 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
|
285 end |
287 *} |
286 *} |
288 |
287 |
289 |
288 |
290 lemma equivp_hack: "equivp x" |
289 lemma equivp_hack: "equivp x" |
291 sorry |
290 sorry |
320 |
319 |
321 ML {* |
320 ML {* |
322 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
321 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
323 let |
322 let |
324 (* definition of the raw datatypes *) |
323 (* definition of the raw datatypes *) |
|
324 |
325 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
325 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
326 if get_STEPS lthy > 1 |
326 if get_STEPS lthy > 0 |
327 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
327 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
328 else raise TEST lthy |
328 else raise TEST lthy |
329 |
329 |
330 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
330 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
331 val {descr, sorts, ...} = dtinfo |
331 val {descr, sorts, ...} = dtinfo |
339 val rel_dtinfos = List.take (dtinfos, (length dts)); |
339 val rel_dtinfos = List.take (dtinfos, (length dts)); |
340 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
340 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
341 val induct_thm = #induct dtinfo; |
341 val induct_thm = #induct dtinfo; |
342 val exhaust_thms = map #exhaust dtinfos; |
342 val exhaust_thms = map #exhaust dtinfos; |
343 |
343 |
344 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = |
|
345 if get_STEPS lthy0 > 1 |
|
346 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 |
|
347 else raise TEST lthy0 |
|
348 |
|
349 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
350 val bns = raw_bn_funs ~~ bn_nos; |
|
351 |
|
352 (* definitions of raw permutations *) |
344 (* definitions of raw permutations *) |
353 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
345 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
354 if get_STEPS lthy1 > 2 |
346 if get_STEPS lthy0 > 1 |
355 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
347 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 |
356 else raise TEST lthy1 |
348 else raise TEST lthy0 |
357 |
349 |
358 (* noting the raw permutations as eqvt theorems *) |
350 (* noting the raw permutations as eqvt theorems *) |
359 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
351 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
360 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2 |
352 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2 |
361 |
353 |
363 val thy_name = Context.theory_name thy |
355 val thy_name = Context.theory_name thy |
364 |
356 |
365 (* definition of raw fv_functions *) |
357 (* definition of raw fv_functions *) |
366 val lthy3 = Theory_Target.init NONE thy; |
358 val lthy3 = Theory_Target.init NONE thy; |
367 |
359 |
368 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) = |
360 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
369 if get_STEPS lthy2 > 3 |
361 if get_STEPS lthy3 > 2 |
370 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 |
362 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
371 else raise TEST lthy3 |
363 else raise TEST lthy3 |
|
364 |
|
365 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
|
366 val bns = raw_bn_funs ~~ bn_nos; |
|
367 |
|
368 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
|
369 if get_STEPS lthy3a > 3 |
|
370 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a |
|
371 else raise TEST lthy3a |
372 |
372 |
373 (* definition of raw alphas *) |
373 (* definition of raw alphas *) |
374 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
374 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
375 if get_STEPS lthy > 4 |
375 if get_STEPS lthy3b > 4 |
376 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a |
376 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
377 else raise TEST lthy3a |
377 else raise TEST lthy3b |
378 |
378 |
379 (* definition of alpha-distinct lemmas *) |
379 (* definition of alpha-distinct lemmas *) |
380 val (alpha_distincts, alpha_bn_distincts) = |
380 val (alpha_distincts, alpha_bn_distincts) = |
381 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
381 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
382 |
382 |
391 val bn_eqvt = |
391 val bn_eqvt = |
392 if get_STEPS lthy > 6 |
392 if get_STEPS lthy > 6 |
393 then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
393 then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
394 else raise TEST lthy4 |
394 else raise TEST lthy4 |
395 |
395 |
|
396 (* noting the bn_eqvt lemmas in a temprorary theory *) |
396 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
397 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
397 val (_, lthy_tmp) = Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4 |
398 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
398 |
399 |
399 val fv_eqvt = |
400 val fv_eqvt = |
400 if get_STEPS lthy > 7 |
401 if get_STEPS lthy > 7 |
401 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
402 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
402 else raise TEST lthy4 |
403 else raise TEST lthy4 |
403 |
404 |
404 val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp |
405 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
405 |
|
406 |
|
407 |
406 |
408 val (alpha_eqvt, _) = |
407 val (alpha_eqvt, _) = |
409 if get_STEPS lthy > 8 |
408 if get_STEPS lthy > 8 |
410 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
409 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
411 else raise TEST lthy4 |
410 else raise TEST lthy4 |
412 |
411 |
413 (* |
|
414 val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) |
412 val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) |
415 val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) |
413 val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) |
416 val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) |
414 val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) |
417 *) |
|
418 |
415 |
419 val _ = |
416 val _ = |
420 if get_STEPS lthy > 9 |
417 if get_STEPS lthy > 9 |
421 then true else raise TEST lthy4 |
418 then true else raise TEST lthy4 |
422 |
419 |