Theory Nonuniform_Datatype

theory Nonuniform_Datatype
imports BNF_Axiomatization
theory Nonuniform_Datatype
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 snoc: "snoc x xs = xs @ [x]"
  by (induct xs) auto

lemma rev_Cons: "rev (x # xs) = snoc x (rev xs)"
  by (auto simp: snoc)

lemma rev_snoc: "rev (snoc x xs) = x # rev xs"
  by (auto simp: snoc)

lemma vimage2p_eq_onp: "inj f ⟹ BNF_Def.vimage2p f f (eq_onp S) = eq_onp (S o f)"
  unfolding vimage2p_def eq_onp_def inj_on_def by auto

lemma vimage2pD: "BNF_Def.vimage2p f g R x y ⟹ R (f x) (g y)"
  unfolding vimage2p_def .

lemma eq_onpD: "eq_onp S x x ⟹ S x"
  unfolding eq_onp_def by 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

lemma pred_funD: "pred_fun A B f ⟹ A x ⟹ B (f x)"
  unfolding pred_fun_def by auto

section ‹Input›

declare [[bnf_internals, typedef_overloaded]]

(*
datatype 'a l = N | C 'a "('a * 'a) l"

('a, 'x) G = unit + 'a * 'x
'a F = 'a * 'a

specs = [(G, [[F]])]
*)

bnf_axiomatization 'a F

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 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_Cons t ≡ case t of Cons x ⇒ x"


section ‹Invariant›

primrec 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)"

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 (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 (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_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 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 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 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_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_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, 'c F) R) G ⇒ ('b, 'c) R) ⇒
  (∀'a. 'a D F ⇒ 'a F D) ⇒
  'a D T ⇒ ('b, 'c) R 
*)

bnf_axiomatization 'a V
datatype 'a shapeV = LeafV 'a | NodeV "'a shapeV V"

abbreviation "un_LeafV u ≡ case u of LeafV x ⇒ x"
abbreviation "un_NodeV u ≡ case u of NodeV x ⇒ x"

primrec 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)"

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_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))"

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_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: V.pred_map)+

lemma flat_shapeV_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_shapeV_unflat_shapeV =
  mp[OF spec[OF flat_shapeV_unflat_shapeV_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_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_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]]


