# HG changeset patch # User blanchet # Date 1473322597 -7200 # Node ID 24c4fa81f81c71e15eb9ccfcb1cf91faa4f51fae # Parent ca8b737b08cf7645c73dc8ef466d5c66010853a8 tuning diff -r ca8b737b08cf -r 24c4fa81f81c src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 08 00:43:21 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 08 10:16:37 2016 +0200 @@ -306,7 +306,7 @@ (fn {context = ctxt, prems = _} => mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |> Thm.close_derivation) - (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt); + (map2 (curry mk_Trueprop_eq) sets sets_alt); fun map_cong0_tac ctxt = mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer) diff -r ca8b737b08cf -r 24c4fa81f81c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 08 00:43:21 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 08 10:16:37 2016 +0200 @@ -2303,14 +2303,6 @@ register_hint ()) end); - val abss = map #abs absT_infos; - val reps = map #rep absT_infos; - val absTs = map #absT absT_infos; - val repTs = map #repT absT_infos; - val abs_injects = map #abs_inject absT_infos; - val abs_inverses = map #abs_inverse absT_infos; - val type_definitions = map #type_definition absT_infos; - val time = time lthy; val timer = time (Timer.startRealTimer ()); @@ -2328,6 +2320,7 @@ val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs; + val liveness = liveness_of_fp_bnf num_As any_fp_bnf; val live = live_of_bnf any_fp_bnf; val _ = if live = 0 andalso exists (not o Binding.is_empty) (map_bs @ rel_bs @ pred_bs) then @@ -2335,14 +2328,21 @@ else (); - val Bs = - @{map 3} (fn alive => fn A as TFree (_, S) => fn B => - if alive then resort_tfree_or_tvar S B else A) - (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0; + val Bs = @{map 3} (fn alive => fn A as TFree (_, S) => fn B => + if alive then resort_tfree_or_tvar S B else A) + liveness As Bs0; val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); val live_AsBs = filter (op <>) (As ~~ Bs); + val abss = map #abs absT_infos; + val reps = map #rep absT_infos; + val absTs = map #absT absT_infos; + val repTs = map #repT absT_infos; + val abs_injects = map #abs_inject absT_infos; + val abs_inverses = map #abs_inverse absT_infos; + val type_definitions = map #type_definition absT_infos; + val ctors = map (mk_ctor As) ctors0; val dtors = map (mk_dtor As) dtors0; @@ -2454,10 +2454,8 @@ fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy); val maps0 = map map_of_bnf fp_bnfs; - val ABs = As ~~ Bs - val liveness = map (op <>) ABs; val f_names = variant_names num_As "f"; - val fs = map2 (curry Free) f_names (map (op -->) ABs); + val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs)); val live_gs = AList.find (op =) (fs ~~ liveness) true; val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; @@ -2474,7 +2472,7 @@ val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps; - val ABfs = ABs ~~ fs; + val ABfs = (As ~~ Bs) ~~ fs; fun mk_rec_arg_arg (x as Free (_, T)) = let val U = B_ify_T T in @@ -2607,11 +2605,10 @@ else let fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); + val maps0 = map map_of_bnf fp_bnfs; - val ABs = As ~~ Bs - val liveness = map (op <>) ABs; val f_names = variant_names num_As "f"; - val fs = map2 (curry Free) f_names (map (op -->) ABs); + val fs = map2 (curry Free) f_names (map (op -->) (As ~~ Bs)); val live_fs = AList.find (op =) (fs ~~ liveness) true; val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0; @@ -2628,7 +2625,7 @@ val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs; - val ABgs = ABs ~~ fs; + val ABfs = (As ~~ Bs) ~~ fs; fun mk_map_o_corec_arg corec_argB_T g = let @@ -2636,7 +2633,7 @@ val U = range_type corec_argB_T; in if T = U then g - else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U), g) + else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABfs) (T, U), g) end; fun mk_map_o_corec_rhs corecx = diff -r ca8b737b08cf -r 24c4fa81f81c src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Sep 08 00:43:21 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Sep 08 10:16:37 2016 +0200 @@ -13,7 +13,6 @@ val substT: typ -> typ -> term -> term val freeze_types: Proof.context -> (indexname * sort) list -> typ list -> typ list val dummify_atomic_types: term -> term - val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term val define_const: bool -> binding -> int -> string -> term -> local_theory -> (term * thm) * local_theory @@ -213,9 +212,6 @@ val dummify_atomic_types = Term.map_types (Term.map_atyps (K Term.dummyT)); -fun enforce_type ctxt get_T T t = - Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t; - fun mk_internal internal ctxt f = if internal andalso not (Config.get ctxt bnf_internals) then f else I fun mk_fp_binding fp_b pre = Binding.map_name (K pre) fp_b diff -r ca8b737b08cf -r 24c4fa81f81c src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 08 00:43:21 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 08 10:16:37 2016 +0200 @@ -36,6 +36,8 @@ val snd_const: typ -> term val Id_const: typ -> term + val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term + val mk_Ball: term -> term -> term val mk_Bex: term -> term -> term val mk_Card_order: term -> term @@ -221,6 +223,9 @@ (** Operators **) +fun enforce_type ctxt get_T T t = + Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t; + fun mk_converse R = let val RT = dest_relT (fastype_of R);