Theory TopoS_Helper

theory TopoS_Helper
imports Main TopoS_Interface 
  TopoS_ENF
  vertex_example_simps
begin

lemma (in SecurityInvariant_preliminaries) sinvar_valid_remove_flattened_offending_flows:
  assumes "wf_graph ⦇nodes = nodesG, edges = edgesG⦈" (*TODO: we could get rid of this assumption*)
  shows "sinvar ⦇nodes = nodesG, edges = edgesG - ⋃ (set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP) ⦈ nP"
proof -
  { fix f
    assume *: "f∈set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP"

    from * have 1: "sinvar ⦇nodes = nodesG, edges = edgesG - f ⦈ nP"
      by (metis (opaque_lifting, mono_tags) SecurityInvariant_withOffendingFlows.valid_without_offending_flows delete_edges_simp2 graph.select_convs(1) graph.select_convs(2))
    from * have 2: "edgesG - ⋃ (set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP) ⊆ edgesG - f"
      by blast
    note 1 2
  }
  with assms show ?thesis 
    by (metis (opaque_lifting, no_types) Diff_empty Union_empty defined_offending equals0I mono_sinvar wf_graph_remove_edges)
qed


lemma (in SecurityInvariant_preliminaries) sinvar_valid_remove_SOME_offending_flows:
  assumes "set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP ≠ {}"
  shows "sinvar ⦇nodes = nodesG, edges = edgesG - (SOME F. F ∈ set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP) ⦈ nP"
proof -
  { fix f
    assume *: "f∈set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP"

    from * have 1: "sinvar ⦇nodes = nodesG, edges = edgesG - f ⦈ nP"
      by (metis (opaque_lifting, mono_tags) SecurityInvariant_withOffendingFlows.valid_without_offending_flows delete_edges_simp2 graph.select_convs(1) graph.select_convs(2))
    from * have 2: "edgesG - ⋃ (set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP) ⊆ edgesG - f"
      by blast
    note 1 2
  }
  with assms show ?thesis by (simp add: some_in_eq)
qed


lemma (in SecurityInvariant_preliminaries) sinvar_valid_remove_minimalize_offending_overapprox:
  assumes "wf_graph ⦇nodes = nodesG, edges = edgesG⦈"
      and "¬ sinvar ⦇nodes = nodesG, edges = edgesG⦈ nP" (*"set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP ≠ {}"*)
      and "set Es = edgesG" and "distinct Es"
  shows "sinvar ⦇nodes = nodesG, edges = edgesG -
              set (minimalize_offending_overapprox Es [] ⦇nodes = nodesG, edges = edgesG⦈ nP) ⦈ nP"
proof -
  from assms have off_Es: "is_offending_flows (set Es) ⦇nodes = nodesG, edges = edgesG⦈ nP"
    by (metis (no_types, lifting) Diff_cancel
        SecurityInvariant_withOffendingFlows.valid_empty_edges_iff_exists_offending_flows defined_offending
        delete_edges_simp2 graph.select_convs(2) is_offending_flows_def sinvar_monoI) 
  from minimalize_offending_overapprox_gives_back_an_offending_flow[OF assms(1) off_Es _ assms(4)] have
    in_offending: "set (minimalize_offending_overapprox Es [] ⦇nodes = nodesG, edges = edgesG⦈ nP)
      ∈ set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP"
     using assms(3) by simp

  { fix f
    assume *: "f∈set_offending_flows ⦇nodes = nodesG, edges = edgesG⦈ nP"
    from * have 1: "sinvar ⦇nodes = nodesG, edges = edgesG - f ⦈ nP"
      by (metis (opaque_lifting, mono_tags) SecurityInvariant_withOffendingFlows.valid_without_offending_flows delete_edges_simp2 graph.select_convs(1) graph.select_convs(2))
    note 1
  }
  with in_offending show ?thesis by (simp add: some_in_eq)
qed

end