theory Cut_Points imports Show.Show_Instances Certification_Monads.Check_Monad Gabow_SCC_RBT Relations Diff_Array_Code_Haskell Shows_Literal begin definition "cut_points R X ≡ ∀Y. Y ≠ {} ⟶ Y × Y ⊆ (R ↾ Y)⇧+ ⟶ X ∩ Y ≠ {}" lemma cut_points_via_acyclic: assumes "acyclic (R ↾ (UNIV - X))" shows "cut_points R X" unfolding cut_points_def proof (intro allI impI notI) fix Y assume Y: "Y ≠ {}" "Y × Y ⊆ (R ↾ Y)⇧+" "X ∩ Y = {}" from Y obtain y where y: "y ∈ Y" by auto from y Y have "(y,y) ∈ (R ↾ Y)⇧+" by auto also have "… ⊆ (R ↾ (UNIV - X))⇧+" by (rule trancl_mono_set, insert Y(3), auto) finally show False using assms[unfolded acyclic_def] by auto qed lemma acyclic_via_sccs: "acyclic R = (∀ C. is_scc R C ⟶ C × C ⊆ R^+ ⟶ False)" unfolding acyclic_def proof (intro iffI allI notI impI) fix x assume "(x,x) ∈ R⇧+" and no_scc: "∀C. is_scc R C ⟶ C × C ⊆ R⇧+ ⟶ False" then obtain y where xy: "(x,y) ∈ R" "(y,x) ∈ R⇧*" by (meson tranclD) from is_scc_ex[of R x] obtain X where x: "x ∈ X" and scc: "is_scc R X" by blast from no_scc[rule_format, OF scc] obtain x1 x2 where x1: "x1 ∈ X" "x2 ∈ X" and no: "(x1,x2) ∉ R^+" by auto from is_scc_closed[OF scc x _ xy(2)] xy(1) have y: "y ∈ X" by auto note conn = is_scc_connected[OF scc] from conn[OF x1(1) x] xy(1) conn[OF y x1(2)] have "(x1,x2) ∈ R^+" by auto with no show False by auto next fix C assume *: "∀ x. (x,x) ∉ R^+" "is_scc R C" "C × C ⊆ R^+" from *(2) have "C ≠ {}" by auto then obtain v where v: "v ∈ C" by auto with *(1,3) show False by auto qed definition check_acyclic :: "('a :: {showl,compare_order} × 'a) list ⇒ showsl check" where "check_acyclic R ≡ do { check_allm (λ scc. error (showsl_lit (STR ''SCC '') o showsl_list scc o showsl_lit (STR '' detected ''))) (scc_decomp R) } <+? (λ s. showsl_lit (STR ''⏎graph '') o showsl_list R o showsl_lit (STR '' not acyclic⏎'') o s)" lemma check_acyclic[simp]: "isOK(check_acyclic R) = acyclic (set R)" unfolding check_acyclic_def acyclic_via_sccs by (simp add: scc_decomp_empty) definition check_cut_points :: "('a :: {showl,compare_order} × 'a) list ⇒ 'a set ⇒ showsl check" where "check_cut_points R X ≡ check_acyclic(filter (λ ab. fst ab ∉ X ∧ snd ab ∉ X) R)" lemma check_cut_points: "isOK(check_cut_points R X) ⟹ cut_points (set R) X" proof - have id: "{x ∈ set R. fst x ∉ X ∧ snd x ∉ X} = set R ↾ (UNIV - X)" by force show "isOK(check_cut_points R X) ⟹ cut_points (set R) X" unfolding check_cut_points_def by (intro cut_points_via_acyclic, simp add: id) qed end