Theory Recursion_With_Parameters

theory Recursion_With_Parameters
imports BNF_Axiomatization
theory Recursion_With_Parameters
imports "~~/src/HOL/Library/BNF_Axiomatization"
begin

primrec snoc where
  "snoc x [] = [x]"
| "snoc x (y # xs) = y # snoc x xs"

lemma snoc_neq_Nil: "snoc x xs ≠ []"
  by (cases xs; simp)

lemma bi_unique_Grp: "bi_unique (BNF_Def.Grp A f) = inj_on f A"
  unfolding bi_unique_def Grp_def inj_on_def by auto

lemma bi_unique_eq_onp: "bi_unique (eq_onp P)"
  unfolding eq_onp_def bi_unique_def by simp

lemma fun_pred_rel: "pred_fun A B x = rel_fun (eq_onp A) (eq_onp B) x x"
  unfolding pred_fun_def rel_fun_def eq_onp_def by auto

section ‹Input›

declare [[bnf_internals, typedef_overloaded]]

bnf_axiomatization 'a F

bnf_axiomatization 'b V  (* only needed for recursion *)

bnf_axiomatization ('a, 'x) G [wits: "'a ⇒ ('a, 'x) G"]

section ‹Raw Type›

datatype label = F
type_synonym depth = "label list"
datatype 'a shape = Leaf 'a | Node "'a shape F"
datatype 'a shapeV = LeafV 'a | NodeV "'a shapeV V"
datatype 'a raw = Cons "('a shape, 'a raw) G"

abbreviation "un_Leaf u ≡ case u of Leaf x ⇒ x"
abbreviation "un_Node u ≡ case u of Node x ⇒ x"
abbreviation "un_LeafV u ≡ case u of LeafV x ⇒ x"
abbreviation "un_NodeV u ≡ case u of NodeV x ⇒ x"

abbreviation "un_Cons t ≡ case t of Cons x ⇒ x"


section ‹Invariant›

fun invar_shape :: "depth ⇒ 'a shape ⇒ bool" where
  "invar_shape u0 (Leaf u) = (case u0 of [] ⇒ True | _ ⇒ False)"
| "invar_shape u0 (Node f1) = (case u0 of F # u0 ⇒ pred_F (invar_shape u0) f1 | _ ⇒ False)"

lemma invar_shape_induct[consumes 1, case_names Leaf Node, induct pred: invar_shape]: 
assumes i: "invar_shape u0 s"
and leaf: "⋀u. PP [] (Leaf u)" 
and node: "⋀u0 f1. pred_F (invar_shape u0) f1 ⟹ pred_F (PP u0) f1 ⟹ PP (F # u0) (Node f1)"
shows "PP u0 s"
using assms by (induct s arbitrary: u0) (auto simp: Cons pred_F_def split: list.splits label.splits)

fun invar_shapeV :: "depth ⇒ 'a shapeV ⇒ bool" where
  "invar_shapeV u0 (LeafV u) = (case u0 of [] ⇒ True | _ ⇒ False)"
| "invar_shapeV u0 (NodeV f1) = (case u0 of F # u0 ⇒ pred_V (invar_shapeV u0) f1 | _ ⇒ False)"

lemma G_pred_mono: 
"a ≤ a1 ⟹ pred_G p a ≤ pred_G p a1"
  by (simp add: G.pred_mono)

inductive invar :: "depth ⇒ 'a raw ⇒ bool" where
  "pred_G (invar_shape u0) (invar (F # u0)) g ⟹ invar u0 (Cons g)"
monos G_pred_mono

lemmas invar_simps = invar.simps[of _ "Cons _", unfolded simp_thms(39,40) ex_simps raw.inject]

section ‹The Type›

definition "wit x = Cons (wit_G (Leaf x))"

lemma invar_wit: "invar [] (wit x)"
  by (auto simp only:
    wit_def invar_simps invar_shape.simps G.pred_map o_def id_apply G.pred_set
    G.set_map list.case dest: G.wit)


typedef 'a T = "{t :: 'a raw. invar [] t}"
  by (rule exI[of _ "wit undefined"]) (auto simp only: invar_wit)

section ‹Flat and Unflat›

primrec (transfer)
  flat_shape :: "'a F shape ⇒ 'a shape" where
  "flat_shape (Leaf f1) = Node (map_F Leaf f1)"
| "flat_shape (Node f1) = Node (map_F flat_shape f1)"

primrec (transfer)
  flat_shapeV :: "'a V shapeV ⇒ 'a shapeV" where
  "flat_shapeV (LeafV f1) = NodeV (map_V LeafV f1)"
| "flat_shapeV (NodeV f1) = NodeV (map_V flat_shapeV f1)"
    
primrec (nonexhaustive)
   unflat_shape :: "depth ⇒ 'a shape ⇒ 'a F shape" where
  "unflat_shape u0 (Node f1) =
      (case u0 of
        [] ⇒ Leaf (map_F un_Leaf f1)
      | _ # u0 ⇒ Node (map_F (unflat_shape u0) f1))"

primrec (nonexhaustive)
   unflat_shapeV :: "depth ⇒ 'a shapeV ⇒ 'a V shapeV" where
  "unflat_shapeV u0 (NodeV f1) =
      (case u0 of
        [] ⇒ LeafV (map_V un_LeafV f1)
      | _ # u0 ⇒ NodeV (map_V (unflat_shapeV u0) f1))"

primrec (transfer) flat :: "'a F raw ⇒ 'a raw" where
  "flat (Cons g) = Cons (map_G flat_shape flat g)"

primrec unflat :: "depth ⇒ 'a raw ⇒ 'a F raw" where
  "unflat u0 (Cons g) = Cons (map_G (unflat_shape u0) (unflat (F # u0)) g)"


section ‹Constructor and Selector›

definition T :: "('a, 'a F T) G ⇒ 'a T" where
  "T g = Abs_T (Cons (map_G Leaf (flat o Rep_T) g))"

definition un_T :: "'a T ⇒ ('a, 'a F T) G" where
  "un_T t = map_G un_Leaf (Abs_T o unflat []) (un_Cons (Rep_T t))"


section ‹BNF Instance›

lemma invar_shape_map_closed_raw:
  "∀u0. invar_shape u0 (map_shape f u) ⟷ invar_shape u0 u"
  apply (rule shape.induct[of
    "λu. ∀u0. invar_shape u0 (map_shape f u) ⟷ invar_shape u0 u" u])
  apply (auto simp only:
      shape.map invar_shape.simps
      F.pred_map
      o_apply
    elim!: F.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas invar_shape_map_closed =
  spec[OF invar_shape_map_closed_raw]

lemma invar_shapeV_map_closed_raw:
  "∀u0. invar_shapeV u0 (map_shapeV f u) ⟷ invar_shapeV u0 u"
  apply (rule shapeV.induct[of
    "λu. ∀u0. invar_shapeV u0 (map_shapeV f u) ⟷ invar_shapeV u0 u" u])
  apply (auto simp only:
      shapeV.map invar_shapeV.simps
      V.pred_map
      o_apply
    elim!: V.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas invar_shapeV_map_closed =
  spec[OF invar_shapeV_map_closed_raw]

lemma invar_map_closed_raw:
  "∀u0. invar u0 (map_raw f t) ⟷ invar u0 t"
  apply (induct t)
  apply (auto simp only:
      raw.map invar_simps id_apply o_apply
      G.pred_map invar_shape_map_closed
    elim!: G.pred_mono_strong)
  done
lemmas invar_map_closed =
  spec[OF invar_map_closed_raw]


lift_bnf 'a T
  apply (auto simp only:
      invar_map_closed)
  done




section ‹Lemmas about Flat, Unflat, Invar›

lemma invar_shape_depth_iff:
  "invar_shape [] x = (∃a. x = Leaf a)"
  "invar_shape (F # u0) x = (∃y. x = Node y ∧ pred_F (invar_shape u0) y)"
  by (cases x; simp add: F.pred_map)+


lemma invar_shapeV_depth_iff:
  "invar_shapeV [] x = (∃a. x = LeafV a)"
  "invar_shapeV (F # u0) x = (∃y. x = NodeV y ∧ pred_V (invar_shapeV u0) y)"
  by (cases x; simp add: F.pred_map)+


lemma flat_shape_unflat_shape_raw:
  fixes u :: "'a shape"
  shows
  "∀u0. invar_shape (snoc F u0) u ⟶ flat_shape (unflat_shape u0 u) = u"
  apply (rule shape.induct[of
    "λu. ∀u0. invar_shape (snoc F u0) u ⟶ flat_shape (unflat_shape u0 u) = u" u])
  apply (auto simp only:
    unflat_shape.simps flat_shape.simps
    invar_shape.simps F.pred_map F.map_comp
    shape.case invar_shape_depth_iff snoc.simps snoc_neq_Nil
    id_apply o_apply
    intro!: trans[OF F.map_cong_pred F.map_ident]
    elim!: F.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas flat_shape_unflat_shape =
  mp[OF spec[OF flat_shape_unflat_shape_raw]]

lemma flat_shape_unflat_shapeV_raw:
  fixes u :: "'a shapeV"
  shows
  "∀u0. invar_shapeV (snoc F u0) u ⟶ flat_shapeV (unflat_shapeV u0 u) = u"
  apply (rule shapeV.induct[of
    "λu. ∀u0. invar_shapeV (snoc F u0) u ⟶ flat_shapeV (unflat_shapeV u0 u) = u" u])
  apply (auto simp only:
    unflat_shapeV.simps flat_shapeV.simps
    invar_shapeV.simps V.pred_map V.map_comp
    shapeV.case invar_shapeV_depth_iff snoc.simps snoc_neq_Nil
    id_apply o_apply
    intro!: trans[OF V.map_cong_pred V.map_ident]
    elim!: V.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas flat_shape_unflat_shapeV =
  mp[OF spec[OF flat_shape_unflat_shapeV_raw]]

lemma unflat_shape_flat_shape_raw:
  fixes u :: "'a F shape"
  shows
  "∀u0. invar_shape u0 u ⟶ unflat_shape u0 (flat_shape u) = u"
  apply (rule shape.induct[of
    "λu. ∀u0. invar_shape u0 u ⟶ unflat_shape u0 (flat_shape u) = u" u])
  apply (auto simp only:
      unflat_shape.simps flat_shape.simps invar_shape.simps
      F.pred_map F.map_comp F.pred_True
      shape.case
      id_apply o_apply refl
    intro!: trans[OF F.map_cong_pred F.map_ident]
    elim!: F.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas unflat_shape_flat_shape =
  mp[OF spec[OF unflat_shape_flat_shape_raw]]

lemma unflat_shapeV_flat_shapeV_raw:
  fixes u :: "'a V shapeV"
  shows
  "∀u0. invar_shapeV u0 u ⟶ unflat_shapeV u0 (flat_shapeV u) = u"
  apply (rule shapeV.induct[of
    "λu. ∀u0. invar_shapeV u0 u ⟶ unflat_shapeV u0 (flat_shapeV u) = u" u])
  apply (auto simp only:
      unflat_shapeV.simps flat_shapeV.simps invar_shapeV.simps
      V.pred_map V.map_comp V.pred_True
      shapeV.case
      id_apply o_apply refl
    intro!: trans[OF V.map_cong_pred V.map_ident]
    elim!: V.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas unflat_shapeV_flat_shapeV =
  mp[OF spec[OF unflat_shapeV_flat_shapeV_raw]]

lemma invar_shape_flat_shape_raw:
  fixes u :: "'a F shape"
  shows
  "∀u0. invar_shape u0 u ⟶ invar_shape (snoc F u0) (flat_shape u)"
  apply (rule shape.induct[of
    "λu. ∀u0. invar_shape u0 u ⟶ invar_shape (snoc F u0) (flat_shape u)" u])
  apply (auto simp only:
      flat_shape.simps invar_shape.simps snoc.simps
      F.pred_map F.pred_True
      id_apply o_apply
    elim!: F.pred_mono_strong
    intro: F.pred_mono_strong[OF iffD2[OF fun_cong[OF F.pred_True] TrueI]]
    split: list.splits label.splits)
  done


lemmas invar_shape_flat_shape =
  mp[OF spec[OF invar_shape_flat_shape_raw]]

lemma invar_shapeV_flat_shapeV_raw:
  fixes u :: "'a V shapeV"
  shows
  "∀u0. invar_shapeV u0 u ⟶ invar_shapeV (snoc F u0) (flat_shapeV u)"
apply (rule shapeV.induct[of
    "λu. ∀u0. invar_shapeV u0 u ⟶ invar_shapeV (snoc F u0) (flat_shapeV u)" u])
  apply (auto simp only:
      flat_shapeV.simps invar_shapeV.simps snoc.simps
      V.pred_map V.pred_True
      id_apply o_apply
    elim!: V.pred_mono_strong
    intro: V.pred_mono_strong[OF iffD2[OF fun_cong[OF V.pred_True] TrueI]]
    split: list.splits label.splits)
  done

lemmas invar_shapeV_flat_shapeV =
  mp[OF spec[OF invar_shapeV_flat_shapeV_raw]]

lemma invar_flat_raw: "∀u0. invar u0 x ⟶ invar (snoc F u0) (flat x)"
  apply (induct x)
  apply (auto simp only:
      flat.simps invar_simps snoc.simps[symmetric] invar_shape_flat_shape id_apply o_apply G.pred_map
    elim!: G.pred_mono_strong)
  done


lemmas invar_flat = mp[OF spec[OF invar_flat_raw]]

lemma invar_shape_unflat_shape_raw:
  fixes u :: "'a shape"
  shows
  "∀u0. invar_shape (snoc F u0) u ⟶ invar_shape u0 (unflat_shape u0 u)"
  apply (rule shape.induct[of
    "λu. ∀u0. invar_shape (snoc F u0) u ⟶ invar_shape u0 (unflat_shape u0 u)" u])
  apply (auto simp only:
      unflat_shape.simps invar_shape.simps snoc.simps snoc_neq_Nil
      F.pred_map id_apply o_apply refl
    elim!: F.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas invar_shape_unflat_shape =
  mp[OF spec[OF invar_shape_unflat_shape_raw]]

lemma invar_shapeV_unflat_shapeV_raw:
  fixes u :: "'a shapeV"
  shows
  "∀u0. invar_shapeV (snoc F u0) u ⟶ invar_shapeV u0 (unflat_shapeV u0 u)"
  apply (rule shapeV.induct[of
    "λu. ∀u0. invar_shapeV (snoc F u0) u ⟶ invar_shapeV u0 (unflat_shapeV u0 u)" u])
  apply (auto simp only:
      unflat_shapeV.simps invar_shapeV.simps snoc.simps snoc_neq_Nil
      V.pred_map id_apply o_apply refl
    elim!: V.pred_mono_strong
    split: list.splits label.splits)
  done

lemmas invar_shapeV_unflat_shapeV =
  mp[OF spec[OF invar_shapeV_unflat_shapeV_raw]]

lemma invar_unflat_raw: "∀u0. invar (snoc F u0) t ⟶ invar u0 (unflat u0 t)"
  apply (induct t)
  apply (auto simp only:
      unflat.simps invar_simps snoc.simps invar_shape_unflat_shape id_apply o_apply G.pred_map
    elim!: G.pred_mono_strong)
  done

lemmas invar_unflat = mp[OF spec[OF invar_unflat_raw]]

lemma flat_unflat_raw: "∀u0. invar (snoc F u0) t ⟶ flat (unflat u0 t) = t"
  apply (induct t)
  apply (auto simp only:
      unflat.simps flat.simps invar_simps snoc.simps
      flat_shape_unflat_shape id_apply o_apply G.pred_map G.map_comp
    intro!: trans[OF G.map_cong_pred G.map_ident]
    elim!: G.pred_mono_strong)
  done


lemmas flat_unflat = mp[OF spec[OF flat_unflat_raw]]

lemma unflat_flat_raw: "∀u0. invar u0 t ⟶ unflat u0 (flat t) = t"
  apply (induct t)
  apply (auto simp only:
      unflat.simps flat.simps invar_simps unflat_shape_flat_shape id_apply o_apply G.pred_map G.map_comp
    intro!: trans[OF G.map_cong_pred G.map_ident]
    elim!: G.pred_mono_strong)
  done


lemmas unflat_flat = mp[OF spec[OF unflat_flat_raw]]


section ‹Constructor is Bijection›

lemma un_T_T: "un_T (T x) = x"
  unfolding T_def un_T_def
  apply (subst Abs_T_inverse)
   apply (auto simp only:
       invar_simps invar_shape.simps list.case id_apply o_apply
       snoc.simps(1)[of F, symmetric]
       G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
    intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
  apply (auto simp only:
      raw.case shape.case Rep_T_inverse o_apply
      G.map_comp G.map_ident Rep_T[unfolded mem_Collect_eq] unflat_flat
    intro!: trans[OF G.map_cong G.map_ident]) []
  done


lemma T_un_T: "T (un_T x) = x"
  unfolding T_def un_T_def G.map_comp o_def
  apply (rule iffD1[OF Rep_T_inject])
  apply (subst Abs_T_inverse)
   apply (auto simp only:
       invar_simps invar_shape.simps list.case id_apply o_apply
       snoc.simps(1)[of F, symmetric]
       G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
     intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
  apply (insert Rep_T[simplified, of x])
  apply (rule raw.exhaust[of "Rep_T x"])
  apply (auto simp only:
      raw.case shape.case invar_simps invar_shape_depth_iff
       snoc.simps(1)[of F, symmetric]
      G.pred_map Abs_T_inverse invar_unflat flat_unflat id_apply o_apply mem_Collect_eq
    intro!: trans[OF G.map_cong_pred G.map_ident]
    elim!: G.pred_mono_strong) []
  done



section ‹Characteristic Theorems›

subsection ‹map›

lemma flat_shape_map:
  "map_shape f (flat_shape u) = flat_shape (map_shape (map_F f) u)"
  apply (rule shape.induct[of
    "λu. map_shape f (flat_shape u) = flat_shape (map_shape (map_F f) u)" u])
  apply (auto simp only:
      shape.map flat_shape.simps F.map_comp o_apply
    intro!: F.map_cong0)
  done

lemma map_raw_flat: "map_raw f (flat t) = flat (map_raw (map_F f) t)"
  apply (induct t)
  apply (auto simp only:
      raw.map flat.simps G.map_comp flat_shape_map o_apply
    intro!: G.map_cong0)
  done

lemma map_T: "map_T f (T t) = T (map_G f (map_T (map_F f)) t)"
  unfolding map_T_def T_def o_apply
  apply (subst Abs_T_inverse)
   apply (auto simp only:
       invar_simps invar_shape.simps list.case id_apply o_apply
       snoc.simps(1)[of F, symmetric]
       G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
     intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
  apply (auto simp only:
      raw.map shape.map G.map_comp o_apply mem_Collect_eq
     invar_map_closed Abs_T_inverse Rep_T[unfolded mem_Collect_eq] map_raw_flat
    intro!: arg_cong[of _ _ "λx. Abs_T (raw.Cons x)"] G.map_cong0) []
  done


subsection ‹set›

lemma flat_shape_set:
  fixes u :: "'a F shape"
  shows
  "set_shape (flat_shape u) = UNION (set_shape u) set_F"
  apply (rule shape.induct[of
    "λu. set_shape (flat_shape u) = UNION (set_shape u) set_F" u])
  apply (auto simp only:
      flat_shape.simps shape.set F.set_map
      UN_simps UN_singleton UN_insert UN_empty UN_empty2 UN_Un UN_Un_distrib Un_ac Un_empty_left
    cong: SUP_cong)
  done

lemma set_raw_flat:
  "set_raw (flat t) = UNION (set_raw t) set_F"
  apply (induct t)
  apply (auto simp only:
      flat.simps raw.set shape.set G.set_map flat_shape_set
      UN_simps UN_Un UN_Un_distrib Un_ac
    cong: SUP_cong)
  done

lemma set_T: "set_T (T g) = set1_G g ∪
  (⋃(set_F ` (⋃(set_T ` (set2_G g)))))"
  unfolding set_T_def T_def o_apply
  apply -
  apply (subst Abs_T_inverse)
   apply (auto simp only:
       invar_simps invar_shape.simps list.case id_apply o_apply
       snoc.simps(1)[of F, symmetric]
       G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
     intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
  apply (auto simp only:
      raw.set shape.set G.set_map set_raw_flat o_apply
        UN_simps UN_singleton UN_empty2 UN_Un UN_Un_distrib Un_ac Un_empty_left
    cong: SUP_cong) []
  done


subsection ‹rel›

lemma flat_shape_rel_raw:
  "(∀u0 u'. invar_shape u0 u ⟶ invar_shape u0 u' ⟶ rel_shape R (flat_shape u) (flat_shape u') ⟶
     rel_shape (rel_F R) u u')"
  apply (rule shape.induct[of
    "λu. ∀u0 u'. invar_shape u0 u ⟶ invar_shape u0 u' ⟶ rel_shape R (flat_shape u) (flat_shape u') ⟶
    rel_shape (rel_F R) u u'"
    u])
   apply (auto 0 4 simp only:
     invar_shape.simps flat_shape.simps shape.rel_inject
     invar_shape_depth_iff ball_simps id_apply
     F.rel_map pred_F_def F.set_map
     elim!: F.rel_mono_strong
     split: list.splits label.splits)
  done

lemma flat_shape_rel:
  "invar_shape u0 u ⟹ invar_shape u0 u' ⟹
    rel_shape R (flat_shape u) (flat_shape u') = rel_shape (rel_F R) u u'"
  apply (rule iffI[rotated, OF rel_funD[OF flat_shape.transfer]], assumption)
  apply (rule mp[OF mp[OF mp[OF spec[OF spec[OF flat_shape_rel_raw]]]]]; assumption)
  done

lemma rel_raw_flat_raw:
  "∀t' u0. invar u0 t ⟶ invar u0 t' ⟶
   rel_raw R (flat t) (flat t') ⟶ rel_raw (rel_F R) t t'"
  apply (induct t)
  apply (rule allI)
  apply (case_tac t')
  apply (auto simp only:
      invar_simps flat.simps raw.rel_inject G.rel_map G.pred_set flat_shape_rel G.set_map ball_simps id_apply
    elim!: G.rel_mono_strong)
  done

lemma rel_raw_flat:
  "invar u0 t ⟹ invar u0 t' ⟹
   rel_raw R (flat t) (flat t') = rel_raw (rel_F R) t t'"
  apply (rule iffI[rotated, OF rel_funD[OF flat.transfer]], assumption)
  apply (rule mp[OF mp[OF mp[OF spec[OF spec[OF rel_raw_flat_raw]]]]]; assumption)
  done

lemma rel_T: "rel_T R (T g) (T g') = rel_G R (rel_T (rel_F R)) g g'"
  unfolding rel_T_def T_def vimage2p_def
  apply (subst (1 2) Abs_T_inverse)
   apply (auto simp only:
       invar_simps invar_shape.simps list.case id_apply o_apply
       snoc.simps(1)[of F, symmetric]
       G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
     intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) [2]
  apply (simp only:
    raw.rel_inject G.rel_map shape.rel_inject o_apply
    rel_raw_flat[OF Rep_T[unfolded mem_Collect_eq] Rep_T[unfolded mem_Collect_eq]])
  done

section ‹Recursion›

(*normal datatype recursor
  (('b, 'a) G ⇒ 'a) ⇒
  'b T ⇒ 'a
*)

(*generalized recursor
  (∀'a. ('a D, 'b F R) G ⇒ 'b R) ⇒
  (∀'a. 'a D F ⇒ 'a F D) ⇒
  (∀'a. 'a D T ⇒ 'b R) 
*)


bnf_axiomatization 'a R1 
bnf_axiomatization 'a R2
type_synonym 'a R = "'a R1 ⇒ 'a R2"

abbreviation "pred_R B ≡ pred_fun (pred_R1 B) (pred_R2 B)"
abbreviation "rel_R B ≡ rel_fun (rel_R1 B) (rel_R2 B)"
abbreviation "map_R b1 b2 r12 ≡ map_R2 b2 o r12 o map_R1 b1"

bnf_axiomatization 'a D

consts defobj :: "('a D, 'a V R) G ⇒ 'a R"
consts argobj :: "'a D F ⇒ 'a V D"

axiomatization where
  defobj_transfer: "⋀A.
    bi_unique A ⟹ 
    rel_fun (rel_G (rel_D A) (rel_R (rel_V A))) (rel_R A) defobj defobj" 
and
  argobj_transfer: "⋀A.
    bi_unique A ⟹
    rel_fun (rel_F (rel_D A)) (rel_D (rel_V A)) argobj argobj"

lemma eq_onpE: "eq_onp R x y ⟹ (R x ⟹ x = y ⟹ thesis) ⟹ thesis"
  unfolding eq_onp_def by auto

lemma eq_onpI: "R x ⟹ x = y ⟹ eq_onp R x y"
  unfolding eq_onp_def by auto

lemma rel_fun_mono_strong:
  "rel_fun X A f g ⟹ (⋀x y. Y x y ⟹ X x y) ⟹
   (⋀x y. (x, y) ∈ {(f a, g b) | a b. Y a b} ⟹ A x y ⟹ B x y) ⟹ rel_fun Y B f g"
  unfolding rel_fun_def by force
  
lemma defobj_invar: "pred_fun (pred_G (pred_D A) (pred_R (pred_V A))) (pred_R A) defobj"
  unfolding fun_pred_rel G.rel_eq_onp[symmetric] D.rel_eq_onp[symmetric]
    R1.rel_eq_onp[symmetric] R2.rel_eq_onp[symmetric] V.rel_eq_onp[symmetric]
  apply (rule rel_fun_mono_strong[OF defobj_transfer[OF bi_unique_eq_onp, of A]])
   apply (erule G.rel_mono_strong)
    apply assumption
   apply (erule eq_onpE)
   apply hypsubst
   apply assumption
  apply (erule CollectE exE conjE prod.inject[THEN iffD1, elim_format])+
  apply hypsubst
  apply (drule iffD1[OF fun_cong[OF fun_cong[OF G.rel_eq]] G.rel_mono_strong])
    apply (erule iffD1[OF fun_cong[OF fun_cong[OF D.rel_eq]] D.rel_mono_strong])
      apply (erule eq_onp_to_eq)
     apply (erule eq_onp_to_eq)
  apply hypsubst
  apply (erule eq_onpI)
  apply (rule refl)
  done

  
lemma argobj_invar: 
"pred_fun (pred_F (pred_D A)) (pred_D (pred_V A)) argobj"
  unfolding fun_pred_rel F.rel_eq_onp[symmetric] V.rel_eq_onp[symmetric] D.rel_eq_onp[symmetric]
  by (rule argobj_transfer; rule bi_unique_eq_onp)


(* variant of the above: *)
lemma defobj_pred: 
assumes "pred_G (pred_D A) (pred_R (pred_V A)) x"
shows "(pred_R A) (defobj x)"
using assms defobj_invar unfolding pred_fun_def by auto

lemma argobj_pred: 
assumes "pred_F (pred_D A) x" 
shows "(pred_D (pred_V A)) (argobj x)"
using assms argobj_invar by auto


lemma R1_map_cong_id: 
  assumes "⋀ a. a ∈ set_R1 r ⟹ ff a = a"
  shows "map_R1 ff r = r"
  by (metis R1.map_cong0 R1.map_id0 assms id_apply)

lemma V_map_cong_id: 
  assumes "⋀ a. a ∈ set_V r ⟹ ff a = a"
  shows "map_V ff r = r"
  by (metis V.map_cong0 V.map_id0 assms id_apply)

lemma defobj_natural:
assumes A1: "⋃(set_D ` set1_G x) ⊆ A"
and A2: "⋀ rv12 rv1. rv12 ∈ set2_G x ∧ ⋃ (set_V ` (set_R1 rv1)) ⊆ A ⟹ 
                      ⋃ (set_V ` (set_R2 (rv12 rv1))) ⊆ A"
and f: "bij_betw f A B" and g: "bij_betw g B A" 
and gf: "⋀ a. a ∈ A ⟹ g (f a) = a" and fg: "⋀ b. b ∈ B ⟹ f (g b) = b"
and q1: "set_R1 q1 ⊆ B"
shows "map_R2 f (defobj x (map_R1 g q1)) = 
       defobj (map_G (map_D f) (map_R (map_V g) (map_V f)) x) q1"
(is "_ = defobj ?y q1")
proof-  
  let ?K1 = "eq_onp (λd. set_D d ⊆ A)"
  let ?K2 = "eq_onp (λrv12. ∀ rv1. rv12 ∈ set2_G x ∧ ⋃ (set_V ` (set_R1 rv1)) ⊆ A 
                     ⟶  ⋃ (set_V ` (set_R2 (rv12 rv1))) ⊆ A)"
  have 0: "rel_G ?K1 ?K2 x x" 
    unfolding G.rel_eq_onp 
    unfolding eq_onp_def pred_G_def using A1 A2 by auto
  define y where "y ≡ ?y" 
  have 1: "rel_G (rel_D (BNF_Def.Grp A f)) 
              (rel_R (rel_V (BNF_Def.Grp A f))
              ) x y" 
    unfolding y_def D.rel_Grp V.rel_Grp G.rel_map
    unfolding rel_fun_def apply simp
    unfolding R2.rel_map BNF_Def.Grp_def 
    apply(rule G.rel_mono_strong0[OF 0]) unfolding eq_onp_def
  proof auto
    fix rv12 rv1 qv1
    assume "rv12 ∈ set2_G x"
    and a: "∀rv1.
          (⋃x∈set_R1 rv1. set_V x) ⊆ A ⟶
          (⋃x∈set_R2 (rv12 rv1). set_V x) ⊆ A"
    and "rel_R1 (λa b. b = map_V f a ∧ set_V a ⊆ A) rv1 qv1"
    hence "rel_R1 (BNF_Def.Grp {v. set_V v ⊆ A} (map_V f)) rv1 qv1" 
      unfolding BNF_Def.Grp_def by auto
    hence qv1: "qv1 = map_R1 (map_V f) rv1" and s: "set_R1 rv1 ⊆ {v. set_V v ⊆ A}" 
      unfolding R1.rel_Grp unfolding BNF_Def.Grp_def by auto
    have c: "map_R1 (map_V g) qv1 = rv1" 
      unfolding qv1 R1.map_comp V.axiom2_V[symmetric]
      using s gf by (intro R1_map_cong_id V_map_cong_id) auto     
    have d: "(⋃x∈set_R1 rv1. set_V x) ⊆ A" using s by auto
    have e: "rel_R2 (eq_onp (λv . set_V v ⊆ A)) (rv12 rv1) (rv12 rv1)"
      unfolding R2.rel_eq_onp
      unfolding eq_onp_def pred_R2_def using a d by auto 
    
    show "rel_R2 (λx y. map_V f y = map_V f x ∧ set_V x ⊆ A)
        (rv12 rv1) (rv12 (map_R1 (map_V g) qv1))"
      unfolding c
      apply(rule R2.rel_mono_strong0[OF e])
      unfolding eq_onp_def by auto
    qed
  have 2: "rel_R (BNF_Def.Grp A f) (defobj x) (defobj y)"  
    apply(rule rel_funD[OF defobj_transfer 1]) 
    using f unfolding bij_betw_def by (simp add: bi_unique_Grp)
  have "rel_R2 (BNF_Def.Grp A f) (defobj x (map_R1 g q1)) (defobj y q1)"  
    apply(rule 2[unfolded rel_fun_def, rule_format])
    unfolding rel_fun_def R1.rel_Grp unfolding BNF_Def.Grp_def apply auto
    unfolding R1.set_map R1.map_comp 
     apply(rule R1_map_cong_id[symmetric])
     using q1 fg g unfolding bij_betw_def by auto
   hence "map_R2 f (defobj x (map_R1 g q1)) = defobj y q1"
   unfolding rel_fun_def R1.rel_Grp R2.rel_Grp 
    unfolding BNF_Def.Grp_def o_def by (auto intro!: R2.map_cong)
  thus ?thesis unfolding y_def .
qed

(* Variant of defobj_natural with B = UNIV; the important
advantage being that we obtain full function equality on the codomain R
(there is no assumption on the input q1) *)
lemma defobj_natural_UNIV:
assumes A1: "⋃(set_D ` set1_G x) ⊆ A"
and A2: "⋀ rv12 rv1. rv12 ∈ set2_G x ∧ ⋃ (set_V ` (set_R1 rv1)) ⊆ A ⟹ 
                      ⋃ (set_V ` (set_R2 (rv12 rv1))) ⊆ A"
and f: "inj_on f A" and g: "inj g" "range g ⊆ A"
and gf: "⋀ a. a ∈ A ⟹ g (f a) = a" and fg: "⋀ b. f (g b) = b"
shows "map_R g f (defobj x) = 
       defobj (map_G (map_D f) (map_R (map_V g) (map_V f)) x)"
    apply (rule ext) apply simp
  apply(rule defobj_natural[of _ _ _ UNIV])
  using assms unfolding bij_betw_def inj_on_def 
  by auto (smt UN_I range_eqI UNIV_I image_eqI subsetCE subset_trans)+


lemma argobj_natural:
  "inj_on a (⋃(set_D ` set_F x)) ⟹
  argobj (map_F (map_D a) x) = map_D (map_V a) (argobj x)"
  using rel_funD[OF argobj_transfer, of "BNF_Def.Grp (⋃(set_D ` set_F x)) a"]
  unfolding F.rel_Grp V.rel_Grp D.rel_Grp bi_unique_Grp
  by (auto simp add: Grp_def)

lemma argobj_flat_shape_natural: 
fixes x :: "('a V shapeV) D F"
  shows
    "pred_F (pred_D (invar_shapeV u)) x ⟹
     argobj (map_F (map_D flat_shapeV) x) =
     map_D (map_V flat_shapeV) (argobj x)"
apply(rule argobj_natural)
unfolding pred_F_def pred_D_def inj_on_def  
by simp (metis unflat_shapeV_flat_shapeV)

lemma defobj_flat_shape_natural: 
fixes x :: "(('a V shapeV) D, ('a V shapeV V) R) G"
assumes q1: "⋀ sh. sh ∈ set_R1 q1 ⟹ invar_shapeV (snoc F u) sh"   
and pr: "pred_G (pred_D (invar_shapeV u)) 
        (pred_R (pred_V (invar_shapeV u))) x"
shows   
"defobj (map_G (map_D flat_shapeV) 
              (map_R (map_V (unflat_shapeV u)) (map_V flat_shapeV)) x) q1 = 
 map_R2 flat_shapeV (defobj x (map_R1 (unflat_shapeV u) q1))"
 apply(rule defobj_natural[symmetric, of _ "{sh . invar_shapeV u sh}" _
   "{sh . invar_shapeV (snoc F u) sh} "])
        apply auto
  using assms unfolding pred_G_def pred_D_def pred_V_def 
        apply (auto simp: pred_R1_def pred_R2_def)
      apply (smt UN_subset_iff mem_Collect_eq subsetCE)
  unfolding bij_betw_def inj_on_def apply auto
  apply (metis unflat_shapeV_flat_shapeV)
  using invar_shapeV_flat_shapeV apply blast
  apply (metis CollectI flat_shape_unflat_shapeV image_eqI invar_shapeV_unflat_shapeV)
      apply (metis flat_shape_unflat_shapeV)
  using invar_shapeV_unflat_shapeV apply blast
  apply (metis CollectI image_iff invar_shapeV_flat_shapeV_raw unflat_shapeV_flat_shapeV_raw)
  using unflat_shapeV_flat_shapeV apply blast
  using flat_shape_unflat_shapeV by blast
  
primrec f_shape :: "'a D shape ⇒ 'a shapeV D" where
  "f_shape (Leaf a) = map_D LeafV a"
| "f_shape (Node f) = map_D NodeV (argobj (map_F f_shape f))"

primrec f_raw :: "'a D raw ⇒ 'a shapeV R" where
  "f_raw (Cons x) = defobj (map_G f_shape (map_R NodeV un_NodeV o f_raw) x)"

definition f :: "'a D T ⇒ 'a R" where
  "f t = map_R LeafV un_LeafV (f_raw (Rep_T t))"
  
lemma f_def2: "f = map_R LeafV un_LeafV o f_raw o Rep_T"
unfolding f_def[abs_def] by auto

lemma invar_shape_f_shape:
assumes "invar_shape u0 u" shows "pred_D (invar_shapeV u0) (f_shape u)"
using assms apply (induct) 
  apply (auto simp add: F.pred_map D.pred_map D.pred_True intro!: argobj_pred cong: D.pred_cong
    elim: F.pred_mono_strong)+
  done


lemma f_shape_flat_shape: 
assumes "invar_shape u x" 
shows "f_shape (flat_shape x) = map_D flat_shapeV (f_shape (map_shape argobj x))"
using assms proof induct 
  case Leaf
  thus ?case
  apply simp unfolding D.map_comp o_def apply simp
  unfolding o_def[symmetric] D.map_comp[symmetric]
  apply(rule D.map_cong)
  apply simp_all unfolding F.map_comp o_def apply simp
  apply(rule argobj_natural) 
unfolding inj_on_def by auto
next
  case (Node u0 f1)
  hence 1: 
    "map_F (λa. f_shape (flat_shape a)) f1 = 
     map_F (map_D flat_shapeV o (λa. f_shape (map_shape argobj a))) f1"
  by (intro F.map_cong_pred) auto
  show ?case apply simp
  unfolding D.map_comp o_def apply simp
  unfolding o_def[symmetric] D.map_comp[symmetric]
  apply(rule D.map_cong) apply simp_all
  unfolding F.map_comp o_def unfolding 1 unfolding F.map_comp[symmetric]
  apply(rule argobj_flat_shape_natural[of u0])
  using Node unfolding F.pred_map
  unfolding pred_F_def pred_D_def
  by simp (meson invar_shape_f_shape invar_shape_map_closed pred_D_def)
qed


lemma invar_shapeV_set_V_un_NodeV: 
assumes "invar_shapeV (F # u0) ss" and "s ∈ set_V (un_NodeV ss)"
shows "invar_shapeV u0 s"
using assms by (metis invar_shapeV_depth_iff(2) pred_V_def shapeV.simps(6))

lemma invar_f_raw:
assumes "invar u0 (x::'a D raw)"
shows "pred_R (invar_shapeV u0) (f_raw x :: 'a shapeV R)"
using assms proof induct
  case (1 u0 g)
  show ?case unfolding f_raw.simps
    apply(rule defobj_pred) unfolding G.pred_map
    apply (rule G.pred_mono_strong[OF 1])
    apply (simp add: invar_shape_f_shape)
     apply auto
     unfolding R2.pred_map 
     by (smt R1.pred_set R1.set_map axiom10_R2 image_iff 
        invar_shapeV_depth_iff(2) o_apply shapeV.case(2))
qed


(* D, the previous lemma was now split in the next two: *)
lemma invar_f_raw_map_raw_argobj:
assumes "invar u0 x"
shows "pred_R (invar_shapeV u0) ((f_raw :: 'a V D raw ⇒ 'a V shapeV R) 
              (map_raw argobj x))"
using invar_f_raw
  [OF assms[unfolded invar_map_closed_raw[rule_format, symmetric, of u0 x argobj]]] .

lemma un_NodeV_flat_shapeV_Nil:
assumes "invar_shapeV [] vv"
shows "un_NodeV (flat_shapeV vv) = map_V LeafV (un_LeafV vv)" 
by (metis (no_types, lifting) assms flat_shapeV.simps(1) 
   invar_shapeV_depth_iff(1) shapeV.simps(5) shapeV.simps(6))

lemma un_NodeV_flat_shapeV:
assumes "invar_shapeV (F # u0) vv"
shows "un_NodeV (flat_shapeV vv) = map_V flat_shapeV (un_NodeV vv)" 
  by (metis assms flat_shapeV.simps(2) invar_shapeV_depth_iff(2) shapeV.simps(6))

lemma map_raw_Rep_T: "map_raw ff (Rep_T t) = Rep_T (map_T ff t)"
  by (simp only: map_T_def invar_map_closed_raw
    Abs_T_inverse[unfolded mem_Collect_eq] Rep_T[unfolded mem_Collect_eq] o_apply)

lemma R_map_comp: 
"map_R (ff1 ∘ gg1) (gg2 o ff2) = map_R gg1 gg2 o map_R ff1 ff2"
  apply(rule ext, auto)
  by (metis (no_types, hide_lams) R1.map_comp0 R2.map_comp0 fcomp_assoc fcomp_comp)

lemma defobj_natural_eq_onp:
assumes "(rel_G (rel_D (eq_onp PP)) (rel_R (rel_V (eq_onp PP)))) g g'"
shows "(rel_R (eq_onp PP)) (defobj g) (defobj g')"
using defobj_transfer[of "eq_onp PP"] 
  by (metis assms bi_unique_eq_onp rel_funE)

lemma rel_R1_pred_R1_refl: 
assumes "rel_R1 (λ a b. PP a ∧ a = b) x y"
shows "pred_R1 PP x ∧ y = x"
by (smt R1.pred_rel R1.rel_eq R1.rel_mono_strong assms eq_onp_def)
   
lemma defobj_natural_eq_onp_pred: 
assumes 1: "rel_G (eq_onp (pred_D PP)) (rel_R (eq_onp (pred_V PP))) g g'"
and 2: "pred_R1 PP q1"
shows "defobj g q1 = defobj g' q1"
proof-
  have "(rel_R (eq_onp PP)) (defobj g) (defobj g')"
  apply(rule defobj_natural_eq_onp)
    using 1 unfolding V.rel_eq_onp D.rel_eq_onp pred_R1_def rel_fun_def by auto
  thus ?thesis using 2 unfolding rel_fun_def
    unfolding R1.rel_eq_onp R2.rel_eq_onp unfolding eq_onp_def by auto
qed

lemma pred_R1_invar_shapeV_NodeV:
assumes "pred_R1 (pred_V (invar_shapeV u)) x"
shows "pred_R1 (invar_shapeV (F # u)) (map_R1 NodeV x)"
  by (smt R1.set_map assms axiom10_R1 image_iff invar_shapeV_depth_iff(2))

lemma unflat_shapeV_Cons_o_NodeV:
"unflat_shapeV (F # u0) ∘ NodeV = NodeV ∘ map_V (unflat_shapeV u0)"
  by (rule ext, auto)
 
lemma f_raw_flat:
assumes "invar u0 (r::'a D F raw)" and "pred_R1 (invar_shapeV (snoc F u0)) q1"
shows "(f_raw (flat r)::'a shapeV R) q1 = 
        map_R (unflat_shapeV u0) flat_shapeV (f_raw (map_raw argobj r)) q1"
using assms proof (induct arbitrary: q1)
  case (1 u0 g q1) 
  hence  q1: "pred_R1 (invar_shapeV (snoc F u0)) q1"   
  and IH1: "∀sh∈set1_G g. invar_shape u0 sh" and 
  IH2: "⋀r. r ∈ set2_G g ⟶ invar (F # u0) r ∧
               (∀ q1. pred_R1 (invar_shapeV (F # (snoc F u0))) q1 ⟶
              (f_raw (flat r)::'a shapeV R) q1 = 
             map_R (unflat_shapeV (F # u0)) 
                   flat_shapeV (f_raw (map_raw argobj r)) q1)"  
    unfolding pred_G_def by auto
  (* Preparations: *)
  let ?x = "map_G (f_shape o map_shape argobj)
                  (map_R NodeV un_NodeV o f_raw o map_raw argobj) g :: 
            ('a V shapeV D, 'a V shapeV V R) G" 
  let ?y = "map_G (map_shape argobj) (map_raw argobj) g"
  (* *) 
  have x: "pred_G (pred_D (invar_shapeV u0))
                  (pred_R (pred_V (invar_shapeV u0))) ?x" 
    using IH1 IH2 q1 unfolding pred_G_def pred_D_def pred_V_def 
    apply (auto simp: G.set_map pred_R1_def pred_R2_def R1.set_map R2.set_map)
     apply (meson D.pred_set invar_shape_f_shape invar_shape_map_closed)
    apply(rule invar_shapeV_set_V_un_NodeV) apply auto
    apply(rule invar_f_raw_map_raw_argobj[unfolded pred_fun_def pred_R1_def pred_R2_def, 
        simplified, rule_format])
      by (auto simp: R1.set_map pred_V_def) 
  (* The diagram chase: *)
  have "(f_raw (flat (raw.Cons g))::'a shapeV R) q1 =
         f_raw (Cons (map_G flat_shape flat g)) q1"
    unfolding flat.simps ..
  also have "… = defobj (map_G (f_shape ∘ flat_shape)
                                (map_R NodeV un_NodeV ∘ f_raw ∘ flat)
                                g) q1" 
    unfolding f_raw.simps G.map_comp ..
  also have "… = 
    defobj (map_G (map_D flat_shapeV o f_shape o map_shape argobj)
                  (map_R (unflat_shapeV (F # u0) o NodeV) (un_NodeV ∘ flat_shapeV) o f_raw o map_raw argobj)
                  g) q1" 
    apply(rule defobj_natural_eq_onp_pred[OF _ q1])
    unfolding G.rel_map unfolding eq_onp_def pred_D_def apply auto 
    apply(rule G.rel_refl_strong) using IH1 f_shape_flat_shape apply auto
     apply(rule invar_shape_f_shape[unfolded pred_D_def, simplified, rule_format]) 
      apply(rule invar_shape_flat_shape) apply auto
      using IH1 IH2 q1 f_shape_flat_shape 
     apply (auto simp: rel_fun_def fun_eq_iff)
      unfolding R2.rel_map apply auto
      apply(drule rel_R1_pred_R1_refl) apply auto
      apply(drule pred_R1_invar_shapeV_NodeV) apply auto
      unfolding pred_R1_def pred_V_def R1.map_comp[symmetric] apply auto
      unfolding R2.rel_map apply auto
      apply(rule R2.rel_refl_strong) apply auto 
      apply(rule invar_shapeV_set_V_un_NodeV, auto)
      apply(rule invar_shapeV_flat_shapeV[of "F # u0", simplified])
      apply(rule invar_f_raw[unfolded pred_R1_def pred_R2_def, 
             simplified, rule_format], auto)
      by (auto simp: invar_map_closed_raw invar_shapeV_unflat_shapeV_raw R1.map_comp 
          R1.set_map pred_V_def V.set_map)
  also have "… = 
    defobj (map_G (map_D flat_shapeV o f_shape o map_shape argobj)
                  (map_R (unflat_shapeV (F # u0) o NodeV) 
                           (map_V flat_shapeV o un_NodeV) o f_raw o map_raw argobj)
                  g) q1"
    apply(rule defobj_natural_eq_onp_pred[OF _ q1])
    unfolding G.rel_map unfolding eq_onp_def pred_D_def apply auto 
    apply(rule G.rel_refl_strong) using IH1 f_shape_flat_shape 
     apply (auto simp: D.set_map) 
     apply(rule invar_shapeV_flat_shapeV)
    apply(rule invar_shape_f_shape[unfolded pred_D_def, simplified, rule_format])
      apply auto unfolding invar_shape_map_closed using IH1 apply simp
    unfolding rel_fun_def apply auto
    unfolding R2.rel_map apply auto
    unfolding pred_V_def apply auto
    apply(drule rel_R1_pred_R1_refl) apply auto
    apply(rule R2.rel_refl_strong) apply auto
    apply(rule invar_shapeV_set_V_un_NodeV, auto)
      apply(rule invar_shapeV_flat_shapeV[of "F # u0", simplified])
      apply(rule invar_f_raw[unfolded pred_R1_def pred_R2_def, 
             simplified, rule_format], auto)
      using IH1 IH2
      apply (auto simp: invar_map_closed_raw invar_shapeV_unflat_shapeV_raw R1.map_comp 
          R1.set_map pred_V_def V.set_map)
       apply (simp add: R1.pred_set invar_shapeV_unflat_shapeV_raw)
      apply(rule un_NodeV_flat_shapeV[of "u0"])
      apply(rule invar_f_raw[unfolded pred_R1_def pred_R2_def, 
             simplified, rule_format], auto)
      apply (auto simp: invar_map_closed_raw invar_shapeV_unflat_shapeV_raw R1.map_comp 
          R1.set_map pred_V_def V.set_map)
      by (simp add: R1.pred_set invar_shapeV_unflat_shapeV_raw)              
    also have "… = map_R (unflat_shapeV u0) flat_shapeV (defobj ?x) q1"
       
      unfolding G.map_comp  o_assoc R_map_comp[symmetric] 
      unfolding unflat_shapeV_Cons_o_NodeV
      unfolding defobj_flat_shape_natural
     [of q1, OF q1[unfolded pred_R1_def, simplified, rule_format] x, simplified, 
        unfolded G.map_comp  o_assoc R_map_comp[symmetric]] 
      by simp
  also have "… = map_R (unflat_shapeV u0) flat_shapeV (f_raw (Cons ?y)) q1" 
    unfolding f_raw.simps G.map_comp ..
  also have "… = map_R (unflat_shapeV u0) 
                  flat_shapeV (f_raw (map_raw argobj (Cons g))) q1"
  unfolding raw.simps ..
  finally show ?case .
qed

(* Crucial: Leaf-unLeaf will close a diagram that diverges a little: *)
lemma map_R_LeafV: 
fixes r r' :: "'a shapeV R"
assumes "⋀ q1. pred_R1 (invar_shapeV []) q1 ⟹ r q1 = r' q1"
shows "map_R LeafV un_LeafV r = map_R LeafV un_LeafV r'"
apply(rule ext) apply simp
apply(rule R2.map_cong) apply auto
apply(rule assms)
by (simp add: R1.set_map axiom10_R1)


theorem "f (T g) = defobj (map_G id (f o map_T argobj) g)"
  (is "?A = ?B")
proof-
  (* Preparations: *)
  have 1: "invar [] (Cons (map_G Leaf (flat ∘ Rep_T) g))"
    unfolding invar_simps pred_G_def using Rep_T invar_flat_raw
    by (fastforce simp: G.set_map Rep_T invar_flat_raw)
  (*  *)
  have "?A = map_R LeafV un_LeafV (f_raw (Rep_T (T g)))"
    unfolding f_def ..
  also have "… = 
  map_R LeafV un_LeafV (f_raw ((Cons (map_G Leaf (flat ∘ Rep_T) g))))"
    unfolding T_def using T.Abs_T_inverse[simplified, OF 1] by simp
  also have "… = 
  map_R LeafV un_LeafV (defobj
     (map_G (f_shape ∘ Leaf)
            (map_R NodeV un_NodeV ∘ f_raw ∘ (flat ∘ Rep_T)) 
            g))" 
    unfolding f_raw.simps G.map_comp ..
  also have "… = 
  map_R LeafV un_LeafV (defobj
     (map_G (f_shape ∘ Leaf)
         (map_R (unflat_shapeV [] o NodeV) (un_NodeV ∘ flat_shapeV) o f_raw o map_raw argobj ∘ Rep_T)
            g))" 
    apply(rule map_R_LeafV) 
    apply(rule defobj_natural_eq_onp_pred, auto)
    unfolding G.rel_map apply(rule G.rel_refl_strong)
    unfolding eq_onp_def apply auto 
    using invar_shape_depth_iff(1) invar_shape_f_shape apply fastforce
    unfolding rel_fun_def apply auto
    unfolding R2.rel_map  apply auto 
    apply(drule rel_R1_pred_R1_refl) apply auto
    apply(drule pred_R1_invar_shapeV_NodeV)
    apply (auto simp: f_raw_flat[OF T.Rep_T[simplified], simplified])
    unfolding R2.rel_map unfolding R1.map_comp
    apply(rule R2.rel_refl_strong) apply auto 
    unfolding pred_V_def apply auto
    apply(rule invar_shapeV_set_V_un_NodeV, auto)
    apply(rule invar_shapeV_flat_shapeV[of "[]", simplified])
    apply(rule invar_f_raw[of "[]", unfolded pred_R1_def pred_R2_def, 
      simplified, rule_format]) apply auto
    using Rep_T invar_map_closed_raw unfolding R1.set_map by auto
  also have "… = 
  map_R LeafV un_LeafV (defobj
     (map_G (f_shape ∘ Leaf)
            (map_R (unflat_shapeV [] o NodeV) (un_NodeV ∘ flat_shapeV) ∘ f_raw ∘ Rep_T ∘ map_T argobj)
            g))" 
    unfolding o_apply map_raw_Rep_T ..  
  also have "… = 
  map_R LeafV un_LeafV (defobj
     (map_G (f_shape ∘ Leaf)
            (map_R (unflat_shapeV [] o NodeV) (map_V LeafV o un_LeafV) ∘ f_raw ∘ Rep_T ∘ map_T argobj)
            g))"
    apply(rule cong[of "map_R LeafV un_LeafV"], force)  
    apply(rule cong[of defobj], simp) 
    apply(rule G.map_cong, simp) 
     apply (auto simp: fun_eq_iff  intro!: R2.map_cong un_NodeV_flat_shapeV_Nil)
    apply(rule invar_f_raw[unfolded pred_fun_def pred_R1_def pred_R2_def, 
               simplified, rule_format])
    using Rep_T by (auto simp: R1.set_map)
  also have "… = 
  defobj (map_G (map_D un_LeafV) (map_R (map_V LeafV) (map_V un_LeafV))
     (map_G (f_shape ∘ Leaf)
            (map_R (unflat_shapeV [] o NodeV) (map_V LeafV o un_LeafV) ∘ f_raw ∘ Rep_T ∘ map_T argobj)
            g))"
    apply(rule defobj_natural_UNIV[of _ "range LeafV" un_LeafV _ ]) 
    unfolding inj_on_def 
    by (auto simp: G.set_map D.set_map R2.set_map R1.set_map V.set_map)
  also have "… = defobj (map_G id (f ∘ map_T argobj) g)" 
    unfolding G.map_comp o_assoc  V.axiom2_V[symmetric] 
    unfolding R_map_comp[symmetric]
    unfolding f_def2 
    unfolding o_assoc[symmetric] unfolding o_assoc
    unfolding D.axiom2_D[symmetric]
    apply(rule cong[of defobj], simp) 
    apply(rule G.map_cong, simp)
     apply(subst D.axiom1_D[symmetric]) unfolding o_apply f_shape.simps D.map_comp
      apply(rule D.map_cong, simp) apply auto[]
     (* *)
    apply simp
    unfolding V.map_comp by (auto simp: V.map_ident cong: V.map_cong) 
  finally show ?thesis .
qed

hide_const (open) f

end