Theory Cut_Points

theory Cut_Points
imports Show_Instances Check_Monad Gabow_SCC_RBT Relations Shows_Literal
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