Theory N2M

(*  Title:       N2M
    Authors:     Jasmin Blanchette, Andrei Popescu, Dmitriy Traytel
    Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Mutual View on Nested Datatypes›

(*<*)
theory N2M
  imports "HOL-Library.BNF_Axiomatization"
begin
(*>*)

notation BNF_Def.convol (‹<_, _>›)

declare [[bnf_internals]]

declare [[typedef_overloaded]]

bnf_axiomatization ('a, 'b) F0 [wits: "'a ⇒ ('a, 'b) F0"]
bnf_axiomatization ('a, 'b) G0 [wits: "'a ⇒ ('a, 'b) G0"]


subsection ‹Nested Definition›

datatype 'a F = CF "('a, 'a F) F0"
datatype 'a G = CG "('a, ('a G) F) G0"

type_synonym ('b, 'c) F_pre_F = "('c, 'b) F0"
type_synonym ('c, 'a) G_pre_G = "('a, 'c F) G0"

term "ctor_fold_F :: (('b, 'c) F_pre_F ⇒ 'b) ⇒ 'c F ⇒ 'b"
term "ctor_fold_G :: (('c, 'a) G_pre_G ⇒ 'c) ⇒ 'a G ⇒ 'c"
term "ctor_rec_F :: (('c F × 'b, 'c) F_pre_F ⇒ 'b) ⇒ 'c F ⇒ 'b"
term "ctor_rec_G :: (('a G × 'c, 'a) G_pre_G ⇒ 'c) ⇒ 'a G ⇒ 'c"
thm F.ctor_rel_induct
thm G.ctor_rel_induct[unfolded rel_pre_G_def id_apply]


subsection ‹Isomorphic Mutual Definition›

datatype 'a GM = CG "('a, 'a GFM) G0"
  and  'a GFM = CF "('a GM, 'a GFM) F0"

type_synonym ('b, 'c) GFM_pre_GFM = "('c, 'b) F0"
type_synonym ('c, 'a) GM_pre_GM = "('a, 'c) G0"

term "ctor_fold_GM :: (('c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('c, 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a GM ⇒ 'b"
term "ctor_fold_GFM :: (('c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('c, 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a GFM ⇒ 'c"
term "ctor_rec_GM :: (('a GFM × 'c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('a GFM × 'c, 'a GM × 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a GM ⇒ 'b"
term "ctor_rec_GFM :: (('a GFM × 'c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('a GFM × 'c, 'a GM × 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a GFM ⇒ 'c"
thm GM_GFM.ctor_rel_induct[unfolded rel_pre_GM_def rel_pre_GFM_def]

subsection ‹Mutualization›

subsubsection ‹Iterators›

definition n2m_ctor_fold_G :: "(('c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('c, 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a G ⇒ 'b"
  where "n2m_ctor_fold_G s1 s2 = ctor_fold_G (s1 o
    map_pre_GM id (id :: unit ⇒ unit) (ctor_fold_F (s2 o BNF_Composition.id_bnf o BNF_Composition.id_bnf)) o BNF_Composition.id_bnf o BNF_Composition.id_bnf)"
definition n2m_ctor_fold_G_F :: "(('c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('c, 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a G F ⇒ 'c"
  where "n2m_ctor_fold_G_F s1 s2 = ctor_fold_F (s2 o map_pre_GFM (id :: unit ⇒ unit) (n2m_ctor_fold_G s1 s2) id o BNF_Composition.id_bnf o BNF_Composition.id_bnf)"

lemma G_ctor_o_fold: "ctor_fold_G s o ctor_G = s o map_pre_G id (ctor_fold_G s)"
  unfolding fun_eq_iff o_apply G.ctor_fold by simp
lemma F_ctor_o_fold: "ctor_fold_F s o ctor_F = s o map_pre_F id (ctor_fold_F s)"
  unfolding fun_eq_iff o_apply F.ctor_fold by simp

lemma G_ctor_o_rec: "ctor_rec_G s o ctor_G = s o map_pre_G id (BNF_Def.convol id (ctor_rec_G s))"
  unfolding fun_eq_iff o_apply G.ctor_rec by simp
lemma F_ctor_o_rec: "ctor_rec_F s o ctor_F = s o map_pre_F id (BNF_Def.convol id (ctor_rec_F s))"
  unfolding fun_eq_iff o_apply F.ctor_rec by simp

lemma n2m_ctor_fold_G:
  "n2m_ctor_fold_G s1 s2 o ctor_G = s1 o map_pre_GM id id (n2m_ctor_fold_G_F s1 s2) o BNF_Composition.id_bnf o BNF_Composition.id_bnf"
  unfolding n2m_ctor_fold_G_def n2m_ctor_fold_G_F_def
    map_pre_G_def map_pre_F_def map_pre_GM_def map_pre_GFM_def
    G_ctor_o_fold id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF type_copy_map_comp0_undo[OF BNF_Composition.type_definition_id_bnf_UNIV BNF_Composition.type_definition_id_bnf_UNIV BNF_Composition.type_definition_id_bnf_UNIV pre_GM.map_comp0[unfolded map_pre_GM_def]]]
    F.ctor_fold_o_map
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

