389 if get_STEPS lthy > 7 |
389 if get_STEPS lthy > 7 |
390 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
390 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
391 (Local_Theory.restore lthy_tmp) |
391 (Local_Theory.restore lthy_tmp) |
392 else raise TEST lthy4 |
392 else raise TEST lthy4 |
393 |
393 |
394 val size_eqvt = |
394 val raw_size_eqvt = |
395 if get_STEPS lthy > 8 |
395 if get_STEPS lthy > 8 |
396 then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
396 then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
397 (Local_Theory.restore lthy_tmp) |
397 (Local_Theory.restore lthy_tmp) |
|
398 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
|
399 |> map (fn thm => thm RS @{thm sym}) |
398 else raise TEST lthy4 |
400 else raise TEST lthy4 |
399 |
401 |
400 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
402 val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
401 |
403 |
402 val (alpha_eqvt, lthy6) = |
404 val (alpha_eqvt, lthy6) = |
499 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
501 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
500 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
502 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
501 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
503 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
502 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
504 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
503 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
505 ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp) |
504 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt) |
506 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
|
507 ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms) |
|
508 ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms) |
505 |
509 |
506 val _ = |
510 val _ = |
507 if get_STEPS lthy > 17 |
511 if get_STEPS lthy > 17 |
508 then true else raise TEST lthy8' |
512 then true else raise TEST lthy8' |
509 |
513 |