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
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›
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)
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
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
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
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)
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
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-
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