lemma n2m_ctor_fold_G_F:
  "n2m_ctor_fold_G_F s1 s2 o ctor_F = s2 o map_pre_GFM id (n2m_ctor_fold_G s1 s2) (n2m_ctor_fold_G_F s1 s2) o BNF_Composition.id_bnf o BNF_Composition.id_bnf"
  unfolding n2m_ctor_fold_G_F_def map_pre_F_def map_pre_GM_def map_pre_GFM_def
    F_ctor_o_fold id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF F0.map_comp0[symmetric]]
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

subsubsection ‹Recursors›

definition n2m_ctor_rec_G ::
  "(('a G F × 'c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('a G F × 'c, 'a G × 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a G ⇒ 'b"
  where "n2m_ctor_rec_G s1 s2 =
    ctor_rec_G (s1 o
      map_pre_GM id (id :: unit ⇒ unit)
        (BNF_Def.convol (map_F fst) (ctor_rec_F (s2 o map_pre_GFM (id :: unit ⇒ unit) id (map_prod (map_F fst) id) o BNF_Composition.id_bnf o BNF_Composition.id_bnf))) o
      BNF_Composition.id_bnf o BNF_Composition.id_bnf)"

definition n2m_ctor_rec_G_F ::
  "(('a G F × 'c, 'a) GM_pre_GM ⇒ 'b) ⇒ (('a G F × 'c, 'a G × 'b) GFM_pre_GFM ⇒ 'c) ⇒ 'a G F ⇒ 'c"
  where "n2m_ctor_rec_G_F s1 s2 = ctor_rec_F (s2 o map_pre_GFM (id :: unit ⇒ unit) (BNF_Def.convol id (n2m_ctor_rec_G s1 s2)) id o BNF_Composition.id_bnf o BNF_Composition.id_bnf)"

lemma n2m_ctor_rec_G:
  "n2m_ctor_rec_G s1 s2 o ctor_G = s1 o map_pre_GM id id (BNF_Def.convol id (n2m_ctor_rec_G_F s1 s2)) o BNF_Composition.id_bnf o BNF_Composition.id_bnf"
  unfolding n2m_ctor_rec_G_def n2m_ctor_rec_G_F_def
    map_pre_G_def map_pre_F_def map_pre_GM_def map_pre_GFM_def
    G_ctor_o_rec
    id_apply comp_id id_comp comp_assoc map_prod.comp map_prod.id
    fst_convol map_prod_o_convol convol_o
    rewriteL_comp_comp[OF G0.map_comp0[symmetric]]
    rewriteL_comp_comp[OF F0.map_comp0[symmetric]]
    F.map_comp0[symmetric] F.map_id0
    F.ctor_rec_o_map
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

lemma n2m_ctor_rec_G_F:
  "n2m_ctor_rec_G_F s1 s2 o ctor_F = s2 o map_pre_GFM id (BNF_Def.convol id (n2m_ctor_rec_G s1 s2)) (BNF_Def.convol id (n2m_ctor_rec_G_F s1 s2)) o BNF_Composition.id_bnf o BNF_Composition.id_bnf"
  unfolding n2m_ctor_rec_G_F_def map_pre_F_def map_pre_GM_def map_pre_GFM_def
    F_ctor_o_rec id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF F0.map_comp0[symmetric]]
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

subsubsection ‹Induction›

