1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
     1.3 @@ -130,8 +130,8 @@
     1.4      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
     1.5        REPEAT_DETERM o hyp_subst_tac ctxt) THEN
     1.6      unfold_thms_tac ctxt maps THEN
     1.7 -    unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
     1.8 -      handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
     1.9 +    unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
    1.10 +      handle THM _ => thm RS eqTrueI) discs) THEN
    1.11      ALLGOALS (rtac refl ORELSE' rtac TrueI);
    1.12  
    1.13  fun solve_prem_prem_tac ctxt =
    1.14 @@ -219,8 +219,8 @@
    1.15        hyp_subst_tac ctxt) THEN
    1.16    unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
    1.17      True_implies_equals conj_imp_eq_imp_imp} @
    1.18 -    map (fn thm => iffD2 OF [@{thm eq_False}, thm]) (distincts @ rel_distincts) @
    1.19 -    map (fn thm => thm RS @{thm eqTrueI}) rel_injects) THEN
    1.20 +    map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
    1.21 +    map (fn thm => thm RS eqTrueI) rel_injects) THEN
    1.22    TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
    1.23      REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
    1.24  
    1.25 @@ -234,7 +234,7 @@
    1.26          arg_cong2}) RS iffD1)) THEN'
    1.27          atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
    1.28          REPEAT_DETERM o etac conjE))) 1 THEN
    1.29 -      unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
    1.30 +      unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels
    1.31          @ simp_thms') THEN
    1.32        unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
    1.33          abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
    1.34 @@ -264,7 +264,7 @@
    1.35    TRYALL Goal.conjunction_tac THEN
    1.36      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.37        REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.38 -    unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
    1.39 +    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
    1.40        @{thms not_True_eq_False not_False_eq_True}) THEN
    1.41      TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
    1.42      unfold_thms_tac ctxt (maps @ sels) THEN
    1.43 @@ -274,7 +274,7 @@
    1.44    TRYALL Goal.conjunction_tac THEN
    1.45      ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.46        REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.47 -    unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
    1.48 +    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
    1.49        @{thms not_True_eq_False not_False_eq_True}) THEN
    1.50      TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
    1.51      unfold_thms_tac ctxt (sels @ sets) THEN
    1.52 @@ -289,7 +289,7 @@
    1.53    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
    1.54      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
    1.55    unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
    1.56 -    SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
    1.57 +    SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
    1.58    ALLGOALS (rtac refl ORELSE' etac FalseE);
    1.59  
    1.60  end;

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 07 16:06:46 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 07 16:06:46 2014 +0200
     2.3 @@ -639,7 +639,7 @@
     2.4        let
     2.5          val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
     2.6          val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
     2.7 -      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS @{thm eqTrueI} end;
     2.8 +      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
     2.9      val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
    2.10        imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
    2.11    in

     3.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Jul 07 16:06:46 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Jul 07 16:06:46 2014 +0200
     3.3 @@ -123,6 +123,8 @@
     3.4    val mk_ordLeq_csum: int -> int -> thm -> thm
     3.5    val mk_UnIN: int -> int -> thm
     3.6  
     3.7 +  val eqTrueI: thm
     3.8 +  val eqFalseI: thm
     3.9    val prod_injectD: thm
    3.10    val prod_injectI: thm
    3.11    val ctrans: thm
    3.12 @@ -518,6 +520,8 @@
    3.13  fun mk_sym thm = thm RS sym;
    3.14  
    3.15  (*TODO: antiquote heavily used theorems once*)
    3.16 +val eqTrueI = @{thm iffD2[OF eq_True]};
    3.17 +val eqFalseI =  @{thm iffD2[OF eq_False]};
    3.18  val prod_injectD = @{thm iffD1[OF prod.inject]};
    3.19  val prod_injectI = @{thm iffD2[OF prod.inject]};
    3.20  val ctrans = @{thm ordLeq_transitive};