Theory Nonuniform_Codatatype

theory Nonuniform_Codatatype
imports BNF_Axiomatization
theory Nonuniform_Codatatype
  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 [wits: "'a ⇒ 'a F"]
  
bnf_axiomatization ('a, 'x) G [wits: "'a ⇒ 'x ⇒ ('a, 'x) G"]
  
section ‹Raw Type›
  
datatype label = F
type_synonym depth = "label list"
datatype 'a shape = Leaf 'a | Node "'a shape F"
codatatype 'a raw = Cons (unCons: "('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)"
  
coinductive invar :: "depth ⇒ 'a raw ⇒ bool" where
  "pred_G (invar_shape u0) (λx. invar (F # u0) x) 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›
  
primrec mk_shape where
  "mk_shape [] x = Leaf x"
| "mk_shape (_ # u0) x = Node (wit_F (mk_shape u0 x))"
  
primcorec wit :: "label list ⇒ 'a ⇒ 'a raw" where
  "wit u0 x = Cons (map_G id (case_prod wit) (wit_G (mk_shape u0 x) (F # u0, x)))"
  
lemma invar_shape_mk_shape: "invar_shape u0 (mk_shape u0 x)"
  apply (induct u0)
  apply (auto split: label.splits simp: F.pred_set dest!: F.wit)
  done
    
lemma invar_wit: "invar u0 (wit u0 x)"
  apply (coinduction arbitrary: u0)
  apply (subst wit.ctr)
  apply (auto simp: G.set_map G.pred_set invar_shape_mk_shape dest!: G.wit)
  done
    
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))"
  
primcorec (transfer) flat :: "'a F raw ⇒ 'a raw" where
  "flat r = Cons (map_G flat_shape flat (un_Cons r))"
  
lemmas flat_simps = flat.ctr[of "Cons z" for z, unfolded raw.sel]
  
primcorec unflat :: "depth ⇒ 'a raw ⇒ 'a F raw" where
  "unflat u0 r = Cons (map_G (unflat_shape u0) (unflat (F # u0)) (un_Cons r))"
  
lemmas unflat_simps = unflat.ctr[of _ "Cons z" for z, unfolded raw.sel]
  
  
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:
  "invar u0 (map_raw f t) = invar u0 (t :: 'a raw)"
  apply (rule iffI)
  subgoal
    apply (coinduction arbitrary: u0 t)
    subgoal for u0 t
      apply (cases t)
      apply (auto simp only: simp_thms ex_simps o_apply raw.inject
          raw.map invar_simps G.pred_map invar_shape_map_closed elim!: G.pred_mono_strong)
      done
    done
  subgoal
    apply (coinduction arbitrary: u0 t)
    subgoal for u0 t
      apply (cases t)
      apply (auto simp only: simp_thms ex_simps o_apply raw.inject
          raw.map invar_simps G.pred_map invar_shape_map_closed elim!: G.pred_mono_strong)
      done
    done
  done
    
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_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_flat: "invar u0 t ⟶ invar (snoc F u0) (flat t)"
  apply (rule impI)
  apply (rule invar.coinduct[of "λx y. ∃u0 t. x = (snoc F u0) ∧ y = (flat t) ∧ invar u0 t"])
  apply (rule exI conjI refl)+
  apply assumption
  apply (erule exE conjE)+
  apply hypsubst
  subgoal for _ _ u0 t
    apply (rule raw.exhaust[of t])
    apply (auto simp only: raw.inject
        flat_simps invar_simps invar_shape_flat_shape
        G.pred_map
        id_apply o_apply snoc.simps[symmetric] ex_simps simp_thms(39,40)
        elim!: G.pred_mono_strong |
        ((rule exI)+, rule conjI[OF refl]))+
    done
  done
    
lemma invar_unflat[THEN mp]: "invar (snoc F u0) t ⟶ invar u0 (unflat u0 t)"
  apply (rule impI)
  apply (rule invar.coinduct[of "λx y. ∃u0 t. x = u0 ∧ y = (unflat u0 t) ∧ invar (snoc F u0) t"])
  apply (rule exI conjI refl)+
  apply assumption
  apply (erule exE conjE)+
  apply hypsubst
  subgoal for _ _ u0 t
    apply (rule raw.exhaust[of t])
    apply (auto simp only: raw.inject
        unflat_simps invar_simps invar_shape_unflat_shape
        G.pred_map
        id_apply o_apply snoc.simps[symmetric] ex_simps simp_thms(39,40)
        elim!: G.pred_mono_strong |
        ((rule exI)+, rule conjI[OF refl]))+
    done
  done
    