lemma n2m_rel_induct_G_G_F:
  assumes IH1: "∀x y. BNF_Def.vimage2p (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (rel_pre_GM P R S) x y ⟶ R (ctor_G x) (ctor_G y)"
    and     IH2: "∀x y. BNF_Def.vimage2p (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (rel_pre_GFM P R S) x y ⟶ S (ctor_F x) (ctor_F y)"
  shows "rel_G P ≤ R ∧ rel_F (rel_G P) ≤ S"
  apply (rule context_conjI)
  apply (rule G.ctor_rel_induct[unfolded rel_pre_G_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF IH1], OF vimage2p_mono[OF _ pre_GM.rel_mono], unfolded vimage2p_def o_apply rel_pre_GM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])
  apply (rule order_refl)
  apply (rule order_refl)
  apply (rule F.ctor_rel_induct[unfolded rel_pre_F_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF IH2], unfolded vimage2p_def o_apply rel_pre_GFM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])

  apply (rule F.ctor_rel_induct[unfolded rel_pre_F_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF IH2], OF vimage2p_mono[OF _ pre_GFM.rel_mono], unfolded vimage2p_def o_apply rel_pre_GFM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])
  apply (rule order_refl)
  apply assumption
  apply (rule order_refl)
  done

lemmas n2m_ctor_induct_G_G_F = spec[OF spec [OF
      n2m_rel_induct_G_G_F[of "(=)" "BNF_Def.Grp (Collect R) id" "BNF_Def.Grp (Collect S) id" for R S,
        unfolded G.rel_eq F.rel_eq eq_le_Grp_id_iff all_simps(1,2)[symmetric]]],
    unfolded eq_alt pre_GM.rel_Grp pre_GFM.rel_Grp pre_GM.map_id0 pre_GFM.map_id0,
    unfolded vimage2p_comp vimage2p_id comp_apply comp_id Grp_id_mono_subst
    type_copy_vimage2p_Grp_Rep[OF BNF_Composition.type_definition_id_bnf_UNIV]
    type_copy_Abs_o_Rep[OF BNF_Composition.type_definition_id_bnf_UNIV]
    eqTrueI[OF subset_UNIV] simp_thms(22)
    atomize_conjL[symmetric] atomize_all[symmetric] atomize_imp[symmetric],
    unfolded subset_iff mem_Collect_eq]


section ‹Mutual View on Nested Coatatypes›

bnf_axiomatization ('a, 'b) coF0
bnf_axiomatization ('a, 'b) coG0


subsection ‹Nested definition›

codatatype 'a coF = CcoF "('a, 'a coF) coF0"
codatatype 'a coG = CcoG "('a, ('a coG) coF) coG0"

type_synonym ('b, 'c) coF_pre_coF = "('c, 'b) coF0"
type_synonym ('c, 'a) coG_pre_coG = "('a, 'c coF) coG0"

term "dtor_unfold_coF :: ('b ⇒ ('b, 'c) coF_pre_coF) ⇒ 'b ⇒ 'c coF"
term "dtor_unfold_coG :: ('c ⇒ ('c, 'a) coG_pre_coG) ⇒ 'c ⇒ 'a coG"
term "dtor_corec_coF :: ('b ⇒ ('c coF + 'b, 'c) coF_pre_coF) ⇒ 'b ⇒ 'c coF"
term "dtor_corec_coG :: ('c ⇒ ('a coG + 'c, 'a) coG_pre_coG) ⇒ 'c ⇒ 'a coG"
thm coF.dtor_rel_coinduct
thm coG.dtor_rel_coinduct[unfolded rel_pre_coG_def id_apply]


subsection ‹Isomorphic Mutual Definition›

codatatype 'a coGM = CcoG "('a, 'a coGcoFM) coG0"
  and  'a coGcoFM = CcoF "('a coGM, 'a coGcoFM) coF0"

type_synonym ('b, 'c) coGcoFM_pre_coGcoFM = "('c, 'b) coF0"
type_synonym ('c, 'a) coGM_pre_coGM = "('a, 'c) coG0"

term "dtor_unfold_coGM :: ('b ⇒ ('c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('c, 'b) coGcoFM_pre_coGcoFM) ⇒ 'b ⇒ 'a coGM"
term "dtor_unfold_coGcoFM :: ('b ⇒ ('c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('c, 'b) coGcoFM_pre_coGcoFM) ⇒ 'c ⇒ 'a coGcoFM"
term "dtor_corec_coGM :: ('b ⇒ ('a coGcoFM + 'c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('a coGcoFM + 'c, 'a coGM + 'b) coGcoFM_pre_coGcoFM) ⇒ 'b ⇒ 'a coGM"
term "dtor_corec_coGcoFM :: ('b ⇒ ('a coGcoFM + 'c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('a coGcoFM + 'c, 'a coGM + 'b) coGcoFM_pre_coGcoFM) ⇒ 'c ⇒ 'a coGcoFM"
thm coGM_coGcoFM.dtor_rel_coinduct[unfolded rel_pre_coGM_def rel_pre_coGcoFM_def]

subsection ‹Mutualization›

subsubsection ‹Coiterators›

definition n2m_dtor_unfold_coG :: "('b ⇒ ('c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('c, 'b) coGcoFM_pre_coGcoFM) ⇒ 'b ⇒ 'a coG"
  where "n2m_dtor_unfold_coG s1 s2 = dtor_unfold_coG (BNF_Composition.id_bnf o BNF_Composition.id_bnf o
    map_pre_coGM id (id :: unit ⇒ unit) (dtor_unfold_coF (BNF_Composition.id_bnf o BNF_Composition.id_bnf o s2)) o s1)"
