# HG changeset patch
# User blanchet
# Date 1398639270 -7200
# Node ID 644f0d4820a13efd37bbf598247467849f3672bf
# Parent  5b6f4655e2f2872a7e0debffbaba8eaf9ecd84c6
cleaner 'rel_inject' theorems

diff -r 5b6f4655e2f2 -r 644f0d4820a1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -1179,8 +1179,6 @@
               fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
                 mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
 
-              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
-
               fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
                 mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
                   cxIn cyIn;
@@ -1189,6 +1187,7 @@
                 flip_rels lthy live thm
                 RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
 
+              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
               val half_rel_distinct_thmss =
                 map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
               val other_half_rel_distinct_thmss =
diff -r 5b6f4655e2f2 -r 644f0d4820a1 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -42,7 +42,7 @@
   @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
       Union_Un_distrib image_iff o_apply map_prod_simp
       mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
-val sumprod_thms_rel = @{thms rel_prod_apply rel_sum_simps id_apply};
+val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
 
 fun hhf_concl_conv cv ctxt ct =
   (case Thm.term_of ct of
@@ -82,7 +82,7 @@
 fun mk_inject_tac ctxt ctr_def ctor_inject abs_inject =
   unfold_thms_tac ctxt [ctr_def] THEN
   HEADGOAL (rtac (ctor_inject RS ssubst)) THEN
-  unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN
+  unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject prod.inject conj_assoc}) THEN
   HEADGOAL (rtac refl);
 
 val rec_unfold_thms =
@@ -155,8 +155,7 @@
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: fp_abs_inverse :: abs_inverse :: dtor_ctor ::
     sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
   (atac ORELSE' REPEAT o etac conjE THEN'
-     full_simp_tac
-       (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
+     full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
      REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
      REPEAT o (resolve_tac [refl, conjI] ORELSE' atac));
 
diff -r 5b6f4655e2f2 -r 644f0d4820a1 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -288,7 +288,7 @@
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
         rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         etac @{thm relcompE},
-        REPEAT_DETERM o dtac Pair_eqD,
+        REPEAT_DETERM o dtac prod_injectD,
         etac conjE, hyp_subst_tac ctxt,
         REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
@@ -607,7 +607,7 @@
           rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
         rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
-          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
+          DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
             rtac equalityI, rtac subsetI, etac thin_rl, 
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
@@ -969,7 +969,7 @@
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]},
                 REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
-                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                 hyp_subst_tac ctxt,
                 dtac (in_Jrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
@@ -984,8 +984,8 @@
           rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
-            REPEAT_DETERM o
-              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+            REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
             hyp_subst_tac ctxt, dtac (in_Jrel RS iffD1),
             dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jrels),
           atac]]
diff -r 5b6f4655e2f2 -r 644f0d4820a1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -204,7 +204,7 @@
     (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac iffD2 THEN'
     rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
     REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
-    CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
+    CONJ_WRAP_GEN' (EVERY' [rtac prod_injectI, rtac conjI]) minH_tac in_congs) 1
   end;
 
 fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac relChainD, rtac allI, rtac allI, rtac impI,
@@ -679,7 +679,7 @@
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]},
                 REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
-                  @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                 hyp_subst_tac ctxt,
                 dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
                 TRY o
@@ -693,8 +693,8 @@
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
-            REPEAT_DETERM o
-              eresolve_tac (CollectE :: conjE :: @{thms case_prodE iffD1[OF Pair_eq, elim_format]}),
+            REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
+              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
             hyp_subst_tac ctxt,
             dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac])
           in_Irels),
diff -r 5b6f4655e2f2 -r 644f0d4820a1 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Sun Apr 27 19:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Apr 28 00:54:30 2014 +0200
@@ -123,8 +123,8 @@
   val mk_ordLeq_csum: int -> int -> thm -> thm
   val mk_UnIN: int -> int -> thm
 
-  val Pair_eqD: thm
-  val Pair_eqI: thm
+  val prod_injectD: thm
+  val prod_injectI: thm
   val ctrans: thm
   val id_apply: thm
   val meta_mp: thm
@@ -518,8 +518,8 @@
 fun mk_sym thm = thm RS sym;
 
 (*TODO: antiquote heavily used theorems once*)
-val Pair_eqD = @{thm iffD1[OF Pair_eq]};
-val Pair_eqI = @{thm iffD2[OF Pair_eq]};
+val prod_injectD = @{thm iffD1[OF prod.inject]};
+val prod_injectI = @{thm iffD2[OF prod.inject]};
 val ctrans = @{thm ordLeq_transitive};
 val id_apply = @{thm id_apply};
 val meta_mp = @{thm meta_mp};