lemma flat_unflat: "invar (snoc F u0) t ⟶ flat (unflat u0 t) = t"
  apply (rule impI)
  apply (rule raw.coinduct[of
        "λl r. ∃u0 t. l = flat (unflat u0 t) ∧ r = t ∧ invar (snoc F u0) t" "flat (unflat u0 t)" t])
  apply ((rule exI conjI refl | assumption)+)
  apply (erule exE conjE)+
  apply hypsubst
  subgoal for _ _ u0 t
    apply (rule raw.exhaust[of t])
    apply (auto simp only: raw.sel unflat_simps flat_simps G.rel_map invar_simps G.pred_rel
        flat_shape_unflat_shape snoc.simps[symmetric] eq_onp_def elim!: G.rel_mono_strong)
    done
  done
    
lemma unflat_flat: "invar u0 t ⟶ unflat u0 (flat t) = t"
  apply (rule impI)
  apply (rule raw.coinduct[of
        "λl r. ∃u0 t. l = unflat u0 (flat t) ∧ r = t ∧ invar u0 t" "unflat u0 (flat t)" t])
  apply ((rule exI conjI refl | assumption)+)
  apply (erule exE conjE)+
  apply hypsubst
  subgoal for _ _ u0 t
    apply (rule raw.exhaust[of t])
    apply (auto simp only: raw.sel unflat_simps flat_simps G.rel_map invar_simps G.pred_rel
        unflat_shape_flat_shape snoc.simps[symmetric] eq_onp_def elim!: G.rel_mono_strong)
    done
  done
    
    
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 (coinduction arbitrary: t rule: raw.coinduct)
  apply (rename_tac t)
  apply (case_tac t)
  apply (auto simp only: raw.sel G.rel_map
      raw.map flat_simps flat_shape_map o_apply
      intro!: G.rel_refl)
  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 subset_UN_I:
  "(⋀x y. x ∈ C y ⟹ ∀t. fl t = y ⟶ x ∈ (⋃x∈C' t. B x)) ⟹ C (fl t) ⊆ (⋃x∈C' t. B x)"
  by blast
    
lemma UN_E': "b ∈ (⋃x∈A. B x) ⟹ (⋀x. x ∈ A ⟹ ∀b. b ∈ B x ⟶ b ∈ C) ⟹ b ∈ C"
  by blast
    
    
lemma set_raw_flat:
  "set_raw (flat t) = UNION (set_raw t) set_F"
  apply (rule equalityI)
  apply (rule subset_UN_I[of set_raw flat set_F set_raw t])
  apply (erule raw.set_induct)
  apply (rule allI impI)+
  subgoal for _ _ g sh a t
    apply (rule raw.exhaust[of t])
    apply (auto 0 4 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
  apply (rule allI impI)+
  subgoal for _ _ g sh a t
    apply (rule raw.exhaust[of t])
    apply (auto 0 4 simp only:
        flat_simps raw.set G.set_map
        UN_simps UN_Un UN_Un_distrib Un_ac
        cong: SUP_cong) []
    done
      
  apply (rule subsetI)
  apply (erule UN_E')
  apply (erule raw.set_induct)
  apply (rule allI impI)+
  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) []
  apply (rule allI impI)+
  apply (auto simp only:
      flat_simps raw.set G.set_map
      UN_simps UN_Un UN_Un_distrib Un_ac) []
  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:
  "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 (coinduction arbitrary: u0 t t' rule: raw.rel_coinduct)
  apply (rename_tac t t')
  apply (case_tac t)
  apply (case_tac t')
  apply (auto simp only: raw.sel
      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 |
      ((rule exI)+, rule conjI[OF refl]))+
  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 impI)+
  apply (rule raw.rel_coinduct[of "λt t'. ∃u0. invar u0 t ∧ invar u0 t' ∧ rel_raw R (flat t) (flat t')" t t' "rel_F R"])
  apply ((rule conjI exI | assumption))+
  subgoal for raw raw'
    apply (rule raw.exhaust[of raw])
    apply (rule raw.exhaust[of raw'])
    apply (auto simp only: raw.sel G.rel_map
        raw.rel_inject flat_shape_rel flat_simps invar_simps G.pred_set
        o_apply simp_thms
        intro: G.rel_refl
        cong: G.rel_cong
        elim!: G.rel_mono_strong)
    done
  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 ‹Corecursion›
  
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) R ⇒ (('a, 'b, 'c) D, ('a V, 'b V, 'c V) R) G"
consts argobj :: "('a V, 'b V, 'c V) D ⇒ ('a, 'b, 'c) D F"
  
axiomatization where
  defobj_transfer: "⋀A B C.
    bi_unique A ⟹ bi_unique B ⟹ bi_unique C ⟹
    rel_fun (rel_R A B C) (rel_G (rel_D A B C) (rel_R (rel_V A) (rel_V B) (rel_V C))) defobj defobj" and
  argobj_transfer: "⋀A B C.
    bi_unique A ⟹ bi_unique B ⟹ bi_unique C ⟹
    rel_fun  (rel_D (rel_V A) (rel_V B) (rel_V C)) (rel_F (rel_D A B C)) argobj argobj"
  
lemma defobj_invar: "pred_fun (pred_R A B C) (pred_G (pred_D A B C) (pred_R (pred_V A) (pred_V B) (pred_V 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_D (pred_V A) (pred_V B) (pred_V C)) (pred_F (pred_D A B 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_R x) ⟹
   inj_on b (set2_R x) ⟹
   inj_on c (set3_R x) ⟹
  defobj (map_R a b c x) =  map_G (map_D a b c) (map_R (map_V a) (map_V b) (map_V c)) (defobj x)"
  using rel_funD[OF defobj_transfer, of
      "BNF_Def.Grp (set1_R x) a"
      "BNF_Def.Grp (set2_R x) b"
      "BNF_Def.Grp (set3_R 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 (⋃(set_V ` set1_D x)) ⟹
   inj_on b (⋃(set_V ` set2_D x)) ⟹
   inj_on c (⋃(set_V ` set3_D x)) ⟹
  argobj (map_D (map_V a) (map_V b) (map_V c) x) = map_F (map_D a b c) (argobj x)"
  using rel_funD[OF argobj_transfer, of "BNF_Def.Grp (⋃(set_V ` set1_D x)) a" "BNF_Def.Grp (⋃(set_V ` set2_D x)) b" "BNF_Def.Grp (⋃(set_V ` set3_D 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
  shows
    "pred_D (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u)) x ⟹
    argobj (map_D (map_V flat_shapeV) (map_V flat_shapeV) (map_V flat_shapeV) x) =
    map_F (map_D flat_shapeV flat_shapeV flat_shapeV) (argobj x)"
  apply (rule argobj_natural; rule inj_onI;
      drule arg_cong[of _ _ "unflat_shapeV u"])
  apply (auto simp only: V.pred_set D.pred_set unflat_shapeV_flat_shapeV)
  done
    
lemma defobj_flat_shape_natural: fixes x
  shows
    "pred_R (invar_shapeV u) (invar_shapeV u) (invar_shapeV u) x ⟹
    defobj (map_R flat_shapeV flat_shapeV flat_shapeV x) = map_G (map_D flat_shapeV flat_shapeV flat_shapeV) (map_R (map_V flat_shapeV) (map_V flat_shapeV) (map_V 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 shapeV, 'b shapeV, 'c shapeV) D ⇒ ('a, 'b, 'c) D shape" where
  "f_shape [] = Leaf o map_D un_LeafV un_LeafV un_LeafV"
| "f_shape (_ # u0) = Node o map_F (f_shape u0) o argobj o map_D un_NodeV un_NodeV un_NodeV"
  
primcorec f_raw :: "depth ⇒ ('a shapeV, 'b shapeV, 'c shapeV) R ⇒ ('a, 'b, 'c) D raw" where
  "f_raw u0 r = Cons (map_G (f_shape u0) (f_raw (F # u0) o map_R NodeV NodeV NodeV) (defobj r))"
  
definition f :: "('a, 'b, 'c) R ⇒ ('a, 'b, 'c) D T" where
  "f = Abs_T o f_raw [] o map_R LeafV LeafV LeafV"
  
lemma invar_shape_f_shape[THEN predicate1D]:
  "pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) ≤ (λr. invar_shape u0 (f_shape u0 r))"
  apply (induct u0)
  apply (auto simp only: invar_shape.simps invar_shapeV.simps f_shape.simps D.pred_map D.pred_True o_apply
      simp_thms all_simps list.inject list.distinct F.pred_map
      intro!: pred_funD[OF argobj_invar]
      split: list.splits label.splits)
  apply (rule F.pred_mono_strong[rotated])
  unfolding o_apply
  apply (erule (1) predicate1D)
  apply (auto simp only: invar_shape.simps invar_shapeV.simps f_shape.simps D.pred_map D.pred_True o_apply
      simp_thms all_simps list.inject list.distinct F.pred_map
      invar_shapeV_depth_iff shapeV.case
      elim!: D.pred_mono_strong
      intro!: pred_funD[OF argobj_invar]
      split: list.splits label.splits)
  done
    
lemma f_shape_flat_shape[THEN spec, THEN mp]:
  "∀x. pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) x ⟶
  flat_shape (map_shape argobj (f_shape u0 x)) = f_shape (snoc F u0) (map_D flat_shapeV flat_shapeV flat_shapeV x)"
  apply (induct u0)
  apply (auto simp add: F.map_comp[symmetric]
      intro!: arg_cong[of _ _ "map_F Leaf"]) []
  apply (subst argobj_natural[symmetric];
      (auto simp: D.set_map D.pred_set V.set_map invar_shapeV_depth_iff inj_on_def
        split: shapeV.splits | (drule bspec[rotated], assumption)+)+)
  apply ((auto simp: D.map_comp V.map_comp V.map_ident
        cong: V.map_cong intro!:  D.map_cong arg_cong[of _ _ argobj]
        | (drule bspec[rotated], assumption)+)+) []
  apply (rule allI)
  subgoal premises IH for x u0 f
    apply (rule impI)
    apply (unfold flat_shape.simps flat_shapeV.simps f_shape.simps shape.map D.map_comp o_def
        snoc.simps)
    apply (cases x)
    apply (auto simp only: D.pred_map
        F.set_map F.map_comp invar_shape.simps list.sel o_apply
        invar_shape_map_closed invar_shape_f_shape invar_shapeV_depth_iff shapeV.case
        intro!: arg_cong[of _ _ argobj] D.map_cong F.map_cong
        trans[OF F.map_cong_pred[OF refl F.pred_mono_strong[OF _ IH[THEN spec, THEN mp]]]]
        pred_funD[OF argobj_invar]
        cong: F.map_cong
        elim!: D.pred_mono_strong
        split: list.splits label.splits)
    apply (auto simp only: F.map_comp[unfolded o_def, symmetric])
    apply (subst argobj_natural[symmetric])
    apply (auto simp only: inj_on_def D.set_map D.pred_set V.pred_set shapeV.case
        unflat_shapeV_flat_shapeV D.map_comp o_apply flat_shapeV.simps
        dest: arg_cong[of _ _ "unflat_shapeV u0"]
        intro!: F.map_cong arg_cong[of _ _ argobj] D.map_cong
        | drule bspec[rotated], assumption)+
    done
  done
    
lemma invar_f_raw:
  "pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) x ⟹
   invar u0 (f_raw u0 x)"
  apply (coinduction arbitrary: x u0 rule: invar.coinduct)
  apply (rule exI conjI refl f_raw.ctr)+
  apply (auto simp: G.pred_map
      intro!: G.pred_mono_strong[OF pred_funD[OF defobj_invar]] invar_shape_f_shape) []
  apply (rule exI conjI refl)+
  apply (auto simp only: R.pred_map o_apply invar_shapeV_depth_iff elim!: R.pred_mono_strong)
  done
    
lemma f_raw_flat: "pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) x ⟹
  flat (map_raw argobj (f_raw u0 x)) = f_raw (snoc F u0) (map_R flat_shapeV flat_shapeV flat_shapeV x)"
  apply (coinduction arbitrary: x u0)
  apply (auto simp: G.rel_map raw.map_sel defobj_flat_shape_natural G.pred_set
      intro!: G.rel_refl_strong f_shape_flat_shape
      dest!: pred_funD[OF defobj_invar])
  apply (rule exI conjI refl)+
  apply (auto simp: R.map_comp R.pred_map cong: R.map_cong R.pred_cong)
  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_D (rel_shapeV A) (rel_shapeV B) (rel_shapeV C) s1 s2"
    and invar: "pred_D (invar_shapeV u1) (invar_shapeV u1) (invar_shapeV u1) s1"
    "pred_D (invar_shapeV u2) (invar_shapeV u2) (invar_shapeV u2) s2"
  shows "rel_shape (rel_D A B 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 (force simp: invar_shapeV_depth_iff D.rel_map D.pred_set
        elim!: D.rel_mono_strong)
next
  case (Cons a21 a22 b21 b22)
  note argobj = 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 apply (cases b21) apply (auto simp:
        invar_shapeV_depth_iff D.rel_map F.rel_map D.pred_set V.pred_set
        intro!: F.rel_mono_strong[OF argobj]
        elim!: D.rel_mono_strong)
    apply (force)
    apply (force)
    apply (force)
    apply (drule meta_spec2)
    apply (drule meta_mp)
    defer
    apply (drule meta_mp)
    defer
    apply (erule meta_mp)
    defer
    apply assumption
    apply (drule argobj_invar[THEN pred_funD, unfolded F.pred_set, THEN bspec, rotated -1,
          of _ _ "invar_shapeV a22"])
    apply (auto simp: D.pred_set D.set_map V.pred_set) [2]
    apply (drule argobj_invar[THEN pred_funD, unfolded F.pred_set, THEN bspec, rotated -1,
          of _ _ "invar_shapeV b22"]) back
    apply (auto simp: D.pred_set D.set_map V.pred_set) [2]
    done
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_R (rel_shapeV A) (rel_shapeV B) (rel_shapeV C) r1 r2"
    and invar: "pred_R (invar_shapeV u1) (invar_shapeV u1) (invar_shapeV u1) r1"
    "pred_R (invar_shapeV u2) (invar_shapeV u2) (invar_shapeV u2) r2"
  shows "rel_raw (rel_D A B C) (f_raw u1 r1) (f_raw u2 r2)"
  using args depth invar
proof (coinduction arbitrary: u1 u2 r1 r2 rule: raw.rel_coinduct)
  case (Eq_raw a b)
  note defobj = 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 Eq_raw show ?case
    by (force simp: list.rel_eq
        G.rel_map R.rel_map R.pred_map
        cong: R.pred_cong
        elim!: G.rel_mono_strong R.rel_mono_strong
        dest!:
        defobj_invar[THEN pred_funD, unfolded G.pred_set, THEN conjunct1,
          THEN bspec, rotated -1]
        defobj_invar[THEN pred_funD, unfolded G.pred_set, THEN conjunct2,
          THEN bspec, rotated -1]
        intro!: G.rel_mono_strong[OF defobj])
qed
  
lemma f_transfer:
  assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
  shows "rel_fun (rel_R A B C) (rel_T (rel_D A B C)) f f"
  unfolding f_def rel_fun_def o_apply rel_T_def vimage2p_def
  by (subst (1 2) Abs_T_inverse)
    (auto simp: R.pred_map R.pred_True R.rel_map
      Abs_T_inverse cong: R.pred_cong
      intro!: invar_f_raw f_raw_transfer[OF bi_unique])
    
lemma "f r = T (map_G id (map_T argobj o f) (defobj r))"
  apply (simp only: f_def map_T_def T_def o_apply G.map_comp id_apply cong: G.map_cong)
  apply (subst (1 2) Abs_T_inverse)
  apply ((simp only: mem_Collect_eq Rep_T[unfolded mem_Collect_eq] R.pred_map R.pred_True
        o_apply invar_shapeV_depth_iff shapeV.inject simp_thms invar_f_raw invar_map_closed
        cong: R.pred_cong)+) [2]
  apply (subst f_raw.ctr)
  apply (auto simp: G.map_comp D.map_comp R.map_comp invar_simps
      G.pred_map R.pred_map V.pred_map V.pred_True R.pred_True D.map_ident
      defobj_natural[of LeafV _ LeafV LeafV, unfolded inj_on_def, simplified]
      invar_map_closed  invar_f_raw invar_flat[of "[]", simplified, THEN mp]
      cong: G.pred_cong R.pred_cong V.pred_cong D.map_cong R.map_cong
      intro!: iffD2[OF Abs_T_inject] G.map_cong[OF refl]
      G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]
      trans[OF _ sym[OF f_raw_flat]])
  done
    
hide_const (open) f
  
section ‹Coinduction›
  
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
    
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 ⇒ 'a T ⇒ bool"
axiomatization where 
  Q_param: "⋀(R :: 'a ⇒ 'a' ⇒ bool). bi_unique R ⟹ left_total R ⟹
    rel_fun (rel_T R) (rel_fun (rel_T R) op ⟶) Q Q" and
  Q_coind: "Q ≤ BNF_Def.vimage2p un_T un_T (rel_G op = Q)"
  
lemma Q_map_T_inj:
  assumes "inj f"
  shows "Q t1 t2 ⟶ Q (map_T f t1) (map_T f t2)"
  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
    
definition Qrr where 
  "Qrr r1 r2 ul = ((invar (rev ul) r1 ∧ invar (rev ul) r2) ∧ Q (Abs_T (cimmerse ul r1)) (Abs_T (cimmerse ul r2)))"
  
theorem Qr_un_Cons:
  "Qrr r1 r2 ul ⟹
    rel_G op = (λx y. Q (Abs_T x) (Abs_T y))
    (map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r1))
    (map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r2))"
  apply (unfold un_Cons_cimmerse[symmetric] Qrr_def rev.simps)
  apply (erule conjE)+
  apply (drule vimage2pD[OF predicate2D[OF Q_coind]])
  apply (drule invar_cimmerse)
  apply (drule invar_cimmerse)
  apply (hypsubst_thin |
      drule mp[OF Q_map_T_inj[of Node], rotated -1] |
      drule bspec, assumption |
      erule G.rel_mono_strong conjE exE |
      rule allI impI ballI |
      simp only:
      G.rel_map un_T_def Abs_T_inverse map_T_def invar_cimmerse rev.simps
      mem_Collect_eq 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: 
  fixes r1 r2 :: "'a shape raw"  
  shows "Ex (Qrr r1 r2) ⟹ r1 = r2"
  apply (erule raw.coinduct[of "λr1 r2. Ex (Qrr r1 r2)"], unfold unCons_def)
  apply (erule exE)
  apply (frule Qr_un_Cons[rotated -1])
  apply (unfold Qrr_def)
  apply (drule conjunct1)
  apply (hypsubst_thin |
      erule G.rel_mono_strong cimmerse_shape_inj[rotated -1] conjE |
      rule allI impI |
      drule bspec, assumption |
      simp only: G.rel_map id_apply invar_simps G.pred_set raw.inject rev_snoc split: raw.splits |
      rule exI, rule conjI[rotated], assumption)+
  done
    
theorem T_coind: "(Q::'a T ⇒ 'a T ⇒ bool) ≤ op ="
  apply (rule predicate2I)
  subgoal for x y
    apply (rule Abs_T_cases[of x])
    apply (rule Abs_T_cases[of y])
    apply hypsubst_thin
    apply (rule iffD2[OF Abs_T_inject])
    apply assumption
    apply assumption
    apply (rule raw.inj_map_strong[of _ _ Leaf Leaf])
    apply (simp only: shape.inject(1))
    apply (rule Qrr)
    apply (drule mp[OF Q_map_T_inj[of Leaf], rotated -1])
    apply (simp only: inj_on_def shape.inject simp_thms ball_simps)
    apply (rule exI[of _ "[]"])
    apply (simp only: Qrr_def invar_map_closed cimmerse.simps
        map_T_def Abs_T_inverse o_apply mem_Collect_eq rev.simps(1))
    done
  done
    
end