definition n2m_dtor_unfold_coG_coF :: "('b ⇒ ('c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('c, 'b) coGcoFM_pre_coGcoFM) ⇒ 'c ⇒ 'a coG coF"
  where "n2m_dtor_unfold_coG_coF s1 s2 = dtor_unfold_coF (BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGcoFM (id :: unit ⇒ unit) (n2m_dtor_unfold_coG s1 s2) id o s2)"

lemma coG_dtor_o_unfold: "dtor_coG o dtor_unfold_coG s = map_pre_coG id (dtor_unfold_coG s) o s"
  unfolding fun_eq_iff o_apply coG.dtor_unfold by simp
lemma coF_dtor_o_unfold: "dtor_coF o dtor_unfold_coF s = map_pre_coF id (dtor_unfold_coF s) o s"
  unfolding fun_eq_iff o_apply coF.dtor_unfold by simp

lemma coG_dtor_o_corec: "dtor_coG o dtor_corec_coG s = map_pre_coG id (case_sum id (dtor_corec_coG s)) o s"
  unfolding fun_eq_iff o_apply coG.dtor_corec by simp
lemma coF_dtor_o_corec: "dtor_coF o dtor_corec_coF s = map_pre_coF id (case_sum id (dtor_corec_coF s)) o s"
  unfolding fun_eq_iff o_apply coF.dtor_corec by simp

lemma n2m_dtor_unfold_coG:
  "dtor_coG o n2m_dtor_unfold_coG s1 s2 = BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGM id id (n2m_dtor_unfold_coG_coF s1 s2) o s1"
  unfolding n2m_dtor_unfold_coG_def n2m_dtor_unfold_coG_coF_def
    map_pre_coG_def map_pre_coF_def map_pre_coGM_def map_pre_coGcoFM_def
    coG_dtor_o_unfold id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF type_copy_map_comp0_undo[OF BNF_Composition.type_definition_id_bnf_UNIV BNF_Composition.type_definition_id_bnf_UNIV BNF_Composition.type_definition_id_bnf_UNIV pre_coGM.map_comp0[unfolded map_pre_coGM_def]]]
    coF.dtor_unfold_o_map
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

lemma n2m_dtor_unfold_coG_coF:
  "dtor_coF o n2m_dtor_unfold_coG_coF s1 s2 = BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGcoFM id (n2m_dtor_unfold_coG s1 s2) (n2m_dtor_unfold_coG_coF s1 s2) o s2"
  unfolding n2m_dtor_unfold_coG_coF_def map_pre_coF_def map_pre_coGM_def map_pre_coGcoFM_def
    coF_dtor_o_unfold id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF coF0.map_comp0[symmetric]]
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

subsubsection ‹Corecursors›

definition n2m_dtor_corec_coG ::
  "('b ⇒ ('a coG coF + 'c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('a coG coF + 'c, 'a coG + 'b) coGcoFM_pre_coGcoFM) ⇒ 'b ⇒ 'a coG"
  where "n2m_dtor_corec_coG s1 s2 =
    dtor_corec_coG (BNF_Composition.id_bnf o BNF_Composition.id_bnf o
      map_pre_coGM id (id :: unit ⇒ unit)
        (case_sum (map_coF Inl) (dtor_corec_coF (BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGcoFM (id :: unit ⇒ unit) id (map_sum (map_coF Inl) id) o s2))) o
      s1)"

definition n2m_dtor_corec_coG_coF ::
  "('b ⇒ ('a coG coF + 'c, 'a) coGM_pre_coGM) ⇒ ('c ⇒ ('a coG coF + 'c, 'a coG + 'b) coGcoFM_pre_coGcoFM) ⇒ 'c ⇒ 'a coG coF"
  where "n2m_dtor_corec_coG_coF s1 s2 = dtor_corec_coF (BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGcoFM (id :: unit ⇒ unit) (case_sum id (n2m_dtor_corec_coG s1 s2)) id o s2)"

lemma n2m_dtor_corec_coG:
  "dtor_coG o n2m_dtor_corec_coG s1 s2 = BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGM id id (case_sum id (n2m_dtor_corec_coG_coF s1 s2)) o s1"
  unfolding n2m_dtor_corec_coG_def n2m_dtor_corec_coG_coF_def
    map_pre_coG_def map_pre_coF_def map_pre_coGM_def map_pre_coGcoFM_def
    coG_dtor_o_corec
    id_apply comp_id id_comp comp_assoc[symmetric] map_sum.comp map_sum.id
    case_sum_o_inj(1) case_sum_o_map_sum o_case_sum
    rewriteR_comp_comp[OF coG0.map_comp0[symmetric]]
    rewriteR_comp_comp[OF coF0.map_comp0[symmetric]]
    coF.map_comp0[symmetric] coF.map_id0
    coF.dtor_corec_o_map
    rewriteR_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

lemma n2m_dtor_corec_coG_coF:
  "dtor_coF o n2m_dtor_corec_coG_coF s1 s2 = BNF_Composition.id_bnf o BNF_Composition.id_bnf o map_pre_coGcoFM id (case_sum id (n2m_dtor_corec_coG s1 s2)) (case_sum id (n2m_dtor_corec_coG_coF s1 s2)) o s2"
  unfolding n2m_dtor_corec_coG_coF_def map_pre_coF_def map_pre_coGM_def map_pre_coGcoFM_def
    coF_dtor_o_corec id_apply comp_id id_comp comp_assoc
    rewriteL_comp_comp[OF coF0.map_comp0[symmetric]]
    rewriteL_comp_comp[OF type_copy_Rep_o_Abs[OF BNF_Composition.type_definition_id_bnf_UNIV]] ..

subsubsection ‹Coinduction›

lemma n2m_rel_coinduct_coG_coG_coF:
  assumes CIH1: "∀x y. R x y ⟶ BNF_Def.vimage2p (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (rel_pre_coGM P R S) (dtor_coG x) (dtor_coG y)"
    and     CIH2: "∀x y. S x y ⟶ BNF_Def.vimage2p (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (BNF_Composition.id_bnf o BNF_Composition.id_bnf) (rel_pre_coGcoFM P R S) (dtor_coF x) (dtor_coF y)"
  shows "R ≤ rel_coG P ∧ S ≤ rel_coF (rel_coG P)"
  apply (rule context_conjI)
  apply (rule coG.dtor_rel_coinduct[unfolded rel_pre_coG_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF CIH1], THEN vimage2p_mono[OF _ pre_coGM.rel_mono], unfolded vimage2p_def o_apply rel_pre_coGM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])
  apply (rule order_refl)
  apply (rule order_refl)
  apply (rule coF.dtor_rel_coinduct[unfolded rel_pre_coF_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF CIH2], unfolded vimage2p_def o_apply rel_pre_coGcoFM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])

  apply (rule coF.dtor_rel_coinduct[unfolded rel_pre_coF_def id_apply vimage2p_def o_apply])
  apply (erule mp[OF spec2[OF CIH2], THEN vimage2p_mono[OF _ pre_coGcoFM.rel_mono], unfolded vimage2p_def o_apply rel_pre_coGcoFM_def type_definition.Abs_inverse[OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]])
  apply (rule order_refl)
  apply assumption
  apply (rule order_refl)
  done

lemmas n2m_ctor_induct_coG_coG_coF = spec[OF spec[OF spec[OF spec[OF
          n2m_rel_coinduct_coG_coG_coF[of _ "(=)",
            unfolded coG.rel_eq coF.rel_eq le_fun_def le_bool_def all_simps(1,2)[symmetric]]]]]]

(*<*)
end
(*>*)