careful with op = in n2m (actually by Dmitriy Traytel)
authorblanchet
Thu Sep 18 16:47:40 2014 +0200 (2014-09-18)
changeset 583757b92932ffea5
parent 58374 1b4d31b7bd10
child 58376 c9d3074f83b3
careful with op = in n2m (actually by Dmitriy Traytel)
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	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -182,12 +182,13 @@
     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 +    val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     1.9 +    val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
    1.10  
    1.11      val rel_xtor_co_induct_thm =
    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 +          rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    1.16          lthy;
    1.17  
    1.18      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
    1.19 @@ -209,7 +210,8 @@
    1.20            in
    1.21              cterm_instantiate_pos cts rel_xtor_co_induct_thm
    1.22              |> singleton (Proof_Context.export names_lthy lthy)
    1.23 -            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
    1.24 +            |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
    1.25 +                fp_or_nesting_rel_eqs)
    1.26              |> funpow n (fn thm => thm RS spec)
    1.27              |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
    1.28              |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
    1.29 @@ -224,7 +226,8 @@
    1.30              val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
    1.31            in
    1.32              cterm_instantiate_pos cts rel_xtor_co_induct_thm
    1.33 -            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @ rel_eqs)
    1.34 +            |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
    1.35 +                fp_or_nesting_rel_eqs)
    1.36              |> funpow (2 * n) (fn thm => thm RS spec)
    1.37              |> Conv.fconv_rule (Object_Logic.atomize lthy)
    1.38              |> funpow n (fn thm => thm RS mp)
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Thu Sep 18 16:47:40 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Thu Sep 18 16:47:40 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 -> thm list -> {prems: thm list, context: Proof.context} -> tactic
     2.8 +    thm list -> 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,11 +20,13 @@
    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 nesting_rel_eqs
    2.17 -  {context = ctxt, prems = raw_C_IHs} =
    2.18 +fun mk_rel_xtor_co_induct_tactic fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0
    2.19 +  nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} =
    2.20    let
    2.21 -    val co_inducts = map (unfold_thms ctxt
    2.22 -      (vimage2p_unfolds @ @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs)) co_inducts0;
    2.23 +    val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0;
    2.24 +    val nesting_rel_monos = map (fn thm => rotate_prems ~1 (thm RS @{thm predicate2D}))
    2.25 +      (@{thms prod.rel_mono sum.rel_mono} @ nesting_rel_monos0);
    2.26 +    val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0;
    2.27      val unfolds = map (fn def =>
    2.28        unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
    2.29      val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
    2.30 @@ -41,7 +43,9 @@
    2.31      HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI})
    2.32        (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
    2.33           REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
    2.34 -           rtac @{thm order_refl}, atac, resolve_tac co_inducts])))
    2.35 +           SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac @{thm order_refl},
    2.36 +           atac, resolve_tac co_inducts,
    2.37 +           resolve_tac C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac nesting_rel_monos)])))
    2.38      co_inducts)
    2.39    end;
    2.40