equal
deleted
inserted
replaced
279 |
279 |
280 val alpha_eqvt = |
280 val alpha_eqvt = |
281 let |
281 let |
282 val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result |
282 val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result |
283 in |
283 in |
284 Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5 |
284 Nominal_Eqvt.raw_equivariance lthy5 (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros |
285 end |
285 end |
286 |
286 |
287 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
287 val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt |
288 |
288 |
289 val _ = trace_msg (K "Proving equivalence of alpha...") |
289 val _ = trace_msg (K "Proving equivalence of alpha...") |
443 (* postprocessing of eq and fv theorems *) |
443 (* postprocessing of eq and fv theorems *) |
444 val qeq_iffs' = qeq_iffs |
444 val qeq_iffs' = qeq_iffs |
445 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
445 |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms)) |
446 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
446 |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
447 |
447 |
448 (* filters the theormes that are of the form "qfv = supp" *) |
448 (* filters the theorems that are of the form "qfv = supp" *) |
449 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs |
449 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs |
450 | is_qfv_thm _ = false |
450 | is_qfv_thm _ = false |
451 |
451 |
452 val qsupp_constrs = qfv_defs |
452 val qsupp_constrs = qfv_defs |
453 |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
453 |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
740 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
740 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
741 "declaration of nominal datatypes" |
741 "declaration of nominal datatypes" |
742 (main_parser >> nominal_datatype2_cmd) |
742 (main_parser >> nominal_datatype2_cmd) |
743 *} |
743 *} |
744 |
744 |
745 |
745 end |
746 end |
|
747 |
|
748 |
|
749 |
|