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