bnf_axiomatization ('a, 'b, 'c) R
bnf_axiomatization ('a, 'b, 'c) D

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

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

lemma defobj_invar: "pred_fun (pred_G (pred_D A B C) (pred_R (pred_V A) (pred_V B) (pred_V C))) (pred_R A B C) defobj"
  unfolding fun_pred_rel G.rel_eq_onp[symmetric] F.rel_eq_onp[symmetric]
    D.rel_eq_onp[symmetric] R.rel_eq_onp[symmetric] V.rel_eq_onp[symmetric]
  by (rule defobj_transfer; rule bi_unique_eq_onp)

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

lemma defobj_natural:
  "inj_on a (⋃(set1_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set1_R ` set2_G x))) ⟹
   inj_on b (⋃(set2_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set2_R ` set2_G x))) ⟹
   inj_on c (⋃(set3_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set3_R ` set2_G x))) ⟹
  defobj (map_G (map_D a b c) (map_R (map_V a) (map_V b) (map_V c)) x) = map_R a b c (defobj x)"
  using rel_funD[OF defobj_transfer, of
     "BNF_Def.Grp (⋃(set1_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set1_R ` set2_G x))) a"
     "BNF_Def.Grp (⋃(set2_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set2_R ` set2_G x))) b"
     "BNF_Def.Grp (⋃(set3_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set3_R ` set2_G x))) c"]
  unfolding F.rel_Grp R.rel_Grp D.rel_Grp G.rel_Grp V.rel_Grp bi_unique_Grp
  by (force simp add: Grp_def)

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

lemma argobj_flat_shape_natural: fixes x :: "('a V shapeV, 'b V shapeV, 'c V shapeV) D F"
  shows
    "pred_F (pred_D (invar_shapeV u) (invar_shapeV u) (invar_shapeV u)) x ⟹
    argobj (map_F (map_D flat_shapeV flat_shapeV flat_shapeV) x) =
    map_D (map_V flat_shapeV) (map_V flat_shapeV) (map_V flat_shapeV) (argobj x)"
  apply (rule argobj_natural; rule inj_onI;
    rule box_equals[OF _ unflat_shapeV_flat_shapeV[of u] unflat_shapeV_flat_shapeV[of u]])
  apply (auto simp only: F.pred_set D.pred_set)
  done

lemma defobj_flat_shape_natural: fixes x :: "(('a V shapeV, 'b V shapeV, 'c V shapeV) D, ('a V shapeV V, 'b V shapeV V, 'c V shapeV V) R) G"
  shows
    "pred_G (pred_D (invar_shapeV u) (invar_shapeV u) (invar_shapeV u)) (pred_R (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u))) x ⟹
    defobj (map_G (map_D flat_shapeV flat_shapeV flat_shapeV) (map_R (map_V flat_shapeV) (map_V flat_shapeV) (map_V flat_shapeV)) x) = map_R flat_shapeV flat_shapeV flat_shapeV (defobj x)"
  apply (rule defobj_natural; rule inj_onI;
    rule box_equals[OF _ unflat_shapeV_flat_shapeV[of u] unflat_shapeV_flat_shapeV[of u]])
  apply (auto simp only: F.pred_set G.pred_set D.pred_set R.pred_set V.pred_set)
  done

primrec f_shape :: "depth ⇒ ('a, 'b, 'c) D shape ⇒ ('a shapeV, 'b shapeV, 'c shapeV) D" where
  "f_shape [] = map_D LeafV LeafV LeafV o un_Leaf"
| "f_shape (_ # u0) = map_D NodeV NodeV NodeV o argobj o map_F (f_shape u0) o un_Node"

primrec f_raw :: "depth ⇒ ('a, 'b, 'c) D raw ⇒ ('a shapeV, 'b shapeV, 'c shapeV) R" where
  "f_raw u0 (Cons g) =
     defobj (map_G (f_shape u0) (map_R un_NodeV un_NodeV un_NodeV o f_raw (F # u0)) g)"

definition f :: "('a, 'b, 'c) D T ⇒ ('a, 'b, 'c) R" where
  "f = map_R un_LeafV un_LeafV un_LeafV o f_raw [] o Rep_T"

lemma invar_shape_f_shape[THEN spec, THEN mp]:
  "∀u. invar_shape u0 u ⟶ pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_shape u0 u)"
  apply (rule list.induct[of "λu0. ∀u. invar_shape u0 u ⟶ pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_shape u0 u)" u0])
   apply (auto simp only: f_shape.simps o_apply D.pred_map
     invar_shape.simps invar_shapeV.simps list.case D.pred_True
     cong: D.pred_cong) []
  subgoal for x xs
  apply (cases x)
    apply (auto simp only: invar_shape_depth_iff shape.case
     invar_shapeV.simps f_shape.simps D.pred_map D.pred_True o_apply
    simp_thms all_simps imp_conjL list.inject list.distinct F.pred_map
    intro!: pred_funD[OF argobj_invar]
    elim!: F.pred_mono_strong
    cong: D.pred_cong
    split: list.splits label.splits)
    done
  done

lemma f_shape_flat_shape[THEN spec, THEN mp]: "∀x. invar_shape u0 x ⟶
  f_shape (snoc F u0) (flat_shape x) = map_D flat_shapeV flat_shapeV flat_shapeV (f_shape u0 (map_shape argobj x))"
  apply (rule list.induct[of "λu0. ∀x. invar_shape u0 x ⟶ f_shape (snoc F u0) (flat_shape x) = map_D flat_shapeV flat_shapeV flat_shapeV (f_shape u0 (map_shape argobj x))" u0])
   apply (auto simp only: flat_shape.simps flat_shapeV.simps f_shape.simps
     invar_shape_depth_iff shape.case
     snoc.simps shape.map D.map_comp F.map_comp argobj_natural inj_on_def shapeV.inject
     o_apply simp_thms Ball_def cong: F.map_cong D.map_cong) []
  apply (rule allI)
  subgoal premises IH for x xs u
    apply (rule impI)
    apply (cases x)
    apply (unfold flat_shape.simps flat_shapeV.simps f_shape.simps shape.map D.map_comp o_def)
    apply (auto simp only: D.map_comp[unfolded o_def, symmetric]
        F.set_map F.map_comp F.pred_set o_apply
        invar_shape_map_closed invar_shape_f_shape invar_shape_depth_iff snoc.simps
        f_shape.simps flat_shape.simps shape.map shape.case
      intro!: arg_cong[of _ _ argobj] D.map_cong F.map_cong
         IH[THEN spec, THEN mp]
        trans[OF _ argobj_flat_shape_natural[of xs]]
      elim!: F.pred_mono_strong
      split: list.splits label.splits)
    done
  done

lemma invar_f_raw[THEN spec, THEN mp]:
  "∀u0. invar u0 x ⟶ pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_raw u0 x)"
  apply (rule raw.induct[of "λx. ∀u0. invar u0 x ⟶ pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_raw u0 x)" x])
  apply (rule allI)
  subgoal premises IH for g u0
    apply (auto simp only: invar_simps raw.map f_raw.simps G.map_comp o_apply G.pred_map R.pred_map
    invar_shape_map_closed invar_shapeV_depth_iff shapeV.case
    intro!: pred_funD[OF defobj_invar[of "invar_shapeV u0" "invar_shapeV u0" "invar_shapeV u0"]] invar_shape_f_shape
      R.pred_mono_strong[OF mp[OF spec[OF IH, of _ "F # u0"]]]
    elim!: G.pred_mono_strong
    cong: G.map_cong)
    done
  done

lemma f_raw_flat[THEN spec, THEN mp]:
  "∀u0. invar u0 x ⟶ f_raw (snoc F u0) (flat x) = map_R flat_shapeV flat_shapeV flat_shapeV (f_raw u0 (map_raw argobj x))"
  apply (rule raw.induct[of "λx. ∀u0. invar u0 x ⟶ f_raw (snoc F u0) (flat x) = map_R flat_shapeV flat_shapeV flat_shapeV (f_raw u0 (map_raw argobj x))" x])
  apply (rule allI)
  subgoal premises IH for g u0
    apply (auto simp only: flat.simps f_raw.simps G.map_comp o_apply
      f_shape_flat_shape raw.map invar_map_closed
      invar_simps G.pred_set G.set_map mp[OF spec[OF IH, of _ "F # u0"], simplified]
      R.map_comp invar_shapeV_depth_iff shapeV.case flat_shapeV.simps invar_shape_map_closed R.pred_map
      intro!: arg_cong[of _ _ defobj] G.map_cong0 R.map_cong_pred invar_shape_f_shape
        R.pred_mono_strong[OF invar_f_raw[of "F # u0"]]
        trans[OF _ defobj_flat_shape_natural[of u0]] f_shape_flat_shape[of u0])
    done
  done

lemma f_shape_transfer:
  assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
  and depth: "list_all2 op = u1 u2"
  and args: "rel_shape (rel_D A B C) s1 s2"
  and invar: "invar_shape u1 s1" "invar_shape u2 s2"
  shows "rel_D (rel_shapeV A) (rel_shapeV B) (rel_shapeV C)
    (f_shape u1 s1) (f_shape u2 s2)"
using depth args invar proof (induct u1 u2 arbitrary: s1 s2 rule: list.rel_induct)
  case Nil
  then show ?case by (auto simp: invar_shape_depth_iff D.rel_map)
next
  case (Cons a21 a22 b21 b22)
  note [intro!] = argobj_transfer[OF
    shapeV.bi_unique_rel[OF bi_unique(1)]
    shapeV.bi_unique_rel[OF bi_unique(2)]
    shapeV.bi_unique_rel[OF bi_unique(3)], THEN rel_funD] 
  from Cons show ?case by (cases b21) (auto simp:
    invar_shape_depth_iff D.rel_map F.rel_map F.pred_set
    elim!: F.rel_mono_strong)
qed

lemma f_raw_transfer:
  assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
  and depth: "list_all2 op = u1 u2"
  and args: "rel_raw (rel_D A B C) r1 r2"
  and invar: "invar u1 r1" "invar u2 r2"
  shows "rel_R (rel_shapeV A) (rel_shapeV B) (rel_shapeV C)
    (f_raw u1 r1) (f_raw u2 r2)"
using args depth invar proof (induct r1 r2 arbitrary: u1 u2 rule: raw.rel_induct)
  case (Cons a b)
  note [intro!] = defobj_transfer[OF
    shapeV.bi_unique_rel[OF bi_unique(1)]
    shapeV.bi_unique_rel[OF bi_unique(2)]
    shapeV.bi_unique_rel[OF bi_unique(3)], THEN rel_funD]
    f_shape_transfer[OF bi_unique]
  from Cons show ?case
    by (force simp: list.rel_eq invar_simps invar_shapeV_depth_iff
      G.rel_map G.pred_set R.rel_map
      elim!: G.rel_mono_strong R.rel_mono_strong
      dest!: spec[of _ "F # u2"]
      dest: conjunct1[OF invar_f_raw[unfolded R.pred_set], THEN bspec, rotated -1]
        conjunct1[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1]
        conjunct2[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1])
qed
    
lemma f_transfer:
  assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
  shows "rel_fun (rel_T (rel_D A B C)) (rel_R A B C) f f"
  unfolding f_def rel_fun_def o_apply
  by (force simp: R.rel_map Rep_T[simplified] rel_T_def vimage2p_def
      invar_shapeV_depth_iff
    intro!: R.rel_mono_strong[OF f_raw_transfer[OF bi_unique]]
    dest: conjunct1[OF invar_f_raw[unfolded R.pred_set], THEN bspec, rotated -1]
        conjunct1[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1]
        conjunct2[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1])

lemma f_ctor: "f (T g) = defobj (map_G id (f o map_T argobj) g)"
  apply (simp only: f_def map_T_def T_def o_apply cong: G.map_cong)
  apply (subst (1 2) Abs_T_inverse)
    apply (simp only: mem_Collect_eq invar_map_closed_raw Rep_T[unfolded mem_Collect_eq])
   apply (simp only: mem_Collect_eq invar_simps G.pred_map G.pred_True o_apply
     invar_shape.simps list.case invar_flat Rep_T[unfolded mem_Collect_eq] snoc.simps[symmetric]
     cong: G.pred_cong)
   apply (auto simp only:
    G.map_comp V.map_comp D.map_comp R.map_comp
    V.map_ident D.map_ident
    G.set_map V.set_map D.set_map R.set_map shape.simps
    f_raw.simps f_shape.simps shapeV.case flat_shapeV.simps invar_shapeV_depth_iff
    f_raw_flat[OF Rep_T[unfolded mem_Collect_eq], unfolded snoc.simps]
    inj_on_def o_apply id_apply
    intro!: arg_cong[of _ _ defobj] G.map_cong R.map_cong
      trans[OF defobj_natural[of un_LeafV _ un_LeafV un_LeafV, symmetric]]
    dest!: bspec[OF conjunct1[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]
           bspec[OF conjunct1[OF conjunct2[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]]
           bspec[OF conjunct2[OF conjunct2[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]]
    cong: V.map_cong D.map_cong)
  done

hide_const (open) f

section ‹Induction›

abbreviation "immerse ul ≡ map_raw Node o unflat (rev ul)"

  (* cumulative immerse: *)  
primrec cimmerse_shape :: "depth ⇒ 'a shape shape ⇒ 'a shape shape" where 
  "cimmerse_shape [] sh = sh"
| "cimmerse_shape (u # ul) sh = cimmerse_shape ul (map_shape Node (unflat_shape (rev ul) sh))"

primrec cimmerse :: "depth ⇒ 'a shape raw ⇒ 'a shape raw" where 
  "cimmerse [] r = r"
| "cimmerse (u # ul) r = cimmerse ul (immerse ul r)"

lemma cimmerse_shape_inj[THEN spec, THEN spec, THEN mp, THEN mp, THEN mp]:
  "∀sh1 sh2. invar_shape (rev ul) sh1 ⟶ invar_shape (rev ul) sh2 ⟶
    cimmerse_shape ul sh1 = cimmerse_shape ul sh2 ⟶ sh1 = sh2"
  apply (rule list.induct[of "λul. ∀sh1 sh2. invar_shape (rev ul) sh1 ⟶ invar_shape (rev ul) sh2 ⟶
    cimmerse_shape ul sh1 = cimmerse_shape ul sh2 ⟶ sh1 = sh2" ul])
   apply (rule allI impI)+
   apply (simp only: cimmerse_shape.simps(1) rev.simps(1) id_apply)
  subgoal premises prems for u ul
    apply (rule label.exhaust[of u])
    apply (rule allI impI)+
    apply (drule prems[THEN spec, THEN spec, THEN mp, THEN mp, THEN mp, rotated -1]
        shape.inj_map_strong[rotated -1] arg_cong[of _ _ flat_shape] |
      simp only: cimmerse_shape.simps o_apply rev_Cons shape.inject
        invar_shape_map_closed invar_shape_unflat_shape flat_shape_unflat_shape)+
    done
  done

lemma invar_cimmerse[THEN spec, THEN mp]:
  "∀r. invar (rev ul) r ⟶ invar [] (cimmerse ul r)"
  apply (rule list.induct[of "λul. ∀r. invar (rev ul) r ⟶ invar [] (cimmerse ul r)" ul])
   apply (rule allI impI)+
   apply (simp only: cimmerse.simps(1) rev.simps(1) id_apply)
  subgoal for u ul
    apply (rule label.exhaust[of u])
    apply (rule allI impI)+
    apply (simp only: cimmerse.simps(2) rev_Cons o_apply invar_map_closed invar_unflat)
    done
  done

lemma un_Cons_cimmerse[THEN spec]:
  "∀r. map_G id (immerse (rev [])) (un_Cons (cimmerse ul r)) = 
   map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)"
  apply (rule list.induct[of "λul. ∀r. map_G id (immerse (rev [])) (un_Cons (cimmerse ul r)) = 
    map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)" ul])
   apply (rule allI)
   apply (simp only: cimmerse.simps cimmerse_shape.simps snoc.simps(1) rev.simps id_o id_apply
     cong: G.map_cong)
  apply (rule allI)
  apply (auto simp only: cimmerse.simps cimmerse_shape.simps rev_snoc rev.simps
    snoc.simps o_apply id_apply id_o G.map_comp unflat.simps raw.map
    cong: G.map_cong split: raw.splits)
  done

abbreviation (input) rimplies (infixr "⟵" 25) where
  "P ⟵ PP ≡ PP ⟶ P"
lemma
  "left_total R ⟹ rel_fun (rel_fun R (op ⟵)) (op ⟵) All All"
  unfolding rel_fun_def left_total_def by auto
lemma
  "left_total R ⟹ rel_fun (rel_fun R (op ⟶)) (op ⟶) Ex Ex"
  unfolding rel_fun_def left_total_def by force
    
    (*  THE ASSUMPTIONS: *)
consts Q :: "'a T ⇒ bool"
axiomatization where 
  Q_param: "⋀(R :: 'a ⇒ 'a' ⇒ bool). bi_unique R ⟹ left_total R ⟹ rel_fun (rel_T R) op ⟵ Q Q" and
  Q_ind: "pred_G (λ_. True) Q ≤ Q o T"
  
lemma reorient_le_o_Abs:
  "(⋀x. Abs (Rep x) = x) ⟹ (A :: _ ⇒ _ :: order) ≤ B o Abs ⟹ A o Rep ≤ B"
  unfolding le_fun_def o_apply
  by (rule allI, rule order_trans, erule spec) auto

lemma Q_map_T_inj:
  assumes "inj f"
  shows "Q (map_T f t) ⟶ Q t"
  using assms Q_param[of "BNF_Def.Grp UNIV f"] unfolding bi_unique_Grp
  unfolding rel_fun_def T.rel_Grp left_total_def unfolding Grp_def
  by (auto simp: inj_on_def)

abbreviation Qr where 
  "Qr ul r ≡ Q (Abs_T (cimmerse ul r))"

theorem Qr_un_Cons:
  "invar (rev ul) r ⟹ pred_G (λ_. True) (λx. Q (Abs_T x))
    (map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)) ⟹
    Qr ul r"
  apply (unfold un_Cons_cimmerse[symmetric] rev.simps(1))
  apply (rule predicate1D[OF reorient_le_o_Abs[OF T_un_T Q_ind]])
  apply (drule invar_cimmerse)
  apply (hypsubst_thin |
    rule mp[OF Q_map_T_inj[of Node], rotated -1] |
    drule raw.inj_map_strong[rotated -1] |
    drule bspec, assumption |
    erule conjE exE |
    rule allI impI ballI conjI |
    simp only: eq_onp_def Abs_T_inject invar_map_closed
      G.set_map un_T_def Abs_T_inverse map_T_def invar_cimmerse
      mem_Collect_eq ball_simps o_apply id_apply snoc.simps inj_on_def
      invar_unflat raw.inject shape.inject shape.case invar_simps G.pred_set invar_shape_depth_iff
      split: raw.splits)+
  done

theorem Qrr[THEN spec, THEN mp]: 
  fixes r :: "'a shape raw"  
  shows "∀ul. invar (rev ul) r ⟶ Qr ul r"
  apply (rule raw.induct[of "λr. ∀ul. invar (rev ul) r ⟶ Qr ul r"])
  apply (rule allI)
  apply (rule impI)
  apply (rule Qr_un_Cons, assumption)
  apply (hypsubst_thin |
      erule cimmerse_shape_inj[rotated -1] conjE |
      rule ballI impI |
      drule bspec, assumption |
      simp only: G.set_map id_apply invar_simps G.pred_set raw.inject rev_snoc shape.rel_eq ball_simps ball_triv simp_thms split: raw.splits |
      rule exI, rule conjI[rotated], assumption)+
  done

theorem T_ind: "(Q::'a T ⇒ bool) t"
  apply (insert Qrr[of "[]" "Rep_T (map_T Leaf t)"])
  apply (rule Abs_T_cases[of t])
  apply (auto simp only: rev.simps invar_map_closed True_implies_equals
      Rep_T_inverse Rep_T[unfolded mem_Collect_eq] inj_on_def shape.inject
      simp_thms ball_simps cimmerse.simps eq_onp_def
      elim!: mp[OF Q_map_T_inj[of Leaf], rotated])
  done

end