1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jul 01 16:26:14 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jul 01 17:01:28 2014 +0200
     1.3 @@ -28,7 +28,9 @@
     1.4      tactic
     1.5    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
     1.6      thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
     1.7 -    thm list -> thm list -> tactic
     1.8 +    thm list -> thm list -> thm list -> tactic
     1.9 +  val mk_rel_induct0_tac: Proof.context -> thm -> thm list -> cterm list -> thm list ->
    1.10 +    thm list list -> thm list -> thm list -> thm list -> thm list -> tactic
    1.11    val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.12    val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
    1.13    val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
    1.14 @@ -210,7 +212,7 @@
    1.15        selsss));
    1.16  
    1.17  fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
    1.18 -  dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses =
    1.19 +  dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
    1.20    rtac dtor_rel_coinduct 1 THEN
    1.21    EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
    1.22      fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
    1.23 @@ -222,14 +224,29 @@
    1.24        Local_Defs.unfold_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
    1.25          @ simp_thms') THEN
    1.26        Local_Defs.unfold_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
    1.27 -        abs_inject :: ctor_defs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def rel_sum_simps
    1.28 -        rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject
    1.29 -        prod.inject}) THEN
    1.30 +        abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
    1.31 +        rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
    1.32 +        sum.inject prod.inject}) THEN
    1.33        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
    1.34          (rtac refl ORELSE' atac))))
    1.35      cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
    1.36        abs_inverses);
    1.37  
    1.38 +fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects
    1.39 +    rel_pre_list_defs Abs_inverses nesting_rel_eqs =
    1.40 +  rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs =>
    1.41 +      fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
    1.42 +        HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
    1.43 +          (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
    1.44 +            THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
    1.45 +        unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    1.46 +          @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
    1.47 +        TRYALL (hyp_subst_tac ctxt) THEN
    1.48 +        unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    1.49 +          Inr_Inl_False  sum.inject prod.inject}) THEN
    1.50 +        TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
    1.51 +    cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
    1.52 +
    1.53  fun mk_sel_map_tac ctxt ct exhaust discs maps sels =
    1.54    TRYALL Goal.conjunction_tac THEN
    1.55      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW