Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: WHATSNEW   Sprache: SML

Original von: Isabelle©

(*  Title:      HOL/Tools/BNF/bnf_gfp_tactics.ML
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2012

Tactics for the codatatype construction.
*)


signature BNF_GFP_TACTICS =
sig
  val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic
  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
  val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
  val mk_bis_converse_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
  val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    thm list list -> tactic
  val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
  val mk_coalg_final_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list list ->
    thm list list -> tactic
  val mk_coalg_set_tac: Proof.context -> thm -> tactic
  val mk_coind_wit_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
  val mk_col_bd_tac: Proof.context -> int -> int -> cterm option list -> thm list -> thm list ->
    thm -> thm -> thm list list -> tactic
  val mk_col_natural_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    thm list list -> tactic
  val mk_congruent_str_final_tac: Proof.context -> int -> thm -> thm -> thm -> thm list -> tactic
  val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
  val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
  val mk_dtor_coinduct_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
  val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
    thm list -> tactic
  val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    thm -> thm -> thm list -> thm list -> thm list list -> tactic
  val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
  val mk_equiv_lsbis_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic
  val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic
  val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
    tactic
  val mk_incl_lsbis_tac: Proof.context -> int -> int -> thm -> tactic
  val mk_length_Lev'_tac: Proof.context -> thm -> tactic
  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
  val mk_map_comp0_tac: Proof.context -> thm list -> thm list -> thm -> tactic
  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
    thm list list -> thm list list -> thm list list list -> thm list -> tactic
  val mk_map_id0_tac: Proof.context -> thm list -> thm -> thm -> tactic
  val mk_map_tac: Proof.context -> int -> int -> thm -> thm -> thm -> thm -> tactic
  val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
  val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
  val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
    thm list -> thm list -> tactic
  val mk_mor_T_final_tac: Proof.context -> thm -> thm list -> thm list -> tactic
  val mk_mor_UNIV_tac: Proof.context -> thm list -> thm -> tactic
  val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
    thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
    thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
    thm list list -> thm list -> thm list -> tactic
  val mk_mor_comp_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> tactic
  val mk_mor_elim_tac: Proof.context -> thm -> tactic
  val mk_mor_col_tac: Proof.context -> int -> int -> cterm option list -> int -> thm list ->
    thm list -> thm list -> thm list list -> thm list list -> tactic
  val mk_mor_incl_tac: Proof.context -> thm -> thm list -> tactic
  val mk_mor_str_tac: Proof.context -> 'a list -> thm -> tactic
  val mk_mor_unfold_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    thm list -> thm list -> thm list -> tactic
  val mk_raw_coind_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm ->
    thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic
  val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
    thm list -> thm list -> tactic
  val mk_rel_coinduct_coind_tac: Proof.context -> bool -> int -> thm -> int list -> thm list ->
    thm list -> thm list -> thm list list -> thm list -> thm list -> thm list -> tactic
  val mk_rel_coinduct_ind_tac: Proof.context -> int -> int list -> thm list -> thm list list ->
    int -> thm -> tactic
  val mk_rv_last_tac: Proof.context -> ctyp option list -> cterm option list -> thm list ->
    thm list -> tactic
  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    thm list -> thm list list -> tactic
  val mk_set_bd_tac: Proof.context -> thm -> thm -> tactic
  val mk_set_Jset_incl_Jset_tac: Proof.context -> int -> thm -> int -> tactic
  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
    thm list -> thm list -> thm list list -> thm list list -> tactic
  val mk_set_incl_Jset_tac: Proof.context -> thm -> tactic
  val mk_set_ge_tac: Proof.context -> int  -> thm -> thm list -> tactic
  val mk_set_le_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic
  val mk_set_map0_tac: Proof.context -> thm -> tactic
  val mk_unfold_unique_mor_tac: Proof.context -> thm list -> thm -> thm -> thm list -> tactic
  val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
  val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
  val mk_le_rel_OO_tac: Proof.context -> thm -> thm list -> thm list -> tactic
end;

structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
struct

open BNF_Tactics
open BNF_Util
open BNF_FP_Util
open BNF_GFP_Util

val fst_convol_fun_cong_sym = @{thm fst_convol[simplified convol_def]} RS fun_cong RS sym;
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 ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
val snd_convol_fun_cong_sym = @{thm snd_convol[simplified convol_def]} RS fun_cong RS sym;
val sum_case_cong_weak = @{thm sum.case_cong_weak};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
val rev_bspec = Drule.rotate_prems 1 bspec;
val Un_cong = @{thm arg_cong2[of _ _ _ _ "(\)"]};
val converse_shift = @{thm converse_subset_swap} RS iffD1;

fun mk_coalg_set_tac ctxt coalg_def =
  dtac ctxt (coalg_def RS iffD1) 1 THEN
  REPEAT_DETERM (etac ctxt conjE 1) THEN
  EVERY' [dtac ctxt rev_bspec, assume_tac ctxt] 1 THEN
  REPEAT_DETERM (eresolve_tac ctxt [CollectE, conjE] 1) THEN assume_tac ctxt 1;

fun mk_mor_elim_tac ctxt mor_def =
  (dtac ctxt (mor_def RS iffD1) THEN'
  REPEAT o etac ctxt conjE THEN'
  TRY o rtac ctxt @{thm image_subsetI} THEN'
  etac ctxt bspec THEN'
  assume_tac ctxt) 1;

fun mk_mor_incl_tac ctxt mor_def map_ids =
  (rtac ctxt (mor_def RS iffD2) THEN'
  rtac ctxt conjI THEN'
  CONJ_WRAP' (K (EVERY' [rtac ctxt ballI, etac ctxt set_mp, etac ctxt (id_apply RS @{thm ssubst_mem})]))
    map_ids THEN'
  CONJ_WRAP' (fn thm =>
    (EVERY' [rtac ctxt ballI, rtac ctxt (thm RS trans), rtac ctxt sym, rtac ctxt (id_apply RS arg_cong)])) map_ids) 1;

fun mk_mor_comp_tac ctxt mor_def mor_images morEs map_comp_ids =
  let
    fun fbetw_tac image = EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS @{thm ssubst_mem}), etac ctxt image,
      etac ctxt image, assume_tac ctxt];
    fun mor_tac ((mor_image, morE), map_comp_id) =
      EVERY' [rtac ctxt ballI, stac ctxt o_apply, rtac ctxt trans, rtac ctxt (map_comp_id RS sym), rtac ctxt trans,
        etac ctxt (morE RS arg_cong), assume_tac ctxt, etac ctxt morE,
        etac ctxt mor_image, assume_tac ctxt];
  in
    (rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
    CONJ_WRAP' fbetw_tac mor_images THEN'
    CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
  end;

fun mk_mor_UNIV_tac ctxt morEs mor_def =
  let
    val n = length morEs;
    fun mor_tac morE = EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply, rtac ctxt trans, etac ctxt morE,
      rtac ctxt UNIV_I, rtac ctxt sym, rtac ctxt o_apply];
  in
    EVERY' [rtac ctxt iffI, CONJ_WRAP' mor_tac morEs,
    rtac ctxt (mor_def RS iffD2), rtac ctxt conjI, CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) morEs,
    CONJ_WRAP' (fn i =>
      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt ballI, etac ctxt @{thm comp_eq_dest}]) (1 upto n)] 1
  end;

fun mk_mor_str_tac ctxt ks mor_UNIV =
  (rtac ctxt (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac ctxt refl)) ks) 1;

fun mk_set_incl_Jset_tac ctxt rec_Suc =
  EVERY' (map (rtac ctxt) [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
    rec_Suc]) 1;

fun mk_set_Jset_incl_Jset_tac ctxt n rec_Suc i =
  EVERY' (map (rtac ctxt) [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2,
    rec_Suc, UnI2, mk_UnIN n i] @ [etac ctxt @{thm UN_I}, assume_tac ctxt]) 1;

fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs =
  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
    REPEAT_DETERM o rtac ctxt allI,
    CONJ_WRAP' (fn thm => EVERY'
      [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt @{thm empty_subsetI}]) rec_0s,
    REPEAT_DETERM o rtac ctxt allI,
    CONJ_WRAP' (fn rec_Suc => EVERY'
      [rtac ctxt ord_eq_le_trans, rtac ctxt rec_Suc,
        if m = 0 then K all_tac
        else (rtac ctxt @{thm Un_least} THEN' Goal.assume_rule_tac ctxt),
        CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
          (K (EVERY' [rtac ctxt @{thm UN_least}, REPEAT_DETERM o eresolve_tac ctxt [allE, conjE],
            rtac ctxt subset_trans, assume_tac ctxt, Goal.assume_rule_tac ctxt])) rec_0s])
      rec_Sucs] 1;

fun mk_Jset_minimal_tac ctxt n col_minimal =
  (CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm UN_least}, rtac ctxt rev_mp, rtac ctxt col_minimal,
    EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac ctxt impI,
    REPEAT_DETERM o eresolve_tac ctxt [allE, conjE], assume_tac ctxt])) (1 upto n)) 1

fun mk_mor_col_tac ctxt m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
  EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
    REPEAT_DETERM o rtac ctxt allI,
    CONJ_WRAP' (fn thm => EVERY' (map (rtac ctxt) [impI, thm RS trans, thm RS sym])) rec_0s,
    REPEAT_DETERM o rtac ctxt allI,
    CONJ_WRAP'
      (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
        EVERY' [rtac ctxt impI, rtac ctxt (rec_Suc RS trans), rtac ctxt (rec_Suc RS trans RS sym),
          if m = 0 then K all_tac
          else EVERY' [rtac ctxt Un_cong, rtac ctxt @{thm box_equals},
            rtac ctxt (nth passive_set_map0s (j - 1) RS sym),
            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt (morE RS arg_cong),
            assume_tac ctxt],
          CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
            (fn (i, (set_map0, coalg_set)) =>
              EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
                etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
                rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
                forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
                rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
                REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
            (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;

fun mk_bis_rel_tac ctxt m bis_def in_rels map_comp0s map_cong0s set_map0ss =
  let
    val n = length in_rels;
    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);

    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, dtac ctxt (mk_conjunctN n i),
        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt, etac ctxt bexE,
        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI),
        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt trans, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt map_cong0,
          REPEAT_DETERM_N m o rtac ctxt thm, REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
          assume_tac ctxt])
        @{thms fst_diag_id snd_diag_id},
        rtac ctxt CollectI,
        CONJ_WRAP' (fn (i, thm) =>
          if i <= m
          then EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt thm, rtac ctxt subset_trans,
            etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
            rtac ctxt @{thm case_prodI}, rtac ctxt refl]
          else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
        (1 upto (m + n) ~~ set_map0s)];

    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
      EVERY' [dtac ctxt (mk_conjunctN n i), rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
        etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
        dtac ctxt (in_rel RS @{thm iffD1}),
        REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
          @{thms CollectE Collect_case_prod_in_rel_leE}),
        rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
        REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
        REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
        assume_tac ctxt, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
        REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
        REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
        rtac ctxt trans, rtac ctxt map_cong0,
        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
        REPEAT_DETERM_N n o rtac ctxt refl,
        assume_tac ctxt, rtac ctxt CollectI,
        CONJ_WRAP' (fn (i, thm) =>
          if i <= m then rtac ctxt subset_UNIV
          else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
            rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt])
        (1 upto (m + n) ~~ set_map0s)];
  in
    EVERY' [rtac ctxt (bis_def RS trans),
      rtac ctxt iffI, etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_if_tac thms,
      etac ctxt conjE, etac ctxt conjI, CONJ_WRAP' mk_only_if_tac thms] 1
  end;

fun mk_bis_converse_tac ctxt m bis_rel rel_congs rel_converseps =
  EVERY' [rtac ctxt (bis_rel RS iffD2), dtac ctxt (bis_rel RS iffD1),
    REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
    CONJ_WRAP' (K (EVERY' [rtac ctxt converse_shift, etac ctxt subset_trans,
      rtac ctxt equalityD2, rtac ctxt @{thm converse_Times}])) rel_congs,
    CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
        rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
        REPEAT_DETERM_N m o rtac ctxt @{thm conversep_eq},
        REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm conversep_in_rel},
        rtac ctxt (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
        REPEAT_DETERM o etac ctxt allE,
        rtac ctxt @{thm conversepI}, etac ctxt mp, etac ctxt @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;

fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs =
  EVERY' [rtac ctxt (bis_rel RS iffD2), REPEAT_DETERM o dtac ctxt (bis_rel RS iffD1),
    REPEAT_DETERM o etac ctxt conjE, rtac ctxt conjI,
    CONJ_WRAP' (K (EVERY' [etac ctxt @{thm relcomp_subset_Sigma}, assume_tac ctxt])) rel_congs,
    CONJ_WRAP' (fn (rel_cong, le_rel_OO) =>
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
        rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
        REPEAT_DETERM_N m o rtac ctxt @{thm eq_OO},
        REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm relcompp_in_rel},
        rtac ctxt (le_rel_OO RS @{thm predicate2D}),
        etac ctxt @{thm relcompE},
        REPEAT_DETERM o dtac ctxt prod_injectD,
        etac ctxt conjE, hyp_subst_tac ctxt,
        REPEAT_DETERM o etac ctxt allE, rtac ctxt @{thm relcomppI},
        etac ctxt mp, assume_tac ctxt, etac ctxt mp, assume_tac ctxt]) (rel_congs ~~ le_rel_OOs)] 1;

fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
  unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
  EVERY' [rtac ctxt conjI,
    CONJ_WRAP' (fn thm => rtac ctxt (@{thm Gr_incl} RS iffD2) THEN' etac ctxt thm) mor_images,
    CONJ_WRAP' (fn (coalg_in, morE) =>
      EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt @{thm GrpI}, etac ctxt (morE RS trans),
        etac ctxt @{thm GrD1}, etac ctxt (@{thm GrD2} RS arg_cong), etac ctxt coalg_in, etac ctxt @{thm GrD1}])
    (coalg_ins ~~ morEs)] 1;

fun mk_bis_Union_tac ctxt bis_def in_monos =
  let
    val n = length in_monos;
    val ks = 1 upto n;
  in
    unfold_thms_tac ctxt [bis_def] THEN
    EVERY' [rtac ctxt conjI,
      CONJ_WRAP' (fn i =>
        EVERY' [rtac ctxt @{thm UN_least}, dtac ctxt bspec, assume_tac ctxt,
          dtac ctxt conjunct1, etac ctxt (mk_conjunctN n i)]) ks,
      CONJ_WRAP' (fn (i, in_mono) =>
        EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, etac ctxt @{thm UN_E},
          dtac ctxt bspec, assume_tac ctxt,
          dtac ctxt conjunct2, dtac ctxt (mk_conjunctN n i), etac ctxt allE, etac ctxt allE, dtac ctxt mp,
          assume_tac ctxt, etac ctxt bexE, rtac ctxt bexI, assume_tac ctxt, rtac ctxt in_mono,
          REPEAT_DETERM_N n o etac ctxt @{thm SUP_upper2[OF _ subset_refl]},
          assume_tac ctxt]) (ks ~~ in_monos)] 1
  end;

fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
  let
    val n = length lsbis_defs;
  in
    EVERY' [rtac ctxt (Thm.permute_prems 0 1 bis_cong), EVERY' (map (rtac ctxt) lsbis_defs),
      rtac ctxt bis_Union, rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, exE],
      hyp_subst_tac ctxt, etac ctxt bis_cong, EVERY' (map (rtac ctxt o mk_nth_conv n) (1 upto n))] 1
  end;

fun mk_incl_lsbis_tac ctxt n i lsbis_def =
  EVERY' [rtac ctxt @{thm xt1(3)}, rtac ctxt lsbis_def, rtac ctxt @{thm SUP_upper2}, rtac ctxt CollectI,
    REPEAT_DETERM_N n o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,
    rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;

fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
  EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2),

    rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2),
    rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp,
    rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},

    rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2),
    rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp,
    rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI},

    rtac ctxt (@{thm trans_def} RS iffD2),
    rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp,
    rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
    etac ctxt @{thm relcompI}, assume_tac ctxt] 1;

fun mk_coalgT_tac ctxt m defs strT_defs set_map0ss =
  let
    val n = length strT_defs;
    val ks = 1 upto n;
    fun coalg_tac (i, (active_sets, def)) =
      EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
        hyp_subst_tac ctxt, rtac ctxt (def RS trans RS @{thm ssubst_mem}), etac ctxt (arg_cong RS trans),
        rtac ctxt (mk_sum_caseN n i), rtac ctxt CollectI,
        REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
        CONJ_WRAP' (fn (i, thm) => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
          rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt exI, rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
          rtac ctxt conjI,
          rtac ctxt conjI, etac ctxt @{thm empty_Shift}, dtac ctxt set_rev_mp,
            etac ctxt equalityD1, etac ctxt CollectD,
          rtac ctxt ballI,
            CONJ_WRAP' (fn i => EVERY' [rtac ctxt ballI, etac ctxt CollectE, dtac ctxt @{thm ShiftD},
              dtac ctxt bspec, etac ctxt thin_rl, assume_tac ctxt, dtac ctxt (mk_conjunctN n i),
              dtac ctxt bspec, rtac ctxt CollectI, etac ctxt @{thm set_mp[OF equalityD1[OF Succ_Shift]]},
              REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
              rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
              rtac ctxt (@{thm append_Cons} RS sym RS arg_cong RS trans), assume_tac ctxt,
              CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
                rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
                rtac ctxt (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
          dtac ctxt bspec, assume_tac ctxt, dtac ctxt (mk_conjunctN n i), dtac ctxt bspec,
          etac ctxt @{thm set_mp[OF equalityD1]}, assume_tac ctxt,
          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], rtac ctxt exI,
          rtac ctxt conjI, rtac ctxt (@{thm shift_def} RS fun_cong RS trans),
          etac ctxt (@{thm append_Nil} RS sym RS arg_cong RS trans),
          REPEAT_DETERM_N m o (rtac ctxt conjI THEN' assume_tac ctxt),
          CONJ_WRAP' (K (EVERY' [etac ctxt trans, rtac ctxt @{thm Collect_cong},
            rtac ctxt @{thm eqset_imp_iff}, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm Succ_Shift},
            rtac ctxt (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
  in
    unfold_thms_tac ctxt defs THEN
    CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
  end;

fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
  let
    val n = length Lev_0s;
    val ks = n downto 1;
  in
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn Lev_0 =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
          etac ctxt @{thm singletonE}, etac ctxt ssubst, rtac ctxt @{thm list.size(3)}]) Lev_0s,
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn Lev_Suc =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
            (fn i =>
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
                rtac ctxt trans, rtac ctxt @{thm length_Cons}, rtac ctxt @{thm arg_cong[of _ _ Suc]},
                REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
                etac ctxt mp, assume_tac ctxt]) ks])
      Lev_Sucs] 1
  end;

fun mk_length_Lev'_tac ctxt length_Lev =
  EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1;

fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
  let
    val n = length rv_Nils;
    val ks = 1 upto n;
  in
    EVERY' [rtac ctxt (Thm.instantiate' cTs cts @{thm list.induct}),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn rv_Cons =>
        CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac ctxt exI,
          rtac ctxt (@{thm append_Nil} RS arg_cong RS trans),
          rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans), rtac ctxt rv_Nil]))
        (ks ~~ rv_Nils))
      rv_Conss,
      REPEAT_DETERM o rtac ctxt allI, rtac ctxt (mk_sumEN n),
      EVERY' (map (fn i =>
        CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac ctxt allE, dtac ctxt (mk_conjunctN n i),
          CONJ_WRAP' (fn i' => EVERY' [dtac ctxt (mk_conjunctN n i'), etac ctxt exE, rtac ctxt exI,
            rtac ctxt (@{thm append_Cons} RS arg_cong RS trans), rtac ctxt (rv_Cons RS trans),
            if n = 1 then K all_tac else etac ctxt (sum_case_cong_weak RS trans),
            rtac ctxt (mk_sum_caseN n i RS trans), assume_tac ctxt])
          ks])
        rv_Conss)
      ks)] 1
  end;

fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
  let
    val n = length Lev_0s;
    val ks = 1 upto n;
  in
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
          etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
          CONJ_WRAP' (fn i' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
            (if i = i'
            then EVERY' [dtac ctxt (mk_InN_inject n i), hyp_subst_tac ctxt,
              CONJ_WRAP' (fn (i'', Lev_0'') =>
                EVERY' [rtac ctxt impI, rtac ctxt @{thm ssubst_mem[OF append_Nil]},
                  rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i''),
                  rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
                  etac ctxt conjI, rtac ctxt (Lev_0'' RS equalityD2 RS set_mp),
                  rtac ctxt @{thm singletonI}])
              (ks ~~ Lev_0s)]
            else etac ctxt (mk_InN_not_InM i' i RS notE)))
          ks])
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
            (fn (i, from_to_sbd) =>
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE], hyp_subst_tac ctxt,
                CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
                  CONJ_WRAP' (fn i'' =>
                    EVERY' [rtac ctxt impI, rtac ctxt (Lev_Suc RS equalityD2 RS set_mp),
                      rtac ctxt @{thm ssubst_mem[OF append_Cons]}, rtac ctxt (mk_UnIN n i),
                      rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl,
                      rtac ctxt conjI, assume_tac ctxt, dtac ctxt (sym RS trans RS sym),
                      rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS trans),
                      etac ctxt (from_to_sbd RS arg_cong), REPEAT_DETERM o etac ctxt allE,
                      dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
                      dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
                      dtac ctxt (mk_conjunctN n i''), etac ctxt mp, assume_tac ctxt])
                  ks)
                ks])
          (rev (ks ~~ from_to_sbds))])
      ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
  end;

fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
  let
    val n = length Lev_0s;
    val ks = 1 upto n;
  in
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_0 RS equalityD1 RS set_mp),
          etac ctxt @{thm singletonE}, hyp_subst_tac ctxt,
          CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
            CONJ_WRAP' (fn i'' => rtac ctxt impI THEN' dtac ctxt (sym RS trans) THEN' rtac ctxt rv_Nil THEN'
              (if i = i''
              then EVERY' [dtac ctxt @{thm ssubst_mem[OF sym[OF append_Nil]]},
                dtac ctxt (Lev_Suc RS equalityD1 RS set_mp), dtac ctxt (mk_InN_inject n i),
                hyp_subst_tac ctxt,
                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
                  (fn k => REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
                    dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
                    (if k = i'
                    then EVERY' [dtac ctxt (mk_InN_inject n k), hyp_subst_tac ctxt, etac ctxt imageI]
                    else etac ctxt (mk_InN_not_InM i' k RS notE)))
                (rev ks)]
              else etac ctxt (mk_InN_not_InM i'' i RS notE)))
            ks)
          ks])
      ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) =>
        EVERY' [rtac ctxt impI, dtac ctxt (Lev_Suc RS equalityD1 RS set_mp),
          CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE))
            (fn (i, (from_to_sbd, to_sbd_inj)) =>
              REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
              CONJ_WRAP' (fn i' => rtac ctxt impI THEN'
                dtac ctxt @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
                dtac ctxt (Lev_Suc RS equalityD1 RS set_mp) THEN'
                CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn k =>
                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE] THEN'
                  dtac ctxt list_inject_iffD1 THEN' etac ctxt conjE THEN'
                  (if k = i
                  then EVERY' [dtac ctxt (mk_InN_inject n i),
                    dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                    assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt] THEN'
                    CONJ_WRAP' (fn i'' =>
                      EVERY' [rtac ctxt impI, dtac ctxt (sym RS trans),
                        rtac ctxt (rv_Cons RS trans), rtac ctxt (mk_sum_caseN n i RS arg_cong RS trans),
                        etac ctxt (from_to_sbd RS arg_cong),
                        REPEAT_DETERM o etac ctxt allE,
                        dtac ctxt (mk_conjunctN n i), dtac ctxt mp, assume_tac ctxt,
                        dtac ctxt (mk_conjunctN n i'), dtac ctxt mp, assume_tac ctxt,
                        dtac ctxt (mk_conjunctN n i''), etac ctxt mp, etac ctxt sym])
                    ks
                  else etac ctxt (mk_InN_not_InM i k RS notE)))
                (rev ks))
              ks)
          (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))])
      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1
  end;

fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss
  from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss
  set_image_Levsss set_map0ss map_comp_ids map_cong0s =
  let
    val n = length beh_defs;
    val ks = 1 upto n;

    fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'),
      (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) =
      EVERY' [rtac ctxt ballI, rtac ctxt (carT_def RS equalityD2 RS set_mp),
        rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, rtac ctxt conjI,
        rtac ctxt conjI,
          rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
          rtac ctxt @{thm singletonI},
        (**)
          rtac ctxt ballI, etac ctxt @{thm UN_E},
          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
            (set_Levs, set_image_Levs))))) =>
            EVERY' [rtac ctxt ballI,
              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
              rtac ctxt (rev_mp OF [rv_last, impI]), etac ctxt exE, rtac ctxt (isNode_def RS iffD2),
              rtac ctxt exI, rtac ctxt conjI,
              if n = 1 then rtac ctxt refl
              else etac ctxt (sum_case_cong_weak RS trans) THEN' rtac ctxt (mk_sum_caseN n i),
              CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
                  rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, etac ctxt set_Lev,
                  if n = 1 then rtac ctxt refl else assume_tac ctxt, assume_tac ctxt, rtac ctxt subsetI,
                  REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
                  REPEAT_DETERM_N 4 o etac ctxt thin_rl,
                  rtac ctxt set_image_Lev,
                  assume_tac ctxt, dtac ctxt length_Lev, hyp_subst_tac ctxt, dtac ctxt length_Lev',
                  etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                  if n = 1 then rtac ctxt refl else assume_tac ctxt])
              (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
            (set_Levss ~~ set_image_Levss))))),
        (*root isNode*)
          rtac ctxt (isNode_def RS iffD2), rtac ctxt exI, rtac ctxt conjI,
          CONVERSION (Conv.top_conv
            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
          if n = 1 then rtac ctxt refl else rtac ctxt (mk_sum_caseN n i),
          CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
            EVERY' [rtac ctxt (set_map0 RS trans), rtac ctxt equalityI, rtac ctxt @{thm image_subsetI},
              rtac ctxt CollectI, rtac ctxt @{thm SuccI}, rtac ctxt @{thm UN_I}, rtac ctxt UNIV_I, rtac ctxt set_Lev,
              rtac ctxt (Lev_0 RS equalityD2 RS set_mp), rtac ctxt @{thm singletonI}, rtac ctxt rv_Nil,
              assume_tac ctxt, rtac ctxt subsetI,
              REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm SuccE}, @{thm UN_E}],
              rtac ctxt set_image_Lev, rtac ctxt (Lev_0 RS equalityD2 RS set_mp),
              rtac ctxt @{thm singletonI}, dtac ctxt length_Lev',
              etac ctxt @{thm set_mp[OF equalityD1[OF arg_cong[OF
                trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
              rtac ctxt rv_Nil])
          (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];

    fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)),
      ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
      EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt strT_def,
        CONVERSION (Conv.top_conv
          (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
        if n = 1 then K all_tac
        else (rtac ctxt (sum_case_cong_weak RS trans) THEN'
          rtac ctxt (mk_sum_caseN n i) THEN' rtac ctxt (mk_sum_caseN n i RS trans)),
        rtac ctxt (map_comp_id RS trans), rtac ctxt (map_cong0 OF replicate m refl),
        EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
          DETERM o EVERY' [rtac ctxt trans, rtac ctxt o_apply, rtac ctxt prod_injectI, rtac ctxt conjI,
            rtac ctxt trans, rtac ctxt @{thm Shift_def},
            rtac ctxt equalityI, rtac ctxt subsetI, etac ctxt thin_rl,
            REPEAT_DETERM o eresolve_tac ctxt [CollectE, @{thm UN_E}], dtac ctxt length_Lev', dtac ctxt asm_rl,
            etac ctxt thin_rl, dtac ctxt @{thm set_rev_mp[OF _ equalityD1]},
            rtac ctxt (@{thm length_Cons} RS arg_cong RS trans), rtac ctxt Lev_Suc,
            CONJ_WRAP_GEN' (etac ctxt (Thm.permute_prems 1 1 UnE)) (fn i'' =>
              EVERY' [REPEAT_DETERM o eresolve_tac ctxt [CollectE, exE, conjE],
                dtac ctxt list_inject_iffD1, etac ctxt conjE,
                if i' = i'' then EVERY' [dtac ctxt (mk_InN_inject n i'),
                  dtac ctxt (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
                  assume_tac ctxt, assume_tac ctxt, hyp_subst_tac ctxt, etac ctxt @{thm UN_I[OF UNIV_I]}]
                else etac ctxt (mk_InN_not_InM i' i'' RS notE)])
            (rev ks),
            rtac ctxt @{thm UN_least}, rtac ctxt subsetI, rtac ctxt CollectI, rtac ctxt @{thm UN_I[OF UNIV_I]},
            rtac ctxt (Lev_Suc RS equalityD2 RS set_mp), rtac ctxt (mk_UnIN n i'), rtac ctxt CollectI,
            REPEAT_DETERM o rtac ctxt exI, rtac ctxt conjI, rtac ctxt refl, etac ctxt conjI, assume_tac ctxt,
            rtac ctxt trans, rtac ctxt @{thm shift_def}, rtac ctxt iffD2, rtac ctxt @{thm fun_eq_iff}, rtac ctxt allI,
            CONVERSION (Conv.top_conv
              (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
            if n = 1 then K all_tac
            else rtac ctxt sum_case_cong_weak THEN' rtac ctxt (mk_sum_caseN n i' RS trans),
            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac ctxt refl])
        ks to_sbd_injs from_to_sbds)];
  in
    (rtac ctxt mor_cong THEN'
    EVERY' (map (fn thm => rtac ctxt (thm RS @{thm ext})) beh_defs) THEN'
    rtac ctxt (mor_def RS iffD2) THEN' rtac ctxt conjI THEN'
    CONJ_WRAP' fbetw_tac
      (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
        (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN'
    CONJ_WRAP' mor_tac
      (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~
        ((map_comp_ids ~~ map_cong0s) ~~
          (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
  end;

fun mk_congruent_str_final_tac ctxt m lsbisE map_comp_id map_cong0 equiv_LSBISs =
  EVERY' [rtac ctxt @{thm congruentI}, dtac ctxt lsbisE,
    REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, bexE], rtac ctxt (o_apply RS trans),
    etac ctxt (sym RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
    rtac ctxt (map_cong0 RS trans), REPEAT_DETERM_N m o rtac ctxt refl,
    EVERY' (map (fn equiv_LSBIS =>
      EVERY' [rtac ctxt @{thm equiv_proj}, rtac ctxt equiv_LSBIS, etac ctxt set_mp, assume_tac ctxt])
    equiv_LSBISs), rtac ctxt sym, rtac ctxt (o_apply RS trans),
    etac ctxt (sym RS arg_cong RS trans), rtac ctxt map_comp_id] 1;

fun mk_coalg_final_tac ctxt m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
  EVERY' [rtac ctxt (coalg_def RS iffD2),
    CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
      EVERY' [rtac ctxt @{thm univ_preserves}, rtac ctxt equiv_LSBIS, rtac ctxt congruent_str_final,
        rtac ctxt ballI, rtac ctxt @{thm ssubst_mem}, rtac ctxt o_apply, rtac ctxt CollectI,
        REPEAT_DETERM_N m o EVERY' [rtac ctxt conjI, rtac ctxt subset_UNIV],
        CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
          EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
            rtac ctxt @{thm image_subsetI}, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
            rtac ctxt equiv_LSBIS, etac ctxt set_rev_mp, etac ctxt coalgT_set])
        (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
    ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;

fun mk_mor_T_final_tac ctxt mor_def congruent_str_finals equiv_LSBISs =
  EVERY' [rtac ctxt (mor_def RS iffD2), rtac ctxt conjI,
    CONJ_WRAP' (fn equiv_LSBIS =>
      EVERY' [rtac ctxt ballI, rtac ctxt iffD2, rtac ctxt @{thm proj_in_iff},
        rtac ctxt equiv_LSBIS, assume_tac ctxt])
    equiv_LSBISs,
    CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
      EVERY' [rtac ctxt ballI, rtac ctxt sym, rtac ctxt trans, rtac ctxt @{thm univ_commute}, rtac ctxt equiv_LSBIS,
        rtac ctxt congruent_str_final, assume_tac ctxt, rtac ctxt o_apply])
    (equiv_LSBISs ~~ congruent_str_finals)] 1;

fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
  unfold_thms_tac ctxt defs THEN
  EVERY' [rtac ctxt conjI,
    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' rtac ctxt thm) Reps,
    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
      EVERY' [rtac ctxt ballI, rtac ctxt (map_comp_id RS trans), rtac ctxt map_cong0L,
        EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
          EVERY' [rtac ctxt ballI, rtac ctxt (o_apply RS trans), rtac ctxt Abs_inverse,
            etac ctxt set_rev_mp, rtac ctxt coalg_final_set, rtac ctxt Rep])
        Abs_inverses coalg_final_sets)])
    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;

fun mk_mor_Abs_tac ctxt defs Abs_inverses =
  unfold_thms_tac ctxt defs THEN
  EVERY' [rtac ctxt conjI,
    CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
    CONJ_WRAP' (fn thm => rtac ctxt ballI THEN' etac ctxt (thm RS arg_cong RS sym)) Abs_inverses] 1;

fun mk_mor_unfold_tac ctxt m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
  EVERY' [rtac ctxt iffD2, rtac ctxt mor_UNIV,
    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
      EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (dtor_def RS trans),
        rtac ctxt (unfold_def RS arg_cong RS trans), rtac ctxt (Abs_inverse RS arg_cong RS trans),
        rtac ctxt (morE RS arg_cong RS trans), rtac ctxt (map_comp_id RS trans),
        rtac ctxt (o_apply RS trans RS sym), rtac ctxt map_cong0,
        REPEAT_DETERM_N m o rtac ctxt refl,
        EVERY' (map (fn thm => rtac ctxt (thm RS trans) THEN' rtac ctxt (o_apply RS sym)) unfold_defs)])
    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;

fun mk_raw_coind_tac ctxt 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 ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1],
      REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
      rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
      rtac ctxt bis_Gr, rtac ctxt tcoalg,
      rtac ctxt mor_Rep, REPEAT_DETERM_N n o etac ctxt @{thm relImage_Gr},
      rtac ctxt impI, rtac ctxt rev_mp, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_Gr, rtac ctxt coalgT,
      rtac ctxt mor_T_final, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt bis_converse, rtac ctxt bis_Gr, rtac ctxt coalgT,
      rtac ctxt mor_T_final, EVERY' (map (fn thm => rtac ctxt (thm RS @{thm relInvImage_Gr})) lsbis_incls),
      rtac ctxt impI,
      CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) =>
        EVERY' [rtac ctxt subset_trans, rtac ctxt @{thm relInvImage_UNIV_relImage}, rtac ctxt subset_trans,
          rtac ctxt @{thm relInvImage_mono}, rtac ctxt subset_trans, etac ctxt incl_lsbis,
          rtac ctxt ord_eq_le_trans, rtac ctxt @{thm sym[OF relImage_relInvImage]},
          rtac ctxt @{thm xt1(3)}, rtac ctxt @{thm Sigma_cong},
          rtac ctxt @{thm proj_image}, rtac ctxt @{thm proj_image}, rtac ctxt lsbis_incl,
          rtac ctxt subset_trans, rtac ctxt @{thm relImage_mono}, rtac ctxt incl_lsbis, assume_tac ctxt,
          rtac ctxt @{thm relImage_proj}, rtac ctxt equiv_LSBIS, rtac ctxt @{thm relInvImage_Id_on},
          rtac ctxt Rep_inject])
      (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
  end;

fun mk_unfold_unique_mor_tac ctxt raw_coinds bis mor unfold_defs =
  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
    EVERY' [rtac ctxt @{thm ext}, etac ctxt (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac ctxt mor,
      rtac ctxt @{thm image2_eqI}, rtac ctxt refl, rtac ctxt (unfold_def RS arg_cong RS trans),
      rtac ctxt (o_apply RS sym), rtac ctxt UNIV_I]) (raw_coinds ~~ unfold_defs) 1;

fun mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id map_cong0L unfold_o_dtors =
  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ctxt @{thm ext}, rtac ctxt trans, rtac ctxt o_apply,
    rtac ctxt trans, rtac ctxt unfold, rtac ctxt trans, rtac ctxt map_comp_id, rtac ctxt trans, rtac ctxt map_cong0L,
    EVERY' (map (fn thm =>
      rtac ctxt ballI THEN' rtac ctxt (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
    rtac ctxt sym, rtac ctxt id_apply] 1;

fun mk_corec_tac ctxt m corec_defs unfold map_cong0 corec_Inls =
  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac ctxt trans, rtac ctxt (o_apply RS arg_cong),
    rtac ctxt trans, rtac ctxt unfold, fo_rtac ctxt (@{thm sum.case(2)} RS arg_cong RS trans),
    rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt refl,
    EVERY' (map (fn thm => rtac ctxt @{thm case_sum_expand_Inr} THEN' rtac ctxt thm) corec_Inls)] 1;

fun mk_corec_unique_mor_tac ctxt corec_defs corec_Inls unfold_unique_mor =
  unfold_thms_tac ctxt
    (corec_defs @ map (fn thm => thm RS @{thm case_sum_expand_Inr'}) corec_Inls) THEN
  etac ctxt unfold_unique_mor 1;

fun mk_dtor_coinduct_tac ctxt m raw_coind bis_rel rel_congs =
  EVERY' [rtac ctxt rev_mp, rtac ctxt raw_coind, rtac ctxt iffD2, rtac ctxt bis_rel, rtac ctxt conjI,
    CONJ_WRAP' (K (rtac ctxt @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
    rel_congs,
    CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
      REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
      REPEAT_DETERM_N m o rtac ctxt refl,
      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
    rel_congs,
    rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
    CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
      rtac ctxt CollectI, etac ctxt @{thm case_prodI}])) rel_congs] 1;

fun mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0 =
  EVERY' [rtac ctxt @{thm ext}, rtac ctxt (o_apply RS trans RS sym), rtac ctxt (o_apply RS trans RS sym),
    rtac ctxt (unfold RS trans), rtac ctxt (Thm.permute_prems 0 1 (map_comp RS @{thm box_equals})),
    rtac ctxt map_cong0,
    REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
    REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
    rtac ctxt map_arg_cong, rtac ctxt (o_apply RS sym)] 1;

fun mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss =
  EVERY' [rtac ctxt Jset_minimal,
    REPEAT_DETERM_N n o rtac ctxt @{thm Un_upper1},
    REPEAT_DETERM_N n o
      EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
        EVERY' [rtac ctxt subsetI, rtac ctxt @{thm UnI2}, rtac ctxt (mk_UnIN n i), etac ctxt @{thm UN_I},
          etac ctxt UnE, etac ctxt set_Jset, REPEAT_DETERM_N (n - 1) o etac ctxt UnE,
          EVERY' (map (fn thm => EVERY' [etac ctxt @{thm UN_E}, etac ctxt thm, assume_tac ctxt]) set_Jset_Jsets)])
      (1 upto n) set_Jsets set_Jset_Jsetss)] 1;

fun mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets =
  EVERY' [rtac ctxt @{thm Un_least}, rtac ctxt set_incl_Jset,
    REPEAT_DETERM_N (n - 1) o rtac ctxt @{thm Un_least},
    EVERY' (map (fn thm => rtac ctxt @{thm UN_least} THEN' etac ctxt thm) set_Jset_incl_Jsets)] 1;

fun mk_map_id0_tac ctxt maps unfold_unique unfold_dtor =
  EVERY' [rtac ctxt (unfold_unique RS trans), EVERY' (map (rtac ctxt o mk_sym) maps),
    rtac ctxt unfold_dtor] 1;

fun mk_map_comp0_tac ctxt maps map_comp0s map_unique =
  EVERY' [rtac ctxt map_unique,
    EVERY' (map2 (fn map_thm => fn map_comp0 =>
      EVERY' (map (rtac ctxt)
        [@{thm comp_assoc[symmetric]} RS trans,
        @{thm arg_cong2[of _ _ _ _ "(\)"]} OF [map_thm, refl] RS trans,
        @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans,
        @{thm comp_assoc[symmetric]} RS trans,
        @{thm arg_cong2[of _ _ _ _ "(\)"]} OF [map_comp0 RS sym, refl]]))
    maps map_comp0s)] 1;

fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss
  set_Jset_Jsetsss in_rels =
  let
    val n = length map_comps;
    val ks = 1 upto n;
  in
    EVERY' ([rtac ctxt rev_mp, coinduct_tac] @
      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
        set_Jset_Jsetss), in_rel) =>
        [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
         REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], hyp_subst_tac ctxt, rtac ctxt exI,
         rtac ctxt (Drule.rotate_prems 1 conjI),
         rtac ctxt conjI, rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
         REPEAT_DETERM_N m o (rtac ctxt o_apply_trans_sym THEN' rtac ctxt @{thm fst_conv}),
         REPEAT_DETERM_N n o rtac ctxt fst_convol_fun_cong_sym,
         rtac ctxt map_comp_trans, rtac ctxt sym, rtac ctxt dtor_maps_trans, rtac ctxt map_cong0,
         EVERY' (maps (fn set_Jset =>
           [rtac ctxt o_apply_trans_sym, rtac ctxt (@{thm snd_conv} RS trans), etac ctxt CollectE,
           REPEAT_DETERM o etac ctxt conjE, etac ctxt bspec, etac ctxt set_Jset]) set_Jsets),
         REPEAT_DETERM_N n o rtac ctxt snd_convol_fun_cong_sym,
         rtac ctxt CollectI,
         EVERY' (map (fn set_map0 => EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
           rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt refl])
        (take m set_map0s)),
         CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
           EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
             rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI}, rtac ctxt exI, rtac ctxt conjI,
             rtac ctxt CollectI, etac ctxt CollectE,
             REPEAT_DETERM o etac ctxt conjE,
             CONJ_WRAP' (fn set_Jset_Jset =>
               EVERY' [rtac ctxt ballI, etac ctxt bspec, etac ctxt set_Jset_Jset, assume_tac ctxt]) set_Jset_Jsets,
             rtac ctxt (conjI OF [refl, refl])])
           (drop m set_map0s ~~ set_Jset_Jsetss)])
        (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
          map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
      [rtac ctxt impI,
       CONJ_WRAP' (fn k =>
         EVERY' [rtac ctxt impI, dtac ctxt (mk_conjunctN n k), etac ctxt mp, rtac ctxt exI, rtac ctxt conjI, etac ctxt CollectI,
           rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl]) ks]) 1
  end

fun mk_dtor_map_unique_tac ctxt unfold_unique sym_map_comps =
  rtac ctxt unfold_unique 1 THEN
  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
  ALLGOALS (etac ctxt sym);

fun mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_maps set_map0ss =
  let
    val n = length dtor_maps;
  in
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
      REPEAT_DETERM o rtac ctxt allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
      CONJ_WRAP' (K (rtac ctxt @{thm image_empty})) rec_0s,
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
        [SELECT_GOAL (unfold_thms_tac ctxt
          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
        rtac ctxt Un_cong, rtac ctxt refl,
        CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 Un_cong))
          (fn i => EVERY' [rtac ctxt @{thm SUP_cong[OF refl]},
            REPEAT_DETERM o etac ctxt allE, etac ctxt (mk_conjunctN n i)]) (n downto 1)])
      (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
  end;

fun mk_set_map0_tac ctxt col_natural =
  EVERY' (map (rtac ctxt) [@{thm ext}, o_apply RS trans, sym, o_apply RS trans,
    @{thm image_UN} RS trans, refl RS @{thm SUP_cong}, col_natural]) 1;

fun mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
  let
    val n = length rec_0s;
  in
    EVERY' [rtac ctxt (Thm.instantiate' [] cts nat_induct),
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn rec_0 => EVERY' (map (rtac ctxt) [ordIso_ordLeq_trans,
        @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s,
      REPEAT_DETERM o rtac ctxt allI,
      CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY'
        [rtac ctxt ordIso_ordLeq_trans, rtac ctxt @{thm card_of_ordIso_subst}, rtac ctxt rec_Suc,
        rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac ctxt (nth set_sbds (j - 1)),
        REPEAT_DETERM_N (n - 1) o rtac ctxt (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
        EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac ctxt @{thm UNION_Cinfinite_bound},
          rtac ctxt set_sbd, rtac ctxt ballI, REPEAT_DETERM o etac ctxt allE,
          etac ctxt (mk_conjunctN n i), rtac ctxt sbd_Cinfinite]) (1 upto n) (drop m set_sbds))])
      (rec_Sucs ~~ set_sbdss)] 1
  end;

fun mk_set_bd_tac ctxt sbd_Cinfinite col_bd =
  EVERY' (map (rtac ctxt) [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
    @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1;

fun mk_le_rel_OO_tac ctxt coinduct rel_Jrels le_rel_OOs =
  EVERY' (rtac ctxt coinduct :: map2 (fn rel_Jrel => fn le_rel_OO =>
    let val Jrel_imp_rel = rel_Jrel RS iffD1;
    in
      EVERY' [rtac ctxt (le_rel_OO RS @{thm predicate2D}), etac ctxt @{thm relcomppE},
      rtac ctxt @{thm relcomppI}, etac ctxt Jrel_imp_rel, etac ctxt Jrel_imp_rel]
    end)
  rel_Jrels le_rel_OOs) 1;

fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
  ALLGOALS (TRY o (eresolve_tac ctxt coind_wits THEN' rtac ctxt refl)) THEN
  REPEAT_DETERM (assume_tac ctxt 1 ORELSE
    EVERY' [dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
    K (unfold_thms_tac ctxt dtor_ctors),
    REPEAT_DETERM_N n o etac ctxt UnE,
    REPEAT_DETERM o
      (TRY o REPEAT_DETERM o etac ctxt UnE THEN' TRY o etac ctxt @{thm UN_E} THEN'
        (eresolve_tac ctxt wit ORELSE'
        (dresolve_tac ctxt wit THEN'
          (etac ctxt FalseE ORELSE'
          EVERY' [hyp_subst_tac ctxt, dtac ctxt set_rev_mp, rtac ctxt equalityD1, resolve_tac ctxt dtor_set,
            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac ctxt UnE]))))] 1);

