364 val _ = warning "Definition of alphas"; |
364 val _ = warning "Definition of alphas"; |
365 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
365 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
366 if get_STEPS lthy3b > 4 |
366 if get_STEPS lthy3b > 4 |
367 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
367 then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b |
368 else raise TEST lthy3b |
368 else raise TEST lthy3b |
369 |
369 val alpha_tys = map (domain_type o fastype_of) alpha_trms |
|
370 |
370 (* definition of alpha-distinct lemmas *) |
371 (* definition of alpha-distinct lemmas *) |
371 val _ = warning "Distinct theorems"; |
372 val _ = warning "Distinct theorems"; |
372 val (alpha_distincts, alpha_bn_distincts) = |
373 val (alpha_distincts, alpha_bn_distincts) = |
373 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
374 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
374 |
375 |
394 if get_STEPS lthy > 7 |
395 if get_STEPS lthy > 7 |
395 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) |
396 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) |
396 (Local_Theory.restore lthy_tmp) |
397 (Local_Theory.restore lthy_tmp) |
397 else raise TEST lthy4 |
398 else raise TEST lthy4 |
398 |
399 |
399 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
400 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
400 |
401 |
401 val (alpha_eqvt, lthy_tmp'') = |
402 val (alpha_eqvt, lthy6) = |
402 if get_STEPS lthy > 8 |
403 if get_STEPS lthy > 8 |
403 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp' |
404 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
404 else raise TEST lthy4 |
405 else raise TEST lthy4 |
405 |
406 |
406 (* proving alpha equivalence *) |
407 (* proving alpha equivalence *) |
407 val _ = warning "Proving equivalence" |
408 val _ = warning "Proving equivalence" |
408 |
409 |
409 val alpha_refl_thms = |
410 val alpha_refl_thms = |
410 if get_STEPS lthy > 9 |
411 if get_STEPS lthy > 9 |
411 then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp'' |
412 then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy6 |
412 else raise TEST lthy4 |
413 else raise TEST lthy6 |
413 |
414 |
414 val alpha_sym_thms = |
415 val alpha_sym_thms = |
415 if get_STEPS lthy > 10 |
416 if get_STEPS lthy > 10 |
416 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' |
417 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy6 |
417 else raise TEST lthy4 |
418 else raise TEST lthy6 |
418 |
419 |
419 val alpha_trans_thms = |
420 val alpha_trans_thms = |
420 if get_STEPS lthy > 11 |
421 if get_STEPS lthy > 11 |
421 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
422 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
422 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
423 alpha_intros alpha_induct alpha_cases lthy6 |
423 else raise TEST lthy4 |
424 else raise TEST lthy6 |
424 |
425 |
425 val alpha_equivp_thms = |
426 val alpha_equivp_thms = |
426 if get_STEPS lthy > 12 |
427 if get_STEPS lthy > 12 |
427 then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy_tmp'' |
428 then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6 |
428 else raise TEST lthy4 |
429 else raise TEST lthy6 |
429 |
430 |
430 (* proving alpha implies alpha_bn *) |
431 (* proving alpha implies alpha_bn *) |
431 val _ = warning "Proving alpha implies bn" |
432 val _ = warning "Proving alpha implies bn" |
432 |
433 |
433 val alpha_bn_imp_thms = |
434 val alpha_bn_imp_thms = |
434 if get_STEPS lthy > 13 |
435 if get_STEPS lthy > 13 |
435 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy_tmp'' |
436 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
436 else raise TEST lthy4 |
437 else raise TEST lthy6 |
437 |
438 |
438 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
439 (* defining the quotient type *) |
439 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
440 val _ = warning "Declaring the quotient types" |
440 val _ = tracing ("alpha_refl\n" ^ |
441 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
441 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms)) |
442 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
442 val _ = tracing ("alpha_bn_imp\n" ^ |
|
443 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_bn_imp_thms)) |
|
444 val _ = tracing ("alpha_equivp\n" ^ |
|
445 cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_equivp_thms)) |
|
446 |
|
447 (* old stuff *) |
|
448 val _ = |
|
449 if get_STEPS lthy > 14 |
|
450 then true else raise TEST lthy4 |
|
451 |
|
452 val qty_binds = map (fn (_, b, _, _) => b) dts; |
|
453 val qty_names = map Name.of_binding qty_binds; |
443 val qty_names = map Name.of_binding qty_binds; |
454 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
444 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
455 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp_thms lthy4; |
445 |
|
446 val qty_args' = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms |
|
447 val qty_args = (qty_descr ~~ qty_args') ~~ alpha_equivp_thms |
|
448 |
|
449 val (qty_infos, lthy7) = |
|
450 if get_STEPS lthy > 14 |
|
451 then fold_map Quotient_Type.add_quotient_type qty_args lthy6 |
|
452 else raise TEST lthy6 |
|
453 |
|
454 val qtys = map #qtyp qty_infos |
|
455 |
|
456 val _ = |
|
457 if get_STEPS lthy > 15 |
|
458 then true else raise TEST lthy7 |
|
459 |
|
460 (* old stuff *) |
|
461 |
456 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
462 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
457 val raw_consts = |
463 val raw_consts = |
458 flat (map (fn (i, (_, _, l)) => |
464 flat (map (fn (i, (_, _, l)) => |
459 map (fn (cname, dts) => |
465 map (fn (cname, dts) => |
460 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
466 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |