# Theory Pasting_Diagram

theory Pasting_Diagram
imports Strict_Omega_Category

begin

section ‹The category of pasting diagrams›

text ‹We define the strict $\omega$-category of pasting diagrams, 'pd'. We encode its cells as rooted
trees. First we develop some basic theory of trees.›

subsection ‹Rooted trees›

datatype tree = Node (subtrees: "tree list") ― ‹\cite[p. 268]{Leinster2004}›

abbreviation Leaf :: tree where
"Leaf ≡ Node []"

fun subtree :: "tree ⇒ nat list ⇒ tree" ("_ !t _" [59,60]59) where
"t !t [] = t" |
"t !t (i#xs) = subtrees (t !t xs) ! i"

value "Leaf !t []" (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0]"    (* Node [Leaf, Leaf, Leaf] *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [2,0]"  (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [1]"    (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0,2]"  (* Leaf *)

lemma subtrees_Leaf: "(t = Leaf) = (subtrees t = [])"
by (metis tree.collapse tree.sel)

fun is_subtree_index :: "tree ⇒ nat list ⇒  bool" where
"is_subtree_index t [] = True" |
"is_subtree_index t (i#xs) = (is_subtree_index t xs ∧ i < length (subtrees (t !t xs)))"

lemma subtree_append: "ts ! i !t xs = Node ts !t xs @ [i]"
by (induction xs, auto)

lemma is_subtree_index_append [iff]: "is_subtree_index (Node ts) (xs @ [i]) =
(i < length ts ∧ is_subtree_index (ts!i) xs)"
proof
show "is_subtree_index (Node ts) (xs @ [i]) ⟹ i < length ts ∧ is_subtree_index (ts ! i) xs"
by (induction xs, auto simp: subtree_append)
next
show "i < length ts ∧ is_subtree_index (ts ! i) xs ⟹ is_subtree_index (Node ts) (xs @ [i])"
by (induction xs, auto simp: subtree_append)
qed

lemma is_subtree_index_append' [iff]: "is_subtree_index t (xs @ [i]) =
(is_subtree_index t [i] ∧ is_subtree_index (t !t [i]) xs)"
by (metis is_subtree_index_append is_subtree_index.simps subtree.simps tree.collapse)

lemma max_set_upt [simp]: "Max {0..<Suc n} = n"

lemma length_subtrees_eq_Max: assumes "is_subtree_index t xs" "subtrees (t !t xs) ≠ []"
shows "length (subtrees (t !t xs)) = Suc (Max {i. is_subtree_index t (i # xs)})"
proof -
have "⋀i. is_subtree_index t (i # xs) = (i < length (subtrees (t !t xs)))" using assms(1) by simp
hence "{i. is_subtree_index t (i # xs)} = {0..<length (subtrees (t !t xs))}" by fastforce
moreover have "length (subtrees (t !t xs)) > 0" using assms(2) by simp
ultimately show "length (subtrees (t !t xs)) = Suc (Max {i. is_subtree_index t (i # xs)})"
by (metis max_set_upt gr0_implies_Suc)
qed

lemma tree_eq_iff_subtree_eq: "(t = u) = (length (subtrees t) = length (subtrees u) ∧
(∀i < length (subtrees t). t !t [i] = u !t [i]))"
by (cases t, cases u, auto simp add: list_eq_iff_nth_eq)

text ‹We define the height of a rooted tree. A tree with only one node has height 0. The trees of
height at most n encode the n-cells in 'pd'.›
fun height :: "tree ⇒ nat" where
"height Leaf = 0" |
"height (Node ts) = Suc (fold (max ∘ height) ts 0)"

value "height Leaf"                              (* 0 *)
value "height (Node [Leaf, Leaf])"               (* 1 *)
value "height (Node [Node [Leaf, Leaf], Leaf])"  (* 2 *)
value "height (Node [Node [Leaf, Node [Leaf]]])" (* 3 *)

lemma height_Node [simp]: "ts ≠ [] ⟹ height (Node ts) = Suc (fold (max ∘ height) ts 0)"
by (metis height.simps(2) neq_Nil_conv)

lemma fold_eq_Max [simp]: "ts ≠ [] ⟹ fold (max ∘ height) ts 0 = Max (set (map height ts))"
using Max.set_eq_fold fold_map list.exhaust
by (metis (no_types, lifting) fold_simps(2) map_is_Nil_conv max_nat.right_neutral)

lemma height_Node_Max: "ts ≠ [] ⟹ height (Node ts) = Suc (Max (set (map height ts)))"
by simp

lemma height_Node_pos : "ts ≠ [] ⟹ 0 < height (Node ts)"
proof (induction "Node ts" rule: height.induct)
case 1
then show ?case by blast
next
case (2 t ts')
then show ?case by fastforce
qed

lemma height_exists:
assumes "height (Node ts) = Suc n"
shows "∃t. t ∈ set ts ∧ height t = n"
proof (cases "ts = []")
case True
then show ?thesis using assms by simp
next
case False
hence "n = Max (set (map height ts))" using assms height_Node_Max by force
hence "n ∈ set (map height ts)" using Max_in ts ≠ [] by auto
then show ?thesis by auto
qed

lemma height_lt: assumes "t ∈ set ts" shows "height t < height (Node ts)"
proof -
from assms have nemp: "ts ≠ []" by fastforce
have "height t ≤ Max (set (map height ts))" using assms by fastforce
also have "… = fold (max ∘ height) ts 0" using nemp fold_eq_Max by simp
finally show ?thesis using nemp by simp
qed

lemma height_le_imp_le_Suc:
assumes "∀t ∈ set ts. height t ≤ n"
shows "height (Node ts) ≤ Suc n"
proof (cases "ts = []")
case True
then show ?thesis by simp
next
case False
hence "height (Node ts) = Suc (Max (set (map height ts)))" using height_Node_Max by blast
also have "… ≤ Suc (Max (height  set ts))" using set_map by fastforce
finally show ?thesis using ts ≠ [] assms by simp
qed

lemma height_zero [simp]: "height t = 0 ⟹ t = Leaf"
by (metis height.cases height_Node_pos less_nat_zero_code)

lemma is_subtree_index_length_le: "is_subtree_index t xs ⟹ length xs ≤ height t"
proof (induction xs arbitrary: t rule: rev_induct)
case Nil
then show ?case by force
next
case (snoc i xs)
hence hi: "i < length (subtrees t)" by (metis is_subtree_index_append tree.exhaust_sel)
hence "length xs ≤ height (subtrees t ! i)"
by (metis snoc is_subtree_index_append tree.exhaust_sel)
moreover have "subtrees t ! i ∈ set (subtrees t)" using hi by simp
ultimately show ?case using height_lt by fastforce
qed

lemma height_subtree: "is_subtree_index t xs ⟹ height (t !t xs) ≤ height t - length xs"
proof (induction xs arbitrary: t rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc i xs)
hence "is_subtree_index (t !t [i]) xs" using is_subtree_index_append' by fastforce
hence "height (t !t [i] !t xs) ≤ height (t !t [i]) - length xs" using snoc.IH by blast
moreover have "height (t !t [i]) < height t"
by (metis height_lt is_subtree_index.simps(2) is_subtree_index_append' nth_mem snoc.prems
subtree.simps tree.collapse)
moreover have "t !t [i] !t xs = t !t xs @ [i]" using subtree_append by simp
ultimately show ?case by auto
qed

lemma height_induct: "(⋀t. ∀u. height u < height t ⟶ P u ⟹ P t) ⟹ P t"
by (metis Nat.measure_induct)

lemma subtree_index_induct [case_names Index Step]:
assumes
"is_subtree_index t xs"
"⋀xs. ⟦is_subtree_index t xs; ∀i < length (subtrees (t !t xs)). P (i#xs)⟧ ⟹ P xs"
shows "P xs"
proof -
have hl: "length xs ≤ height t" by (simp add: assms(1) is_subtree_index_length_le)
then show "P xs" using assms
proof (induction "height t - length xs" arbitrary: xs)
case 0
hence "height (t !t xs) = 0" using height_subtree by fastforce
hence "∀i < length (subtrees (t !t xs)). P (i # xs)"
by (metis height_zero length_0_conv less_nat_zero_code tree.sel)
then show ?case using "0.prems" by blast
next
case (Suc n)
have "∀i < length (subtrees (t !t xs)). P (i # xs)"
proof (safe)
fix i assume "i < length (subtrees (t !t xs))"
hence "is_subtree_index t (i # xs)" using Suc(4) by simp
moreover hence "length (i # xs) ≤ height t" using is_subtree_index_length_le by blast
moreover have "n = height t - length (i # xs)" using Suc(2) by simp
ultimately show "P (i # xs)" using Suc(1) Suc(5) by blast
qed
then show ?case using Suc.prems by blast
qed
qed

text ‹The function ‹trim› keeps the first n layers of a tree and removes the remaining ones.›
fun trim :: "nat ⇒ tree ⇒ tree" where
"trim 0 t = Leaf" |
"trim (Suc n) (Node ts) = Node (map (trim n) ts)"

lemma trim_Leaf [simp]: "trim n Leaf = Leaf"
by (metis list.simps(8) trim.elims trim.simps(2))

lemma height_trim_le: "height (trim n t) ≤ n"
proof (induction n t rule: trim.induct)
case (1 t)
then show ?case by auto
next
case (2 n ts)
hence "∀t' ∈ set (map (trim n) ts). height t' ≤ n" by auto
then show ?case using height_le_imp_le_Suc trim.simps(2) by presburger
qed

lemma trim_const: "height t ≤ n ⟹ trim n t = t"
proof (induction n t rule: trim.induct)
case (1 t)
then show ?case using height_zero trim_Leaf by blast
next
case (2 n ts)
hence "⋀t. t ∈ set ts ⟹ trim n t = t" using height_lt by fastforce
hence "map (trim n) ts = ts" using map_idI by blast
then show ?case by fastforce
qed

lemma height_trim_le': "n ≤ height t ⟹ height (trim n t) = n"
proof (induction n t rule: trim.induct)
case (1 t)
then show ?case by fastforce
next
case (2 n ts)
hence "∃m. height (Node ts) = Suc m" by presburger
then obtain m where hm: "height (Node ts) = Suc m" by presburger
then obtain t where ht: "t ∈ set ts ∧ height t = m" using height_exists by meson
have "n ≤ m" using 2 hm by fastforce
hence hn: "height (trim n t) = n" using 2 ht by blast
have "trim n t ∈ set (subtrees (trim (Suc n) (Node ts)))" using ht by simp
then show ?case using hn height_lt by (metis height_trim_le leD le_SucE tree.collapse)
qed

lemma height_trim: "height (trim n t) = (if n ≤ height t then n else height t)"
using height_trim_le' trim_const by auto

value "trim 1 Leaf"
value "trim 1 (Node [Leaf, Leaf])"
value "trim 2 (Node [Node [Leaf, Leaf], Leaf])"
value "trim 1 (Node [Node [Leaf, Node [Leaf]], Node [Leaf]])"

lemma trim_trim' [simp]: "trim n ∘ trim n = trim n"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case apply (simp add: fun_eq_iff) proof
fix t
show "trim (Suc n) (trim (Suc n) t) = trim (Suc n) t"
using Suc by (metis list.map_comp tree.exhaust trim.simps(2))
qed
qed

lemma trim_trim_Suc [simp]: "trim n ∘ trim (Suc n) = trim n"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case apply (simp add: fun_eq_iff) proof
fix t
show "trim (Suc n) (trim (Suc (Suc n)) t) = trim (Suc n) t"
using Suc by (metis list.map_comp tree.exhaust trim.simps(2))
qed
qed

lemma trim_trim [simp]: "n ≤ m ⟹ trim n ∘ trim m = trim n"
proof (induction m arbitrary: n)
case 0
then show ?case by force
next
case (Suc m)
then show ?case proof (cases "n = Suc m")
case True
then show ?thesis by auto
next
case False
hence "n ≤ m" using Suc.prems by auto
hence ih: "trim n = trim n ∘ trim m" using Suc by presburger
hence "trim n ∘ trim (Suc m) = (trim n ∘ trim m) ∘ trim (Suc m)" by simp
also have "… = trim n ∘ trim m" by (metis fun.map_comp trim_trim_Suc)
finally show ?thesis using ih by auto
qed
qed

lemma trim_eq_imp_trim_eq [simp]: "⟦n ≤ m; trim m t = trim m u⟧ ⟹ trim n t = trim n u"
by (metis trim_trim comp_apply)

lemma trim_1_eq: assumes "trim 1 (Node ts) = trim 1 (Node us)" shows "length ts = length us"
proof -
have "⋀vs. trim 1 (Node vs) = Node (map (λx. Leaf) vs)" by force
then show ?thesis using assms map_eq_imp_length_eq by auto
qed

lemma length_subtrees_trim_Suc: "length (subtrees (trim (Suc n) t)) = length (subtrees t)"
by (induction t, simp)

lemma trim_eq_Leaf: "trim n t = Leaf ⟹ n = 0 ∨ t = Leaf"
by (induction n t rule: trim.induct, simp_all)

lemma map_eq_imp_pairs_eq: "map f xs = map g ys ⟹ (⋀x y. (x, y) ∈ set (zip xs ys) ⟹ f x = g y)"
by (metis fst_eqD in_set_zip nth_map snd_eqD)

lemma trim_eq_subtree_eq:
assumes "trim (Suc n) (Node ts) = trim (Suc n) (Node us)"
shows "⋀t u. (t, u) ∈ set (zip ts us) ⟹ trim n t = trim n u"
proof -
fix t u assume "(t, u) ∈ set (zip ts us)"
moreover from assms have "map (trim n) ts = map (trim n) us" by fastforce
ultimately show "trim n t = trim n u" using map_eq_imp_pairs_eq by fast
qed

lemma pairs_eq_imp_map_eq:
assumes "length xs = length ys" "∀(x, y) ∈ set (zip xs ys). f x = g y"
shows "map f xs = map g ys"
proof -
have "⋀x y. (x, y) ∈ set (zip (map f xs) (map g ys)) ⟹ x = y" proof -
fix x y assume h: "(x, y) ∈ set (zip (map f xs) (map g ys))"
hence "∃n. (map f xs)!n = x ∧ (map g ys)!n = y ∧ n < length xs ∧ n < length ys"
by (metis in_set_zip fst_conv length_map snd_conv)
then obtain n where hn: "(map f xs)!n = x" "(map g ys)!n = y" "n < length xs" "n < length ys"
by blast
hence "(xs!n, ys!n) ∈ set (zip xs ys)" using in_set_zip by fastforce
with hn assms(2) show "x = y" by auto
qed
hence "∀(x, y) ∈ set (zip (map f xs) (map g ys)). x = y" by force
with assms(1) list_eq_iff_zip_eq show "map f xs = map g ys" by fastforce
qed

lemma map_eq_iff_pairs_eq: "(map f xs = map g ys) =
(length xs = length ys ∧ (∀(x, y) ∈ set (zip xs ys). f x = g y))"
proof -
have "map f xs = map g ys ⟹ ∀(x, y) ∈ set (zip xs ys). f x = g y" using map_eq_imp_pairs_eq
by fast
thus ?thesis by (metis pairs_eq_imp_map_eq length_map)
qed

lemma subtree_eq_trim_eq:
assumes "length ts = length us" "∀(t, u) ∈ set (zip ts us). trim n t = trim n u"
shows "trim (Suc n) (Node ts) = trim (Suc n) (Node us)"
by (auto simp add: assms map_eq_iff_pairs_eq)

lemma subtree_trim_1: "is_subtree_index t [i] ⟹ trim (Suc n) t !t [i] = trim n (t !t [i])"
by (smt (verit) Suc_inject is_subtree_index.simps(2) list.distinct(1) nat.distinct(1) nth_map
subtree.elims subtree.simps(2) tree.sel trim.elims)

lemma is_subtree_index_trim:
"is_subtree_index (trim n t) xs = (is_subtree_index t xs ∧ length xs ≤ n)"
proof (induction n t arbitrary: xs rule: trim.induct)
case (1 t)
then show ?case using is_subtree_index_length_le by fastforce
next
case (2 n ts)
then show ?case proof (induction xs rule: rev_induct)
case Nil
then show ?case by auto
next
case (snoc x xs)
then show ?case by fastforce
qed
qed

lemma subtree_trim: "⟦is_subtree_index t xs; length xs ≤ n⟧ ⟹
trim n t !t xs = trim (n - length xs) (t !t xs)"
proof (induction n t arbitrary: xs rule: trim.induct)
case (1 t)
then show ?case by simp
next
case (2 n ts)
then show ?case proof (cases "length xs = Suc n")
case True
hence "is_subtree_index (trim (Suc n) (Node ts)) xs" using is_subtree_index_trim 2 by blast
hence "height (trim (Suc n) (Node ts) !t xs) ≤ 0"
by (metis height_subtree height_trim_le True diff_is_0_eq')
then show ?thesis using True height_zero by fastforce
next
case False
then show ?thesis proof (cases xs rule: rev_cases)
case Nil
then show ?thesis by simp
next
case (snoc ys i)
have hi: "ts ! i ∈ set ts" "is_subtree_index (ts ! i) ys" using snoc 2(2) by simp_all
have hl: "length ys ≤ n" using snoc 2(3) by simp
have "Node (map (trim n) ts) !t ys @ [i] = trim n (ts ! i) !t ys"
by (metis "2.prems"(1) is_subtree_index_append nth_map snoc subtree_append)
also have "… = trim (n - length ys) (ts ! i !t ys)" using 2(1) hi hl by blast
finally show "trim (Suc n) (Node ts) !t xs = trim (Suc n - length xs) (Node ts !t xs)"
qed
qed
qed

lemma length_subtrees_trim: "⟦is_subtree_index t xs; length xs < n⟧ ⟹
length (subtrees (trim n t !t xs)) = length (subtrees (t !t xs))"
by (metis subtree_trim length_subtrees_trim_Suc Suc_diff_Suc less_imp_le_nat)

lemma subtree_trim_Leaf: assumes "is_subtree_index (trim n t) xs" "t !t xs = Leaf"
shows "trim n t !t xs = Leaf"
proof (cases "length xs < n")
case True
then show ?thesis
using length_subtrees_trim assms is_subtree_index_trim subtrees_Leaf by fastforce
next
case False
hence "length xs = n" using assms(1) by (simp add: is_subtree_index_trim)
then show ?thesis using assms(1) is_subtree_index_trim subtree_trim by auto
qed

subsection ‹The strict $\omega$-category of pasting diagrams›

text ‹The function ‹δ› acts as both the source and target map in the globular set of pasting
diagrams. It is denoted $\partial$ in Leinster \cite[p. 264]{Leinster2004}.›
abbreviation δ where
"δ ≡ trim"

value "δ 1 (Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]])"  (* Leinster2004: (8.1), p. 264 *)
value "δ 2 (Node [Node [Node [Leaf, Leaf]], Node [Leaf, Leaf]])" (* Leinster2004: (8.3), p. 265 *)

abbreviation PD :: "nat ⇒ tree set" where
"PD n ≡ {t. height t ≤ n}"

interpretation pd: globular_set PD δ δ
by (unfold_locales, auto simp add: height_trim_le)

text ‹The generalised source and target maps have simple interpretations in terms of ‹trim›.›

lemma s'_eq_trim: assumes "n ≤ m" "height t ≤ m" shows "pd.s' m n t = trim n t"
using assms
proof (induction m arbitrary: t)
case 0
moreover hence "n = 0" by force
ultimately show ?case using pd.s'_n_n trim_const by simp
next
case (Suc m)
then show ?case proof (cases "n = Suc m")
case True
then show ?thesis using pd.s'_n_n Suc(3) trim_const by simp
next
case False
with Suc(2) have "n ≤ m" by simp
hence "pd.s' (Suc m) n t = pd.s' m n (δ m t)" using Suc(3) by force
also have "… = δ n (δ m t)" using Suc.IH height_trim_le ‹n ≤ m› by blast
finally show ?thesis by (metis trim_trim ‹n ≤ m› comp_apply)
qed
qed

lemma s'_eq_t': "pd.s' = pd.t'"
fix m n t
show "pd.s' m n t = pd.t' m n t" proof (induction m arbitrary: n t)
case 0
then show ?case
using pd.s'_n_n pd.t'_n_n pd.s'.simps(2) pd.t'.simps(2) by (cases n, presburger+)
next
case (Suc m)
then show ?case by (cases "Suc m" rule: linorder_cases, simp_all)
qed
qed

lemma t'_eq_trim: assumes "n ≤ m" "height t ≤ m" shows "pd.t' m n t = trim n t"
by (metis (mono_tags, lifting) assms s'_eq_trim s'_eq_t')

text ‹Next we define identities and composition \cite[p. 266]{Leinster2004}. The identity of a tree with height at most ‹n› is
the same tree seen as a tree of height at most ‹n + 1›.›

fun tree_comp :: "nat ⇒ tree ⇒ tree ⇒ tree" where
"tree_comp 0 (Node ts) (Node us) = Node (ts @ us)" |
"tree_comp (Suc n) (Node ts) (Node us) = Node (map2 (tree_comp n) ts us)"

value "tree_comp 1
(Node [Node [Leaf, Leaf], Leaf, Node [Leaf]])
(Node [Leaf, Leaf, Node [Leaf, Leaf]])"
(* Node [Node [Leaf, Leaf], Leaf, Node [Leaf, Leaf, Leaf]] *)
(* Leinster2001: p. 39 *)

value "tree_comp 0
(Node [Node [Node [Leaf, Leaf]]])
(Node [Node [Leaf, Leaf]])"
(* Node [Node [Node [Leaf, Leaf]], Node [Leaf, Leaf]] *)
(* Leinster2001: p. 39 *)

value "tree_comp 0
(tree_comp 0
(tree_comp 1
(Node [Leaf, Leaf])
(Node [Node [Leaf], Node [Leaf, Leaf, Leaf]]))
(Node [Leaf, Node [Leaf, Leaf]]))
(Node [Leaf, Leaf, Leaf])"
(* Node [
Node [Leaf],
Node [Leaf, Leaf, Leaf],
Leaf,
Node [Leaf, Leaf],
Leaf,
Leaf,
Leaf]*)
(* Leinster2001: p. 40 *)

lemma tree_comp_0_Leaf1 [simp]: "tree_comp 0 Leaf t = t"
by (metis eq_Nil_appendI tree.exhaust tree_comp.simps(1))

lemma tree_comp_0_Leaf2 [simp]: "tree_comp 0 t Leaf = t"
by (metis append_Nil2 tree.exhaust tree_comp.simps(1))

lemma tree_comp_Suc_Leaf1 [simp]: "tree_comp (Suc n) Leaf t = Leaf"
by (cases t, simp)

lemma tree_comp_Suc_Leaf2 [simp]: "tree_comp (Suc n) t Leaf = Leaf"
by (cases t, simp)

lemma height_tree_comp_0 [simp]: "height (tree_comp 0 t u) = max (height t) (height u)"
proof (cases "t = Leaf ∨ u = Leaf")
case True
then show ?thesis by auto
next
case False
hence nempt: "subtrees t ≠ [] ∧ subtrees u ≠ []" by (metis tree.exhaust_sel)
have "height (tree_comp 0 t u) = height (Node (subtrees t @ subtrees u))"
by (metis tree.collapse tree_comp.simps(1))
also have "… = Suc (Max (set (map height (subtrees t @ subtrees u))))"
using nempt height_Node_Max by blast
also have "… = Suc (Max (set (map height (subtrees t)) ∪ set (map height (subtrees u))))"
by simp
also have "… = Suc (max (Max (set (map height (subtrees t))))
(Max (set (map height (subtrees u)))))"
using nempt Max_Un by (metis List.finite_set map_is_Nil_conv set_empty2)
also have "… = max (Suc (Max (set (map height (subtrees t)))))
(Suc (Max (set (map height (subtrees u)))))"
by linarith
finally show "height (tree_comp 0 t u) = max (height t) (height u)"
using nempt height_Node_Max by (metis tree.collapse)
qed

text ‹An alternative description of being composable for trees. Defined so that
‹tree_comp n t u› is defined if and only if ‹composable_tree n t u›.›
fun composable_tree :: "nat ⇒ tree ⇒ tree ⇒ bool" where
"composable_tree 0 (Node ts) (Node us) = True" |
"composable_tree (Suc n) (Node ts) (Node us) = (length ts = length us ∧
(∀i < length ts. composable_tree n (ts!i) (us!i)))"

lemma sym_composable_tree: "composable_tree n t u = composable_tree n u t"
by (induction n t u rule: composable_tree.induct, simp, fastforce)

lemma is_composable_pair_imp_composable_tree: "pd.is_composable_pair m n t u ⟹
composable_tree n t u"
proof (induction n t u rule: composable_tree.induct)
case (1 ts us)
then show ?case by fastforce
next
case (2 n ts us)
with pd.is_composable_pair_def have h: "Suc n < m" "height (Node ts) ≤ m" "height (Node us) ≤ m"
"pd.t' m (Suc n) (Node us) = pd.s' m (Suc n) (Node ts)" by blast+
moreover hence "Suc n ≤ m" by linarith
ultimately have htrim: "trim (Suc n) (Node ts) = trim (Suc n) (Node us)"
by (metis (mono_tags, lifting) s'_eq_trim t'_eq_trim)
hence "trim 1 (Node ts) = trim 1 (Node us)"
by (metis One_nat_def Suc_le_mono le0 trim_eq_imp_trim_eq)
with trim_1_eq have hl: "length ts = length us" by blast
moreover have "∀i < length ts. composable_tree n (ts!i) (us!i)" proof (safe)
fix i assume hi: "i < length ts"
hence "height (ts!i) ≤ m" using h(2) height_lt nth_mem by fastforce
moreover have "height (us!i) ≤ m" using hi h(3) height_lt nth_mem hl by fastforce
moreover have "n < m" using h(1) by simp
moreover have "trim n (ts!i) = trim n (us!i)" proof -
have "map (trim n) ts = map (trim n) us" using htrim by auto
thus "trim n (ts!i) = trim n (us!i)" using nth_map hi hl by metis
qed
ultimately have "pd.t' m n (us!i) = pd.s' m n (ts!i)"
using s'_eq_trim t'_eq_trim order_less_imp_le[of n m] by presburger
hence "pd.is_composable_pair m n (ts!i) (us!i)"
using pd.is_composable_pair_def ‹n < m› ‹height (ts!i) ≤ m› ‹height (us!i) ≤ m› by blast
with 2(1) hi show "composable_tree n (ts!i) (us!i)" by fast
qed
ultimately show ?case by fastforce
qed

lemma composable_tree_imp_trim_eq: "composable_tree n t u ⟹ trim n t = trim n u"
proof (induction n t u rule: composable_tree.induct)
case (1 ts us)
then show ?case by simp
next
case (2 n ts us)
then show ?case
by (metis (mono_tags, lifting) nth_map trim.simps(2) length_map nth_equalityI
composable_tree.simps(2))
qed

lemma composable_tree_imp_is_composable_pair:
assumes "n < m" "height t ≤ m" "height u ≤ m" "composable_tree n t u"
shows "pd.is_composable_pair m n t u"
using assms
proof (induction m arbitrary: n t u)
case 0
then show ?case by blast
next
case (Suc m)
hence "trim n u = trim n t" using composable_tree_imp_trim_eq by presburger
hence "pd.t' (Suc m) n u = pd.s' (Suc m) n t"
using Suc(2-4) s'_eq_trim t'_eq_trim less_imp_le_nat by presburger
with Suc(2-4) pd.is_composable_pair_def show ?case by blast
qed

lemma is_composable_pair_iff_composable_tree: "pd.is_composable_pair m n t u =
(n < m ∧ height t ≤ m ∧ height u ≤ m ∧ composable_tree n t u)"
by (metis (mono_tags, lifting) composable_tree_imp_is_composable_pair
is_composable_pair_imp_composable_tree mem_Collect_eq pd.is_composable_pair_def)

lemma composable_tree_imp_composable_tree_subtrees:
"composable_tree (Suc n) (Node ts) (Node us) ⟹ ∀(t, u) ∈ set (zip ts us). composable_tree n t u"
by (metis in_set_zip case_prod_beta composable_tree.simps(2))

lemma composable_tree_nth_subtrees:
"⟦composable_tree (Suc n) (Node ts) (Node us); i < length ts⟧ ⟹ composable_tree n (ts!i) (us!i)"
by fastforce

lemma is_composable_pair_imp_is_composable_pair_subtrees:
assumes "pd.is_composable_pair (Suc m) (Suc n) (Node ts) (Node us)"
shows "∀(t, u) ∈ set (zip ts us). pd.is_composable_pair m n t u"
proof
have "pd.is_composable_pair m n (fst p) (snd p)" if hp: "p ∈ set (zip ts us)" for p proof -
have "composable_tree (Suc n) (Node ts) (Node us)"
using is_composable_pair_iff_composable_tree assms by blast
hence h: "composable_tree n (fst p) (snd p)"
using hp composable_tree_imp_composable_tree_subtrees by fastforce
have "fst p ∈ set ts" "snd p ∈ set us" by (metis hp in_set_zipE prod.exhaust_sel)+
hence "height (fst p) ≤ m" "height (snd p) ≤ m"
by (meson hp height_lt assms less_Suc_eq_le order_less_le_trans
is_composable_pair_iff_composable_tree)+
with h is_composable_pair_iff_composable_tree assms
show "pd.is_composable_pair m n (fst p) (snd p)" by force
qed
then show "⋀x. x ∈ set (zip ts us) ⟹ case x of (t, u) ⇒ pd.is_composable_pair m n t u"
by force
qed

lemma in_set_map2: "(z ∈ set (map2 f xs ys)) = (∃(x, y) ∈ set (zip xs ys). z = f x y)"
by auto

lemma height_tree_comp_le: "⟦height t ≤ m; height u ≤ m⟧ ⟹ height (tree_comp n t u) ≤ m"
proof (induction n t u arbitrary: m rule: tree_comp.induct)
case (1 ts us)
then show ?case using height_tree_comp_0 by presburger
next
case (2 n ts us)
show ?case proof (cases "ts ≠ [] ∧ us ≠ []")
case True
hence "∃m'. m = Suc m'" using height_zero "2.prems"(1) not0_implies_Suc by auto
then obtain m' where "m = Suc m'" by blast
hence "∀t ∈ set ts. height t ≤ m'" "∀u ∈ set us. height u ≤ m'"
using True "2.prems" by simp+
hence "∀(t, u) ∈ set (zip ts us). height (tree_comp n t u) ≤ m'"
by (metis (no_types, lifting) "2.IH" case_prodI2 set_zip_leftD set_zip_rightD)
then show ?thesis using True ‹m = Suc m'› by auto
next
case False
then show ?thesis by force
qed
qed

lemma nth_map2 [simp]: "⟦n < length xs; n < length ys⟧ ⟹ map2 f xs ys ! n = f (xs ! n) (ys ! n)"
by fastforce

lemma trim_tree_comp1: "composable_tree n t u ⟹ trim n (tree_comp n t u) = trim n t"
proof (induction n t u rule: composable_tree.induct)
case (1 ts us)
then show ?case by fastforce
next
case (2 n ts us)
then show ?case by (simp add: list_eq_iff_nth_eq)
qed

lemma trim_tree_comp2: "composable_tree n t u ⟹ trim n (tree_comp n t u) = trim n u"
using trim_tree_comp1 composable_tree_imp_trim_eq by presburger

lemma map2_map_map': "map2 f (map g xs) (map h ys) = map (λ(x, y). f (g x) (h y)) (zip xs ys)"
proof (induction xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case proof (induction ys)
case Nil
then show ?case by simp
next
case (Cons a ys)
then show ?case by auto
qed
qed

lemma trim_tree_comp_commute: "trim m (tree_comp n t u) = tree_comp n (trim m t) (trim m u)"
proof (induction m arbitrary: n t u)
case 0
then show ?case by (cases n, simp_all)
next
case (Suc m)
then show ?case
by (induction n t u rule: composable_tree.induct, simp_all add: list_eq_iff_nth_eq)
qed

interpretation pd_pre_cat: pre_strict_omega_category PD δ δ "λ m. tree_comp" "λ n. id"
proof (unfold_locales)
fix m n x' x assume "pd.is_composable_pair m n x' x"
then show "tree_comp n x' x ∈ PD m"
using is_composable_pair_iff_composable_tree height_tree_comp_le by auto
next
fix n show "id ∈ PD n → PD (Suc n)" by simp
next
fix m x' x assume "pd.is_composable_pair (Suc m) m x' x"
then show "δ m (tree_comp m x' x) = δ m x"
by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp2 height_tree_comp_le)
next
fix m x' x assume "pd.is_composable_pair (Suc m) m x' x"
then show "δ m (tree_comp m x' x) = δ m x'"
by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp1 height_tree_comp_le)
next
fix m n x' x assume "pd.is_composable_pair (Suc m) n x' x" "n < m"
then show "δ m (tree_comp n x' x) = tree_comp n (δ m x') (δ m x)"
by (simp add: is_composable_pair_iff_composable_tree trim_tree_comp_commute height_tree_comp_le)
next
fix x n assume "x ∈ PD n"
then show "δ n (id x) = x" using trim_const by auto
qed

lemma tree_comp_assoc: "tree_comp n (tree_comp n t u) v = tree_comp n t (tree_comp n u v)"
proof (induction n t u arbitrary: v rule: composable_tree.induct)
case (1 ts us)
then show ?case by (metis append_assoc tree_comp.simps(1) tree.exhaust)
next
case (2 n ts us)
define vs where "vs = subtrees v" hence hv: "v = Node vs" by force
let ?k = "min (length ts) (min (length us) (length vs))"
have "∀i < ?k. tree_comp n (tree_comp n (ts!i) (us!i)) (vs!i) =
tree_comp n (ts!i) (tree_comp n (us!i) (vs!i))" using "2.IH" by auto
hence "map2 (tree_comp n) (map2 (tree_comp n) ts us) vs =
map2 (tree_comp n) ts (map2 (tree_comp n) us vs)" by (simp add: list_eq_iff_nth_eq)
then show ?case using hv by auto
qed

lemma i'_eq_id: "n ≤ m ⟹ pd_pre_cat.i' m n = id"
proof (induction m)
case 0
then show ?case using pd_pre_cat.i'.simps(1) by blast
next
case (Suc m)
then show ?case by (metis pd_pre_cat.i'_Suc id_comp le_Suc_eq pd_pre_cat.i'_n_n)
qed

lemma composable_tree_trim1: "n ≤ m ⟹ composable_tree n (trim m t) t"
proof (induction n t arbitrary: m rule: trim.induct)
case (1 t)
then show ?case by (metis composable_tree.simps(1) tree.exhaust)
next
case (2 n ts)
hence "∃m'. m = Suc m'" by presburger
then obtain m' where hm: "m = Suc m'" "n ≤ m'" using 2(2) by blast
moreover hence "∀i < length ts. composable_tree n (δ m' (ts!i)) (ts!i)" using 2(1) by simp
ultimately show ?case by force
qed

lemma composable_tree_trim2: "n ≤ m ⟹ composable_tree n t (trim m t)"
using sym_composable_tree composable_tree_trim1 by presburger

lemma tree_comp_trim1: "tree_comp n (trim n t) t = t"
by (induction n t rule: trim.induct, simp add: tree.exhaust, simp add: list_eq_iff_nth_eq)

lemma tree_comp_trim2: "tree_comp n t (trim n t) = t"
by (induction n t rule: trim.induct, simp add: tree.exhaust, simp add: list_eq_iff_nth_eq)

lemma tree_comp_exchange:
"⟦q < p; composable_tree p y' y; composable_tree p x' x;
composable_tree q y' x'; composable_tree q y x⟧ ⟹
tree_comp q (tree_comp p y' y) (tree_comp p x' x) =
tree_comp p (tree_comp q y' x') (tree_comp q y x)"
proof (induction p y' y arbitrary: q x' x rule: composable_tree.induct)
case (1 ys' ys)
then show ?case proof (induction q x' x rule: composable_tree.induct)
case (1 xs' xs)
then show ?case by blast
next
case (2 q xs' xs)
then show ?case by force
qed
next
case (2 p ys' ys)
then show ?case proof (induction q x' x rule: composable_tree.induct)
case (1 ts us)
then show ?case by force
next
case (2 n ts us)
then show ?case by (simp add: list_eq_iff_nth_eq)
qed
qed

interpretation pd_cat': strict_omega_category PD δ δ "λ m. tree_comp" "λ n. id"
proof (unfold_locales)
fix m n x' x x'' assume "pd.is_composable_pair m n x' x" "pd.is_composable_pair m n x'' x'"
then show "tree_comp n (tree_comp n x'' x') x = tree_comp n x'' (tree_comp n x' x)"
using tree_comp_assoc is_composable_pair_iff_composable_tree by force
next
fix n m x assume "n < m" "x ∈ PD m"
moreover hence "height x ≤ m" by simp
ultimately show "tree_comp n (pd_pre_cat.i' m n (pd.t' m n x)) x = x"
by (metis (no_types, lifting) i'_eq_id t'_eq_trim tree_comp_trim1 id_apply nat_less_le)
next
fix n m x assume "n < m" "x ∈ PD m"
moreover hence "height x ≤ m" by simp
ultimately show "tree_comp n x (pd_pre_cat.i' m n (pd.s' m n x)) = x"
by (metis (no_types, lifting) i'_eq_id s'_eq_trim tree_comp_trim2 id_apply nat_less_le)
next
fix q p m y' y x' x assume "q < p" "p < m"
"pd.is_composable_pair m p y' y" "pd.is_composable_pair m p x' x"
"pd.is_composable_pair m q y' x'" "pd.is_composable_pair m q y x"
then show "tree_comp q (tree_comp p y' y) (tree_comp p x' x) =
tree_comp p (tree_comp q y' x') (tree_comp q y x)"
using is_composable_pair_iff_composable_tree tree_comp_exchange by meson
qed (simp)

end`