267 in |
267 in |
268 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
268 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
269 end |
269 end |
270 *} |
270 *} |
271 |
271 |
272 ML {* val restricted_nominal=ref 0 *} |
|
273 ML {* val cheat_alpha_eqvt = ref true *} |
272 ML {* val cheat_alpha_eqvt = ref true *} |
274 ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *) |
273 ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *) |
275 ML {* val cheat_fv_rsp = ref true *} |
274 ML {* val cheat_fv_rsp = ref true *} |
276 ML {* val cheat_const_rsp = ref true *} |
275 ML {* val cheat_const_rsp = ref true *} |
277 |
276 |
378 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
377 val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; |
379 val thy = Local_Theory.exit_global lthy12c; |
378 val thy = Local_Theory.exit_global lthy12c; |
380 val perm_names = map (fn x => "permute_" ^ x) qty_names |
379 val perm_names = map (fn x => "permute_" ^ x) qty_names |
381 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
380 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
382 val lthy13 = Theory_Target.init NONE thy'; |
381 val lthy13 = Theory_Target.init NONE thy'; |
383 in |
|
384 if !restricted_nominal = 0 then |
|
385 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy13) |
|
386 else |
|
387 let |
|
388 val q_name = space_implode "_" qty_names; |
382 val q_name = space_implode "_" qty_names; |
389 val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct)); |
383 val q_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy13, induct)); |
390 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
384 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
391 val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def; |
385 val q_perm = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy14, th))) raw_perm_def; |
392 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
386 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
406 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
400 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
407 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
401 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
408 in |
402 in |
409 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
403 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
410 end |
404 end |
411 end |
|
412 *} |
405 *} |
413 |
406 |
414 ML {* |
407 ML {* |
415 (* parsing the datatypes and declaring *) |
408 (* parsing the datatypes and declaring *) |
416 (* constructors in the local theory *) |
409 (* constructors in the local theory *) |