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" by (simp add: Max_eq_iff) 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)" by (simp add: snoc subtree_append) 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'" proof (clarsimp simp add: fun_eq_iff) 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