360 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
360 mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info |
361 |
361 |
362 (* definition of alpha_eq_iff lemmas *) |
362 (* definition of alpha_eq_iff lemmas *) |
363 (* they have a funny shape for the simplifier *) |
363 (* they have a funny shape for the simplifier *) |
364 val _ = warning "Eq-iff theorems"; |
364 val _ = warning "Eq-iff theorems"; |
365 val alpha_eq_iff = |
365 val (alpha_eq_iff_simps, alpha_eq_iff) = |
366 if get_STEPS lthy > 5 |
366 if get_STEPS lthy > 5 |
367 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
367 then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases |
368 else raise TEST lthy4 |
368 else raise TEST lthy4 |
369 |
369 |
370 (* proving equivariance lemmas for bns, fvs and alpha *) |
370 (* proving equivariance lemmas for bns, fvs and alpha *) |
424 else raise TEST lthy6 |
424 else raise TEST lthy6 |
425 |
425 |
426 (* auxiliary lemmas for respectfulness proofs *) |
426 (* auxiliary lemmas for respectfulness proofs *) |
427 (* HERE *) |
427 (* HERE *) |
428 |
428 |
429 |
429 val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns |
|
430 alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
|
431 val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test)) |
430 |
432 |
431 (* defining the quotient type *) |
433 (* defining the quotient type *) |
432 val _ = warning "Declaring the quotient types" |
434 val _ = warning "Declaring the quotient types" |
433 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
435 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
434 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
436 val qty_binds = map (fn (_, bind, _, _) => bind) dts |
479 |
481 |
480 (* HERE *) |
482 (* HERE *) |
481 |
483 |
482 val (_, lthy8') = lthy8 |
484 val (_, lthy8') = lthy8 |
483 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
485 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
484 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
486 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
|
487 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
485 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
488 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
486 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
489 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
487 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
490 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
488 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
491 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
489 |
492 |