src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 59049 0d1bfc982501
parent 58634 9f10d82e8188
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Nov 24 12:20:14 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Nov 24 15:50:10 2014 +0100
     1.3 @@ -185,9 +185,21 @@
     1.4      val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     1.5      val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
     1.6  
     1.7 +    val rel_xtor_co_inducts_inst =
     1.8 +      let
     1.9 +        val extract =
    1.10 +          case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
    1.11 +        val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
    1.12 +        val thetas = AList.group (op =)
    1.13 +          (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis));
    1.14 +      in
    1.15 +        map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
    1.16 +        mutual_cliques rel_xtor_co_inducts
    1.17 +      end
    1.18 +
    1.19      val xtor_rel_co_induct =
    1.20        mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.21 -        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    1.22 +        xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts_inst rel_defs
    1.23            rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    1.24          lthy;
    1.25