equal
deleted
inserted
replaced
444 |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps qfv_supp_thms)) |
444 |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps qfv_supp_thms)) |
445 |> map (simplify (put_simpset HOL_basic_ss lthyC |
445 |> map (simplify (put_simpset HOL_basic_ss lthyC |
446 addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
446 addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) |
447 |
447 |
448 (* filters the theorems 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 val qfv_names = map (fst o dest_Const) qfvs |
|
450 fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Const (lhs, _) $ _)) = |
|
451 member (op=) qfv_names lhs |
450 | is_qfv_thm _ = false |
452 | is_qfv_thm _ = false |
451 |
453 |
452 val qsupp_constrs = qfv_defs |
454 val qsupp_constrs = qfv_defs |
453 |> map (simplify (put_simpset HOL_basic_ss lthyC |
455 |> map (simplify (put_simpset HOL_basic_ss lthyC |
454 addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |
456 addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms))) |