# Theory Rtrancl_On

(* Title: Rtrancl_On.thy Author: Lars Noschinski, TU München Author: René Neumann, TU München *) theory Rtrancl_On imports Main begin section ‹Reflexive-Transitive Closure on a Domain› text ‹ In this section we introduce a variant of the reflexive-transitive closure of a relation which is useful to formalize the reachability relation on digraphs. › inductive_set rtrancl_on :: "'a set ⇒ 'a rel ⇒ 'a rel" for F :: "'a set" and r :: "'a rel" where rtrancl_on_refl [intro!, Pure.intro!, simp]: "a ∈ F ⟹ (a, a) ∈ rtrancl_on F r" | rtrancl_on_into_rtrancl_on [Pure.intro]: "(a, b) ∈ rtrancl_on F r ⟹ (b, c) ∈ r ⟹ c ∈ F ⟹ (a, c) ∈ rtrancl_on F r" definition symcl :: "'a rel ⇒ 'a rel" ("(_⇧^{s})" [1000] 999) where "symcl R = R ∪ (λ(a,b). (b,a)) ` R" lemma in_rtrancl_on_in_F: assumes "(a,b) ∈ rtrancl_on F r" shows "a ∈ F" "b ∈ F" using assms by induct auto lemma rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]: assumes "(a, b) ∈ rtrancl_on F r" and "a ∈ F ⟹ P a" "⋀y z. ⟦(a, y) ∈ rtrancl_on F r; (y,z) ∈ r; y ∈ F; z ∈ F; P y⟧ ⟹ P z" shows "P b" using assms by (induct a b) (auto dest: in_rtrancl_on_in_F) lemma rtrancl_on_trans: assumes "(a,b) ∈ rtrancl_on F r" "(b,c) ∈ rtrancl_on F r" shows "(a,c) ∈ rtrancl_on F r" using assms(2,1) by induct (auto intro: rtrancl_on_into_rtrancl_on) lemma converse_rtrancl_on_into_rtrancl_on: assumes "(a,b) ∈ r" "(b, c) ∈ rtrancl_on F r" "a ∈ F" shows "(a, c) ∈ rtrancl_on F r" proof - have "b ∈ F" using ‹(b,c) ∈ _› by (rule in_rtrancl_on_in_F) show ?thesis apply (rule rtrancl_on_trans) apply (rule rtrancl_on_into_rtrancl_on) apply (rule rtrancl_on_refl) by fact+ qed lemma rtrancl_on_converseI: assumes "(y, x) ∈ rtrancl_on F r" shows "(x, y) ∈ rtrancl_on F (r¯)" using assms proof induct case (step a b) then have "(b,b) ∈ rtrancl_on F (r¯)" "(b,a) ∈ r¯" by auto then show ?case using step by (metis rtrancl_on_trans rtrancl_on_into_rtrancl_on) qed auto theorem rtrancl_on_converseD: assumes "(y, x) ∈ rtrancl_on F (r¯)" shows "(x, y) ∈ rtrancl_on F r" using assms by - (drule rtrancl_on_converseI, simp) lemma converse_rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]: assumes major: "(a, b) ∈ rtrancl_on F r" and cases: "b ∈ F ⟹ P b" "⋀x y. ⟦(x,y) ∈ r; (y,b) ∈ rtrancl_on F r; x ∈ F; y ∈ F; P y⟧ ⟹ P x" shows "P a" using rtrancl_on_converseI[OF major] cases by induct (auto intro: rtrancl_on_converseD) lemma converse_rtrancl_on_cases: assumes "(a, b) ∈ rtrancl_on F r" obtains (base) "a = b" "b ∈ F" | (step) c where "(a,c) ∈ r" "(c,b) ∈ rtrancl_on F r" using assms by induct auto lemma rtrancl_on_sym: assumes "sym r" shows "sym (rtrancl_on F r)" using assms by (auto simp: sym_conv_converse_eq intro: symI dest: rtrancl_on_converseI) lemma rtrancl_on_mono: assumes "s ⊆ r" "F ⊆ G" "(a,b) ∈ rtrancl_on F s" shows "(a,b) ∈ rtrancl_on G r" using assms(3,1,2) proof induct case (step x y) show ?case using step assms by (intro converse_rtrancl_on_into_rtrancl_on[OF _ step(5)]) auto qed auto lemma rtrancl_consistent_rtrancl_on: assumes "(a,b) ∈ r⇧^{*}" and "a ∈ F" "b ∈ F" and consistent: "⋀a b. ⟦ a ∈ F; (a,b) ∈ r ⟧ ⟹ b ∈ F" shows "(a,b) ∈ rtrancl_on F r" using assms(1-3) proof (induction rule: converse_rtrancl_induct) case (step y z) then have "z ∈ F" by (rule_tac consistent) simp with step have "(z,b) ∈ rtrancl_on F r" by simp with step.prems ‹(y,z) ∈ r› ‹z ∈ F› show ?case using converse_rtrancl_on_into_rtrancl_on by metis qed simp lemma rtrancl_on_rtranclI: "(a,b) ∈ rtrancl_on F r ⟹ (a,b) ∈ r⇧^{*}" by (induct rule: rtrancl_on_induct) simp_all lemma rtrancl_on_sub_rtrancl: "rtrancl_on F r ⊆ r^*" using rtrancl_on_rtranclI by auto end

# Theory Stuff

(* Title: Stuff.thy Author: Lars Noschinski, TU München *) theory Stuff imports Main "HOL-Library.Extended_Real" begin section ‹Additional theorems for base libraries› text ‹ This section contains lemmas unrelated to graph theory which might be interesting for the Isabelle distribution › lemma ereal_Inf_finite_Min: fixes S :: "ereal set" assumes "finite S" and "S ≠ {}" shows "Inf S = Min S" using assms by (induct S rule: finite_ne_induct) (auto simp: min_absorb1) lemma finite_INF_in: fixes f :: "'a ⇒ ereal" assumes "finite S" assumes "S ≠ {}" shows "(INF s∈ S. f s) ∈ f ` S" proof - from assms have "finite (f ` S)" "f ` S ≠ {}" by auto then show "Inf (f ` S) ∈ f ` S" using ereal_Inf_finite_Min [of "f ` S"] by simp qed lemma not_mem_less_INF: fixes f :: "'a ⇒ 'b :: complete_lattice" assumes "f x < (INF s∈ S. f s)" assumes "x ∈ S" shows "False" using assms by (metis INF_lower less_le_not_le) lemma sym_diff: assumes "sym A" "sym B" shows "sym (A - B)" using assms by (auto simp: sym_def) subsection ‹List› lemmas list_exhaust2 = list.exhaust[case_product list.exhaust] lemma list_exhaust_NSC: obtains (Nil) "xs = []" | (Single) x where "xs = [x]" | (Cons_Cons) x y ys where "xs = x # y # ys" by (metis list.exhaust) lemma tl_rev: "tl (rev p) = rev (butlast p)" by (induct p) auto lemma butlast_rev: "butlast (rev p) = rev (tl p)" by (induct p) auto lemma take_drop_take: "take n xs @ drop n (take m xs) = take (max n m) xs" proof cases assume "m < n" then show ?thesis by (auto simp: max_def) next assume "¬m < n" then have "take n xs = take n (take m xs)" by (auto simp: min_def) then show ?thesis by (simp del: take_take add: max_def) qed lemma drop_take_drop: "drop n (take m xs) @ drop m xs = drop (min n m) xs" proof cases assume A: "¬m < n" then show ?thesis using drop_append[of n "take m xs" "drop m xs"] by (cases "length xs < n") (auto simp: not_less min_def) qed (auto simp: min_def) lemma not_distinct_decomp_min_prefix: assumes "¬ distinct ws" shows "∃ xs ys zs y. ws = xs @ y # ys @ y # zs ∧ distinct xs ∧ y ∉ set xs ∧ y ∉ set ys " proof - obtain xs y ys where "y ∈ set xs" "distinct xs" "ws = xs @ y # ys" using assms by (auto simp: not_distinct_conv_prefix) moreover then obtain xs' ys' where "xs = xs' @ y # ys'" by (auto simp: in_set_conv_decomp) ultimately show ?thesis by auto qed lemma not_distinct_decomp_min_not_distinct: assumes "¬ distinct ws" shows "∃xs y ys zs. ws = xs @ y # ys @ y # zs ∧ distinct (ys @ [y])" using assms proof (induct ws) case (Cons w ws) show ?case proof (cases "distinct ws") case True then obtain xs ys where "ws = xs @ w # ys" "w ∉ set xs" using Cons.prems by (fastforce dest: split_list_first) then have "distinct (xs @ [w])" "w # ws = [] @ w # xs @ w # ys" using ‹distinct ws› by auto then show ?thesis by blast next case False then obtain xs y ys zs where "ws = xs @ y # ys @ y # zs ∧ distinct (ys @ [y])" using Cons by auto then have "w # ws = (w # xs) @ y # ys @ y # zs ∧ distinct (ys @ [y])" by simp then show ?thesis by blast qed qed simp lemma card_Ex_subset: "k ≤ card M ⟹ ∃N. N ⊆ M ∧ card N = k" by (induct rule: inc_induct) (auto simp: card_Suc_eq) lemma list_set_tl: "x ∈ set (tl xs) ⟹ x ∈ set xs" by (cases xs) auto section ‹NOMATCH simproc› text ‹ The simplification procedure can be used to avoid simplification of terms of a certain form › definition NOMATCH :: "'a ⇒ 'a ⇒ bool" where "NOMATCH val pat ≡ True" lemma NOMATCH_cong[cong]: "NOMATCH val pat = NOMATCH val pat" by (rule refl) simproc_setup NOMATCH ("NOMATCH val pat") = ‹fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd) val m = Pattern.matches thy (dest_binop (Thm.term_of ct)) in if m then NONE else SOME @{thm NOMATCH_def} end › text ‹ This setup ensures that a rewrite rule of the form @{term "NOMATCH val pat ⟹ t"} is only applied, if the pattern @{term pat} does not match the value @{term val}. › end

# Theory Digraph

(* Title: Digraph.thy Author: Lars Noschinski, TU München Author: René Neumann *) theory Digraph imports Main Rtrancl_On Stuff begin section ‹Digraphs› record ('a,'b) pre_digraph = verts :: "'a set" arcs :: "'b set" tail :: "'b ⇒ 'a" head :: "'b ⇒ 'a" definition arc_to_ends :: "('a,'b) pre_digraph ⇒ 'b ⇒ 'a × 'a" where "arc_to_ends G e ≡ (tail G e, head G e)" locale pre_digraph = fixes G :: "('a, 'b) pre_digraph" (structure) locale wf_digraph = pre_digraph + assumes tail_in_verts[simp]: "e ∈ arcs G ⟹ tail G e ∈ verts G" assumes head_in_verts[simp]: "e ∈ arcs G ⟹ head G e ∈ verts G" begin lemma wf_digraph: "wf_digraph G" by intro_locales lemmas wellformed = tail_in_verts head_in_verts end definition arcs_ends :: "('a,'b) pre_digraph ⇒ ('a × 'a) set" where "arcs_ends G ≡ arc_to_ends G ` arcs G" definition symmetric :: "('a,'b) pre_digraph ⇒ bool" where "symmetric G ≡ sym (arcs_ends G)" text ‹ Matches "pseudo digraphs" from \cite{bangjensen2009digraphs}, except for allowing the null graph. For a discussion of that topic, see also \cite{harary1974nullgraph}. › locale fin_digraph = wf_digraph + assumes finite_verts[simp]: "finite (verts G)" and finite_arcs[simp]: "finite (arcs G)" locale loopfree_digraph = wf_digraph + assumes no_loops: "e ∈ arcs G ⟹ tail G e ≠ head G e" locale nomulti_digraph = wf_digraph + assumes no_multi_arcs: "⋀e1 e2. ⟦e1 ∈ arcs G; e2 ∈ arcs G; arc_to_ends G e1 = arc_to_ends G e2⟧ ⟹ e1 = e2" locale sym_digraph = wf_digraph + assumes sym_arcs[intro]: "symmetric G" locale digraph = fin_digraph + loopfree_digraph + nomulti_digraph text ‹ We model graphs as symmetric digraphs. This is fine for many purposes, but not for all. For example, the path $a,b,a$ is considered to be a cycle in a digraph (and hence in a symmetric digraph), but not in an undirected graph. › locale pseudo_graph = fin_digraph + sym_digraph locale graph = digraph + pseudo_graph lemma (in wf_digraph) fin_digraphI[intro]: assumes "finite (verts G)" assumes "finite (arcs G)" shows "fin_digraph G" using assms by unfold_locales lemma (in wf_digraph) sym_digraphI[intro]: assumes "symmetric G" shows "sym_digraph G" using assms by unfold_locales lemma (in digraph) graphI[intro]: assumes "symmetric G" shows "graph G" using assms by unfold_locales definition (in wf_digraph) arc :: "'b ⇒ 'a × 'a ⇒ bool" where "arc e uv ≡ e ∈ arcs G ∧ tail G e = fst uv ∧ head G e = snd uv" lemma (in fin_digraph) fin_digraph: "fin_digraph G" by unfold_locales lemma (in nomulti_digraph) nomulti_digraph: "nomulti_digraph G" by unfold_locales lemma arcs_ends_conv: "arcs_ends G = (λe. (tail G e, head G e)) ` arcs G" by (auto simp: arc_to_ends_def arcs_ends_def) lemma symmetric_conv: "symmetric G ⟷ (∀e1 ∈ arcs G. ∃e2 ∈ arcs G. tail G e1 = head G e2 ∧ head G e1 = tail G e2)" unfolding symmetric_def arcs_ends_conv sym_def by auto lemma arcs_ends_symmetric: assumes "symmetric G" shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G" using assms unfolding symmetric_def sym_def by auto lemma (in nomulti_digraph) inj_on_arc_to_ends: "inj_on (arc_to_ends G) (arcs G)" by (rule inj_onI) (rule no_multi_arcs) subsection ‹Reachability› abbreviation dominates :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40) where "dominates G u v ≡ (u,v) ∈ arcs_ends G" abbreviation reachable1 :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧^{+}ı _" [100,100] 40) where "reachable1 G u v ≡ (u,v) ∈ (arcs_ends G)^+" definition reachable :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧^{*}ı _" [100,100] 40) where "reachable G u v ≡ (u,v) ∈ rtrancl_on (verts G) (arcs_ends G)" lemma reachableE[elim]: assumes "u →⇘_{G}⇙ v" obtains e where "e ∈ arcs G" "tail G e = u" "head G e = v" using assms by (auto simp add: arcs_ends_conv) lemma (in loopfree_digraph) adj_not_same: assumes "a → a" shows "False" using assms by (rule reachableE) (auto dest: no_loops) lemma reachable_in_vertsE: assumes "u →⇧^{*}⇘_{G}⇙ v" obtains "u ∈ verts G" "v ∈ verts G" using assms unfolding reachable_def by induct auto lemma symmetric_reachable: assumes "symmetric G" "v →⇧^{*}⇘_{G}⇙ w" shows "w →⇧^{*}⇘_{G}⇙ v" proof - have "sym (rtrancl_on (verts G) (arcs_ends G))" using assms by (auto simp add: symmetric_def dest: rtrancl_on_sym) then show ?thesis using assms unfolding reachable_def by (blast elim: symE) qed lemma reachable_rtranclI: "u →⇧^{*}⇘_{G }⇙ v ⟹ (u, v) ∈ (arcs_ends G)⇧^{*}" unfolding reachable_def by (rule rtrancl_on_rtranclI) context wf_digraph begin lemma adj_in_verts: assumes "u →⇘_{G}⇙ v" shows "u ∈ verts G" "v ∈ verts G" using assms unfolding arcs_ends_conv by auto lemma dominatesI: assumes "arc_to_ends G a = (u,v)" "a ∈ arcs G" shows "u →⇘_{G}⇙ v" using assms by (auto simp: arcs_ends_def intro: rev_image_eqI) lemma reachable_refl [intro!, Pure.intro!, simp]: "v ∈ verts G ⟹ v →⇧^{*}v" unfolding reachable_def by auto lemma adj_reachable_trans[trans]: assumes "a →⇘_{G}⇙ b" "b →⇧^{*}⇘_{G}⇙ c" shows "a →⇧^{*}⇘_{G}⇙ c" using assms by (auto simp: reachable_def intro: converse_rtrancl_on_into_rtrancl_on adj_in_verts) lemma reachable_adj_trans[trans]: assumes "a →⇧^{*}⇘_{G}⇙ b" "b →⇘_{G}⇙ c" shows "a →⇧^{*}⇘_{G}⇙ c" using assms by (auto simp: reachable_def intro: rtrancl_on_into_rtrancl_on adj_in_verts) lemma reachable_adjI [intro, simp]: "u → v ⟹ u →⇧^{*}v" by (auto intro: adj_reachable_trans adj_in_verts) lemma reachable_trans[trans]: assumes "u →⇧^{*}v" "v →⇧^{*}w" shows "u →⇧^{*}w" using assms unfolding reachable_def by (rule rtrancl_on_trans) lemma reachable_induct[consumes 1, case_names base step]: assumes major: "u →⇧^{*}⇘_{G}⇙ v" and cases: "u ∈ verts G ⟹ P u" "⋀x y. ⟦u →⇧^{*}⇘_{G}⇙ x; x →⇘_{G}⇙ y; P x⟧ ⟹ P y" shows "P v" using assms unfolding reachable_def by (rule rtrancl_on_induct) auto lemma converse_reachable_induct[consumes 1, case_names base step, induct pred: reachable]: assumes major: "u →⇧^{*}⇘_{G}⇙ v" and cases: "v ∈ verts G ⟹ P v" "⋀x y. ⟦x →⇘_{G}⇙ y; y →⇧^{*}⇘_{G}⇙ v; P y⟧ ⟹ P x" shows "P u" using assms unfolding reachable_def by (rule converse_rtrancl_on_induct) auto lemma (in pre_digraph) converse_reachable_cases: assumes "u →⇧^{*}⇘_{G}⇙ v" obtains (base) "u = v" "u ∈ verts G" | (step) w where "u →⇘_{G}⇙ w" "w →⇧^{*}⇘_{G}⇙ v" using assms unfolding reachable_def by (cases rule: converse_rtrancl_on_cases) auto lemma reachable_in_verts: assumes "u →⇧^{*}v" shows "u ∈ verts G" "v ∈ verts G" using assms by induct (simp_all add: adj_in_verts) lemma reachable1_in_verts: assumes "u →⇧^{+}v" shows "u ∈ verts G" "v ∈ verts G" using assms by induct (simp_all add: adj_in_verts) lemma reachable1_reachable[intro]: "v →⇧^{+}w ⟹ v →⇧^{*}w" unfolding reachable_def by (rule rtrancl_consistent_rtrancl_on) (simp_all add: reachable1_in_verts adj_in_verts) lemmas reachable1_reachableE[elim] = reachable1_reachable[elim_format] lemma reachable_neq_reachable1[intro]: assumes reach: "v →⇧^{*}w" and neq: "v ≠ w" shows "v →⇧^{+}w" proof - from reach have "(v,w) ∈ (arcs_ends G)^*" by (rule reachable_rtranclI) with neq show ?thesis by (auto dest: rtranclD) qed lemmas reachable_neq_reachable1E[elim] = reachable_neq_reachable1[elim_format] lemma reachable1_reachable_trans [trans]: "u →⇧^{+}v ⟹ v →⇧^{*}w ⟹ u →⇧^{+}w" by (metis trancl_trans reachable_neq_reachable1) lemma reachable_reachable1_trans [trans]: "u →⇧^{*}v ⟹ v →⇧^{+}w ⟹ u →⇧^{+}w" by (metis trancl_trans reachable_neq_reachable1) lemma reachable_conv: "u →⇧^{*}v ⟷ (u,v) ∈ (arcs_ends G)^* ∩ (verts G × verts G)" apply (auto intro: reachable_in_verts) apply (induct rule: rtrancl_induct) apply auto done lemma reachable_conv': assumes "u ∈ verts G" shows "u →⇧^{*}v ⟷ (u,v) ∈ (arcs_ends G)⇧^{*}" (is "?L = ?R") proof assume "?R" then show "?L" using assms by induct auto qed (auto simp: reachable_conv) end lemma (in sym_digraph) symmetric_reachable': assumes "v →⇧^{*}⇘_{G}⇙ w" shows "w →⇧^{*}⇘_{G}⇙ v" using sym_arcs assms by (rule symmetric_reachable) subsection ‹Degrees of vertices› definition in_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where "in_arcs G v ≡ {e ∈ arcs G. head G e = v}" definition out_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where "out_arcs G v ≡ {e ∈ arcs G. tail G e = v}" definition in_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where "in_degree G v ≡ card (in_arcs G v)" definition out_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where "out_degree G v ≡ card (out_arcs G v)" lemma (in fin_digraph) finite_in_arcs[intro]: "finite (in_arcs G v)" unfolding in_arcs_def by auto lemma (in fin_digraph) finite_out_arcs[intro]: "finite (out_arcs G v)" unfolding out_arcs_def by auto lemma in_in_arcs_conv[simp]: "e ∈ in_arcs G v ⟷ e ∈ arcs G ∧ head G e = v" unfolding in_arcs_def by auto lemma in_out_arcs_conv[simp]: "e ∈ out_arcs G v ⟷ e ∈ arcs G ∧ tail G e = v" unfolding out_arcs_def by auto lemma inout_arcs_arc_simps[simp]: assumes "e ∈ arcs G" shows "tail G e = u ⟹ out_arcs G u ∩ insert e E = insert e (out_arcs G u ∩ E)" "tail G e ≠ u ⟹ out_arcs G u ∩ insert e E = out_arcs G u ∩ E" "out_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *) "head G e = u ⟹ in_arcs G u ∩ insert e E = insert e (in_arcs G u ∩ E)" "head G e ≠ u ⟹ in_arcs G u ∩ insert e E = in_arcs G u ∩ E" "in_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *) using assms by auto lemma in_arcs_int_arcs[simp]: "in_arcs G u ∩ arcs G = in_arcs G u" and out_arcs_int_arcs[simp]: "out_arcs G u ∩ arcs G = out_arcs G u" by auto lemma in_arcs_in_arcs: "x ∈ in_arcs G u ⟹ x ∈ arcs G" and out_arcs_in_arcs: "x ∈ out_arcs G u ⟹ x ∈ arcs G" by (auto simp: in_arcs_def out_arcs_def) subsection ‹Graph operations› context pre_digraph begin definition add_arc :: "'b ⇒ ('a,'b) pre_digraph" where "add_arc a = ⦇ verts = verts G ∪ {tail G a, head G a}, arcs = insert a (arcs G), tail = tail G, head = head G ⦈" definition del_arc :: "'b ⇒ ('a,'b) pre_digraph" where "del_arc a = ⦇ verts = verts G, arcs = arcs G - {a}, tail = tail G, head = head G ⦈" definition add_vert :: "'a ⇒ ('a,'b) pre_digraph" where "add_vert v = ⦇ verts = insert v (verts G), arcs = arcs G, tail = tail G, head = head G ⦈" definition del_vert :: "'a ⇒ ('a,'b) pre_digraph" where "del_vert v = ⦇ verts = verts G - {v}, arcs = {a ∈ arcs G. tail G a ≠ v ∧ head G a ≠ v}, tail = tail G, head = head G ⦈" lemma verts_add_arc: "⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ verts (add_arc a) = verts G" and verts_add_arc_conv: "verts (add_arc a) = verts G ∪ {tail G a, head G a}" and arcs_add_arc: "arcs (add_arc a) = insert a (arcs G)" and tail_add_arc: "tail (add_arc a) = tail G" and head_add_arc: "head (add_arc a) = head G" by (auto simp: add_arc_def) lemmas add_arc_simps[simp] = verts_add_arc arcs_add_arc tail_add_arc head_add_arc lemma verts_del_arc: "verts (del_arc a) = verts G" and arcs_del_arc: "arcs (del_arc a) = arcs G - {a}" and tail_del_arc: "tail (del_arc a) = tail G" and head_del_arc: "head (del_arc a) = head G" by (auto simp: del_arc_def) lemmas del_arc_simps[simp] = verts_del_arc arcs_del_arc tail_del_arc head_del_arc lemma verts_add_vert: "verts (pre_digraph.add_vert G u) = insert u (verts G)" and arcs_add_vert: "arcs (pre_digraph.add_vert G u) = arcs G" and tail_add_vert: "tail (pre_digraph.add_vert G u) = tail G" and head_add_vert: "head (pre_digraph.add_vert G u) = head G" by (auto simp: pre_digraph.add_vert_def) lemmas add_vert_simps = verts_add_vert arcs_add_vert tail_add_vert head_add_vert lemma verts_del_vert: "verts (pre_digraph.del_vert G u) = verts G - {u}" and arcs_del_vert: "arcs (pre_digraph.del_vert G u) = {a ∈ arcs G. tail G a ≠ u ∧ head G a ≠ u}" and tail_del_vert: "tail (pre_digraph.del_vert G u) = tail G" and head_del_vert: "head (pre_digraph.del_vert G u) = head G" and ends_del_vert: "arc_to_ends (pre_digraph.del_vert G u) = arc_to_ends G" by (auto simp: pre_digraph.del_vert_def arc_to_ends_def) lemmas del_vert_simps = verts_del_vert arcs_del_vert tail_del_vert head_del_vert lemma add_add_arc_collapse[simp]: "pre_digraph.add_arc (add_arc a) a = add_arc a" by (auto simp: pre_digraph.add_arc_def) lemma add_del_arc_collapse[simp]: "pre_digraph.add_arc (del_arc a) a = add_arc a" by (auto simp: pre_digraph.verts_add_arc_conv pre_digraph.add_arc_simps) lemma del_add_arc_collapse[simp]: "⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ pre_digraph.del_arc (add_arc a) a = del_arc a" by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps) lemma del_del_arc_collapse[simp]: "pre_digraph.del_arc (del_arc a) a = del_arc a" by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps) lemma add_arc_commute: "pre_digraph.add_arc (add_arc b) a = pre_digraph.add_arc (add_arc a) b" by (auto simp: pre_digraph.add_arc_def) lemma del_arc_commute: "pre_digraph.del_arc (del_arc b) a = pre_digraph.del_arc (del_arc a) b" by (auto simp: pre_digraph.del_arc_def) lemma del_arc_in: "a ∉ arcs G ⟹ del_arc a = G" by (rule pre_digraph.equality) (auto simp: add_arc_def) lemma in_arcs_add_arc_iff: "in_arcs (add_arc a) u = (if head G a = u then insert a (in_arcs G u) else in_arcs G u)" by auto lemma out_arcs_add_arc_iff: "out_arcs (add_arc a) u = (if tail G a = u then insert a (out_arcs G u) else out_arcs G u)" by auto lemma in_arcs_del_arc_iff: "in_arcs (del_arc a) u = (if head G a = u then in_arcs G u - {a} else in_arcs G u)" by auto lemma out_arcs_del_arc_iff: "out_arcs (del_arc a) u = (if tail G a = u then out_arcs G u - {a} else out_arcs G u)" by auto lemma (in wf_digraph) add_arc_in: "a ∈ arcs G ⟹ add_arc a = G" by (rule pre_digraph.equality) (auto simp: add_arc_def) end context wf_digraph begin lemma wf_digraph_add_arc[intro]: "wf_digraph (add_arc a)" by unfold_locales (auto simp: verts_add_arc_conv) lemma wf_digraph_del_arc[intro]: "wf_digraph (del_arc a)" by unfold_locales (auto simp: verts_add_arc_conv) lemma wf_digraph_del_vert: "wf_digraph (del_vert u)" by standard (auto simp: del_vert_simps) lemma wf_digraph_add_vert: "wf_digraph (add_vert u)" by standard (auto simp: add_vert_simps) lemma del_vert_add_vert: assumes "u ∉ verts G" shows "pre_digraph.del_vert (add_vert u) u = G" using assms by (intro pre_digraph.equality) (auto simp: pre_digraph.del_vert_def add_vert_def) end context fin_digraph begin lemma in_degree_add_arc_iff: "in_degree (add_arc a) u = (if head G a = u ∧ a ∉ arcs G then in_degree G u + 1 else in_degree G u)" proof - have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def) with finite_in_arcs show ?thesis unfolding in_degree_def by (auto simp: in_arcs_add_arc_iff intro: arg_cong[where f=card]) qed lemma out_degree_add_arc_iff: "out_degree (add_arc a) u = (if tail G a = u ∧ a ∉ arcs G then out_degree G u + 1 else out_degree G u)" proof - have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def) with finite_out_arcs show ?thesis unfolding out_degree_def by (auto simp: out_arcs_add_arc_iff intro: arg_cong[where f=card]) qed lemma in_degree_del_arc_iff: "in_degree (del_arc a) u = (if head G a = u ∧ a ∈ arcs G then in_degree G u - 1 else in_degree G u)" proof - have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def) with finite_in_arcs show ?thesis unfolding in_degree_def by (auto simp: in_arcs_del_arc_iff intro: arg_cong[where f=card]) qed lemma out_degree_del_arc_iff: "out_degree (del_arc a) u = (if tail G a = u ∧ a ∈ arcs G then out_degree G u - 1 else out_degree G u)" proof - have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def) with finite_out_arcs show ?thesis unfolding out_degree_def by (auto simp: out_arcs_del_arc_iff intro: arg_cong[where f=card]) qed lemma fin_digraph_del_vert: "fin_digraph (del_vert u)" by standard (auto simp: del_vert_simps) lemma fin_digraph_del_arc: "fin_digraph (del_arc a)" by standard (auto simp: del_vert_simps) end end

# Theory Bidirected_Digraph

theory Bidirected_Digraph imports Digraph "HOL-Combinatorics.Permutations" begin section ‹Bidirected Graphs› locale bidirected_digraph = wf_digraph G for G + fixes arev :: "'b ⇒ 'b" assumes arev_dom: "⋀a. a ∈ arcs G ⟷ arev a ≠ a" assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a" assumes tail_arev[simp]: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a" lemma (in wf_digraph) bidirected_digraphI: assumes arev_eq: "⋀a. a ∉ arcs G ⟹ arev a = a" assumes arev_neq: "⋀a. a ∈ arcs G ⟹ arev a ≠ a" assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a" assumes tail_arev: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a" shows "bidirected_digraph G arev" using assms by unfold_locales (auto simp: permutes_def) context bidirected_digraph begin lemma bidirected_digraph[intro!]: "bidirected_digraph G arev" by unfold_locales lemma arev_arev[simp]: "arev (arev a) = a" using arev_dom by (cases "a ∈ arcs G") (auto simp: arev_arev_raw) lemma arev_o_arev[simp]: "arev o arev = id" by (simp add: fun_eq_iff) lemma arev_eq: "a ∉ arcs G ⟹ arev a = a" by (simp add: arev_dom) lemma arev_neq: "a ∈ arcs G ⟹ arev a ≠ a" by (simp add: arev_dom) lemma arev_in_arcs[simp]: "a ∈ arcs G ⟹ arev a ∈ arcs G" by (metis arev_arev arev_dom) lemma head_arev[simp]: assumes "a ∈ arcs G" shows "head G (arev a) = tail G a" proof - from assms have "head G (arev a) = tail G (arev (arev a)) " by (simp only: tail_arev arev_in_arcs) then show ?thesis by simp qed lemma ate_arev[simp]: assumes "a ∈ arcs G" shows "arc_to_ends G (arev a) = prod.swap (arc_to_ends G a)" using assms by (auto simp: arc_to_ends_def) lemma bij_arev: "bij arev" using arev_arev by (metis bij_betw_imageI inj_on_inverseI surjI) lemma arev_permutes_arcs: "arev permutes arcs G" using arev_dom bij_arev by (auto simp: permutes_def bij_iff) lemma arev_eq_iff: "⋀x y. arev x = arev y ⟷ x = y" by (metis arev_arev) lemma in_arcs_eq: "in_arcs G w = arev ` out_arcs G w" by auto (metis arev_arev arev_in_arcs image_eqI in_out_arcs_conv tail_arev) lemma inj_on_arev[intro!]: "inj_on arev S" by (metis arev_arev inj_on_inverseI) lemma even_card_loops: "even (card (in_arcs G w ∩ out_arcs G w))" (is "even (card ?S)") proof - { assume "¬finite ?S" then have ?thesis by simp } moreover { assume A:"finite ?S" have "card ?S = card (⋃{{a,arev a} | a. a ∈ ?S})" (is "_ = card (⋃ ?T)") by (rule arg_cong[where f=card]) (auto intro!: exI[where x="{x, arev x}" for x]) also have "…= sum card ?T" proof (rule card_Union_disjoint) show "⋀A. A∈{{a, arev a} |a. a ∈ ?S} ⟹ finite A" by auto show "pairwise disjnt {{a, arev a} |a. a ∈ in_arcs G w ∩ out_arcs G w}" unfolding pairwise_def disjnt_def by safe (simp_all add: arev_eq_iff) qed also have "… = sum (λa. 2) ?T" by (intro sum.cong) (auto simp: card_insert_if dest: arev_neq) also have "… = 2 * card ?T" by simp finally have ?thesis by simp } ultimately show ?thesis by blast qed end (*XXX*) sublocale bidirected_digraph ⊆ sym_digraph proof (unfold_locales, unfold symmetric_def, intro symI) fix u v assume "u →⇘_{G}⇙ v" then obtain a where "a ∈ arcs G" "arc_to_ends G a = (u,v)" by (auto simp: arcs_ends_def) then have "arev a ∈ arcs G" "arc_to_ends G (arev a) = (v,u)" by (auto simp: arc_to_ends_def) then show "v →⇘_{G}⇙ u" by (auto simp: arcs_ends_def intro: rev_image_eqI) qed end

# Theory Arc_Walk

(* Title: Arc_Walk.thy Author: Lars Noschinski, TU München *) theory Arc_Walk imports Digraph begin section ‹Arc Walks› text ‹ We represent a walk in a graph by the list of its arcs. › type_synonym 'b awalk = "'b list" context pre_digraph begin text ‹ The list of vertices of a walk. The additional vertex argument is there to deal with the case of empty walks. › primrec awalk_verts :: "'a ⇒ 'b awalk ⇒ 'a list" where "awalk_verts u [] = [u]" | "awalk_verts u (e # es) = tail G e # awalk_verts (head G e) es" abbreviation awhd :: "'a ⇒ 'b awalk ⇒ 'a" where "awhd u p ≡ hd (awalk_verts u p)" abbreviation awlast:: "'a ⇒ 'b awalk ⇒ 'a" where "awlast u p ≡ last (awalk_verts u p)" text ‹ Tests whether a list of arcs is a consistent arc sequence, i.e. a list of arcs, where the head G node of each arc is the tail G node of the following arc. › fun cas :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "cas u [] v = (u = v)" | "cas u (e # es) v = (tail G e = u ∧ cas (head G e) es v)" lemma cas_simp: assumes "es ≠ []" shows "cas u es v ⟷ tail G (hd es) = u ∧ cas (head G (hd es)) (tl es) v" using assms by (cases es) auto definition awalk :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "awalk u p v ≡ u ∈ verts G ∧ set p ⊆ arcs G ∧ cas u p v" (* XXX: rename to atrail? *) definition (in pre_digraph) trail :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "trail u p v ≡ awalk u p v ∧ distinct p" definition apath :: "'a ⇒'b awalk ⇒ 'a ⇒ bool" where "apath u p v ≡ awalk u p v ∧ distinct (awalk_verts u p)" end subsection ‹Basic Lemmas› lemma (in pre_digraph) awalk_verts_conv: "awalk_verts u p = (if p = [] then [u] else map (tail G) p @ [head G (last p)])" by (induct p arbitrary: u) auto lemma (in pre_digraph) awalk_verts_conv': assumes "cas u p v" shows "awalk_verts u p = (if p = [] then [u] else tail G (hd p) # map (head G) p)" using assms by (induct u p v rule: cas.induct) (auto simp: cas_simp) lemma (in pre_digraph) length_awalk_verts: "length (awalk_verts u p) = Suc (length p)" by (simp add: awalk_verts_conv) lemma (in pre_digraph) awalk_verts_ne_eq: assumes "p ≠ []" shows "awalk_verts u p = awalk_verts v p" using assms by (auto simp: awalk_verts_conv) lemma (in pre_digraph) awalk_verts_non_Nil[simp]: "awalk_verts u p ≠ []" by (simp add: awalk_verts_conv) context wf_digraph begin lemma assumes "cas u p v" shows awhd_if_cas: "awhd u p = u" and awlast_if_cas: "awlast u p = v" using assms by (induct p arbitrary: u) auto lemma awalk_verts_in_verts: assumes "u ∈ verts G" "set p ⊆ arcs G" "v ∈ set (awalk_verts u p)" shows "v ∈ verts G" using assms by (induct p arbitrary: u) (auto intro: wellformed) lemma assumes "u ∈ verts G" "set p ⊆ arcs G" shows awhd_in_verts: "awhd u p ∈ verts G" and awlast_in_verts: "awlast u p ∈ verts G" using assms by (auto elim: awalk_verts_in_verts) lemma awalk_conv: "awalk u p v = (set (awalk_verts u p) ⊆ verts G ∧ set p ⊆ arcs G ∧ awhd u p = u ∧ awlast u p = v ∧ cas u p v)" unfolding awalk_def using hd_in_set[OF awalk_verts_non_Nil, of u p] by (auto intro: awalk_verts_in_verts awhd_if_cas awlast_if_cas simp del: hd_in_set) lemma awalkI: assumes "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" shows "awalk u p v" using assms by (auto simp: awalk_conv awhd_if_cas awlast_if_cas) lemma awalkE[elim]: assumes "awalk u p v" obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" "awhd u p = u" "awlast u p = v" using assms by (auto simp add: awalk_conv) lemma awalk_Nil_iff: "awalk u [] v ⟷ u = v ∧ u ∈ verts G" unfolding awalk_def by auto lemma trail_Nil_iff: "trail u [] v ⟷ u = v ∧ u ∈ verts G" by (auto simp: trail_def awalk_Nil_iff) lemma apath_Nil_iff: "apath u [] v ⟷ u = v ∧ u ∈ verts G" by (auto simp: apath_def awalk_Nil_iff) lemma awalk_hd_in_verts: "awalk u p v ⟹ u ∈ verts G" by (cases p) auto lemma awalk_last_in_verts: "awalk u p v ⟹ v ∈ verts G" unfolding awalk_conv by auto lemma hd_in_awalk_verts: "awalk u p v ⟹ u ∈ set (awalk_verts u p)" "apath u p v ⟹ u ∈ set (awalk_verts u p)" by (case_tac [!]p) (auto simp: apath_def) lemma awalk_Cons_iff: "awalk u (e # es) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ awalk (head G e) es w" by (auto simp: awalk_def) lemma trail_Cons_iff: "trail u (e # es ) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ e ∉ set es ∧ trail (head G e) es w" by (auto simp: trail_def awalk_Cons_iff) lemma apath_Cons_iff: "apath u (e # es) w ⟷ e ∈ arcs G ∧ tail G e = u ∧ apath (head G e) es w ∧ tail G e ∉ set (awalk_verts (head G e) es)" (is "?L ⟷ ?R") by (auto simp: apath_def awalk_Cons_iff) lemmas awalk_simps = awalk_Nil_iff awalk_Cons_iff lemmas trail_simps = trail_Nil_iff trail_Cons_iff lemmas apath_simps = apath_Nil_iff apath_Cons_iff lemma arc_implies_awalk: "e ∈ arcs G ⟹ awalk (tail G e) [e] (head G e)" by (simp add: awalk_simps) lemma apath_nonempty_ends: assumes "apath u p v" assumes "p ≠ []" shows "u ≠ v" using assms proof (induct p arbitrary: u) case (Cons e es) then have "apath (head G e) es v" "u ∉ set (awalk_verts (head G e) es)" by (auto simp: apath_Cons_iff) moreover then have "v ∈ set (awalk_verts (head G e) es)" by (auto simp: apath_def) ultimately show "u ≠ v" by auto qed simp (* replace by awalk_Cons_iff?*) lemma awalk_ConsI: assumes "awalk v es w" assumes "e ∈ arcs G" and "arc_to_ends G e = (u,v)" shows "awalk u (e # es) w" using assms by (cases es) (auto simp: awalk_def arc_to_ends_def) lemma (in pre_digraph) awalkI_apath: assumes "apath u p v" shows "awalk u p v" using assms by (simp add: apath_def) lemma arcE: assumes "arc e (u,v)" assumes "⟦e ∈ arcs G; tail G e = u; head G e = v⟧ ⟹ P" shows "P" using assms by (auto simp: arc_def) lemma in_arcs_imp_in_arcs_ends: assumes "e ∈ arcs G" shows "(tail G e, head G e) ∈ arcs_ends G" using assms by (auto simp: arcs_ends_conv) lemma set_awalk_verts_cas: assumes "cas u p v" shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)" using assms proof (induct p arbitrary: u) case Nil then show ?case by simp next case (Cons e es) then have "set (awalk_verts (head G e) es) = {head G e} ∪ set (map (tail G) es) ∪ set (map (head G) es)" by (auto simp: awalk_Cons_iff) with Cons.prems show ?case by auto qed lemma set_awalk_verts_not_Nil_cas: assumes "cas u p v" "p ≠ []" shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)" proof - have "u ∈ set (map (tail G) p)" using assms by (cases p) auto with assms show ?thesis by (auto simp: set_awalk_verts_cas) qed lemma set_awalk_verts: assumes "awalk u p v" shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)" using assms by (intro set_awalk_verts_cas) blast lemma set_awalk_verts_not_Nil: assumes "awalk u p v" "p ≠ []" shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)" using assms by (intro set_awalk_verts_not_Nil_cas) blast lemma awhd_of_awalk: "awalk u p v ⟹ awhd u p = u" and awlast_of_awalk: "awalk u p v ⟹ NOMATCH (awlast u p) v ⟹ awlast u p = v" unfolding NOMATCH_def by auto lemmas awends_of_awalk[simp] = awhd_of_awalk awlast_of_awalk lemma awalk_verts_arc1: assumes "e ∈ set p" shows "tail G e ∈ set (awalk_verts u p)" using assms by (auto simp: awalk_verts_conv) lemma awalk_verts_arc2: assumes "awalk u p v" "e ∈ set p" shows "head G e ∈ set (awalk_verts u p)" using assms by (simp add: set_awalk_verts) lemma awalk_induct_raw[case_names Base Cons(*, induct pred: awalk*)]: assumes "awalk u p v" assumes "⋀w1. w1 ∈ verts G ⟹ P w1 [] w1" assumes "⋀w1 w2 e es. e ∈ arcs G ⟹ arc_to_ends G e = (w1, w2) ⟹ P w2 es v ⟹ P w1 (e # es) v" shows "P u p v" using assms proof (induct p arbitrary: u v) case Nil then show ?case using Nil.prems by auto next case (Cons e es) from Cons.prems(1) show ?case by (intro Cons) (auto intro: Cons(2-) simp: arc_to_ends_def awalk_Cons_iff) qed subsection ‹Appending awalks› lemma (in pre_digraph) cas_append_iff[simp]: "cas u (p @ q) v ⟷ cas u p (awlast u p) ∧ cas (awlast u p) q v" by (induct u p v rule: cas.induct) auto lemma cas_ends: assumes "cas u p v" "cas u' p v'" shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms by (induct u p v arbitrary: u u' rule: cas.induct) auto lemma awalk_ends: assumes "awalk u p v" "awalk u' p v'" shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms by (simp add: awalk_def cas_ends) lemma awalk_ends_eqD: assumes "awalk u p u" "awalk v p w" shows "v = w" using awalk_ends[OF assms(1,2)] by auto lemma awalk_empty_ends: assumes "awalk u [] v" shows "u = v" using assms by (auto simp: awalk_def) lemma apath_ends: assumes "apath u p v" and "apath u' p v'" shows "(p ≠ [] ∧ u ≠ v ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms unfolding apath_def by (metis assms(2) apath_nonempty_ends awalk_ends) lemma awalk_append_iff[simp]: "awalk u (p @ q) v ⟷ awalk u p (awlast u p) ∧ awalk (awlast u p) q v" (is "?L ⟷ ?R") by (auto simp: awalk_def intro: awlast_in_verts) lemma awlast_append: "awlast u (p @ q) = awlast (awlast u p) q" by (simp add: awalk_verts_conv) lemma awhd_append: "awhd u (p @ q) = awhd (awhd u q) p" by (simp add: awalk_verts_conv) declare awalkE[rule del] lemma awalkE'[elim]: assumes "awalk u p v" obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" "awhd u p = u" "awlast u p = v" "u ∈ verts G" "v ∈ verts G" proof - have "u ∈ set (awalk_verts u p)" "v ∈ set (awalk_verts u p)" using assms by (auto simp: hd_in_awalk_verts elim: awalkE) then show ?thesis using assms by (auto elim: awalkE intro: that) qed lemma awalk_appendI: assumes "awalk u p v" assumes "awalk v q w" shows "awalk u (p @ q) w" using assms proof (induct p arbitrary: u) case Nil then show ?case by auto next case (Cons e es) from Cons.prems have ee_e: "arc_to_ends G e = (u, head G e)" unfolding arc_to_ends_def by auto have "awalk (head G e) es v" using ee_e Cons(2) awalk_Cons_iff by auto then show ?case using Cons ee_e by (auto simp: awalk_Cons_iff) qed lemma awalk_verts_append_cas: assumes "cas u (p @ q) v" shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)" using assms proof (induct p arbitrary: u) case Nil then show ?case by (cases q) auto qed (auto simp: awalk_Cons_iff) lemma awalk_verts_append: assumes "awalk u (p @ q) v" shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)" using assms by (intro awalk_verts_append_cas) blast lemma awalk_verts_append2: assumes "awalk u (p @ q) v" shows "awalk_verts u (p @ q) = butlast (awalk_verts u p) @ awalk_verts (awlast u p) q" using assms by (auto simp: awalk_verts_conv) lemma apath_append_iff: "apath u (p @ q) v ⟷ apath u p (awlast u p) ∧ apath (awlast u p) q v ∧ set (awalk_verts u p) ∩ set (tl (awalk_verts (awlast u p) q)) = {}" (is "?L ⟷ ?R") proof assume ?L then have "distinct (awalk_verts (awlast u p) q)" by (auto simp: apath_def awalk_verts_append2) with ‹?L› show ?R by (auto simp: apath_def awalk_verts_append) next assume ?R then show ?L by (auto simp: apath_def awalk_verts_append dest: distinct_tl) qed lemma (in wf_digraph) set_awalk_verts_append_cas: assumes "cas u p v" "cas v q w" shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)" proof - from assms have cas_pq: "cas u (p @ q) w" by (simp add: awlast_if_cas) moreover from assms have "v ∈ set (awalk_verts u p)" by (metis awalk_verts_non_Nil awlast_if_cas last_in_set) ultimately show ?thesis using assms by (auto simp: set_awalk_verts_cas) qed lemma (in wf_digraph) set_awalk_verts_append: assumes "awalk u p v" "awalk v q w" shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)" proof - from assms have "awalk u (p @ q) w" by auto moreover with assms have "v ∈ set (awalk_verts u (p @ q))" by (auto simp: awalk_verts_append) ultimately show ?thesis using assms by (auto simp: set_awalk_verts) qed lemma cas_takeI: assumes "cas u p v" "awlast u (take n p) = v'" shows "cas u (take n p) v'" proof - from assms have "cas u (take n p @ drop n p) v" by simp with assms show ?thesis unfolding cas_append_iff by simp qed lemma cas_dropI: assumes "cas u p v" "awlast u (take n p) = u'" shows "cas u' (drop n p) v" proof - from assms have "cas u (take n p @ drop n p) v" by simp with assms show ?thesis unfolding cas_append_iff by simp qed lemma awalk_verts_take_conv: assumes "cas u p v" shows "awalk_verts u (take n p) = take (Suc n) (awalk_verts u p)" proof - from assms have "cas u (take n p) (awlast u (take n p))" by (auto intro: cas_takeI) with assms show ?thesis by (cases n p rule: nat.exhaust[case_product list.exhaust]) (auto simp: awalk_verts_conv' take_map simp del: awalk_verts.simps) qed lemma awalk_verts_drop_conv: assumes "cas u p v" shows "awalk_verts u' (drop n p) = (if n < length p then drop n (awalk_verts u p) else [u'])" using assms by (auto simp: awalk_verts_conv drop_map) lemma awalk_decomp_verts: assumes cas: "cas u p v" and ev_decomp: "awalk_verts u p = xs @ y # ys" obtains q r where "cas u q y" "cas y r v" "p = q @ r" "awalk_verts u q = xs @ [y]" "awalk_verts y r = y # ys" using assms proof - define q r where "q = take (length xs) p" and "r = drop (length xs) p" then have p: "p = q @ r" by simp moreover from p have "cas u q (awlast u q)" "cas (awlast u q) r v" using ‹cas u p v› by auto moreover have "awlast u q = y" using q_def and assms by (auto simp: awalk_verts_take_conv) moreover have *: "awalk_verts u q = xs @ [awlast u q]" using assms q_def by (auto simp: awalk_verts_take_conv) moreover from * have "awalk_verts y r = y # ys" unfolding q_def r_def using assms by (auto simp: awalk_verts_drop_conv not_less) ultimately show ?thesis by (intro that) auto qed lemma awalk_decomp: assumes "awalk u p v" assumes "w ∈ set (awalk_verts u p)" shows "∃q r. p = q @ r ∧ awalk u q w ∧ awalk w r v" proof - from assms have "cas u p v" by auto moreover from assms obtain xs ys where "awalk_verts u p = xs @ w # ys" by (auto simp: in_set_conv_decomp) ultimately obtain q r where "cas u q w" "cas w r v" "p = q @ r" "awalk_verts u q = xs @ [w]" by (auto intro: awalk_decomp_verts) with assms show ?thesis by auto qed lemma awalk_not_distinct_decomp: assumes "awalk u p v" assumes "¬ distinct (awalk_verts u p)" shows "∃q r s. p = q @ r @ s ∧ distinct (awalk_verts u q) ∧ 0 < length r ∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)" proof - from assms obtain xs ys zs y where pv_decomp: "awalk_verts u p = xs @ y # ys @ y # zs" and xs_y_props: "distinct xs" "y ∉ set xs" "y ∉ set ys" using not_distinct_decomp_min_prefix by blast obtain q p' where "cas u q y" "p = q @ p'" "awalk_verts u q = xs @ [y]" and p'_props: "cas y p' v" "awalk_verts y p' = (y # ys) @ y # zs" using assms pv_decomp by - (rule awalk_decomp_verts, auto) obtain r s where "cas y r y" "cas y s v" "p' = r @ s" "awalk_verts y r = y # ys @ [y]" "awalk_verts y s = y # zs" using p'_props by (rule awalk_decomp_verts) auto have "p = q @ r @ s" using ‹p = q @ p'› ‹p' = r @ s› by simp moreover have "distinct (awalk_verts u q)" using ‹awalk_verts u q = xs @ [y]› and xs_y_props by simp moreover have "0 < length r" using ‹awalk_verts y r = y # ys @ [y]› by auto moreover from pv_decomp assms have "y ∈ verts G" by auto then have "awalk u q y" "awalk y r y" "awalk y s v" using ‹awalk u p v› ‹cas u q y› ‹cas y r y› ‹cas y s v› unfolding ‹p = q @ r @ s› by (auto simp: awalk_def) ultimately show ?thesis by blast qed lemma apath_decomp_disjoint: assumes "apath u p v" assumes "p = q @ r" assumes "x ∈ set (awalk_verts u q)" "x ∈ set (tl (awalk_verts (awlast u q) r))" shows False using assms by (auto simp: apath_def awalk_verts_append) subsection ‹Cycles› definition closed_w :: "'b awalk ⇒ bool" where "closed_w p ≡ ∃u. awalk u p u ∧ 0 < length p" text ‹ The definitions of cycles in textbooks vary w.r.t to the minimial length of a cycle. The definition given here matches \cite{diestel2010graph}. \cite{bangjensen2009digraphs} excludes loops from being cycles. Volkmann (Lutz Volkmann: Graphen an allen Ecken und Kanten, 2006 (?)) places no restriction on the length in the definition, but later usage assumes cycles to be non-empty. › definition (in pre_digraph) cycle :: "'b awalk ⇒ bool" where "cycle p ≡ ∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ p ≠ []" lemma cycle_altdef: "cycle p ⟷ closed_w p ∧ (∃u. distinct (tl (awalk_verts u p)))" by (cases p) (auto simp: closed_w_def cycle_def) lemma (in wf_digraph) distinct_tl_verts_imp_distinct: assumes "awalk u p v" assumes "distinct (tl (awalk_verts u p))" shows "distinct p" proof (rule ccontr) assume "¬distinct p" then obtain e xs ys zs where p_decomp: "p = xs @ e # ys @ e # zs" by (blast dest: not_distinct_decomp_min_prefix) then show False using assms p_decomp by (auto simp: awalk_verts_append awalk_Cons_iff set_awalk_verts) qed lemma (in wf_digraph) distinct_verts_imp_distinct: assumes "awalk u p v" assumes "distinct (awalk_verts u p)" shows "distinct p" using assms by (blast intro: distinct_tl_verts_imp_distinct distinct_tl) lemma (in wf_digraph) cycle_conv: "cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ distinct p ∧ p ≠ [])" unfolding cycle_def by (auto intro: distinct_tl_verts_imp_distinct) lemma (in loopfree_digraph) cycle_digraph_conv: "cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ 2 ≤ length p)" (is "?L ⟷ ?R") proof assume "cycle p" then obtain u where *: "awalk u p u" "distinct (tl (awalk_verts u p))" "p ≠ []" unfolding cycle_def by auto have "2 ≤ length p" proof (rule ccontr) assume "¬?thesis" with * obtain e where "p=[e]" by (cases p) (auto simp: not_le) then show False using * by (auto simp: awalk_simps dest: no_loops) qed then show ?R using * by auto qed (auto simp: cycle_def) lemma (in wf_digraph) closed_w_imp_cycle: assumes "closed_w p" shows "∃p. cycle p" using assms proof (induct "length p" arbitrary: p rule: less_induct) case less then obtain u where *: "awalk u p u" "p ≠ []" by (auto simp: closed_w_def) show ?thesis proof cases assume "distinct (tl (awalk_verts u p))" with less show ?thesis by (auto simp: closed_w_def cycle_altdef) next assume A: "¬distinct (tl (awalk_verts u p))" then obtain e es where "p = e # es" by (cases p) auto with A * have **: "awalk (head G e) es u" "¬distinct (awalk_verts (head G e) es)" by (auto simp: awalk_Cons_iff) obtain q r s where "es = q @ r @ s" "∃w. awalk w r w" "closed_w r" using awalk_not_distinct_decomp[OF **] by (auto simp: closed_w_def) then have "length r < length p" using ‹p = _› by auto then show ?thesis using ‹closed_w r› by (rule less) qed qed subsection ‹Reachability› lemma reachable1_awalk: "u →⇧^{+}v ⟷ (∃p. awalk u p v ∧ p ≠ [])" proof assume "u →⇧^{+}v" then show "∃p. awalk u p v ∧ p ≠ []" proof (induct rule: converse_trancl_induct) case (base y) then obtain e where "e ∈ arcs G" "tail G e = y" "head G e = v" by auto with arc_implies_awalk show ?case by auto next case (step x y) then obtain p where "awalk y p v" "p ≠ []" by auto moreover from ‹x → y› obtain e where "tail G e = x" "head G e = y" "e ∈ arcs G" by auto ultimately have "awalk x (e # p) v" by (auto simp: awalk_Cons_iff) then show ?case by auto qed next assume "∃p. awalk u p v ∧ p ≠ []" then obtain p where "awalk u p v" "p ≠ []" by auto thus "u →⇧^{+}v" proof (induct p arbitrary: u) case (Cons a as) then show ?case by (cases "as = []") (auto simp: awalk_simps trancl_into_trancl2 dest: in_arcs_imp_in_arcs_ends) qed simp qed lemma reachable_awalk: "u →⇧^{*}v ⟷ (∃p. awalk u p v)" proof cases assume "u = v" have "u →⇧^{*}u ⟷ awalk u [] u" by (auto simp: awalk_Nil_iff reachable_in_verts) also have "… ⟷ (∃p. awalk u p u)" by (metis awalk_Nil_iff awalk_hd_in_verts) finally show ?thesis using ‹u = v› by simp next assume "u ≠ v" then have "u →⇧^{*}v ⟷ u →⇧^{+}v" by auto also have "… ⟷ (∃p. awalk u p v)" using ‹u ≠ v› unfolding reachable1_awalk by force finally show ?thesis . qed lemma reachable_awalkI[intro?]: assumes "awalk u p v" shows "u →⇧^{*}v" unfolding reachable_awalk using assms by auto lemma reachable1_awalkI: "awalk v p w ⟹ p ≠ [] ⟹ v →⇧^{+}w" by (auto simp add: reachable1_awalk) lemma reachable_arc_trans: assumes "u →⇧^{*}v" "arc e (v,w)" shows "u →⇧^{*}w" proof - from ‹u →⇧^{*}v› obtain p where "awalk u p v" by (auto simp: reachable_awalk) moreover have "awalk v [e] w" using ‹arc e (v,w)› by (auto simp: arc_def awalk_def) ultimately have "awalk u (p @ [e]) w" by (rule awalk_appendI) then show ?thesis .. qed lemma awalk_verts_reachable_from: assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "u →⇧^{*}⇘_{G}⇙ w" proof - obtain s where "awalk u s w" using awalk_decomp[OF assms] by blast then show ?thesis by (metis reachable_awalk) qed lemma awalk_verts_reachable_to: assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "w →⇧^{*}⇘_{G}⇙ v" proof - obtain s where "awalk w s v" using awalk_decomp[OF assms] by blast then show ?thesis by (metis reachable_awalk) qed subsection ‹Paths› lemma (in fin_digraph) length_apath_less: assumes "apath u p v" shows "length p < card (verts G)" proof - have "length p < length (awalk_verts u p)" unfolding awalk_verts_conv by (auto simp: awalk_verts_conv) also have "length (awalk_verts u p) = card (set (awalk_verts u p))" using ‹apath u p v› by (auto simp: apath_def distinct_card) also have "… ≤ card (verts G)" using ‹apath u p v› unfolding apath_def awalk_conv by (auto intro: card_mono) finally show ?thesis . qed lemma (in fin_digraph) length_apath: assumes "apath u p v" shows "length p ≤ card (verts G)" using length_apath_less[OF assms] by auto lemma (in fin_digraph) apaths_finite_triple: shows "finite {(u,p,v). apath u p v}" proof - have "⋀u p v. awalk u p v ⟹ distinct (awalk_verts u p) ⟹length p ≤ card (verts G)" by (rule length_apath) (auto simp: apath_def) then have "{(u,p,v). apath u p v} ⊆ verts G × {es. set es ⊆ arcs G ∧ length es ≤ card (verts G)} × verts G" by (auto simp: apath_def) moreover have "finite ..." using finite_verts finite_arcs by (intro finite_cartesian_product finite_lists_length_le) ultimately show ?thesis by (rule finite_subset) qed lemma (in fin_digraph) apaths_finite: shows "finite {p. apath u p v}" proof - have "{p. apath u p v} ⊆ (fst o snd) ` {(u,p,v). apath u p v}" by force with apaths_finite_triple show ?thesis by (rule finite_surj) qed fun is_awalk_cyc_decomp :: "'b awalk => ('b awalk × 'b awalk × 'b awalk) ⇒ bool" where "is_awalk_cyc_decomp p (q,r,s) ⟷ p = q @ r @ s ∧ (∃u v w. awalk u q v ∧ awalk v r v ∧ awalk v s w) ∧ 0 <length r ∧ (∃u. distinct (awalk_verts u q))" definition awalk_cyc_decomp :: "'b awalk ⇒ 'b awalk × 'b awalk × 'b awalk" where "awalk_cyc_decomp p = (SOME qrs. is_awalk_cyc_decomp p qrs)" function awalk_to_apath :: "'b awalk ⇒ 'b awalk" where "awalk_to_apath p = (if ¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v) then (let (q,r,s) = awalk_cyc_decomp p in awalk_to_apath (q @ s)) else p)" by auto lemma awalk_cyc_decomp_has_prop: assumes "awalk u p v" and "¬distinct (awalk_verts u p)" shows "is_awalk_cyc_decomp p (awalk_cyc_decomp p)" proof - obtain q r s where *: "p = q @ r @ s ∧ distinct (awalk_verts u q) ∧ 0 < length r ∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)" by (atomize_elim) (rule awalk_not_distinct_decomp[OF assms]) then have "∃x. is_awalk_cyc_decomp p x" by (intro exI[where x="(q,r,s)"]) auto then show ?thesis unfolding awalk_cyc_decomp_def .. qed lemma awalk_cyc_decompE: assumes dec: "awalk_cyc_decomp p = (q,r,s)" assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)" obtains "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" proof show "p = q @ r @ s" "distinct (awalk_verts u q)" "closed_w r" using awalk_cyc_decomp_has_prop[OF p_props] and dec by (auto simp: closed_w_def awalk_verts_conv) then have "p ≠ []" by (auto simp: closed_w_def) (* TODO: Can we find some general rules to prove the last property?*) obtain u' w' v' where obt_awalk: "awalk u' q w'" "awalk w' r w'" "awalk w' s v'" using awalk_cyc_decomp_has_prop[OF p_props] and dec by auto then have "awalk u' p v'" using ‹p = q @ r @ s› by simp then have "u = u'" and "v = v'" using ‹p ≠ []› ‹awalk u p v› by (metis awalk_ends)+ then have "awalk u q w'" "awalk w' r w'" "awalk w' s v" using obt_awalk by auto then show "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" by auto qed lemma awalk_cyc_decompE': assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)" obtains q r s where "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" proof - obtain q r s where "awalk_cyc_decomp p = (q,r,s)" by (cases "awalk_cyc_decomp p") auto then have "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" using assms by (auto elim: awalk_cyc_decompE) then show ?thesis .. qed termination awalk_to_apath proof (relation "measure length") fix G p qrs rs q r s have X: "⋀x y. closed_w r ⟹ awalk x r y ⟹ x = y" unfolding closed_w_def by (blast dest: awalk_ends) assume "¬(∃u. distinct (awalk_verts u p)) ∧(∃u v. awalk u p v)" and **:"qrs = awalk_cyc_decomp p" "(q, rs) = qrs" "(r, s) = rs" then obtain u v where *: "awalk u p v" "¬distinct (awalk_verts u p)" by (cases p) auto then have "awalk_cyc_decomp p = (q,r,s)" using ** by simp then have "is_awalk_cyc_decomp p (q,r,s)" apply (rule awalk_cyc_decompE[OF _ *]) using X[of "awlast u q" "awlast (awlast u q) r"] *(1) by (auto simp: closed_w_def) then show "(q @ s, p) ∈ measure length" by (auto simp: closed_w_def) qed simp declare awalk_to_apath.simps[simp del] lemma awalk_to_apath_induct[consumes 1, case_names path decomp]: assumes awalk: "awalk u p v" assumes dist: "⋀p. awalk u p v ⟹ distinct (awalk_verts u p) ⟹ P p" assumes dec: "⋀p q r s. ⟦awalk u p v; awalk_cyc_decomp p = (q,r,s); ¬distinct (awalk_verts u p); P (q @ s)⟧ ⟹ P p" shows "P p" using awalk proof (induct "length p" arbitrary: p rule: less_induct) case less show ?case proof (cases "distinct (awalk_verts u p)") case True then show ?thesis by (auto intro: dist less.prems) next case False obtain q r s where p_cdecomp: "awalk_cyc_decomp p = (q,r,s)" by (cases "awalk_cyc_decomp p") auto then have "is_awalk_cyc_decomp p (q,r,s)" "p = q @ r @ s" using awalk_cyc_decomp_has_prop[OF less.prems(1) False] by auto then have "length (q @ s) < length p" "awalk u (q @ s) v" using less.prems by (auto dest!: awalk_ends_eqD) then have "P (q @ s)" by (auto intro: less) with p_cdecomp False show ?thesis by (auto intro: dec less.prems) qed qed lemma step_awalk_to_apath: assumes awalk: "awalk u p v" and decomp: "awalk_cyc_decomp p = (q, r, s)" and dist: "¬ distinct (awalk_verts u p)" shows "awalk_to_apath p = awalk_to_apath (q @ s)" proof - from dist have "¬(∃u. distinct (awalk_verts u p))" by (auto simp: awalk_verts_conv) with awalk and decomp show "awalk_to_apath p = awalk_to_apath (q @ s)" by (auto simp: awalk_to_apath.simps) qed lemma apath_awalk_to_apath: assumes "awalk u p v" shows "apath u (awalk_to_apath p) v" using assms proof (induct rule: awalk_to_apath_induct) case (path p) then have "awalk_to_apath p = p" by (auto simp: awalk_to_apath.simps) then show ?case using path by (auto simp: apath_def) next case (decomp p q r s) then show ?case using step_awalk_to_apath[of _ p _ q r s] by simp qed lemma (in wf_digraph) awalk_to_apath_subset: assumes "awalk u p v" shows "set (awalk_to_apath p) ⊆ set p" using assms proof (induct rule: awalk_to_apath_induct) case (path p) then have "awalk_to_apath p = p" by (auto simp: awalk_to_apath.simps) then show ?case by simp next case (decomp p q r s) have *: "¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v)" using decomp by (cases p) auto have "set (awalk_to_apath (q @ s)) ⊆ set p" using decomp by (auto elim!: awalk_cyc_decompE) then show ?case by (subst awalk_to_apath.simps) (simp only: * simp_thms if_True decomp Let_def prod.simps) qed lemma reachable_apath: "u →⇧^{*}v ⟷ (∃p. apath u p v)" by (auto intro: awalkI_apath apath_awalk_to_apath simp: reachable_awalk) lemma no_loops_in_apath: assumes "apath u p v" "a ∈ set p" shows "tail G a ≠ head G a" proof - from ‹a ∈ set p› obtain p1 p2 where "p = p1 @ a # p2" by (auto simp: in_set_conv_decomp) with ‹apath u p v› have "apath (tail G a) ([a] @ p2) (v)" by (auto simp: apath_append_iff apath_Cons_iff apath_Nil_iff) then have "apath (tail G a) [a] (head G a)" by - (drule apath_append_iff[THEN iffD1], simp) then show ?thesis by (auto simp: apath_Cons_iff) qed end end

# Theory Pair_Digraph

(* Title: Pair_Digraph.thy Author: Lars Noschinski, TU München *) theory Pair_Digraph imports Digraph Bidirected_Digraph Arc_Walk begin section ‹Digraphs without Parallel Arcs› text ‹ If no parallel arcs are desired, arcs can be accurately described as pairs of This is the natural representation for Digraphs without multi-arcs. and @{term "head G"}, making it easier to deal with multiple related graphs and to modify a graph by adding edges. This theory introduces such a specialisation of digraphs. › record 'a pair_pre_digraph = pverts :: "'a set" parcs :: "'a rel" definition with_proj :: "'a pair_pre_digraph ⇒ ('a, 'a × 'a) pre_digraph" where "with_proj G = ⦇ verts = pverts G, arcs = parcs G, tail = fst, head = snd ⦈" declare [[coercion with_proj]] primrec pawalk_verts :: "'a ⇒ ('a × 'a) awalk ⇒ 'a list" where "pawalk_verts u [] = [u]" | "pawalk_verts u (e # es) = fst e # pawalk_verts (snd e) es" fun pcas :: "'a ⇒ ('a × 'a) awalk ⇒ 'a ⇒ bool" where "pcas u [] v = (u = v)" | "pcas u (e # es) v = (fst e = u ∧ pcas (snd e) es v)" lemma with_proj_simps[simp]: "verts (with_proj G) = pverts G" "arcs (with_proj G) = parcs G" "arcs_ends (with_proj G) = parcs G" "tail (with_proj G) = fst" "head (with_proj G) = snd" by (auto simp: with_proj_def arcs_ends_conv) lemma cas_with_proj_eq: "pre_digraph.cas (with_proj G) = pcas" proof (unfold fun_eq_iff, intro allI) fix u es v show "pre_digraph.cas (with_proj G) u es v = pcas u es v" by (induct es arbitrary: u) (auto simp: pre_digraph.cas.simps) qed lemma awalk_verts_with_proj_eq: "pre_digraph.awalk_verts (with_proj G) = pawalk_verts" proof (unfold fun_eq_iff, intro allI) fix u es show "pre_digraph.awalk_verts (with_proj G) u es = pawalk_verts u es" by (induct es arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps) qed locale pair_pre_digraph = fixes G :: "'a pair_pre_digraph" begin lemmas [simp] = cas_with_proj_eq awalk_verts_with_proj_eq end locale pair_wf_digraph = pair_pre_digraph + assumes arc_fst_in_verts: "⋀e. e ∈ parcs G ⟹ fst e ∈ pverts G" assumes arc_snd_in_verts: "⋀e. e ∈ parcs G ⟹ snd e ∈ pverts G" begin lemma in_arcsD1: "(u,v) ∈ parcs G ⟹ u ∈ pverts G" and in_arcsD2: "(u,v) ∈ parcs G ⟹ v ∈ pverts G" by (auto dest: arc_fst_in_verts arc_snd_in_verts) lemmas wellformed' = in_arcsD1 in_arcsD2 end locale pair_fin_digraph = pair_wf_digraph + assumes pair_finite_verts: "finite (pverts G)" and pair_finite_arcs: "finite (parcs G)" locale pair_sym_digraph = pair_wf_digraph + assumes pair_sym_arcs: "symmetric G" locale pair_loopfree_digraph = pair_wf_digraph + assumes pair_no_loops: "e ∈ parcs G ⟹ fst e ≠ snd e" locale pair_bidirected_digraph = pair_sym_digraph + pair_loopfree_digraph locale pair_pseudo_graph = pair_fin_digraph + pair_sym_digraph locale pair_digraph = pair_fin_digraph + pair_loopfree_digraph locale pair_graph = pair_digraph + pair_pseudo_graph sublocale pair_pre_digraph ⊆ pre_digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" by unfold_locales auto sublocale pair_wf_digraph ⊆ wf_digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" by unfold_locales (auto simp: arc_fst_in_verts arc_snd_in_verts) sublocale pair_fin_digraph ⊆ fin_digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" using pair_finite_verts pair_finite_arcs by unfold_locales auto sublocale pair_sym_digraph ⊆ sym_digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" using pair_sym_arcs by unfold_locales auto sublocale pair_pseudo_graph ⊆ pseudo_graph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" by unfold_locales auto sublocale pair_loopfree_digraph ⊆ loopfree_digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" using pair_no_loops by unfold_locales auto sublocale pair_digraph ⊆ digraph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" by unfold_locales (auto simp: arc_to_ends_def) sublocale pair_graph ⊆ graph "with_proj G" rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd" and "arcs_ends G = parcs G" and "pre_digraph.awalk_verts G = pawalk_verts" and "pre_digraph.cas G = pcas" by unfold_locales auto sublocale pair_graph ⊆ pair_bidirected_digraph by unfold_locales lemma wf_digraph_wp_iff: "wf_digraph (with_proj G) = pair_wf_digraph G" (is "?L ⟷ ?R") proof assume ?L then interpret wf_digraph "with_proj G" . show ?R using wellformed by unfold_locales auto next assume ?R then interpret pair_wf_digraph G . show ?L by unfold_locales qed lemma (in pair_fin_digraph) pair_fin_digraph[intro!]: "pair_fin_digraph G" .. context pair_digraph begin lemma pair_wf_digraph[intro!]: "pair_wf_digraph G" by intro_locales lemma pair_digraph[intro!]: "pair_digraph G" .. lemma (in pair_loopfree_digraph) no_loops': "(u,v) ∈ parcs G ⟹ u ≠ v" by (auto dest: no_loops) end lemma (in pair_wf_digraph) apath_succ_decomp: assumes "apath u p v" assumes "(x,y) ∈ set p" assumes "y ≠ v" shows "∃p1 z p2. p = p1 @ (x,y) # (y,z) # p2 ∧ x ≠ z ∧ y ≠ z" proof - from ‹(x,y) ∈ set p› obtain p1 p2 where p_decomp: "p = p1 @ (x,y) # p2" by (metis (no_types) in_set_conv_decomp_first) from p_decomp ‹apath u p v› ‹y ≠ v› have "p2 ≠ []" "awalk y p2 v" by (auto simp: apath_def awalk_Cons_iff) then obtain z p2' where p2_decomp: "p2 = (y,z) # p2'" by atomize_elim (cases p2, auto simp: awalk_Cons_iff) then have "x ≠ z ∧ y ≠ z" using p_decomp p2_decomp ‹apath u p v› by (auto simp: apath_append_iff apath_simps hd_in_awalk_verts) with p_decomp p2_decomp have "p = p1 @ (x,y) # (y,z) # p2' ∧ x ≠ z ∧ y ≠ z" by auto then show ?thesis by blast qed lemma (in pair_sym_digraph) arcs_symmetric: "(a,b) ∈ parcs G ⟹ (b,a) ∈ parcs G" using sym_arcs by (auto simp: symmetric_def elim: symE) lemma (in pair_pseudo_graph) pair_pseudo_graph[intro]: "pair_pseudo_graph G" .. lemma (in pair_graph) pair_graph[intro]: "pair_graph G" by unfold_locales lemma (in pair_graph) pair_graphD_graph: "graph G" by unfold_locales lemma pair_graphI_graph: assumes "graph (with_proj G)" shows "pair_graph G" proof - interpret G: graph "with_proj G" by fact show ?thesis using G.wellformed G.finite_arcs G.finite_verts G.no_loops by unfold_locales auto qed lemma pair_loopfreeI_loopfree: assumes "loopfree_digraph (with_proj G)" shows "pair_loopfree_digraph G" proof - interpret loopfree_digraph "with_proj G" by fact show ?thesis using wellformed no_loops by unfold_locales auto qed subsection ‹Path reversal for Pair Digraphs› text ‹This definition is only meaningful in @{term Pair_Digraph}› primrec rev_path :: "('a × 'a) awalk ⇒ ('a × 'a) awalk" where "rev_path [] = []" | "rev_path (e # es) = rev_path es @ [(snd e, fst e)]" lemma rev_path_append[simp]: "rev_path (p @ q) = rev_path q @ rev_path p" by (induct p) auto lemma rev_path_rev_path[simp]: "rev_path (rev_path p) = p" by (induct p) auto lemma rev_path_empty[simp]: "rev_path p = [] ⟷ p = []" by (induct p) auto lemma rev_path_eq: "rev_path p = rev_path q ⟷ p = q" by (metis rev_path_rev_path) lemma (in pair_sym_digraph) assumes "awalk u p v" shows awalk_verts_rev_path: "awalk_verts v (rev_path p) = rev (awalk_verts u p)" and awalk_rev_path': "awalk v (rev_path p) u" using assms proof (induct p arbitrary: u) case Nil case 1 then show ?case by auto next case Nil case 2 then show ?case by (auto simp: awalk_Nil_iff) next case (Cons e es) case 1 with Cons have walks: "awalk v (rev_path es) (snd e)" "awalk (snd e) [(snd e, fst e)] u" and verts: "awalk_verts v (rev_path es) = rev (awalk_verts (snd e) es)" by (auto simp: awalk_simps intro: arcs_symmetric) from walks have "awalk v (rev_path es @ [(snd e, fst e)]) u" by simp moreover have "tl (awalk_verts (awlast v (rev_path es)) [(snd e, fst e)]) = [fst e]" by auto ultimately show ?case using 1 verts by (auto simp: awalk_verts_append) next case (Cons e es) case 2 with Cons have "awalk v (rev_path es) (snd e)" by (auto simp: awalk_Cons_iff) moreover have "rev_path (e # es) = rev_path es @ [(snd e, fst e)]" by auto moreover from Cons 2 have "awalk (snd e) [(snd e, fst e)] u" by (auto simp: awalk_simps intro: arcs_symmetric) ultimately show "awalk v (rev_path (e # es)) u" by simp qed lemma (in pair_sym_digraph) awalk_rev_path[simp]: "awalk v (rev_path p) u = awalk u p v" (is "?L = ?R") by (metis awalk_rev_path' rev_path_rev_path) lemma (in pair_sym_digraph) apath_rev_path[simp]: "apath v (rev_path p) u = apath u p v" by (auto simp: awalk_verts_rev_path apath_def) subsection ‹Subdividing Edges› text ‹subdivide an edge (=two associated arcs) in graph› fun subdivide :: "'a pair_pre_digraph ⇒ 'a × 'a ⇒ 'a ⇒ 'a pair_pre_digraph" where "subdivide G (u,v) w = ⦇ pverts = pverts G ∪ {w}, parcs = (parcs G - {(u,v),(v,u)}) ∪ {(u,w), (w,u), (w, v), (v, w)}⦈" declare subdivide.simps[simp del] text ‹subdivide an arc in a path› fun sd_path :: "'a × 'a ⇒ 'a ⇒ ('a × 'a) awalk ⇒ ('a × 'a) awalk" where "sd_path _ _ [] = []" | "sd_path (u,v) w (e # es) = (if e = (u,v) then [(u,w),(w,v)] else if e = (v,u) then [(v,w),(w,u)] else [e]) @ sd_path (u,v) w es" text ‹contract an arc in a path› fun co_path :: "'a × 'a ⇒ 'a ⇒ ('a × 'a) awalk ⇒ ('a × 'a) awalk" where "co_path _ _ [] = []" | "co_path _ _ [e] = [e]" | "co_path (u,v) w (e1 # e2 # es) = (if e1 = (u,w) ∧ e2 = (w,v) then (u,v) # co_path (u,v) w es else if e1 = (v,w) ∧ e2 = (w,u) then (v,u) # co_path (u,v) w es else e1 # co_path (u,v) w (e2 # es))" lemma co_path_simps[simp]: "⟦e1 ≠ (fst e, w); e1 ≠ (snd e,w)⟧ ⟹ co_path e w (e1 # es) = e1 # co_path e w es" "⟦e1 = (fst e, w); e2 = (w, snd e)⟧ ⟹ co_path e w (e1 # e2 # es) = e # co_path e w es" "⟦e1 = (snd e, w); e2 = (w, fst e)⟧ ⟹ co_path e w (e1 # e2 # es) = (snd e, fst e) # co_path e w es" "⟦e1 ≠ (fst e, w) ∨ e2 ≠ (w, snd e); e1 ≠ (snd e, w) ∨ e2 ≠ (w, fst e)⟧ ⟹ co_path e w (e1 # e2 # es) = e1 # co_path e w (e2 # es)" apply (cases es; auto) apply (cases e; auto) apply (cases e; auto) apply (cases e; cases "fst e = snd e"; auto) apply (cases e; cases "fst e = snd e"; auto) done lemma co_path_nonempty[simp]: "co_path e w p = [] ⟷ p = []" by (cases e) (cases p rule: list_exhaust_NSC, auto) declare co_path.simps(3)[simp del] lemma verts_subdivide[simp]: "pverts (subdivide G e w) = pverts G ∪ {w}" by (cases e) (auto simp: subdivide.simps) lemma arcs_subdivide[simp]: shows "parcs (subdivide G (u,v) w) = (parcs G - {(u,v),(v,u)}) ∪ {(u,w), (w,u), (w, v), (v, w)}" by (auto simp: subdivide.simps) lemmas subdivide_simps = verts_subdivide arcs_subdivide lemma sd_path_induct[case_names empty pass sd sdrev]: assumes A: "P e []" and B: "⋀e' es. e' ≠ e ⟹ e' ≠ (snd e , fst e) ⟹ P e es ⟹ P e (e' # es)" "⋀es. P e es ⟹ P e (e # es)" "⋀es. fst e ≠ snd e ⟹ P e es ⟹ P e ((snd e, fst e) # es)" shows "P e es" by (induct es) (rule A, metis B prod.collapse) lemma co_path_induct[case_names empty single co corev pass]: fixes e :: "'a × 'a" and w :: "'a" and p :: "('a × 'a) awalk" assumes Nil: "P e w []" and ConsNil:"⋀e'. P e w [e']" and ConsCons1: "⋀e1 e2 es. e1 = (fst e, w) ∧ e2 = (w, snd e) ⟹ P e w es ⟹ P e w (e1 # e2 # es)" and ConsCons2: "⋀e1 e2 es. ¬(e1 = (fst e, w) ∧ e2 = (w, snd e)) ∧ e1 = (snd e, w) ∧ e2 = (w, fst e) ⟹ P e w es ⟹ P e w (e1 # e2 # es)" and ConsCons3: "⋀e1 e2 es. ¬ (e1 = (fst e, w) ∧ e2 = (w, snd e)) ⟹ ¬ (e1 = (snd e, w) ∧ e2 = (w, fst e)) ⟹ P e w (e2 # es) ⟹ P e w (e1 # e2 # es)" shows "P e w p" proof (induct p rule: length_induct) case (1 p) then show ?case proof (cases p rule: list_exhaust_NSC) case (Cons_Cons e1 e2 es) then have "P e w es" "P e w (e2 # es)"using 1 by auto then show ?thesis unfolding Cons_Cons by (blast intro: ConsCons1 ConsCons2 ConsCons3) qed (auto intro: Nil ConsNil) qed lemma co_sd_id: assumes "(u,w) ∉ set p" "(v,w) ∉ set p" shows "co_path (u,v) w (sd_path (u,v) w p) = p" using assms by (induct p) auto lemma sd_path_id: assumes "(x,y) ∉ set p" "(y,x) ∉ set p" shows "sd_path (x,y) w p = p" using assms by (induct p) auto lemma (in pair_wf_digraph) pair_wf_digraph_subdivide: assumes props: "e ∈ parcs G" "w ∉ pverts G" shows "pair_wf_digraph (subdivide G e w)" (is "pair_wf_digraph ?sG") proof obtain u v where [simp]: "e = (u,v)" by (cases e) auto fix e' assume "e' ∈ parcs ?sG" then show "fst e' ∈ pverts ?sG" "snd e' ∈ pverts ?sG" using props by (auto dest: wellformed) qed lemma (in pair_sym_digraph) pair_sym_digraph_subdivide: assumes props: "e ∈ parcs G" "w ∉ pverts G" shows "pair_sym_digraph (subdivide G e w)" (is "pair_sym_digraph ?sG") proof - interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide) obtain u v where [simp]: "e = (u,v)" by (cases e) auto show ?thesis proof have "⋀a b. (a, b) ∈ parcs (subdivide G e w) ⟹ (b, a) ∈ parcs (subdivide G e w)" unfolding ‹e = _› arcs_subdivide by (elim UnE, rule UnI1, rule_tac [2] UnI2) (blast intro: arcs_symmetric)+ then show "symmetric ?sG" unfolding symmetric_def with_proj_simps by (rule symI) qed qed lemma (in pair_loopfree_digraph) pair_loopfree_digraph_subdivide: assumes props: "e ∈ parcs G" "w ∉ pverts G" shows "pair_loopfree_digraph (subdivide G e w)" (is "pair_loopfree_digraph ?sG") proof - interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide) from assms show ?thesis by unfold_locales (cases e, auto dest: wellformed no_loops) qed lemma (in pair_bidirected_digraph) pair_bidirected_digraph_subdivide: assumes props: "e ∈ parcs G" "w ∉ pverts G" shows "pair_bidirected_digraph (subdivide G e w)" (is "pair_bidirected_digraph ?sG") proof - interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide) interpret sdG: pair_loopfree_digraph "subdivide G e w" using assms by (rule pair_loopfree_digraph_subdivide) show ?thesis by unfold_locales qed lemma (in pair_pseudo_graph) pair_pseudo_graph_subdivide: assumes props: "e ∈ parcs G" "w ∉ pverts G" shows "pair_pseudo_graph (subdivide G e w)" (is "pair_pseudo_graph ?sG") proof - interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide) obtain u v where [simp]: "e = (u,v)" by (cases e) auto show ?thesis by unfold_locales (cases e, auto) qed lemma (in pair_graph) pair_graph_subdivide: assumes "e ∈ parcs G" "w ∉ pverts G" shows "pair_graph (subdivide G e w)" (is "pair_graph ?sG") proof - interpret PPG: pair_pseudo_graph "subdivide G e w" using assms by (rule pair_pseudo_graph_subdivide) interpret PPG: pair_loopfree_digraph "subdivide G e w" using assms by (rule pair_loopfree_digraph_subdivide) from assms show ?thesis by unfold_locales qed lemma arcs_subdivideD: assumes "x ∈ parcs (subdivide G e w)" "fst x ≠ w" "snd x ≠ w" shows "x ∈ parcs G" using assms by (cases e) auto context pair_sym_digraph begin lemma assumes path: "apath u p v" assumes elems: "e ∈ parcs G" "w ∉ pverts G" shows apath_sd_path: "pre_digraph.apath (subdivide G e w) u (sd_path e w p) v" (is ?A) and set_awalk_verts_sd_path: "set (awalk_verts u (sd_path e w p)) ⊆ set (awalk_verts u p) ∪ {w}" (is ?B) proof - obtain x y where e_conv: "e = (x,y)" by (cases e) auto define sG where "sG = subdivide G e w" interpret S: pair_sym_digraph sG unfolding sG_def using elems by (rule pair_sym_digraph_subdivide) have ev_sG: "S.awalk_verts = awalk_verts" by (auto simp: fun_eq_iff pre_digraph.awalk_verts_conv) have w_sG: "{(x,w), (y,w), (w,x), (w,y)} ⊆ parcs sG" by (auto simp: sG_def e_conv) from path have "S.apath u (sd_path (x,y) w p) v" and "set (S.awalk_verts u (sd_path (x,y) w p)) ⊆ set (awalk_verts u p) ∪ {w}" proof (induct p arbitrary: u rule: sd_path_induct) case empty case 1 moreover have "pverts sG = pverts G ∪ {w}" by (simp add: sG_def) ultimately show ?case by (auto simp: apath_Nil_iff S.apath_Nil_iff) next case empty case 2 then show ?case by simp next case (pass e' es) { case 1 then have "S.apath (snd e') (sd_path (x,y) w es) v" "u ≠ w" "fst e' = u" "u ∉ set (S.awalk_verts (snd e') (sd_path (x,y) w es))" using pass elems by (fastforce simp: apath_Cons_iff)+ moreover then have "e' ∈ parcs sG" using 1 pass by (auto simp: e_conv sG_def S.apath_Cons_iff apath_Cons_iff) ultimately show ?case using pass by (auto simp: S.apath_Cons_iff) } note case1 = this { case 2 with pass 2 show ?case by (simp add: apath_Cons_iff) blast } next { fix u es a b assume A: "apath u ((a,b) # es) v" and ab: "(a,b) = (x,y) ∨ (a,b) = (y,x)" and hyps: "⋀u. apath u es v ⟹ S.apath u (sd_path (x, y) w es) v" "⋀u. apath u es v ⟹ set (awalk_verts u (sd_path (x, y) w es)) ⊆ set (awalk_verts u es) ∪ {w}" from ab A have "(x,y) ∉ set es" "(y,x) ∉ set es" by (auto simp: apath_Cons_iff dest!: awalkI_apath dest: awalk_verts_arc1 awalk_verts_arc2) then have ev_sd: "set (S.awalk_verts b (sd_path (x,y) w es)) = set (awalk_verts b es)" by (simp add: sd_path_id) from A ab have [simp]: "x ≠ y" by (simp add: apath_Cons_iff) (metis awalkI_apath awalk_verts_non_Nil awhd_of_awalk hd_in_set) from A have "S.apath b (sd_path (x,y) w es) v" "u = a" "u ≠ w" using ab hyps elems by (auto simp: apath_Cons_iff wellformed') moreover then have "S.awalk u (sd_path (x, y) w ((a, b) # es)) v " using ab w_sG by (auto simp: S.apath_def S.awalk_simps S.wellformed') then have "u ∉ set (S.awalk_verts w ((w,b) # sd_path (x,y) w es))" using ab ‹u ≠ w› ev_sd A by (auto simp: apath_Cons_iff S.awalk_def) moreover have "w ∉ set (awalk_verts b (sd_path (x, y) w es))" using ab ev_sd A elems by (auto simp: awalk_Cons_iff apath_def) ultimately have path: "S.apath u (sd_path (x, y) w ((a, b) # es)) v " using ab hyps w_sG ‹u = a› by (auto simp: S.apath_Cons_iff ) } note path = this { case (sd es) { case 1 with sd show ?case by (intro path) auto } { case 2 show ?case using 2 sd by (auto simp: apath_Cons_iff) } } { case (sdrev es) { case 1 with sdrev show ?case by (intro path) auto } { case 2 show ?case using 2 sdrev by (auto simp: apath_Cons_iff) } } qed then show ?A ?B unfolding sG_def e_conv . qed lemma assumes elems: "e ∈ parcs G" "w ∉ pverts G" "u ∈ pverts G" "v ∈ pverts G" assumes path: "pre_digraph.apath (subdivide G e w) u p v" shows apath_co_path: "apath u (co_path e w p) v" (is ?thesis_path) and set_awalk_verts_co_path: "set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}" (is ?thesis_set) proof - obtain x y where e_conv: "e = (x,y)" by (cases e) auto interpret S: pair_sym_digraph "subdivide G e w" using elems(1,2) by (rule pair_sym_digraph_subdivide) have e_w: "fst e ≠ w" "snd e ≠ w" using elems by auto have "S.apath u p v" "u ≠ w" using elems path by auto then have co_path: "apath u (co_path e w p) v ∧ set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}" proof (induction p arbitrary: u rule: co_path_induct) case empty with elems show ?case by (simp add: apath_Nil_iff S.apath_Nil_iff) next case (single e') with elems show ?case by (auto simp: apath_Cons_iff S.apath_Cons_iff apath_Nil_iff S.apath_Nil_iff dest: arcs_subdivideD) next case (co e1 e2 es) then have "apath u (co_path e w (e1 # e2 # es)) v" using co e_w elems by (auto simp: apath_Cons_iff S.apath_Cons_iff) moreover have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}" using co e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff) ultimately show ?case by fast next case (corev e1 e2 es) have "apath u (co_path e w (e1 # e2 # es)) v" using corev(1-3) e_w(1) elems(1) by (auto simp: apath_Cons_iff S.apath_Cons_iff intro: arcs_symmetric) moreover have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}" using corev e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff) ultimately show ?case by fast next case (pass e1 e2 es) have "fst e1 ≠ w" using elems pass.prems by (auto simp: S.apath_Cons_iff) have "snd e1 ≠ w" proof assume "snd e1 = w" then have "e1 ∉ parcs G" using elems by auto then have "e1 ∈ parcs (subdivide G e w) - parcs G" using pass by (auto simp: S.apath_Cons_iff) then have "e1 = (x,w) ∨ e1 = (y,w)" using ‹fst e1 ≠ w› e_w by (auto simp add: e_conv) moreover have "fst e2 = w" using ‹snd e1 = w› pass.prems by (auto simp: S.apath_Cons_iff) then have "e2 ∉ parcs G" using elems by auto then have "e2 ∈ parcs (subdivide G e w) - parcs G" using pass by (auto simp: S.apath_Cons_iff) then have "e2 = (w,x) ∨ e2 = (w,y)" using ‹fst e2 = w› e_w by (cases e2) (auto simp add: e_conv) ultimately have "e1 = (x,w) ∧ e2 = (w,x) ∨ e1 = (y,w) ∧ e2 = (w,y)" using pass.hyps[simplified e_conv] by auto then show False using pass.prems by (cases es) (auto simp: S.apath_Cons_iff) qed then have "e1 ∈ parcs G" using ‹fst e1 ≠ w› pass.prems by (auto simp: S.apath_Cons_iff dest: arcs_subdivideD) have ih: "apath (snd e1) (co_path e w (e2 # es)) v ∧ set (awalk_verts (snd e1) (co_path e w (e2 # es))) = set (awalk_verts (snd e1) (e2 # es)) - {w}" using pass.prems ‹snd e1 ≠ w› by (intro pass.IH) (auto simp: apath_Cons_iff S.apath_Cons_iff) then have "fst e1 ∉ set (awalk_verts (snd e1) (co_path e w (e2 # es)))" "fst e1 = u" using pass.prems by (clarsimp simp: S.apath_Cons_iff)+ then have "apath u (co_path e w (e1 # e2 # es)) v" using ih pass ‹e1 ∈ parcs G› by (auto simp: apath_Cons_iff S.apath_Cons_iff)[] moreover have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}" using pass.hyps ih ‹fst e1 ≠ w› by auto ultimately show ?case by fast qed then show ?thesis_set ?thesis_path by blast+ qed end subsection ‹Bidirected Graphs› definition (in -) swap_in :: "('a × 'a) set ⇒ 'a × 'a ⇒ 'a × 'a" where "swap_in S x = (if x ∈ S then prod.swap x else x)" lemma bidirected_digraph_rev_conv_pair: assumes "bidirected_digraph (with_proj G) rev_G" shows "rev_G = swap_in (parcs G)" proof - interpret bidirected_digraph G rev_G by fact have "⋀a b. (a, b) ∈ parcs G ⟹ rev_G (a, b) = (b, a)" using tail_arev[simplified with_proj_simps] head_arev[simplified with_proj_simps] by (metis fst_conv prod.collapse snd_conv) then show ?thesis by (auto simp: swap_in_def fun_eq_iff arev_eq) qed lemma (in pair_bidirected_digraph) bidirected_digraph: "bidirected_digraph (with_proj G) (swap_in (parcs G))" using no_loops' arcs_symmetric by unfold_locales (auto simp: swap_in_def) lemma pair_bidirected_digraphI_bidirected_digraph: assumes "bidirected_digraph (with_proj G) (swap_in (parcs G))" shows "pair_bidirected_digraph G" proof - interpret bidirected_digraph "with_proj G" "swap_in (parcs G)" by fact { fix a assume "a ∈ parcs G" then have "fst a ≠ snd a" using arev_neq[of a] bidirected_digraph_rev_conv_pair[OF assms(1)] by (cases a) (auto simp: swap_in_def) } then show ?thesis using tail_in_verts head_in_verts by unfold_locales auto qed end

# Theory Digraph_Component

(* Title: Digraph_Component.thy Author: Lars Noschinski, TU München *) theory Digraph_Component imports Digraph Arc_Walk Pair_Digraph begin section ‹Components of (Symmetric) Digraphs› definition compatible :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where "compatible G H ≡ tail G = tail H ∧ head G = head H" (* Require @{term "wf_digraph G"}? *) definition subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where "subgraph H G ≡ verts H ⊆ verts G ∧ arcs H ⊆ arcs G ∧ wf_digraph G ∧ wf_digraph H ∧ compatible G H" definition induced_subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where "induced_subgraph H G ≡ subgraph H G ∧ arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}" definition spanning :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where "spanning H G ≡ subgraph H G ∧ verts G = verts H" definition strongly_connected :: "('a,'b) pre_digraph ⇒ bool" where "strongly_connected G ≡ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. u →⇧^{*}⇘_{G}⇙ v)" text ‹ The following function computes underlying symmetric graph of a digraph and removes parallel arcs. › definition mk_symmetric :: "('a,'b) pre_digraph ⇒ 'a pair_pre_digraph" where "mk_symmetric G ≡ ⦇ pverts = verts G, parcs = ⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)}⦈" definition connected :: "('a,'b) pre_digraph ⇒ bool" where "connected G ≡ strongly_connected (mk_symmetric G)" definition forest :: "('a,'b) pre_digraph ⇒ bool" where "forest G ≡ ¬(∃p. pre_digraph.cycle G p)" definition tree :: "('a,'b) pre_digraph ⇒ bool" where "tree G ≡ connected G ∧ forest G" definition spanning_tree :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where "spanning_tree H G ≡ tree H ∧ spanning H G" definition (in pre_digraph) max_subgraph :: "(('a,'b) pre_digraph ⇒ bool) ⇒ ('a,'b) pre_digraph ⇒ bool" where "max_subgraph P H ≡ subgraph H G ∧ P H ∧ (∀H'. H' ≠ H ∧ subgraph H H' ⟶ ¬(subgraph H' G ∧ P H'))" definition (in pre_digraph) sccs :: "('a,'b) pre_digraph set" where "sccs ≡ {H. induced_subgraph H G ∧ strongly_connected H ∧ ¬(∃H'. induced_subgraph H' G ∧ strongly_connected H' ∧ verts H ⊂ verts H')}" definition (in pre_digraph) sccs_verts :: "'a set set" where "sccs_verts = {S. S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧^{*}⇘_{G}⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧^{*}⇘_{G}⇙ v ∨ ¬v →⇧^{*}⇘_{G}⇙ u)}" (*XXX: "sccs_verts = verts ` sccs" *) definition (in pre_digraph) scc_of :: "'a ⇒ 'a set" where "scc_of u ≡ {v. u →⇧^{*}v ∧ v →⇧^{*}u}" definition union :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph" where "union G H ≡ ⦇ verts = verts G ∪ verts H, arcs = arcs G ∪ arcs H, tail = tail G, head = head G⦈" definition (in pre_digraph) Union :: "('a,'b) pre_digraph set ⇒ ('a,'b) pre_digraph" where "Union gs = ⦇ verts = (⋃G ∈ gs. verts G), arcs = (⋃G ∈ gs. arcs G), tail = tail G , head = head G ⦈" subsection ‹Compatible Graphs› lemma compatible_tail: assumes "compatible G H" shows "tail G = tail H" using assms by (simp add: fun_eq_iff compatible_def) lemma compatible_head: assumes "compatible G H" shows "head G = head H" using assms by (simp add: fun_eq_iff compatible_def) lemma compatible_cas: assumes "compatible G H" shows "pre_digraph.cas G = pre_digraph.cas H" proof (unfold fun_eq_iff, intro allI) fix u es v show "pre_digraph.cas G u es v = pre_digraph.cas H u es v" using assms by (induct es arbitrary: u) (simp_all add: pre_digraph.cas.simps compatible_head compatible_tail) qed lemma compatible_awalk_verts: assumes "compatible G H" shows "pre_digraph.awalk_verts G = pre_digraph.awalk_verts H" proof (unfold fun_eq_iff, intro allI) fix u es show "pre_digraph.awalk_verts G u es = pre_digraph.awalk_verts H u es" using assms by (induct es arbitrary: u) (simp_all add: pre_digraph.awalk_verts.simps compatible_head compatible_tail) qed lemma compatibleI_with_proj[intro]: shows "compatible (with_proj G) (with_proj H)" by (auto simp: compatible_def) subsection ‹Basic lemmas› lemma (in sym_digraph) graph_symmetric: shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G" using sym_arcs by (auto simp add: symmetric_def sym_def) lemma strongly_connectedI[intro]: assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧^{*}⇘_{G}⇙ v" shows "strongly_connected G" using assms by (simp add: strongly_connected_def) lemma strongly_connectedE[elim]: assumes "strongly_connected G" assumes "(⋀u v. u ∈ verts G ∧ v ∈ verts G ⟹ u →⇧^{*}⇘_{G}⇙ v) ⟹ P" shows "P" using assms by (auto simp add: strongly_connected_def) lemma subgraph_imp_subverts: assumes "subgraph H G" shows "verts H ⊆ verts G" using assms by (simp add: subgraph_def) lemma induced_imp_subgraph: assumes "induced_subgraph H G" shows "subgraph H G" using assms by (simp add: induced_subgraph_def) lemma (in pre_digraph) in_sccs_imp_induced: assumes "c ∈ sccs" shows "induced_subgraph c G" using assms by (auto simp: sccs_def) lemma spanning_tree_imp_tree[dest]: assumes "spanning_tree H G" shows "tree H" using assms by (simp add: spanning_tree_def) lemma tree_imp_connected[dest]: assumes "tree G" shows "connected G" using assms by (simp add: tree_def) lemma spanning_treeI[intro]: assumes "spanning H G" assumes "tree H" shows "spanning_tree H G" using assms by (simp add: spanning_tree_def) lemma spanning_treeE[elim]: assumes "spanning_tree H G" assumes "tree H ∧ spanning H G ⟹ P" shows "P" using assms by (simp add: spanning_tree_def) lemma spanningE[elim]: assumes "spanning H G" assumes "subgraph H G ∧ verts G = verts H ⟹ P" shows "P" using assms by (simp add: spanning_def) lemma (in pre_digraph) in_sccsI[intro]: assumes "induced_subgraph c G" assumes "strongly_connected c" assumes "¬(∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧ verts c ⊂ verts c')" shows "c ∈ sccs" using assms by (auto simp add: sccs_def) lemma (in pre_digraph) in_sccsE[elim]: assumes "c ∈ sccs" assumes "induced_subgraph c G ⟹ strongly_connected c ⟹ ¬ (∃d. induced_subgraph d G ∧ strongly_connected d ∧ verts c ⊂ verts d) ⟹ P" shows "P" using assms by (simp add: sccs_def) lemma subgraphI: assumes "verts H ⊆ verts G" assumes "arcs H ⊆ arcs G" assumes "compatible G H" assumes "wf_digraph H" assumes "wf_digraph G" shows "subgraph H G" using assms by (auto simp add: subgraph_def) lemma subgraphE[elim]: assumes "subgraph H G" obtains "verts H ⊆ verts G" "arcs H ⊆ arcs G" "compatible G H" "wf_digraph H" "wf_digraph G" using assms by (simp add: subgraph_def) lemma induced_subgraphI[intro]: assumes "subgraph H G" assumes "arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}" shows "induced_subgraph H G" using assms unfolding induced_subgraph_def by safe lemma induced_subgraphE[elim]: assumes "induced_subgraph H G" assumes "⟦subgraph H G; arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}⟧ ⟹ P" shows "P" using assms by (auto simp add: induced_subgraph_def) lemma pverts_mk_symmetric[simp]: "pverts (mk_symmetric G) = verts G" and parcs_mk_symmetric: "parcs (mk_symmetric G) = (⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)})" by (auto simp: mk_symmetric_def arcs_ends_conv image_UN) lemma arcs_ends_mono: assumes "subgraph H G" shows "arcs_ends H ⊆ arcs_ends G" using assms by (auto simp add: subgraph_def arcs_ends_conv compatible_tail compatible_head) lemma (in wf_digraph) subgraph_refl: "subgraph G G" by (auto simp: subgraph_def compatible_def) unfold_locales lemma (in wf_digraph) induced_subgraph_refl: "induced_subgraph G G" by (rule induced_subgraphI) (auto simp: subgraph_refl) subsection ‹The underlying symmetric graph of a digraph› lemma (in wf_digraph) wellformed_mk_symmetric[intro]: "pair_wf_digraph (mk_symmetric G)" by unfold_locales (auto simp: parcs_mk_symmetric) lemma (in fin_digraph) pair_fin_digraph_mk_symmetric[intro]: "pair_fin_digraph (mk_symmetric G)" proof - have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv) also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto finally have X: "finite ..." . then show ?thesis by unfold_locales (auto simp: mk_symmetric_def arcs_ends_conv) qed lemma (in digraph) digraph_mk_symmetric[intro]: "pair_digraph (mk_symmetric G)" proof - have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv) also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto finally have "finite ..." . then show ?thesis by unfold_locales (auto simp: mk_symmetric_def arc_to_ends_def dest: no_loops) qed lemma (in wf_digraph) reachable_mk_symmetricI: assumes "u →⇧^{*}v" shows "u →⇧^{*}⇘_{mk_symmetric G}⇙ v" proof - have "arcs_ends G ⊆ parcs (mk_symmetric G)" "(u, v) ∈ rtrancl_on (pverts (mk_symmetric G)) (arcs_ends G)" using assms unfolding reachable_def by (auto simp: parcs_mk_symmetric) then show ?thesis unfolding reachable_def by (auto intro: rtrancl_on_mono) qed lemma (in wf_digraph) adj_mk_symmetric_eq: "symmetric G ⟹ parcs (mk_symmetric G) = arcs_ends G" by (auto simp: parcs_mk_symmetric in_arcs_imp_in_arcs_ends arcs_ends_symmetric) lemma (in wf_digraph) reachable_mk_symmetric_eq: assumes "symmetric G" shows "u →⇧^{*}⇘_{mk_symmetric G}⇙ v ⟷ u →⇧^{*}v" (is "?L ⟷ ?R") using adj_mk_symmetric_eq[OF assms] unfolding reachable_def by auto lemma (in wf_digraph) mk_symmetric_awalk_imp_awalk: assumes sym: "symmetric G" assumes walk: "pre_digraph.awalk (mk_symmetric G) u p v" obtains q where "awalk u q v" proof - interpret S: pair_wf_digraph "mk_symmetric G" .. from walk have "u →⇧^{*}⇘_{mk_symmetric G}⇙ v" by (simp only: S.reachable_awalk) rule then have "u →⇧^{*}v" by (simp only: reachable_mk_symmetric_eq[OF sym]) then show ?thesis by (auto simp: reachable_awalk intro: that) qed lemma symmetric_mk_symmetric: "symmetric (mk_symmetric G)" by (auto simp: symmetric_def parcs_mk_symmetric intro: symI) subsection ‹Subgraphs and Induced Subgraphs› lemma subgraph_trans: assumes "subgraph G H" "subgraph H I" shows "subgraph G I" using assms by (auto simp: subgraph_def compatible_def) text ‹ The @{term digraph} and @{term fin_digraph} properties are preserved under the (inverse) subgraph relation › lemma (in fin_digraph) fin_digraph_subgraph: assumes "subgraph H G" shows "fin_digraph H" proof (intro_locales) from assms show "wf_digraph H" by auto have HG: "arcs H ⊆ arcs G" "verts H ⊆ verts G" using assms by auto then have "finite (verts H)" "finite (arcs H)" using finite_verts finite_arcs by (blast intro: finite_subset)+ then show "fin_digraph_axioms H" by unfold_locales qed lemma (in digraph) digraph_subgraph: assumes "subgraph H G" shows "digraph H" proof fix e assume e: "e ∈ arcs H" with assms show "tail H e ∈ verts H" "head H e ∈ verts H" by (auto simp: subgraph_def intro: wf_digraph.wellformed) from e and assms have "e ∈ arcs H ∩ arcs G" by auto with assms show "tail H e ≠ head H e" using no_loops by (auto simp: subgraph_def compatible_def arc_to_ends_def) next have "arcs H ⊆ arcs G" "verts H ⊆ verts G" using assms by auto then show "finite (arcs H)" "finite (verts H)" using finite_verts finite_arcs by (blast intro: finite_subset)+ next fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H" and eq: "arc_to_ends H e1 = arc_to_ends H e2" with assms have "e1 ∈ arcs H ∩ arcs G" "e2 ∈ arcs H ∩ arcs G" by auto with eq show "e1 = e2" using no_multi_arcs assms by (auto simp: subgraph_def compatible_def arc_to_ends_def) qed lemma (in pre_digraph) adj_mono: assumes "u →⇘_{H}⇙ v" "subgraph H G" shows "u → v" using assms by (blast dest: arcs_ends_mono) lemma (in pre_digraph) reachable_mono: assumes walk: "u →⇧^{*}⇘_{H}⇙ v" and sub: "subgraph H G" shows "u →⇧^{*}v" proof - have "verts H ⊆ verts G" using sub by auto with assms show ?thesis unfolding reachable_def by (metis arcs_ends_mono rtrancl_on_mono) qed text ‹ Arc walks and paths are preserved under the subgraph relation. › lemma (in wf_digraph) subgraph_awalk_imp_awalk: assumes walk: "pre_digraph.awalk H u p v" assumes sub: "subgraph H G" shows "awalk u p v" using assms by (auto simp: pre_digraph.awalk_def compatible_cas) lemma (in wf_digraph) subgraph_apath_imp_apath: assumes path: "pre_digraph.apath H u p v" assumes sub: "subgraph H G" shows "apath u p v" using assms unfolding pre_digraph.apath_def by (auto intro: subgraph_awalk_imp_awalk simp: compatible_awalk_verts) lemma subgraph_mk_symmetric: assumes "subgraph H G" shows "subgraph (mk_symmetric H) (mk_symmetric G)" proof (rule subgraphI) let ?wpms = "λG. mk_symmetric G" from assms have "compatible G H" by auto with assms show "verts (?wpms H) ⊆ verts (?wpms G)" and "arcs (?wpms H) ⊆ arcs (?wpms G)" by (auto simp: parcs_mk_symmetric compatible_head compatible_tail) show "compatible (?wpms G) (?wpms H)" by rule interpret H: pair_wf_digraph "mk_symmetric H" using assms by (auto intro: wf_digraph.wellformed_mk_symmetric) interpret G: pair_wf_digraph "mk_symmetric G" using assms by (auto intro: wf_digraph.wellformed_mk_symmetric) show "wf_digraph (?wpms H)" by unfold_locales show "wf_digraph (?wpms G)" by unfold_locales qed lemma (in fin_digraph) subgraph_in_degree: assumes "subgraph H G" shows "in_degree H v ≤ in_degree G v" proof - have "finite (in_arcs G v)" by auto moreover have "in_arcs H v ⊆ in_arcs G v" using assms by (auto simp: subgraph_def in_arcs_def compatible_head compatible_tail) ultimately show ?thesis unfolding in_degree_def by (rule card_mono) qed lemma (in wf_digraph) subgraph_cycle: assumes "subgraph H G" "pre_digraph.cycle H p " shows "cycle p" proof - from assms have "compatible G H" by auto with assms show ?thesis by (auto simp: pre_digraph.cycle_def compatible_awalk_verts intro: subgraph_awalk_imp_awalk) qed lemma (in wf_digraph) subgraph_del_vert: "subgraph (del_vert u) G" by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales lemma (in wf_digraph) subgraph_del_arc: "subgraph (del_arc a) G" by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales subsection ‹Induced subgraphs› lemma wf_digraphI_induced: assumes "induced_subgraph H G" shows "wf_digraph H" proof - from assms have "compatible G H" by auto with assms show ?thesis by unfold_locales (auto simp: compatible_tail compatible_head) qed lemma (in digraph) digraphI_induced: assumes "induced_subgraph H G" shows "digraph H" proof - interpret W: wf_digraph H using assms by (rule wf_digraphI_induced) from assms have "compatible G H" by auto from assms have arcs: "arcs H ⊆ arcs G" by blast show ?thesis proof from assms have "verts H ⊆ verts G" by blast then show "finite (verts H)" using finite_verts by (rule finite_subset) next from arcs show "finite (arcs H)" using finite_arcs by (rule finite_subset) next fix e assume "e ∈ arcs H" with arcs ‹compatible G H› show "tail H e ≠ head H e" by (auto dest: no_loops simp: compatible_tail[symmetric] compatible_head[symmetric]) next fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H" and ate: "arc_to_ends H e1 = arc_to_ends H e2" with arcs ‹compatible G H› show "e1 = e2" using ate by (auto intro: no_multi_arcs simp: compatible_tail[symmetric] compatible_head[symmetric] arc_to_ends_def) qed qed text ‹Computes the subgraph of @{term G} induced by @{term vs}› definition induce_subgraph :: "('a,'b) pre_digraph ⇒ 'a set ⇒ ('a,'b) pre_digraph" (infix "↾" 67) where "G ↾ vs = ⦇ verts = vs, arcs = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs}, tail = tail G, head = head G ⦈" lemma induce_subgraph_verts[simp]: "verts (G ↾ vs) = vs" by (auto simp add: induce_subgraph_def) lemma induce_subgraph_arcs[simp]: "arcs (G ↾ vs) = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs}" by (auto simp add: induce_subgraph_def) lemma induce_subgraph_tail[simp]: "tail (G ↾ vs) = tail G" by (auto simp: induce_subgraph_def) lemma induce_subgraph_head[simp]: "head (G ↾ vs) = head G" by (auto simp: induce_subgraph_def) lemma compatible_induce_subgraph: "compatible (G ↾ S) G" by (auto simp: compatible_def) lemma (in wf_digraph) induced_induce[intro]: assumes "vs ⊆ verts G" shows "induced_subgraph (G ↾ vs) G" using assms by (intro subgraphI induced_subgraphI) (auto simp: arc_to_ends_def induce_subgraph_def wf_digraph_def compatible_def) lemma (in wf_digraph) wellformed_induce_subgraph[intro]: "wf_digraph (G ↾ vs)" by unfold_locales auto lemma induced_graph_imp_symmetric: assumes "symmetric G" assumes "induced_subgraph H G" shows "symmetric H" proof (unfold symmetric_conv, safe) from assms have "compatible G H" by auto fix e1 assume "e1 ∈ arcs H" then obtain e2 where "tail G e1 = head G e2" "head G e1 = tail G e2" "e2 ∈ arcs G" using assms by (auto simp add: symmetric_conv) moreover then have "e2 ∈ arcs H" using assms and ‹e1 ∈ arcs H› by auto ultimately show "∃e2∈arcs H. tail H e1 = head H e2 ∧ head H e1 = tail H e2" using assms ‹e1 ∈ arcs H› ‹compatible G H› by (auto simp: compatible_head compatible_tail) qed lemma (in sym_digraph) induced_graph_imp_graph: assumes "induced_subgraph H G" shows "sym_digraph H" proof (rule wf_digraph.sym_digraphI) from assms show "wf_digraph H" by (rule wf_digraphI_induced) next show "symmetric H" using assms sym_arcs by (auto intro: induced_graph_imp_symmetric) qed lemma (in wf_digraph) induce_reachable_preserves_paths: assumes "u →⇧^{*}⇘_{G}⇙ v" shows "u →⇧^{*}⇘_{G ↾ {w. u →⇧*⇘G⇙ w}}⇙ v" using assms proof induct case base then show ?case by (auto simp: reachable_def) next case (step u w) interpret iG: wf_digraph "G ↾ {w. u →⇧^{*}⇘_{G}⇙ w}" by (rule wellformed_induce_subgraph) from ‹u → w› have "u →⇘_{G ↾ {wa. u →⇧*⇘G⇙ wa}}⇙ w" by (auto simp: arcs_ends_conv reachable_def intro: wellformed rtrancl_on_into_rtrancl_on) then have "u →⇧^{*}⇘_{G ↾ {wa. u →⇧*⇘G⇙ wa}}⇙ w" by (rule iG.reachable_adjI) moreover from step have "{x. w →⇧^{*}x} ⊆ {x. u →⇧^{*}x}" by (auto intro: adj_reachable_trans) then have "subgraph (G ↾ {wa. w →⇧^{*}wa}) (G ↾ {wa. u →⇧^{*}wa})" by (intro subgraphI) (auto simp: arcs_ends_conv compatible_def) then have "w →⇧^{*}⇘_{G ↾ {wa. u →⇧* wa}}⇙ v" by (rule iG.reachable_mono[rotated]) fact ultimately show ?case by (rule iG.reachable_trans) qed lemma induce_subgraph_ends[simp]: "arc_to_ends (G ↾ S) = arc_to_ends G" by (auto simp: arc_to_ends_def) lemma dominates_induce_subgraphD: assumes "u →⇘_{G ↾ S}⇙ v" shows "u →⇘_{G}⇙ v" using assms by (auto simp: arcs_ends_def intro: rev_image_eqI) context wf_digraph begin lemma reachable_induce_subgraphD: assumes "u →⇧^{*}⇘_{G ↾ S}⇙ v" "S ⊆ verts G" shows "u →⇧^{*}⇘_{G}⇙ v" proof - interpret GS: wf_digraph "G ↾ S" by auto show ?thesis using assms by induct (auto dest: dominates_induce_subgraphD intro: adj_reachable_trans) qed lemma dominates_induce_ss: assumes "u →⇘_{G ↾ S}⇙ v" "S ⊆ T" shows "u →⇘_{G ↾ T}⇙ v" using assms by (auto simp: arcs_ends_def) lemma reachable_induce_ss: assumes "u →⇧^{*}⇘_{G ↾ S}⇙ v" "S ⊆ T" shows "u →⇧^{*}⇘_{G ↾ T}⇙ v" using assms unfolding reachable_def by induct (auto intro: dominates_induce_ss converse_rtrancl_on_into_rtrancl_on) lemma awalk_verts_induce: "pre_digraph.awalk_verts (G ↾ S) = awalk_verts" proof (intro ext) fix u p show "pre_digraph.awalk_verts (G ↾ S) u p = awalk_verts u p" by (induct p arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps) qed lemma (in -) cas_subset: assumes "pre_digraph.cas G u p v" "subgraph G H" shows "pre_digraph.cas H u p v" using assms by (induct p arbitrary: u) (auto simp: pre_digraph.cas.simps subgraph_def compatible_def) lemma cas_induce: assumes "cas u p v" "set (awalk_verts u p) ⊆ S" shows "pre_digraph.cas (G ↾ S) u p v" using assms proof (induct p arbitrary: u S) case Nil then show ?case by (auto simp: pre_digraph.cas.simps) next case (Cons a as) have "pre_digraph.cas (G ↾ set (awalk_verts (head G a) as)) (head G a) as v" using Cons by auto then have "pre_digraph.cas (G ↾ S) (head G a) as v" using ‹_ ⊆ S› by (rule_tac cas_subset) (auto simp: subgraph_def compatible_def) then show ?case using Cons by (auto simp: pre_digraph.cas.simps) qed lemma awalk_induce: assumes "awalk u p v" "set (awalk_verts u p) ⊆ S" shows "pre_digraph.awalk (G ↾ S) u p v" proof - interpret GS: wf_digraph "G ↾ S" by auto show ?thesis using assms by (auto simp: pre_digraph.awalk_def cas_induce GS.cas_induce set_awalk_verts) qed lemma subgraph_induce_subgraphI: assumes "V ⊆ verts G" shows "subgraph (G ↾ V) G" by (metis assms induced_imp_subgraph induced_induce) end lemma induced_subgraphI': assumes subg:"subgraph H G" assumes max: "⋀H'. subgraph H' G ⟹ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H)" shows "induced_subgraph H G" proof - interpret H: wf_digraph H using ‹subgraph H G› .. define H' where "H' = G ↾ verts H" then have H'_props: "subgraph H' G" "verts H' = verts H" using subg by (auto intro: wf_digraph.subgraph_induce_subgraphI) moreover have "arcs H' = arcs H" proof show "arcs H' ⊆ arcs H" using max H'_props by auto show "arcs H ⊆ arcs H'" using subg by (auto simp: H'_def compatible_def) qed then show "induced_subgraph H G" by (auto simp: induced_subgraph_def H'_def subg) qed lemma (in pre_digraph) induced_subgraph_altdef: "induced_subgraph H G ⟷ subgraph H G ∧ (∀H'. subgraph H' G ⟶ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H))" (is "?L ⟷ ?R") proof - { fix H' :: "('a,'b) pre_digraph" assume A: "verts H' = verts H" "subgraph H' G" interpret H': wf_digraph H' using ‹subgraph H' G› .. from ‹subgraph H' G› have comp: "tail G = tail H'" "head G = head H'" by (auto simp: compatible_def) then have "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H" "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H" by (auto dest: H'.wellformed simp: A) then have "arcs H' ⊆ {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}" using ‹subgraph H' G› by (auto simp: subgraph_def comp A(1)[symmetric]) } then show ?thesis using induced_subgraphI'[of H G] by (auto simp: induced_subgraph_def) qed subsection ‹Unions of Graphs› lemma verts_union[simp]: "verts (union G H) = verts G ∪ verts H" and arcs_union[simp]: "arcs (union G H) = arcs G ∪ arcs H" and tail_union[simp]: "tail (union G H) = tail G" and head_union[simp]: "head (union G H) = head G" by (auto simp: union_def) lemma wellformed_union: assumes "wf_digraph G" "wf_digraph H" "compatible G H" shows "wf_digraph (union G H)" using assms by unfold_locales (auto simp: union_def compatible_tail compatible_head dest: wf_digraph.wellformed) lemma subgraph_union_iff: assumes "wf_digraph H1" "wf_digraph H2" "compatible H1 H2" shows "subgraph (union H1 H2) G ⟷ subgraph H1 G ∧ subgraph H2 G" using assms by (fastforce simp: compatible_def intro!: subgraphI wellformed_union) lemma subgraph_union[intro]: assumes "subgraph H1 G" "compatible H1 G" assumes "subgraph H2 G" "compatible H2 G" shows "subgraph (union H1 H2) G" proof - from assms have "wf_digraph (union H1 H2)" by (auto intro: wellformed_union simp: compatible_def) with assms show ?thesis by (auto simp add: subgraph_def union_def arc_to_ends_def compatible_def) qed lemma union_fin_digraph: assumes "fin_digraph G" "fin_digraph H" "compatible G H" shows "fin_digraph (union G H)" proof intro_locales interpret G: fin_digraph G by (rule assms) interpret H: fin_digraph H by (rule assms) show "wf_digraph (union G H)" using assms by (intro wellformed_union) intro_locales show "fin_digraph_axioms (union G H)" using assms by unfold_locales (auto simp: union_def) qed lemma subgraphs_of_union: assumes "wf_digraph G" "wf_digraph G'" "compatible G G'" shows "subgraph G (union G G')" and "subgraph G' (union G G')" using assms by (auto intro!: subgraphI wellformed_union simp: compatible_def) subsection ‹Maximal Subgraphs› lemma (in pre_digraph) max_subgraph_mp: assumes "max_subgraph Q x" "⋀x. P x ⟹ Q x" "P x" shows "max_subgraph P x" using assms by (auto simp: max_subgraph_def) lemma (in pre_digraph) max_subgraph_prop: "max_subgraph P x ⟹ P x" by (simp add: max_subgraph_def) lemma (in pre_digraph) max_subgraph_subg_eq: assumes "max_subgraph P H1" "max_subgraph P H2" "subgraph H1 H2" shows "H1 = H2" using assms by (auto simp: max_subgraph_def) lemma subgraph_induce_subgraphI2: assumes "subgraph H G" shows "subgraph H (G ↾ verts H)" using assms by (auto simp: subgraph_def compatible_def wf_digraph.wellformed wf_digraph.wellformed_induce_subgraph) definition arc_mono :: "(('a,'b) pre_digraph ⇒ bool) ⇒ bool" where "arc_mono P ≡ (∀H1 H2. P H1 ∧ subgraph H1 H2 ∧ verts H1 = verts H2 ⟶ P H2)" lemma (in pre_digraph) induced_subgraphI_arc_mono: assumes "max_subgraph P H" assumes "arc_mono P" shows "induced_subgraph H G" proof - interpret wf_digraph G using assms by (auto simp: max_subgraph_def) have "subgraph H (G ↾ verts H)" "subgraph (G ↾ verts H) G" "verts H = verts (G ↾ verts H)" "P H" using assms by (auto simp: max_subgraph_def subgraph_induce_subgraphI2 subgraph_induce_subgraphI) moreover then have "P (G ↾ verts H)" using assms by (auto simp: arc_mono_def) ultimately have "max_subgraph P (G ↾ verts H)" using assms by (auto simp: max_subgraph_def) metis then have "H = G ↾ verts H" using ‹max_subgraph P H› ‹subgraph H _› by (intro max_subgraph_subg_eq) show ?thesis using assms by (subst ‹H = _›) (auto simp: max_subgraph_def) qed lemma (in pre_digraph) induced_subgraph_altdef2: "induced_subgraph H G ⟷ max_subgraph (λH'. verts H' = verts H) H" (is "?L ⟷ ?R") proof assume ?L moreover { fix H' assume "induced_subgraph H G" "subgraph H H'" "H ≠ H'" then have "¬(subgraph H' G ∧ verts H' = verts H)" by (auto simp: induced_subgraph_altdef compatible_def elim!: allE[where x=H']) } ultimately show "max_subgraph (λH'. verts H' = verts H) H" by (auto simp: max_subgraph_def) next assume ?R moreover have "arc_mono (λH'. verts H' = verts H)" by (auto simp: arc_mono_def) ultimately show ?L by (rule induced_subgraphI_arc_mono) qed (*XXX*) lemma (in pre_digraph) max_subgraphI: assumes "P x" "subgraph x G" "⋀y. ⟦x ≠ y; subgraph x y; subgraph y G⟧ ⟹ ¬P y" shows "max_subgraph P x" using assms by (auto simp: max_subgraph_def) lemma (in pre_digraph) subgraphI_max_subgraph: "max_subgraph P x ⟹ subgraph x G" by (simp add: max_subgraph_def) subsection ‹Connected and Strongly Connected Graphs› context wf_digraph begin lemma in_sccs_verts_conv_reachable: "S ∈ sccs_verts ⟷ S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧^{*}⇘_{G}⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧^{*}⇘_{G}⇙ v ∨ ¬v →⇧^{*}⇘_{G}⇙ u)" by (simp add: sccs_verts_def) lemma sccs_verts_disjoint: assumes "S ∈ sccs_verts" "T ∈ sccs_verts" "S ≠ T" shows "S ∩ T = {}" using assms unfolding in_sccs_verts_conv_reachable by safe meson+ lemma strongly_connected_spanning_imp_strongly_connected: assumes "spanning H G" assumes "strongly_connected H" shows "strongly_connected G" proof (unfold strongly_connected_def, intro ballI conjI) from assms show "verts G ≠ {}" unfolding strongly_connected_def spanning_def by auto next fix u v assume "u ∈ verts G" and "v ∈ verts G" then have "u →⇧^{*}⇘_{H}⇙ v" "subgraph H G" using assms by (auto simp add: strongly_connected_def) then show "u →⇧^{*}v" by (rule reachable_mono) qed lemma strongly_connected_imp_induce_subgraph_strongly_connected: assumes subg: "subgraph H G" assumes sc: "strongly_connected H" shows "strongly_connected (G ↾ (verts H))" proof - let ?is_H = "G ↾ (verts H)" interpret H: wf_digraph H using subg by (rule subgraphE) interpret GrH: wf_digraph "?is_H" by (rule wellformed_induce_subgraph) have "verts H ⊆ verts G" using assms by auto have "subgraph H (G ↾ verts H)" using subg by (intro subgraphI) (auto simp: compatible_def) then show ?thesis using induced_induce[OF ‹verts H ⊆ verts G›] and sc GrH.strongly_connected_spanning_imp_strongly_connected unfolding spanning_def by auto qed lemma in_sccs_vertsI_sccs: assumes "S ∈ verts ` sccs" shows "S ∈ sccs_verts" unfolding sccs_verts_def proof (intro CollectI conjI allI ballI impI) show "S ≠ {}" using assms by (auto simp: sccs_verts_def sccs_def strongly_connected_def) from assms have sc: "strongly_connected (G ↾ S)" "S ⊆ verts G" apply (auto simp: sccs_verts_def sccs_def) by (metis induced_imp_subgraph subgraphE wf_digraph.strongly_connected_imp_induce_subgraph_strongly_connected) { fix u v assume A: "u ∈ S" "v ∈ S" with sc have "u →⇧^{*}⇘_{G ↾ S}⇙ v" by auto then show "u →⇧^{*}⇘_{G}⇙ v" using ‹S ⊆ verts G› by (rule reachable_induce_subgraphD) next fix u v assume A: "u ∈ S" "v ∉ S" { assume B: "u →⇧^{*}⇘_{G}⇙ v" "v →⇧^{*}⇘_{G}⇙ u" from B obtain p_uv where p_uv: "awalk u p_uv v" by (metis reachable_awalk) from B obtain p_vu where p_vu: "awalk v p_vu u" by (metis reachable_awalk) define T where "T = S ∪ set (awalk_verts u p_uv) ∪ set (awalk_verts v p_vu)" have "S ⊆ T" by (auto simp: T_def) have "v ∈ T" using p_vu by (auto simp: T_def set_awalk_verts) then have "T ≠ S" using ‹v ∉ S› by auto interpret T: wf_digraph "G ↾ T" by auto from p_uv have T_p_uv: "T.awalk u p_uv v" by (rule awalk_induce) (auto simp: T_def) from p_vu have T_p_vu: "T.awalk v p_vu u" by (rule awalk_induce) (auto simp: T_def) have uv_reach: "u →⇧^{*}⇘_{G ↾ T}⇙ v" "v →⇧^{*}⇘_{G ↾ T}⇙ u" using T_p_uv T_p_vu A by (metis T.reachable_awalk)+ { fix x y assume "x ∈ S" "y ∈ S" then have "x →⇧^{*}⇘_{G ↾ S}⇙ y" "y →⇧^{*}⇘_{G ↾ S}⇙ x" using sc by auto then have "x →⇧^{*}⇘_{G ↾ T}⇙ y" "y →⇧^{*}⇘_{G ↾ T}⇙ x" using ‹S ⊆ T› by (auto intro: reachable_induce_ss) } note A1 = this { fix x assume "x ∈ T" moreover { assume "x ∈ S" then have "x →⇧^{*}⇘_{G ↾ T}⇙ v" using uv_reach A1 A by (auto intro: T.reachable_trans[rotated]) } moreover { assume "x ∈ set (awalk_verts u p_uv)" then have "x →⇧^{*}⇘_{G ↾ T}⇙ v" using T_p_uv by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_to) } moreover { assume "x ∈ set (awalk_verts v p_vu)" then have "x →⇧^{*}⇘_{G ↾ T}⇙ v" using T_p_vu by (rule_tac T.reachable_trans) (auto simp: uv_reach awalk_verts_induce dest: T.awalk_verts_reachable_to) } ultimately have "x →⇧^{*}⇘_{G ↾ T}⇙ v" by (auto simp: T_def) } note xv_reach = this { fix x assume "x ∈ T" moreover { assume "x ∈ S" then have "v →⇧^{*}⇘_{G ↾ T}⇙ x" using uv_reach A1 A by (auto intro: T.reachable_trans) } moreover { assume "x ∈ set (awalk_verts v p_vu)" then have "v →⇧^{*}⇘_{G ↾ T}⇙ x" using T_p_vu by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_from) } moreover { assume "x ∈ set (awalk_verts u p_uv)" then have "v →⇧^{*}⇘_{G ↾ T}⇙ x" using T_p_uv by (rule_tac T.reachable_trans[rotated]) (auto intro: T.awalk_verts_reachable_from uv_reach simp: awalk_verts_induce) } ultimately have "v →⇧^{*}⇘_{G ↾ T}⇙ x" by (auto simp: T_def) } note vx_reach = this { fix x y assume "x ∈ T" "y ∈ T" then have "x →⇧^{*}⇘_{G ↾ T}⇙ y" using xv_reach vx_reach by (blast intro: T.reachable_trans) } then have "strongly_connected (G ↾ T)" using ‹S ≠ {}› ‹S ⊆ T› by auto moreover have "induced_subgraph (G ↾ T) G" using ‹S ⊆ verts G› by (auto simp: T_def intro: awalk_verts_reachable_from p_uv p_vu reachable_in_verts(2)) ultimately have "∃T. induced_subgraph (G ↾ T) G ∧ strongly_connected (G ↾ T) ∧ verts (G ↾ S) ⊂ verts (G ↾ T)" using ‹S ⊆ T› ‹T ≠ S› by auto then have "G ↾ S ∉ sccs" unfolding sccs_def by blast then have "S ∉ verts ` sccs" by (metis (erased, hide_lams) ‹S ⊆ T› ‹T ≠ S› ‹induced_subgraph (G ↾ T) G› ‹strongly_connected (G ↾ T)› dual_order.order_iff_strict image_iff in_sccsE induce_subgraph_verts) then have False using assms by metis } then show "¬u →⇧^{*}⇘_{G}⇙ v ∨ ¬v →⇧^{*}⇘_{G}⇙ u" by metis } qed end lemma arc_mono_strongly_connected[intro,simp]: "arc_mono strongly_connected" by (auto simp: arc_mono_def) (metis spanning_def subgraphE wf_digraph.strongly_connected_spanning_imp_strongly_connected) lemma (in pre_digraph) sccs_altdef2: "sccs = {H. max_subgraph strongly_connected H}" (is "?L = ?R") proof - { fix H H' :: "('a, 'b) pre_digraph" assume a1: "strongly_connected H'" assume a2: "induced_subgraph H' G" assume a3: "max_subgraph strongly_connected H" assume a4: "verts H ⊆ verts H'" have sg: "subgraph H G" and ends_G: "tail G = tail H " "head G = head H" using a3 by (auto simp: max_subgraph_def compatible_def) then interpret H: wf_digraph H by blast have "arcs H ⊆ arcs H'" using a2 a4 sg by (fastforce simp: ends_G) then have "H = H'" using a1 a2 a3 a4 by (metis (no_types) compatible_def induced_imp_subgraph max_subgraph_def subgraph_def) } note X = this { fix H assume a1: "induced_subgraph H G" assume a2: "strongly_connected H" assume a3: "∀H'. strongly_connected H' ⟶ induced_subgraph H' G ⟶ ¬ verts H ⊂ verts H'" interpret G: wf_digraph G using a1 by auto { fix y assume "H ≠ y" and subg: "subgraph H y" "subgraph y G" then have "verts H ⊂ verts y" using a1 by (auto simp: induced_subgraph_altdef2 max_subgraph_def) then have "¬strongly_connected y" using subg a1 a2 a3[THEN spec, of "G ↾ verts y"] by (auto simp: G.induced_induce G.strongly_connected_imp_induce_subgraph_strongly_connected) } then have "max_subgraph strongly_connected H" using a1 a2 by (auto intro: max_subgraphI) } note Y = this show ?thesis unfolding sccs_def by (auto dest: max_subgraph_prop X intro: induced_subgraphI_arc_mono Y) qed locale max_reachable_set = wf_digraph + fixes S assumes S_in_sv: "S ∈ sccs_verts" begin lemma reach_in: "⋀u v. ⟦u ∈ S; v ∈ S⟧ ⟹ u →⇧^{*}⇘_{G}⇙ v" and not_reach_out: "⋀u v. ⟦u ∈ S; v ∉ S⟧ ⟹ ¬u →⇧^{*}⇘_{G}⇙ v ∨ ¬v →⇧^{*}⇘_{G}⇙ u" and not_empty: "S ≠ {}" using S_in_sv by (auto simp: sccs_verts_def) lemma reachable_induced: assumes conn: "u ∈ S" "v ∈ S" "u →⇧^{*}⇘_{G}⇙ v" shows "u →⇧^{*}⇘_{G ↾ S}⇙ v" proof - let ?H = "G ↾ S" have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts) then have "induced_subgraph ?H G" by (rule induced_induce) then interpret H: wf_digraph ?H by (rule wf_digraphI_induced) from conn obtain p where p: "awalk u p v" by (metis reachable_awalk) show ?thesis proof (cases "set p ⊆ arcs (G ↾ S)") case True with p conn have "H.awalk u p v" by (auto simp: pre_digraph.awalk_def compatible_cas[OF compatible_induce_subgraph]) then show ?thesis by (metis H.reachable_awalk) next case False then obtain a where "a ∈ set p" "a ∉ arcs (G ↾ S)" by auto moreover then have "tail G a ∉ S ∨ head G a ∉ S" using p by auto ultimately obtain w where "w ∈ set (awalk_verts u p)" "w ∉ S" using p by (auto simp: set_awalk_verts) then have "u →⇧^{*}⇘_{G}⇙ w" "w →⇧^{*}⇘_{G}⇙ v" using p by (auto intro: awalk_verts_reachable_from awalk_verts_reachable_to) moreover have "v →⇧^{*}⇘_{G}⇙ u" using conn reach_in by auto ultimately have "u →⇧^{*}⇘_{G}⇙ w" "w →⇧^{*}⇘_{G}⇙ u" by (auto intro: reachable_trans) with ‹w ∉ S› conn not_reach_out have False by blast then show ?thesis .. qed qed lemma strongly_connected: shows "strongly_connected (G ↾ S)" using not_empty by (intro strongly_connectedI) (auto intro: reachable_induced reach_in) lemma induced_in_sccs: "G ↾ S ∈ sccs" proof - let ?H = "G ↾ S" have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts) then have "induced_subgraph ?H G" by (rule induced_induce) then interpret H: wf_digraph ?H by (rule wf_digraphI_induced) { fix T assume "S ⊂ T" "T ⊆ verts G" "strongly_connected (G ↾ T)" from ‹S ⊂ T› obtain v where "v ∈ T" "v ∉ S" by auto from not_empty obtain u where "u ∈ S" by auto then have "u ∈ T" using ‹S ⊂ T› by auto from ‹u ∈ S› ‹v ∉ S› have "¬u →⇧^{*}⇘_{G}⇙ v ∨ ¬v →⇧^{*}⇘_{G}⇙ u" by (rule not_reach_out) moreover from ‹strongly_connected _› have "u →⇧^{*}⇘_{G ↾ T}⇙ v" "v →⇧^{*}⇘_{G ↾ T}⇙ u" using ‹v ∈ T› ‹u ∈ T› by (auto simp: strongly_connected_def) then have "u →⇧^{*}⇘_{G}⇙ v" "v →⇧^{*}⇘_{G}⇙ u" using ‹T ⊆ verts G› by (auto dest: reachable_induce_subgraphD) ultimately have False by blast } note psuper_not_sc = this have "¬ (∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧ verts (G ↾ S) ⊂ verts c')" by (metis induce_subgraph_verts induced_imp_subgraph psuper_not_sc subgraphE strongly_connected_imp_induce_subgraph_strongly_connected) with ‹S ⊆ _› not_empty show "?H ∈ sccs" by (intro in_sccsI induced_induce strongly_connected) qed end context wf_digraph begin lemma in_verts_sccsD_sccs: assumes "S ∈ sccs_verts" shows "G ↾ S ∈ sccs" proof - from assms interpret max_reachable_set by unfold_locales show ?thesis by (auto simp: sccs_verts_def intro: induced_in_sccs) qed lemma sccs_verts_conv: "sccs_verts = verts ` sccs" by (auto intro: in_sccs_vertsI_sccs rev_image_eqI dest: in_verts_sccsD_sccs) lemma induce_eq_iff_induced: assumes "induced_subgraph H G" shows "G ↾ verts H = H" using assms by (auto simp: induced_subgraph_def induce_subgraph_def compatible_def) lemma sccs_conv_sccs_verts: "sccs = induce_subgraph G ` sccs_verts" by (auto intro!: rev_image_eqI in_sccs_vertsI_sccs dest: in_verts_sccsD_sccs simp: sccs_def induce_eq_iff_induced) end lemma connected_conv: shows "connected G ⟷ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. (u,v) ∈ rtrancl_on (verts G) ((arcs_ends G)⇧^{s}))" proof - have "symcl (arcs_ends G) = parcs (mk_symmetric G)" by (auto simp: parcs_mk_symmetric symcl_def arcs_ends_conv) then show ?thesis by (auto simp: connected_def strongly_connected_def reachable_def) qed lemma (in wf_digraph) symmetric_connected_imp_strongly_connected: assumes "symmetric G" "connected G" shows "strongly_connected G" proof from ‹connected G› show "verts G ≠ {}" unfolding connected_def strongly_connected_def by auto next from ‹connected G› have sc_mks: "strongly_connected (mk_symmetric G)" unfolding connected_def by simp fix u v assume "u ∈ verts G" "v ∈ verts G" with sc_mks have "u →⇧^{*}⇘_{mk_symmetric G}⇙ v" unfolding strongly_connected_def by auto then show "u →⇧^{*}v" using assms by (simp only: reachable_mk_symmetric_eq) qed lemma (in wf_digraph) connected_spanning_imp_connected: assumes "spanning H G" assumes "connected H" shows "connected G" proof (unfold connected_def strongly_connected_def, intro conjI ballI) from assms show "verts (mk_symmetric G )≠ {}" unfolding spanning_def connected_def strongly_connected_def by auto next fix u v assume "u ∈ verts (mk_symmetric G)" and "v ∈ verts (mk_symmetric G)" then have "u ∈ pverts (mk_symmetric H)" and "v ∈ pverts (mk_symmetric H)" using ‹spanning H G› by (auto simp: mk_symmetric_def) with ‹connected H› have "u →⇧^{*}⇘_{with_proj (mk_symmetric H)}⇙ v" "subgraph (mk_symmetric H) (mk_symmetric G)" using ‹spanning H G› unfolding connected_def by (auto simp: spanning_def dest: subgraph_mk_symmetric) then show "u →⇧^{*}⇘_{mk_symmetric G}⇙ v" by (rule pre_digraph.reachable_mono) qed lemma (in wf_digraph) spanning_tree_imp_connected: assumes "spanning_tree H G" shows "connected G" using assms by (auto intro: connected_spanning_imp_connected) term "LEAST x. P x" lemma (in sym_digraph) induce_reachable_is_in_sccs: assumes "u ∈ verts G" shows "(G ↾ {v. u →⇧^{*}v}) ∈ sccs" proof - let ?c = "(G ↾ {v. u →⇧^{*}v})" have isub_c: "induced_subgraph ?c G" by (auto elim: reachable_in_vertsE) then interpret c: wf_digraph ?c by (rule wf_digraphI_induced) have sym_c: "symmetric (G ↾ {v. u →⇧^{*}v})" using sym_arcs isub_c by (rule induced_graph_imp_symmetric) note ‹induced_subgraph ?c G› moreover have "strongly_connected ?c" proof (rule strongly_connectedI) show "verts ?c ≠ {}" using assms by auto next fix v w assume l_assms: "v ∈ verts ?c" "w ∈ verts ?c" have "u →⇧^{*}⇘_{G ↾ {v. u →⇧* v}}⇙ v" using l_assms by (intro induce_reachable_preserves_paths) auto then have "v →⇧^{*}⇘_{G ↾ {v. u →⇧* v}}⇙ u" by (rule symmetric_reachable[OF sym_c]) also have "u →⇧^{*}⇘_{G ↾ {v. u →⇧* v}}⇙ w" using l_assms by (intro induce_reachable_preserves_paths) auto finally show "v →⇧^{*}⇘_{G ↾ {v. u →⇧* v}}⇙ w" . qed moreover have "¬(∃d. induced_subgraph d G ∧ strongly_connected d ∧ verts ?c ⊂ verts d)" proof assume "∃d. induced_subgraph d G ∧ strongly_connected d ∧ verts ?c ⊂ verts d" then obtain d where "induced_subgraph d G" "strongly_connected d" "verts ?c ⊂ verts d" by auto then obtain v where "v ∈ verts d" and "v ∉ verts ?c" by auto have "u ∈ verts ?c" using ‹u ∈ verts G› by auto then have "u ∈ verts d" using ‹verts ?c ⊂ verts d› by auto then have "u →⇧^{*}⇘_{d}⇙ v" using ‹strongly_connected d› ‹u ∈ verts d› ‹v ∈ verts d› by auto then have "u →⇧^{*}v" using ‹induced_subgraph d G› by (auto intro: pre_digraph.reachable_mono) then have "v ∈ verts ?c" by (auto simp: reachable_awalk) then show False using ‹v ∉ verts ?c› by auto qed ultimately show ?thesis unfolding sccs_def by auto qed lemma induced_eq_verts_imp_eq: assumes "induced_subgraph G H" assumes "induced_subgraph G' H" assumes "verts G = verts G'" shows "G = G'" using assms by (auto simp: induced_subgraph_def subgraph_def compatible_def) lemma (in pre_digraph) in_sccs_subset_imp_eq: assumes "c ∈ sccs" assumes "d ∈ sccs" assumes "verts c ⊆ verts d" shows "c = d" using assms by (blast intro: induced_eq_verts_imp_eq) context wf_digraph begin lemma connectedI: assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧^{*}⇘_{mk_symmetric G}⇙ v" shows "connected G" using assms by (auto simp: connected_def) lemma connected_awalkE: assumes "connected G" "u ∈ verts G" "v ∈ verts G" obtains p where "pre_digraph.awalk (mk_symmetric G) u p v" proof - interpret sG: pair_wf_digraph "mk_symmetric G" .. from assms have "u →⇧^{*}⇘_{mk_symmetric G}⇙ v" by (auto simp: connected_def) then obtain p where "sG.awalk u p v" by (auto simp: sG.reachable_awalk) then show ?thesis .. qed lemma inj_on_verts_sccs: "inj_on verts sccs" by (rule inj_onI) (metis in_sccs_imp_induced induced_eq_verts_imp_eq) lemma card_sccs_verts: "card sccs_verts = card sccs" by (auto simp: sccs_verts_conv intro: inj_on_verts_sccs card_image) end lemma strongly_connected_non_disj: assumes wf: "wf_digraph G" "wf_digraph H" "compatible G H" assumes sc: "strongly_connected G" "strongly_connected H" assumes not_disj: "verts G ∩ verts H ≠ {}" shows "strongly_connected (union G H)" proof from sc show "verts (union G H) ≠ {}" unfolding strongly_connected_def by simp next let ?x = "union G H" fix u v w assume "u ∈ verts ?x" and "v ∈ verts ?x" obtain w where w_in_both: "w ∈ verts G" "w ∈ verts H" using not_disj by auto interpret x: wf_digraph ?x by (rule wellformed_union) fact+ have subg: "subgraph G ?x" "subgraph H ?x" by (rule subgraphs_of_union[OF _ _ ], fact+)+ have reach_uw: "u →⇧^{*}⇘_{?x}⇙ w" using ‹u ∈ verts ?x› subg w_in_both sc by (auto intro: pre_digraph.reachable_mono) also have reach_wv: "w →⇧^{*}⇘_{?x}⇙ v" using ‹v ∈ verts ?x› subg w_in_both sc by (auto intro: pre_digraph.reachable_mono) finally (x.reachable_trans) show "u →⇧^{*}⇘_{?x}⇙ v" . qed context wf_digraph begin lemma scc_disj: assumes scc: "c ∈ sccs" "d ∈ sccs" assumes "c ≠ d" shows "verts c ∩ verts d = {}" proof (rule ccontr) assume contr: "¬?thesis" let ?x = "union c d" have comp1: "compatible G c" "compatible G d" using scc by (auto simp: sccs_def) then have comp: "compatible c d" by (auto simp: compatible_def) have wf: "wf_digraph c" "wf_digraph d" and sc: "strongly_connected c" "strongly_connected d" using scc by (auto intro: in_sccs_imp_induced) have "compatible c d" using comp by (auto simp: sccs_def compatible_def) from wf comp sc have union_conn: "strongly_connected ?x" using contr by (rule strongly_connected_non_disj) have sg: "subgraph ?x G" using scc comp1 by (intro subgraph_union) (auto simp: compatible_def) then have v_cd: "verts c ⊆ verts G" "verts d ⊆ verts G" by (auto elim!: subgraphE) have "wf_digraph ?x" by (rule wellformed_union) fact+ with v_cd sg union_conn have induce_subgraph_conn: "strongly_connected (G ↾ verts ?x)" "induced_subgraph (G ↾ verts ?x) G" by - (intro strongly_connected_imp_induce_subgraph_strongly_connected, auto simp: subgraph_union_iff) from assms have "¬verts c ⊆ verts d" and "¬ verts d ⊆ verts c" by (metis in_sccs_subset_imp_eq)+ then have psub: "verts c ⊂ verts ?x" by (auto simp: union_def) then show False using induce_subgraph_conn by (metis ‹c ∈ sccs› in_sccsE induce_subgraph_verts) qed lemma in_sccs_verts_conv: "S ∈ sccs_verts ⟷ G ↾ S ∈ sccs" by (auto simp: sccs_verts_conv intro: rev_image_eqI) (metis in_sccs_imp_induced induce_subgraph_verts induced_eq_verts_imp_eq induced_imp_subgraph induced_induce subgraphE) end lemma (in wf_digraph) in_scc_of_self: "u ∈ verts G ⟹ u ∈ scc_of u" by (auto simp: scc_of_def) lemma (in wf_digraph) scc_of_empty_conv: "scc_of u = {} ⟷ u ∉ verts G" using in_scc_of_self by (auto simp: scc_of_def reachable_in_verts) lemma (in wf_digraph) scc_of_in_sccs_verts: assumes "u ∈ verts G" shows "scc_of u ∈ sccs_verts" using assms by (auto simp: in_sccs_verts_conv_reachable scc_of_def intro: reachable_trans exI[where x=u]) lemma (in wf_digraph) sccs_verts_subsets: "S ∈ sccs_verts ⟹ S ⊆ verts G" by (auto simp: sccs_verts_conv) lemma (in fin_digraph) finite_sccs_verts: "finite sccs_verts" proof - have "finite (Pow (verts G))" by auto moreover with sccs_verts_subsets have "sccs_verts ⊆ Pow (verts G)" by auto ultimately show ?thesis by (rule rev_finite_subset) qed lemma (in wf_digraph) sccs_verts_conv_scc_of: "sccs_verts = scc_of ` verts G" (is "?L = ?R") proof (intro set_eqI iffI) fix S assume "S ∈ ?R" then show "S ∈ ?L" by (auto simp: in_sccs_verts_conv_reachable scc_of_empty_conv) (auto simp: scc_of_def intro: reachable_trans) next fix S assume "S ∈ ?L" moreover then obtain u where "u ∈ S" by (auto simp: in_sccs_verts_conv_reachable) moreover then have "u ∈ verts G" using ‹S ∈ ?L› by (metis sccs_verts_subsets subsetCE) then have "scc_of u ∈ sccs_verts" "u ∈ scc_of u" by (auto intro: scc_of_in_sccs_verts in_scc_of_self) ultimately have "scc_of u = S" using sccs_verts_disjoint by blast then show "S ∈ ?R" using ‹scc_of u ∈ _› ‹u ∈ verts G› by auto qed lemma (in sym_digraph) scc_ofI_reachable: assumes "u →⇧^{*}v" shows "u ∈ scc_of v" using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs]) lemma (in sym_digraph) scc_ofI_reachable': assumes "v →⇧^{*}u" shows "u ∈ scc_of v" using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs]) lemma (in sym_digraph) scc_ofI_awalk: assumes "awalk u p v" shows "u ∈ scc_of v" using assms by (metis reachable_awalk scc_ofI_reachable) lemma (in sym_digraph) scc_ofI_apath: assumes "apath u p v" shows "u ∈ scc_of v" using assms by (metis reachable_apath scc_ofI_reachable) lemma (in wf_digraph) scc_of_eq: "u ∈ scc_of v ⟹ scc_of u = scc_of v" by (auto simp: scc_of_def intro: reachable_trans) lemma (in wf_digraph) strongly_connected_eq_iff: "strongly_connected G ⟷ sccs = {G}" (is "?L ⟷ ?R") proof assume ?L then have "G ∈ sccs" by (auto simp: sccs_def induced_subgraph_refl) moreover { fix H assume "H ∈ sccs" "G ≠ H" with ‹G ∈ sccs› have "verts G ∩ verts H = {}" by (rule scc_disj) moreover from ‹H ∈ sccs› have "verts H ⊆ verts G" by auto ultimately have "verts H = {}" by auto with ‹H ∈ sccs› have "False" by (auto simp: sccs_def strongly_connected_def) } ultimately show ?R by auto qed (auto simp: sccs_def) subsection ‹Components› lemma (in sym_digraph) exists_scc: assumes "verts G ≠ {}" shows "∃c. c ∈ sccs" proof - from assms obtain u where "u ∈ verts G" by auto then show ?thesis by (blast dest: induce_reachable_is_in_sccs) qed theorem (in sym_digraph) graph_is_union_sccs: shows "Union sccs = G" proof - have "(⋃c ∈ sccs. verts c) = verts G" by (auto intro: induce_reachable_is_in_sccs) moreover have "(⋃c ∈ sccs. arcs c) = arcs G" proof show "(⋃c ∈ sccs. arcs c) ⊆ arcs G" by safe (metis in_sccsE induced_imp_subgraph subgraphE subsetD) show "arcs G ⊆ (⋃c ∈ sccs. arcs c)" proof (safe) fix e assume "e ∈ arcs G" define a b where [simp]: "a = tail G e" and [simp]: "b = head G e" have "e ∈ (⋃x ∈ sccs. arcs x)" proof cases assume "∃x∈sccs. {a,b } ⊆ verts x" then obtain c where "c ∈ sccs" and "{a,b} ⊆ verts c" by auto then have "e ∈ {e ∈ arcs G. tail G e ∈ verts c ∧ head G e ∈ verts c}" using ‹e ∈ arcs G› by auto then have "e ∈ arcs c" using ‹c ∈ sccs› by blast then show ?thesis using ‹c ∈ sccs› by auto next assume l_assm: "¬(∃x∈sccs. {a,b} ⊆ verts x)" have "a →⇧^{*}b" using ‹e ∈ arcs G› by (metis a_def b_def reachable_adjI in_arcs_imp_in_arcs_ends) then have "{a,b} ⊆ verts (G ↾ {v. a →⇧^{*}v})" "a ∈ verts G" by (auto elim: reachable_in_vertsE) moreover have "(G ↾ {v. a →⇧^{*}v}) ∈ sccs" using ‹a ∈ verts G› by (auto intro: induce_reachable_is_in_sccs) ultimately have False using l_assm by blast then show ?thesis by simp qed then show "e ∈ (⋃c ∈ sccs. arcs c)" by auto qed qed ultimately show ?thesis by (auto simp add: Union_def) qed lemma (in sym_digraph) scc_for_vert_ex: assumes "u ∈ verts G" shows "∃c. c∈sccs ∧ u ∈ verts c" using assms by (auto intro: induce_reachable_is_in_sccs) lemma (in sym_digraph) scc_decomp_unique: assumes "S ⊆ sccs" "verts (Union S) = verts G" shows "S = sccs" proof (rule ccontr) assume "S ≠ sccs" with assms obtain c where "c ∈ sccs" and "c ∉ S" by auto with assms have "⋀d. d ∈ S ⟹ verts c ∩ verts d = {}" by (intro scc_disj) auto then have "verts c ∩ verts (Union S) = {}" by (auto simp: Union_def) with assms have "verts c ∩ verts G = {}" by auto moreover from ‹c ∈ sccs› obtain u where "u ∈ verts c ∩ verts G" by (auto simp: sccs_def strongly_connected_def) ultimately show False by blast qed end

# Theory Vertex_Walk

(* Title: Vertex_Walk.thy Author: Lars Noschinski, TU München *) theory Vertex_Walk imports Arc_Walk begin section ‹Walks Based on Vertices› text ‹ These definitions are here mainly for historical purposes, as they do not really work with multigraphs. Consider using Arc Walks instead. › type_synonym 'a vwalk = "'a list" text ‹Computes the list of arcs belonging to a list of nodes› fun vwalk_arcs :: "'a vwalk ⇒ ('a × 'a) list" where "vwalk_arcs [] = []" | "vwalk_arcs [x] = []" | "vwalk_arcs (x#y#xs) = (x,y) # vwalk_arcs (y#xs)" definition vwalk_length :: "'a vwalk ⇒ nat" where "vwalk_length p ≡ length (vwalk_arcs p)" lemma vwalk_length_simp[simp]: shows "vwalk_length p = length p - 1" by (induct p rule: vwalk_arcs.induct) (auto simp: vwalk_length_def) definition vwalk :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where "vwalk p G ≡ set p ⊆ verts G ∧ set (vwalk_arcs p) ⊆ arcs_ends G ∧ p ≠ []" definition vpath :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where "vpath p G ≡ vwalk p G ∧ distinct p" text ‹For a given vwalk, compute a vpath with the same tail G and end› function vwalk_to_vpath :: "'a vwalk ⇒ 'a vwalk" where "vwalk_to_vpath [] = []" | "vwalk_to_vpath (x # xs) = (if (x ∈ set xs) then vwalk_to_vpath (dropWhile (λy. y ≠ x) xs) else x # vwalk_to_vpath xs)" by pat_completeness auto termination by (lexicographic_order simp add: length_dropWhile_le) lemma vwalkI[intro]: