avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
authorblanchet
Wed Sep 17 16:20:13 2014 +0200 (2014-09-17)
changeset 583593782c7b0d1cc
parent 58358 cdce4471d590
child 58360 dee1fd1cc631
avoid 'subst_tac' when possible (it is suspected of not helping 'HOL-Proofs')
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 12:09:33 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Sep 17 16:20:13 2014 +0200
     1.3 @@ -837,7 +837,8 @@
     1.4        rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
     1.5      fun rel_OO_Grp_tac ctxt =
     1.6        (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
     1.7 -       subst_tac ctxt NONE [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
     1.8 +       (if has_live_phantoms then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt)
     1.9 +         [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
    1.10         SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
    1.11           type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
    1.12           type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Sep 17 12:09:33 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Sep 17 16:20:13 2014 +0200
     2.3 @@ -68,6 +68,11 @@
     2.4  val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
     2.5  val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
     2.6  
     2.7 +fun is_def_looping def =
     2.8 +  (case Thm.prop_of def of
     2.9 +    Const (@{const_name Pure.eq}, _) $ lhs $ rhs => Term.exists_subterm (curry (op =) lhs) rhs
    2.10 +  | _ => false);
    2.11 +
    2.12  fun hhf_concl_conv cv ctxt ct =
    2.13    (case Thm.term_of ct of
    2.14      Const (@{const_name Pure.all}, _) $ Abs _ =>
    2.15 @@ -145,7 +150,8 @@
    2.16        case_unit_Unity} @ sumprod_thms_map;
    2.17  
    2.18  fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
    2.19 -  HEADGOAL (subst_tac ctxt NONE [ctr_def]) THEN
    2.20 +  HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
    2.21 +    else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
    2.22    unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    2.23      pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
    2.24  
    2.25 @@ -195,7 +201,10 @@
    2.26  fun mk_induct_tac ctxt nn ns mss kkss ctr_defs ctor_induct' fp_abs_inverses abs_inverses set_maps
    2.27      pre_set_defss =
    2.28    let val n = Integer.sum ns in
    2.29 -    EVERY (map (fn th => HEADGOAL (subst_asm_tac ctxt NONE [th])) ctr_defs) THEN
    2.30 +    (if exists is_def_looping ctr_defs then
    2.31 +       EVERY (map (fn def => HEADGOAL (subst_asm_tac ctxt NONE [def])) ctr_defs)
    2.32 +     else
    2.33 +       unfold_thms_tac ctxt ctr_defs) THEN
    2.34      HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
    2.35      EVERY (map4 (EVERY oooo map3 o
    2.36          mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)