theory Nonuniform_Datatype
imports "~~/src/HOL/Library/BNF_Axiomatization"
begin
primrec snoc where
"snoc x [] = [x]"
| "snoc x (y # xs) = y # snoc x xs"
lemma snoc_neq_Nil: "snoc x xs ≠ []"
by (cases xs; simp)
lemma snoc: "snoc x xs = xs @ [x]"
by (induct xs) auto
lemma rev_Cons: "rev (x # xs) = snoc x (rev xs)"
by (auto simp: snoc)
lemma rev_snoc: "rev (snoc x xs) = x # rev xs"
by (auto simp: snoc)
lemma vimage2p_eq_onp: "inj f ⟹ BNF_Def.vimage2p f f (eq_onp S) = eq_onp (S o f)"
unfolding vimage2p_def eq_onp_def inj_on_def by auto
lemma vimage2pD: "BNF_Def.vimage2p f g R x y ⟹ R (f x) (g y)"
unfolding vimage2p_def .
lemma eq_onpD: "eq_onp S x x ⟹ S x"
unfolding eq_onp_def by simp
lemma bi_unique_Grp: "bi_unique (BNF_Def.Grp A f) = inj_on f A"
unfolding bi_unique_def Grp_def inj_on_def by auto
lemma bi_unique_eq_onp: "bi_unique (eq_onp P)"
unfolding eq_onp_def bi_unique_def by simp
lemma fun_pred_rel: "pred_fun A B x = rel_fun (eq_onp A) (eq_onp B) x x"
unfolding pred_fun_def rel_fun_def eq_onp_def by auto
lemma pred_funD: "pred_fun A B f ⟹ A x ⟹ B (f x)"
unfolding pred_fun_def by auto
section ‹Input›
declare [[bnf_internals, typedef_overloaded]]
bnf_axiomatization 'a F
bnf_axiomatization ('a, 'x) G [wits: "'a ⇒ ('a, 'x) G"]
section ‹Raw Type›
datatype label = F
type_synonym depth = "label list"
datatype 'a shape = Leaf 'a | Node "'a shape F"
datatype 'a raw = Cons "('a shape, 'a raw) G"
abbreviation "un_Leaf u ≡ case u of Leaf x ⇒ x"
abbreviation "un_Node u ≡ case u of Node x ⇒ x"
abbreviation "un_Cons t ≡ case t of Cons x ⇒ x"
section ‹Invariant›
primrec invar_shape :: "depth ⇒ 'a shape ⇒ bool" where
"invar_shape u0 (Leaf u) = (case u0 of [] ⇒ True | _ ⇒ False)"
| "invar_shape u0 (Node f1) = (case u0 of F # u0 ⇒ pred_F (invar_shape u0) f1 | _ ⇒ False)"
inductive invar :: "depth ⇒ 'a raw ⇒ bool" where
"pred_G (invar_shape u0) (invar (F # u0)) g ⟹ invar u0 (Cons g)"
monos G.pred_mono
lemmas invar_simps = invar.simps[of _ "Cons _", unfolded simp_thms(39,40) ex_simps raw.inject]
section ‹The Type›
definition "wit x = Cons (wit_G (Leaf x))"
lemma invar_wit: "invar [] (wit x)"
by (auto simp only:
wit_def invar_simps invar_shape.simps G.pred_map o_def id_apply G.pred_set
G.set_map list.case dest: G.wit)
typedef 'a T = "{t :: 'a raw. invar [] t}"
by (rule exI[of _ "wit undefined"]) (auto simp only: invar_wit)
section ‹Flat and Unflat›
primrec (transfer)
flat_shape :: "'a F shape ⇒ 'a shape" where
"flat_shape (Leaf f1) = Node (map_F Leaf f1)"
| "flat_shape (Node f1) = Node (map_F flat_shape f1)"
primrec (nonexhaustive)
unflat_shape :: "depth ⇒ 'a shape ⇒ 'a F shape" where
"unflat_shape u0 (Node f1) =
(case u0 of
[] ⇒ Leaf (map_F un_Leaf f1)
| _ # u0 ⇒ Node (map_F (unflat_shape u0) f1))"
primrec (transfer) flat :: "'a F raw ⇒ 'a raw" where
"flat (Cons g) = Cons (map_G flat_shape flat g)"
primrec unflat :: "depth ⇒ 'a raw ⇒ 'a F raw" where
"unflat u0 (Cons g) = Cons (map_G (unflat_shape u0) (unflat (F # u0)) g)"
section ‹Constructor and Selector›
definition T :: "('a, 'a F T) G ⇒ 'a T" where
"T g = Abs_T (Cons (map_G Leaf (flat o Rep_T) g))"
definition un_T :: "'a T ⇒ ('a, 'a F T) G" where
"un_T t = map_G un_Leaf (Abs_T o unflat []) (un_Cons (Rep_T t))"
section ‹BNF Instance›
lemma invar_shape_map_closed_raw:
"∀u0. invar_shape u0 (map_shape f u) ⟷ invar_shape u0 u"
apply (rule shape.induct[of
"λu. ∀u0. invar_shape u0 (map_shape f u) ⟷ invar_shape u0 u" u])
apply (auto simp only:
shape.map invar_shape.simps
F.pred_map
o_apply
elim!: F.pred_mono_strong
split: list.splits label.splits)
done
lemmas invar_shape_map_closed =
spec[OF invar_shape_map_closed_raw]
lemma invar_map_closed_raw:
"∀u0. invar u0 (map_raw f t) ⟷ invar u0 t"
apply (induct t)
apply (auto simp only:
raw.map invar_simps id_apply o_apply
G.pred_map invar_shape_map_closed
elim!: G.pred_mono_strong)
done
lemmas invar_map_closed =
spec[OF invar_map_closed_raw]
lift_bnf 'a T
apply (auto simp only:
invar_map_closed)
done
section ‹Lemmas about Flat, Unflat, Invar›
lemma invar_shape_depth_iff:
"invar_shape [] x = (∃a. x = Leaf a)"
"invar_shape (F # u0) x = (∃y. x = Node y ∧ pred_F (invar_shape u0) y)"
by (cases x; simp add: F.pred_map)+
lemma flat_shape_unflat_shape_raw:
fixes u :: "'a shape"
shows
"∀u0. invar_shape (snoc F u0) u ⟶ flat_shape (unflat_shape u0 u) = u"
apply (rule shape.induct[of
"λu. ∀u0. invar_shape (snoc F u0) u ⟶ flat_shape (unflat_shape u0 u) = u" u])
apply (auto simp only:
unflat_shape.simps flat_shape.simps
invar_shape.simps F.pred_map F.map_comp
shape.case invar_shape_depth_iff snoc.simps snoc_neq_Nil
id_apply o_apply
intro!: trans[OF F.map_cong_pred F.map_ident]
elim!: F.pred_mono_strong
split: list.splits label.splits)
done
lemmas flat_shape_unflat_shape =
mp[OF spec[OF flat_shape_unflat_shape_raw]]
lemma unflat_shape_flat_shape_raw:
fixes u :: "'a F shape"
shows
"∀u0. invar_shape u0 u ⟶ unflat_shape u0 (flat_shape u) = u"
apply (rule shape.induct[of
"λu. ∀u0. invar_shape u0 u ⟶ unflat_shape u0 (flat_shape u) = u" u])
apply (auto simp only:
unflat_shape.simps flat_shape.simps invar_shape.simps
F.pred_map F.map_comp F.pred_True
shape.case
id_apply o_apply refl
intro!: trans[OF F.map_cong_pred F.map_ident]
elim!: F.pred_mono_strong
split: list.splits label.splits)
done
lemmas unflat_shape_flat_shape =
mp[OF spec[OF unflat_shape_flat_shape_raw]]
lemma invar_shape_flat_shape_raw:
fixes u :: "'a F shape"
shows
"∀u0. invar_shape u0 u ⟶ invar_shape (snoc F u0) (flat_shape u)"
apply (rule shape.induct[of
"λu. ∀u0. invar_shape u0 u ⟶ invar_shape (snoc F u0) (flat_shape u)" u])
apply (auto simp only:
flat_shape.simps invar_shape.simps snoc.simps
F.pred_map F.pred_True
id_apply o_apply
elim!: F.pred_mono_strong
intro: F.pred_mono_strong[OF iffD2[OF fun_cong[OF F.pred_True] TrueI]]
split: list.splits label.splits)
done
lemmas invar_shape_flat_shape =
mp[OF spec[OF invar_shape_flat_shape_raw]]
lemma invar_flat_raw: "∀u0. invar u0 x ⟶ invar (snoc F u0) (flat x)"
apply (induct x)
apply (auto simp only:
flat.simps invar_simps snoc.simps[symmetric] invar_shape_flat_shape id_apply o_apply G.pred_map
elim!: G.pred_mono_strong)
done
lemmas invar_flat = mp[OF spec[OF invar_flat_raw]]
lemma invar_shape_unflat_shape_raw:
fixes u :: "'a shape"
shows
"∀u0. invar_shape (snoc F u0) u ⟶ invar_shape u0 (unflat_shape u0 u)"
apply (rule shape.induct[of
"λu. ∀u0. invar_shape (snoc F u0) u ⟶ invar_shape u0 (unflat_shape u0 u)" u])
apply (auto simp only:
unflat_shape.simps invar_shape.simps snoc.simps snoc_neq_Nil
F.pred_map id_apply o_apply refl
elim!: F.pred_mono_strong
split: list.splits label.splits)
done
lemmas invar_shape_unflat_shape =
mp[OF spec[OF invar_shape_unflat_shape_raw]]
lemma invar_unflat_raw: "∀u0. invar (snoc F u0) t ⟶ invar u0 (unflat u0 t)"
apply (induct t)
apply (auto simp only:
unflat.simps invar_simps snoc.simps invar_shape_unflat_shape id_apply o_apply G.pred_map
elim!: G.pred_mono_strong)
done
lemmas invar_unflat = mp[OF spec[OF invar_unflat_raw]]
lemma flat_unflat_raw: "∀u0. invar (snoc F u0) t ⟶ flat (unflat u0 t) = t"
apply (induct t)
apply (auto simp only:
unflat.simps flat.simps invar_simps snoc.simps
flat_shape_unflat_shape id_apply o_apply G.pred_map G.map_comp
intro!: trans[OF G.map_cong_pred G.map_ident]
elim!: G.pred_mono_strong)
done
lemmas flat_unflat = mp[OF spec[OF flat_unflat_raw]]
lemma unflat_flat_raw: "∀u0. invar u0 t ⟶ unflat u0 (flat t) = t"
apply (induct t)
apply (auto simp only:
unflat.simps flat.simps invar_simps unflat_shape_flat_shape id_apply o_apply G.pred_map G.map_comp
intro!: trans[OF G.map_cong_pred G.map_ident]
elim!: G.pred_mono_strong)
done
lemmas unflat_flat = mp[OF spec[OF unflat_flat_raw]]
section ‹Constructor is Bijection›
lemma un_T_T: "un_T (T x) = x"
unfolding T_def un_T_def
apply (subst Abs_T_inverse)
apply (auto simp only:
invar_simps invar_shape.simps list.case id_apply o_apply
snoc.simps(1)[of F, symmetric]
G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
apply (auto simp only:
raw.case shape.case Rep_T_inverse o_apply
G.map_comp G.map_ident Rep_T[unfolded mem_Collect_eq] unflat_flat
intro!: trans[OF G.map_cong G.map_ident]) []
done
lemma T_un_T: "T (un_T x) = x"
unfolding T_def un_T_def G.map_comp o_def
apply (rule iffD1[OF Rep_T_inject])
apply (subst Abs_T_inverse)
apply (auto simp only:
invar_simps invar_shape.simps list.case id_apply o_apply
snoc.simps(1)[of F, symmetric]
G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
apply (insert Rep_T[simplified, of x])
apply (rule raw.exhaust[of "Rep_T x"])
apply (auto simp only:
raw.case shape.case invar_simps invar_shape_depth_iff
snoc.simps(1)[of F, symmetric]
G.pred_map Abs_T_inverse invar_unflat flat_unflat id_apply o_apply mem_Collect_eq
intro!: trans[OF G.map_cong_pred G.map_ident]
elim!: G.pred_mono_strong) []
done
section ‹Characteristic Theorems›
subsection ‹map›
lemma flat_shape_map:
"map_shape f (flat_shape u) = flat_shape (map_shape (map_F f) u)"
apply (rule shape.induct[of
"λu. map_shape f (flat_shape u) = flat_shape (map_shape (map_F f) u)" u])
apply (auto simp only:
shape.map flat_shape.simps F.map_comp o_apply
intro!: F.map_cong0)
done
lemma map_raw_flat: "map_raw f (flat t) = flat (map_raw (map_F f) t)"
apply (induct t)
apply (auto simp only:
raw.map flat.simps G.map_comp flat_shape_map o_apply
intro!: G.map_cong0)
done
lemma map_T: "map_T f (T t) = T (map_G f (map_T (map_F f)) t)"
unfolding map_T_def T_def o_apply
apply (subst Abs_T_inverse)
apply (auto simp only:
invar_simps invar_shape.simps list.case id_apply o_apply
snoc.simps(1)[of F, symmetric]
G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
apply (auto simp only:
raw.map shape.map G.map_comp o_apply mem_Collect_eq
invar_map_closed Abs_T_inverse Rep_T[unfolded mem_Collect_eq] map_raw_flat
intro!: arg_cong[of _ _ "λx. Abs_T (raw.Cons x)"] G.map_cong0) []
done
subsection ‹set›
lemma flat_shape_set:
fixes u :: "'a F shape"
shows
"set_shape (flat_shape u) = UNION (set_shape u) set_F"
apply (rule shape.induct[of
"λu. set_shape (flat_shape u) = UNION (set_shape u) set_F" u])
apply (auto simp only:
flat_shape.simps shape.set F.set_map
UN_simps UN_singleton UN_insert UN_empty UN_empty2 UN_Un UN_Un_distrib Un_ac Un_empty_left
cong: SUP_cong)
done
lemma set_raw_flat:
"set_raw (flat t) = UNION (set_raw t) set_F"
apply (induct t)
apply (auto simp only:
flat.simps raw.set shape.set G.set_map flat_shape_set
UN_simps UN_Un UN_Un_distrib Un_ac
cong: SUP_cong)
done
lemma set_T: "set_T (T g) = set1_G g ∪
(⋃(set_F ` (⋃(set_T ` (set2_G g)))))"
unfolding set_T_def T_def o_apply
apply -
apply (subst Abs_T_inverse)
apply (auto simp only:
invar_simps invar_shape.simps list.case id_apply o_apply
snoc.simps(1)[of F, symmetric]
G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) []
apply (auto simp only:
raw.set shape.set G.set_map set_raw_flat o_apply
UN_simps UN_singleton UN_empty2 UN_Un UN_Un_distrib Un_ac Un_empty_left
cong: SUP_cong) []
done
subsection ‹rel›
lemma flat_shape_rel_raw:
"(∀u0 u'. invar_shape u0 u ⟶ invar_shape u0 u' ⟶ rel_shape R (flat_shape u) (flat_shape u') ⟶
rel_shape (rel_F R) u u')"
apply (rule shape.induct[of
"λu. ∀u0 u'. invar_shape u0 u ⟶ invar_shape u0 u' ⟶ rel_shape R (flat_shape u) (flat_shape u') ⟶
rel_shape (rel_F R) u u'"
u])
apply (auto 0 4 simp only:
invar_shape.simps flat_shape.simps shape.rel_inject
invar_shape_depth_iff ball_simps id_apply
F.rel_map pred_F_def F.set_map
elim!: F.rel_mono_strong
split: list.splits label.splits)
done
lemma flat_shape_rel:
"invar_shape u0 u ⟹ invar_shape u0 u' ⟹
rel_shape R (flat_shape u) (flat_shape u') = rel_shape (rel_F R) u u'"
apply (rule iffI[rotated, OF rel_funD[OF flat_shape.transfer]], assumption)
apply (rule mp[OF mp[OF mp[OF spec[OF spec[OF flat_shape_rel_raw]]]]]; assumption)
done
lemma rel_raw_flat_raw:
"∀t' u0. invar u0 t ⟶ invar u0 t' ⟶
rel_raw R (flat t) (flat t') ⟶ rel_raw (rel_F R) t t'"
apply (induct t)
apply (rule allI)
apply (case_tac t')
apply (auto simp only:
invar_simps flat.simps raw.rel_inject G.rel_map G.pred_set flat_shape_rel G.set_map ball_simps id_apply
elim!: G.rel_mono_strong)
done
lemma rel_raw_flat:
"invar u0 t ⟹ invar u0 t' ⟹
rel_raw R (flat t) (flat t') = rel_raw (rel_F R) t t'"
apply (rule iffI[rotated, OF rel_funD[OF flat.transfer]], assumption)
apply (rule mp[OF mp[OF mp[OF spec[OF spec[OF rel_raw_flat_raw]]]]]; assumption)
done
lemma rel_T: "rel_T R (T g) (T g') = rel_G R (rel_T (rel_F R)) g g'"
unfolding rel_T_def T_def vimage2p_def
apply (subst (1 2) Abs_T_inverse)
apply (auto simp only:
invar_simps invar_shape.simps list.case id_apply o_apply
snoc.simps(1)[of F, symmetric]
G.pred_map G.pred_True G.map_comp Rep_T[unfolded mem_Collect_eq] invar_flat
intro!: G.pred_mono_strong[OF iffD2[OF fun_cong[OF G.pred_True] TrueI]]) [2]
apply (simp only:
raw.rel_inject G.rel_map shape.rel_inject o_apply
rel_raw_flat[OF Rep_T[unfolded mem_Collect_eq] Rep_T[unfolded mem_Collect_eq]])
done
section ‹Recursion›
bnf_axiomatization 'a V
datatype 'a shapeV = LeafV 'a | NodeV "'a shapeV V"
abbreviation "un_LeafV u ≡ case u of LeafV x ⇒ x"
abbreviation "un_NodeV u ≡ case u of NodeV x ⇒ x"
primrec invar_shapeV :: "depth ⇒ 'a shapeV ⇒ bool" where
"invar_shapeV u0 (LeafV u) = (case u0 of [] ⇒ True | _ ⇒ False)"
| "invar_shapeV u0 (NodeV f1) = (case u0 of F # u0 ⇒ pred_V (invar_shapeV u0) f1 | _ ⇒ False)"
primrec (transfer)
flat_shapeV :: "'a V shapeV ⇒ 'a shapeV" where
"flat_shapeV (LeafV f1) = NodeV (map_V LeafV f1)"
| "flat_shapeV (NodeV f1) = NodeV (map_V flat_shapeV f1)"
primrec (nonexhaustive)
unflat_shapeV :: "depth ⇒ 'a shapeV ⇒ 'a V shapeV" where
"unflat_shapeV u0 (NodeV f1) =
(case u0 of
[] ⇒ LeafV (map_V un_LeafV f1)
| _ # u0 ⇒ NodeV (map_V (unflat_shapeV u0) f1))"
lemma invar_shapeV_map_closed_raw:
"∀u0. invar_shapeV u0 (map_shapeV f u) ⟷ invar_shapeV u0 u"
apply (rule shapeV.induct[of
"λu. ∀u0. invar_shapeV u0 (map_shapeV f u) ⟷ invar_shapeV u0 u" u])
apply (auto simp only:
shapeV.map invar_shapeV.simps
V.pred_map
o_apply
elim!: V.pred_mono_strong
split: list.splits label.splits)
done
lemmas invar_shapeV_map_closed =
spec[OF invar_shapeV_map_closed_raw]
lemma invar_shapeV_depth_iff:
"invar_shapeV [] x = (∃a. x = LeafV a)"
"invar_shapeV (F # u0) x = (∃y. x = NodeV y ∧ pred_V (invar_shapeV u0) y)"
by (cases x; simp add: V.pred_map)+
lemma flat_shapeV_unflat_shapeV_raw:
fixes u :: "'a shapeV"
shows
"∀u0. invar_shapeV (snoc F u0) u ⟶ flat_shapeV (unflat_shapeV u0 u) = u"
apply (rule shapeV.induct[of
"λu. ∀u0. invar_shapeV (snoc F u0) u ⟶ flat_shapeV (unflat_shapeV u0 u) = u" u])
apply (auto simp only:
unflat_shapeV.simps flat_shapeV.simps
invar_shapeV.simps V.pred_map V.map_comp
shapeV.case invar_shapeV_depth_iff snoc.simps snoc_neq_Nil
id_apply o_apply
intro!: trans[OF V.map_cong_pred V.map_ident]
elim!: V.pred_mono_strong
split: list.splits label.splits)
done
lemmas flat_shapeV_unflat_shapeV =
mp[OF spec[OF flat_shapeV_unflat_shapeV_raw]]
lemma unflat_shapeV_flat_shapeV_raw:
fixes u :: "'a V shapeV"
shows
"∀u0. invar_shapeV u0 u ⟶ unflat_shapeV u0 (flat_shapeV u) = u"
apply (rule shapeV.induct[of
"λu. ∀u0. invar_shapeV u0 u ⟶ unflat_shapeV u0 (flat_shapeV u) = u" u])
apply (auto simp only:
unflat_shapeV.simps flat_shapeV.simps invar_shapeV.simps
V.pred_map V.map_comp V.pred_True
shapeV.case
id_apply o_apply refl
intro!: trans[OF V.map_cong_pred V.map_ident]
elim!: V.pred_mono_strong
split: list.splits label.splits)
done
lemmas unflat_shapeV_flat_shapeV =
mp[OF spec[OF unflat_shapeV_flat_shapeV_raw]]
lemma invar_shapeV_flat_shapeV_raw:
fixes u :: "'a V shapeV"
shows
"∀u0. invar_shapeV u0 u ⟶ invar_shapeV (snoc F u0) (flat_shapeV u)"
apply (rule shapeV.induct[of
"λu. ∀u0. invar_shapeV u0 u ⟶ invar_shapeV (snoc F u0) (flat_shapeV u)" u])
apply (auto simp only:
flat_shapeV.simps invar_shapeV.simps snoc.simps
V.pred_map V.pred_True
id_apply o_apply
elim!: V.pred_mono_strong
intro: V.pred_mono_strong[OF iffD2[OF fun_cong[OF V.pred_True] TrueI]]
split: list.splits label.splits)
done
lemmas invar_shapeV_flat_shapeV =
mp[OF spec[OF invar_shapeV_flat_shapeV_raw]]
lemma invar_shapeV_unflat_shapeV_raw:
fixes u :: "'a shapeV"
shows
"∀u0. invar_shapeV (snoc F u0) u ⟶ invar_shapeV u0 (unflat_shapeV u0 u)"
apply (rule shapeV.induct[of
"λu. ∀u0. invar_shapeV (snoc F u0) u ⟶ invar_shapeV u0 (unflat_shapeV u0 u)" u])
apply (auto simp only:
unflat_shapeV.simps invar_shapeV.simps snoc.simps snoc_neq_Nil
V.pred_map id_apply o_apply refl
elim!: V.pred_mono_strong
split: list.splits label.splits)
done
lemmas invar_shapeV_unflat_shapeV =
mp[OF spec[OF invar_shapeV_unflat_shapeV_raw]]
bnf_axiomatization ('a, 'b, 'c) R
bnf_axiomatization ('a, 'b, 'c) D
consts defobj :: "(('a, 'b, 'c) D, ('a V, 'b V, 'c V) R) G ⇒ ('a, 'b, 'c) R"
consts argobj :: "('a, 'b, 'c) D F ⇒ ('a V, 'b V, 'c V) D"
axiomatization where
defobj_transfer: "⋀A B C.
bi_unique A ⟹ bi_unique B ⟹ bi_unique C ⟹
rel_fun (rel_G (rel_D A B C) (rel_R (rel_V A) (rel_V B) (rel_V C))) (rel_R A B C) defobj defobj" and
argobj_transfer: "⋀A B C.
bi_unique A ⟹ bi_unique B ⟹ bi_unique C ⟹
rel_fun (rel_F (rel_D A B C)) (rel_D (rel_V A) (rel_V B) (rel_V C)) argobj argobj"
lemma defobj_invar: "pred_fun (pred_G (pred_D A B C) (pred_R (pred_V A) (pred_V B) (pred_V C))) (pred_R A B C) defobj"
unfolding fun_pred_rel G.rel_eq_onp[symmetric] F.rel_eq_onp[symmetric]
D.rel_eq_onp[symmetric] R.rel_eq_onp[symmetric] V.rel_eq_onp[symmetric]
by (rule defobj_transfer; rule bi_unique_eq_onp)
lemma argobj_invar: "pred_fun (pred_F (pred_D A B C)) (pred_D (pred_V A) (pred_V B) (pred_V C)) argobj"
unfolding fun_pred_rel F.rel_eq_onp[symmetric] D.rel_eq_onp[symmetric] V.rel_eq_onp[symmetric]
by (rule argobj_transfer; rule bi_unique_eq_onp)
lemma defobj_natural:
"inj_on a (⋃(set1_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set1_R ` set2_G x))) ⟹
inj_on b (⋃(set2_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set2_R ` set2_G x))) ⟹
inj_on c (⋃(set3_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set3_R ` set2_G x))) ⟹
defobj (map_G (map_D a b c) (map_R (map_V a) (map_V b) (map_V c)) x) = map_R a b c (defobj x)"
using rel_funD[OF defobj_transfer, of
"BNF_Def.Grp (⋃(set1_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set1_R ` set2_G x))) a"
"BNF_Def.Grp (⋃(set2_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set2_R ` set2_G x))) b"
"BNF_Def.Grp (⋃(set3_D ` set1_G x) ∪ ⋃(set_V ` ⋃(set3_R ` set2_G x))) c"]
unfolding F.rel_Grp R.rel_Grp D.rel_Grp G.rel_Grp V.rel_Grp bi_unique_Grp
by (force simp add: Grp_def)
lemma argobj_natural:
"inj_on a (⋃(set1_D ` set_F x)) ⟹
inj_on b (⋃(set2_D ` set_F x)) ⟹
inj_on c (⋃(set3_D ` set_F x)) ⟹
argobj (map_F (map_D a b c) x) = map_D (map_V a) (map_V b) (map_V c) (argobj x)"
using rel_funD[OF argobj_transfer, of "BNF_Def.Grp (⋃(set1_D ` set_F x)) a" "BNF_Def.Grp (⋃(set2_D ` set_F x)) b" "BNF_Def.Grp (⋃(set3_D ` set_F x)) c"]
unfolding F.rel_Grp R.rel_Grp D.rel_Grp V.rel_Grp bi_unique_Grp
by (auto simp add: Grp_def)
lemma argobj_flat_shape_natural: fixes x :: "('a V shapeV, 'b V shapeV, 'c V shapeV) D F"
shows
"pred_F (pred_D (invar_shapeV u) (invar_shapeV u) (invar_shapeV u)) x ⟹
argobj (map_F (map_D flat_shapeV flat_shapeV flat_shapeV) x) =
map_D (map_V flat_shapeV) (map_V flat_shapeV) (map_V flat_shapeV) (argobj x)"
apply (rule argobj_natural; rule inj_onI;
rule box_equals[OF _ unflat_shapeV_flat_shapeV[of u] unflat_shapeV_flat_shapeV[of u]])
apply (auto simp only: F.pred_set D.pred_set)
done
lemma defobj_flat_shape_natural: fixes x :: "(('a V shapeV, 'b V shapeV, 'c V shapeV) D, ('a V shapeV V, 'b V shapeV V, 'c V shapeV V) R) G"
shows
"pred_G (pred_D (invar_shapeV u) (invar_shapeV u) (invar_shapeV u)) (pred_R (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u)) (pred_V (invar_shapeV u))) x ⟹
defobj (map_G (map_D flat_shapeV flat_shapeV flat_shapeV) (map_R (map_V flat_shapeV) (map_V flat_shapeV) (map_V flat_shapeV)) x) = map_R flat_shapeV flat_shapeV flat_shapeV (defobj x)"
apply (rule defobj_natural; rule inj_onI;
rule box_equals[OF _ unflat_shapeV_flat_shapeV[of u] unflat_shapeV_flat_shapeV[of u]])
apply (auto simp only: F.pred_set G.pred_set D.pred_set R.pred_set V.pred_set)
done
primrec f_shape :: "depth ⇒ ('a, 'b, 'c) D shape ⇒ ('a shapeV, 'b shapeV, 'c shapeV) D" where
"f_shape [] = map_D LeafV LeafV LeafV o un_Leaf"
| "f_shape (_ # u0) = map_D NodeV NodeV NodeV o argobj o map_F (f_shape u0) o un_Node"
primrec f_raw :: "depth ⇒ ('a, 'b, 'c) D raw ⇒ ('a shapeV, 'b shapeV, 'c shapeV) R" where
"f_raw u0 (Cons g) =
defobj (map_G (f_shape u0) (map_R un_NodeV un_NodeV un_NodeV o f_raw (F # u0)) g)"
definition f :: "('a, 'b, 'c) D T ⇒ ('a, 'b, 'c) R" where
"f = map_R un_LeafV un_LeafV un_LeafV o f_raw [] o Rep_T"
lemma invar_shape_f_shape[THEN spec, THEN mp]:
"∀u. invar_shape u0 u ⟶ pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_shape u0 u)"
apply (rule list.induct[of "λu0. ∀u. invar_shape u0 u ⟶ pred_D (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_shape u0 u)" u0])
apply (auto simp only: f_shape.simps o_apply D.pred_map
invar_shape.simps invar_shapeV.simps list.case D.pred_True
cong: D.pred_cong) []
subgoal for x xs
apply (cases x)
apply (auto simp only: invar_shape_depth_iff shape.case
invar_shapeV.simps f_shape.simps D.pred_map D.pred_True o_apply
simp_thms all_simps imp_conjL list.inject list.distinct F.pred_map
intro!: pred_funD[OF argobj_invar]
elim!: F.pred_mono_strong
cong: D.pred_cong
split: list.splits label.splits)
done
done
lemma f_shape_flat_shape[THEN spec, THEN mp]: "∀x. invar_shape u0 x ⟶
f_shape (snoc F u0) (flat_shape x) = map_D flat_shapeV flat_shapeV flat_shapeV (f_shape u0 (map_shape argobj x))"
apply (rule list.induct[of "λu0. ∀x. invar_shape u0 x ⟶ f_shape (snoc F u0) (flat_shape x) = map_D flat_shapeV flat_shapeV flat_shapeV (f_shape u0 (map_shape argobj x))" u0])
apply (auto simp only: flat_shape.simps flat_shapeV.simps f_shape.simps
invar_shape_depth_iff shape.case
snoc.simps shape.map D.map_comp F.map_comp argobj_natural inj_on_def shapeV.inject
o_apply simp_thms Ball_def cong: F.map_cong D.map_cong) []
apply (rule allI)
subgoal premises IH for x xs u
apply (rule impI)
apply (cases x)
apply (unfold flat_shape.simps flat_shapeV.simps f_shape.simps shape.map D.map_comp o_def)
apply (auto simp only: D.map_comp[unfolded o_def, symmetric]
F.set_map F.map_comp F.pred_set o_apply
invar_shape_map_closed invar_shape_f_shape invar_shape_depth_iff snoc.simps
f_shape.simps flat_shape.simps shape.map shape.case
intro!: arg_cong[of _ _ argobj] D.map_cong F.map_cong
IH[THEN spec, THEN mp]
trans[OF _ argobj_flat_shape_natural[of xs]]
elim!: F.pred_mono_strong
split: list.splits label.splits)
done
done
lemma invar_f_raw[THEN spec, THEN mp]:
"∀u0. invar u0 x ⟶ pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_raw u0 x)"
apply (rule raw.induct[of "λx. ∀u0. invar u0 x ⟶ pred_R (invar_shapeV u0) (invar_shapeV u0) (invar_shapeV u0) (f_raw u0 x)" x])
apply (rule allI)
subgoal premises IH for g u0
apply (auto simp only: invar_simps raw.map f_raw.simps G.map_comp o_apply G.pred_map R.pred_map
invar_shape_map_closed invar_shapeV_depth_iff shapeV.case
intro!: pred_funD[OF defobj_invar[of "invar_shapeV u0" "invar_shapeV u0" "invar_shapeV u0"]] invar_shape_f_shape
R.pred_mono_strong[OF mp[OF spec[OF IH, of _ "F # u0"]]]
elim!: G.pred_mono_strong
cong: G.map_cong)
done
done
lemma f_raw_flat[THEN spec, THEN mp]:
"∀u0. invar u0 x ⟶ f_raw (snoc F u0) (flat x) = map_R flat_shapeV flat_shapeV flat_shapeV (f_raw u0 (map_raw argobj x))"
apply (rule raw.induct[of "λx. ∀u0. invar u0 x ⟶ f_raw (snoc F u0) (flat x) = map_R flat_shapeV flat_shapeV flat_shapeV (f_raw u0 (map_raw argobj x))" x])
apply (rule allI)
subgoal premises IH for g u0
apply (auto simp only: flat.simps f_raw.simps G.map_comp o_apply
f_shape_flat_shape raw.map invar_map_closed
invar_simps G.pred_set G.set_map mp[OF spec[OF IH, of _ "F # u0"], simplified]
R.map_comp invar_shapeV_depth_iff shapeV.case flat_shapeV.simps invar_shape_map_closed R.pred_map
intro!: arg_cong[of _ _ defobj] G.map_cong0 R.map_cong_pred invar_shape_f_shape
R.pred_mono_strong[OF invar_f_raw[of "F # u0"]]
trans[OF _ defobj_flat_shape_natural[of u0]] f_shape_flat_shape[of u0])
done
done
lemma f_shape_transfer:
assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
and depth: "list_all2 op = u1 u2"
and args: "rel_shape (rel_D A B C) s1 s2"
and invar: "invar_shape u1 s1" "invar_shape u2 s2"
shows "rel_D (rel_shapeV A) (rel_shapeV B) (rel_shapeV C)
(f_shape u1 s1) (f_shape u2 s2)"
using depth args invar proof (induct u1 u2 arbitrary: s1 s2 rule: list.rel_induct)
case Nil
then show ?case by (auto simp: invar_shape_depth_iff D.rel_map)
next
case (Cons a21 a22 b21 b22)
note [intro!] = argobj_transfer[OF
shapeV.bi_unique_rel[OF bi_unique(1)]
shapeV.bi_unique_rel[OF bi_unique(2)]
shapeV.bi_unique_rel[OF bi_unique(3)], THEN rel_funD]
from Cons show ?case by (cases b21) (auto simp:
invar_shape_depth_iff D.rel_map F.rel_map F.pred_set
elim!: F.rel_mono_strong)
qed
lemma f_raw_transfer:
assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
and depth: "list_all2 op = u1 u2"
and args: "rel_raw (rel_D A B C) r1 r2"
and invar: "invar u1 r1" "invar u2 r2"
shows "rel_R (rel_shapeV A) (rel_shapeV B) (rel_shapeV C)
(f_raw u1 r1) (f_raw u2 r2)"
using args depth invar proof (induct r1 r2 arbitrary: u1 u2 rule: raw.rel_induct)
case (Cons a b)
note [intro!] = defobj_transfer[OF
shapeV.bi_unique_rel[OF bi_unique(1)]
shapeV.bi_unique_rel[OF bi_unique(2)]
shapeV.bi_unique_rel[OF bi_unique(3)], THEN rel_funD]
f_shape_transfer[OF bi_unique]
from Cons show ?case
by (force simp: list.rel_eq invar_simps invar_shapeV_depth_iff
G.rel_map G.pred_set R.rel_map
elim!: G.rel_mono_strong R.rel_mono_strong
dest!: spec[of _ "F # u2"]
dest: conjunct1[OF invar_f_raw[unfolded R.pred_set], THEN bspec, rotated -1]
conjunct1[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1]
conjunct2[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1])
qed
lemma f_transfer:
assumes bi_unique: "bi_unique A" "bi_unique B" "bi_unique C"
shows "rel_fun (rel_T (rel_D A B C)) (rel_R A B C) f f"
unfolding f_def rel_fun_def o_apply
by (force simp: R.rel_map Rep_T[simplified] rel_T_def vimage2p_def
invar_shapeV_depth_iff
intro!: R.rel_mono_strong[OF f_raw_transfer[OF bi_unique]]
dest: conjunct1[OF invar_f_raw[unfolded R.pred_set], THEN bspec, rotated -1]
conjunct1[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1]
conjunct2[OF conjunct2[OF invar_f_raw[unfolded R.pred_set]], THEN bspec, rotated -1])
lemma f_ctor: "f (T g) = defobj (map_G id (f o map_T argobj) g)"
apply (simp only: f_def map_T_def T_def o_apply cong: G.map_cong)
apply (subst (1 2) Abs_T_inverse)
apply (simp only: mem_Collect_eq invar_map_closed_raw Rep_T[unfolded mem_Collect_eq])
apply (simp only: mem_Collect_eq invar_simps G.pred_map G.pred_True o_apply
invar_shape.simps list.case invar_flat Rep_T[unfolded mem_Collect_eq] snoc.simps[symmetric]
cong: G.pred_cong)
apply (auto simp only:
G.map_comp V.map_comp D.map_comp R.map_comp
V.map_ident D.map_ident
G.set_map V.set_map D.set_map R.set_map shape.simps
f_raw.simps f_shape.simps shapeV.case flat_shapeV.simps invar_shapeV_depth_iff
f_raw_flat[OF Rep_T[unfolded mem_Collect_eq], unfolded snoc.simps]
inj_on_def o_apply id_apply
intro!: arg_cong[of _ _ defobj] G.map_cong R.map_cong
trans[OF defobj_natural[of un_LeafV _ un_LeafV un_LeafV, symmetric]]
dest!: bspec[OF conjunct1[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]
bspec[OF conjunct1[OF conjunct2[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]]
bspec[OF conjunct2[OF conjunct2[OF invar_f_raw[OF iffD2[OF invar_map_closed Rep_T[unfolded mem_Collect_eq]], unfolded R.pred_set]]]]
cong: V.map_cong D.map_cong)
done
hide_const (open) f
section ‹Induction›
abbreviation "immerse ul ≡ map_raw Node o unflat (rev ul)"
primrec cimmerse_shape :: "depth ⇒ 'a shape shape ⇒ 'a shape shape" where
"cimmerse_shape [] sh = sh"
| "cimmerse_shape (u # ul) sh = cimmerse_shape ul (map_shape Node (unflat_shape (rev ul) sh))"
primrec cimmerse :: "depth ⇒ 'a shape raw ⇒ 'a shape raw" where
"cimmerse [] r = r"
| "cimmerse (u # ul) r = cimmerse ul (immerse ul r)"
lemma cimmerse_shape_inj[THEN spec, THEN spec, THEN mp, THEN mp, THEN mp]:
"∀sh1 sh2. invar_shape (rev ul) sh1 ⟶ invar_shape (rev ul) sh2 ⟶
cimmerse_shape ul sh1 = cimmerse_shape ul sh2 ⟶ sh1 = sh2"
apply (rule list.induct[of "λul. ∀sh1 sh2. invar_shape (rev ul) sh1 ⟶ invar_shape (rev ul) sh2 ⟶
cimmerse_shape ul sh1 = cimmerse_shape ul sh2 ⟶ sh1 = sh2" ul])
apply (rule allI impI)+
apply (simp only: cimmerse_shape.simps(1) rev.simps(1) id_apply)
subgoal premises prems for u ul
apply (rule label.exhaust[of u])
apply (rule allI impI)+
apply (drule prems[THEN spec, THEN spec, THEN mp, THEN mp, THEN mp, rotated -1]
shape.inj_map_strong[rotated -1] arg_cong[of _ _ flat_shape] |
simp only: cimmerse_shape.simps o_apply rev_Cons shape.inject
invar_shape_map_closed invar_shape_unflat_shape flat_shape_unflat_shape)+
done
done
lemma invar_cimmerse[THEN spec, THEN mp]:
"∀r. invar (rev ul) r ⟶ invar [] (cimmerse ul r)"
apply (rule list.induct[of "λul. ∀r. invar (rev ul) r ⟶ invar [] (cimmerse ul r)" ul])
apply (rule allI impI)+
apply (simp only: cimmerse.simps(1) rev.simps(1) id_apply)
subgoal for u ul
apply (rule label.exhaust[of u])
apply (rule allI impI)+
apply (simp only: cimmerse.simps(2) rev_Cons o_apply invar_map_closed invar_unflat)
done
done
lemma un_Cons_cimmerse[THEN spec]:
"∀r. map_G id (immerse (rev [])) (un_Cons (cimmerse ul r)) =
map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)"
apply (rule list.induct[of "λul. ∀r. map_G id (immerse (rev [])) (un_Cons (cimmerse ul r)) =
map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)" ul])
apply (rule allI)
apply (simp only: cimmerse.simps cimmerse_shape.simps snoc.simps(1) rev.simps id_o id_apply
cong: G.map_cong)
apply (rule allI)
apply (auto simp only: cimmerse.simps cimmerse_shape.simps rev_snoc rev.simps
snoc.simps o_apply id_apply id_o G.map_comp unflat.simps raw.map
cong: G.map_cong split: raw.splits)
done
abbreviation (input) rimplies (infixr "⟵" 25) where
"P ⟵ PP ≡ PP ⟶ P"
lemma
"left_total R ⟹ rel_fun (rel_fun R (op ⟵)) (op ⟵) All All"
unfolding rel_fun_def left_total_def by auto
lemma
"left_total R ⟹ rel_fun (rel_fun R (op ⟶)) (op ⟶) Ex Ex"
unfolding rel_fun_def left_total_def by force
consts Q :: "'a T ⇒ bool"
axiomatization where
Q_param: "⋀(R :: 'a ⇒ 'a' ⇒ bool). bi_unique R ⟹ left_total R ⟹ rel_fun (rel_T R) op ⟵ Q Q" and
Q_ind: "pred_G (λ_. True) Q ≤ Q o T"
lemma reorient_le_o_Abs:
"(⋀x. Abs (Rep x) = x) ⟹ (A :: _ ⇒ _ :: order) ≤ B o Abs ⟹ A o Rep ≤ B"
unfolding le_fun_def o_apply
by (rule allI, rule order_trans, erule spec) auto
lemma Q_map_T_inj:
assumes "inj f"
shows "Q (map_T f t) ⟶ Q t"
using assms Q_param[of "BNF_Def.Grp UNIV f"] unfolding bi_unique_Grp
unfolding rel_fun_def T.rel_Grp left_total_def unfolding Grp_def
by (auto simp: inj_on_def)
abbreviation Qr where
"Qr ul r ≡ Q (Abs_T (cimmerse ul r))"
theorem Qr_un_Cons:
"invar (rev ul) r ⟹ pred_G (λ_. True) (λx. Q (Abs_T x))
(map_G (cimmerse_shape ul) (cimmerse (snoc F ul)) (un_Cons r)) ⟹
Qr ul r"
apply (unfold un_Cons_cimmerse[symmetric] rev.simps(1))
apply (rule predicate1D[OF reorient_le_o_Abs[OF T_un_T Q_ind]])
apply (drule invar_cimmerse)
apply (hypsubst_thin |
rule mp[OF Q_map_T_inj[of Node], rotated -1] |
drule raw.inj_map_strong[rotated -1] |
drule bspec, assumption |
erule conjE exE |
rule allI impI ballI conjI |
simp only: eq_onp_def Abs_T_inject invar_map_closed
G.set_map un_T_def Abs_T_inverse map_T_def invar_cimmerse
mem_Collect_eq ball_simps o_apply id_apply snoc.simps inj_on_def
invar_unflat raw.inject shape.inject shape.case invar_simps G.pred_set invar_shape_depth_iff
split: raw.splits)+
done
theorem Qrr[THEN spec, THEN mp]:
fixes r :: "'a shape raw"
shows "∀ul. invar (rev ul) r ⟶ Qr ul r"
apply (rule raw.induct[of "λr. ∀ul. invar (rev ul) r ⟶ Qr ul r"])
apply (rule allI)
apply (rule impI)
apply (rule Qr_un_Cons, assumption)
apply (hypsubst_thin |
erule cimmerse_shape_inj[rotated -1] conjE |
rule ballI impI |
drule bspec, assumption |
simp only: G.set_map id_apply invar_simps G.pred_set raw.inject rev_snoc shape.rel_eq ball_simps ball_triv simp_thms split: raw.splits |
rule exI, rule conjI[rotated], assumption)+
done
theorem T_ind: "(Q::'a T ⇒ bool) t"
apply (insert Qrr[of "[]" "Rep_T (map_T Leaf t)"])
apply (rule Abs_T_cases[of t])
apply (auto simp only: rev.simps invar_map_closed True_implies_equals
Rep_T_inverse Rep_T[unfolded mem_Collect_eq] inj_on_def shape.inject
simp_thms ball_simps cimmerse.simps eq_onp_def
elim!: mp[OF Q_map_T_inj[of Leaf], rotated])
done
end