src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML

 open BNF_Tactics
 open BNF_Util
 open BNF_FP
 open BNF_GFP_Util
 
-val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};
 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym;
-val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]};
+val list_inject_iffD1 = @{thm list.inject[THEN iffD1]};
 val nat_induct = @{thm nat_induct};
 val o_apply_trans_sym = o_apply RS trans RS sym;
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
 val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
   @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
-val set_mp = @{thm set_mp};
-val set_rev_mp = @{thm set_rev_mp};
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
-val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
-val subst_id = @{thm subst[of _ _ "%x. x"]};
 val sum_case_weak_cong = @{thm sum_case_weak_cong};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 
 fun mk_coalg_set_tac coalg_def =
-  dtac (coalg_def RS subst_id) 1 THEN
+  dtac (coalg_def RS iffD1) 1 THEN
   REPEAT_DETERM (etac conjE 1) THEN
   EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN
   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
 
 fun mk_mor_elim_tac mor_def =

       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
         dtac (rel_O_Gr RS equalityD1 RS set_mp),
         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
-        REPEAT_DETERM o dtac Pair_eq_subst_id,
+        REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE,
         hyp_subst_tac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
         rtac bexI, rtac conjI, rtac trans, rtac map_comp,
         REPEAT_DETERM_N m o stac @{thm id_o},

       rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
       etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1
   end;
 
 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses =
-  EVERY' [stac bis_rel, dtac (bis_rel RS subst_id),
+  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
       rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_converse) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},

         rtac rel_converse,
         REPEAT_DETERM o etac allE,
         rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1;
 
 fun mk_bis_O_tac m bis_rel rel_congs rel_Os =
-  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id),
+  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_O) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]},
         rtac (rel_cong RS trans),
         REPEAT_DETERM_N m o rtac @{thm diag_Comp},
         REPEAT_DETERM_N (length rel_congs) o rtac refl,
         rtac rel_O,
         etac @{thm relcompE},
-        REPEAT_DETERM o dtac Pair_eq_subst_id,
+        REPEAT_DETERM o dtac Pair_eqD,
         etac conjE, hyp_subst_tac,
         REPEAT_DETERM o etac allE, rtac @{thm relcompI},
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1;
 
 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins

   EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI,
     REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2,
     rtac (mk_nth_conv n i)] 1;
 
 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O =
-  EVERY' [rtac (@{thm equiv_def} RS ssubst_id),
-
-    rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id),
+  EVERY' [rtac (@{thm equiv_def} RS iffD2),
+
+    rtac conjI, rtac (@{thm refl_on_def} RS iffD2),
     rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp,
     rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI},
 
-    rtac conjI, rtac (@{thm sym_def} RS ssubst_id),
+    rtac conjI, rtac (@{thm sym_def} RS iffD2),
     rtac allI, rtac allI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI},
 
-    rtac (@{thm trans_def} RS ssubst_id),
+    rtac (@{thm trans_def} RS iffD2),
     rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp,
     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
     etac @{thm relcompI}, atac] 1;
 
 fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =

       rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
       rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
       hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
-        [rtac (mk_UnIN n i), dtac (def RS subst_id),
+        [rtac (mk_UnIN n i), dtac (def RS iffD1),
         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
         CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
           rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order},
           rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs),

   end;
 
 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
   EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
     REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-    dtac Pair_eq_subst_id,
+    dtac Pair_eqD,
     etac conjE, hyp_subst_tac,
-    dtac (isNode_def RS subst_id),
+    dtac (isNode_def RS iffD1),
     REPEAT_DETERM o eresolve_tac [exE, conjE],
     rtac (equalityD2 RS set_mp),
     rtac (strT_def RS arg_cong RS trans),
     etac (arg_cong RS trans),
     fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,

           rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
           rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
           rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
         else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
-          dtac conjunct2, dtac Pair_eq_subst_id, etac conjE,
-          hyp_subst_tac, dtac (isNode_def RS subst_id),
+          dtac conjunct2, dtac Pair_eqD, etac conjE,
+          hyp_subst_tac, dtac (isNode_def RS iffD1),
           REPEAT_DETERM o eresolve_tac [exE, conjE],
           rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
       (ks ~~ (carT_defs ~~ isNode_defs));
     fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) =
       dtac (mk_conjunctN n i) THEN'

     EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
         EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
           dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
-          rtac (rv_Nil RS arg_cong RS ssubst_id),
-          rtac (mk_sum_casesN n i RS ssubst_id),
+          rtac (rv_Nil RS arg_cong RS iffD2),
+          rtac (mk_sum_casesN n i RS iffD2),
           CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
       (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
             (fn (i, (from_to_sbd, coalg_set)) =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-              rtac (rv_Cons RS arg_cong RS ssubst_id),
-              rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id),
+              rtac (rv_Cons RS arg_cong RS iffD2),
+              rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
               etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
               dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
               etac coalg_set, atac])
           (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
       ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1

               then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
                 dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
                 hyp_subst_tac,
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
                   (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                    dtac list_inject_subst_id THEN' etac conjE THEN'
+                    dtac list_inject_iffD1 THEN' etac conjE THEN'
                     (if k = i'
                     then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
                     else etac (mk_InN_not_InM i' k RS notE)))
                 (rev ks)]
               else etac (mk_InN_not_InM i'' i RS notE)))

               CONJ_WRAP' (fn i' => rtac impI THEN'
                 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
                 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
                 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k =>
                   REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
-                  dtac list_inject_subst_id THEN' etac conjE THEN'
+                  dtac list_inject_iffD1 THEN' etac conjE THEN'
                   (if k = i
                   then EVERY' [dtac (mk_InN_inject n i),
-                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                     atac, atac, hyp_subst_tac] THEN'
                     CONJ_WRAP' (fn i'' =>
                       EVERY' [rtac impI, dtac (sym RS trans),
                         rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
                         etac (from_to_sbd RS arg_cong),

         if n = 1 then K all_tac
         else (rtac (sum_case_weak_cong RS trans) THEN'
           rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
         rtac (map_comp_id RS trans), rtac (map_cong 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 ssubst, rtac @{thm Pair_eq}, rtac conjI,
+          DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
             rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac list_inject_subst_id, etac conjE,
+                dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
             rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,

             rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
             dtac asm_rl, dtac asm_rl, dtac asm_rl,
             dtac (Lev_Suc RS equalityD1 RS set_mp),
             CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' =>
               EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
-                dtac list_inject_subst_id, etac conjE,
+                dtac list_inject_iffD1, etac conjE,
                 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
-                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)),
+                  dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                   atac, atac, hyp_subst_tac, atac]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,

   EVERY' [rtac conjI,
     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
-  EVERY' [rtac ssubst_id, rtac mor_UNIV,
+  EVERY' [rtac iffD2, rtac mor_UNIV,
     CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) =>
       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans),
         rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
         rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
         rtac (o_apply RS trans RS sym), rtac map_cong,

 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
   let
     val n = length Rep_injects;
   in
-    EVERY' [rtac rev_mp, ftac (bis_def RS subst_id),
+    EVERY' [rtac rev_mp, ftac (bis_def RS iffD1),
       REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse,
       rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg,
       rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr},
       rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT,
       rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT,

       (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   end;
 
 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   mor_unique pick_cols hset_defs =
-  EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI,
+  EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
     REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
     rtac box_equals, rtac mor_unique,
     rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
     rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
     rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,