diff --git a/thys/Tree_Enumeration/Labeled_Tree_Enumeration.thy b/thys/Tree_Enumeration/Labeled_Tree_Enumeration.thy --- a/thys/Tree_Enumeration/Labeled_Tree_Enumeration.thy +++ b/thys/Tree_Enumeration/Labeled_Tree_Enumeration.thy @@ -1,391 +1,391 @@ section \Enumeration of Labeled Trees\ theory Labeled_Tree_Enumeration imports Tree_Graph begin definition labeled_trees :: "'a set \ 'a pregraph set" where "labeled_trees V = {(V,E)| E. tree V E}" subsection \Algorithm\ text \Prüfer sequence to tree\ definition prufer_sequences :: "'a list \ 'a list set" where "prufer_sequences verts = {xs. length xs = length verts - 2 \ set xs \ set verts}" fun tree_edges_of_prufer_seq :: "'a list \ 'a list \ 'a edge set" where "tree_edges_of_prufer_seq [u,v] [] = {{u,v}}" | "tree_edges_of_prufer_seq verts (b#seq) = (case find (\x. x \ set (b#seq)) verts of Some a \ insert {a,b} (tree_edges_of_prufer_seq (remove1 a verts) seq))" definition tree_of_prufer_seq :: "'a list \ 'a list \ 'a pregraph" where "tree_of_prufer_seq verts seq = (set verts, tree_edges_of_prufer_seq verts seq)" definition labeled_tree_enum :: "'a list \ 'a pregraph list" where "labeled_tree_enum verts = map (tree_of_prufer_seq verts) (List.n_lists (length verts - 2) verts)" subsection \Correctness\ text \Tree to Prüfer sequence\ definition remove_vertex_edges :: "'a \ 'a edge set \ 'a edge set" where - "remove_vertex_edges v E = {e\E. \ graph_system.incident v e}" + "remove_vertex_edges v E = {e\E. \ graph_system.vincident v e}" lemma find_in_list[termination_simp]: "find P verts = Some v \ v \ set verts" by (metis find_Some_iff nth_mem) lemma [termination_simp]: "find P verts = Some v \ length verts - Suc 0 < length verts" by (meson diff_Suc_less length_pos_if_in_set find_in_list) fun prufer_seq_of_tree :: "'a list \ 'a edge set \ 'a list" where "prufer_seq_of_tree verts E = (if length verts \ 2 then [] else (case find (tree.leaf E) verts of Some leaf \ (THE v. ulgraph.vert_adj E leaf v) # prufer_seq_of_tree (remove1 leaf verts) (remove_vertex_edges leaf E)))" locale valid_verts = fixes verts assumes length_verts: "length verts \ 2" and distinct_verts: "distinct verts" locale tree_of_prufer_seq_ctx = valid_verts + fixes seq assumes prufer_seq: "seq \ prufer_sequences verts" lemma (in valid_verts) card_verts: "card (set verts) = length verts" using length_verts distinct_verts distinct_card by blast lemma length_gt_find_not_in_ys: assumes "length xs > length ys" and "distinct xs" shows "\x. find (\x. x \ set ys) xs = Some x" proof- have "card (set xs) > card (set ys)" by (metis assms card_length distinct_card le_neq_implies_less order_less_trans) then have "\x\set xs. x \ set ys" by (meson finite_set card_subset_not_gt_card subsetI) then show ?thesis by (metis find_None_iff2 not_Some_eq) qed lemma (in tree_of_prufer_seq_ctx) tree_edges_of_prufer_seq_induct': assumes "\u v. P [u, v] []" and "\verts b seq a. find (\x. x \ set (b # seq)) verts = Some a \ a \ set verts \ a \ set (b # seq) \ seq \ prufer_sequences (remove1 a verts) \ tree_of_prufer_seq_ctx (remove1 a verts) seq \ P (remove1 a verts) seq \ P verts (b # seq)" shows "P verts seq" using tree_of_prufer_seq_ctx_axioms proof (induction verts seq rule: tree_edges_of_prufer_seq.induct) case (2 verts b seq) then interpret tree_of_prufer_seq_ctx verts "b # seq" by simp obtain a where a_find: "find (\x. x \ set (b # seq)) verts = Some a" using length_gt_find_not_in_ys[of "b#seq" verts] distinct_verts prufer_seq unfolding prufer_sequences_def by fastforce then have a_in_verts: "a \ set verts" by (simp add: find_in_list) have a_not_in_seq: "a \ set (b#seq)" using a_find by (metis find_Some_iff) have prufer_seq': "seq \ prufer_sequences (remove1 a verts)" using prufer_seq a_in_verts set_remove1_eq length_verts a_not_in_seq distinct_verts unfolding prufer_sequences_def by (auto simp: length_remove1) have "length verts \ 3" using prufer_seq unfolding prufer_sequences_def by auto then have "length (remove1 a verts) \ 2" by (auto simp: length_remove1) then have valid_verts_seq': "tree_of_prufer_seq_ctx (remove1 a verts) seq" using prufer_seq' distinct_verts by unfold_locales auto then show ?case using a_find assms(2) a_in_verts a_not_in_seq prufer_seq' 2(1) by blast qed (auto simp: assms tree_of_prufer_seq_ctx_def tree_of_prufer_seq_ctx_axioms_def valid_verts_def prufer_sequences_def) lemma (in tree_of_prufer_seq_ctx) tree_edges_of_prufer_seq_tree: shows "tree (set verts) (tree_edges_of_prufer_seq verts seq)" using tree_of_prufer_seq_ctx_axioms proof (induction rule: tree_edges_of_prufer_seq_induct') case (1 u v) then show ?case using tree2 unfolding tree_of_prufer_seq_ctx_def valid_verts_def by fastforce next case (2 verts b seq a) interpret tree_of_prufer_seq_ctx verts "b # seq" using 2(7) . interpret tree "set (remove1 a verts)" "tree_edges_of_prufer_seq (remove1 a verts) seq" using 2(5,6) by simp have a_not_in_verts': "a \ set (remove1 a verts)" using distinct_verts by simp have "a \ b" using 2 by auto then have b_in_verts': "b \ set (remove1 a verts)" using prufer_seq unfolding prufer_sequences_def by auto then show ?case using a_not_in_verts' add_vertex_tree[OF a_not_in_verts' b_in_verts'] 2(1,2) distinct_verts by (auto simp: insert_absorb insert_commute) qed lemma (in tree_of_prufer_seq_ctx) tree_of_prufer_seq_tree: "(V,E) = tree_of_prufer_seq verts seq \ tree V E" unfolding tree_of_prufer_seq_def using tree_edges_of_prufer_seq_tree by auto lemma (in valid_verts) labeled_tree_enum_trees: assumes VE_in_labeled_tree_enum: "(V,E) \ set (labeled_tree_enum verts)" shows "tree V E" proof- obtain seq where "seq \ set (List.n_lists (length verts - 2) verts)" and tree_of_seq: "tree_of_prufer_seq verts seq = (V,E)" using VE_in_labeled_tree_enum unfolding labeled_tree_enum_def by auto then interpret tree_of_prufer_seq_ctx verts seq using List.set_n_lists by (unfold_locales) (auto simp: prufer_sequences_def) show ?thesis using tree_of_prufer_seq_tree using tree_of_seq by simp qed subsection \Totality\ locale prufer_seq_of_tree_context = valid_verts verts + tree "set verts" E for verts E begin lemma prufer_seq_of_tree_induct': assumes "\u v. P [u,v] {{u,v}}" and "\verts E l. \ length verts \ 2 \ find (tree.leaf E) verts = Some l \ tree.leaf E l \ l \ set verts \ prufer_seq_of_tree_context (remove1 l verts) (remove_vertex_edges l E) \ P (remove1 l verts) (remove_vertex_edges l E) \ P verts E" shows "P verts E" using prufer_seq_of_tree_context_axioms proof (induction verts E rule: prufer_seq_of_tree.induct) case (1 verts E) then interpret ctx: prufer_seq_of_tree_context verts E by simp show ?case proof (cases "length verts \ 2") case True then have length_verts: "length verts = 2" using ctx.length_verts by simp then obtain u w where verts: "verts = [u,w]" unfolding numeral_2_eq_2 by (metis length_0_conv length_Suc_conv) then have "E = {{u,w}}" using ctx.connected_two_graph_edges ctx.distinct_verts by simp then show ?thesis using assms(1) verts by blast next case False then have "ctx.non_trivial" using ctx.distinct_verts distinct_card unfolding ctx.non_trivial_def by fastforce then obtain l where l: "find ctx.leaf verts = Some l" using ctx.exists_leaf by (metis find_None_iff2 not_Some_eq) then have leaf_l: "ctx.leaf l" by (metis find_Some_iff) then have l_in_verts: "l \ set verts" using ctx.leaf_in_V by simp then have length_verts': "length (remove1 l verts) \ 2" using False unfolding length_remove1 by simp have "tree (set (remove1 l verts)) (remove_vertex_edges l E)" using ctx.tree_remove_leaf[OF leaf_l] unfolding ctx.remove_vertex_def remove_vertex_edges_def using ctx.distinct_verts by simp then have ctx': "prufer_seq_of_tree_context (remove1 l verts) (remove_vertex_edges l E)" unfolding prufer_seq_of_tree_context_def valid_verts_def using ctx.distinct_verts length_verts' by simp then have "P (remove1 l verts) (remove_vertex_edges l E)" using 1 False l by simp then show ?thesis using assms(2)[OF False l leaf_l l_in_verts ctx'] by simp qed qed lemma prufer_seq_of_tree_wf: "set (prufer_seq_of_tree verts E) \ set verts" using prufer_seq_of_tree_context_axioms proof (induction rule: prufer_seq_of_tree_induct') case (1 u v) then show ?case by simp next case (2 verts E l) then interpret ctx: prufer_seq_of_tree_context verts E by simp let ?u = "THE u. ctx.vert_adj l u" have l_u_adj: "ctx.vert_adj l ?u" using ctx.ex1_neighbor_degree_1 2(3) unfolding ctx.leaf_def by (metis theI) then have "?u \ set verts" unfolding ctx.vert_adj_def using ctx.wellformed_alt_snd by blast then show ?case using 2 ctx.ex1_neighbor_degree_1 2(3) by (auto, meson in_mono notin_set_remove1) qed lemma length_prufer_seq_of_tree: "length (prufer_seq_of_tree verts E) = length verts - 2" proof (induction rule: prufer_seq_of_tree_induct') case (1 u v) then show ?case by simp next case (2 verts E l) then show ?case unfolding prufer_seq_of_tree.simps[of verts] by (simp add: length_remove1) qed lemma prufer_seq_of_tree_prufer_seq: "prufer_seq_of_tree verts E \ prufer_sequences verts" using prufer_seq_of_tree_wf length_prufer_seq_of_tree unfolding prufer_sequences_def by blast lemma count_list_prufer_seq_degree: "v \ set verts \ Suc (count_list (prufer_seq_of_tree verts E) v) = degree v" using prufer_seq_of_tree_context_axioms proof (induction rule: prufer_seq_of_tree_induct') case (1 u v) then interpret ctx: prufer_seq_of_tree_context "[u, v]" "{{u, v}}" by simp - show ?case using 1(1) unfolding ctx.alt_degree_def ctx.incident_edges_def ctx.incident_def + show ?case using 1(1) unfolding ctx.alt_degree_def ctx.incident_edges_def ctx.vincident_def by (simp add: Collect_conv_if) next case (2 verts E l) then interpret ctx: prufer_seq_of_tree_context verts E by simp interpret ctx': prufer_seq_of_tree_context "remove1 l verts" "remove_vertex_edges l E" using 2(5) by simp let ?u = "THE u. ctx.vert_adj l u" have l_u_adj: "ctx.vert_adj l ?u" using ctx.ex1_neighbor_degree_1 2(3) unfolding ctx.leaf_def by (metis theI) show ?case proof (cases "v = ?u") case True then have "v \ l" using l_u_adj ctx.vert_adj_not_eq by blast then have "count_list (prufer_seq_of_tree verts E) v = ulgraph.degree (remove_vertex_edges l E) v" using 2 True by simp then show ?thesis using 2 ctx.degree_remove_adj_ne_vert \v\l\ True l_u_adj unfolding ctx.remove_vertex_def remove_vertex_edges_def prufer_seq_of_tree.simps[of verts] by simp next case False then show ?thesis proof (cases "v = l") case True then have "l \ set (remove1 l verts)" using ctx.distinct_verts by simp then have "l \ set (prufer_seq_of_tree (remove1 l verts) (remove_vertex_edges l E))" using ctx'.prufer_seq_of_tree_wf by blast then show ?thesis using 2 False True unfolding ctx.leaf_def prufer_seq_of_tree.simps[of verts] by simp next case False then have "\ ctx.vert_adj l v" using \v\?u\ ctx.ex1_neighbor_degree_1 2(3) l_u_adj unfolding ctx.leaf_def by blast then show ?thesis using False 2 \v\?u\ ctx.degree_remove_non_adj_vert unfolding prufer_seq_of_tree.simps[of verts] ctx'.remove_vertex_def remove_vertex_edges_def ctx.remove_vertex_def by auto qed qed qed lemma not_in_prufer_seq_iff_leaf: "v \ set verts \ v \ set (prufer_seq_of_tree verts E) \ leaf v" using count_list_prufer_seq_degree[symmetric] unfolding leaf_def by (simp add: count_list_0_iff) lemma tree_edges_of_prufer_seq_of_tree: "tree_edges_of_prufer_seq verts (prufer_seq_of_tree verts E) = E" using prufer_seq_of_tree_context_axioms proof (induction rule: prufer_seq_of_tree_induct') case (1 u v) then show ?case by simp next case (2 verts E l) then interpret ctx: prufer_seq_of_tree_context verts E by simp have "tree_edges_of_prufer_seq verts (prufer_seq_of_tree verts E) = tree_edges_of_prufer_seq verts ((THE v. ctx.vert_adj l v) # prufer_seq_of_tree (remove1 l verts) (remove_vertex_edges l E))" using 2 by simp have "find (\x. x \ set (prufer_seq_of_tree verts E)) verts = Some l" using ctx.not_in_prufer_seq_iff_leaf 2(2) by (metis (no_types, lifting) find_cong) then have "tree_edges_of_prufer_seq verts (prufer_seq_of_tree verts E) = insert {The (ctx.vert_adj l), l} (tree_edges_of_prufer_seq (remove1 l verts) (prufer_seq_of_tree (remove1 l verts) (remove_vertex_edges l E)))" using 2 by auto - also have "\ = E" using 2 ctx.degree_1_edge_partition unfolding remove_vertex_edges_def incident_def ctx.leaf_def by simp + also have "\ = E" using 2 ctx.degree_1_edge_partition unfolding remove_vertex_edges_def vincident_def ctx.leaf_def by simp finally show ?case . qed lemma tree_in_labeled_tree_enum: "(set verts, E) \ set (labeled_tree_enum verts)" using prufer_seq_of_tree_prufer_seq tree_edges_of_prufer_seq_of_tree List.set_n_lists unfolding prufer_sequences_def labeled_tree_enum_def tree_of_prufer_seq_def by fastforce end lemma (in valid_verts) V_labeled_tree_enum_verts: "(V,E) \ set (labeled_tree_enum verts) \ V = set verts" unfolding labeled_tree_enum_def by (metis Pair_inject ex_map_conv tree_of_prufer_seq_def) theorem (in valid_verts) labeled_tree_enum_correct: "set (labeled_tree_enum verts) = labeled_trees (set verts)" using labeled_tree_enum_trees V_labeled_tree_enum_verts prufer_seq_of_tree_context.tree_in_labeled_tree_enum valid_verts_axioms unfolding labeled_trees_def prufer_seq_of_tree_context_def by fast subsection \Distinction\ lemma (in tree_of_prufer_seq_ctx) count_prufer_seq_degree: assumes v_in_verts: "v \ set verts" shows "Suc (count_list seq v) = ulgraph.degree (tree_edges_of_prufer_seq verts seq) v" using v_in_verts tree_of_prufer_seq_ctx_axioms proof (induction rule: tree_edges_of_prufer_seq_induct') case (1 u w) then interpret tree_of_prufer_seq_ctx "[u, w]" "[]" by simp interpret tree "{u,w}" "{{u,w}}" using tree_edges_of_prufer_seq_tree by simp - show ?case using 1(1) by (auto simp add: incident_edges_def incident_def Collect_conv_if) + show ?case using 1(1) by (auto simp add: incident_edges_def vincident_def Collect_conv_if) next case (2 verts b seq a) interpret tree_of_prufer_seq_ctx verts "b # seq" using 2(8) . interpret tree "set verts" "tree_edges_of_prufer_seq verts (b#seq)" using tree_edges_of_prufer_seq_tree by simp interpret ctx': tree_of_prufer_seq_ctx "remove1 a verts" seq using 2(5) . interpret T': tree "set (remove1 a verts)" "tree_edges_of_prufer_seq (remove1 a verts) seq" using ctx'.tree_edges_of_prufer_seq_tree by simp show ?case proof (cases "v = b") case True have ab_not_in_T': "{a, b} \ tree_edges_of_prufer_seq (remove1 a verts) seq" using T'.wellformed_alt_snd distinct_verts by (auto, metis doubleton_eq_iff) have "incident_edges v = insert {a,b} {e \ tree_edges_of_prufer_seq (remove1 a verts) seq. v \ e}" - unfolding incident_edges_def incident_def using 2(1) True by auto + unfolding incident_edges_def vincident_def using 2(1) True by auto then have "degree v = Suc (T'.degree v)" - unfolding T'.alt_degree_def alt_degree_def T'.incident_edges_def incident_def + unfolding T'.alt_degree_def alt_degree_def T'.incident_edges_def vincident_def using ab_not_in_T' T'.fin_edges by (simp del: tree_edges_of_prufer_seq.simps) then show ?thesis using 2 True by auto next case False then show ?thesis proof (cases "v = a") case True - also have "incident_edges a = {{a,b}}" unfolding incident_edges_def incident_def + also have "incident_edges a = {{a,b}}" unfolding incident_edges_def vincident_def using 2(1) T'.wellformed distinct_verts by auto then show ?thesis unfolding alt_degree_def True using 2(3) by auto next case False then have "incident_edges v = T'.incident_edges v" - unfolding incident_edges_def T'.incident_edges_def incident_def using 2(1) \v \ b\ by auto + unfolding incident_edges_def T'.incident_edges_def vincident_def using 2(1) \v \ b\ by auto then show ?thesis using False \v \ b\ 2 unfolding alt_degree_def by simp qed qed qed lemma (in tree_of_prufer_seq_ctx) notin_prufer_seq_iff_leaf: assumes "v \ set verts" shows "v \ set seq \ tree.leaf (tree_edges_of_prufer_seq verts seq) v" proof- interpret tree "set verts" "tree_edges_of_prufer_seq verts seq" using tree_edges_of_prufer_seq_tree by auto show ?thesis using count_prufer_seq_degree assms count_list_0_iff unfolding leaf_def by fastforce qed lemma (in valid_verts) inj_tree_edges_of_prufer_seq: "inj_on (tree_edges_of_prufer_seq verts) (prufer_sequences verts)" proof fix seq1 seq2 assume prufer_seq1: "seq1 \ prufer_sequences verts" assume prufer_seq2: "seq2 \ prufer_sequences verts" assume trees_eq: "tree_edges_of_prufer_seq verts seq1 = tree_edges_of_prufer_seq verts seq2" interpret tree_of_prufer_seq_ctx verts seq1 using prufer_seq1 by unfold_locales simp have length_eq: "length seq1 = length seq2" using prufer_seq1 prufer_seq2 unfolding prufer_sequences_def by simp show "seq1 = seq2" using prufer_seq1 prufer_seq2 trees_eq length_eq tree_of_prufer_seq_ctx_axioms proof (induction arbitrary: seq2 rule: tree_edges_of_prufer_seq_induct') case (1 u v) then show ?case by simp next case (2 verts b seq a) then interpret ctx1: tree_of_prufer_seq_ctx verts "b # seq" by simp interpret ctx2: tree_of_prufer_seq_ctx verts seq2 using 2 by unfold_locales blast obtain b' seq2' where seq2: "seq2 = b' # seq2'" using 2(10) by (metis length_Suc_conv) then have "find (\x. x \ set seq2) verts = Some a" using ctx2.notin_prufer_seq_iff_leaf 2(9) 2(1) ctx1.notin_prufer_seq_iff_leaf[symmetric] find_cong by force then have edges_eq: "insert {a, b} (tree_edges_of_prufer_seq (remove1 a verts) seq) = insert {a, b'} (tree_edges_of_prufer_seq (remove1 a verts) seq2')" using 2 seq2 by simp interpret ctx1': tree_of_prufer_seq_ctx "remove1 a verts" seq using 2(5) . interpret T1: tree "set (remove1 a verts)" "tree_edges_of_prufer_seq (remove1 a verts) seq" using ctx1'.tree_edges_of_prufer_seq_tree by blast have "a \ set seq2'" using seq2 2 ctx1.notin_prufer_seq_iff_leaf ctx2.notin_prufer_seq_iff_leaf by auto then interpret ctx2': tree_of_prufer_seq_ctx "remove1 a verts" seq2' using seq2 2(8) 2(2) ctx1.distinct_verts by unfold_locales (auto simp: length_remove1 prufer_sequences_def) interpret T2: tree "set (remove1 a verts)" "tree_edges_of_prufer_seq (remove1 a verts) seq2'" using ctx2'.tree_edges_of_prufer_seq_tree by blast have a_notin_verts': "a \ set (remove1 a verts)" using ctx1.distinct_verts by simp then have ab'_notin_edges: "{a,b'} \ tree_edges_of_prufer_seq (remove1 a verts) seq" using T1.wellformed by blast then have "b = b'" using edges_eq by (metis doubleton_eq_iff insert_iff) have "{a,b} \ tree_edges_of_prufer_seq (remove1 a verts) seq2'" using T2.wellformed a_notin_verts' by blast then have "(tree_edges_of_prufer_seq (remove1 a verts) seq) = tree_edges_of_prufer_seq (remove1 a verts) seq2'" using edges_eq ab'_notin_edges by (simp add: \b = b'\ insert_eq_iff) then have "seq = seq2'" using "2.IH"[of seq2'] ctx1'.prufer_seq ctx2'.prufer_seq 2(10) ctx1'.tree_of_prufer_seq_ctx_axioms unfolding seq2 by simp then show ?case using \b = b'\ seq2 by simp qed qed theorem (in valid_verts) distinct_labeld_tree_enum: "distinct (labeled_tree_enum verts)" using inj_tree_edges_of_prufer_seq distinct_n_lists distinct_verts unfolding labeled_tree_enum_def prufer_sequences_def tree_of_prufer_seq_def by (auto simp add: distinct_map set_n_lists inj_on_def) lemma (in valid_verts) cayleys_formula: "card (labeled_trees (set verts)) = length verts ^ (length verts - 2)" proof- have "card (labeled_trees (set verts)) = length (labeled_tree_enum verts)" using distinct_labeld_tree_enum labeled_tree_enum_correct distinct_card by fastforce also have "\ = length verts ^ (length verts - 2)" unfolding labeled_tree_enum_def using length_n_lists by auto finally show ?thesis . qed end \ No newline at end of file diff --git a/thys/Tree_Enumeration/Rooted_Tree.thy b/thys/Tree_Enumeration/Rooted_Tree.thy --- a/thys/Tree_Enumeration/Rooted_Tree.thy +++ b/thys/Tree_Enumeration/Rooted_Tree.thy @@ -1,1304 +1,1304 @@ section \Rooted Trees\ theory Rooted_Tree imports Tree_Graph "HOL-Library.FSet" begin datatype tree = Node "tree list" fun tree_size :: "tree \ nat" where "tree_size (Node ts) = Suc (\t\ts. tree_size t)" fun height :: "tree \ nat" where "height (Node []) = 0" | "height (Node ts) = Suc (Max (height ` set ts))" text \Convenient case splitting and induction for trees\ lemma tree_cons_exhaust[case_names Nil Cons]: "(t = Node [] \ P) \ (\r ts. t = Node (r # ts) \ P) \ P" by (cases t) (metis list.exhaust) lemma tree_rev_exhaust[case_names Nil Snoc]: "(t = Node [] \ P) \ (\ts r. t = Node (ts @ [r]) \ P) \ P" by (cases t) (metis rev_exhaust) lemma tree_cons_induct[case_names Nil Cons]: assumes "P (Node [])" and "\t ts. P t \ P (Node ts) \ P (Node (t#ts))" shows "P t" proof (induction "size_tree t" arbitrary: t rule: less_induct) case less then show ?case using assms by (cases t rule: tree_cons_exhaust) auto qed fun lexord_tree where "lexord_tree t (Node []) \ False" | "lexord_tree (Node []) r \ True" | "lexord_tree (Node (t#ts)) (Node (r#rs)) \ lexord_tree t r \ (t = r \ lexord_tree (Node ts) (Node rs))" fun mirror :: "tree \ tree" where "mirror (Node ts) = Node (map mirror (rev ts))" instantiation tree :: linorder begin definition tree_less_def: "(t::tree) < r \ lexord_tree (mirror t) (mirror r)" definition tree_le_def: "(t :: tree) \ r \ t < r \ t = r" lemma lexord_tree_empty2[simp]: "lexord_tree (Node []) r \ r \ Node []" by (cases r rule: tree_cons_exhaust) auto lemma mirror_empty[simp]: "mirror t = Node [] \ t = Node []" by (cases t) auto lemma mirror_not_empty[simp]: "mirror t \ Node [] \ t \ Node []" by (cases t) auto lemma tree_le_empty[simp]: "Node [] \ t" unfolding tree_le_def tree_less_def using mirror_not_empty by auto lemma tree_less_empty_iff: "Node [] < t \ t \ Node []" unfolding tree_less_def by simp lemma not_tree_less_empty[simp]: "\ t < Node []" unfolding tree_less_def by simp lemma tree_le_empty2_iff[simp]: "t \ Node [] \ t = Node []" unfolding tree_le_def by simp lemma lexord_tree_antisym: "lexord_tree t r \ \ lexord_tree r t" by (induction r t rule: lexord_tree.induct) auto lemma tree_less_antisym: "(t::tree) < r \ \ r < t" unfolding tree_less_def using lexord_tree_antisym by blast lemma lexord_tree_not_eq: "lexord_tree t r \ t \ r" by (induction r t rule: lexord_tree.induct) auto lemma tree_less_not_eq: "(t::tree) < r \ t \ r" unfolding tree_less_def using lexord_tree_not_eq by blast lemma lexord_tree_irrefl: "\ lexord_tree t t" using lexord_tree_not_eq by blast lemma tree_less_irrefl: "\ (t::tree) < t" unfolding tree_less_def using lexord_tree_irrefl by blast lemma lexord_tree_eq_iff: "\ lexord_tree t r \ \ lexord_tree r t \ t = r" using lexord_tree_empty2 by (induction t r rule: lexord_tree.induct, fastforce+) lemma mirror_mirror: "mirror (mirror t) = t" by (induction t rule: mirror.induct) (simp add: map_idI rev_map) lemma mirror_inj: "mirror t = mirror r \ t = r" using mirror_mirror by metis lemma tree_less_eq_iff: "\ (t::tree) < r \ \ r < t \ t = r" unfolding tree_less_def using lexord_tree_eq_iff mirror_inj by blast lemma lexord_tree_trans: "lexord_tree t r \ lexord_tree r s \ lexord_tree t s" proof (induction t s arbitrary: r rule: lexord_tree.induct) case (1 t) then show ?case by auto next case (2 va vb) then show ?case by auto next case (3 t ts s ss) then show ?case by (cases r rule: tree_cons_exhaust) auto qed instance proof fix t r s :: tree show "t < r \ t \ r \ \ r \ t" unfolding tree_le_def using tree_less_antisym tree_less_irrefl by auto show "t \ t" unfolding tree_le_def by simp show "t \ r \ r \ t \ t = r" unfolding tree_le_def using tree_less_antisym by blast show "t \ r \ r \ t" unfolding tree_le_def using tree_less_eq_iff by blast show "t \ r \ r \ s \ t \ s" unfolding tree_le_def tree_less_def using lexord_tree_trans by blast qed end lemma tree_size_children: "tree_size (Node ts) = Suc n \ t \ set ts \ tree_size t \ n" by (auto simp: le_add1 sum_list_map_remove1) lemma tree_size_ge_1: "tree_size t \ 1" by (cases t) auto lemma tree_size_ne_0: "tree_size t \ 0" by (cases t) auto lemma tree_size_1_iff: "tree_size t = 1 \ t = Node []" using tree_size_ne_0 by (cases t rule: tree_cons_exhaust) auto lemma length_children: "tree_size (Node ts) = Suc n \ length ts \ n" by (induction ts arbitrary: n, auto, metis add_mono plus_1_eq_Suc tree_size_ge_1) lemma height_Node_cons: "height (Node (t#ts)) \ Suc (height t)" by auto lemma height_0_iff: "height t = 0 \ t = Node []" using height.elims by blast lemma height_children: "height (Node ts) = Suc n \ t \ set ts \ height t \ n" by (metis List.finite_set Max_ge diff_Suc_1 finite_imageI height.elims imageI nat.simps(3) tree.inject) lemma height_children_le_height: "\t \ set ts. height t \ n \ height (Node ts) \ Suc n" by (cases ts) auto lemma mirror_iff: "mirror t = Node ts \ t = Node (map mirror (rev ts))" by (metis mirror.simps mirror_mirror) lemma mirror_append: "mirror (Node (ts@rs)) = Node (map mirror (rev rs) @ map mirror (rev ts))" by (induction ts) auto lemma lexord_tree_snoc: "lexord_tree (Node ts) (Node (ts@[t]))" by (induction ts) auto lemma tree_less_cons: "Node ts < Node (t#ts)" unfolding tree_less_def using lexord_tree_snoc by simp lemma tree_le_cons: "Node ts \ Node (t#ts)" unfolding tree_le_def using tree_less_cons by simp lemma tree_less_cons': "t \ Node rs \ t < Node (r#rs)" using tree_less_cons by (simp add: order_le_less_trans) lemma tree_less_snoc2_iff[simp]: "Node (ts@[t]) < Node (rs@[r]) \ t < r \ (t = r \ Node ts < Node rs)" unfolding tree_less_def using mirror_inj by auto lemma tree_le_snoc2_iff[simp]: "Node (ts@[t]) \ Node (rs@[r]) \ t < r \ (t = r \ Node ts \ Node rs)" unfolding tree_le_def by auto lemma lexord_tree_cons2[simp]: "lexord_tree (Node (ts@[t])) (Node (ts@[r])) \ lexord_tree t r" by (induction ts) (auto simp: lexord_tree_irrefl) lemma tree_less_cons2[simp]: "Node (t#ts) < Node (r#ts) \ t < r" unfolding tree_less_def using lexord_tree_cons2 by simp lemma tree_le_cons2[simp]: "Node (t#ts) \ Node (r#ts) \ t \ r" unfolding tree_le_def using tree_less_cons2 by blast lemma tree_less_sorted_snoc: "sorted (ts@[r]) \ Node ts < Node (ts@[r])" unfolding tree_less_def by (induction ts rule: rev_induct, auto, metis leD lexord_tree_eq_iff sorted2 sorted_wrt_append tree_less_def, metis dual_order.strict_iff_not list.set_intros(2) nle_le sorted2 sorted_append tree_less_def) lemma lexord_tree_comm_prefix[simp]: "lexord_tree (Node (ss@ts)) (Node (ss@rs)) \ lexord_tree (Node ts) (Node rs)" using lexord_tree_antisym by (induction ss) auto lemma less_tree_comm_suffix[simp]: "Node (ts@ss) < Node (rs@ss) \ Node ts < Node rs" unfolding tree_less_def by simp lemma tree_le_comm_suffix[simp]: "Node (ts@ss) \ Node (rs@ss) \ Node ts \ Node rs" unfolding tree_le_def by simp lemma tree_less_comm_suffix2: "t < r \ Node (ts@t#ss) < Node (r#ss)" unfolding tree_less_def using lexord_tree_comm_prefix by simp lemma lexord_tree_append[simp]: "lexord_tree (Node ts) (Node (ts@rs)) \ rs \ []" using lexord_tree_irrefl by (induction ts) auto lemma tree_less_append[simp]: "Node ts < Node (rs@ts) \ rs \ []" unfolding tree_less_def by simp lemma tree_le_append: "Node ts \ Node (ss@ts)" unfolding tree_le_def by simp lemma tree_less_singleton_iff[simp]: "Node (ts@[t]) < Node [r] \ t < r" unfolding tree_less_def by simp lemma tree_le_singleton_iff[simp]: "Node (ts@[t]) \ Node [r] \ t < r \ (t = r \ ts = [])" unfolding tree_le_def by auto lemma lexord_tree_nested: "lexord_tree t (Node [t])" proof (induction t rule: tree_cons_induct) case Nil then show ?case by auto next case (Cons t ts) then show ?case by (cases t rule: tree_cons_exhaust) auto qed lemma tree_less_nested: "t < Node [t]" unfolding tree_less_def using lexord_tree_nested by auto lemma tree_le_nested: "t \ Node [t]" unfolding tree_le_def using tree_less_nested by auto lemma lexord_tree_iff: "lexord_tree t r \ (\ts t' ss rs r'. t = Node (ss @ t' # ts) \ r = Node (ss @ r' # rs) \ lexord_tree t' r') \ (\ts rs. rs \ [] \ t = Node ts \ r = Node (ts @ rs))" (is "?l \ ?r") proof show "?l \ ?r" proof- assume lexord: "lexord_tree t r" obtain ts where ts: "t = Node ts" by (cases t) auto obtain rs where rs: "r = Node rs" by (cases r) auto obtain ss ts' rs' where prefix: "ts = ss @ ts' \ rs = ss @ rs' \ (ts' = [] \ rs' = [] \ hd ts' \ hd rs')" using longest_common_prefix by blast then have "ts' = [] \ lexord_tree (hd ts') (hd rs')" using lexord unfolding ts rs by (auto, metis lexord_tree.simps(1) lexord_tree.simps(3) list.exhaust_sel) then show ?thesis using prefix by (metis append.right_neutral lexord lexord_tree.simps(1) lexord_tree_comm_prefix list.exhaust_sel rs ts) qed show "?r \ ?l" by auto qed lemma tree_less_iff: "t < r \ (\ts t' ss rs r'. t = Node (ts @ t' # ss) \ r = Node (rs @ r' # ss) \ t' < r') \ (\ts rs. rs \ [] \ t = Node ts \ r = Node (rs @ ts))" (is "?l \ ?r") proof show "?l \ ?r" unfolding tree_less_def using lexord_tree_iff[of "mirror t" "mirror r", unfolded mirror_iff] by (simp, metis append_Nil lexord_tree_eq_iff mirror_mirror) next show "?r \ ?l" by (auto simp: order_le_neq_trans tree_le_append, meson dual_order.strict_trans1 tree_le_append tree_less_comm_suffix2) qed lemma tree_empty_cons_lt_le: "r < Node (Node [] # ts) \ r \ Node ts" proof (induction ts arbitrary: r rule: rev_induct) case Nil then show ?case by (cases r rule: tree_rev_exhaust) auto next case (snoc x xs) then show ?case proof (cases r rule: tree_rev_exhaust) case Nil then show ?thesis by auto next case (Snoc rs r1) then show ?thesis using snoc by (auto, (metis append_Cons tree_less_snoc2_iff)+) qed qed fun regular :: "tree \ bool" where "regular (Node ts) \ sorted ts \ (\t\set ts. regular t)" definition n_trees :: "nat \ tree set" where "n_trees n = {t. tree_size t = n}" definition regular_n_trees :: "nat \ tree set" where "regular_n_trees n = {t. tree_size t = n \ regular t}" subsection \Rooted Graphs\ type_synonym 'a rpregraph = "('a set) \ ('a edge set) \ 'a" locale rgraph = graph_system + fixes r assumes root_wf: "r \ V" locale rtree = tree + rgraph begin definition subtrees :: "'a rpregraph set" where "subtrees = (let (V',E') = remove_vertex r in (\C. (C, graph_system.induced_edges E' C, THE r'. r' \ C \ vert_adj r r')) ` ulgraph.connected_components V' E')" lemma rtree_subtree: assumes subtree: "(S,E\<^sub>S,r\<^sub>S) \ subtrees" shows "rtree S E\<^sub>S r\<^sub>S" proof- obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce interpret subg: ulsubgraph V' E' V E unfolding ulsubgraph_def using subgraph_remove_vertex subtree ulgraph_axioms remove_vertex by blast interpret g': fin_ulgraph V' E' by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms) have conn_component: "S \ g'.connected_components" using subtree remove_vertex unfolding subtrees_def by auto then interpret subg': subgraph S E\<^sub>S V' E' using g'.connected_component_subgraph subtree remove_vertex unfolding subtrees_def by auto interpret subg': ulsubgraph S E\<^sub>S V' E' by unfold_locales interpret S: connected_ulgraph S E\<^sub>S using g'.connected_components_connected_ulgraphs conn_component subtree remove_vertex unfolding subtrees_def by auto interpret S: fin_connected_ulgraph S E\<^sub>S using subg'.verts_ss g'.finV by unfold_locales (simp add: finite_subset) interpret S: tree S E\<^sub>S using subg.is_cycle2 subg'.is_cycle2 no_cycles by (unfold_locales, blast) show ?thesis using theI'[OF unique_adj_vert_removed[OF root_wf remove_vertex conn_component]] subtree remove_vertex by unfold_locales (auto simp: subtrees_def) qed lemma finite_subtrees: "finite subtrees" proof- obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce then interpret subg: subgraph V' E' V E using subgraph_remove_vertex by auto interpret g': fin_ulgraph V' E' by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms) show ?thesis using g'.finite_connected_components remove_vertex unfolding subtrees_def by simp qed lemma remove_root_subtrees: assumes remove_vertex: "remove_vertex r = (V',E')" and conn_component: "C \ ulgraph.connected_components V' E'" shows "rtree C (graph_system.induced_edges E' C) (THE r'. r' \ C \ vert_adj r r')" proof- interpret subg: ulsubgraph V' E' V E unfolding ulsubgraph_def using subgraph_remove_vertex remove_vertex ulgraph_axioms by blast interpret g': fin_ulgraph V' E' by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms) interpret subg': ulsubgraph C "graph_system.induced_edges E' C" V' E' by (simp add: conn_component g'.connected_component_subgraph g'.ulgraph_axioms ulsubgraph.intro) interpret C: fin_connected_ulgraph C "graph_system.induced_edges E' C" by (simp add: fin_connected_ulgraph.intro fin_ulgraph.intro g'.fin_graph_system_axioms g'.ulgraph_axioms subg'.is_finite_subgraph subg'.is_subgraph_ulgraph conn_component g'.connected_components_connected_ulgraphs) interpret C: tree C "graph_system.induced_edges E' C" using subg.is_cycle2 subg'.is_cycle2 no_cycles by (unfold_locales, blast) show ?thesis using theI'[OF unique_adj_vert_removed[OF root_wf remove_vertex conn_component]] by unfold_locales simp qed end subsection \Rooted Graph Isomorphism\ fun app_rgraph_isomorphism :: "('a \ 'b) \ 'a rpregraph \ 'b rpregraph" where "app_rgraph_isomorphism f (V,E,r) = (f ` V, ((`) f) ` E, f r)" locale rgraph_isomorphism = G: rgraph V\<^sub>G E\<^sub>G r\<^sub>G + graph_isomorphism V\<^sub>G E\<^sub>G V\<^sub>H E\<^sub>H f for V\<^sub>G E\<^sub>G r\<^sub>G V\<^sub>H E\<^sub>H r\<^sub>H f + assumes root_preserving: "f r\<^sub>G = r\<^sub>H" begin interpretation H: graph_system V\<^sub>H E\<^sub>H using graph_system_H . lemma rgraph_H: "rgraph V\<^sub>H E\<^sub>H r\<^sub>H" using root_preserving bij_f G.root_wf V\<^sub>H_def by unfold_locales blast interpretation H: rgraph V\<^sub>H E\<^sub>H r\<^sub>H using rgraph_H . lemma rgraph_isomorphism_inv: "rgraph_isomorphism V\<^sub>H E\<^sub>H r\<^sub>H V\<^sub>G E\<^sub>G r\<^sub>G inv_iso" proof- interpret iso: graph_isomorphism V\<^sub>H E\<^sub>H V\<^sub>G E\<^sub>G inv_iso using graph_isomorphism_inv . show ?thesis using G.root_wf inj_f inv_iso_def root_preserving the_inv_into_f_f by unfold_locales fastforce qed end fun rgraph_isomorph :: "'a rpregraph \ 'b rpregraph \ bool" (infix "\\<^sub>r" 50) where "(V\<^sub>G,E\<^sub>G,r\<^sub>G) \\<^sub>r (V\<^sub>H,E\<^sub>H,r\<^sub>H) \ (\f. rgraph_isomorphism V\<^sub>G E\<^sub>G r\<^sub>G V\<^sub>H E\<^sub>H r\<^sub>H f)" lemma (in rgraph) rgraph_isomorphism_id: "rgraph_isomorphism V E r V E r id" using graph_isomorphism_id rgraph_isomorphism.intro rgraph_axioms unfolding rgraph_isomorphism_axioms_def by fastforce lemma (in rgraph) rgraph_isomorph_refl: "(V,E,r) \\<^sub>r (V,E,r)" using rgraph_isomorphism_id by auto lemma rgraph_isomorph_sym: "G \\<^sub>r H \ H \\<^sub>r G" using rgraph_isomorphism.rgraph_isomorphism_inv by (cases G, cases H) fastforce lemma rgraph_isomorphism_trans: "rgraph_isomorphism V\<^sub>G E\<^sub>G r\<^sub>G V\<^sub>H E\<^sub>H r\<^sub>H f \ rgraph_isomorphism V\<^sub>H E\<^sub>H r\<^sub>H V\<^sub>F E\<^sub>F r\<^sub>F g \ rgraph_isomorphism V\<^sub>G E\<^sub>G r\<^sub>G V\<^sub>F E\<^sub>F r\<^sub>F (g o f)" using graph_isomorphism_trans unfolding rgraph_isomorphism_def rgraph_isomorphism_axioms_def by fastforce lemma rgraph_isomorph_trans: "transp (\\<^sub>r)" using rgraph_isomorphism_trans unfolding transp_def by fastforce lemma (in rtree) rgraph_isomorphis_app_iso: "inj_on f V \ app_rgraph_isomorphism f (V,E,r) = (V',E',r') \ rgraph_isomorphism V E r V' E' r' f" by unfold_locales (auto simp: bij_betw_def) lemma (in rtree) rgraph_isomorph_app_iso: "inj_on f V \ (V, E, r) \\<^sub>r app_rgraph_isomorphism f (V, E, r)" using rgraph_isomorphis_app_iso by fastforce subsection \Conversion between unlabeled, ordered, rooted trees and tree graphs\ datatype 'a ltree = LNode 'a "'a ltree list" fun ltree_size :: "'a ltree \ nat" where "ltree_size (LNode r ts) = Suc (\t\ts. ltree_size t)" fun root_ltree :: "'a ltree \ 'a" where "root_ltree (LNode r ts) = r" fun nodes_ltree :: "'a ltree \ 'a set" where "nodes_ltree (LNode r ts) = {r} \ (\t\set ts. nodes_ltree t)" fun relabel_ltree :: "('a \ 'b) \ 'a ltree \ 'b ltree" where "relabel_ltree f (LNode r ts) = LNode (f r) (map (relabel_ltree f) ts)" fun distinct_ltree_nodes :: "'a ltree \ bool" where "distinct_ltree_nodes (LNode a ts) \ (\t\set ts. a \ nodes_ltree t) \ distinct ts \ disjoint_family_on nodes_ltree (set ts) \ (\t\set ts. distinct_ltree_nodes t)" fun postorder_label_aux :: "nat \ tree \ nat \ nat ltree" where "postorder_label_aux n (Node []) = (n, LNode n [])" | "postorder_label_aux n (Node (t#ts)) = (let (n', t') = postorder_label_aux n t in case postorder_label_aux (Suc n') (Node ts) of (n'', LNode r ts') \ (n'', LNode r (t'#ts')))" definition postorder_label :: "tree \ nat ltree" where "postorder_label t = snd (postorder_label_aux 0 t)" fun tree_ltree :: "'a ltree \ tree" where "tree_ltree (LNode r ts) = Node (map tree_ltree ts)" fun regular_ltree :: "'a ltree \ bool" where "regular_ltree (LNode r ts) \ sorted_wrt (\t s. tree_ltree t \ tree_ltree s) ts \ (\t\set ts. regular_ltree t)" datatype 'a stree = SNode 'a "'a stree fset" lemma stree_size_child_lt[termination_simp]: "t |\| ts \ size t < Suc (\s\fset ts. Suc (size s))" using sum_nonneg_leq_bound zero_le finite_fset Suc_le_eq less_SucI by metis lemma stree_size_child_lt'[termination_simp]: "t \ fset ts \ size t < Suc (\s\fset ts. Suc (size s))" using stree_size_child_lt by metis fun stree_size :: "'a stree \ nat" where "stree_size (SNode r ts) = Suc (fsum stree_size ts)" definition n_strees :: "nat \ 'a stree set" where "n_strees n = {t. stree_size t = n}" fun root_stree :: "'a stree \ 'a" where "root_stree (SNode a ts) = a" fun nodes_stree :: "'a stree \ 'a set" where "nodes_stree (SNode a ts) = {a} \ (\t\fset ts. nodes_stree t)" fun tree_graph_edges :: "'a stree \ 'a edge set" where "tree_graph_edges (SNode a ts) = ((\t. {a, root_stree t}) ` fset ts) \ (\t\fset ts. tree_graph_edges t)" fun distinct_stree_nodes :: "'a stree \ bool" where "distinct_stree_nodes (SNode a ts) \ (\t\fset ts. a \ nodes_stree t) \ disjoint_family_on nodes_stree (fset ts) \ (\t\fset ts. distinct_stree_nodes t)" fun ltree_stree :: "'a stree \ 'a ltree" where "ltree_stree (SNode r ts) = LNode r (SOME xs. fset_of_list xs = ltree_stree |`| ts \ distinct xs \ sorted_wrt (\t s. tree_ltree t \ tree_ltree s) xs)" fun stree_ltree :: "'a ltree \ 'a stree" where "stree_ltree (LNode r ts) = SNode r (fset_of_list (map stree_ltree ts))" definition tree_graph_stree :: "'a stree \ 'a rpregraph" where "tree_graph_stree t = (nodes_stree t, tree_graph_edges t, root_stree t)" function stree_of_graph :: "'a rpregraph \ 'a stree" where "stree_of_graph (V,E,r) = (if \ rtree V E r then undefined else SNode r (Abs_fset (stree_of_graph ` rtree.subtrees V E r)))" by pat_completeness auto termination proof (relation "measure (\p. card (fst p))", auto) fix r :: 'a and V :: "'a set" and E :: "'a edge set" and S :: "'a set" and E\<^sub>S :: "'a edge set" and r\<^sub>S :: 'a assume rtree: "rtree V E r" assume subtree: "(S, E\<^sub>S, r\<^sub>S) \ rtree.subtrees V E r" interpret rtree V E r using rtree . obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce then interpret subg: subgraph V' E' V E using subgraph_remove_vertex by simp interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph fin_graph_system_axioms subg.is_subgraph_ulgraph ulgraph_axioms by blast have "S \ g'.connected_components" using subtree remove_vertex unfolding subtrees_def by auto then have card_C_V':"card S \ card V'" using g'.connected_component_wf g'.finV card_mono by metis have "card V' < card V" using remove_vertex root_wf finV card_Diff1_less unfolding remove_vertex_def by fast then show "card S < card V" using card_C_V' by simp qed definition tree_graph :: "tree \ nat rpregraph" where "tree_graph t = tree_graph_stree (stree_ltree (postorder_label t))" fun relabel_stree :: "('a \ 'b) \ 'a stree \ 'b stree" where "relabel_stree f (SNode r ts) = SNode (f r) ((relabel_stree f) |`| ts)" lemma root_ltree_wf: "root_ltree t \ nodes_ltree t" by (cases t) auto lemma root_relabel_ltree[simp]: "root_ltree (relabel_ltree f t) = f (root_ltree t)" by (cases t) simp lemma nodes_relabel_ltree[simp]: "nodes_ltree (relabel_ltree f t) = f ` nodes_ltree t" by (induction t) auto lemma finite_nodes_ltree: "finite (nodes_ltree t)" by (induction t) auto lemma root_stree_wf: "root_stree t \ nodes_stree t" by (cases t) auto lemma tree_graph_edges_wf: "e \ tree_graph_edges t \ e \ nodes_stree t" using root_stree_wf by (induction t rule: tree_graph_edges.induct) auto lemma card_tree_graph_edges_distinct: "distinct_stree_nodes t \ e \ tree_graph_edges t \ card e = 2" using root_stree_wf card_2_iff by (induction t rule: tree_graph_edges.induct) (auto, fast+) lemma nodes_stree_non_empty: "nodes_stree t \ {}" by (cases t rule: nodes_stree.cases) auto lemma finite_nodes_stree: "finite (nodes_stree t)" by (induction t rule: nodes_stree.induct) auto lemma finite_tree_graph_edges: "finite (tree_graph_edges t)" by (induction t rule: tree_graph_edges.induct) auto lemma root_relabel_stree[simp]: "root_stree (relabel_stree f t) = f (root_stree t)" by (cases t) auto lemma nodes_stree_relabel_stree[simp]: "nodes_stree (relabel_stree f t) = f ` nodes_stree t" by (induction t) auto lemma tree_graph_edges_relabel_stree[simp]: "tree_graph_edges (relabel_stree f t) = ((`) f) ` tree_graph_edges t" by (induction t) (simp add: image_image image_Un image_Union) lemma nodes_stree_ltree[simp]: "nodes_stree (stree_ltree t) = nodes_ltree t" by (induction t) (auto simp: fset_of_list.rep_eq) lemma distinct_sorted_wrt_list: "\xs. fset_of_list xs = A \ distinct xs \ sorted_wrt (\t s. (f t :: 'b::linorder) \ f s) xs" proof- obtain xs where "fset_of_list xs = A \ distinct xs" by (metis finite_distinct_list finite_fset fset_cong fset_of_list.rep_eq) then have "fset_of_list (sort_key f xs) = A \ distinct (sort_key f xs) \ sorted_wrt (\t s. f t \ f s) (sort_key f xs)" using sorted_sort_key sorted_wrt_map by (simp add: fset_of_list.abs_eq, blast) then show ?thesis by blast qed abbreviation "ltree_stree_subtrees ts \ SOME xs. fset_of_list xs = ltree_stree |`| ts \ distinct xs \ sorted_wrt (\t s. tree_ltree t \ tree_ltree s) xs" lemma fset_of_list_ltree_stree_subtrees[simp]: "fset_of_list (ltree_stree_subtrees ts) = ltree_stree |`| ts" using someI_ex[OF distinct_sorted_wrt_list] by fast lemma set_ltree_stree_subtrees[simp]: "set (ltree_stree_subtrees ts) = ltree_stree ` fset ts" using fset_of_list_ltree_stree_subtrees by (metis (mono_tags, lifting) fset.set_map fset_of_list.rep_eq) lemma distinct_ltree_stree_subtrees: "distinct (ltree_stree_subtrees ts)" using someI_ex[OF distinct_sorted_wrt_list] by blast lemma sorted_wrt_ltree_stree_subtrees: "sorted_wrt (\t s. tree_ltree t \ tree_ltree s) (ltree_stree_subtrees ts)" using someI_ex[OF distinct_sorted_wrt_list] by blast lemma nodes_ltree_stree[simp]: "nodes_ltree (ltree_stree t) = nodes_stree t" by (induction t) auto lemma stree_ltree_stree[simp]: "stree_ltree (ltree_stree t) = t" by (induction t) (simp add: fset.map_ident_strong) lemma nodes_tree_graph_stree: "tree_graph_stree t = (V, E, r) \ V = nodes_stree t" by (induction t) (simp add: tree_graph_stree_def) lemma relabel_stree_stree_ltree: "relabel_stree f (stree_ltree t) = stree_ltree (relabel_ltree f t)" by (induction t) (auto simp add: fset_of_list_elem) lemma relabel_stree_relabel_ltree: "relabel_ltree f t1 = t2 \ relabel_stree f (stree_ltree t1) = stree_ltree t2" using relabel_stree_stree_ltree by blast lemma app_rgraph_iso_tree_graph_stree: "app_rgraph_isomorphism f (tree_graph_stree t) = tree_graph_stree (relabel_stree f t)" unfolding tree_graph_stree_def using image_iff mk_disjoint_insert by (induction t) (auto, fastforce+) lemma (in rtree) root_stree_of_graph[simp]: "root_stree (stree_of_graph (V,E,r)) = r" using rtree_axioms by (simp split: prod.split) lemma (in rtree) nodes_stree_stree_of_graph[simp]: "nodes_stree (stree_of_graph (V,E,r)) = V" using rtree_axioms proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct) case (1 V\<^sub>T E\<^sub>T r) then interpret t: rtree V\<^sub>T E\<^sub>T r by simp obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def) interpret subg: subgraph V' E' V\<^sub>T E\<^sub>T using t.subgraph_remove_vertex VE' by metis interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast then have "nodes_stree (stree_of_graph (V\<^sub>T, E\<^sub>T, r)) = {r} \ V'" using 1 using VE' t.rtree_subtree g'.Union_connected_components by (simp add: Abs_fset_inverse t.subtrees_def) then show ?case using VE' t.root_wf unfolding t.remove_vertex_def by auto qed lemma (in rtree) tree_graph_edges_stree_of_graph[simp]: "tree_graph_edges (stree_of_graph (V,E,r)) = E" using rtree_axioms proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct) case (1 V\<^sub>T E\<^sub>T r) then interpret t: rtree V\<^sub>T E\<^sub>T r by simp obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def) interpret subg: subgraph V' E' V\<^sub>T E\<^sub>T using t.subgraph_remove_vertex VE' by metis interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast then have fset_Abs_fset_subtrees[simp]: "fset (Abs_fset (stree_of_graph ` t.subtrees)) = stree_of_graph ` t.subtrees" by (simp add: Abs_fset_inverse) have root_edges: "(\x. {r, root_stree x}) ` stree_of_graph ` t.subtrees = {e\E\<^sub>T. r \ e}" (is "?l = ?r") proof- have "e \ ?l" if "e \ ?r" for e proof- obtain r' where e: "e = {r, r'}" using \e\?r\ by (metis (no_types, lifting) CollectD insert_commute insert_iff singleton_iff t.obtain_edge_pair_adj) then have "r' \ r" using t.singleton_not_edge \e\?r\ by force then have "r' \ V'" using e \e\?r\ VE' t.remove_vertex_def t.wellformed_alt_snd by fastforce then obtain C where C_conn_component: "C \ g'.connected_components" and "r' \ C" using g'.Union_connected_components by auto have "t.vert_adj r r'" unfolding t.vert_adj_def using \e\?r\ e by blast then have "(THE r'. r' \ C \ t.vert_adj r r') = r'" using t.unique_adj_vert_removed[OF t.root_wf VE' C_conn_component] \r'\C\ by auto then show ?thesis using e \r'\C\ C_conn_component rtree.root_stree_of_graph t.rtree_subtree VE' unfolding t.subtrees_def by (auto simp: image_comp) qed then show ?thesis using t.unique_adj_vert_removed[OF t.root_wf VE'] t.rtree_subtree VE' unfolding t.subtrees_def t.vert_adj_def by (auto, metis (no_types, lifting) theI) qed have "(\S\t.subtrees. tree_graph_edges (stree_of_graph S)) = E'" using 1 VE' t.rtree_subtree g'.Union_induced_edges_connected_components unfolding t.subtrees_def by simp then have "tree_graph_edges (stree_of_graph (V\<^sub>T,E\<^sub>T,r)) = {e\E\<^sub>T. r \ e} \ E'" using root_edges 1(2) by simp - then show ?case using VE' unfolding t.remove_vertex_def t.incident_def by blast + then show ?case using VE' unfolding t.remove_vertex_def t.vincident_def by blast qed lemma (in rtree) tree_graph_stree_of_graph[simp]: "tree_graph_stree (stree_of_graph (V,E,r)) = (V,E,r)" using nodes_stree_stree_of_graph tree_graph_edges_stree_of_graph root_stree_of_graph unfolding tree_graph_stree_def by blast lemma postorder_label_aux_mono: "fst (postorder_label_aux n t) \ n" by (induction n t rule: postorder_label_aux.induct) (auto split: prod.split ltree.split, fastforce) lemma nodes_postorder_label_aux_ge: "postorder_label_aux n t = (n', t') \ v \ nodes_ltree t' \ v \ n" by (induction n t arbitrary: n' t' rule: postorder_label_aux.induct, auto split: prod.splits ltree.splits, (metis fst_conv le_SucI order.trans postorder_label_aux_mono)+) lemma nodes_postorder_label_aux_le: "postorder_label_aux n t = (n', t') \ v \ nodes_ltree t' \ v \ n'" by (induction n t arbitrary: n' t' rule: postorder_label_aux.induct, auto split: prod.splits ltree.splits, metis Suc_leD fst_conv order_trans postorder_label_aux_mono, blast) lemma distinct_nodes_postorder_label_aux: "distinct_ltree_nodes (snd (postorder_label_aux n t))" proof (induction n t rule: postorder_label_aux.induct) case (1 n) then show ?case by (simp add: disjoint_family_on_def) next case (2 n t ts) obtain n' t' where t': "postorder_label_aux n t = (n', t')" by fastforce obtain n'' r ts' where ts': "postorder_label_aux (Suc n') (Node ts) = (n'', LNode r ts')" by (metis eq_snd_iff ltree.exhaust) then have "r \ Suc n'" using nodes_postorder_label_aux_ge by auto then have r_notin_t': "r \ nodes_ltree t'" using nodes_postorder_label_aux_le[OF t'] by fastforce have distinct_subtrees: "distinct (t'#ts')" using 2 t' ts' nodes_postorder_label_aux_le[OF t'] nodes_postorder_label_aux_ge[OF ts'] by (auto, meson not_less_eq_eq root_ltree_wf) have "disjoint_family_on nodes_ltree (set (t'#ts'))" using 2 t' ts' nodes_postorder_label_aux_le[OF t'] nodes_postorder_label_aux_ge[OF ts'] by (simp add: disjoint_family_on_def, meson disjoint_iff not_less_eq_eq) then show ?case using 2 t' ts' r_notin_t' distinct_subtrees by simp qed lemma distinct_nodes_postorder_label: "distinct_ltree_nodes (postorder_label t)" unfolding postorder_label_def using distinct_nodes_postorder_label_aux by simp lemma distinct_nodes_stree_ltree: "distinct_ltree_nodes t \ distinct_stree_nodes (stree_ltree t)" by (induction t) (auto simp: fset_of_list.rep_eq disjoint_family_on_def, fast) fun distinct_edges :: "'a stree \ bool" where "distinct_edges (SNode a ts) \ inj_on (\t. {a, root_stree t}) (fset ts) \ (\t\fset ts. disjnt ((\t. {a, root_stree t}) ` fset ts) (tree_graph_edges t)) \ disjoint_family_on tree_graph_edges (fset ts) \ (\t\fset ts. distinct_edges t)" lemma distinct_nodes_inj_on_root_stree: "distinct_stree_nodes (SNode r ts) \ inj_on root_stree (fset ts)" by (auto simp: disjoint_family_on_def, metis IntI emptyE inj_onI root_stree_wf) lemma distinct_nodes_disjoint_edges: assumes distinct_nodes: "distinct_stree_nodes (SNode a ts)" shows "disjoint_family_on tree_graph_edges (fset ts)" proof- have "tree_graph_edges t1 \ tree_graph_edges t2 = {}" if t1_in_ts: "t1 \ fset ts" and t2_in_ts: "t2 \ fset ts" and "t1 \ t2" for t1 t2 proof- have "\e\tree_graph_edges t1. e \ tree_graph_edges t2" proof fix e assume e_in_edges_t1: "e \ tree_graph_edges t1" then have "e \ {}" using t1_in_ts card_tree_graph_edges_distinct distinct_nodes by fastforce then have "\v\nodes_stree t1. v \ e" using tree_graph_edges_wf e_in_edges_t1 by blast then show "e \ tree_graph_edges t2" using \t1\t2\ distinct_nodes t1_in_ts t2_in_ts tree_graph_edges_wf by (auto simp: disjoint_family_on_def, blast) qed then show ?thesis by blast qed then show ?thesis unfolding disjoint_family_on_def by blast qed lemma card_nodes_edges: "distinct_stree_nodes t \ card (nodes_stree t) = Suc (card (tree_graph_edges t))" proof (induction t rule: tree_graph_edges.induct) case (1 a ts) let ?t = "SNode a ts" have "inj_on (\t. {a, root_stree t}) (fset ts)" using distinct_nodes_inj_on_root_stree[OF 1(2)] unfolding inj_on_def doubleton_eq_iff by blast then have card_root_edges: "card ((\t. {a, root_stree t}) ` fset ts) = card (fset ts)" using card_image by blast have finite_Un: "finite (\t\fset ts. nodes_stree t)" using finite_Union finite_nodes_stree finite_fset by auto then have "card (nodes_stree ?t) = Suc (card (\t\fset ts. nodes_stree t))" using 1(2) card_insert_disjoint finite_Un by simp also have "\ = Suc (\t\fset ts. card (nodes_stree t))" using 1(2) card_UN_disjoint' finite_nodes_stree finite_fset by fastforce also have "\ = Suc (\t\fset ts. Suc (card (tree_graph_edges t)))" using 1 by simp also have "\ = Suc (card (fset ts) + (\t\fset ts. card (tree_graph_edges t)))" by (metis add.commute sum_Suc) also have "\ = Suc (card ((\t. {a, root_stree t}) ` fset ts) + (\t\fset ts. card (tree_graph_edges t)))" using card_root_edges by simp also have "\ = Suc (card ((\x. {a, root_stree x}) ` fset ts) + card (\ (tree_graph_edges ` fset ts)))" using distinct_nodes_disjoint_edges[OF 1(2)] card_UN_disjoint' finite_tree_graph_edges by fastforce also have "\ = Suc (card ((\x. {a, root_stree x}) ` fset ts \ (\ (tree_graph_edges ` fset ts))))" (is "Suc (card ?r + card ?Un) = Suc (card (?r \ ?Un))") proof- have "\t \ fset ts. \e \ tree_graph_edges t. a \ e" using 1(2) tree_graph_edges_wf by auto then have disjnt: "disjnt ?r ?Un" using disjoint_UN_iff by (auto simp: disjnt_def) show ?thesis using card_Un_disjnt[OF _ _ disjnt] finite_tree_graph_edges by fastforce qed finally show ?case by simp qed lemma tree_tree_graph_edges: "distinct_stree_nodes t \ tree (nodes_stree t) (tree_graph_edges t)" proof (induction t rule: tree_graph_edges.induct) case (1 a ts) let ?t = "SNode a ts" have "\e. e \ tree_graph_edges ?t \ 0 < card e \ card e \ 2" using card_tree_graph_edges_distinct 1 by (metis order_refl pos2) then interpret g: fin_ulgraph "nodes_stree ?t" "tree_graph_edges ?t" using tree_graph_edges_wf finite_nodes_stree by (unfold_locales) blast+ have "g.vert_connected a v" if t: "t \ fset ts" and v: "v \ nodes_stree t" for t v proof- interpret t: tree "nodes_stree t" "tree_graph_edges t" using 1 t by auto interpret subg: ulsubgraph "nodes_stree t" "tree_graph_edges t" "nodes_stree ?t" "tree_graph_edges ?t" using t by unfold_locales auto have conn_root_v: "g.vert_connected (root_stree t) v" using subg.vert_connected v root_stree_wf t.vertices_connected by blast have "{a, root_stree t} \ tree_graph_edges ?t" using t by auto then have "g.vert_connected a (root_stree t)" using g.vert_connected_neighbors by blast then show ?thesis using conn_root_v g.vert_connected_trans by blast qed then have "\v\nodes_stree ?t. g.vert_connected a v" using g.vert_connected_id by auto then have "g.is_connected_set (nodes_stree ?t)" using g.vert_connected_trans g.vert_connected_rev unfolding g.is_connected_set_def by blast then interpret g: fin_connected_ulgraph "nodes_stree ?t" "tree_graph_edges ?t" by unfold_locales auto show ?case using card_E_treeI card_nodes_edges 1(2) g.fin_connected_ulgraph_axioms by blast qed lemma rtree_tree_graph_edges: assumes distinct_nodes: "distinct_stree_nodes t" shows "rtree (nodes_stree t) (tree_graph_edges t) (root_stree t)" proof- interpret tree "nodes_stree t" "tree_graph_edges t" using distinct_nodes tree_tree_graph_edges by blast show ?thesis using root_stree_wf by unfold_locales blast qed lemma rtree_tree_graph_stree: "distinct_stree_nodes t \ tree_graph_stree t = (V,E,r) \ rtree V E r" using rtree_tree_graph_edges unfolding tree_graph_stree_def by blast lemma rtree_tree_graph: "tree_graph t = (V,E,r) \ rtree V E r" unfolding tree_graph_def using distinct_nodes_postorder_label rtree_tree_graph_stree distinct_nodes_stree_ltree by fast text "Cardinality of the resulting rooted tree is correct" lemma ltree_size_postorder_label_aux: "ltree_size (snd (postorder_label_aux n t)) = tree_size t" by (induction n t rule: postorder_label_aux.induct) (auto split: prod.split ltree.split) lemma ltree_size_postorder_label: "ltree_size (postorder_label t) = tree_size t" unfolding postorder_label_def using ltree_size_postorder_label_aux by blast lemma distinct_nodes_ltree_size_card_nodes: "distinct_ltree_nodes t \ ltree_size t = card (nodes_ltree t)" proof (induction t) case (LNode r ts) have "finite (\ (nodes_ltree ` set ts))" using finite_nodes_ltree by blast then show ?case using LNode disjoint_family_on_disjoint_image by (auto simp: sum_list_distinct_conv_sum_set card_UN_disjoint') qed lemma distinct_nodes_stree_size_card_nodes: "distinct_stree_nodes t \ stree_size t = card (nodes_stree t)" proof (induction t) case (SNode r ts) have "finite (\ (nodes_stree ` fset ts))" using finite_nodes_stree by auto then show ?case using SNode disjoint_family_on_disjoint_image by (auto simp: fsum.F.rep_eq card_UN_disjoint') qed lemma stree_size_stree_ltree: "distinct_ltree_nodes t \ stree_size (stree_ltree t) = ltree_size t" by (simp add: distinct_nodes_ltree_size_card_nodes distinct_nodes_stree_ltree distinct_nodes_stree_size_card_nodes) lemma card_tree_graph_stree: "distinct_stree_nodes t \ tree_graph_stree t = (V,E,r) \ card V = stree_size t" by (simp add: distinct_nodes_stree_size_card_nodes) (metis nodes_tree_graph_stree) lemma card_tree_graph: "tree_graph t = (V,E,r) \ card V = tree_size t" unfolding tree_graph_def using ltree_size_postorder_label stree_size_stree_ltree card_tree_graph_stree by (metis distinct_nodes_postorder_label distinct_nodes_stree_ltree) lemma [termination_simp]: "(t, s) \ set (zip ts ss) \ size t < Suc (size_list size ts)" by (metis less_not_refl not_less_eq set_zip_leftD size_list_estimation) fun obtain_ltree_isomorphism :: "'a ltree \ 'b ltree \ ('a \ 'b)" where "obtain_ltree_isomorphism (LNode r1 ts) (LNode r2 ss) = fold (++) (map2 obtain_ltree_isomorphism ts ss) [r1\r2]" fun postorder_relabel_aux :: "nat \ 'a ltree \ nat \ (nat \ 'a)" where "postorder_relabel_aux n (LNode r []) = (n, [n \ r])" | "postorder_relabel_aux n (LNode r (t#ts)) = (let (n', f\<^sub>t) = postorder_relabel_aux n t; (n'', f\<^sub>t\<^sub>s) = postorder_relabel_aux (Suc n') (LNode r ts) in (n'', f\<^sub>t ++ f\<^sub>t\<^sub>s))" definition postorder_relabel :: "'a ltree \ (nat \ 'a)" where "postorder_relabel t = snd (postorder_relabel_aux 0 t)" lemma fst_postorder_label_aux_tree_ltree: "fst (postorder_label_aux n (tree_ltree t)) = fst (postorder_relabel_aux n t)" by (induction n t rule: postorder_relabel_aux.induct) (auto split: prod.split ltree.split) lemma dom_postorder_relabel_aux: "dom (snd (postorder_relabel_aux n t)) = nodes_ltree (snd (postorder_label_aux n (tree_ltree t)))" proof (induction n t rule: postorder_relabel_aux.induct) case (1 n r) then show ?case by (auto split: if_splits) next case (2 n r t ts) obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel) obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust) show ?case using 2 f_t f_ts t' ts' by auto qed lemma ran_postorder_relabel_aux: "ran (snd (postorder_relabel_aux n t)) = nodes_ltree t" proof (induction n t rule: postorder_relabel_aux.induct) case (1 n r) then show ?case by (simp add: ran_def) next case (2 n r t ts) obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce have "dom f_t \ dom f_ts = {}" using dom_postorder_relabel_aux f_t f_ts by (metis disjoint_iff fst_eqD fst_postorder_label_aux_tree_ltree nodes_postorder_label_aux_ge nodes_postorder_label_aux_le not_less_eq_eq prod.exhaust_sel snd_conv) then show ?case using 2 f_t f_ts by (simp add: ran_map_add) qed lemma relabel_ltree_eq: "\v\nodes_ltree t. f v = g v \ relabel_ltree f t = relabel_ltree g t" by (induction t) auto lemma relabel_postorder_relabel_aux: "relabel_ltree (the o snd (postorder_relabel_aux n t)) (snd (postorder_label_aux n (tree_ltree t))) = t" proof (induction n t rule: postorder_relabel_aux.induct) case (1 n r) then show ?case by auto next case (2 n r t ts) obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel) obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust) have ts'_in_f_ts: "\v\nodes_ltree (LNode r' ts'). v \ dom f_ts" using f_ts ts' dom_postorder_relabel_aux by (metis snd_conv) have "\v\nodes_ltree t'. v \ dom f_ts" using f_ts t' ts' f_t dom_postorder_relabel_aux by (metis nodes_postorder_label_aux_ge nodes_postorder_label_aux_le not_less_eq_eq snd_conv) then show ?case using 2 f_t f_ts t' ts' ts'_in_f_ts by (auto intro!: relabel_ltree_eq simp: map_add_dom_app_simps(3) map_add_dom_app_simps(1), smt (verit, ccfv_threshold) map_add_dom_app_simps(1) map_eq_conv relabel_ltree_eq) qed lemma relabel_postorder_relabel: "relabel_ltree (the o postorder_relabel t) (postorder_label (tree_ltree t)) = t" unfolding postorder_relabel_def postorder_label_def using relabel_postorder_relabel_aux by auto lemma relabel_postorder_aux_inj: "distinct_ltree_nodes t \ inj_on (the o snd (postorder_relabel_aux n t)) (nodes_ltree (snd (postorder_label_aux n (tree_ltree t))))" proof (induction n t rule: postorder_relabel_aux.induct) case (1 n r) then show ?case by auto next case (2 n r t ts) have disjoint_family_on_ts: "disjoint_family_on nodes_ltree (set ts)" using 2(3) by (simp add: disjoint_family_on_def) obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel) obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')" using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust) have t'_in_dom_f_t: "nodes_ltree t' \ dom f_t" using f_t t' dom_postorder_relabel_aux by (metis order_refl snd_conv) have "\v\nodes_ltree t'. v \ dom f_ts" using f_ts ts' t' dom_postorder_relabel_aux by (metis nodes_postorder_label_aux_ge nodes_postorder_label_aux_le not_less_eq_eq snd_conv) then have f_t': "\v\nodes_ltree t'. the ((f_t ++ f_ts) v) = the (f_t v)" by (simp add: map_add_dom_app_simps(3)) have "inj_on (\v. the (f_t v)) (nodes_ltree t')" using 2 ts' f_ts f_t t' disjoint_family_on_ts by auto then have inj_on_t': "inj_on (\v. the ((f_t ++ f_ts) v)) (nodes_ltree t')" by (metis (mono_tags, lifting) inj_on_cong f_t') have ts'_in_dom_f_ts: "\v\nodes_ltree (LNode r' ts'). v \ dom f_ts" using f_ts ts' dom_postorder_relabel_aux by (metis snd_conv) then have f_ts': "\v\nodes_ltree (LNode r' ts'). the ((f_t ++ f_ts) v) = the (f_ts v)" by (simp add: map_add_dom_app_simps(1)) have "inj_on (\v. the (f_ts v)) (nodes_ltree (LNode r' ts'))" using 2 ts' f_ts f_t disjoint_family_on_ts by simp then have inj_on_ts': "inj_on (\v. the ((f_t ++ f_ts) v)) (nodes_ltree (LNode r' ts'))" using f_ts' inj_on_cong by fast have "(\v. the ((f_t ++ f_ts) v)) ` nodes_ltree t' \ (\v. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts') = {}" proof- have "(\v. the ((f_t ++ f_ts) v)) ` nodes_ltree t' = (\v. the (f_t v)) ` nodes_ltree t'" using f_t' by simp also have "\ \ ran f_t" using t'_in_dom_f_t ran_def by fastforce also have "\ = nodes_ltree t" by (metis f_t ran_postorder_relabel_aux snd_conv) finally have f_nodes_t': "(\v. the ((f_t ++ f_ts) v)) ` nodes_ltree t' \ nodes_ltree t" . have "(\v. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts') = (\v. the (f_ts v)) ` nodes_ltree (LNode r' ts')" using f_ts' by (simp del: nodes_ltree.simps) also have "\ \ ran f_ts" using ts'_in_dom_f_ts ran_def by fastforce also have "\ = nodes_ltree (LNode r ts)" by (metis f_ts ran_postorder_relabel_aux snd_conv) finally have f_nodes_ts': "(\v. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts') \ nodes_ltree (LNode r ts)" . have "nodes_ltree t \ nodes_ltree (LNode r ts) = {}" using 2(3) by (auto simp add: disjoint_family_on_def) then show ?thesis using f_nodes_t' f_nodes_ts' by blast qed then have "inj_on (\v. the ((f_t ++ f_ts) v)) (nodes_ltree t' \ nodes_ltree (LNode r' ts'))" using inj_on_t' inj_on_ts' inj_on_Un by fast then show ?case using f_t t' f_ts ts' by simp qed lemma relabel_postorder_inj: "distinct_ltree_nodes t \ inj_on (the o postorder_relabel t) (nodes_ltree (postorder_label (tree_ltree t)))" unfolding postorder_relabel_def postorder_label_def using relabel_postorder_aux_inj by blast lemma (in rtree) distinct_nodes_stree_of_graph: "distinct_stree_nodes (stree_of_graph (V,E,r))" using rtree_axioms proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct) case (1 V\<^sub>T E\<^sub>T r) then interpret t: rtree V\<^sub>T E\<^sub>T r by simp obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def) interpret subg: subgraph V' E' V\<^sub>T E\<^sub>T using t.subgraph_remove_vertex VE' by metis interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast then have fset_Abs_fset_subtrees[simp]: "fset (Abs_fset (stree_of_graph ` t.subtrees)) = stree_of_graph ` t.subtrees" by (simp add: Abs_fset_inverse) have r_notin_subtrees: "\s\t.subtrees. r \ nodes_stree (stree_of_graph s)" proof fix s assume subtree: "s \ t.subtrees" then obtain S E\<^sub>S r\<^sub>S where s: "s = (S,E\<^sub>S,r\<^sub>S)" using prod.exhaust by metis then interpret s: rtree S E\<^sub>S r\<^sub>S using t.rtree_subtree subtree by blast have "S \ g'.connected_components" using subtree VE' unfolding s t.subtrees_def by auto then have "nodes_stree (stree_of_graph (S,E\<^sub>S,r\<^sub>S)) \ V'" using s.nodes_stree_stree_of_graph g'.connected_component_wf by auto then show "r \ nodes_stree (stree_of_graph s)" using VE' unfolding s t.remove_vertex_def by blast qed have "nodes_stree (stree_of_graph s1) \ nodes_stree (stree_of_graph s2) = {}" if s1_subtree: "s1 \ t.subtrees" and s2_subtree: "s2 \ t.subtrees" and ne: "stree_of_graph s1 \ stree_of_graph s2" for s1 s2 proof- obtain V1 E1 r1 where s1: "s1 = (V1,E1,r1)" using prod.exhaust by metis then interpret s1: rtree V1 E1 r1 using t.rtree_subtree s1_subtree by blast have V1_conn_comp: "V1 \ g'.connected_components" using s1_subtree VE' unfolding t.subtrees_def s1 by auto then have s1_conn_comp: "nodes_stree (stree_of_graph s1) \ g'.connected_components" unfolding s1 using s1.nodes_stree_stree_of_graph by auto obtain V2 E2 r2 where s2: "s2 = (V2,E2,r2)" using prod.exhaust by metis then interpret s2: rtree V2 E2 r2 using t.rtree_subtree s2_subtree by blast have V2_conn_comp: "V2 \ g'.connected_components" using s2_subtree VE' unfolding t.subtrees_def s2 by auto have "V1 \ V2" using s1 s2 s1_subtree s2_subtree VE' ne unfolding t.subtrees_def by auto then have "V1 \ V2 = {}" using V1_conn_comp V2_conn_comp g'.disjoint_connected_components unfolding disjoint_def by blast then show ?thesis using s1 s2 s1.nodes_stree_stree_of_graph s2.nodes_stree_stree_of_graph by simp qed then have "disjoint_family_on nodes_stree (stree_of_graph ` t.subtrees)" unfolding disjoint_family_on_def by blast then show ?case using 1 t.rtree_subtree r_notin_subtrees by auto qed lemma disintct_nodes_ltree_stree: "distinct_stree_nodes t \ distinct_ltree_nodes (ltree_stree t)" using distinct_ltree_stree_subtrees by (induction t) (auto simp: disjoint_family_on_def, metis disjoint_iff) lemma (in rtree) tree_graph_tree_of_graph: "tree_graph (tree_ltree (ltree_stree (stree_of_graph (V,E,r)))) \\<^sub>r (V,E,r)" proof- define t where "t = (V,E,r)" define s where "s = stree_of_graph t" define l where "l = ltree_stree s" define l' where "l' = postorder_label (tree_ltree l)" define s' where "s' = stree_ltree l'" define t' where "t' = tree_graph_stree s'" obtain V' E' r' where t': "t' = (V',E',r')" using prod.exhaust by metis interpret t': rtree V' E' r' using t' rtree_tree_graph unfolding tree_graph_def t'_def s'_def l'_def by simp have "distinct_ltree_nodes l" using distinct_nodes_stree_of_graph disintct_nodes_ltree_stree unfolding l_def s_def t_def by blast then obtain f where inj_on_l': "inj_on f (nodes_ltree l')" and relabel_l': "relabel_ltree f l' = l" unfolding l'_def using relabel_postorder_relabel relabel_postorder_inj by blast then have "relabel_stree f s' = s" unfolding l_def s'_def using relabel_stree_relabel_ltree by fastforce then have app_rgraph_iso: "app_rgraph_isomorphism f t' = t" unfolding s_def t'_def t_def using t' tree_graph_stree_of_graph by (simp add: app_rgraph_iso_tree_graph_stree) have "inj_on f (nodes_stree s')" unfolding s'_def using inj_on_l' by simp then have inj_on_V': "inj_on f V'" using t' nodes_tree_graph_stree unfolding t'_def by fast have "(V',E',r') \\<^sub>r (V,E,r)" using app_rgraph_iso t'.rgraph_isomorph_app_iso inj_on_V' unfolding t' t_def by auto then show ?thesis using t' unfolding tree_graph_def t_def s_def l_def l'_def s'_def t'_def by auto qed lemma (in rtree) stree_size_stree_of_graph[simp]: "stree_size (stree_of_graph (V,E,r)) = card V" using distinct_nodes_stree_of_graph by (simp add: distinct_nodes_stree_size_card_nodes del: stree_of_graph.simps) lemma inj_ltree_stree: "inj ltree_stree" proof fix t1 :: "'a stree" and t2 :: "'a stree" assume "ltree_stree t1 = ltree_stree t2" then show "t1 = t2" proof (induction t1 arbitrary: t2) case (SNode r1 ts1) obtain r2 ts2 where t2: "t2 = SNode r2 ts2" using stree.exhaust by blast then show ?case using SNode by (simp, metis SNode.prems stree.inject stree_ltree_stree) qed qed lemma ltree_size_ltree_stree[simp]: "ltree_size (ltree_stree t) = stree_size t" using inj_ltree_stree by (induction t) (auto simp: sum_list_distinct_conv_sum_set[OF distinct_ltree_stree_subtrees] fsum.F.rep_eq, smt (verit, best) inj_on_def stree_ltree_stree sum.reindex_cong) lemma tree_size_tree_ltree[simp]: "tree_size (tree_ltree t) = ltree_size t" by (induction t) (auto, metis comp_eq_dest_lhs map_cong) lemma regular_ltree_stree: "regular_ltree (ltree_stree t)" using sorted_wrt_ltree_stree_subtrees by (induction t) auto lemma regular_tree_ltree: "regular_ltree t \ regular (tree_ltree t)" by (induction t) (auto simp: sorted_map) lemma (in rtree) tree_of_graph_regular_n_tree: "tree_ltree (ltree_stree (stree_of_graph (V,E,r))) \ regular_n_trees (card V)" (is "?t \ ?A") proof- have size_t: "tree_size ?t = card V" by (simp del: stree_of_graph.simps) have "regular ?t" using regular_ltree_stree regular_tree_ltree by blast then show ?thesis using size_t unfolding regular_n_trees_def by blast qed lemma (in rtree) ex_regular_n_tree: "\t\regular_n_trees (card V). tree_graph t \\<^sub>r (V,E,r)" using tree_graph_tree_of_graph tree_of_graph_regular_n_tree by blast subsection "Injectivity with respect to isomorphism" lemma app_rgraph_isomorphism_relabel_stree: "app_rgraph_isomorphism f (tree_graph_stree t) = tree_graph_stree (relabel_stree f t)" unfolding tree_graph_stree_def by simp text \Lemmas relating the connected components of the tree graph with the root removed to the subtrees of an stree.\ context fixes t r ts V' E' assumes t: "t = SNode r ts" assumes distinct_nodes: "distinct_stree_nodes t" and remove_vertex: "graph_system.remove_vertex (nodes_stree t) (tree_graph_edges t) r = (V',E')" begin interpretation t: rtree "nodes_stree t" "tree_graph_edges t" r using rtree_tree_graph_edges[OF distinct_nodes] unfolding t by simp interpretation subg: ulsubgraph V' E' "nodes_stree t" "tree_graph_edges t" using remove_vertex t.subgraph_remove_vertex t.ulgraph_axioms ulsubgraph_def t by blast interpretation g': ulgraph V' E' using subg.is_subgraph_ulgraph t.ulgraph_axioms by blast lemma neighborhood_root: "t.neighborhood r = root_stree ` fset ts" unfolding t.neighborhood_def t.vert_adj_def using distinct_nodes tree_graph_edges_wf root_stree_wf t by (auto, blast, fastforce, blast, blast) lemma V': "V' = nodes_stree t - {r}" using remove_vertex distinct_nodes unfolding t.remove_vertex_def by blast lemma E': "E' = \ (tree_graph_edges ` fset ts)" - using tree_graph_edges_wf distinct_nodes remove_vertex t unfolding t.remove_vertex_def t.incident_def by auto + using tree_graph_edges_wf distinct_nodes remove_vertex t unfolding t.remove_vertex_def t.vincident_def by auto lemma subtrees_not_connected: assumes s_in_ts: "s \ fset ts" and e: "{u, v} \ E'" and u_in_s: "u \ nodes_stree s" shows "v \ nodes_stree s" proof- have "{u,v} \ tree_graph_edges s" using e u_in_s tree_graph_edges_wf s_in_ts distinct_nodes t unfolding E' by (auto simp: disjoint_family_on_def, smt (verit, del_insts) insert_absorb insert_disjoint(2) insert_subset tree_graph_edges_wf) then show ?thesis using tree_graph_edges_wf u_in_s by blast qed lemma subtree_connected_components: assumes s_in_ts: "s \ fset ts" shows "nodes_stree s \ g'.connected_components" proof- interpret s: rtree "nodes_stree s" "tree_graph_edges s" "root_stree s" using rtree_tree_graph_edges distinct_nodes s_in_ts t by auto interpret subg': ulsubgraph "nodes_stree s" "tree_graph_edges s" V' E' using distinct_nodes s_in_ts t by unfold_locales (auto simp: V' E') have conn_set: "g'.is_connected_set (nodes_stree s)" using s.connected subg'.is_connected_set by blast then show ?thesis using subtrees_not_connected s_in_ts g'.connected_set_connected_component nodes_stree_non_empty by fast qed lemma connected_components_subtrees: "g'.connected_components = nodes_stree ` fset ts" proof- have nodes_ts_ss_conn_comps: "nodes_stree ` fset ts \ g'.connected_components" using subtree_connected_components by blast have Un_nodes_ts: "\(nodes_stree ` fset ts) = V'" unfolding V' using distinct_nodes t by auto show ?thesis using g'.subset_conn_comps_if_Union[OF nodes_ts_ss_conn_comps Un_nodes_ts] by simp qed lemma induced_edges_subtree: assumes s_in_ts: "s \ fset ts" shows "graph_system.induced_edges E' (nodes_stree s) = tree_graph_edges s" proof- have "graph_system.induced_edges E' (nodes_stree s) = {e \ \ (tree_graph_edges ` fset ts). e \ nodes_stree s}" using subg.H.induced_edges_def E' by auto also have "\ = tree_graph_edges s" using s_in_ts distinct_nodes tree_graph_edges_wf t by (auto simp: disjoint_family_on_def, metis card.empty card_tree_graph_edges_distinct inf.bounded_iff nat.simps(3) numeral_2_eq_2 subset_empty) finally show ?thesis . qed lemma root_subtree: assumes s_in_ts: "s \ fset ts" shows "(THE r'. r' \ (nodes_stree s) \ t.vert_adj r r') = root_stree s" proof show "root_stree s \ nodes_stree s \ t.vert_adj r (root_stree s)" unfolding t.vert_adj_def using t root_stree_wf s_in_ts by auto next fix r' assume r': "r' \ nodes_stree s \ t.vert_adj r r'" then have edge_in_root_edges: "{r, r'} \ (\t. {r, root_stree t}) ` fset ts" unfolding t.vert_adj_def using distinct_nodes tree_graph_edges_wf t by fastforce have "\s'\fset ts. s' \ s \ r' \ nodes_stree s'" using distinct_nodes s_in_ts r' unfolding t by (auto simp: disjoint_family_on_def) then show "r' = root_stree s" using edge_in_root_edges root_stree_wf by (smt (verit) doubleton_eq_iff image_iff) qed lemma subtrees_tree_subtrees: "t.subtrees = tree_graph_stree ` fset ts" unfolding t.subtrees_def tree_graph_stree_def using remove_vertex by (simp add: connected_components_subtrees image_comp induced_edges_subtree root_subtree) end lemma stree_of_graph_tree_graph_stree[simp]: "distinct_stree_nodes t \ stree_of_graph (tree_graph_stree t) = t" proof (induction t) case (SNode r ts) define t where t: "t = SNode r ts" then have root_t[simp]: "root_stree t = r" by simp have distinct_t: "distinct_stree_nodes t" using SNode(2) t by blast interpret t: rtree "nodes_stree t" "tree_graph_edges t" r using SNode(2) rtree_tree_graph_edges t by (metis root_stree.simps) obtain V' E' where remove_vertex: "t.remove_vertex r = (V',E')" by fastforce have "stree_of_graph (tree_graph_stree t) = SNode r ts" unfolding tree_graph_stree_def using SNode t.rtree_axioms t.rtree_subtree by (simp add: subtrees_tree_subtrees[OF t distinct_t remove_vertex] image_comp fset_inverse) then show ?case unfolding t . qed lemma distinct_nodes_relabel: "distinct_stree_nodes t \ inj_on f (nodes_stree t) \ distinct_stree_nodes (relabel_stree f t)" by (induction t) (auto simp: image_UN disjoint_family_on_def inj_on_def, metis IntI empty_iff) lemma relabel_stree_app_rgraph_isomorphism: assumes "distinct_stree_nodes t" and "inj_on f (nodes_stree t)" shows "relabel_stree f t = stree_of_graph (app_rgraph_isomorphism f (tree_graph_stree t))" using assms by (auto simp: app_rgraph_isomorphism_relabel_stree distinct_nodes_relabel) lemma (in rgraph_isomorphism) app_rgraph_isomorphism_G: "app_rgraph_isomorphism f (V\<^sub>G,E\<^sub>G,r\<^sub>G) = (V\<^sub>H,E\<^sub>H,r\<^sub>H)" using bij_f edge_preserving root_preserving unfolding bij_betw_def by simp lemma tree_graphs_iso_strees_iso: assumes "tree_graph_stree t1 \\<^sub>r tree_graph_stree t2" and distinct_t1: "distinct_stree_nodes t1" and distinct_t2: "distinct_stree_nodes t2" shows "\f. inj_on f (nodes_stree t1) \ relabel_stree f t1 = t2" proof- obtain f where "rgraph_isomorphism (nodes_stree t1) (tree_graph_edges t1) (root_stree t1) (nodes_stree t2) (tree_graph_edges t2) (root_stree t2) f" using assms unfolding tree_graph_stree_def by auto then interpret rgraph_isomorphism "nodes_stree t1" "tree_graph_edges t1" "root_stree t1" "nodes_stree t2" "tree_graph_edges t2" "root_stree t2" f . have inj: "inj_on f (nodes_stree t1)" using bij_f bij_betw_imp_inj_on by blast have "relabel_stree f t1 = t2" unfolding relabel_stree_app_rgraph_isomorphism[OF distinct_t1 inj] tree_graph_stree_def app_rgraph_isomorphism_G using stree_of_graph_tree_graph_stree[OF distinct_t2, unfolded tree_graph_stree_def] by blast then show ?thesis using inj by blast qed text \Skip the ltree representation as it introduces complications with the proofs\ fun tree_stree :: "'a stree \ tree" where "tree_stree (SNode r ts) = Node (sorted_list_of_multiset (image_mset tree_stree (mset_set (fset ts))))" fun postorder_label_stree_aux :: "nat \ tree \ nat \ nat stree" where "postorder_label_stree_aux n (Node []) = (n, SNode n {||})" | "postorder_label_stree_aux n (Node (t#ts)) = (let (n', t') = postorder_label_stree_aux n t in case postorder_label_stree_aux (Suc n') (Node ts) of (n'', SNode r ts') \ (n'', SNode r (finsert t' ts')))" definition postorder_label_stree :: "tree \ nat stree" where "postorder_label_stree t = snd (postorder_label_stree_aux 0 t)" lemma fst_postorder_label_stree_aux_eq: "fst (postorder_label_stree_aux n t) = fst (postorder_label_aux n t)" by (induction n t rule: postorder_label_stree_aux.induct) (auto split: prod.split stree.split ltree.split) lemma postorder_label_stree_aux_eq: "snd (postorder_label_stree_aux n t) = stree_ltree (snd (postorder_label_aux n t))" by (induction n t rule: postorder_label_aux.induct) (simp, simp split: prod.split stree.split ltree.split, metis fset_of_list_map fst_conv fst_postorder_label_stree_aux_eq sndI stree.inject stree_ltree.simps) lemma postorder_label_stree_eq: "postorder_label_stree t = stree_ltree (postorder_label t)" using postorder_label_stree_aux_eq unfolding postorder_label_stree_def postorder_label_def by blast lemma postorder_label_stree_aux_mono: "fst (postorder_label_stree_aux n t) \ n" by (induction n t rule: postorder_label_stree_aux.induct) (auto split: prod.split stree.split, fastforce) lemma nodes_postorder_label_stree_aux_ge: "postorder_label_stree_aux n t = (n', t') \ v \ nodes_stree t' \ v \ n" by (induction n t arbitrary: n' t' rule: postorder_label_stree_aux.induct, auto split: prod.splits stree.splits, (metis fst_conv le_SucI order.trans postorder_label_stree_aux_mono)+) lemma nodes_postorder_label_stree_aux_le: "postorder_label_stree_aux n t = (n', t') \ v \ nodes_stree t' \ v \ n'" by (induction n t arbitrary: n' t' rule: postorder_label_stree_aux.induct, auto split: prod.splits stree.splits, metis Suc_leD fst_conv order_trans postorder_label_stree_aux_mono, blast) lemma distinct_nodes_postorder_label_stree_aux: "distinct_stree_nodes (snd (postorder_label_stree_aux n t))" proof (induction n t rule: postorder_label_stree_aux.induct) case (1 n) then show ?case by (simp add: disjoint_family_on_def) next case (2 n t ts) obtain n' t' where t': "postorder_label_stree_aux n t = (n', t')" by fastforce obtain n'' r ts' where ts': "postorder_label_stree_aux (Suc n') (Node ts) = (n'', SNode r ts')" by (metis eq_snd_iff stree.exhaust) then have "r \ Suc n'" using nodes_postorder_label_stree_aux_ge by auto then have r_notin_t': "r \ nodes_stree t'" using nodes_postorder_label_stree_aux_le[OF t'] by fastforce have "disjoint_family_on nodes_stree (insert t' (fset ts'))" using 2 t' ts' nodes_postorder_label_stree_aux_le[OF t'] nodes_postorder_label_stree_aux_ge[OF ts'] by (auto simp add: disjoint_family_on_def, fastforce+) then show ?case using 2 t' ts' r_notin_t' by simp qed lemma distinct_nodes_postorder_label_stree: "distinct_stree_nodes (postorder_label_stree t)" unfolding postorder_label_stree_def using distinct_nodes_postorder_label_stree_aux by simp lemma tree_stree_postorder_label_stree_aux: "regular t \ tree_stree (snd (postorder_label_stree_aux n t)) = t" proof (induction t rule: postorder_label_stree_aux.induct) case (1 n) then show ?case by auto next case (2 n t ts) obtain n' t' where nt': "postorder_label_stree_aux n t = (n', t')" by fastforce obtain n'' r ts' where nt'': "postorder_label_stree_aux (Suc n') (Node ts) = (n'', SNode r ts')" using stree.exhaust prod.exhaust by metis have "t' \ fset ts'" using nodes_postorder_label_stree_aux_le[OF nt'] nodes_postorder_label_stree_aux_ge[OF nt''] by (auto, meson not_less_eq_eq root_stree_wf) then show ?case using 2 nt' nt'' by (auto simp: insort_is_Cons) qed lemma tree_ltree_postorder_label_stree[simp]: "regular t \ tree_stree (postorder_label_stree t) = t" using tree_stree_postorder_label_stree_aux unfolding postorder_label_stree_def by blast lemma inj_relabel_subtrees: assumes distinct_nodes: "distinct_stree_nodes (SNode r ts)" and inj_on_nodes: "inj_on f (nodes_stree (SNode r ts))" shows "inj_on (relabel_stree f) (fset ts)" proof fix t1 t2 assume t1_subtree: "t1 \ fset ts" and t2_subtree: "t2 \ fset ts" and relabel_eq: "relabel_stree f t1 = relabel_stree f t2" then have "nodes_stree (relabel_stree f t1) = nodes_stree (relabel_stree f t2)" by simp then have "f ` nodes_stree t1 = f ` nodes_stree t2" by simp then have "nodes_stree t1 = nodes_stree t2" using inj_on_nodes t1_subtree t2_subtree inj_on_image[of f "nodes_stree ` fset ts"] by (simp, meson image_eqI inj_onD) then show "t1 = t2" using distinct_nodes nodes_stree_non_empty t1_subtree t2_subtree by (auto simp add: disjoint_family_on_def, force) qed lemma inj_on_subtree: "inj_on f (nodes_stree (SNode r ts)) \ t \ fset ts \ inj_on f (nodes_stree t)" unfolding inj_on_def by simp lemma tree_stree_relabel_stree: "distinct_stree_nodes t \ inj_on f (nodes_stree t) \ tree_stree (relabel_stree f t) = tree_stree t" proof (induction t) case (SNode r ts) then have IH: "\t\# mset_set (fset ts). tree_stree (relabel_stree f t) = tree_stree t" using inj_on_subtree[OF SNode(3)] elem_mset_set finite_fset by auto show ?case using inj_relabel_subtrees[OF SNode(2) SNode(3)] by (auto simp add: mset_set_image_inj, metis IH image_mset_cong) qed lemma tree_ltree_relabel_ltree_postorder_label_stree: "regular t \ inj_on f (nodes_stree (postorder_label_stree t)) \ tree_stree (relabel_stree f (postorder_label_stree t)) = t" using tree_stree_relabel_stree distinct_nodes_postorder_label_stree by fastforce lemma postorder_label_stree_inj: "regular t1 \ regular t2 \ inj_on f (nodes_stree (postorder_label_stree t1)) \ relabel_stree f (postorder_label_stree t1) = postorder_label_stree t2 \ t1 = t2" using tree_ltree_relabel_ltree_postorder_label_stree by fastforce lemma tree_graph_inj_iso: "regular t1 \ regular t2 \ tree_graph t1 \\<^sub>r tree_graph t2 \ t1 = t2" using postorder_label_stree_inj tree_graphs_iso_strees_iso distinct_nodes_postorder_label distinct_nodes_stree_ltree postorder_label_stree_eq unfolding tree_graph_def by metis lemma tree_graph_inj: assumes regular_t1: "regular t1" and regular_t2: "regular t2" and tree_graph_eq: "tree_graph t1 = tree_graph t2" shows "t1 = t2" proof- obtain V E r where g: "tree_graph t1 = (V,E,r)" using prod.exhaust by metis then interpret rtree V E r using rtree_tree_graph by auto have "tree_graph t1 \\<^sub>r tree_graph t2" using tree_graph_eq g rgraph_isomorph_refl by simp then show ?thesis using tree_graph_inj_iso regular_t1 regular_t2 by simp qed end \ No newline at end of file diff --git a/thys/Tree_Enumeration/Tree_Graph.thy b/thys/Tree_Enumeration/Tree_Graph.thy --- a/thys/Tree_Enumeration/Tree_Graph.thy +++ b/thys/Tree_Enumeration/Tree_Graph.thy @@ -1,1131 +1,1131 @@ section \Graphs and Trees\ theory Tree_Graph imports Undirected_Graph_Theory.Undirected_Graphs_Root begin subsection \Miscellaneous\ definition (in ulgraph) loops :: "'a edge set" where "loops = {e\E. is_loop e}" definition (in ulgraph) sedges :: "'a edge set" where "sedges = {e\E. is_sedge e}" lemma (in ulgraph) union_loops_sedges: "loops \ sedges = E" unfolding loops_def sedges_def is_loop_def is_sedge_def using alt_edge_size by blast lemma (in ulgraph) disjnt_loops_sedges: "disjnt loops sedges" unfolding disjnt_def loops_def sedges_def is_loop_def is_sedge_def by auto lemma (in fin_ulgraph) finite_loops: "finite loops" unfolding loops_def using fin_edges by auto lemma (in fin_ulgraph) finite_sedges: "finite sedges" unfolding sedges_def using fin_edges by auto -lemma (in ulgraph) edge_incident_vert: "e \ E \ \v\V. incident v e" - using edge_size wellformed by (metis empty_not_edge equals0I incident_def incident_edge_in_wf) +lemma (in ulgraph) edge_incident_vert: "e \ E \ \v\V. vincident v e" + using edge_size wellformed by (metis empty_not_edge equals0I vincident_def incident_edge_in_wf) lemma (in ulgraph) Union_incident_edges: "(\v\V. incident_edges v) = E" unfolding incident_edges_def using edge_incident_vert by auto lemma (in ulgraph) induced_edges_mono: "V\<^sub>1 \ V\<^sub>2 \ induced_edges V\<^sub>1 \ induced_edges V\<^sub>2" using induced_edges_def by auto definition (in graph_system) remove_vertex :: "'a \ 'a pregraph" where - "remove_vertex v = (V - {v}, {e\E. \ incident v e})" + "remove_vertex v = (V - {v}, {e\E. \ vincident v e})" lemma (in ulgraph) ex_neighbor_degree_not_0: assumes degree_non_0: "degree v \ 0" shows "\u\V. vert_adj v u" proof- have "\e\E. v \ e" using degree_non_0 elem_exists_non_empty_set - unfolding degree_def incident_sedges_def incident_loops_def incident_def by auto + unfolding degree_def incident_sedges_def incident_loops_def vincident_def by auto then show ?thesis by (metis degree_non_0 in_mono is_isolated_vertex_def is_isolated_vertex_degree0 vert_adj_sym wellformed) qed lemma (in ulgraph) ex1_neighbor_degree_1: assumes degree_1: "degree v = 1" shows "\!u. vert_adj v u" proof- have "card (incident_loops v) = 0" using degree_1 unfolding degree_def by auto then have incident_loops: "incident_loops v = {}" by (simp add: finite_incident_loops) then have card_incident_sedges: "card (incident_sedges v) = 1" using degree_1 unfolding degree_def by simp obtain u where vert_adj: "vert_adj v u" using degree_1 ex_neighbor_degree_not_0 by force then have "u \ v" using incident_loops unfolding incident_loops_def vert_adj_def by blast - then have u_incident: "{v,u} \ incident_sedges v" using vert_adj unfolding incident_sedges_def vert_adj_def incident_def by simp + then have u_incident: "{v,u} \ incident_sedges v" using vert_adj unfolding incident_sedges_def vert_adj_def vincident_def by simp then have incident_sedges: "incident_sedges v = {{v,u}}" using card_incident_sedges - by (simp add: comp_sgraph.card1_incident_imp_vert comp_sgraph.incident_def) + by (simp add: comp_sgraph.card1_incident_imp_vert comp_sgraph.vincident_def) have "vert_adj v u' \ u' = u" for u' proof- assume v_u'_adj: "vert_adj v u'" then have "u' \ v" using incident_loops unfolding incident_loops_def vert_adj_def by blast - then have "{v,u'} \ incident_sedges v" using v_u'_adj unfolding incident_sedges_def vert_adj_def incident_def by simp + then have "{v,u'} \ incident_sedges v" using v_u'_adj unfolding incident_sedges_def vert_adj_def vincident_def by simp then show "u' = u" using incident_sedges by force qed then show ?thesis using vert_adj by blast qed lemma (in ulgraph) degree_1_edge_partition: assumes degree_1: "degree v = 1" shows "E = {{THE u. vert_adj v u, v}} \ {e \ E. v \ e}" proof- have "card (incident_loops v) = 0" using degree_1 unfolding degree_def by auto then have incident_loops: "incident_loops v = {}" by (simp add: finite_incident_loops) then have "card (incident_sedges v) = 1" using degree_1 unfolding degree_def by simp then have card_incident_edges: "card (incident_edges v) = 1" using incident_loops incident_edges_union by simp obtain u where vert_adj: "vert_adj v u" using ex1_neighbor_degree_1 degree_1 by blast then have "{v, u} \ {e \ E. v \ e}" unfolding vert_adj_def by blast then have edges_incident_v: "{e \ E. v \ e} = {{v, u}}" using card_incident_edges card_1_singletonE singletonD - unfolding incident_edges_def incident_def by metis + unfolding incident_edges_def vincident_def by metis have u: "u = (THE u. vert_adj v u)" using vert_adj ex1_neighbor_degree_1 degree_1 by (simp add: the1_equality) show ?thesis using edges_incident_v u by blast qed lemma (in sgraph) vert_adj_not_eq: "vert_adj u v \ u \ v" unfolding vert_adj_def using edge_vertices_not_equal by blast subsection \Degree\ lemma (in ulgraph) empty_E_degree_0: "E = {} \ degree v = 0" using incident_edges_empty degree0_inc_edges_empt_iff unfolding incident_edges_def by simp lemma (in fin_ulgraph) handshaking: "(\v\V. degree v) = 2 * card E" using fin_edges fin_ulgraph_axioms proof (induction E) case empty then interpret g: fin_ulgraph V "{}" . show ?case using g.empty_E_degree_0 by simp next case (insert e E') then interpret g': fin_ulgraph V "insert e E'" by blast interpret g: fin_ulgraph V E' using g'.wellformed g'.edge_size finV by (unfold_locales, auto) show ?case proof (cases "is_loop e") case True then obtain u where e: "e = {u}" using card_1_singletonE is_loop_def by blast then have inc_sedges: "\v. g'.incident_sedges v = g.incident_sedges v" unfolding g'.incident_sedges_def g.incident_sedges_def by auto have "\v. v \ u \ g'.incident_loops v = g.incident_loops v" unfolding g'.incident_loops_def g.incident_loops_def using e by auto then have degree_not_u: "\v. v \ u \ g'.degree v = g.degree v" using inc_sedges unfolding g'.degree_def g.degree_def by auto have "g'.incident_loops u = g.incident_loops u \ {e}" unfolding g'.incident_loops_def g.incident_loops_def using e by auto then have degree_u: "g'.degree u = g.degree u + 2" using inc_sedges insert(2) g.finite_incident_loops g.incident_loops_def unfolding g'.degree_def g.degree_def by auto have "u \ V" using e g'.wellformed by blast then have "(\v\V. g'.degree v) = g'.degree u + (\v\V-{u}. g'.degree v)" by (simp add: finV sum.remove) also have "\ = (\v\V. g.degree v) + 2" using degree_not_u degree_u sum.remove[OF finV \u\V\, of g.degree] by auto also have "\ = 2 * card (insert e E')" using insert g.fin_ulgraph_axioms by auto finally show ?thesis . next case False obtain u w where e: "e = {u,w}" using g'.obtain_edge_pair_adj by fastforce then have card_e: "card e = 2" using False g'.alt_edge_size is_loop_def by auto then have "u \ w" using card_2_iff using e by fastforce have inc_loops: "\v. g'.incident_loops v = g.incident_loops v" unfolding g'.incident_loops_alt g.incident_loops_alt using False is_loop_def by auto have "\v. v \ u \ v \ w \ g'.incident_sedges v = g.incident_sedges v" - unfolding g'.incident_sedges_def g.incident_sedges_def g.incident_def using e by auto + unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e by auto then have degree_not_u_w: "\v. v \ u \ v \ w \ g'.degree v = g.degree v" unfolding g'.degree_def g.degree_def using inc_loops by auto have "g'.incident_sedges u = g.incident_sedges u \ {e}" - unfolding g'.incident_sedges_def g.incident_sedges_def g.incident_def using e card_e by auto + unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e card_e by auto then have degree_u: "g'.degree u = g.degree u + 1" using inc_loops insert(2) g.fin_edges g.finite_inc_sedges g.incident_sedges_def unfolding g'.degree_def g.degree_def by auto have "g'.incident_sedges w = g.incident_sedges w \ {e}" - unfolding g'.incident_sedges_def g.incident_sedges_def g.incident_def using e card_e by auto + unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e card_e by auto then have degree_w: "g'.degree w = g.degree w + 1" using inc_loops insert(2) g.fin_edges g.finite_inc_sedges g.incident_sedges_def unfolding g'.degree_def g.degree_def by auto have inV: "u \ V" "w \ V-{u}" using e g'.wellformed \u\w\ by auto then have "(\v\V. g'.degree v) = g'.degree u + g'.degree w + (\v\V-{u}-{w}. g'.degree v)" using sum.remove finV by (metis add.assoc finite_Diff) also have "\ = g.degree u + g.degree w + (\v\V-{u}-{w}. g.degree v) + 2" using degree_not_u_w degree_u degree_w by simp also have "\ = (\v\V. g.degree v) + 2" using sum.remove finV inV by (metis add.assoc finite_Diff) also have "\ = 2 * card (insert e E')" using insert g.fin_ulgraph_axioms by auto finally show ?thesis . qed qed lemma (in fin_ulgraph) degree_remove_adj_ne_vert: assumes "u \ v" and vert_adj: "vert_adj u v" and remove_vertex: "remove_vertex u = (V',E')" shows "ulgraph.degree E' v = degree v - 1" proof- - interpret G': fin_ulgraph V' E' using remove_vertex wellformed edge_size finV unfolding remove_vertex_def incident_def + interpret G': fin_ulgraph V' E' using remove_vertex wellformed edge_size finV unfolding remove_vertex_def vincident_def by (unfold_locales, auto) - have E': "E' = {e \ E. u \ e}" using remove_vertex unfolding remove_vertex_def incident_def by simp + have E': "E' = {e \ E. u \ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp have incident_loops': "G'.incident_loops v = incident_loops v" unfolding incident_loops_def using \u\v\ E' G'.incident_loops_def by auto - have uv_incident: "{u,v} \ incident_sedges v" using vert_adj \u\v\ unfolding vert_adj_def incident_sedges_def incident_def by simp - have uv_incident': "{u, v} \ G'.incident_sedges v" unfolding G'.incident_sedges_def incident_def using E' by blast + have uv_incident: "{u,v} \ incident_sedges v" using vert_adj \u\v\ unfolding vert_adj_def incident_sedges_def vincident_def by simp + have uv_incident': "{u, v} \ G'.incident_sedges v" unfolding G'.incident_sedges_def vincident_def using E' by blast have "e \ E \ u \ e \ v \ e \ card e = 2 \ e = {u,v}" for e using \u\v\ obtain_edge_pair_adj by blast then have "{e \ E. u \ e \ v \ e \ card e = 2} = {{u,v}}" using uv_incident unfolding incident_sedges_def by blast - then have "incident_sedges v = G'.incident_sedges v \ {{u,v}}" unfolding G'.incident_sedges_def incident_sedges_def incident_def using E' by blast + then have "incident_sedges v = G'.incident_sedges v \ {{u,v}}" unfolding G'.incident_sedges_def incident_sedges_def vincident_def using E' by blast then show ?thesis unfolding G'.degree_def degree_def using incident_loops' uv_incident' G'.finite_inc_sedges G'.fin_edges by auto qed lemma (in ulgraph) degree_remove_non_adj_vert: assumes "u \ v" and vert_non_adj: "\ vert_adj u v" and remove_vertex: "remove_vertex u = (V', E')" shows "ulgraph.degree E' v = degree v" proof- - interpret G': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def incident_def + interpret G': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def vincident_def by (unfold_locales, auto) - have E': "E' = {e \ E. u \ e}" using remove_vertex unfolding remove_vertex_def incident_def by simp + have E': "E' = {e \ E. u \ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp have incident_loops': "G'.incident_loops v = incident_loops v" unfolding incident_loops_def using \u\v\ E' G'.incident_loops_def by auto - have "G'.incident_sedges v = incident_sedges v" unfolding G'.incident_sedges_def incident_sedges_def incident_def - using E' \u\v\ incident_def vert_adj_edge_iff2 vert_non_adj by auto + have "G'.incident_sedges v = incident_sedges v" unfolding G'.incident_sedges_def incident_sedges_def vincident_def + using E' \u\v\ vincident_def vert_adj_edge_iff2 vert_non_adj by auto then show ?thesis using incident_loops' unfolding G'.degree_def degree_def by simp qed subsection \Walks\ lemma (in ulgraph) walk_edges_induced_edges: "is_walk p \ set (walk_edges p) \ induced_edges (set p)" unfolding induced_edges_def is_walk_def by (induction p rule: walk_edges.induct) auto lemma (in ulgraph) walk_edges_in_verts: "e \ set (walk_edges xs) \ e \ set xs" by (induction xs rule: walk_edges.induct) auto lemma (in ulgraph) is_walk_prefix: "is_walk (xs@ys) \ xs \ [] \ is_walk xs" unfolding is_walk_def using walk_edges_append_ss2 by fastforce lemma (in ulgraph) split_walk_edge: "{x,y} \ set (walk_edges p) \ \xs ys. p = xs @ x # y # ys \ p = xs @ y # x # ys" by (induction p rule: walk_edges.induct) (auto, metis append_Nil doubleton_eq_iff, (metis append_Cons)+) subsection \Paths\ lemma (in ulgraph) is_gen_path_wf: "is_gen_path p \ set p \ V" unfolding is_gen_path_def using is_walk_wf by auto lemma (in ulgraph) path_wf: "is_path p \ set p \ V" by (simp add: is_path_walk is_walk_wf) lemma (in fin_ulgraph) length_gen_path_card_V: "is_gen_path p \ walk_length p \ card V" by (metis card_mono distinct_card distinct_tl finV is_gen_path_def is_walk_def length_tl list.exhaust_sel order_trans set_subset_Cons walk_length_conv) lemma (in fin_ulgraph) length_path_card_V: "is_path p \ length p \ card V" by (metis path_wf card_mono distinct_card finV is_path_def) lemma (in ulgraph) is_gen_path_prefix: "is_gen_path (xs@ys) \ xs \ [] \ is_gen_path (xs)" unfolding is_gen_path_def using is_walk_prefix by (auto, metis Int_iff distinct.simps(2) emptyE last_appendL last_appendR last_in_set list.collapse) lemma (in ulgraph) connecting_path_append: "connecting_path u w (xs@ys) \ xs \ [] \ connecting_path u (last xs) xs" unfolding connecting_path_def using is_gen_path_prefix by auto lemma (in ulgraph) connecting_path_tl: "connecting_path u v (u # w # xs) \ connecting_path w v (w # xs)" unfolding connecting_path_def is_gen_path_def using is_walk_drop_hd distinct_tl by auto lemma (in fin_ulgraph) obtain_longest_path: assumes "e \ E" and sedge: "is_sedge e" obtains p where "is_path p" "\s. is_path s \ length s \ length p" proof- let ?longest_path = "ARG_MAX length p. is_path p" obtain u v where e: "u \ v" "e = {u,v}" using sedge card_2_iff unfolding is_sedge_def by metis then have inV: "u \ V" "v \ V" using \e\E\ wellformed by auto then have path_ex: "is_path [u,v]" using e \e\E\ unfolding is_path_def is_open_walk_def is_walk_def by simp obtain p where p_is_path: "is_path p" and p_longest_path: "\s. is_path s \ length s \ length p" - using path_ex length_path_card_V ex_has_greatest_nat[of is_path "[u,v]" length order] by force + using path_ex length_path_card_V ex_has_greatest_nat[of is_path "[u,v]" length gorder] by force then show ?thesis .. qed subsection \Cycles\ context ulgraph begin definition is_cycle2 :: "'a list \ bool" where "is_cycle2 xs \ is_cycle xs \ distinct (walk_edges xs)" lemma loop_is_cycle2: "{v} \ E \ is_cycle2 [v, v]" unfolding is_cycle2_def is_cycle_alt is_walk_def using wellformed walk_length_conv by auto end lemma (in sgraph) cycle2_min_length: assumes cycle: "is_cycle2 c" shows "walk_length c \ 3" proof- consider "c = []" | "\v1. c = [v1]" | "\v1 v2. c = [v1, v2]" | "\v1 v2 v3. c = [v1, v2, v3]" | "\v1 v2 v3 v4 vs. c = v1#v2#v3#v4#vs" by (metis list.exhaust_sel) then show ?thesis using cycle walk_length_conv singleton_not_edge unfolding is_cycle2_def is_cycle_alt is_walk_def by (cases, auto) qed lemma (in fin_ulgraph) length_cycle_card_V: "is_cycle c \ walk_length c \ Suc (card V)" using length_gen_path_card_V unfolding is_gen_path_def is_cycle_alt by fastforce lemma (in ulgraph) is_cycle_connecting_path: "is_cycle (u#v#xs) \ connecting_path v u (v#xs)" unfolding is_cycle_def connecting_path_def is_closed_walk_def is_gen_path_def using is_walk_drop_hd by auto lemma (in ulgraph) cycle_edges_notin_tl: "is_cycle2 (u#v#xs) \ {u,v} \ set (walk_edges (v#xs))" unfolding is_cycle2_def by simp subsection \Subgraphs\ locale ulsubgraph = subgraph V\<^sub>H E\<^sub>H V\<^sub>G E\<^sub>G + G: ulgraph V\<^sub>G E\<^sub>G for V\<^sub>H E\<^sub>H V\<^sub>G E\<^sub>G begin interpretation H: ulgraph V\<^sub>H E\<^sub>H using is_subgraph_ulgraph G.ulgraph_axioms by auto lemma is_walk: "H.is_walk xs \ G.is_walk xs" unfolding H.is_walk_def G.is_walk_def using verts_ss edges_ss by blast lemma is_closed_walk: "H.is_closed_walk xs \ G.is_closed_walk xs" unfolding H.is_closed_walk_def G.is_closed_walk_def using is_walk by blast lemma is_gen_path: "H.is_gen_path p \ G.is_gen_path p" unfolding H.is_gen_path_def G.is_gen_path_def using is_walk by blast lemma connecting_path: "H.connecting_path u v p \ G.connecting_path u v p" unfolding H.connecting_path_def G.connecting_path_def using is_gen_path by blast lemma is_cycle: "H.is_cycle c \ G.is_cycle c" unfolding H.is_cycle_def G.is_cycle_def using is_closed_walk by blast lemma is_cycle2: "H.is_cycle2 c \ G.is_cycle2 c" unfolding H.is_cycle2_def G.is_cycle2_def using is_cycle by blast lemma vert_connected: "H.vert_connected u v \ G.vert_connected u v" unfolding H.vert_connected_def G.vert_connected_def using connecting_path by blast lemma is_connected_set: "H.is_connected_set V' \ G.is_connected_set V'" unfolding H.is_connected_set_def G.is_connected_set_def using vert_connected by blast end lemma (in graph_system) subgraph_remove_vertex: "remove_vertex v = (V', E') \ subgraph V' E' V E" - using wellformed unfolding remove_vertex_def incident_def by (unfold_locales, auto) + using wellformed unfolding remove_vertex_def vincident_def by (unfold_locales, auto) subsection \Connectivity\ lemma (in ulgraph) connecting_path_connected_set: assumes conn_path: "connecting_path u v p" shows "is_connected_set (set p)" proof- have "\w\set p. vert_connected u w" proof fix w assume "w \ set p" then obtain xs ys where "p = xs@[w]@ys" using split_list by fastforce then have "connecting_path u w (xs@[w])" using conn_path unfolding connecting_path_def using is_gen_path_prefix by (auto simp: hd_append) then show "vert_connected u w" unfolding vert_connected_def by blast qed then show ?thesis using vert_connected_rev vert_connected_trans unfolding is_connected_set_def by blast qed lemma (in ulgraph) vert_connected_neighbors: assumes "{v,u} \ E" shows "vert_connected v u" proof- have "connecting_path v u [v,u]" unfolding connecting_path_def is_gen_path_def is_walk_def using assms wellformed by auto then show ?thesis unfolding vert_connected_def by auto qed lemma (in ulgraph) connected_empty_E: assumes empty: "E = {}" and connected: "vert_connected u v" shows "u = v" proof (rule ccontr) assume "u \ v" then obtain p where conn_path: "connecting_path u v p" using connected unfolding vert_connected_def by blast then obtain e where "e \ set (walk_edges p)" using \u\v\ connecting_path_length_bound unfolding walk_length_def by fastforce then have "e \ E" using conn_path unfolding connecting_path_def is_gen_path_def is_walk_def by blast then show False using empty by blast qed lemma (in fin_ulgraph) degree_0_not_connected: assumes degree_0: "degree v = 0" and "u \ v" shows "\ vert_connected v u" proof assume connected: "vert_connected v u" then obtain p where conn_path: "connecting_path v u p" unfolding vert_connected_def by blast then have "walk_length p \ 1" using \u\v\ connecting_path_length_bound by metis then have "length p \ 2" using walk_length_conv by simp then obtain w p' where "p = v#w#p'" using walk_length_conv conn_path unfolding connecting_path_def by (metis assms(2) is_gen_path_def is_walk_not_empty2 last_ConsL list.collapse) then have inE: "{v,w} \ E" using conn_path unfolding connecting_path_def is_gen_path_def is_walk_def by simp - then have "{v,w} \ incident_edges v" unfolding incident_edges_def incident_def by simp + then have "{v,w} \ incident_edges v" unfolding incident_edges_def vincident_def by simp then show False using degree0_inc_edges_empt_iff fin_edges degree_0 by blast qed lemma (in fin_connected_ulgraph) degree_not_0: assumes "card V \ 2" and inV: "v \ V" shows "degree v \ 0" proof- obtain u where "u \ V" and "u \ v" using assms by (metis card_eq_0_iff card_le_Suc0_iff_eq less_eq_Suc_le nat_less_le not_less_eq_eq numeral_2_eq_2) then show ?thesis using degree_0_not_connected inV vertices_connected by blast qed lemma (in connected_ulgraph) V_E_empty: "E = {} \ \v. V = {v}" using connected_empty_E connected not_empty unfolding is_connected_set_def by (metis ex_in_conv insert_iff mk_disjoint_insert) lemma (in connected_ulgraph) vert_connected_remove_edge: assumes e: "{u,v} \ E" shows "\w\V. ulgraph.vert_connected V (E - {{u,v}}) w u \ ulgraph.vert_connected V (E - {{u,v}}) w v" proof fix w assume "w\V" interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto) have inV: "u \ V" "v \ V" using e wellformed by auto obtain p where conn_path: "connecting_path w v p" using connected inV \w\V\ unfolding is_connected_set_def vert_connected_def by blast then show "g'.vert_connected w u \ g'.vert_connected w v" proof (cases "{u,v} \ set (walk_edges p)") case True assume walk_edge: "{u,v} \ set (walk_edges p)" then show ?thesis proof (cases "w = v") case True then show ?thesis using inV g'.vert_connected_id by blast next case False then have distinct: "distinct p" using conn_path by (simp add: connecting_path_def is_gen_path_distinct) have "u \ set p" using walk_edge walk_edges_in_verts by blast obtain xs ys where p_split: "p = xs @ u # v # ys \ p = xs @ v # u # ys" using split_walk_edge[OF walk_edge] by blast have v_notin_ys: "v \ set ys" using distinct p_split by auto have "last p = v" using conn_path unfolding connecting_path_def by simp then have p: "p = (xs@[u]) @ [v]" using v_notin_ys p_split last_in_set last_appendR by (metis append.assoc append_Cons last.simps list.discI self_append_conv2) then have conn_path_u: "connecting_path w u (xs@[u])" using connecting_path_append conn_path by fastforce have "v \ set (xs@[u])" using p distinct by auto then have "{u,v} \ set (walk_edges (xs@[u]))" using walk_edges_in_verts by blast then have "g'.connecting_path w u (xs@[u])" using conn_path_u unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast then show ?thesis unfolding g'.vert_connected_def by blast qed next case False then have "g'.connecting_path w v p" using conn_path unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast then show ?thesis unfolding g'.vert_connected_def by blast qed qed lemma (in ulgraph) vert_connected_remove_cycle_edge: assumes cycle: "is_cycle2 (u#v#xs)" shows "ulgraph.vert_connected V (E - {{u,v}}) u v" proof- interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto) have conn_path: "connecting_path v u (v#xs)" using cycle is_cycle_connecting_path unfolding is_cycle2_def by blast have "{u,v} \ set (walk_edges (v#xs))" using cycle unfolding is_cycle2_def by simp then have "g'.connecting_path v u (v#xs)" using conn_path unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast then show ?thesis using g'.vert_connected_rev unfolding g'.vert_connected_def by blast qed lemma (in connected_ulgraph) connected_remove_cycle_edges: assumes cycle: "is_cycle2 (u#v#xs)" shows "connected_ulgraph V (E - {{u,v}})" proof- interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto) have "g'.vert_connected x y" if inV: "x \ V" "y \ V" for x y proof- have e: "{u,v} \ E" using cycle unfolding is_cycle2_def is_cycle_alt is_walk_def by auto show ?thesis using vert_connected_remove_cycle_edge[OF cycle] vert_connected_remove_edge[OF e] g'.vert_connected_trans g'.vert_connected_rev inV by metis qed then show ?thesis using not_empty by (unfold_locales, auto simp: g'.is_connected_set_def) qed lemma (in connected_ulgraph) connected_remove_leaf: assumes degree: "degree l = 1" and remove_vertex: "remove_vertex l = (V', E')" shows "ulgraph.is_connected_set V' E' V'" proof- interpret g': ulgraph V' E' using remove_vertex wellformed edge_size - unfolding remove_vertex_def incident_def by (unfold_locales, auto) + unfolding remove_vertex_def vincident_def by (unfold_locales, auto) have V': "V' = V - {l}" using remove_vertex unfolding remove_vertex_def by simp - have E': "E' = {e\E. l \ e}" using remove_vertex unfolding remove_vertex_def incident_def by simp + have E': "E' = {e\E. l \ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp have "u \ V' \ v \ V' \ g'.vert_connected u v" for u v proof- assume inV': "u \ V'" "v \ V'" then have inV: "u \ V" "v \ V" using remove_vertex unfolding remove_vertex_def by auto then obtain p where conn_path: "connecting_path u v p" using vertices_connected_path by blast show ?thesis proof (cases "u = v") case True then show ?thesis using g'.vert_connected_id inV' by simp next case False then have distinct: "distinct p" using conn_path unfolding connecting_path_def is_gen_path_def by blast have l_notin_p: "l \ set p" proof assume l_in_p: "l \ set p" then obtain xs ys where p: "p = xs @ l # ys" by (meson split_list) have "l \ u" "l \ v" using inV' remove_vertex unfolding remove_vertex_def by auto then have "xs \ []" using p conn_path unfolding connecting_path_def by fastforce then obtain x where last_xs: "last xs = x" by simp then have "x \ l" using distinct p \xs\[]\ by auto have "{x,l} \ set (walk_edges p)" using walk_edges_append_union \xs\[]\ unfolding p by (simp add: walk_edges_append_union last_xs) then have xl_incident: "{x,l} \ incident_sedges l" using conn_path \x\l\ - unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def incident_def by auto + unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def vincident_def by auto have "ys \ []" using \l\v\ p conn_path unfolding connecting_path_def by fastforce then obtain y ys' where ys: "ys = y # ys'" by (meson list.exhaust) then have "y \ l" using distinct p by auto then have "{y,l} \ set (walk_edges p)" using p ys conn_path walk_edges_append_ss1 by fastforce then have yl_incident: "{y,l} \ incident_sedges l" using conn_path \y\l\ - unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def incident_def by auto + unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def vincident_def by auto have card_loops: "card (incident_loops l) = 0" using degree unfolding degree_def by auto have "x \ y" using distinct last_xs \xs\[]\ unfolding p ys by fastforce then have "{x,l} \ {y,l}" by (metis doubleton_eq_iff) then have "card (incident_sedges l) \ 1" using xl_incident yl_incident by (metis card_1_singletonE singletonD) then have "degree l \ 1" using card_loops unfolding degree_def by simp then show False using degree .. qed then have "set (walk_edges p) \ E'" using walk_edges_in_verts conn_path E' unfolding connecting_path_def is_gen_path_def is_walk_def by blast then have "g'.connecting_path u v p" using conn_path V' l_notin_p unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast then show ?thesis unfolding g'.vert_connected_def by blast qed qed then show ?thesis unfolding g'.is_connected_set_def by blast qed lemma (in connected_sgraph) connected_two_graph_edges: assumes "u \ v" and V: "V = {u,v}" shows "E = {{u,v}}" proof- obtain p where conn_path: "connecting_path u v p" using V vertices_connected_path by blast then obtain p' where p: "p = u # p' @ [v]" using \u\v\ unfolding connecting_path_def is_gen_path_def by (metis append_Nil is_walk_not_empty2 list.exhaust_sel list.sel(1) snoc_eq_iff_butlast tl_append2) have "distinct p" using conn_path \u\v\ unfolding connecting_path_def is_gen_path_def by auto then have "p' = []" using V conn_path is_gen_path_wf append_is_Nil_conv last_in_set self_append_conv2 unfolding connecting_path_def p by fastforce then have edge_in_E: "{u,v} \ E" using \u\v\ conn_path unfolding p connecting_path_def is_gen_path_def is_walk_def by simp have "E \ {{}, {u}, {v}, {u,v}}" using wellformed V by blast then show ?thesis using two_edges edge_in_E by fastforce qed subsection "Connected components" context ulgraph begin abbreviation "vert_connected_rel \ {(u,v). vert_connected u v}" definition connected_components :: "'a set set" where "connected_components = V // vert_connected_rel" definition connected_component_of :: "'a \ 'a set" where "connected_component_of v = vert_connected_rel `` {v}" lemma vert_connected_rel_on_V: "vert_connected_rel \ V \ V" using vert_connected_wf by auto lemma vert_connected_rel_refl: "refl_on V vert_connected_rel" unfolding refl_on_def using vert_connected_rel_on_V vert_connected_id by simp lemma vert_connected_rel_sym: "sym vert_connected_rel" unfolding sym_def using vert_connected_rev by simp lemma vert_connected_rel_trans: "trans vert_connected_rel" unfolding trans_def using vert_connected_trans by blast lemma equiv_vert_connected: "equiv V vert_connected_rel" unfolding equiv_def using vert_connected_rel_refl vert_connected_rel_sym vert_connected_rel_trans by blast lemma connected_component_non_empty: "V' \ connected_components \ V' \ {}" unfolding connected_components_def using equiv_vert_connected in_quotient_imp_non_empty by auto lemma connected_component_connected: "V' \ connected_components \ is_connected_set V'" unfolding connected_components_def is_connected_set_def using quotient_eq_iff[OF equiv_vert_connected, of V' V'] by simp lemma connected_component_wf: "V' \ connected_components \ V' \ V" by (simp add: connected_component_connected is_connected_set_wf) lemma connected_component_of_self: "v \ V \ v \ connected_component_of v" unfolding connected_component_of_def using vert_connected_id by blast lemma conn_comp_of_conn_comps: "v \ V \ connected_component_of v \ connected_components" unfolding connected_components_def quotient_def connected_component_of_def by blast lemma Un_connected_components: "connected_components = connected_component_of ` V" unfolding connected_components_def connected_component_of_def quotient_def by blast lemma connected_component_subgraph: "V' \ connected_components \ subgraph V' (induced_edges V') V E" using induced_is_subgraph connected_component_wf by simp lemma connected_components_connected2: assumes conn_comp: "V' \ connected_components" shows "ulgraph.is_connected_set V' (induced_edges V') V'" proof- interpret subg: subgraph V' "induced_edges V'" V E using connected_component_subgraph conn_comp by simp interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by simp have "\u v. u \ V' \ v \ V' \ g'.vert_connected u v" proof- fix u v assume "u \ V'" "v \ V'" then obtain p where conn_path: "connecting_path u v p" using connected_component_connected conn_comp unfolding is_connected_set_def vert_connected_def by blast then have u_in_p: "u \ set p" unfolding connecting_path_def is_gen_path_def is_walk_def by force then have set_p: "set p \ V'" using connecting_path_connected_set[OF conn_path] in_quotient_imp_closed[OF equiv_vert_connected] conn_comp \u \ V'\ unfolding is_connected_set_def connected_components_def by blast then have "set (g'.walk_edges p) \ induced_edges V'" using walk_edges_induced_edges induced_edges_mono conn_path unfolding connecting_path_def is_gen_path_def by blast then have "g'.connecting_path u v p" using set_p conn_path unfolding g'.connecting_path_def g'.connecting_path_def g'.is_gen_path_def g'.is_walk_def unfolding connecting_path_def connecting_path_def is_gen_path_def is_walk_def by auto then show "g'.vert_connected u v" unfolding g'.vert_connected_def by blast qed then show ?thesis unfolding g'.is_connected_set_def by blast qed lemma vert_connected_connected_component: "C \ connected_components \ u \ C \ vert_connected u v \ v \ C" unfolding connected_components_def using equiv_vert_connected in_quotient_imp_closed by fastforce lemma connected_components_connected_ulgraphs: assumes conn_comp: "V' \ connected_components" shows "connected_ulgraph V' (induced_edges V')" proof- interpret subg: subgraph V' "induced_edges V'" V E using connected_component_subgraph conn_comp by simp interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by simp show ?thesis using conn_comp connected_component_non_empty connected_components_connected2 by (unfold_locales, auto) qed lemma connected_components_partition_on_V: "partition_on V connected_components" using partition_on_quotient equiv_vert_connected unfolding connected_components_def by blast lemma Union_connected_components: "\connected_components = V" using connected_components_partition_on_V unfolding partition_on_def by blast lemma disjoint_connected_components: "disjoint connected_components" using connected_components_partition_on_V unfolding partition_on_def by blast lemma Union_induced_edges_connected_components: "\(induced_edges ` connected_components) = E" proof- have "\C\connected_components. e \ induced_edges C" if "e \ E" for e proof- obtain u v where e: "e = {u,v}" by (meson \e \ E\ obtain_edge_pair_adj) then have "vert_connected u v" using that vert_connected_neighbors by blast then have "v \ connected_component_of u" unfolding connected_component_of_def by simp then have "e \ induced_edges (connected_component_of u)" using connected_component_of_self wellformed \e\E\ unfolding e induced_edges_def by auto then show ?thesis using conn_comp_of_conn_comps e wellformed \e\E\ by auto qed then show ?thesis using connected_component_wf induced_edges_ss by blast qed lemma connected_components_empty_E: assumes empty: "E = {}" shows "connected_components = {{v} | v. v\V}" proof- have "\v\V. vert_connected_rel``{v} = {v}" using vert_connected_id connected_empty_E empty by auto then show ?thesis unfolding connected_components_def quotient_def by auto qed lemma connected_iff_connected_components: assumes non_empty: "V \ {}" shows "is_connected_set V \ connected_components = {V}" proof assume "is_connected_set V" then have "\v\V. connected_component_of v = V" unfolding connected_component_of_def is_connected_set_def using vert_connected_wf by blast then show "connected_components = {V}" unfolding quotient_def connected_component_of_def connected_components_def using non_empty by auto next show "connected_components = {V} \ is_connected_set V" using connected_component_connected unfolding connected_components_def is_connected_set_def by auto qed end lemma (in connected_ulgraph) connected_components[simp]: "connected_components = {V}" using connected connected_iff_connected_components not_empty by simp lemma (in fin_ulgraph) finite_connected_components: "finite connected_components" unfolding connected_components_def using finV vert_connected_rel_on_V finite_quotient by blast lemma (in fin_ulgraph) finite_connected_component: "C \ connected_components \ finite C" using connected_component_wf finV finite_subset by blast lemma (in connected_ulgraph) connected_components_remove_edges: assumes edge: "{u,v} \ E" shows "ulgraph.connected_components V (E - {{u,v}}) = {ulgraph.connected_component_of V (E - {{u,v}}) u, ulgraph.connected_component_of V (E - {{u,v}}) v}" proof- interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto) have inV: "u \ V" "v \ V" using edge wellformed by auto have "\w\V. g'.connected_component_of w = g'.connected_component_of u \ g'.connected_component_of w = g'.connected_component_of v" using vert_connected_remove_edge[OF edge] g'.equiv_vert_connected equiv_class_eq unfolding g'.connected_component_of_def by fast then show ?thesis unfolding g'.connected_components_def quotient_def g'.connected_component_of_def using inV by auto qed lemma (in ulgraph) connected_set_connected_component: assumes conn_set: "is_connected_set C" and non_empty: "C \ {}" and "\u v. {u,v} \ E \ u \ C \ v \ C" shows "C \ connected_components" proof- have walk_subset_C: "is_walk xs \ hd xs \ C \ set xs \ C" for xs proof (induction xs rule: rev_induct) case Nil then show ?case by auto next case (snoc x xs) then show ?case proof (cases xs rule: rev_exhaust) case Nil then show ?thesis using snoc by auto next fix ys y assume xs: "xs = ys @ [y]" then have "is_walk xs" using is_walk_prefix snoc(2) by blast then have set_xs_C: "set xs \ C" using snoc xs is_walk_not_empty2 hd_append2 by metis have yx_E: "{y,x} \ E" using snoc(2) walk_edges_app unfolding xs is_walk_def by simp have "x \ C" using assms(3)[OF yx_E] set_xs_C unfolding xs by simp then show ?thesis using set_xs_C by simp qed qed obtain u where "u \ C" using non_empty by blast then have "u \ V" using conn_set is_connected_set_wf by blast have "v \ C" if vert_connected: "vert_connected u v" for v proof- obtain p where "connecting_path u v p" using vert_connected unfolding vert_connected_def by blast then show ?thesis using walk_subset_C[of p] \u\C\ is_walk_def last_in_set unfolding connecting_path_def is_gen_path_def by auto qed then have "connected_component_of u = C" using assms \u\C\ unfolding connected_component_of_def is_connected_set_def by auto then show ?thesis using conn_comp_of_conn_comps \u\V\ by blast qed lemma (in ulgraph) subset_conn_comps_if_Union: assumes A_subset_conn_comps: "A \ connected_components" and Un_A: "\A = V" shows "A = connected_components" proof (rule ccontr) assume "A \ connected_components" then obtain C where C_conn_comp: "C \ connected_components " "C \ A" using A_subset_conn_comps by blast then obtain v where "v \ C" using connected_component_non_empty by blast then have "v \ V" using A_subset_conn_comps Un_A connected_components_partition_on_V C_conn_comp using partition_onD4 by fastforce then show False using C_conn_comp connected_component_wf \v\C\ by auto qed lemma (in connected_ulgraph) exists_adj_vert_removed: assumes "v \ V" and remove_vertex: "remove_vertex v = (V',E')" and conn_component: "C \ ulgraph.connected_components V' E'" shows "\u\C. vert_adj v u" proof- - have V': "V' = V - {v}" and E': "E' = {e\E. v \ e}" using remove_vertex unfolding remove_vertex_def incident_def by auto + have V': "V' = V - {v}" and E': "E' = {e\E. v \ e}" using remove_vertex unfolding remove_vertex_def vincident_def by auto interpret subg: subgraph "V - {v}" "{e\E. v \ e}" V E using subgraph_remove_vertex remove_vertex V' E' by metis interpret g': ulgraph "V - {v}" "{e\E. v \ e}" using subg.is_subgraph_ulgraph ulgraph_axioms by blast obtain c where "c \ C" using g'.connected_component_non_empty conn_component V' E' by blast then have "c \ V'" using g'.connected_component_wf conn_component V' E' by blast then have "c \ V" using subg.verts_ss V' by blast then obtain p where conn_path: "connecting_path v c p" using \v\V\ vertices_connected_path by blast have "v \ c" using \c\V'\ remove_vertex unfolding remove_vertex_def by blast then obtain u p' where p: "p = v # u # p'" using conn_path by (metis connecting_path_def is_gen_path_def is_walk_def last.simps list.exhaust_sel) then have conn_path_uc: "connecting_path u c (u#p')" using conn_path connecting_path_tl unfolding p by blast have v_notin_p': "v \ set (u#p')" using conn_path \v\c\ unfolding p connecting_path_def is_gen_path_def by auto then have "g'.connecting_path u c (u#p')" using conn_path_uc v_notin_p' walk_edges_in_verts unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast then have "g'.vert_connected u c" unfolding g'.vert_connected_def by blast then have "u \ C" using \c\C\ conn_component g'.vert_connected_connected_component g'.vert_connected_rev unfolding V' E' by blast have "vert_adj v u" using conn_path unfolding p connecting_path_def is_gen_path_def is_walk_def vert_adj_def by auto then show ?thesis using \u\C\ by blast qed subsection \Trees\ locale tree = fin_connected_ulgraph + assumes no_cycles: "\ is_cycle2 c" begin sublocale fin_connected_sgraph using alt_edge_size no_cycles loop_is_cycle2 card_1_singletonE connected by (unfold_locales, metis, simp) end locale spanning_tree = ulgraph V E + T: tree V T for V E T + assumes subgraph: "T \ E" lemma (in fin_connected_ulgraph) has_spanning_tree: "\T. spanning_tree V E T" using fin_connected_ulgraph_axioms proof (induction "card E" arbitrary: E) case 0 then interpret g: fin_connected_ulgraph V edges by blast have edges: "edges = {}" using g.fin_edges 0 by simp then obtain v where V: "V = {v}" using g.V_E_empty by blast interpret g': fin_connected_sgraph V edges using g.connected edges by (unfold_locales, auto) interpret t: tree V edges using g.length_cycle_card_V g'.cycle2_min_length g.is_cycle2_def V by (unfold_locales, fastforce) have "spanning_tree V edges edges" by (unfold_locales, auto) then show ?case by blast next case (Suc m) then interpret g: fin_connected_ulgraph V edges by blast show ?case proof (cases "\c. \g.is_cycle2 c") case True then have "spanning_tree V edges edges" by (unfold_locales, auto) then show ?thesis by blast next case False then obtain c where cycle: "g.is_cycle2 c" by blast then have "length c \ 2" unfolding g.is_cycle2_def g.is_cycle_alt walk_length_conv by auto then obtain u v xs where c: "c = u#v#xs" by (metis Suc_le_length_iff numeral_2_eq_2) then have g': "fin_connected_ulgraph V (edges - {{u,v}})" using finV g.connected_remove_cycle_edges by (metis connected_ulgraph_def cycle fin_connected_ulgraph_def fin_graph_system.intro fin_graph_system_axioms.intro fin_ulgraph.intro ulgraph_def) have "{u,v} \ edges" using cycle unfolding c g.is_cycle2_def g.is_cycle_alt g.is_walk_def by auto then obtain T where "spanning_tree V (edges - {{u,v}}) T" using Suc card_Diff_singleton g' by fastforce then have "spanning_tree V edges T" unfolding spanning_tree_def spanning_tree_axioms_def using g.ulgraph_axioms by blast then show ?thesis by blast qed qed context tree begin definition leaf :: "'a \ bool" where "leaf v \ degree v = 1" definition leaves :: "'a set" where "leaves = {v. leaf v}" definition non_trivial :: "bool" where "non_trivial \ card V \ 2" lemma obtain_2_verts: assumes "non_trivial" obtains u v where "u \ V" "v \ V" "u \ v" using assms unfolding non_trivial_def by (meson diameter_obtains_path_vertices) lemma leaf_in_V: "leaf v \ v \ V" unfolding leaf_def using degree_none by force lemma exists_leaf: assumes "non_trivial" shows "\v\V. leaf v" proof- obtain p where is_path: "is_path p" and longest_path: "\s. is_path s \ length s \ length p" using obtain_longest_path by (metis One_nat_def assms connected connected_sgraph_axioms connected_sgraph_def degree_0_not_connected is_connected_setD is_edge_or_loop is_isolated_vertex_def is_isolated_vertex_degree0 is_loop_def n_not_Suc_n numeral_2_eq_2 obtain_2_verts sgraph.two_edges vert_adj_def) then obtain l v xs where p: "p = l#v#xs" by (metis is_open_walk_def is_path_def is_walk_not_empty2 last_ConsL list.exhaust_sel) then have lv_incident: "{l,v} \ incident_edges l" using is_path - unfolding incident_edges_def incident_def is_path_def is_open_walk_def is_walk_def by simp + unfolding incident_edges_def vincident_def is_path_def is_open_walk_def is_walk_def by simp have "\e. e\E \ e \ {l,v} \ e \ incident_edges l" proof fix e assume e_in_E: "e \ E" and not_lv: "e \ {l,v}" and incident: "e \ incident_edges l" obtain u where e: "e = {l,u}" using e_in_E obtain_edge_pair_adj incident - unfolding incident_edges_def incident_def by auto + unfolding incident_edges_def vincident_def by auto then have "u \ l" using e_in_E edge_vertices_not_equal by blast have "u \ v" using e not_lv by auto have u_in_V: "u \ V" using e_in_E e wellformed by blast then show False proof (cases "u \ set p") case True then have "u \ set xs" using \u\l\ \u\v\ p by simp then obtain ys zs where "xs = ys@u#zs" by (meson split_list) then have "is_cycle2 (u#l#v#ys@[u])" using is_path \u\l\ \u\v\ e_in_E distinct_edgesI walk_edges_append_ss2 walk_edges_in_verts unfolding is_cycle2_def is_cycle_def p is_path_def is_closed_walk_def is_open_walk_def is_walk_def e walk_length_conv by (auto, metis insert_commute, fastforce+) then show ?thesis using no_cycles by blast next case False then have "is_path (u#p)" using is_path u_in_V e_in_E unfolding is_path_def is_open_walk_def is_walk_def e p by (auto, (metis insert_commute)+) then show False using longest_path by auto qed qed then have "incident_edges l = {{l,v}}" using lv_incident unfolding incident_edges_def by blast then have leaf: "leaf l" unfolding leaf_def alt_degree_def by simp then show ?thesis using leaf_in_V by blast qed lemma tree_remove_leaf: assumes leaf: "leaf l" and remove_vertex: "remove_vertex l = (V',E')" shows "tree V' E'" proof- - interpret g': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def incident_def + interpret g': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def vincident_def by (unfold_locales, auto) interpret subg: ulsubgraph V' E' V E using subgraph_remove_vertex ulgraph_axioms remove_vertex unfolding ulsubgraph_def by blast have V': "V' = V - {l}" using remove_vertex unfolding remove_vertex_def by blast - have E': "E' = {e\E. l \ e}" using remove_vertex unfolding remove_vertex_def incident_def by blast + have E': "E' = {e\E. l \ e}" using remove_vertex unfolding remove_vertex_def vincident_def by blast have "\v\V. v \ l" using leaf unfolding leaf_def by (metis One_nat_def is_independent_alt is_isolated_vertex_def is_isolated_vertex_degree0 n_not_Suc_n radius_obtains singletonI singleton_independent_set) - then have "V' \ {}" using remove_vertex unfolding remove_vertex_def incident_def by blast + then have "V' \ {}" using remove_vertex unfolding remove_vertex_def vincident_def by blast then have "g'.is_connected_set V'" using connected_remove_leaf leaf remove_vertex unfolding leaf_def by blast then show ?thesis using \V'\{}\ finV subg.is_cycle2 V' E' no_cycles by (unfold_locales, auto) qed end lemma tree_induct [case_names singolton insert, induct set: tree]: assumes tree: "tree V E" and trivial: "\v. tree {v} {} \ P {v} {}" and insert: "\l v V E. tree V E \ P V E \ l \ V \ v \ V \ {l,v} \ E \ tree.leaf (insert {l,v} E) l \ P (insert l V) (insert {l,v} E)" shows "P V E" using tree proof (induction "card V" arbitrary: V E) case 0 then interpret tree V E by simp have "V = {}" using finV 0(1) by simp then show ?case using not_empty by blast next case (Suc n) then interpret t: tree V E by simp show ?case proof (cases "card V = 1") case True then obtain v where V: "V = {v}" using card_1_singletonE by blast then have "E = {}" - using True subset_antisym t.edge_incident_vert t.incident_def t.singleton_not_edge t.wellformed + using True subset_antisym t.edge_incident_vert t.vincident_def t.singleton_not_edge t.wellformed by fastforce then show ?thesis using trivial t.tree_axioms V by simp next case False then have card_V: "card V \ 2" using Suc by simp then obtain l where leaf: "t.leaf l" using t.exists_leaf t.non_trivial_def by blast then obtain e where inc_edges: "t.incident_edges l = {e}" unfolding t.leaf_def t.alt_degree_def using card_1_singletonE by blast then have e_in_E: "e \ E" unfolding t.incident_edges_def by blast - then obtain u where e: "e = {l,u}" using t.two_edges card_2_iff inc_edges unfolding t.incident_edges_def t.incident_def + then obtain u where e: "e = {l,u}" using t.two_edges card_2_iff inc_edges unfolding t.incident_edges_def t.vincident_def by (metis (no_types, lifting) empty_iff insert_commute insert_iff mem_Collect_eq) then have "l \ u" using e_in_E t.edge_vertices_not_equal by blast have "u \ V" using e e_in_E t.wellformed by blast let ?V' = "V - {l}" let ?E' = "E - {{l,u}}" have remove_vertex: "t.remove_vertex l = (?V', ?E')" using inc_edges e unfolding t.remove_vertex_def t.incident_edges_def by blast then have t': "tree ?V' ?E'" using t.tree_remove_leaf leaf by blast have "l \ V" using leaf t.leaf_in_V by blast then have P': "P ?V' ?E'" using Suc t' by auto show ?thesis using insert[OF t' P'] Suc leaf \u\V\ \l\u\ \l \ V\ e e_in_E by (auto, metis insert_Diff) qed qed context tree begin lemma card_V_card_E: "card V = Suc (card E)" using tree_axioms proof (induction V E) case (singolton v) then show ?case by auto next case (insert l v V' E') then interpret t': tree V' E' by simp show ?case using t'.finV t'.fin_edges insert by simp qed end lemma card_E_treeI: assumes fin_conn_sgraph: "fin_connected_ulgraph V E" and card_V_E: "card V = Suc (card E)" shows "tree V E" proof- interpret G: fin_connected_ulgraph V E using fin_conn_sgraph . obtain T where T: "spanning_tree V E T" using G.has_spanning_tree by blast show ?thesis proof (cases "E = T") case True then show ?thesis using T unfolding spanning_tree_def by blast next case False then have "card E > card T" using T G.fin_edges unfolding spanning_tree_def spanning_tree_axioms_def by (simp add: psubsetI psubset_card_mono) then show ?thesis using tree.card_V_card_E T card_V_E unfolding spanning_tree_def by fastforce qed qed context tree begin lemma add_vertex_tree: assumes "v \ V" and "w \ V" shows "tree (insert v V) (insert {v,w} E)" proof - let ?V' = "insert v V" and ?E' = "insert {v,w} E" have cardV: "card {v,w} = 2" using card_2_iff assms by auto then interpret t': ulgraph ?V' ?E' using wellformed assms two_edges by (unfold_locales, auto) interpret subg: ulsubgraph V E ?V' ?E' by (unfold_locales, auto) have connected: "t'.is_connected_set ?V'" unfolding t'.is_connected_set_def using subg.vert_connected t'.vert_connected_neighbors t'.vert_connected_trans t'.vert_connected_id vertices_connected t'.ulgraph_axioms ulgraph_axioms assms t'.vert_connected_rev - by (auto, metis+) + by simp metis then have fin_connected_ulgraph: "fin_connected_ulgraph ?V' ?E'" using finV by (unfold_locales, auto) from assms have "{v,w} \ E" using wellformed_alt_fst by auto then have "card ?E' = Suc (card E)" using fin_edges card_insert_if by auto then have "card ?V' = Suc (card ?E')" using card_V_card_E assms wellformed_alt_fst finV card_insert_if by auto then show ?thesis using card_E_treeI fin_connected_ulgraph by auto qed lemma tree_connected_set: assumes non_empty: "V' \ {}" and subg: "V' \ V" and connected_V': "ulgraph.is_connected_set V' (induced_edges V') V'" shows "tree V' (induced_edges V')" proof- interpret subg: subgraph V' "induced_edges V'" V E using induced_is_subgraph subg by simp interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by blast interpret subg: ulsubgraph V' "induced_edges V'" V E by unfold_locales show ?thesis using connected_V' subg.is_cycle2 no_cycles finV subg non_empty rev_finite_subset by (unfold_locales) (auto, blast) qed lemma unique_adj_vert_removed: assumes "v \ V" and remove_vertex: "remove_vertex v = (V',E')" and conn_component: "C \ ulgraph.connected_components V' E'" shows "\!u\C. vert_adj v u" proof- interpret subg: ulsubgraph V' E' V E using remove_vertex subgraph_remove_vertex ulgraph_axioms ulsubgraph.intro by metis interpret g': ulgraph V' E' using subg.is_subgraph_ulgraph ulgraph_axioms by simp obtain u where "u \ C" and adj_vu: "vert_adj v u" using exists_adj_vert_removed using assms by blast have "w = u" if "w \ C" and adj_vw: "vert_adj v w" for w proof (rule ccontr) assume "w \ u" obtain p where g'_conn_path: "g'.connecting_path w u p" using \u\C\ \w\C\ conn_component g'.connected_component_connected g'.is_connected_setD g'.vert_connected_def by blast then have v_notin_p: "v \ set p" using remove_vertex unfolding g'.connecting_path_def g'.is_gen_path_def g'.is_walk_def remove_vertex_def by blast have conn_path: "connecting_path w u p" using g'_conn_path subg.connecting_path by simp then obtain p' where p: "p = w # p' @ [u]" unfolding connecting_path_def using \w\u\ by (metis hd_Cons_tl last.simps last_rev rev_is_Nil_conv snoc_eq_iff_butlast) then have "walk_edges (v#p@[v]) = {v,w} # walk_edges ((w # p') @ [u,v])" by simp also have "\ = {v,w} # walk_edges p @ [{u,v}]" unfolding p using walk_edges_app by (metis Cons_eq_appendI) finally have walk_edges: "walk_edges (v#p@[v]) = {v,w} # walk_edges p @ [{v,u}]" by (simp add: insert_commute) then have "is_cycle (v#p@[v])" using conn_path adj_vu adj_vw \w\u\ \v\V\ g'.walk_length_conv singleton_not_edge v_notin_p unfolding connecting_path_def is_cycle_def is_gen_path_def is_closed_walk_def is_walk_def p vert_adj_def by auto then have "is_cycle2 (v#p@[v])" using \w\u\ v_notin_p walk_edges_in_verts unfolding is_cycle2_def walk_edges by (auto simp: doubleton_eq_iff is_cycle_alt distinct_edgesI) then show False using no_cycles by blast qed then show ?thesis using \u\C\ adj_vu by blast qed lemma non_trivial_card_E: "non_trivial \ card E \ 1" using card_V_card_E unfolding non_trivial_def by simp lemma V_Union_E: "non_trivial \ V = \E" using tree_axioms proof (induction V E) case (singolton v) then interpret t: tree "{v}" "{}" by simp show ?case using singolton unfolding t.non_trivial_def by simp next case (insert l v V' E') then interpret t: tree V' E' by simp show ?case proof (cases "card V' = 1") case True then have V: "V' = {v}" using insert(3) card_1_singletonE by blast then have E: "E' = {}" using t.fin_edges t.card_V_card_E by fastforce then show ?thesis unfolding E V by simp next case False then have "t.non_trivial" using t.card_V_card_E unfolding t.non_trivial_def by simp then show ?thesis using insert by blast qed qed end lemma singleton_tree: "tree {v} {}" proof- interpret g: fin_ulgraph "{v}" "{}" by (unfold_locales, auto) show ?thesis using g.is_walk_def g.walk_length_def by (unfold_locales, auto simp: g.is_connected_set_singleton g.is_cycle2_def g.is_cycle_alt) qed lemma tree2: assumes "u \ v" shows "tree {u,v} {{u,v}}" proof- interpret ulgraph "{u,v}" "{{u,v}}" using \u\v\ by unfold_locales auto have "fin_connected_ulgraph {u,v} {{u,v}}" by unfold_locales (auto simp: is_connected_set_def vert_connected_id vert_connected_neighbors vert_connected_rev) then show ?thesis using card_E_treeI \u\v\ by fastforce qed subsection \Graph Isomorphism\ locale graph_isomorphism = G: graph_system V\<^sub>G E\<^sub>G for V\<^sub>G E\<^sub>G + fixes V\<^sub>H E\<^sub>H f assumes bij_f: "bij_betw f V\<^sub>G V\<^sub>H" and edge_preserving: "((`) f) ` E\<^sub>G = E\<^sub>H" begin lemma inj_f: "inj_on f V\<^sub>G" using bij_f unfolding bij_betw_def by blast lemma V\<^sub>H_def: "V\<^sub>H = f ` V\<^sub>G" using bij_f unfolding bij_betw_def by blast definition "inv_iso \ the_inv_into V\<^sub>G f" lemma graph_system_H: "graph_system V\<^sub>H E\<^sub>H" using G.wellformed edge_preserving bij_f bij_betw_imp_surj_on by unfold_locales blast interpretation H: graph_system V\<^sub>H E\<^sub>H using graph_system_H . lemma graph_isomorphism_inv: "graph_isomorphism V\<^sub>H E\<^sub>H V\<^sub>G E\<^sub>G inv_iso" proof (unfold_locales) show "bij_betw inv_iso V\<^sub>H V\<^sub>G" unfolding inv_iso_def using bij_betw_the_inv_into bij_f by blast next have "\v\V\<^sub>G. the_inv_into V\<^sub>G f (f v) = v" using bij_f by (simp add: bij_betw_imp_inj_on the_inv_into_f_f) then have "\e\E\<^sub>G. (\v. the_inv_into V\<^sub>G f (f v)) ` e = e" using G.wellformed by (simp add: subset_iff) then show "((`) inv_iso)` E\<^sub>H = E\<^sub>G" unfolding inv_iso_def by (simp add: edge_preserving[symmetric] image_comp) qed interpretation inv_iso: graph_isomorphism V\<^sub>H E\<^sub>H V\<^sub>G E\<^sub>G inv_iso using graph_isomorphism_inv . end fun graph_isomorph :: "'a pregraph \ 'b pregraph \ bool" (infix "\" 50) where "(V\<^sub>G,E\<^sub>G) \ (V\<^sub>H,E\<^sub>H) \ (\f. graph_isomorphism V\<^sub>G E\<^sub>G V\<^sub>H E\<^sub>H f)" lemma (in graph_system) graph_isomorphism_id: "graph_isomorphism V E V E id" by unfold_locales auto lemma (in graph_system) graph_isomorph_refl: "(V,E) \ (V,E)" using graph_isomorphism_id by auto lemma graph_isomorph_sym: "symp (\)" using graph_isomorphism.graph_isomorphism_inv unfolding symp_def by fastforce lemma graph_isomorphism_trans: "graph_isomorphism V\<^sub>G E\<^sub>G V\<^sub>H E\<^sub>H f \ graph_isomorphism V\<^sub>H E\<^sub>H V\<^sub>F E\<^sub>F g \ graph_isomorphism V\<^sub>G E\<^sub>G V\<^sub>F E\<^sub>F (g o f)" unfolding graph_isomorphism_def graph_isomorphism_axioms_def using bij_betw_trans by (auto, blast) lemma graph_isomorph_trans: "transp (\)" using graph_isomorphism_trans unfolding transp_def by fastforce end \ No newline at end of file