# HG changeset patch # User blanchet # Date 1459159547 -7200 # Node ID d229f9749507f01cdcab91248727d8a3d7ac6eca # Parent 5b2a7caa855b6c0354235619ce897653d2122b34 tuning diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Mar 28 12:05:47 2016 +0200 @@ -1161,7 +1161,7 @@ fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def = (trans OF [iffD2 OF [dtor_inject, eval_def RS meta_eq_to_obj_eq RS fun_cong], dtor_unfold_thm]) - |> unfold_thms ctxt [o_apply, eval_def RS Drule.symmetric_thm]; + |> unfold_thms ctxt [o_apply, eval_def RS symmetric_thm]; fun derive_eval_flat ctxt Y Z fpT ssig_T dead_ssig_map flat eval x dead_pre_map_comp0 dtor_unfold_unique ssig_map_id ssig_map_comp flat_pointful_natural eval_core_pointful_natural @@ -1360,8 +1360,8 @@ in unfold_thms ctxt @{thms atomize_imp} (((inject_refine' OF [extdd_o_VLeaf, extdd_o_VLeaf] RS iffD1) - OF [Drule.asm_rl, corecU_pointfree]) - OF [Drule.asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] + OF [asm_rl, corecU_pointfree]) + OF [asm_rl, trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [extdd_mor, corecU_pointfree RS extdd_mor]]) RS @{thm obj_distinct_prems} end; diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Mon Mar 28 12:05:47 2016 +0200 @@ -273,7 +273,7 @@ val var = Free (var_name, fpT); val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var); - val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust; + val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust; in Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} => HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200 @@ -47,15 +47,13 @@ end; fun instantiate_distrib thm ctxt t = - Drule.infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm; + infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm; -(* TODO (here and elsewhere): Use metaequality in goal instead and keep uninstianted version of - theorem? *) val mk_if_distrib_of = instantiate_distrib @{thm if_distrib}; val mk_case_sum_distrib_of = instantiate_distrib @{thm sum.case_distrib}; fun mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust cases = - let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in + let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in HEADGOAL (rtac ctxt exhaust') THEN REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' SELECT_GOAL (unfold_thms_tac ctxt cases THEN @@ -180,7 +178,7 @@ end; fun mk_last_disc_tac ctxt u exhaust discs' = - let val exhaust' = Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in + let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in HEADGOAL (rtac ctxt exhaust') THEN REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' simp_tac (ss_only (distinct Thm.eq_thm discs' @ @{thms simp_thms}) ctxt))) diff -r 5b2a7caa855b -r d229f9749507 src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Mon Mar 28 12:05:47 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML Mon Mar 28 12:05:47 2016 +0200 @@ -163,7 +163,7 @@ sctr_pointful_natural eval_sctr_pointful corecUU_def = unfold_thms_tac ctxt [corecUU_def] THEN HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN - unfold_thms_tac ctxt [corecUU_def RS Drule.symmetric_thm] THEN + unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN' mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural @@ -241,7 +241,7 @@ old_eval eval = HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext]) - OF [Drule.asm_rl, old_eval RS sym])) THEN + OF [asm_rl, old_eval RS sym])) THEN unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval, o_apply] THEN HEADGOAL (rtac ctxt refl); @@ -359,7 +359,7 @@ asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 :: cutSsig_def_pointful_natural :: flat_simps @ @{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN' - rtac ctxt (dead_pre_map_cong OF [Drule.asm_rl, refl]) THEN' + rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN' asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural :: eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) :: (flat_flat RS sym) ::