# HG changeset patch
# User desharna
# Date 1404742006 -7200
# Node ID 5e83df79eaa0d4bd3f723f496c2ce4af42a32e1b
# Parent  9afc832252a32f5114a8ef39ee105221141d9f77
refactor some tactics

diff -r 9afc832252a3 -r 5e83df79eaa0 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -130,8 +130,8 @@
     ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
       REPEAT_DETERM o hyp_subst_tac ctxt) THEN
     unfold_thms_tac ctxt maps THEN
-    unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
-      handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
+    unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
+      handle THM _ => thm RS eqTrueI) discs) THEN
     ALLGOALS (rtac refl ORELSE' rtac TrueI);
 
 fun solve_prem_prem_tac ctxt =
@@ -219,8 +219,8 @@
       hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
     True_implies_equals conj_imp_eq_imp_imp} @
-    map (fn thm => iffD2 OF [@{thm eq_False}, thm]) (distincts @ rel_distincts) @
-    map (fn thm => thm RS @{thm eqTrueI}) rel_injects) THEN
+    map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
+    map (fn thm => thm RS eqTrueI) rel_injects) THEN
   TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
     REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
 
@@ -234,7 +234,7 @@
         arg_cong2}) RS iffD1)) THEN'
         atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'
         REPEAT_DETERM o etac conjE))) 1 THEN
-      unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @ sels
+      unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels
         @ simp_thms') THEN
       unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
         abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
@@ -264,7 +264,7 @@
   TRYALL Goal.conjunction_tac THEN
     ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
       REPEAT_DETERM o hyp_subst_tac ctxt) THEN
-    unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
+    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
       @{thms not_True_eq_False not_False_eq_True}) THEN
     TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
     unfold_thms_tac ctxt (maps @ sels) THEN
@@ -274,7 +274,7 @@
   TRYALL Goal.conjunction_tac THEN
     ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
       REPEAT_DETERM o hyp_subst_tac ctxt) THEN
-    unfold_thms_tac ctxt ((discs RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
+    unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
       @{thms not_True_eq_False not_False_eq_True}) THEN
     TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
     unfold_thms_tac ctxt (sels @ sets) THEN
@@ -289,7 +289,7 @@
   ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
     REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
-    SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
+    SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
   ALLGOALS (rtac refl ORELSE' etac FalseE);
 
 end;
diff -r 9afc832252a3 -r 5e83df79eaa0 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -639,7 +639,7 @@
       let
         val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
         val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset});
-      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS @{thm eqTrueI} end;
+      in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS eqTrueI end;
     val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
       imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
   in
diff -r 9afc832252a3 -r 5e83df79eaa0 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Jul 07 16:06:46 2014 +0200
@@ -123,6 +123,8 @@
   val mk_ordLeq_csum: int -> int -> thm -> thm
   val mk_UnIN: int -> int -> thm
 
+  val eqTrueI: thm
+  val eqFalseI: thm
   val prod_injectD: thm
   val prod_injectI: thm
   val ctrans: thm
@@ -518,6 +520,8 @@
 fun mk_sym thm = thm RS sym;
 
 (*TODO: antiquote heavily used theorems once*)
+val eqTrueI = @{thm iffD2[OF eq_True]};
+val eqFalseI =  @{thm iffD2[OF eq_False]};
 val prod_injectD = @{thm iffD1[OF prod.inject]};
 val prod_injectI = @{thm iffD2[OF prod.inject]};
 val ctrans = @{thm ordLeq_transitive};