made tactic more robust w.r.t. dead variables
authortraytel
Mon Sep 08 09:52:06 2014 +0200 (2014-09-08)
changeset 582039003cc8ac94d
parent 58202 be1d10595b7b
child 58204 83a8570b44bc
made tactic more robust w.r.t. dead variables
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sun Sep 07 17:51:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Sep 08 09:52:06 2014 +0200
     1.3 @@ -182,12 +182,14 @@
     1.4      val castAs = map2 (curry HOLogic.mk_comp) absAs fp_repAs;
     1.5      val castBs = map2 (curry HOLogic.mk_comp) absBs fp_repBs;
     1.6  
     1.7 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     1.8 +
     1.9      val rel_xtor_co_induct_thm =
    1.10 -      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys xtors
    1.11 -        xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
    1.12 +      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.13 +        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    1.14 +          rel_monos rel_eqs)
    1.15          lthy;
    1.16  
    1.17 -    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    1.18      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
    1.19  
    1.20      val xtor_co_induct_thm =
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Sun Sep 07 17:51:32 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Sep 08 09:52:06 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  signature BNF_FP_N2M_TACTICS =
     2.5  sig
     2.6    val mk_rel_xtor_co_induct_tactic: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
     2.7 -    thm list -> {prems: thm list, context: Proof.context} -> tactic
     2.8 +    thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic
     2.9  end;
    2.10  
    2.11  structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
    2.12 @@ -20,10 +20,10 @@
    2.13  
    2.14  val vimage2p_unfolds = o_apply :: @{thms vimage2p_def};
    2.15  
    2.16 -fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos
    2.17 +fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs
    2.18    {context = ctxt, prems = raw_C_IHs} =
    2.19    let
    2.20 -    val co_inducts = map (unfold_thms ctxt vimage2p_unfolds) co_inducts0;
    2.21 +    val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0;
    2.22      val unfolds = map (fn def =>
    2.23        unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
    2.24      val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;