fun mk_coind_wit_tac ctxt induct unfolds set_nats wits =
  rtac ctxt induct 1 THEN ALLGOALS (TRY o rtac ctxt impI THEN' TRY o hyp_subst_tac ctxt) THEN
  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
  ALLGOALS (REPEAT_DETERM o etac ctxt imageE THEN' TRY o hyp_subst_tac ctxt) THEN
  ALLGOALS (TRY o
    FIRST' [rtac ctxt TrueI, rtac ctxt refl, etac ctxt (refl RSN (2, mp)), dresolve_tac ctxt wits THEN' etac ctxt FalseE]);

fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
    dtor_rels =
  CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
      REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
      unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
      HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
        EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
          etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
          rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
          rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
          REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
          REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN'
          rtac ctxt rel_funI THEN'
          etac ctxt (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
        etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
    (dtor_corec_defs ~~ dtor_unfold_transfer);

fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
    dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
  let
    val m = length dtor_set_incls;
    val n = length dtor_set_set_inclss;
    val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
    val in_Jrel = nth in_Jrels (i - 1);
    val if_tac =
      EVERY' [dtac ctxt (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
        rtac ctxt (in_rel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
        EVERY' (map2 (fn set_map0 => fn set_incl =>
          EVERY' [rtac ctxt conjI, rtac ctxt ord_eq_le_trans, rtac ctxt set_map0,
            rtac ctxt ord_eq_le_trans, rtac ctxt trans_fun_cong_image_id_id_apply,
            etac ctxt (set_incl RS @{thm subset_trans})])
        passive_set_map0s dtor_set_incls),
        CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt set_map0, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
            rtac ctxt @{thm case_prodI}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
            CONJ_WRAP' (fn thm => etac ctxt (thm RS @{thm subset_trans}) THEN' assume_tac ctxt) dtor_set_set_incls,
            rtac ctxt conjI, rtac ctxt refl, rtac ctxt refl])
        (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
        CONJ_WRAP' (fn conv =>
          EVERY' [rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
          REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
          REPEAT_DETERM_N n o EVERY' (map (rtac ctxt) [trans, o_apply, conv]),
          rtac ctxt trans, rtac ctxt sym, rtac ctxt dtor_map, rtac ctxt (dtor_inject RS iffD2), assume_tac ctxt])
        @{thms fst_conv snd_conv}];
    val only_if_tac =
      EVERY' [dtac ctxt (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE],
        rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI, rtac ctxt CollectI,
        CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
          EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt dtor_set, rtac ctxt @{thm Un_least},
            rtac ctxt ord_eq_le_trans, rtac ctxt @{thm box_equals}, rtac ctxt passive_set_map0,
            rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans_fun_cong_image_id_id_apply, assume_tac ctxt,
            CONJ_WRAP_GEN' (rtac ctxt (Thm.permute_prems 0 1 @{thm Un_least}))
              (fn (active_set_map0, in_Jrel) => EVERY' [rtac ctxt ord_eq_le_trans,
                rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
                rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
                dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
                REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
                  @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                hyp_subst_tac ctxt,
                dtac ctxt (in_Jrel RS iffD1),
                dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE,
                REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], assume_tac ctxt])
            (rev (active_set_map0s ~~ in_Jrels))])
        (dtor_sets ~~ passive_set_map0s),
        rtac ctxt conjI,
        REPEAT_DETERM_N 2 o EVERY'[rtac ctxt (dtor_inject RS iffD1), rtac ctxt trans, rtac ctxt dtor_map,
          rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
          rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
          EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
            REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
              @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
            hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),
            dtac ctxt @{thm someI_ex}, REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt]) in_Jrels),
          assume_tac ctxt]]
  in
    EVERY' [rtac ctxt iffI, if_tac, only_if_tac] 1
  end;

fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
  dtor_unfolds dtor_maps in_rels =
  let
    val n = length ks;
    val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd};
    val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
  in
    EVERY' [rtac ctxt coinduct,
      EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
          fn dtor_unfold => fn dtor_map => fn in_rel =>
        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI, in_rel RS iffD2],
          REPEAT_DETERM o eresolve_tac ctxt [exE, conjE],
          select_prem_tac ctxt (length ks) (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
          REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
          rtac ctxt exI, rtac ctxt (Drule.rotate_prems 1 conjI), rtac ctxt conjI,
          rtac ctxt (map_comp0 RS trans), rtac ctxt (dtor_map RS trans RS sym),
          rtac ctxt (dtor_unfold RS map_arg_cong RS trans), rtac ctxt (trans OF [map_comp0, map_cong]),
          REPEAT_DETERM_N m o rtac ctxt (fst_diag_nth RS @{thm fun_cong[OF trans[OF o_id sym]]}),
          REPEAT_DETERM_N n o (rtac ctxt @{thm sym[OF trans[OF o_apply]]} THEN' rtac ctxt @{thm fst_conv}),
          rtac ctxt (map_comp0 RS trans), rtac ctxt (map_cong RS trans),
          REPEAT_DETERM_N m o rtac ctxt (snd_diag_nth RS fun_cong),
          REPEAT_DETERM_N n o (rtac ctxt @{thm trans[OF o_apply]} THEN' rtac ctxt @{thm snd_conv}),
          etac ctxt (@{thm prod.case} RS map_arg_cong RS trans),
          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.case o_def fst_conv snd_conv}),
          rtac ctxt CollectI,
          CONJ_WRAP' (fn set_map0 =>
            EVERY' [rtac ctxt (set_map0 RS ord_eq_le_trans),
              rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI, rtac ctxt @{thm case_prodI},
              FIRST' [rtac ctxt refl, EVERY'[rtac ctxt exI, rtac ctxt conjI, etac ctxt Collect_splitD_set_mp,
                assume_tac ctxt, rtac ctxt (@{thm surjective_pairing} RS arg_cong)]]])
          set_map0s])
      ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels)] 1
  end;

val split_id_unfolds = @{thms prod.case image_id id_apply};

fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
  let val n = length ks;
  in
    rtac ctxt set_induct 1 THEN
    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
      EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
        hyp_subst_tac ctxt,
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
        rtac ctxt subset_refl])
    unfolds set_map0ss ks) 1 THEN
    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
      EVERY' (map (fn set_map0 =>
        EVERY' [REPEAT_DETERM o resolve_tac ctxt [allI, impI], etac ctxt conjE,
        select_prem_tac ctxt n (dtac ctxt @{thm spec2}) i, dtac ctxt mp, assume_tac ctxt,
        REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], hyp_subst_tac ctxt,
        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
        etac ctxt imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp],
        rtac ctxt conjI, etac ctxt Collect_splitD_set_mp, assume_tac ctxt,
        rtac ctxt (@{thm surjective_pairing} RS arg_cong)])
      (drop m set_map0s)))
    unfolds set_map0ss ks) 1
  end;

fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
  let val n = length in_rels;
  in
    Method.insert_tac ctxt CIHs 1 THEN
    unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
    REPEAT_DETERM (etac ctxt exE 1) THEN
    CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
      EVERY' [rtac ctxt @{thm predicate2I}, rtac ctxt (in_Jrel RS iffD2), rtac ctxt exI, rtac ctxt conjI,
        if null helper_inds then rtac ctxt UNIV_I
        else rtac ctxt CollectI THEN'
          CONJ_WRAP' (fn helper_ind =>
            EVERY' [rtac ctxt (helper_ind RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
              REPEAT_DETERM_N n o etac ctxt thin_rl, rtac ctxt impI,
              REPEAT_DETERM o resolve_tac ctxt [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
              dtac ctxt bspec, assume_tac ctxt, REPEAT_DETERM o eresolve_tac ctxt [allE, mp, conjE],
              etac ctxt (refl RSN (2, conjI))])
          helper_inds,
        rtac ctxt conjI,
        rtac ctxt (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
        REPEAT_DETERM_N n o etac ctxt thin_rl,
        rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI)),
        rtac ctxt (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o assume_tac ctxt,
        REPEAT_DETERM_N n o etac ctxt thin_rl,
        rtac ctxt impI, etac ctxt mp, rtac ctxt exI, etac ctxt (refl RSN (2, conjI))])
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik