src/HOL/BNF/Tools/bnf_gfp_tactics.ML

   val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
   val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
     thm -> thm -> tactic
+  val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
     thm list -> thm list -> tactic
   val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     thm list -> thm list -> thm list list -> tactic

   val mk_set_incl_hset_tac: thm -> thm -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   val mk_set_natural_tac: thm -> thm -> tactic
   val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
     thm list list -> thm list list -> tactic
-  val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
   val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
     cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
     thm list list -> thm list list -> thm -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_unique_mor_tac: thm list -> thm -> tactic

   atac) 1;
 
 fun mk_mor_incl_tac mor_def map_id's =
   (stac mor_def THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))
-    map_id's THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
-  map_id's) 1;
+   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
 
 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   let
     fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
     fun mor_tac ((mor_image, morE), map_comp_id) =

     fun coalg_tac (i, ((passive_sets, active_sets), def)) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
         hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_casesN n i), rtac CollectI,
         EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
-          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])
+          etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
           passive_sets),
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
           rtac conjI,
           rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp,

       CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
         (if i = i'
         then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
           rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
           rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
-          rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
+          rtac (trans OF [@{thm image_id} RS fun_cong, 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_eqD, etac conjE,
           hyp_subst_tac, dtac (isNode_def RS iffD1),

 fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
   {context = ctxt, prems = _} =
   unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
     rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
     EVERY' (map (fn thm =>
-      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
-    rtac sym, rtac @{thm id_apply}] 1;
+      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
+    rtac sym, rtac id_apply] 1;
 
 fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
   unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
     rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
     REPEAT_DETERM_N m o rtac refl,

   end;
 
 fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
-      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
+      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
         atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
         etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
         rtac exI, rtac conjI, etac conjI, atac,
         CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],

         EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
           etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
           EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
       (1 upto n) set_hsets set_hset_hsetss)] 1;
 
-fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets =
+fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
   EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
     EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
 
 fun mk_map_id_tac maps unfold_unique unfold_dtor =

       coinduct_tac] @
       maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
         set_hset_hsetss) =>
         [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
          rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
-         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
+         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
          rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
          EVERY' (maps (fn set_hset =>
-           [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
+           [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
            REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
          CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
            EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
              etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural,

         rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
         rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
         rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
     (pick_cols ~~ hset_defs)] 1;
 
-fun mk_wit_tac n dtor_ctors set_simp wit coind_wits {context = ctxt, prems = _} =
+fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
-    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
     K (unfold_thms_tac ctxt dtor_ctors),
     REPEAT_DETERM_N n o etac UnE,
     REPEAT_DETERM o
       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
             K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN

           rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
         @{thms fst_conv snd_conv}];
     val only_if_tac =
       EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
-          EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+        CONJ_WRAP' (fn (dtor_set, passive_set_natural) =>
+          EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
             rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
               (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},