318 val induct_thm = #induct dtinfo; |
318 val induct_thm = #induct dtinfo; |
319 val exhaust_thms = map #exhaust dtinfos; |
319 val exhaust_thms = map #exhaust dtinfos; |
320 |
320 |
321 (* definitions of raw permutations *) |
321 (* definitions of raw permutations *) |
322 val _ = warning "Definition of raw permutations"; |
322 val _ = warning "Definition of raw permutations"; |
323 val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) = |
323 val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) = |
324 if get_STEPS lthy0 > 1 |
324 if get_STEPS lthy0 > 1 |
325 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 |
325 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0 |
326 else raise TEST lthy0 |
326 else raise TEST lthy0 |
327 |
327 |
328 (* noting the raw permutations as eqvt theorems *) |
328 (* noting the raw permutations as eqvt theorems *) |
329 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
329 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
330 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_defs) lthy2 |
330 val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2 |
331 |
331 |
332 val thy = Local_Theory.exit_global lthy2a; |
332 val thy = Local_Theory.exit_global lthy2a; |
333 val thy_name = Context.theory_name thy |
333 val thy_name = Context.theory_name thy |
334 |
334 |
335 (* definition of raw fv_functions *) |
335 (* definition of raw fv_functions *) |
369 |
369 |
370 (* proving equivariance lemmas for bns, fvs and alpha *) |
370 (* proving equivariance lemmas for bns, fvs and alpha *) |
371 val _ = warning "Proving equivariance"; |
371 val _ = warning "Proving equivariance"; |
372 val bn_eqvt = |
372 val bn_eqvt = |
373 if get_STEPS lthy > 6 |
373 if get_STEPS lthy > 6 |
374 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
374 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4 |
375 else raise TEST lthy4 |
375 else raise TEST lthy4 |
376 |
376 |
377 (* noting the bn_eqvt lemmas in a temprorary theory *) |
377 (* noting the bn_eqvt lemmas in a temprorary theory *) |
378 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
378 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
379 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
379 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
380 |
380 |
381 val fv_eqvt = |
381 val fv_eqvt = |
382 if get_STEPS lthy > 7 |
382 if get_STEPS lthy > 7 |
383 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) |
383 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
384 (Local_Theory.restore lthy_tmp) |
384 (Local_Theory.restore lthy_tmp) |
385 else raise TEST lthy4 |
385 else raise TEST lthy4 |
386 |
386 |
387 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
387 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
388 |
388 |
421 val alpha_bn_imp_thms = |
421 val alpha_bn_imp_thms = |
422 if get_STEPS lthy > 13 |
422 if get_STEPS lthy > 13 |
423 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
423 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
424 else raise TEST lthy6 |
424 else raise TEST lthy6 |
425 |
425 |
|
426 (* auxiliary lemmas for respectfulness proofs *) |
|
427 (* HERE *) |
|
428 |
|
429 |
|
430 |
426 (* defining the quotient type *) |
431 (* defining the quotient type *) |
427 val _ = warning "Declaring the quotient types" |
432 val _ = warning "Declaring the quotient types" |
428 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
433 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
429 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
434 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
430 val qty_names = map Name.of_binding qty_binds; |
435 val qty_names = map Name.of_binding qty_binds; |
450 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
455 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
451 |
456 |
452 val qfv_bns_descr = |
457 val qfv_bns_descr = |
453 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
458 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
454 |
459 |
455 (* TODO: probably also needs alpha_bn *) |
460 val qalpha_bns_descr = |
456 val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = |
461 map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs alpha_bn_trms |
|
462 |
|
463 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
457 if get_STEPS lthy > 15 |
464 if get_STEPS lthy > 15 |
458 then |
465 then |
459 lthy7 |
466 lthy7 |
460 |> qconst_defs qtys qconstrs_descr |
467 |> qconst_defs qtys qconstrs_descr |
461 ||>> qconst_defs qtys qbns_descr |
468 ||>> qconst_defs qtys qbns_descr |
462 ||>> qconst_defs qtys qfvs_descr |
469 ||>> qconst_defs qtys qfvs_descr |
463 ||>> qconst_defs qtys qfv_bns_descr |
470 ||>> qconst_defs qtys qfv_bns_descr |
|
471 ||>> qconst_defs qtys qalpha_bns_descr |
464 else raise TEST lthy7 |
472 else raise TEST lthy7 |
465 |
473 |
466 val qconstrs = map #qconst qconstrs_info |
474 val qconstrs = map #qconst qconstrs_info |
467 val qbns = map #qconst qbns_info |
475 val qbns = map #qconst qbns_info |
468 val qfvs = map #qconst qfvs_info |
476 val qfvs = map #qconst qfvs_info |
469 val qfv_bns = map #qconst qfv_bns_info |
477 val qfv_bns = map #qconst qfv_bns_info |
470 |
478 val qalpha_bns = map #qconst qalpha_bns_info |
471 (* respectfulness proofs *) |
479 |
472 |
|
473 (* HERE *) |
480 (* HERE *) |
474 |
481 |
475 val (_, lthy8') = lthy8 |
482 val (_, lthy8') = lthy8 |
476 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
483 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
477 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
484 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
478 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
485 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
479 ||>> Local_Theory.note ((@{binding "perm_defs"}, []), raw_perm_defs) |
|
480 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
486 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
481 |
487 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
|
488 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
482 |
489 |
483 val _ = |
490 val _ = |
484 if get_STEPS lthy > 16 |
491 if get_STEPS lthy > 16 |
485 then true else raise TEST lthy8' |
492 then true else raise TEST lthy8' |
486 |
493 |
539 val _ = warning "Lifting permutations"; |
546 val _ = warning "Lifting permutations"; |
540 val thy = Local_Theory.exit_global lthy12c; |
547 val thy = Local_Theory.exit_global lthy12c; |
541 val perm_names = map (fn x => "permute_" ^ x) qty_names |
548 val perm_names = map (fn x => "permute_" ^ x) qty_names |
542 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
549 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
543 (* use Local_Theory.theory_result *) |
550 (* use Local_Theory.theory_result *) |
544 val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy; |
551 val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy; |
545 val lthy13 = Theory_Target.init NONE thy'; |
552 val lthy13 = Theory_Target.init NONE thy'; |
546 |
553 |
547 val q_name = space_implode "_" qty_names; |
554 val q_name = space_implode "_" qty_names; |
548 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
555 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
549 val _ = warning "Lifting induction"; |
556 val _ = warning "Lifting induction"; |
556 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
563 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
557 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
564 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
558 [Rule_Cases.name constr_names q_induct]) lthy13; |
565 [Rule_Cases.name constr_names q_induct]) lthy13; |
559 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
566 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
560 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
567 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
561 val q_perm = map (lift_thm qtys lthy14) raw_perm_defs; |
568 val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; |
562 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
569 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
563 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
570 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
564 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
571 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
565 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
572 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
566 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
573 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |