Session Network_Security_Policy_Verification

Theory ML_GraphViz

theory ML_GraphViz
imports Main
begin

ML (*should we open a pdf viewer to display the generated graph?*)
datatype open_viewer = DoNothing | OpenImmediately | AskTimeouted of real

signature GRAPHVIZ =
sig
  val open_viewer: open_viewer Unsynchronized.ref

  (*function to modify the printing of a node name*)
  val default_tune_node_format: term -> string -> string

  (* edges is a term of type ('a × 'a) list *)
  
  (* @{context} default_tune_node_format (edges_format × edges)list*)
  val visualize_graph: Proof.context -> (term -> string -> string) -> term -> unit

  (* @{context} default_tune_node_format (edges_format × edges)list graphviz_header*)
  val visualize_graph_pretty: Proof.context -> (term -> string -> string) -> (string * term) list -> string-> unit

  (* helper function.
     @{context} tune_node_format node *)
  val node_to_string: Proof.context -> (term -> string -> string) ->  term -> string
  val term_to_string: Proof.context ->  term -> string;
  val term_to_string_safe: Proof.context ->  term -> string;
  val term_to_string_html: Proof.context ->  term -> string;
end

structure Graphviz: GRAPHVIZ =
struct

(*if set to `DoNothing`, graphviz will not be run and not pdf will be opened. Include ML_GraphViz_Disable.thy to run in batch mode.*)
val open_viewer = (* FIXME avoid mutable state *)
  Unsynchronized.ref (if getenv "ISABELLE_DOT" = "" then DoNothing else OpenImmediately)

val default_tune_node_format: term -> string -> string = (fn _ => I)

fun evaluate_term (ctxt: Proof.context) edges = 
  case Code_Evaluation.dynamic_value ctxt edges of
    SOME x => x
  | NONE => error "ML_GraphViz: failed to evaluate term"


fun is_valid_char c =
  (c <= #"z" andalso c >= #"a") orelse (c <= #"Z" andalso c >= #"A") orelse
  (c <= #"9" andalso c >= #"0")

val sanitize_string =
  String.map (fn c => if is_valid_char c then c else #"_")


fun term_to_string ctxt t =
  let
    val ctxt' = Config.put show_markup false ctxt;
  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t
  end;


fun term_to_string_safe ctxt t = 
  let
    val str = term_to_string ctxt t
  in
    if sanitize_string str <> str
    then (warning ("String  "^str^" contains invalid characters!"); sanitize_string str)
    else str end;

local
  val sanitize_string_html =
    String.map (fn c => if (is_valid_char c orelse c = #" " orelse (c <= #"/" andalso c >= #"(")
                            orelse c = #"|" orelse c = #"=" orelse c = #"?" orelse c = #"!" orelse c = #"_"
                            orelse c = #"[" orelse c = #"]") then c else #"_")
in
  fun term_to_string_html ctxt (n: term) : string = 
    let
      val str = term_to_string ctxt n
    in
      if sanitize_string_html str <> str
      then (warning ("String  "^str^" contains invalid characters!"); sanitize_string_html str)
      else str end
end;

fun node_to_string ctxt (tune_node_format: term -> string -> string) (n: term) : string = 
  n |> term_to_string ctxt |> tune_node_format n
  handle Subscript =>
    error ("Subscript Exception in node_to_string for string " ^
           (Pretty.string_of (Syntax.pretty_term ctxt n)));

local
  fun display_graph graph =
    if getenv "ISABELLE_DOT" = "" then
      error "Missing $ISABELLE_DOT settings variable (Graphviz \"dot\" executable)"
    else
      Isabelle_System.with_tmp_file "graphviz" "dot" (fn graph_file =>
        let
          val _ = File.write graph_file graph;
          val pdf_file = Path.explode "$ISABELLE_HOME_USER/graphviz.pdf";
          val _ =
            (Isabelle_System.bash o cat_lines)
             ["set -e",
              "cd " ^ File.bash_path (Path.dir graph_file),
              "\"$ISABELLE_DOT\" -o " ^ Bash.string (File.platform_path pdf_file) ^
                " -Tpdf " ^ Bash.string (File.platform_path graph_file),
              "\"$PDF_VIEWER\" " ^ File.bash_path pdf_file ^ " &"];
        in () end);

  fun format_dot_edges ctxt tune_node_format trm =
    let
      fun format_node t = let val str = node_to_string ctxt tune_node_format t in
                              if sanitize_string str <> str then
                                (warning ("Node "^str^" contains invalid characters!"); sanitize_string str)
                              else str
                            end;
      fun format_dot_edge (t1, t2) = format_node t1 ^ " -> " ^ format_node t2 ^ ";\n"
    in
      map format_dot_edge trm
    end

  fun apply_dot_header header edges =
    "digraph graphname {\n#header\n" ^ header ^"\n#edges\n\n"^ implode edges ^ "}"
in
  fun visualize_graph_pretty ctxt tune_node_format Es (header: string) =
    let 
      val evaluated_edges = map (fn (str, t) => (str, evaluate_term ctxt t)) Es;
      val edge_to_string = HOLogic.dest_list #> map HOLogic.dest_prod #> format_dot_edges ctxt tune_node_format #> implode;
      val formatted_edges = map (fn (str, t) => str ^ "\n" ^ edge_to_string t) evaluated_edges;
      fun execute_command () = display_graph (apply_dot_header header formatted_edges);
    in
      case !open_viewer of
          DoNothing => writeln "visualization disabled (Graphviz.open_viewer)"
        | OpenImmediately => execute_command ()
        | AskTimeouted wait_seconds => let val (text, promise) = Active.dialog_text ();
            val _ = writeln ("Run Grpahviz and display pdf? " ^ text "yes" ^ "/" ^ text "no" ^ " (execution paused)")
            in
              Timeout.apply (seconds wait_seconds) (fn _ => 
                let val m = (Future.join promise) in
                (if m = "yes" then execute_command () else (writeln "no"))
                end
              ) ()
             end handle Timeout.TIMEOUT _ =>
                  (writeln ("Timeouted. You did not klick yes/no. Killed to continue. " ^
                            "If you want to see the pdf, just re-run this and klick yes."))
    end
  end

fun visualize_graph ctxt tune_node_format edges =
  visualize_graph_pretty ctxt tune_node_format [("", edges)] "#TODO add header here"

end;


end

Theory ML_GraphViz_Disable

theory ML_GraphViz_Disable
imports ML_GraphViz
begin

MLGraphviz.open_viewer := DoNothing

end

Theory FiniteGraph

theory FiniteGraph
imports Main 
begin

(*Lots of this theory is based on a work by Benedikt Nordhoff and Peter Lammich*)

section ‹Specification of a finite directed graph›

text‹A graph G=(V,E)› consits of a set of vertices V›, also called nodes, 
       and a set of edges E›. The edges are tuples of vertices. Both, 
       the set of vertices and edges is finite.›

(* Inspired by
Title: Dijkstra's Shortest Path Algorithm
Author: Benedikt Nordhoff and Peter Lammich
http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml
*)

section ‹Graph›
subsection‹Definitions›
  text ‹A graph is represented by a record.›
  record 'v graph =
    nodes :: "'v set"
    edges :: "('v ×'v) set"

  text ‹In a well-formed graph, edges only go from nodes to nodes.›
  locale wf_graph = 
    fixes G :: "'v graph"
    ― ‹Edges only reference to existing nodes›
    assumes E_wf: "fst ` (edges G)  (nodes G)"
                     "snd ` (edges G)  (nodes G)"
    and finiteE: "finite (edges G)" (*implied by finiteV*)
    and finiteV: "finite (nodes G)"
  begin
    abbreviation "V  (nodes G)"
    abbreviation "E  (edges G)"

    lemma E_wfD: assumes "(v,v')  E"
      shows "v  V" "v'  V"
      apply -
       apply (rule subsetD[OF E_wf(1)])
       using assms apply force
      apply (rule subsetD[OF E_wf(2)])
      using assms apply force
      done

    lemma E_wfD2: "e  E. fst e  V  snd e  V"
    by (auto simp add: E_wfD)
  end

subsection ‹Basic operations on Graphs›
  text ‹The empty graph.›
  definition empty :: "'v graph" where 
    "empty   nodes = {}, edges = {} "

  text ‹Adds a node to a graph.›
  definition add_node :: "'v  'v graph  'v graph" where 
    "add_node v G   nodes = ({v}  (nodes G)), edges=edges G "

  text ‹Deletes a node from a graph. Also deletes all adjacent edges.›
  definition delete_node where "delete_node v G   
      nodes = (nodes G) - {v},   
      edges = {(e1, e2). (e1, e2)  edges G  e1  v  e2  v}
    "

  text ‹Adds an edge to a graph.›
  definition add_edge where 
  "add_edge v v' G = nodes = nodes G  {v,v'}, edges = {(v, v')}  edges G "

  text ‹Deletes an edge from a graph.›
  definition delete_edge where "delete_edge v v' G  
      nodes = nodes G, 
      edges = {(e1,e2). (e1, e2)  edges G  (e1,e2)  (v,v')}
    "
  
  definition delete_edges::"'v graph  ('v × 'v) set  'v graph" where 
    "delete_edges G es  
      nodes = nodes G, 
      edges = {(e1,e2). (e1, e2)  edges G  (e1,e2)  es}
    "

  fun delete_edges_list::"'v graph  ('v × 'v) list  'v graph" where 
    "delete_edges_list G [] = G"|
    "delete_edges_list G ((v,v')#es) = delete_edges_list (delete_edge v v' G) es"

  definition fully_connected :: "'v graph  'v graph" where
    "fully_connected G  nodes = nodes G, edges = nodes G × nodes G "


text ‹Extended graph operations›
  text ‹Reflexive transitive successors of a node. Or: All reachable nodes for v› including v›.›
  definition succ_rtran :: "'v graph  'v  'v set" where
    "succ_rtran G v = {e2. (v,e2)  (edges G)*}"

  text ‹Transitive successors of a node. Or: All reachable nodes for v›.›
  definition succ_tran :: "'v graph  'v  'v set" where
    "succ_tran G v = {e2. (v,e2)  (edges G)+}"

  ― ‹succ_tran is always finite›
  lemma succ_tran_finite: "wf_graph G  finite (succ_tran G v)"
  proof -
    assume "wf_graph G"
    from wf_graph.finiteE[OF this] have "finite ((edges G)+)" using finite_trancl[symmetric, of "edges G"] by metis
    from this have "finite {(e1,e2). (e1, e2)  (edges G)+}" by simp
    from this have finite: "finite (snd ` {(e1,e2). (e1, e2)  (edges G)+})" by (metis finite_imageI)
    have "{(e1,e2). (e1, e2)  (edges G)+  e1 = v}  {(e1,e2). (e1, e2)  (edges G)+}" by blast
    have 1: "snd ` {(e1,e2). (e1, e2)  (edges G)+  e1 = v}  snd ` {(e1,e2). (e1, e2)  (edges G)+}" by blast
    have 2: "snd ` {(e1,e2). (e1, e2)  (edges G)+  e1 = v} = {e2. (v,e2)  (edges G)+}" by force
    from 1 2 have "{e2. (v,e2)  (edges G)+}  snd ` {(e1,e2). (e1, e2)  (edges G)+}" by blast
    from this finite have "finite {e2. (v, e2)  (edges G)+}" by (metis finite_subset)
    thus "finite (succ_tran G v)" using succ_tran_def by metis
  qed
  
  text‹If there is no edge leaving from v›, then v› has no successors›
  lemma succ_tran_empty: " wf_graph G; v  (fst ` edges G)   succ_tran G v = {}"
    unfolding succ_tran_def using image_iff tranclD by fastforce

  text@{const succ_tran} is subset of nodes›
  lemma succ_tran_subseteq_nodes: " wf_graph G   succ_tran G v  nodes G"
    unfolding succ_tran_def using tranclD2 wf_graph.E_wfD(2) by fastforce

  text ‹The number of reachable nodes from v›
  definition num_reachable :: "'v graph  'v  nat" where
    "num_reachable G v = card (succ_tran G v)"

  definition num_reachable_norefl :: "'v graph  'v  nat" where
    "num_reachable_norefl G v = card (succ_tran G v - {v})"

  text@{const card} returns @{term 0} for infinite sets.
        Here, for a well-formed graph, if @{const num_reachable} is zero, there are actually no nodes reachable.›
  lemma num_reachable_zero: "wf_graph G; num_reachable G v = 0  succ_tran G v = {}"
  unfolding num_reachable_def
  apply(subgoal_tac "finite (succ_tran G v)")
   apply(simp)
  apply(blast intro: succ_tran_finite)
  done
  lemma num_succtran_zero: "succ_tran G v = {}  num_reachable G v = 0"
    unfolding num_reachable_def by simp
  lemma num_reachable_zero_iff: "wf_graph G  (num_reachable G v = 0)  (succ_tran G v = {})"
  by(metis num_succtran_zero num_reachable_zero)


section‹Undirected Graph›

subsection‹undirected graph simulation›
  text ‹Create undirected graph from directed graph by adding backward links›

  definition backflows :: "('v × 'v) set  ('v × 'v) set" where
    "backflows E  {(r,s). (s,r)  E}"

  definition undirected :: "'v graph  'v graph"
    where "undirected G =  nodes = nodes G, edges = (edges G)  {(b,a). (a,b)  edges G} "

section ‹Graph Lemmas›

  lemma graph_eq_intro: "(nodes (G::'a graph) = nodes G')  (edges G = edges G')  G = G'" by simp

  ― ‹finite›
  lemma wf_graph_finite_filterE: "wf_graph G  finite {(e1, e2). (e1, e2)  edges G  P e1 e2}"
  by(simp add: wf_graph.finiteE split_def)
  lemma wf_graph_finite_filterV: "wf_graph G  finite {n. n  nodes G  P n}"
  by(simp add: wf_graph.finiteV)

  ― ‹empty›
  lemma empty_wf[simp]: "wf_graph empty"
    unfolding empty_def by unfold_locales auto
  lemma nodes_empty[simp]: "nodes empty = {}" unfolding empty_def by simp
  lemma edges_empty[simp]: "edges empty = {}" unfolding empty_def by simp

  ― ‹add node›
  lemma add_node_wf[simp]: "wf_graph g  wf_graph (add_node v g)"
    unfolding add_node_def wf_graph_def by (auto)

  lemma delete_node_wf[simp]: "wf_graph G  wf_graph (delete_node v G)"
    by(auto simp add: delete_node_def wf_graph_def wf_graph_finite_filterE)

  ― ‹add edgde›
  lemma add_edge_wf[simp]: "wf_graph G  wf_graph (add_edge v v' G)"
    by(auto simp add: add_edge_def add_node_def wf_graph_def)

  ― ‹delete edge›
  lemma delete_edge_wf[simp]: "wf_graph G  wf_graph (delete_edge v v' G)"
    by(auto simp add: delete_edge_def add_node_def wf_graph_def split_def)
 
  ― ‹delte edges›
  lemma delete_edges_list_wf[simp]: "wf_graph G  wf_graph (delete_edges_list G E)"
    by(induction E arbitrary: G, simp, force)
  lemma delete_edges_wf[simp]: "wf_graph G  wf_graph (delete_edges G E)"
    by(auto simp add: delete_edges_def add_node_def wf_graph_def split_def)
  lemma delete_edges_list_set: "delete_edges_list G E = delete_edges G (set E)"
    proof(induction E arbitrary: G)
    case Nil thus ?case by (simp add: delete_edges_def)
    next
    case (Cons e E) thus ?case by(cases e)(simp add: delete_edge_def delete_edges_def)
    qed
  lemma delete_edges_list_union: "delete_edges_list G (ff @ keeps) = delete_edges G (set ff  set keeps)"
   by(simp add: delete_edges_list_set)
  lemma add_edge_delete_edges_list: 
    "(add_edge (fst a) (snd a) (delete_edges_list G (a # ff))) = (add_edge (fst a) (snd a) (delete_edges G (set ff)))"
   by(auto simp add: delete_edges_list_set delete_edges_def add_edge_def add_node_def)
  lemma delete_edges_empty[simp]: "delete_edges G {} = G"
   by(simp add: delete_edges_def)
  lemma delete_edges_simp2: "delete_edges G E =  nodes = nodes G, edges = edges G - E"
   by(auto simp add: delete_edges_def)
  lemma delete_edges_set_nodes: "nodes (delete_edges G E) = nodes G"
   by(simp add: delete_edges_simp2)
  lemma delete_edges_edges_mono: "E'  E  edges (delete_edges G E)  edges (delete_edges G E')"
    by(simp add: delete_edges_def, fast)
  lemma delete_edges_edges_empty: "(delete_edges G (edges G)) = Gedges := {}"
    by(simp add: delete_edges_simp2)

 ― ‹add delete›
  lemma add_delete_edge: "wf_graph (G::'a graph)  (a,b)  edges G  add_edge a b (delete_edge a b G) = G"
   apply(simp add: delete_edge_def add_edge_def wf_graph_def)
   apply(intro graph_eq_intro)
    by auto

  lemma add_delete_edges: "wf_graph (G::'v graph)  (a,b)  edges G  (a,b)  fs 
    add_edge a b (delete_edges G (insert (a, b) fs)) = (delete_edges G fs)"
    by(auto simp add: delete_edges_simp2 add_edge_def wf_graph_def)


 ― ‹fully_connected›
  lemma fully_connected_simp: "fully_connected nodes = N, edges = ignore  nodes = N, edges = N × N "
    by(simp add: fully_connected_def)
  lemma fully_connected_wf: "wf_graph G  wf_graph (fully_connected G)"
    by(simp add: fully_connected_def wf_graph_def)

 ― ‹succ_tran›
 lemma succ_tran_mono: 
  "wf_graph nodes=N, edges=E  E'  E  succ_tran nodes=N, edges=E' v  succ_tran nodes=N, edges=E v"
   apply(drule wf_graph.finiteE)
   apply(frule_tac A="E'" in rev_finite_subset, simp)
   apply(simp add: num_reachable_def)
   apply(simp add: succ_tran_def)
   apply(metis (lifting, full_types) Collect_mono trancl_mono)
  done

  ― ‹num_reachable›
  lemma num_reachable_mono:
  "wf_graph nodes=N, edges=E  E'  E  num_reachable nodes=N, edges=E' v  num_reachable nodes=N, edges=E v"
   apply(simp add: num_reachable_def)
   apply(frule_tac E'="E'" and v="v" in succ_tran_mono, simp)
   apply(frule_tac v="v" in succ_tran_finite)
   apply(simp add: card_mono)
  done

  ― ‹num_reachable_norefl›
  lemma num_reachable_norefl_mono:
  "wf_graph nodes=N, edges=E  E'  E  num_reachable_norefl nodes=N, edges=E' v  num_reachable_norefl nodes=N, edges=E v"
   apply(simp add: num_reachable_norefl_def)
   apply(frule_tac E'="E'" and v="v" in succ_tran_mono, simp)
   apply(frule_tac v="v" in succ_tran_finite)
   using card_mono by (metis Diff_mono finite_Diff subset_refl)

  ― ‹backflows›
  lemma backflows_wf: 
    "wf_graph nodes=N, edges=E  wf_graph nodes=N, edges=backflows E"
    using [[simproc add: finite_Collect]] by(auto simp add: wf_graph_def backflows_def)
  lemma undirected_backflows: 
    "undirected G =  nodes = nodes G, edges = (edges G)  backflows (edges G) "
    by(simp add: backflows_def undirected_def)
  lemma backflows_id: 
    "backflows (backflows E) = E"
    by(simp add: backflows_def)
  lemma backflows_finite: "finite E  finite (backflows E)"
    using [[simproc add: finite_Collect]] by(simp add: backflows_def) 
  lemma backflows_minus_backflows: "backflows (X - backflows Y) = (backflows X) - Y"
    by(auto simp add: backflows_def)
  lemma backflows_subseteq: "X  Y  backflows X  backflows Y"
    by(auto simp add: backflows_def)
  lemma backflows_un: "backflows (A  B) = (backflows A)  (backflows B)"
    by(auto simp add: backflows_def)
  lemma backflows_inter: "backflows (A  B) = (backflows A)  (backflows B)"
    by(auto simp add: backflows_def)
  lemma backflows_alt_fstsnd: "backflows E = (λe. (snd e, fst e)) ` E"
    by(auto simp add: backflows_def, force)


lemmas graph_ops=add_node_def delete_node_def add_edge_def delete_edge_def delete_edges_simp2


  ― ‹wf_graph›
  lemma wf_graph_remove_edges: "wf_graph  nodes = V, edges = E   wf_graph  nodes = V, edges=E - X"
    by (metis delete_edges_simp2 delete_edges_wf select_convs(1) select_convs(2))

  lemma wf_graph_remove_edges_union: 
    "wf_graph  nodes = V, edges = E  E'   wf_graph  nodes = V, edges=E"
    by(auto simp add: wf_graph_def)

  lemma wf_graph_union_edges: " wf_graph  nodes = V, edges = E ; wf_graph  nodes = V, edges=E'  
     wf_graph  nodes = V, edges=E  E'"
    by(auto simp add: wf_graph_def)

  lemma wf_graph_add_subset_edges: " wf_graph  nodes = V, edges = E ; E'  E  
     wf_graph  nodes = V, edges= E  E'"
    by(auto simp add: wf_graph_def) (metis rev_finite_subset)


(*Inspired by 
Benedikt Nordhoff and Peter Lammich
Dijkstra's Shortest Path Algorithm
http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml*)
(*more a literal copy of http://isa-afp.org/browser_info/current/AFP/Dijkstra_Shortest_Path/Graph.html*)

  text ‹Successors of a node.›
  definition succ :: "'v graph  'v  'v set"
    where "succ G v  {v'. (v,v')edges G}"


  lemma succ_finite[simp, intro]: "finite (edges G)  finite (succ G v)"
    unfolding succ_def
    by (rule finite_subset[where B="snd`edges G"]) force+

  lemma succ_empty: "succ empty v = {}" unfolding empty_def succ_def by auto

  lemma (in wf_graph) succ_subset: "succ G v  V"
    unfolding succ_def using E_wf
    by (force)


end

Theory FiniteListGraph

theory FiniteListGraph
imports 
  FiniteGraph
  "Transitive-Closure.Transitive_Closure_List_Impl"
begin

section ‹Specification of a finite graph, implemented by lists›

text‹A graph G=(V,E)› consits of a list of vertices @{term V}, also called nodes, 
       and a list of edges @{term E}. The edges are tuples of vertices.
       Using lists instead of sets, code can be easily created.›

  record 'v list_graph =
    nodesL :: "'v list"
    edgesL :: "('v ×'v) list"

text‹Correspondence the FiniteGraph›
  definition list_graph_to_graph :: "'v list_graph  'v graph" where 
    "list_graph_to_graph G =  nodes = set (nodesL G), edges = set (edgesL G) "


  definition wf_list_graph_axioms :: "'v list_graph  bool" where
    "wf_list_graph_axioms G  fst` set (edgesL G)  set (nodesL G)  snd` set (edgesL G)  set (nodesL G)"


  lemma wf_list_graph_iff_wf_graph: "wf_graph (list_graph_to_graph G)  wf_list_graph_axioms G"
  unfolding list_graph_to_graph_def wf_graph_def wf_list_graph_axioms_def
  by simp

  text‹We say a @{typ "'v list_graph"} is valid if it fulfills the graph axioms and its lists are distinct›
  definition wf_list_graph::"('v) list_graph  bool" where
   "wf_list_graph G = (distinct (nodesL G)  distinct (edgesL G)  wf_list_graph_axioms G)"


section‹FiniteListGraph operations›

  text ‹Adds a node to a graph.›
  definition add_node :: "'v  'v list_graph  'v list_graph" where 
    "add_node v G =  nodesL = (if v  set (nodesL G) then nodesL G else v#nodesL G), edgesL=edgesL G "

  text ‹Adds an edge to a graph.›
  definition add_edge :: "'v  'v  'v list_graph  'v list_graph" where 
    "add_edge v v' G = (add_node v (add_node v' G)) edgesL := (if (v, v')  set (edgesL G) then edgesL G else (v, v')#edgesL G) "

  text ‹Deletes a node from a graph. Also deletes all adjacent edges.›
  definition delete_node :: "'v  'v list_graph  'v list_graph" where 
  "delete_node v G =  
    nodesL = remove1 v (nodesL G), edgesL = [(e1,e2)  (edgesL G). e1  v  e2  v]
    "

  text ‹Deletes an edge from a graph.›
  definition delete_edge :: "'v  'v  'v list_graph  'v list_graph" where 
    "delete_edge v v' G = nodesL = nodesL G, edgesL = [(e1,e2)  edgesL G. e1  v  e2  v'] "

  
  fun delete_edges::"'v list_graph  ('v × 'v) list  'v list_graph" where 
    "delete_edges G [] = G"|
    "delete_edges G ((v,v')#es) = delete_edges (delete_edge v v' G) es"



text ‹extended graph operations›
   text ‹Reflexive transitive successors of a node. Or: All reachable nodes for v including v.›
    definition succ_rtran :: "'v list_graph  'v  'v list" where
      "succ_rtran G v = rtrancl_list_impl (edgesL G) [v]"

   text ‹Transitive successors of a node. Or: All reachable nodes for v.›
    definition succ_tran :: "'v list_graph  'v  'v list" where
      "succ_tran G v = trancl_list_impl (edgesL G) [v]"
  
   text ‹The number of reachable nodes from v›
    definition num_reachable :: "'v list_graph  'v  nat" where
      "num_reachable G v = length (succ_tran G v)"


    definition num_reachable_norefl :: "'v list_graph  'v  nat" where
      "num_reachable_norefl G v = length ([ x  succ_tran G v. x  v])"


subsection‹undirected graph simulation›
  text ‹Create undirected graph from directed graph by adding backward links›
  fun backlinks :: "('v × 'v) list  ('v × 'v) list" where
    "backlinks [] = []" |
    "backlinks ((e1, e2)#es) = (e2, e1)#(backlinks es)"

  definition undirected :: "'v list_graph  'v list_graph"
    where "undirected G   nodesL = nodesL G, edgesL = remdups (edgesL G @ backlinks (edgesL G)) "

section‹Correctness lemmata›

  ― ‹add node›
  lemma add_node_wf: "wf_list_graph G  wf_list_graph (add_node v G)"
  unfolding wf_list_graph_def wf_list_graph_axioms_def add_node_def
  by auto

  lemma add_node_set_nodes: "set (nodesL (add_node v G)) = set (nodesL G)  {v}"
  unfolding add_node_def
  by auto

  lemma add_node_set_edges: "set (edgesL (add_node v G)) = set (edgesL G)"
  unfolding add_node_def
  by auto

  lemma add_node_correct: "FiniteGraph.add_node v (list_graph_to_graph G) = list_graph_to_graph (add_node v G)"
  unfolding FiniteGraph.add_node_def list_graph_to_graph_def
  by (simp add: add_node_set_edges add_node_set_nodes)

  lemma add_node_wf2: "wf_graph (list_graph_to_graph G)  wf_graph (list_graph_to_graph (add_node v G))"
  by (subst add_node_correct[symmetric]) simp

  ― ‹add edge›
  lemma add_edge_wf: "wf_list_graph G  wf_list_graph (add_edge v v' G)"
  unfolding wf_list_graph_def add_edge_def add_node_def wf_list_graph_axioms_def
  by auto

  lemma add_edge_set_nodes: "set (nodesL (add_edge v v' G)) = set (nodesL G)  {v,v'}"
  unfolding add_edge_def add_node_def
  by auto

  lemma add_edge_set_edges: "set (edgesL (add_edge v v' G)) = set (edgesL G)  {(v,v')}"
  unfolding add_edge_def add_node_def
  by auto

  lemma add_edge_correct: "FiniteGraph.add_edge v v' (list_graph_to_graph G) = list_graph_to_graph (add_edge v v' G)"
  unfolding FiniteGraph.add_edge_def add_edge_def list_graph_to_graph_def
  by (auto simp: add_node_set_nodes)

  lemma add_edge_wf2: "wf_graph (list_graph_to_graph G)  wf_graph (list_graph_to_graph (add_edge v v' G))"
  by (subst add_edge_correct[symmetric]) simp

  ― ‹delete node›
  lemma delete_node_wf: "wf_list_graph G  wf_list_graph (delete_node v G)"
  unfolding wf_list_graph_def delete_node_def wf_list_graph_axioms_def
  by auto

  lemma delete_node_set_edges:
    "set (edgesL (delete_node v G)) = {(a,b). (a, b)  set (edgesL G)  a  v  b  v}"
  unfolding delete_node_def
  by auto

  lemma delete_node_correct:
    assumes "wf_list_graph G"
    shows "FiniteGraph.delete_node v (list_graph_to_graph G) = list_graph_to_graph (delete_node v G)"
  using assms
  unfolding FiniteGraph.delete_node_def delete_node_def list_graph_to_graph_def wf_list_graph_def
  by auto

  ― ‹delete edge›
  lemma delete_edge_set_nodes: "set (nodesL (delete_edge v v' G)) = set (nodesL G)"
  unfolding delete_edge_def
  by simp

  lemma delete_edge_set_edges:
    "set (edgesL (delete_edge v v' G)) = {(a,b). (a,b)  set (edgesL G)  (a,b)  (v,v')}"
  unfolding delete_edge_def
  by auto

  lemma delete_edge_set_edges2:
    "set (edgesL (delete_edge v v' G)) = set (edgesL G) - {(v,v')}"
  by (auto simp:delete_edge_set_edges)

  lemma delete_edge_wf: "wf_list_graph G  wf_list_graph (delete_edge v v' G)"
  unfolding wf_list_graph_def delete_edge_def wf_list_graph_axioms_def
  by auto
    
  lemma delete_edge_length: "length (edgesL (delete_edge v v' G))  length (edgesL G)"
  unfolding delete_edge_def
  by simp

  lemma delete_edge_commute: "delete_edge a1 a2 (delete_edge b1 b2 G) = delete_edge b1 b2 (delete_edge a1 a2 G)"
  unfolding delete_edge_def
  by simp metis (* auto doesn't seem to like filter_cong *)

  lemma delete_edge_correct: "FiniteGraph.delete_edge v v' (list_graph_to_graph G) = list_graph_to_graph (delete_edge v v' G)"
  unfolding FiniteGraph.delete_edge_def delete_edge_def list_graph_to_graph_def
  by auto

  lemma delete_edge_wf2: "wf_graph (list_graph_to_graph G)  wf_graph (list_graph_to_graph (delete_edge v v' G))"
  by (subst delete_edge_correct[symmetric]) simp

  ― ‹delete edges›
  lemma delete_edges_wf: "wf_list_graph G  wf_list_graph (delete_edges G E)"
  by (induction E arbitrary: G) (auto simp: delete_edge_wf)

  lemma delete_edges_set_nodes: "set (nodesL (delete_edges G E)) = set (nodesL G)"
  by (induction E arbitrary: G) (auto simp: delete_edge_set_nodes)

  lemma delete_edges_nodes: "nodesL (delete_edges G es) = nodesL G"
  by (induction es arbitrary: G) (auto simp: delete_edge_def)

  lemma delete_edges_set_edges: "set (edgesL (delete_edges G E)) = set (edgesL G) - set E"
  by (induction E arbitrary: G) (auto simp: delete_edge_def delete_edge_set_nodes)

  lemma delete_edges_set_edges2:
    "set (edgesL (delete_edges G E)) = {(a,b). (a,b)  set (edgesL G)  (a,b)  set E}"
  by (auto simp: delete_edges_set_edges)

  lemma delete_edges_length: "length (edgesL (delete_edges G f))  length (edgesL G)"
  proof (induction f arbitrary:G)
    case (Cons f fs)
    thus ?case
      apply (cases f, hypsubst)
      apply (subst delete_edges.simps(2))
      apply (metis delete_edge_length le_trans)
      done
  qed simp

  lemma delete_edges_chain: "delete_edges G (as @ bs) = delete_edges (delete_edges G as) bs"
  proof (induction as arbitrary: bs G)
    case (Cons f fs)
    thus ?case
      by (cases f) auto
  qed simp

  lemma delete_edges_delete_edge_commute:
    "delete_edges (delete_edge a1 a2 G) as = delete_edge a1 a2 (delete_edges G as)"
  proof (induction as arbitrary: G a1 a2)
    case (Cons f fs)
    thus ?case
      by (cases f) (simp add: delete_edge_commute)
  qed simp

  lemma delete_edges_commute:
    "delete_edges (delete_edges G as) bs = delete_edges (delete_edges G bs) as"
  proof (induction as arbitrary: bs G)
    case (Cons f fs)
    thus ?case
      by (cases f) (simp add: delete_edges_delete_edge_commute)
  qed simp

  lemma delete_edges_as_filter:
    "delete_edges G l =  nodesL = nodesL G,  edgesL = [x  edgesL G. x  set l] "
  proof (induction l)
    case (Cons f fs)
    thus ?case
      apply (cases f)
      apply (simp add: delete_edges_delete_edge_commute)
      apply (simp add: delete_edge_def)
      apply (metis (lifting, full_types) prod.exhaust case_prodI split_conv)
      done
  qed simp

  declare delete_edges.simps[simp del] (*do not automatically expand definition*)

  lemma delete_edges_correct:
    "FiniteGraph.delete_edges (list_graph_to_graph G) (set E) = list_graph_to_graph (delete_edges G E)"
  unfolding list_graph_to_graph_def FiniteGraph.delete_edges_def
  by (auto simp add: delete_edges_as_filter )
  
  lemma delete_edges_wf2:
    "wf_graph (list_graph_to_graph G)  wf_graph (list_graph_to_graph (delete_edges G E))"
  by (subst delete_edges_correct[symmetric]) simp

  ― ‹helper about reflexive transitive closure impl›
  lemma distinct_relpow_impl:
    "distinct L  distinct new  distinct have  distinct (new@have)  
     distinct (relpow_impl (λas. remdups (map snd [(a, b)L . a  set as])) (λxs ys. [xxs . x  set ys] @ ys) (λx xs. x  set xs) new have M)"
  proof (induction M arbitrary: "new" "have")
    case Suc
    hence
      "distinct ([xnew . x  set have] @ have)"
      "set ([nremdups (map snd [(a, b)L . a  set new]) . (n  set new  n  set have)  n  set have])  set ([xnew . x  set have] @ have) = {}"
      by auto

    with Suc show ?case
      by auto
  qed auto

  lemma distinct_rtrancl_list_impl: "distinct L  distinct ls  distinct (rtrancl_list_impl L ls)"
  unfolding rtrancl_list_impl_def rtrancl_impl_def
  by (simp add:distinct_relpow_impl)

  lemma distinct_trancl_list_impl: "distinct L  distinct ls  distinct (trancl_list_impl L ls)"
  unfolding trancl_list_impl_def trancl_impl_def
  by (simp add:distinct_relpow_impl)

  ― ‹succ rtran›
  value "succ_rtran  nodesL = [1::nat,2,3,4,8,9,10], edgesL = [(1,2), (2,3), (3,4), (8,9),(9,8)]  1"

  lemma succ_rtran_correct: "FiniteGraph.succ_rtran (list_graph_to_graph G) v = set (succ_rtran G v)"
  unfolding FiniteGraph.succ_rtran_def succ_rtran_def list_graph_to_graph_def
  by (simp add: rtrancl_list_impl)

  lemma distinct_succ_rtran: "wf_list_graph G  distinct (succ_rtran G v)"
  unfolding succ_rtran_def wf_list_graph_def
  by (auto intro: distinct_rtrancl_list_impl)

  lemma succ_rtran_set: "set (succ_rtran G v) = {e2. (v,e2)  (set (edgesL G))*}"
  unfolding succ_rtran_def
  by (simp add: rtrancl_list_impl)

  ― ‹succ tran›
  lemma distinct_succ_tran: "wf_list_graph G  distinct (succ_tran G v)"
  unfolding succ_tran_def wf_list_graph_def
  by (auto intro: distinct_trancl_list_impl)

  lemma succ_tran_set: "set (succ_tran G v) = {e2. (v,e2)  (set (edgesL G))+}"
  unfolding succ_tran_def
  by (simp add: trancl_list_impl)

  value "succ_tran  nodesL = [1::nat,2,3,4,8,9,10], edgesL = [(1,2), (2,3), (3,4), (8,9),(9,8)]  1"

  lemma succ_tran_correct: "FiniteGraph.succ_tran (list_graph_to_graph G) v = set (succ_tran G v)"
  unfolding FiniteGraph.succ_tran_def succ_tran_def list_graph_to_graph_def
  by (simp add:trancl_list_impl)
  
  ― ‹num_reachable›
  lemma num_reachable_correct:
    "wf_list_graph G  FiniteGraph.num_reachable (list_graph_to_graph G) v = num_reachable G v"
  unfolding num_reachable_def FiniteGraph.num_reachable_def
  by (metis List.distinct_card distinct_succ_tran succ_tran_correct)

  ― ‹num_reachable_norefl›
  lemma num_reachable_norefl_correct:
    "wf_list_graph G  
     FiniteGraph.num_reachable_norefl (list_graph_to_graph G) v = num_reachable_norefl G v"
 unfolding num_reachable_norefl_def FiniteGraph.num_reachable_norefl_def
 by (metis (full_types) List.distinct_card distinct_filter distinct_succ_tran set_minus_filter_out succ_tran_correct)

  ― ‹backlinks, i.e. backflows in formal def›
  lemma backlinks_alt: "backlinks E = [(snd e, fst e). e  E]"
  by (induction E) auto

  lemma backlinks_set: "set (backlinks E) = {(e2, e1). (e1, e2)  set E}"
  by (induction E) auto

  lemma undirected_nodes_set: "set (edgesL (undirected G)) = set (edgesL G)  {(e2, e1). (e1, e2)  set (edgesL G)}"
  unfolding undirected_def
  by (simp add: backlinks_set)

  lemma undirected_succ_tran_set: "set (succ_tran (undirected G) v) = {e2. (v,e2)  (set (edgesL (undirected G)))+}"
  by (fact succ_tran_set)

  lemma backlinks_in_nodes_G: " fst ` set (edgesL G)  set (nodesL G); snd ` set (edgesL G)  set (nodesL G)   
    fst` set (edgesL (undirected G))  set (nodesL (undirected G))  snd` set (edgesL (undirected G))  set (nodesL (undirected G))"
  unfolding undirected_def
  by(auto simp: backlinks_set)

  lemma backlinks_distinct: "distinct E  distinct (backlinks E)"
  by (induction E) (auto simp: backlinks_alt)

  lemma backlinks_subset: "set (backlinks X)  set (backlinks Y)  set X  set Y"
  by (auto simp: backlinks_set)

  lemma backlinks_correct: "FiniteGraph.backflows (set E) = set (backlinks E)"
  unfolding backflows_def
  by(simp add: backlinks_set)

  ― ‹undirected›
  lemma undirected_wf: "wf_list_graph G  wf_list_graph (undirected G)"
  unfolding wf_list_graph_def wf_list_graph_axioms_def
  by (simp add:backlinks_in_nodes_G) (simp add: undirected_def)

  lemma undirected_correct: 
    "FiniteGraph.undirected (list_graph_to_graph G) = list_graph_to_graph (undirected G)"
  unfolding FiniteGraph.undirected_def undirected_def list_graph_to_graph_def
  by (simp add: backlinks_set)
      
lemmas wf_list_graph_wf =
  add_node_wf
  add_edge_wf
  delete_node_wf
  delete_edge_wf
  delete_edges_wf
  undirected_wf

lemmas list_graph_correct =
  add_node_correct
  add_edge_correct
  delete_node_correct
  delete_edge_correct
  delete_edges_correct
  succ_rtran_correct
  succ_tran_correct
  num_reachable_correct
  undirected_correct


end

Theory TopoS_Util

theory TopoS_Util
imports Main
begin

lemma finite_ne_subset_induct [case_names singleton insert, consumes 2]:
  assumes "finite F" and "F  {}" and "F  A"
  assumes "x. x  A  P {x}"
    and "x F. finite F  F  {}  x  A  x  F  P F   P (insert x F)"
  shows "P F"
using assms
proof induct
  case empty then show ?case by simp
next
  case (insert x F) then show ?case by cases auto
qed


(*lemma from afp collections Misc*)
lemma set_union_code:
  "set xs  set ys = set (xs @ ys)"
  by auto

end

Theory Efficient_Distinct

theory Efficient_Distinct
imports 
  Automatic_Refinement.Misc (*mergesort*)
  "HOL-Library.List_Lexorder"
  "HOL-Library.Product_Lexorder"
  "HOL-Library.Char_ord"
  TopoS_Util
begin

text ‹efficient distinct code›

  lemma list_length_iff_distinct: 
  "set xs = set ys; distinct ys  distinct xs  length xs = length ys"
  by (metis distinct_card card_distinct)

  lemma distinct_by_mergesort: "(length (mergesort_remdups xs) = length xs)  distinct xs"
  by (metis list_length_iff_distinct mergesort_remdups_correct)

  lemma [code]: "distinct xs = (length (mergesort_remdups xs) = length xs)"
  by (fact distinct_by_mergesort[symmetric])

  text‹providing tail recursive versions of certain functions›
  (*otherwise scala code generated with this code always produces a StackOverflowException for large inputs*)

text@{const List.map}

  fun map_tailrec ::  "('a  'b)  'a list  'b list  'b list" where
  "map_tailrec f [] accs = accs" | 
  "map_tailrec f (a#as) accs = (map_tailrec f as ((f a)#accs))"

  lemma map_tailrec_is_listmap: "rev (map_tailrec f l accs) = (rev accs)@(List.map f l)"
  by (induction l accs rule: map_tailrec.induct) auto

  definition efficient_map :: "('a  'b)  'a list  'b list" where
    "efficient_map f l  rev (map_tailrec f l [])"

  lemma [code]: "List.map f l = efficient_map f l"
  by (simp add: efficient_map_def map_tailrec_is_listmap)

text@{const merge}

 (*inefficient version*)
 fun merge_tailrec_inefficient :: "('a::linorder) list  'a list  'a list  'a list" where
    "merge_tailrec_inefficient (a#as) (b#bs) accs = (if a < b
      then merge_tailrec_inefficient (as) (b#bs) (accs@[a])
      else if a = b then merge_tailrec_inefficient (as) (bs) (accs@[a])
      else merge_tailrec_inefficient (a#as) (bs) (accs@[b]))"
  | "merge_tailrec_inefficient [] bs accs= accs@bs"
  | "merge_tailrec_inefficient as [] accs = accs@as"

  lemma merge_tailrec_inefficient_prepend:
  "merge_tailrec_inefficient as bs (a # accs) = a # merge_tailrec_inefficient as bs accs"
  by (induction as bs accs rule: merge_tailrec_inefficient.induct) auto

  lemma merge_as_tailrec_inefficient: "merge as bs = merge_tailrec_inefficient as bs []"
  by (induction as bs rule: merge.induct)  (auto simp: merge_tailrec_inefficient_prepend)

 fun merge_tailrec :: "('a::linorder) list  'a list  'a list  'a list" where
    "merge_tailrec (a#as) (b#bs) accs = (if a < b
      then merge_tailrec (as) (b#bs) (a#accs)
      else if a = b then merge_tailrec (as) (bs) (a#accs)
      else merge_tailrec (a#as) (bs) (b#accs))"
  | "merge_tailrec [] bs accs= (rev accs)@bs"
  | "merge_tailrec as [] accs = (rev accs)@as"

  lemma merge_tailrec_listappend:
    "merge_tailrec as bs (accs1@accs2) = (rev accs2)@(merge_tailrec as bs accs1)"
  proof (induction as bs "accs1@accs2" arbitrary: accs1 accs2 rule: merge_tailrec.induct)
    case (1 a as b bs)
    thus ?case
      by (cases a b rule: linorder_cases) (metis append_Cons merge_tailrec.simps(1))+
  qed auto

  lemma merge_tailrec_acc_append: 
    "merge_tailrec as bs (accs@[a]) = a#(merge_tailrec as bs (accs))"
  by (induction as bs accs rule: merge_tailrec.induct) auto

  lemma merge_inefficient_as_efficient:
    "merge_tailrec_inefficient as bs (rev accs) = (merge_tailrec as bs accs)"
  proof (induction as bs accs arbitrary: accs rule: merge_tailrec_inefficient.induct)
    case (1 a as b bs)
    thus ?case
      by (cases a b rule: linorder_cases) (metis merge_tailrec.simps(1) merge_tailrec_inefficient.simps(1) rev.simps(2))+
  qed auto

  lemma [code]: "merge as bs = merge_tailrec as bs []"
  apply (subst merge_as_tailrec_inefficient)
  apply (subst merge_inefficient_as_efficient[where accs = "[]", unfolded rev.simps(1)])
  apply (rule refl)
  done

(*import scala.annotation.tailrec*)
  export_code distinct checking Scala


  value "distinct [(CHR ''A'')]"
  value "distinct [''a'', ''b'']"
  value "distinct [(''a'', ''b'')]" 
  value "distinct (map fst [(''a'', ''b''), (''a'', ''c'')])"

end

Theory FiniteListGraph_Impl

theory FiniteListGraph_Impl
imports 
  FiniteListGraph
  (*"../../Collections/ICF/impl/RBTSetImpl" (*red black trees*)*)
    "HOL-Library.RBT_Impl"
    "HOL-Library.RBT"
  "HOL-Library.Product_Lexorder"
  (*maybe import the following only at the end*)
  Efficient_Distinct
  "HOL-Library.Code_Target_Nat"
begin



text ‹A graph's well-formed-ness can be tested with an executable function.›  
  fun wf_list_graph_impl::"'v list  ('v × 'v) list  bool" where
    "wf_list_graph_impl V [] = True" |
    "wf_list_graph_impl V ((v1,v2)#Es) = (v1  set V  v2  set V  wf_list_graph_impl V Es)"


  lemma wf_list_graph_impl_axioms_locale_props: 
    "wf_list_graph_impl V E  fst` set E  set V  snd` set E  set V"
  by (induction E) auto


definition rbt_fromlist :: "'a list  ('a::linorder, unit) RBT.rbt" where 
  "rbt_fromlist ls  RBT.bulkload (map (λl. (l, ())) ls)"
definition "rbt_contains a rbt  RBT.lookup rbt a  None"

lemma rbt_contains: "rbt_contains a (rbt_fromlist V)  a  set V"
  apply(simp add: rbt_contains_def rbt_fromlist_def)
  apply(induction V)
   by(simp)+

  (*making the ∈ more efficient*)
  fun wf_list_graph_impl_rs::"('v::linorder,unit) RBT.rbt  ('v × 'v) list  bool" where
    "wf_list_graph_impl_rs V [] = True" |
    "wf_list_graph_impl_rs V ((v1,v2)#Es) = (rbt_contains v1 V  rbt_contains v2 V  wf_list_graph_impl_rs V Es)"

    
 lemma[code]: "wf_list_graph_impl V E = wf_list_graph_impl_rs (rbt_fromlist V) E"
   apply(induction E)
    apply(simp; fail)
   apply(rename_tac e Es)
   apply(case_tac e)
   by(simp add: rbt_contains)

  lemma[code]: "FiniteListGraph.wf_list_graph_axioms G = wf_list_graph_impl (nodesL G) (edgesL G)"
    by(simp add: FiniteListGraph.wf_list_graph_axioms_def wf_list_graph_impl_axioms_locale_props)

  text‹The list implementation matches the @{term "wf_graph"} definition›
  theorem wf_list_graph_iff_wf_graph: 
    "wf_graph (list_graph_to_graph G)  wf_list_graph_axioms G"
  apply(unfold list_graph_to_graph_def wf_graph_def wf_list_graph_axioms_def wf_list_graph_impl_axioms_locale_props)
    by simp
  corollary wf_list_graph_iff_wf_graph_simplified: 
  "wf_graph nodes = set (nodesL G), edges = set (edgesL G)  wf_list_graph_axioms G"
  apply(simp add: wf_list_graph_iff_wf_graph[unfolded list_graph_to_graph_def, simplified])
  done


 
text ‹Code examples.›
  definition wf_graph_example where
  "wf_graph_example   nodesL = [1::nat,4,6], edgesL = [(1,4), (1,6), (6,4)] "

  value "wf_list_graph wf_graph_example"

  definition wf_graph_impl_example where
  "wf_graph_impl_example  wf_list_graph wf_graph_example"


  export_code wf_list_graph empty add_node delete_node add_edge delete_edge checking Scala


end

Theory TopoS_Vertices

theory TopoS_Vertices
imports Main 
"HOL-Library.Char_ord" (*order on char*)
"HOL-Library.List_Lexorder" (*order on strings*)
begin


section‹A type for vertices›

text‹
This theory makes extensive use of graphs.
We define a typeclass vertex› for the vertices we will use in our theory.
The vertices will correspond to network or policy entities.

Later, we will conduct some proves by providing counterexamples.
Therefore, we say that the type of a vertex has at least three pairwise distinct members.

For example, the types @{typ "string"}, @{typ nat}, @{typ "bool × bool"} and many other fulfill this assumption. 
The type @{typ "bool"} alone does not fulfill this assumption, because it only has two elements.

This is only a constraint over the type, of course, a policy with less than three entities can also be verified.

TL;DR: We define @{typ "'a"} vertex›, which is as good as @{typ "'a"}.
›


― ‹We need at least some vertices available for a graph ...›
class vertex =
  fixes vertex_1 :: "'a"
  fixes vertex_2 :: "'a"
  fixes vertex_3 :: "'a"
  assumes distinct_vertices: "distinct [vertex_1, vertex_2, vertex_3]"
begin
  lemma distinct_vertices12[simp]: "vertex_1  vertex_2" using distinct_vertices by(simp)
  lemma distinct_vertices13[simp]: "vertex_1  vertex_3" using distinct_vertices by(simp)
  lemma distinct_vertices23[simp]: "vertex_2  vertex_3" using distinct_vertices by(simp)
  
  lemmas distinct_vertices_sym = distinct_vertices12[symmetric] distinct_vertices13[symmetric]
          distinct_vertices23[symmetric]
  declare distinct_vertices_sym[simp]
end


text ‹Numbers, chars and strings are good candidates for vertices.›

instantiation nat::vertex
begin
  definition "vertex_1_nat" ::nat where "vertex_1  (1::nat)"
  definition "vertex_2_nat" ::nat where "vertex_2  (2::nat)"
  definition "vertex_3_nat" ::nat where "vertex_3  (3::nat)"
instance proof qed(simp add: vertex_1_nat_def vertex_2_nat_def vertex_3_nat_def)
end
value "vertex_1::nat"

instantiation int::vertex
begin
  definition "vertex_1_int" ::int where "vertex_1  (1::int)"
  definition "vertex_2_int" ::int where "vertex_2  (2::int)"
  definition "vertex_3_int" ::int where "vertex_3  (3::int)"
instance proof qed(simp add: vertex_1_int_def vertex_2_int_def vertex_3_int_def)
end

instantiation char::vertex
begin
  definition "vertex_1_char" ::char where "vertex_1  CHR ''A''"
  definition "vertex_2_char" ::char where "vertex_2  CHR ''B''"
  definition "vertex_3_char" ::char where "vertex_3  CHR ''C''"
instance proof(intro_classes) qed(simp add: vertex_1_char_def  vertex_2_char_def vertex_3_char_def)
end
value "vertex_1::char"


instantiation list :: ("vertex") vertex
begin
  definition "vertex_1_list" where "vertex_1  []"
  definition "vertex_2_list" where "vertex_2  [vertex_1]"
  definition "vertex_3_list" where "vertex_3  [vertex_1, vertex_1]"
instance proof qed(simp add: vertex_1_list_def vertex_2_list_def vertex_3_list_def)
end

― ‹for the ML graphviz visualizer›
ML fun tune_string_vertex_format (t: term) (s: string) : string = 
    if fastype_of t = @{typ string} then
      if String.isPrefix "''" s then
        String.substring (s, (size "''"), (size s - (size "''''")))
      else let val _ = writeln ("no tune_string_vertex_format for \""^s^"\"") in s end
    else s
    handle Subscript => let val _ = writeln ("tune_string_vertex_format Subscript excpetion") in s end;


  
end

Theory TopoS_Interface

theory TopoS_Interface
imports Main "Lib/FiniteGraph" TopoS_Vertices "Lib/TopoS_Util"
begin



section ‹Security Invariants›
  text‹
    A good documentation of this formalization is available in \cite{diekmann2014forte}. 
›

  text‹
    We define security invariants over a graph.
    The graph corresponds to the network's access control structure.
›

  (*TODO: make datatype!*)
  ― ‹@{typ "'v"} is the type of the nodes in the graph (hosts in the network). 
     @{typ "'a"} is the type of the host attributes.›
  record ('v::vertex, 'a) TopoS_Params =
    node_properties :: "'v::vertex  'a option"

text‹
A Security Invariant is defined as locale.

We successively define more and more locales with more and more assumptions.
This clearly depicts which assumptions are necessary to use certain features of a Security Invariant.
In addition, it makes instance proofs of Security Invariants easier, since the lemmas obtained by an (easy, few assumptions) instance proof 
can be used for the complicated (more assumptions) instance proofs.

A security Invariant consists of one function: sinvar›.
Essentially, it is a predicate over the policy (depicted as graph G› and a host attribute mapping (nP›)).
›

text ‹A Security Invariant where the offending flows (flows that invalidate the policy) can be defined and calculated.
No assumptions are necessary for this step.
›  
  locale SecurityInvariant_withOffendingFlows = 
    fixes sinvar::"('v::vertex) graph  ('v::vertex  'a)  bool" ― ‹policy @{text "⇒"} host attribute mapping @{text "⇒"} bool›
   begin
    ― ‹Offending Flows definitions:›
    definition is_offending_flows::"('v × 'v) set  'v graph  ('v  'a)  bool" where
      "is_offending_flows f G nP  ¬ sinvar G nP  sinvar (delete_edges G f) nP"
    
    ― ‹Above definition is not minimal:›
    definition is_offending_flows_min_set::"('v × 'v) set  'v graph  ('v  'a)  bool" where
      "is_offending_flows_min_set f G nP  is_offending_flows f G nP  
        ( (e1, e2)  f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP)"

    ― ‹The set of all offending flows.›
    definition set_offending_flows::"'v graph  ('v  'a)  ('v × 'v) set set" where
      "set_offending_flows G  nP = {F. F  (edges G)  is_offending_flows_min_set F G nP}"
  

    text ‹Some of the @{const set_offending_flows} definition›
    lemma offending_not_empty: " F  set_offending_flows G nP   F  {}"
     by(auto simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma empty_offending_contra:
       " F  set_offending_flows G nP; F = {}  False"
     by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma offending_notevalD: "F  set_offending_flows G nP  ¬ sinvar G nP"
     by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    lemma sinvar_no_offending: "sinvar G nP  set_offending_flows G nP = {}"
      by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def)
    theorem removing_offending_flows_makes_invariant_hold:
      "F  set_offending_flows G nP. sinvar (delete_edges G F) nP"
      proof(cases "sinvar G nP")
       case True
        hence no_offending: "set_offending_flows G nP = {}" using sinvar_no_offending by simp
        thus "Fset_offending_flows G nP. sinvar (delete_edges G F) nP" using empty_iff by simp
       next
       case False thus "Fset_offending_flows G nP. sinvar (delete_edges G F) nP"
        by(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def graph_ops)
      qed
  corollary valid_without_offending_flows:
  " F  set_offending_flows G nP   sinvar (delete_edges G F) nP"
    by(simp add: removing_offending_flows_makes_invariant_hold)

  lemma set_offending_flows_simp: 
    " wf_graph G  
      set_offending_flows G nP = {F. F  edges G 
        (¬ sinvar G nP  sinvar nodes = nodes G, edges = edges G - F nP) 
        ((e1, e2)F. ¬ sinvar nodes = nodes G, edges = {(e1, e2)}  (edges G - F) nP)}"
    apply(simp only: set_offending_flows_def is_offending_flows_min_set_def 
      is_offending_flows_def delete_edges_simp2 add_edge_def graph.select_convs)
    apply(subgoal_tac "F e1 e2. F  edges G  (e1, e2)  F  nodes G  {e1, e2} = nodes G")
     apply fastforce
    apply(simp add: wf_graph_def)
    by (metis fst_conv imageI in_mono insert_absorb snd_conv)

   end



print_locale! SecurityInvariant_withOffendingFlows


text‹
The locale SecurityInvariant_withOffendingFlows› has no assumptions about the security invariant sinvar›.
Undesirable things may happen:
The offending flows can be empty, even for a violated invariant.

We provide an example, the security invariant @{term "(λ_ _. False)"}.
As host attributes, we simply use the identity function @{const id}.
›
lemma "SecurityInvariant_withOffendingFlows.set_offending_flows (λ_ _. False)  nodes = {''v1''}, edges={}  id = {}"
by %invisible (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def 
  SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
lemma "SecurityInvariant_withOffendingFlows.set_offending_flows (λ_ _. False) 
   nodes = {''v1'', ''v2''}, edges = {(''v1'', ''v2'')}  id = {}"
by %invisible (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def 
  SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)

text ‹In general, there exists a @{term sinvar} such that the invariant does not hold and no offending flows exits.›
  lemma "sinvar. ¬ sinvar G nP  SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP = {}"
  apply(simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
    SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
  apply(rule_tac x="(λ_ _. False)" in exI)
  apply(simp)
  done


text‹Thus, we introduce usefulness properties that prohibits such useless invariants.›
text‹We summarize them in an invariant.
It requires the following: 
\begin{enumerate}
  \item The offending flows are always defined.
  \item The invariant is monotonic, i.e. prohibiting more is more secure.
  \item And, the (non-minimal) offending flows are monotonic, i.e. prohibiting more solves more security issues.
\end{enumerate}

Later, we will show that is suffices to show that the invariant is monotonic. The other two properties can be derived.
›

  locale SecurityInvariant_preliminaries = SecurityInvariant_withOffendingFlows sinvar
    for sinvar
    +
    assumes 
      defined_offending:
      " wf_graph G; ¬ sinvar G nP   set_offending_flows G nP  {}"
    and
      mono_sinvar:
      " wf_graph  nodes = N, edges = E ; E'  E; sinvar  nodes = N, edges = E  nP   
        sinvar  nodes = N, edges = E'  nP"
    and mono_offending:
      " wf_graph G; is_offending_flows ff G nP   is_offending_flows (ff  f') G nP"
  begin

  text ‹
    \begin{small}
    To instantiate a @{const SecurityInvariant_preliminaries}, here are some hints: 
    Have a look at the TopoS_withOffendingFlows.thy› file.
    There is a definition of @{prop sinvar_mono}. It impplies @{prop mono_sinvar} and @{prop mono_offending}
    apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_sinvar_mono[OF sinvar_mono])
    apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])›
  
    In addition, SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono]› gives a nice proof rule for
    @{prop defined_offending}
  
    Basically, sinvar_mono.› implies almost all assumptions here and is equal to @{prop mono_sinvar}.
    \end{small}
›
  end


subsection‹Security Invariants with secure auto-completion of host attribute mappings›

text‹
We will now add a new artifact to the Security Invariant.
It is a secure default host attribute, we will use the symbol ⊥›.

The newly introduced Boolean receiver_violation› tells whether a security violation happens at the sender's or the receiver's side.

The details can be looked up in \cite{diekmann2014forte}. 
›

  ― ‹Some notes about the notation:
          @{term "fst ` F"} means to apply the function @{const "fst"} to the set @{term "F"} element-wise.
          Example: If @{term "F"} is a set of directed edges, 
          @{term "F  edges G"}, then @{term "fst ` F"}
          is the set of senders and @{term "snd ` f"} the set of receivers.›

  locale SecurityInvariant = SecurityInvariant_preliminaries sinvar
    for sinvar::"('v::vertex) graph  ('v::vertex  'a)  bool"
    +
    fixes default_node_properties :: "'a" ("") 
    and receiver_violation :: "bool"
    assumes 
      ― ‹default value can never fix a security violation.›
      ― ‹Idea: Assume there is a violation, then there is some offending flow. 
        @{text receiver_violation} defines whether the violation happens at the sender's or the receiver's side. 
        We call the place of the violation the \emph{offending host}. 
        We replace the host attribute of the offending host with the default attribute. 
        Giving an offending host, a \emph{secure} default attribute does not change whether the invariant holds.
        I.e.\ this reconfiguration does not remove information, thus preserves all security critical information.
        Thought experiment preliminaries: Can a default configuration ever solve an existing security violation? NO!
        Thought experiment 1: admin forgot to configure host, hence it is handled by default configuration value ...
        Thought experiment 2: new node (attacker) is added to the network. What is its default configuration value ...›
      default_secure:
      " wf_graph G; ¬ sinvar G nP; F  set_offending_flows G nP  
        (¬ receiver_violation  i  fst ` F  ¬ sinvar G (nP(i := ))) 
        (receiver_violation  i  snd ` F  ¬ sinvar G (nP(i := )))"
      and
      default_unique:
      "otherbot    
         (G::('v::vertex) graph) nP i F. wf_graph G  ¬ sinvar G nP  F  set_offending_flows G nP  
         sinvar (delete_edges G F) nP 
         (¬ receiver_violation  i  fst ` F  sinvar G (nP(i := otherbot))) 
         (receiver_violation  i  snd ` F  sinvar G (nP(i := otherbot))) "
   begin
    ― ‹Removes option type, replaces with default host attribute›
    fun node_props :: "('v, 'a) TopoS_Params  ('v  'a)" where
    "node_props P = (λ i. (case (node_properties P) i of Some property  property | None  ))"

    definition node_props_formaldef :: "('v, 'a) TopoS_Params  ('v  'a)" where
    "node_props_formaldef P 
    (λ i. (if i  dom (node_properties P) then the (node_properties P i) else ))"

    lemma node_props_eq_node_props_formaldef: "node_props_formaldef = node_props"
     by(simp add: fun_eq_iff node_props_formaldef_def option.case_eq_if domIff)

    text‹
      Checking whether a security invariant holds.
      \begin{enumerate}
        \item check that the policy @{term G} is syntactically valid
        \item check the security invariant @{term sinvar}
      \end{enumerate}
›
    definition eval::"'v graph  ('v, 'a) TopoS_Params  bool" where
    "eval G P  wf_graph G  sinvar G (node_props P)"


    lemma unique_common_math_notation:
    assumes "G nP i F. wf_graph (G::('v::vertex) graph)  ¬ sinvar G nP  F  set_offending_flows G nP  
         sinvar (delete_edges G F) nP  
         (¬ receiver_violation  i  fst ` F  ¬ sinvar G (nP(i := otherbot))) 
         (receiver_violation  i  snd ` F  ¬ sinvar G (nP(i := otherbot)))"
    shows "otherbot = "
    apply(rule ccontr)
    apply(drule default_unique)
    using assms by blast
   end

print_locale! SecurityInvariant



subsection‹Information Flow Security and Access Control›
text@{term receiver_violation} defines the offending host. Thus, it defines when the violation happens. 

We found that this coincides with the invariant's security strategy. 

\begin{description}
\item[ACS] If the violation happens at the sender, we have an access control strategy (\emph{ACS}). 
I.e.\ the sender does not have the appropriate rights to initiate the connection.

\item[IFS] If the violation happens at the receiver, we have an information flow security strategy (\emph{IFS})
I.e.\ the receiver lacks the appropriate security level to retrieve the (confidential) information. 
The violations happens only when the receiver reads the data.
\end{description}

We refine our @{term SecurityInvariant} locale.
›

subsection ‹Information Flow Security Strategy (IFS)›
  locale SecurityInvariant_IFS = SecurityInvariant_preliminaries sinvar
      for sinvar::"('v::vertex) graph  ('v::vertex  'a)  bool"
      +
      fixes default_node_properties :: "'a" ("") 
      assumes  default_secure_IFS:
        " wf_graph G; f  set_offending_flows G nP  
          i  snd` f. ¬ sinvar G (nP(i := ))"
      and
      ― ‹If some otherbot fulfills @{text default_secure}, it must be @{term ""} 
             Hence, @{term ""} is uniquely defined›
      default_unique_IFS:
      "(G f nP i. wf_graph G  f  set_offending_flows G nP  i  snd` f 
                 ¬ sinvar G (nP(i := otherbot)))  otherbot = "
      begin
        lemma default_unique_EX_notation: "otherbot    
           G nP i f. wf_graph G  ¬ sinvar G nP  f  set_offending_flows G nP  
           sinvar (delete_edges G f) nP 
           (i  snd` f  sinvar G (nP(i := otherbot)))"
          apply(erule contrapos_pp)
          apply(simp)
          using default_unique_IFS SecurityInvariant_withOffendingFlows.valid_without_offending_flows offending_notevalD
          by metis
      end
  
  sublocale SecurityInvariant_IFS  SecurityInvariant where receiver_violation=True
  apply(unfold_locales)
   apply(simp add: default_secure_IFS)
  apply(simp only: HOL.simp_thms)
  apply(drule default_unique_EX_notation)
  apply(assumption)
  done

  (*other direction*)
  locale SecurityInvariant_IFS_otherDirectrion = SecurityInvariant where receiver_violation=True
  sublocale SecurityInvariant_IFS_otherDirectrion  SecurityInvariant_IFS
  apply(unfold_locales)
   apply (metis default_secure offending_notevalD)
  apply(erule contrapos_pp)
  apply(simp)
  apply(drule default_unique)
  apply(simp)
  apply(blast)
  done
  

lemma default_uniqueness_by_counterexample_IFS:
  assumes "(G F nP i. wf_graph G  F  SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP  i  snd` F 
                 ¬ sinvar G (nP(i := otherbot)))"
  and "otherbot  default_value 
    G nP i F. wf_graph G  ¬ sinvar G nP  F  (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP) 
       sinvar (delete_edges G F) nP 
        i  snd ` F  sinvar G (nP(i := otherbot)) "
   shows "otherbot = default_value"
   using assms by blast


subsection ‹Access Control Strategy (ACS)›
  locale SecurityInvariant_ACS = SecurityInvariant_preliminaries sinvar
      for sinvar::"('v::vertex) graph  ('v::vertex  'a)  bool"
      +
      fixes default_node_properties :: "'a" ("") 
      assumes  default_secure_ACS:
        " wf_graph G; f  set_offending_flows G nP  
          i  fst` f. ¬ sinvar G (nP(i := ))"
      and
      default_unique_ACS:
      "(G f nP i. wf_graph G  f  set_offending_flows G nP  i  fst` f 
                 ¬ sinvar G (nP(i := otherbot)))  otherbot = "
      begin
        lemma default_unique_EX_notation: "otherbot    
           G nP i f. wf_graph G  ¬ sinvar G nP  f  set_offending_flows G nP  
           sinvar (delete_edges G f) nP 
           (i  fst` f  sinvar G (nP(i := otherbot)))"
          apply(erule contrapos_pp)
          apply(simp)
          using default_unique_ACS SecurityInvariant_withOffendingFlows.valid_without_offending_flows offending_notevalD
          by metis
      end
  
  sublocale SecurityInvariant_ACS  SecurityInvariant where receiver_violation=False
  apply(unfold_locales)
   apply(simp add: default_secure_ACS)
  apply(simp only: HOL.simp_thms)
  apply(drule default_unique_EX_notation)
  apply(assumption)
  done


  (*other direction*)
  locale SecurityInvariant_ACS_otherDirectrion = SecurityInvariant where receiver_violation=False
  sublocale SecurityInvariant_ACS_otherDirectrion  SecurityInvariant_ACS
  apply(unfold_locales)
   apply (metis default_secure offending_notevalD)
  apply(erule contrapos_pp)
  apply(simp)
  apply(drule default_unique)
  apply(simp)
  apply(blast)
  done


lemma default_uniqueness_by_counterexample_ACS:
  assumes "(G F nP i. wf_graph G  F  SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP  i  fst ` F 
                 ¬ sinvar G (nP(i := otherbot)))"
  and "otherbot  default_value 
    G nP i F. wf_graph G  ¬ sinvar G nP  F  (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP) 
       sinvar (delete_edges G F) nP 
        i  fst ` F  sinvar G (nP(i := otherbot))"
  shows "otherbot = default_value"
  using assms by blast


text‹The sublocale relationships tell that the simplified @{const SecurityInvariant_ACS} and @{const SecurityInvariant_IFS} 
  assumptions suffice to do tho generic SecurityInvariant assumptions.›

end

Theory TopoS_withOffendingFlows

theory TopoS_withOffendingFlows
imports TopoS_Interface
begin


section @{term SecurityInvariant} Instantiation Helpers›

text‹
  The security invariant locales are set up hierarchically to ease instantiation proofs.
  The first locale, @{term SecurityInvariant_withOffendingFlows} has no assumptions, thus instantiations is for free. 
  The first step focuses on monotonicity,
›



context SecurityInvariant_withOffendingFlows
begin
  text‹We define the monotonicity of sinvar›:
  
  @{term "( nP N E' E. wf_graph  nodes = N, edges = E    E'  E  sinvar  nodes = N, edges = E  nP  sinvar  nodes = N, edges = E'  nP )"}
  
  Having a valid invariant, removing edges retains the validity. I.e.\ prohibiting more, is more or equally secure.
›

  definition sinvar_mono :: "bool" where
    "sinvar_mono  ( nP N E' E. 
      wf_graph  nodes = N, edges = E   
      E'  E  
      sinvar  nodes = N, edges = E  nP  sinvar  nodes = N, edges = E'  nP )"

  text‹
    If one can show @{const sinvar_mono}, then the instantiation of the @{term SecurityInvariant_preliminaries} locale is tremendously simplified. 
›

  lemma sinvar_mono_I_proofrule_simple: 
  " ( G nP. sinvar G nP = ( (e1, e2)  edges G. P e1 e2 nP) )   sinvar_mono"
  apply(simp add: sinvar_mono_def)
  apply(clarify)
  apply(fast)
  done

  lemma sinvar_mono_I_proofrule:
  " ( nP (G:: 'v graph). sinvar G nP = ( (e1, e2)  edges G. P e1 e2 nP G) ); 
    ( nP e1 e2 N E' E. 
      wf_graph  nodes = N, edges = E   
      (e1,e2)  E  
      E'  E  
      P e1 e2 nP nodes = N, edges = E  P e1 e2 nP nodes = N, edges = E')   sinvar_mono"
  unfolding sinvar_mono_def
  proof(clarify)
    fix nP N E' E
    assume AllForm: "( nP (G:: 'v graph). sinvar G nP = ( (e1, e2)  edges G. P e1 e2 nP G) )"
    and Pmono: "nP e1 e2 N E' E. wf_graph  nodes = N, edges = E   (e1,e2)  E  E'  E  P e1 e2 nP nodes = N, edges = E  P e1 e2 nP nodes = N, edges = E'"
    and wfG: "wf_graph nodes = N, edges = E"
    and E'subset: "E'  E"
    and evalE: "sinvar nodes = N, edges = E nP"
    
    from Pmono have Pmono1: 
      "nP N E' E. wf_graph  nodes = N, edges = E   E'  E  ((e1,e2)  E. P e1 e2 nP nodes = N, edges = E  P e1 e2 nP nodes = N, edges = E')" 
    by blast

    from AllForm have "sinvar nodes = N, edges = E nP = ( (e1, e2)  E. P e1 e2 nP nodes = N, edges = E)" by force
    from this evalE have "( (e1, e2)  E. P e1 e2 nP nodes = N, edges = E)" by simp
    from Pmono1[OF wfG E'subset, of "nP"] this have "(e1, e2)  E. P e1 e2 nP nodes = N, edges = E'" by fast
    from this E'subset have "(e1, e2)  E'. P e1 e2 nP nodes = N, edges = E'" by fast
    from this have "(e1, e2)  (edges nodes = N, edges = E'). P e1 e2 nP nodes = N, edges = E'" by simp
    from this AllForm show "sinvar nodes = N, edges = E' nP" by presburger
  qed
 

   text‹Invariant violations do not disappear if we add more flows.›
   lemma sinvar_mono_imp_negative_mono:
   "sinvar_mono  wf_graph  nodes = N, edges = E    E'  E 
   ¬ sinvar  nodes = N, edges = E'  nP  ¬ sinvar  nodes = N, edges = E  nP"
   unfolding sinvar_mono_def by(blast)

  corollary sinvar_mono_imp_negative_delete_edge_mono:
   "sinvar_mono  wf_graph G  X  Y  ¬ sinvar (delete_edges G Y) nP  ¬ sinvar (delete_edges G X) nP "
  proof -
   assume sinvar_mono
   and "wf_graph G" and "X  Y" and "¬ sinvar (delete_edges G Y) nP"
   from delete_edges_wf[OF ‹wf_graph G] have valid_G_delete: "wf_graph nodes = nodes G, edges = edges G - X" by(simp add: delete_edges_simp2)
   from X  Y have "edges G - Y  edges G - X" by blast
   with ‹sinvar_mono› sinvar_mono_def valid_G_delete have
    "sinvar nodes = nodes G, edges = edges G - X nP  sinvar nodes = nodes G, edges = edges G - Y nP" by blast
   hence "sinvar (delete_edges G X) nP  sinvar (delete_edges G Y) nP" by(simp add: delete_edges_simp2)
   with ¬ sinvar (delete_edges G Y) nP show ?thesis by blast
  qed


  (*lemma mono_offending_flows_min_set:
  assumes mono_isoffending: "(∀ ff f' G nP. is_offending_flows ff G nP ⟶ is_offending_flows (f' ∪ ff) G nP)"
  and offending: "is_offending_flows_min_set As G nP"
  shows "sinvar (delete_edges G (As ∪ Bs)) nP"
  proof -
    from offending have "is_offending_flows As G nP" using is_offending_flows_min_set_def by simp
    from mono_isoffending this have "is_offending_flows (Bs ∪ As) G nP" by simp
    hence "is_offending_flows (As ∪ Bs) G nP" by (metis Un_commute)
    from this is_offending_flows_def show ?thesis by simp
  qed*)


  (*use this to show locale preliminaries from mono*)
  lemma sinvar_mono_imp_is_offending_flows_mono:
  assumes mono: "sinvar_mono"
  and wfG: "wf_graph G"
  shows "is_offending_flows FF G nP   is_offending_flows (FF  F) G nP"
  proof -
    from wfG have wfG': "wf_graph nodes = nodes G, edges = {(e1, e2). (e1, e2)  edges G  (e1, e2)  FF}" 
      by (metis delete_edges_def delete_edges_wf)
    from mono have sinvarE: "( nP N E' E. wf_graph  nodes = N, edges = E   E'  E  sinvar  nodes = N, edges = E  nP  sinvar  nodes = N, edges = E'  nP )"
      unfolding sinvar_mono_def
      by metis
    have " G FF F. {(e1, e2). (e1, e2)  edges G  (e1, e2)  FF  (e1, e2)  F}  {(e1, e2). (e1, e2)  edges G  (e1, e2)  FF} "
      by(rule Collect_mono) (simp)
    from sinvarE[OF wfG' this]
    show "is_offending_flows FF G nP  is_offending_flows (FF  F) G nP"
      by(simp add: is_offending_flows_def delete_edges_def)
  qed

  (*use this to show locale sinvar_mono*)
  lemma sinvar_mono_imp_sinvar_mono: 
  "sinvar_mono  wf_graph  nodes = N, edges = E   E'  E  sinvar  nodes = N, edges = E  nP  
        sinvar  nodes = N, edges = E'  nP"
  apply(simp add: sinvar_mono_def)
  by blast

end



subsection ‹Offending Flows Not Empty Helper Lemmata›
context SecurityInvariant_withOffendingFlows
begin
  text ‹Give an over-approximation of offending flows (e.g. all edges) and get back a
          minimal set›
  (*offending_overapproximation keepingInOffendingApproximation G nP*)
  fun minimalize_offending_overapprox :: "('v × 'v) list  ('v × 'v) list  
  'v graph  ('v  'a)  ('v × 'v) list" where
  "minimalize_offending_overapprox [] keep _ _ = keep" |
  "minimalize_offending_overapprox (f#fs) keep G nP = (if sinvar (delete_edges_list G (fs@keep)) nP then
      minimalize_offending_overapprox fs keep G nP 
    else
      minimalize_offending_overapprox fs (f#keep) G nP
    )"



  text‹The graph we check in @{const minimalize_offending_overapprox},
  @{term "G minus (fs  keep)"} is the graph from the offending_flows_min_set› condition.
  We add @{term f} and remove it.›
 

  (*lemma minimalize_offending_overapprox_not_in: 
  "f ∉ set fs ⟹ f ∉ set keep ⟹ f ∉ set (minimalize_offending_overapprox fs keep G nP)"
   apply(induction fs arbitrary: keep)
    by(simp_all)*)




  (*lemma offending_min_set_ab_in_fs: "wf_graph (G::'v graph) ⟹ (a,b) ∈ edges G ⟹
       is_offending_flows_min_set ({(a, b)} ∪ fs) G nP ⟹
       sinvar (delete_edges G fs) nP ⟹
       (a,b) ∈ fs"
  apply(rule ccontr)
  apply(simp add: is_offending_flows_min_set_def)
  apply(clarify)
  apply(simp add: add_delete_edges)
  done*)


  lemma minimalize_offending_overapprox_subset:
  "set (minimalize_offending_overapprox ff keeps G nP)  set ff  set keeps"
   proof(induction ff arbitrary: keeps)
   case Nil
    thus ?case by simp
   next
   case (Cons a ff)
    from Cons have case1: "(sinvar (delete_edges_list G (ff @ keeps)) nP 
     set (minimalize_offending_overapprox ff keeps G nP)  insert a (set ff  set keeps))" 
      by blast
     from Cons have case2: "(¬ sinvar (delete_edges_list G (ff @ keeps)) nP 
     set (minimalize_offending_overapprox ff (a # keeps) G nP)  insert a (set ff  set keeps))"
      by fastforce
    from case1 case2 show ?case by simp
   qed



  lemma not_model_mono_imp_addedge_mono: 
  assumes mono: "sinvar_mono"
   and vG: "wf_graph G" and ain: "(a1,a2)  edges G" and xy: "X  Y" and ns: "¬ sinvar (add_edge a1 a2 (delete_edges G (Y))) nP"  
  shows "¬ sinvar (add_edge a1 a2 (delete_edges G X)) nP"
   proof -
      have wf_graph_add_delete_edge_simp: 
        "Y. add_edge a1 a2 (delete_edges G Y) = (delete_edges G (Y - {(a1,a2)}))"
        apply(simp add: delete_edges_simp2 add_edge_def)
        apply(rule conjI)
         using ain apply (metis insert_absorb vG wf_graph.E_wfD(1) wf_graph.E_wfD(2))
         apply(auto simp add: ain)
        done
      from this ns have 1: "¬ sinvar (delete_edges G (Y - {(a1, a2)})) nP" by simp
      have 2: "X - {(a1, a2)}  Y - {(a1, a2)}" by (metis Diff_mono subset_refl xy)
      from sinvar_mono_imp_negative_delete_edge_mono[OF mono] vG have
        "X Y. X  Y  ¬ sinvar (delete_edges G Y) nP  ¬ sinvar (delete_edges G X) nP" by blast
      from this[OF 2 1] have "¬ sinvar (delete_edges G (X - {(a1, a2)})) nP" by simp
      from this wf_graph_add_delete_edge_simp[symmetric] show ?thesis by simp
   qed


  theorem is_offending_flows_min_set_minimalize_offending_overapprox:
      assumes mono: "sinvar_mono"
      and vG: "wf_graph G" and iO: "is_offending_flows (set ff) G nP" and sF: "set ff  edges G" and dF: "distinct ff"
      shows "is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP"
              (is "is_offending_flows_min_set ?minset G nP")
  proof -
    from iO have "sinvar (delete_edges G (set ff)) nP" by (metis is_offending_flows_def)

    ― ‹@{term "sinvar"} holds if we delete @{term "ff"}.
        With the following generalized statement, we show that it also holds if we delete @{term "minimalize_offending_overapprox ff []"}
    { 
      fix keeps
      ― ‹Generalized for arbitrary @{term keeps}
        have "sinvar (delete_edges G (set ff  set keeps)) nP  
          sinvar (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP))) nP"
         apply(induction ff arbitrary: keeps)
          apply(simp)
         apply(simp)
         apply(rule impI)
         apply(simp add:delete_edges_list_union)
         done
    } 
    ― ‹@{term "keeps = []"}
    note minimalize_offending_overapprox_maintains_evalmodel=this[of "[]"]


    from sinvar (delete_edges G (set ff)) nP minimalize_offending_overapprox_maintains_evalmodel have
      "sinvar (delete_edges G ?minset) nP" by simp
    hence 1: "is_offending_flows ?minset G nP" by (metis iO is_offending_flows_def)

    txt‹We need to show minimality of @{term "minimalize_offending_overapprox ff []"}.
      Minimality means @{term "(e1, e2)?minset. ¬ sinvar (add_edge e1 e2 (delete_edges G ?minset)) nP"}.
      We show the following generalized fact.
›
    {
      fix ff keeps
      have " x  set ff. x  set keeps 
         x  set ff. x  edges G 
        distinct ff 
        (e1, e2) set keeps.
           ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP)))) nP 
        (e1, e2)set (minimalize_offending_overapprox ff keeps G nP).
           ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP)))) nP"
       proof(induction ff arbitrary: keeps)
       case Nil
        from Nil show ?case by(simp)
       next
       case (Cons a ff)
        assume not_in_keeps: "xset (a # ff). x  set keeps"
          hence a_not_in_keeps: "a  set keeps" by simp
        assume in_edges: "xset (a # ff). x  edges G"
          hence ff_in_edges: "xset ff. x  edges G" and a_in_edges: "a  edges G" by simp_all
        assume distinct: "distinct (a # ff)"
          hence ff_distinct: "distinct ff" and a_not_in_ff: "a  set ff "by simp_all
        assume minimal: "(e1, e2)set keeps. 
          ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
        
        
        have delete_edges_list_union_insert: " f fs keep. delete_edges_list G (f#fs@keep) = delete_edges G ({f}  set fs  set keep)"
        by(simp add: graph_ops delete_edges_list_set)

        let ?goal="?case" ― ‹we show this by case distinction›
        show ?case
        proof(cases "sinvar (delete_edges_list G (ff@keeps)) nP")
        case True 
          from True have "sinvar (delete_edges_list G (ff@keeps)) nP" .
          from this Cons show ?goal using delete_edges_list_union by simp
        next
        case False
          (*MONO=Cons.prems(1)"*)
           { ― ‹a lemma we only need once here›
              fix a ff keeps
              assume mono: "sinvar_mono" and ankeeps: "a  set keeps"
              and anff: "a  set ff" and aE: "a  edges G"
              and nsinvar: "¬ sinvar (delete_edges_list G (ff @ keeps)) nP"
              have "¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
              proof -
                { fix F Fs keep
                  from vG have "F  edges G  F  set Fs  F  set keep 
                    (add_edge (fst F) (snd F) (delete_edges_list G (F#Fs@keep))) = (delete_edges_list G (Fs@keep))"
                  apply(simp add:delete_edges_list_union delete_edges_list_union_insert)
                  apply(simp add: graph_ops)
                  apply(rule conjI)
                   apply(simp add: wf_graph_def)
                   apply blast
                  apply(simp add: wf_graph_def)
                  by fastforce
                } note delete_edges_list_add_add_iff=this
                from aE have "(fst a, snd a)  edges G" by simp
                from delete_edges_list_add_add_iff[of a ff keeps] have
                  "delete_edges_list G (ff @ keeps) = add_edge (fst a) (snd a) (delete_edges_list G (a # ff @ keeps))"
                  by (metis aE anff ankeeps)
                from this nsinvar have "¬ sinvar (add_edge (fst a) (snd a) (delete_edges_list G (a # ff @ keeps))) nP" by simp
                from this delete_edges_list_union_insert have 1:
                  "¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (insert a (set ff  set keeps)))) nP" by (metis insert_is_Un sup_assoc)
            
                from minimalize_offending_overapprox_subset[of "ff" "a#keeps" G nP] have
                  "set (minimalize_offending_overapprox ff (a # keeps) G nP)  insert a (set ff  set keeps)" by simp
            
                from not_model_mono_imp_addedge_mono[OF mono vG (fst a, snd a)  edges G this 1] show ?thesis
                  by (metis minimalize_offending_overapprox.simps(2) nsinvar)
              qed
           } note not_model_mono_imp_addedge_mono_minimalize_offending_overapprox=this
    
          from not_model_mono_imp_addedge_mono_minimalize_offending_overapprox[OF mono a_not_in_keeps a_not_in_ff a_in_edges False] have a_minimal: "
          ¬ sinvar (add_edge (fst a) (snd a) (delete_edges G (set (minimalize_offending_overapprox (a # ff) keeps G nP)))) nP"
          by simp
          from minimal a_minimal
          have a_keeps_minimal: "(e1, e2)set (a # keeps). 
          ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff (a # keeps) G nP)))) nP" 
            using False by fastforce
          from Cons.prems have a_not_in_keeps: "xset ff. x  set (a#keeps)" by auto
          from Cons.IH[OF a_not_in_keeps ff_in_edges ff_distinct a_keeps_minimal] have IH:
            "(e1, e2)set (minimalize_offending_overapprox ff (a # keeps) G nP).
           ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff (a # keeps) G nP)))) nP" .
          
          from False have "¬ sinvar (delete_edges G (set ff  set keeps)) nP " using delete_edges_list_union by metis
          from this have "set (minimalize_offending_overapprox (a # ff) keeps G nP) = 
            set (minimalize_offending_overapprox ff (a#keeps) G nP)"
            by(simp add: delete_edges_list_union)
          from this IH have ?goal by presburger
          thus ?goal .
        qed
      qed
    } note mono_imp_minimalize_offending_overapprox_minimal=this[of ff "[]"]

    from mono_imp_minimalize_offending_overapprox_minimal[OF _ _ dF] sF have 2:
      "(e1, e2)?minset. ¬ sinvar (add_edge e1 e2 (delete_edges G ?minset)) nP"
    by auto
    from 1 2 show ?thesis
      by(simp add: is_offending_flows_def is_offending_flows_min_set_def)
  qed

  corollary mono_imp_set_offending_flows_not_empty:
  assumes mono_sinvar: "sinvar_mono"
  and vG: "wf_graph G" and iO: "is_offending_flows (set ff) G nP" and sS: "set ff  edges G" and dF: "distinct ff"
  shows
    "set_offending_flows G nP  {}"
  proof -
    from iO SecurityInvariant_withOffendingFlows.is_offending_flows_def have nS: "¬ sinvar G nP" by metis
    from sinvar_mono_imp_negative_delete_edge_mono[OF mono_sinvar] have negative_delete_edge_mono: 
      " G nP X Y. wf_graph G  X  Y  ¬ sinvar (delete_edges G (Y)) nP  ¬ sinvar (delete_edges G X) nP" by blast
      
    from is_offending_flows_min_set_minimalize_offending_overapprox[OF mono_sinvar vG iO sS dF] 
     have "is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP" by simp
    from this set_offending_flows_def sS have
      "(set (minimalize_offending_overapprox ff [] G nP))  set_offending_flows G nP"
      using minimalize_offending_overapprox_subset[where keeps="[]"] by fastforce
    thus ?thesis by blast 
   qed


   text‹
   To show that @{const set_offending_flows} is not empty, the previous corollary @{thm mono_imp_set_offending_flows_not_empty} is very useful.
   Just select @{term "set ff = edges G"}.
›



   text‹
   If there exists a security violations,
   there a means to fix it if and only if the network in which nobody communicates with anyone fulfills the security requirement
›
   theorem valid_empty_edges_iff_exists_offending_flows: 
    assumes mono: "sinvar_mono" and wfG: "wf_graph G" and noteval: "¬ sinvar G nP"
    shows "sinvar  nodes = nodes G, edges = {}  nP  set_offending_flows G nP  {}"
   proof 
      assume a: "sinvar  nodes = nodes G, edges = {}  nP"
  
      from finite_distinct_list[OF wf_graph.finiteE] wfG
      obtain list_edges where list_edges_props: "set list_edges = edges G  distinct list_edges" by blast
      hence listedges_subseteq_edges: "set list_edges  edges G" by blast
  
      have empty_edge_graph_simp: "(delete_edges G (edges G)) =  nodes = nodes G, edges = {} " by(auto simp add: graph_ops)
      from a is_offending_flows_def noteval list_edges_props empty_edge_graph_simp 
        have overapprox: "is_offending_flows (set list_edges) G nP" by auto
  
      from mono_imp_set_offending_flows_not_empty[OF mono wfG overapprox listedges_subseteq_edges] list_edges_props 
      show "set_offending_flows G nP  {}" by simp
    next
      assume a: "set_offending_flows G nP  {}"
  
      from a obtain f where f_props: "f  edges G  is_offending_flows_min_set f G nP" using set_offending_flows_def by fastforce
  
      from f_props have "sinvar (delete_edges G f) nP" using is_offending_flows_min_set_def is_offending_flows_def by simp
        hence evalGf: "sinvar nodes = nodes G, edges = {(e1, e2). (e1, e2)  edges G  (e1, e2)  f} nP" by(simp add: delete_edges_def)
      from delete_edges_wf[OF wfG, unfolded delete_edges_def] 
        have wfGf: "wf_graph nodes = nodes G, edges = {(e1, e2). (e1, e2)  edges G  (e1, e2)  f}" by simp
      have emptyseqGf: "{}   {(e1, e2). (e1, e2)  edges G  (e1, e2)  f}" by simp
  
      from mono[unfolded sinvar_mono_def] evalGf wfGf emptyseqGf have "sinvar nodes = nodes G, edges = {} nP" by blast
      thus "sinvar nodes = nodes G, edges = {} nP" .
  qed



  text@{const minimalize_offending_overapprox} not only computes a set where @{const is_offending_flows_min_set} holds, but it also returns a subset of the input.
›
  lemma minimalize_offending_overapprox_keeps_keeps: "(set keeps)  set (minimalize_offending_overapprox ff keeps G nP)"
    proof(induction ff keeps G nP rule: minimalize_offending_overapprox.induct)
    qed(simp_all)

  lemma minimalize_offending_overapprox_subseteq_input: "set (minimalize_offending_overapprox ff keeps G nP)  (set ff)  (set keeps)"
    proof(induction ff keeps G nP rule: minimalize_offending_overapprox.induct)
    case 1 thus ?case by simp
    next
    case 2 thus ?case by(simp add: delete_edges_list_set delete_edges_simp2) blast
    qed

end




context SecurityInvariant_preliminaries
  begin
    text@{const sinvar_mono} naturally holds in @{const SecurityInvariant_preliminaries}
    lemma sinvar_monoI: "sinvar_mono"
      unfolding sinvar_mono_def using mono_sinvar by blast

    text‹Note: due to monotonicity, the minimality also holds for arbitrary subsets›
    lemma assumes "wf_graph G" and "is_offending_flows_min_set F G nP" and "F  edges G" and "E  F" and "E  {}"
          shows "¬ sinvar  nodes = nodes G, edges = ((edges G) - F)  E  nP"
    proof -
      from sinvar_mono_imp_negative_delete_edge_mono[OF sinvar_monoI ‹wf_graph G] have negative_delete_edge_mono: 
      "X Y. X  Y  ¬ sinvar  nodes = nodes G, edges = (edges G) - Y  nP  ¬ sinvar  nodes = nodes G, edges = edges G - X  nP"
        using delete_edges_simp2 by metis
      from assms(2) have "((e1, e2)F. ¬ sinvar (add_edge e1 e2 (delete_edges G F)) nP)"
      unfolding is_offending_flows_min_set_def by simp
      with ‹wf_graph G have min: "((e1, e2)F. ¬ sinvar  nodes = nodes G, edges = ((edges G) - F)  {(e1,e2)}  nP)"
        apply(simp add: delete_edges_simp2 add_edge_def)
        apply(rule, rename_tac x, case_tac x, rename_tac e1 e2, simp)
        apply(erule_tac x="(e1, e2)" in ballE)
         apply(simp_all)
        apply(subgoal_tac "insert e1 (insert e2 (nodes G)) = nodes G")
         apply(simp)
        by (metis assms(3) insert_absorb rev_subsetD wf_graph.E_wfD(1) wf_graph.E_wfD(2))
      from E  {} obtain e where "e  E" by blast
      with min E  F have mine: "¬ sinvar  nodes = nodes G, edges = ((edges G) - F)  {e}  nP" by fast
      have e1: "edges G - (F - {e}) = insert e (edges G - F)" using DiffD2 e  E assms(3) assms(4) by auto 
      have e2: "edges G - (F - E) = ((edges G) - F)  E" using assms(3) assms(4) by auto 
      from negative_delete_edge_mono[where Y="F - {e}" and X="F - E"] e  E have
      "¬ sinvar nodes = nodes G, edges = edges G - (F - {e}) nP  ¬ sinvar nodes = nodes G, edges = edges G - (F - E) nP" by blast
      with mine e1 e2 show ?thesis by simp
    qed

    
    text‹The algorithm @{const minimalize_offending_overapprox} is correct›
    lemma minimalize_offending_overapprox_sound: 
      " wf_graph G; is_offending_flows (set ff) G nP; set ff  edges G; distinct ff 
         is_offending_flows_min_set (set (minimalize_offending_overapprox ff [] G nP)) G nP "
    using is_offending_flows_min_set_minimalize_offending_overapprox sinvar_monoI by blast

    text‹
      If @{term "¬ sinvar G nP"}
      Given a list ff, (ff is distinct and a subset of G's edges)
      such that sinvar (V, E - ff) nP›
      @{const minimalize_offending_overapprox} minimizes ff such that we get an offending flows
      Note: choosing ff = edges G is a good choice!
›
    theorem minimalize_offending_overapprox_gives_back_an_offending_flow:
      " wf_graph G; is_offending_flows (set ff) G nP; set ff  edges G; distinct ff 
        
         (set (minimalize_offending_overapprox ff [] G nP))  set_offending_flows G nP"
    apply(frule(3) minimalize_offending_overapprox_sound)
    apply(simp add: set_offending_flows_def)
    using minimalize_offending_overapprox_subseteq_input[where keeps="[]", simplified] by blast


    (*TODO better minimality condition for keeps*)
    (*lemma  minimalize_offending_overapprox_sound_fixKeep:
      "⟦ wf_graph G; is_offending_flows (set (ff @ keeps)) G nP; ∀ x ∈ set ff. x ∉ set keeps; ∀ x ∈ set ff. x ∈ edges G; distinct ff; 
        ∀(e1, e2)∈ set keeps. ¬ sinvar (add_edge e1 e2 (delete_edges G (set (minimalize_offending_overapprox ff keeps G nP)))) nP ⟧
        ⟹
         is_offending_flows_min_set (set (minimalize_offending_overapprox ff keeps G nP)) G nP ∧ set keeps ⊆ (set (minimalize_offending_overapprox ff keeps G nP))"
       apply(rule conjI)
        apply(simp only: is_offending_flows_min_set_def)
        apply(rule conjI)
         apply(simp add: is_offending_flows_def is_offending_flows_min_set_def)
         apply(simp add:minimalize_offending_overapprox_maintains_evalmodel)
        apply(rule mono_imp_minimalize_offending_overapprox_minimal)
             apply (metis sinvar_monoI sinvar_mono_imp_negative_delete_edge_mono)
            apply(simp)
           apply(simp)
          apply(simp)
         apply(simp)
        apply(simp)
          
       apply(thin_tac "?x")+
       apply(induction ff keeps G nP rule: minimalize_offending_overapprox.induct)
        apply(simp_all)
      done*)

    
end


text‹A version which acts on configured security invariants.
      I.e. there is no type @{typ 'a} for the host attributes in it.›
fun minimalize_offending_overapprox :: "('v graph  bool)  ('v × 'v) list  ('v × 'v) list  
'v graph ('v × 'v) list" where
"minimalize_offending_overapprox _ [] keep _ = keep" |
"minimalize_offending_overapprox m (f#fs) keep G = (if m (delete_edges_list G (fs@keep)) then
    minimalize_offending_overapprox m fs keep G
  else
    minimalize_offending_overapprox m fs (f#keep) G
  )"

lemma minimalize_offending_overapprox_boundnP:
shows "minimalize_offending_overapprox (λG. m G nP) fs keeps G =
         SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox m fs keeps G nP"
  apply(induction fs arbitrary: keeps)
   apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps; fail)
  apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps)
  done

context SecurityInvariant_withOffendingFlows
begin

    text‹If there is a violation and there are no offending flows, there does not exist a possibility to fix the violation by 
          tightening the policy. @{thm valid_empty_edges_iff_exists_offending_flows} already hints this.›
    lemma mono_imp_emptyoffending_eq_nevervalid:
       " sinvar_mono; wf_graph G; ¬ sinvar G nP; set_offending_flows G nP = {}  
        ¬ ( F  edges G. sinvar (delete_edges G F) nP)"
    proof -
      assume mono: "sinvar_mono"
      and wfG: "wf_graph G"
      and a1:  "¬ sinvar G nP"
      and a2: "set_offending_flows G nP = {}"

      from wfG have wfG': "wf_graph nodes = nodes G, edges = edges G" by(simp add:wf_graph_def)

      from a2 set_offending_flows_def have "f  edges G. ¬ is_offending_flows_min_set f G nP" by simp
      from this is_offending_flows_min_set_def is_offending_flows_def a1 have notdeleteconj:
        "f  edges G. 
          ¬ sinvar (delete_edges G f) nP  
          ¬ (((e1, e2)f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP))" 
      by simp
      have "fedges G. ¬ sinvar (delete_edges G f) nP"
      proof (rule allI, rule impI)
        fix f
        assume "f  edges G"
        from this notdeleteconj have 
         "¬ sinvar (delete_edges G f) nP  
          ¬ (((e1, e2)f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP))" by simp
        from this show "¬ sinvar (delete_edges G f) nP"
          proof
            assume "¬ sinvar (delete_edges G f) nP" thus "¬ sinvar (delete_edges G f) nP" .
          next
            assume "¬ ((e1, e2)f. ¬ sinvar (add_edge e1 e2 (delete_edges G f)) nP)"
            hence "(e1,e2)f. sinvar (add_edge e1 e2 (delete_edges G f)) nP" by(auto)
            from this obtain e1 e2 where e1e2cond: "(e1,e2)f  sinvar (add_edge e1 e2 (delete_edges G f)) nP" by blast
            
            from f  edges G wfG have "finite f" apply(simp add: wf_graph_def) by (metis rev_finite_subset)
            from this obtain listf where listf: "set listf = f  distinct listf" by (metis finite_distinct_list)

            from e1e2cond f  edges G have Geq:
            "(add_edge e1 e2 (delete_edges G f)) =  nodes = nodes G, edges = edges G - f  {(e1,e2)}"
              apply(simp add: graph_ops wfG')
              apply(clarify)
               using wfG[unfolded wf_graph_def] by force


            from this[symmetric] add_edge_wf[OF delete_edges_wf[OF wfG]] have 
              "wf_graph nodes = nodes G, edges = edges G - f  {(e1, e2)}" by simp
            from mono this  have mono'':
              " E'. E'  edges G - f  {(e1, e2)} 
                sinvar nodes = nodes G, edges = edges G - f  {(e1, e2)} nP  
                sinvar nodes = nodes G, edges = E' nP" unfolding sinvar_mono_def by blast
            
            from e1e2cond Geq have "sinvar  nodes = nodes G, edges = edges G - f  {(e1,e2)} nP" by simp
            from this mono'' have "sinvar  nodes = nodes G, edges = edges G - f nP" by auto
            hence overapprox: "sinvar (delete_edges G f) nP" by (simp add: delete_edges_simp2) 
            (*Interesting, the opposite of what we want to show holds ...*)

            from a1 overapprox have "is_offending_flows f G nP" by(simp add: is_offending_flows_def)
            from this listf have c1: "is_offending_flows (set listf) G nP" by(simp add: is_offending_flows_def)
            from listf f  edges G have c2: "set listf  edges G" by simp

            from mono_imp_set_offending_flows_not_empty[OF mono wfG c1 c2 conjunct2[OF listf]] have 
              "set_offending_flows G nP  {}" .
            from this a2 have "False" by simp
            (*I knew this can't be!*)

            thus "¬ sinvar (delete_edges G f) nP" by simp
          qed
      qed
      thus ?thesis by simp
    qed
end
 

(*
text{* Old version of security invariant gave @{term "F ∈ set_offending_flows G nP"} and @{term "sinvar (delete_edges G F) nP"}
  as assumption for @{text "default_secure"}. We can conclude this from mono. *}
context SecurityInvariant_withOffendingFlows
begin
  lemma mono_exists_offending_flows:
  "⟦ sinvar_mono; wf_graph G; is_offending_flows (set ff) G nP; set ff ⊆ edges G; distinct ff ⟧ 
    ⟹ ∃F. F ∈ set_offending_flows G nP ∧ sinvar (delete_edges G F) nP"
    apply(frule mono_imp_set_offending_flows_not_empty[of G nP ff])
         apply(simp_all add:is_offending_flows_def)
    apply(simp add: set_offending_flows_def)
    apply(erule exE)
    apply(rename_tac exF)
    apply(clarify)
    apply(rule_tac x="exF" in exI)
    apply(rule conjI)
     apply(simp)
    apply(rule conjI)
     apply(simp)
    apply(simp add:is_offending_flows_min_set_def is_offending_flows_def)
  done
end
*)


subsection ‹Monotonicity of offending flows›
  context SecurityInvariant_preliminaries
  begin
  
    (*todo: simplify proof*)
    text‹If there is some @{term "F'"} in the offending flows of a small graph and you have a bigger graph, 
          you can extend @{term "F'"} by some @{term "Fadd"} and minimality in @{term F} is preserved›
    lemma minimality_offending_flows_mono_edges_graph_extend:
    " wf_graph  nodes = V, edges = E ; E'  E; Fadd  E' = {}; F'  set_offending_flows nodes = V, edges = E' nP   
            ((e1, e2)F'. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E  (F'  Fadd))) nP)"
    proof -
      assume a1: "wf_graph  nodes = V, edges = E "
      and    a2: "E'  E"
      and    a3: "Fadd  E' = {}"
      and    a4: "F'  set_offending_flows nodes = V, edges = E' nP"

      from a4 have "F'  E'" by(simp add: set_offending_flows_def)

      obtain Eadd where Eadd_prop: "E'  Eadd = E" and "E'  Eadd = {}" using a2 by blast

      have Fadd_notinE': "Fadd. Fadd  E' = {}   E' - (F'  Fadd) =  E' - F'" by blast
      from F'  E' a1[simplified wf_graph_def] a2 have FinV1: "fst ` F'  V" and FinV2: "snd ` F'  V"
      proof -
        from a1 have "fst ` E  V" by(simp add: wf_graph_def)
        with F'  E' a2 show "fst ` F'  V" by fast
        from a1 have "snd ` E  V" by(simp add: wf_graph_def)
        with F'  E' a2 show "snd ` F'  V" by fast
      qed
      hence insert_e1_e2_V: " (e1, e2)  F'. insert e1 (insert e2 V) = V" by auto
      hence add_edge_F: " (e1, e2)  F'. add_edge e1 e2 nodes = V, edges = E' - F'  =  nodes = V, edges = (E' - F')  {(e1, e2)}"
        by(simp add: add_edge_def)
         
      have Fadd_notinE': "Fadd. Fadd  E' = {}   E' - (F'  Fadd) =  E' - F'" by blast
       from F'  E' this have Fadd_notinF: "Fadd. Fadd  E' = {}   F'  Fadd = {}" by blast
 
      have Fadd_subseteq_Eadd: "Fadd. (Fadd  E' = {}  Fadd  E) = (Fadd  Eadd)"
        proof(rule iffI, goal_cases)
        case 1 thus ?case using Eadd_prop a2 by blast
        next
        case 2 thus ?case using Eadd_prop a2 E'  Eadd = {} by blast
        qed
 
      from a4 have "((e1, e2)F'. ¬ sinvar (add_edge e1 e2 nodes = V, edges = E' - F') nP)"
        by(simp add: set_offending_flows_def is_offending_flows_min_set_def delete_edges_simp2)
      with add_edge_F have noteval_F: "(e1, e2)F'. ¬ sinvar nodes = V, edges = (E' - F')  {(e1, e2)} nP"
        by fastforce 

      (*proof rule that preserves the tuple*)
      have tupleBallI: "A P. (e1 e2. (e1, e2)A  P (e1, e2))  ALL (e1, e2):A. P (e1, e2)" by force
      have "(e1, e2)F'. ¬ sinvar nodes = V, edges = (E - (F'  Fadd))  {(e1, e2)} nP"
      proof(rule tupleBallI)
        fix e1 e2
        assume f2: "(e1, e2)  F'"
           with a3 have gFadd1: "¬ sinvar nodes = V, edges = (E' - (F'  Fadd))  {(e1, e2)} nP"
           using Fadd_notinE' noteval_F by fastforce
     
           from a1 FinV1 FinV2 a3 f2 have gFadd2: 
             "wf_graph nodes = V, edges = (E - (F'  Fadd))  {(e1, e2)}"
             by(auto simp add: wf_graph_def)
           from a2 a3 f2 have gFadd3: 
                "(E' - (F'  Fadd))  {(e1, e2)}  (E - (F'  Fadd))  {(e1, e2)}" by blast
             
           from mono_sinvar[OF gFadd2 gFadd3] gFadd1
           show "¬ sinvar nodes = V, edges = (E - (F'  Fadd))  {(e1, e2)} nP" by blast 
       qed
       thus ?thesis
        apply(simp add: delete_edges_simp2 Fadd_notinE' add_edge_def)
        apply(clarify)
        using insert_e1_e2_V by fastforce
    qed

    text‹The minimality condition of the offending flows also holds if we increase the graph.›
    corollary minimality_offending_flows_mono_edges_graph: 
      " wf_graph  nodes = V, edges = E ; 
         E'  E;
         F  set_offending_flows nodes = V, edges = E' nP  
      (e1, e2)F. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E  F)) nP"
      using minimality_offending_flows_mono_edges_graph_extend[where Fadd="{}", simplified] by presburger


    text‹all sets in the set of offending flows are monotonic, hence, for a larger graph, they can be extended to match the smaller graph. I.e. everything is monotonic.›
    theorem mono_extend_set_offending_flows: " wf_graph  nodes = V, edges = E ; E'  E; F'  set_offending_flows  nodes = V, edges = E'  nP  
         F  set_offending_flows  nodes = V, edges = E  nP. F'  F"
      proof -
        fix F'V E E'
        assume a1: "wf_graph  nodes = V, edges = E "
        and    a2: "E'  E"
        and    a4: "F'  set_offending_flows nodes = V, edges = E' nP"

        ― ‹Idea: @{text "F = F' ∪ minimize (E - E')"}
  
        have "f. wf_graph (delete_edges nodes = V, edges = E f)"
        using delete_edges_wf[OF a1] by fast
        hence wf1: "f. wf_graph nodes = V, edges = E -f"
        by(simp add: delete_edges_simp2)
  
        obtain Eadd where Eadd_prop: "E'  Eadd = E" and "E'  Eadd = {}" using a2 by blast
  
        from a4 have "F'  E'" by(simp add: set_offending_flows_def)
  
        from wf1 have wf2: "wf_graph nodes = V, edges = E' - F'  Eadd"
          apply(subgoal_tac "E' - F'  Eadd = E - F'")
           apply fastforce
          using Eadd_prop E'  Eadd = {} F'  E' by fast
  
        from a4 have offending_F: "¬ sinvar nodes = V, edges = E' nP"
          by(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
        from this mono_sinvar[OF a1 a2] have 
          goal_noteval: "¬ sinvar nodes = V, edges = E nP" by blast
  
         from a4 have eval_E_minus_FEadd_simp: "sinvar nodes = V, edges = E' - F' nP"
           by(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def delete_edges_simp2)
        (* moreover have "E - (F' ∪ Eadd) = E' - F'"  using `E' ∩ Eadd = {}` Eadd_prop by blast
         ultimately have eval_E_minus_FEadd: "sinvar (delete_edges ⦇nodes = V, edges = E⦈ (F' ∪ Eadd)) nP"
           by(simp add: delete_edges_simp2)*)
  
        show " F  set_offending_flows  nodes = V, edges = E  nP. F'  F"
        proof(cases "¬ sinvar nodes = V, edges = E' - F'  Eadd nP")
          assume assumption_new_violation: "¬ sinvar nodes = V, edges = E' - F'  Eadd nP"
          from a1 have "finite Eadd"
            apply(simp add: wf_graph_def)
            using Eadd_prop wf_graph.finiteE by blast
          from this obtain Eadd_list where Eadd_list_prop: "set Eadd_list = Eadd" and "distinct Eadd_list" by (metis finite_distinct_list)
          from a1 have "finite E'"
            apply(simp add: wf_graph_def)
            using Eadd_prop by blast
          from this obtain E'_list where E'_list_prop: "set E'_list = E'" and "distinct E'_list" by (metis finite_distinct_list)
          from ‹finite E' F'  E' obtain F'_list where "set F'_list = F'" and "distinct F'_list" by (metis finite_distinct_list rev_finite_subset)
    
          have "E' - F'  Eadd - Eadd = E' - F'" using Eadd_prop E'  Eadd = {} F'  E' by blast
          with assumption_new_violation eval_E_minus_FEadd_simp have
            "is_offending_flows (set (Eadd_list)) nodes = V, edges = (E' - F')  Eadd nP"
            by (simp add: Eadd_list_prop delete_edges_simp2 is_offending_flows_def)
          from minimalize_offending_overapprox_sound[OF wf2 this _ ‹distinct Eadd_list] have
            "is_offending_flows_min_set
              (set (minimalize_offending_overapprox Eadd_list []
                 nodes = V, edges = E' - F'  Eadd nP)) nodes = V, edges = E' - F'  Eadd nP"
            by(simp add: Eadd_list_prop)
          with minimalize_offending_overapprox_subseteq_input[of "Eadd_list" "[]" "nodes = V, edges = E' - F'  Eadd" "nP", simplified Eadd_list_prop]
          obtain Fadd where Fadd_prop: "is_offending_flows_min_set Fadd nodes = V, edges = E' - F'  Eadd nP" and "Fadd  Eadd" by auto
        
          have graph_edges_simp_helper: "E' - F'  Eadd - Fadd =  E - (F'  Fadd)"
            using E'  Eadd = {} Eadd_prop F'  E' by blast
        
          from Fadd_prop graph_edges_simp_helper have
            goal_eval_Fadd: "sinvar (delete_edges nodes = V, edges = E (F'  Fadd)) nP" and
            pre_goal_minimal_Fadd: "((e1, e2)Fadd. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E  (F'  Fadd))) nP)"
            by(simp add: is_offending_flows_min_set_def is_offending_flows_def delete_edges_simp2)+
    
          from E'  Eadd = {} Fadd  Eadd have "Fadd  E' = {}" by blast
          from minimality_offending_flows_mono_edges_graph_extend[OF a1 E'  E Fadd  E' = {} a4]
          have mono_delete_edges_minimal: "((e1, e2)F'. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E  (F'  Fadd))) nP)" .
    
          from mono_delete_edges_minimal pre_goal_minimal_Fadd have goal_minimal: 
            "(e1, e2)F'  Fadd. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E (F'  Fadd))) nP" by fastforce
    
           from Eadd_prop Fadd  Eadd F'  E' have goal_subset: "F'  E  Fadd  E" by blast
    
          show " F  set_offending_flows  nodes = V, edges = E  nP. F'  F"
              apply(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
              apply(rule_tac x="F'  Fadd" in exI)
              apply(simp add: goal_noteval goal_eval_Fadd goal_minimal goal_subset)
             done
      next
          assume "¬ ¬ sinvar nodes = V, edges = E' - F'  Eadd nP"
          hence assumption_no_new_violation: "sinvar nodes = V, edges = E' - F'  Eadd nP" by simp
          from this  F'  E' E'  Eadd = {}  have "sinvar nodes = V, edges = E - F' nP"
            proof(subst Eadd_prop[symmetric])
              assume a1: "F'  E'"
              assume a2: "E'  Eadd = {}"
              assume a3: "sinvar nodes = V, edges = E' - F'  Eadd nP"
              have "x1. x1  E' - Eadd = x1  E'"
                using a2 Un_Diff_Int by auto
              hence "F' - Eadd = F'"
                using a1 by auto
              hence "{}  (Eadd - F') = Eadd"
                using Int_Diff Un_Diff_Int sup_commute by auto
              thus "sinvar nodes = V, edges = E'  Eadd - F' nP"
                using a3 by (metis Un_Diff sup_bot.left_neutral)
            qed
          from this have goal_eval: "sinvar (delete_edges nodes = V, edges = E F') nP" 
          by(simp add: delete_edges_simp2)
  
          from Eadd_prop F'  E' have goal_subset: "F'  E" by(blast)
  
          from minimality_offending_flows_mono_edges_graph[OF a1 a2 a4] 
          have goal_minimal: "((e1, e2)F'. ¬ sinvar (add_edge e1 e2 (delete_edges nodes = V, edges = E  F')) nP)" .
  
          show " F  set_offending_flows  nodes = V, edges = E  nP. F'  F"
              apply(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
              apply(rule_tac x="F'" in exI)
              apply(simp add: goal_noteval goal_subset goal_minimal goal_eval)
            done
         qed
    qed


    text‹The offending flows are monotonic.›
    corollary offending_flows_union_mono: " wf_graph  nodes = V, edges = E ; E'  E   
       (set_offending_flows  nodes = V, edges = E'  nP)   (set_offending_flows  nodes = V, edges = E  nP)"
      apply(clarify)
      apply(drule(2) mono_extend_set_offending_flows)
      by blast



   (* I guess set_offending_flows = {{e}} does not hold. Consider the Dependability invariant:
      having a wf graph.
      Add an edge s.t. a dependability violation occurs.
      The offending flows now contains the new edge ans all edges on the path from the node with the violation to the end of the new edge. *)
   lemma set_offending_flows_insert_contains_new:
   " wf_graph  nodes = V, edges = insert e E ; set_offending_flows nodes = V, edges = E nP = {}; set_offending_flows nodes = V, edges = insert e E nP  {}   
      {e}  set_offending_flows nodes = V, edges = insert e E nP"
     proof -
       assume wfG: "wf_graph  nodes = V, edges = insert e E "
       and    a1: "set_offending_flows nodes = V, edges = E nP = {}"
       and    a2: "set_offending_flows nodes = V, edges = insert e E nP  {}"

       from a1 a2 have "e  E" by (metis insert_absorb)
       
       from a1 have a1': "F  E. ¬ is_offending_flows_min_set F nodes = V, edges = E nP"
         by(simp add: set_offending_flows_def)
       from a2 have a2': "F  insert e E. is_offending_flows_min_set F nodes = V, edges = insert e E nP"
        by(simp add: set_offending_flows_def)

       from wfG have wfG': "wf_graph  nodes = V, edges = E " by(simp add:wf_graph_def)

       from a1 defined_offending[OF wfG'] have evalG: "sinvar nodes = V, edges = E  nP" by blast
       from sinvar_monoI[unfolded sinvar_mono_def] wfG' this
       have goal_eval: "sinvar nodes = V, edges = E - {e} nP" by (metis Diff_subset)

       from sinvar_no_offending a2 have goal_not_eval: "¬ sinvar nodes = V, edges = insert e E nP" by blast

       obtain a b where e: "e = (a,b)" by (cases e) blast
       with wfG have insert_e_V: "insert a (insert b V) = V" by(auto simp add: wf_graph_def)

       from a1' a2' have min_set_e: "is_offending_flows_min_set {e} nodes = V, edges = insert e E nP"
        apply(simp add: is_offending_flows_min_set_def is_offending_flows_def add_edge_def delete_edges_simp2 goal_not_eval goal_eval)
        using goal_not_eval by(simp add: e insert_e_V)

       thus "{e}  set_offending_flows nodes = V, edges = insert e E nP"
        by(simp add: set_offending_flows_def)
    qed
     
end

    value "Pow {1::int, 2, 3}  {{8}, {9}}"
    value " xPow {1::int, 2, 3}.  y  {{8::int}, {9}}. {x  y}"
    
    (*similar to ×_def*)
    ― ‹combines powerset of A with B›
    definition pow_combine :: "'x set  'x set set  'x set set" where 
      "pow_combine A B  ( X  Pow A.  Y  B. {X  Y})  Pow A"

    value "pow_combine {1::int,2} {{5::int, 6}, {8}}"
    value "pow_combine {1::int,2} {}"

    lemma pow_combine_mono: 
    fixes S :: "'a set set"
    and   X :: "'a set"
    and   Y :: "'a set"
    assumes a1: " F  S. F  X"
    shows " F  pow_combine Y S. F  Y  X"
    apply(simp add: pow_combine_def)
    apply(rule)
    apply(simp)
    by (metis Pow_iff assms sup.coboundedI1 sup.orderE sup.orderI sup_assoc)


    lemma "S  pow_combine X S" by(auto simp add: pow_combine_def)
    lemma "Pow X  pow_combine X S" by(auto simp add: pow_combine_def)

    lemma rule_pow_combine_fixfst: "B  C  pow_combine A B  pow_combine A C"
      by(auto simp add: pow_combine_def)


    value "pow_combine {1::int,2} {{5::int, 6}, {1}}  pow_combine {1::int,2} {{5::int, 6}, {8}}"

    lemma rule_pow_combine_fixfst_Union: " B   C   (pow_combine A B)   (pow_combine A C)"
      apply(rule)
      apply(fastforce simp: pow_combine_def)
    done

    (*does the following hold?
      (set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP) ⊆ pow_combine X (set_offending_flows ⦇nodes = V, edges = E⦈ nP)

      I guess not:  ^D  I'm convinced this does not hold!
      Graph:   A -> B -> C
      E = A -> B
      E ∪ X = A -> B -> C
      
      model is A and C are interfering

      set_offending_flows(E ∪ X) = {{(A,B)}, {B,C}}
       set_offending_flows(E) = {}
      pow_combine X set_offending_flows(E) = {{}, {C}}

      the {(A,B)} is the problem here such that subset does not hold.

      It holds if
        ∀ F ∈ (set_offending_flows ⦇nodes = V, edges = E ∪ X⦈ nP). F ⊆ X
      however, then (set_offending_flows ⦇nodes = V, edges = E⦈ nP) = {} which renders the whole statement useless
     *)

  context SecurityInvariant_preliminaries
  begin

    lemma offending_partition_subset_empty: 
    assumes a1:" F  (set_offending_flows nodes = V, edges = E  X nP). F  X"
    and wfGEX: "wf_graph nodes = V, edges = E  X"
    and disj: "E  X = {}"
    shows "(set_offending_flows nodes = V, edges = E nP) = {}"
    proof(rule ccontr)
      assume c: "set_offending_flows nodes = V, edges = E nP  {}"
      from this obtain F' where F'_prop: "F'  set_offending_flows nodes = V, edges = E nP" by blast
      from F'_prop have "F'  E" using set_offending_flows_def by simp
      from mono_extend_set_offending_flows[OF wfGEX _ F'_prop] have 
        "Fset_offending_flows nodes = V, edges = E  X nP. F'  F" by blast
      from this a1 have "F'  X" by fast
      from F'_prop have "{}  F'" by (metis empty_offending_contra)
      from F'  X F'  E disj {}  F'
      show "False" by blast
    qed

    corollary partitioned_offending_subseteq_pow_combine:
    assumes wfGEX: "wf_graph nodes = V, edges = E  X"
    and disj: "E  X = {}"
    and partitioned_offending: " F  (set_offending_flows nodes = V, edges = E  X nP). F  X" (*offending does not contain E*)
    shows "(set_offending_flows nodes = V, edges = E  X nP)  pow_combine X (set_offending_flows nodes = V, edges = E nP)"
    apply(subst offending_partition_subset_empty[OF partitioned_offending wfGEX disj])
    apply(simp add: pow_combine_def)
    apply(rule)
    apply(simp)
    using partitioned_offending by simp
  end


  context SecurityInvariant_preliminaries
  begin

    text‹Knowing that the ⋃ offending is ⊆ X›, removing something from the graphs's edges, 
           it also disappears from the offending flows.›
    lemma Un_set_offending_flows_bound_minus:
    assumes wfG: "wf_graph  nodes = V, edges = E "
    and     Foffending: "(set_offending_flows nodes = V, edges = E nP)  X"
    shows   "(set_offending_flows nodes = V, edges = E - {f} nP)  X - {f}"
    proof -
      from wfG have wfG': "wf_graph  nodes = V, edges = E - {f} "
        by(auto simp add: wf_graph_def finite_subset)
      
      from offending_flows_union_mono[OF wfG, where E'="E - {f}"] have 
        "(set_offending_flows nodes = V, edges = E - {f} nP) - {f}  (set_offending_flows nodes = V, edges = E nP) - {f}" by blast
      also have 
        "(set_offending_flows nodes = V, edges = E - {f} nP)  (set_offending_flows nodes = V, edges = E - {f} nP) - {f}"
        apply(simp add: set_offending_flows_simp[OF wfG']) by blast
      ultimately have Un_set_offending_flows_minus:
        "(set_offending_flows nodes = V, edges = E - {f} nP)  (set_offending_flows nodes = V, edges = E  nP) - {f}"
        by blast

      from Foffending Un_set_offending_flows_minus 
      show ?thesis by blast
    qed


  text‹
    If the offending flows are bound by some @{term X},
    the we can remove all finite @{term "E'"}from the graph's edges
    and the offending flows from the smaller graph are bound by @{term "X - E'"}.
›
    lemma Un_set_offending_flows_bound_minus_subseteq:
    assumes wfG: "wf_graph  nodes = V, edges = E "
    and     Foffending: " (set_offending_flows nodes = V, edges = E nP)  X"
    shows   " (set_offending_flows nodes = V, edges = E - E' nP)  X - E'"
    proof -
      from wfG have wfG': "wf_graph  nodes = V, edges = E - E' "
        by(auto simp add: wf_graph_def finite_subset)
      
      from offending_flows_union_mono[OF wfG, where E'="E - E'"] have 
        "(set_offending_flows nodes = V, edges = E - E' nP) - E'  (set_offending_flows nodes = V, edges = E nP) - E'" by blast
      also have 
        "(set_offending_flows nodes = V, edges = E - E' nP)  (set_offending_flows nodes = V, edges = E - E' nP) - E'"
        apply(simp add: set_offending_flows_simp[OF wfG']) by blast
      ultimately have Un_set_offending_flows_minus:
        " (set_offending_flows nodes = V, edges = E - E' nP)   (set_offending_flows nodes = V, edges = E  nP) - E'"
        by blast

      from Foffending Un_set_offending_flows_minus 
      show ?thesis by blast
    qed

  corollary Un_set_offending_flows_bound_minus_subseteq': 
    " wf_graph  nodes = V, edges = E ;
     (set_offending_flows  nodes = V, edges = E  nP)  X  
     (set_offending_flows  nodes = V, edges = E - E'  nP)  X - E'"
    apply(drule(1) Un_set_offending_flows_bound_minus_subseteq) by blast


  end

end

Theory TopoS_ENF

theory TopoS_ENF
imports Main TopoS_Interface "Lib/TopoS_Util" TopoS_withOffendingFlows
begin


section‹Special Structures of Security Invariants›

text ‹Security Invariants may have a common structure: 
  If the function @{term "sinvar"} is predicate which starts with ∀ (v1, v2) ∈ edges G. …›,
  we call this the all edges normal form (ENF).
  We found that this form has some nice properties.
  Also, locale instantiation is easier in ENF with the help of the following lemmata.›

subsection ‹Simple Edges Normal Form (ENF)›

context SecurityInvariant_withOffendingFlows
begin 

  definition sinvar_all_edges_normal_form :: "('a  'a  bool)  bool" where
  "sinvar_all_edges_normal_form P   G nP. sinvar G nP = ( (e1, e2) edges G. P (nP e1) (nP e2))"
  
  text‹reflexivity is needed for convenience. If a security invariant is not reflexive, that means that all nodes with the default
    parameter ⊥› are not allowed to communicate with each other. Non-reflexivity is possible, but requires more work.›
  definition ENF_refl :: "('a  'a  bool)  bool" where
  "ENF_refl P  sinvar_all_edges_normal_form P  ( p1. P p1 p1)"

  lemma monotonicity_sinvar_mono: "sinvar_all_edges_normal_form P  sinvar_mono"
  unfolding sinvar_all_edges_normal_form_def sinvar_mono_def
  by auto

end 

subsubsection ‹Offending Flows›

context SecurityInvariant_withOffendingFlows
begin

  text‹The insight: for all edges in the members of the offending flows, @{term "¬ P"} holds.›
  lemma ENF_offending_imp_not_P:
    assumes "sinvar_all_edges_normal_form P" "F  set_offending_flows G nP" "(e1, e2)  F"
    shows "¬ P (nP e1) (nP e2)"
  using assms
  unfolding sinvar_all_edges_normal_form_def set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def
  by (fastforce simp: graph_ops)

  text‹Hence, the members of @{const set_offending_flows} must look as follows.›
  lemma ENF_offending_set_P_representation: 
    assumes "sinvar_all_edges_normal_form P" "F  set_offending_flows G nP"
    shows "F = {(e1,e2). (e1, e2)  edges G  ¬ P (nP e1) (nP e2)}" (is "F = ?E")
  proof -
    { fix a b
      assume "(a, b)  F"
      hence "(a, b)  ?E"
        using assms
        by (auto simp: set_offending_flows_def ENF_offending_imp_not_P)
    }
    moreover
    { fix x
      assume "x  ?E"
      hence "x  F"
        using assms
        unfolding sinvar_all_edges_normal_form_def set_offending_flows_def is_offending_flows_min_set_def
        by (fastforce simp: is_offending_flows_def graph_ops)
    }
    ultimately show ?thesis
      by blast
  qed

  text‹We can show left to right of the desired representation of @{const set_offending_flows}
  lemma ENF_offending_subseteq_lhs:
    assumes "sinvar_all_edges_normal_form P"
    shows "set_offending_flows G nP  { {(e1,e2). (e1, e2)  edges G  ¬ P (nP e1) (nP e2)} }"
  using assms
  by (force simp: ENF_offending_set_P_representation)

  text‹if @{const set_offending_flows} is not empty, we have the other direction.›
  lemma ENF_offending_not_empty_imp_ENF_offending_subseteq_rhs:
    assumes "sinvar_all_edges_normal_form P" "set_offending_flows G nP  {}"
    shows "{ {(e1,e2)  edges G. ¬ P (nP e1) (nP e2)} }  set_offending_flows G nP"
  using assms ENF_offending_set_P_representation
  by blast
  
  lemma ENF_notevalmodel_imp_offending_not_empty:
  "sinvar_all_edges_normal_form P  ¬ sinvar G nP  set_offending_flows G nP  {}"
    (*TODO get easier from monotonicity? but would require valid graph assumption ...*)
    proof -
      assume enf: "sinvar_all_edges_normal_form P"
      and ns: "¬ sinvar G nP"

      {
        let ?F'="{(e1,e2)  (edges G). ¬P (nP e1) (nP e2)}"
        ― ‹select @{term "?F'"} as the list of all edges which violate @{term "P"}

        from enf have ENF_notevalmodel_offending_imp_ex_offending_min:
            "F. is_offending_flows F G nP  F  edges G 
             F'. F'  edges G  is_offending_flows_min_set F' G nP"
          unfolding sinvar_all_edges_normal_form_def is_offending_flows_min_set_def is_offending_flows_def
          by (-) (rule exI[where x="?F'"], fastforce simp: graph_ops)

        from enf ns have "F. F  (edges G)  is_offending_flows F G nP"
          unfolding sinvar_all_edges_normal_form_def is_offending_flows_def
          by (-) (rule exI[where x="?F'"], fastforce simp: graph_ops)
      
        from enf ns this ENF_notevalmodel_offending_imp_ex_offending_min have ENF_notevalmodel_imp_ex_offending_min:
          "F. F  edges G  is_offending_flows_min_set F G nP" by blast
        } note ENF_notevalmodel_imp_ex_offending_min=this

      from ENF_notevalmodel_imp_ex_offending_min show "set_offending_flows G nP  {}" using set_offending_flows_def by simp
    qed

  lemma ENF_offending_case1:
    " sinvar_all_edges_normal_form P;  ¬ sinvar G nP  
    { {(e1,e2). (e1, e2)  (edges G)  ¬ P (nP e1) (nP e2)} } = set_offending_flows G nP"
    apply(rule)
     apply(frule ENF_notevalmodel_imp_offending_not_empty, simp)
     apply(rule ENF_offending_not_empty_imp_ENF_offending_subseteq_rhs, simp)
     apply simp
    apply(rule ENF_offending_subseteq_lhs)
    apply simp
  done
  
  lemma ENF_offending_case2:
    " sinvar_all_edges_normal_form P; sinvar G nP  
    {} = set_offending_flows G nP"
    apply(drule sinvar_no_offending[of G nP])
    apply simp
  done
  
  
  theorem ENF_offending_set:
    " sinvar_all_edges_normal_form P  
    set_offending_flows G nP = (if sinvar G nP then
      {}
     else 
      { {(e1,e2). (e1, e2)  edges G  ¬ P (nP e1) (nP e2)} })"
  by(simp add: ENF_offending_case1 ENF_offending_case2)
end

subsubsection ‹Lemmata›

  lemma (in SecurityInvariant_withOffendingFlows)  ENF_offending_members:
    " ¬ sinvar G nP; sinvar_all_edges_normal_form P; f  set_offending_flows G nP  
    f  (edges G)  ( (e1, e2) f. ¬ P (nP e1) (nP e2))"
  by(auto simp add: ENF_offending_set)
 


subsubsection ‹Instance Helper›
  
  lemma (in SecurityInvariant_withOffendingFlows) ENF_refl_not_offedning:
        " ¬ sinvar G nP; f  set_offending_flows G nP; 
          ENF_refl P 
          (e1,e2)  f. e1  e2"
  proof -
  assume a_not_eval: "¬ sinvar G nP"
    and   a_enf_refl: "ENF_refl P"
    and   a_offedning: "f  set_offending_flows G nP"
  
    from a_enf_refl have a_enf: "sinvar_all_edges_normal_form P" using ENF_refl_def by simp
    hence a_ENF: " G nP. sinvar G nP  = ( (e1, e2)  edges G. P (nP e1) (nP e2))" using sinvar_all_edges_normal_form_def by simp
    
    from a_enf_refl ENF_refl_def have a_refl: " (e1,e1)  f. P (nP e1) (nP e1)" by simp
    from ENF_offending_members[OF a_not_eval a_enf a_offedning] have " (e1, e2)  f. ¬ P (nP e1) (nP e2)" by fast
    from this a_refl show "(e1,e2)  f. e1  e2" by fast
  qed
  
  lemma (in SecurityInvariant_withOffendingFlows) ENF_default_update_fst: 
  fixes "default_node_properties" :: "'a" ("")
  assumes modelInv: "¬ sinvar G nP"
    and   ENFdef: "sinvar_all_edges_normal_form P"
    and   secdef: " (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P  (nP e2))"
  shows
    "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) (nP e2))"
  proof -
    from ENFdef have ENF: " G nP. sinvar G nP  = ( (e1, e2) edges G. P (nP e1) (nP e2))" 
      using sinvar_all_edges_normal_form_def by simp
    from modelInv ENF have modelInv': "¬ ( (e1, e2) edges G. P (nP e1) (nP e2))" by simp
    from this secdef have modelInv'': "¬ ( (e1, e2) edges G. P  (nP e2))" by blast
      have simpUpdateI: " e1 e2. ¬ P (nP e1) (nP e2)  ¬ P  (nP e2)  ¬ P ((nP(i := )) e1) (nP e2)" by simp
      hence " X. (e1,e2)  X. ¬ P (nP e1) (nP e2)  (e1,e2)  X.¬ P  (nP e2)  (e1,e2)  X.¬ P ((nP(i := )) e1) (nP e2)" 
        using secdef by blast
    from this modelInv' modelInv'' show "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) (nP e2))" by blast
  qed

  
  lemma (in SecurityInvariant_withOffendingFlows) 
    fixes "default_node_properties" :: "'a" ("")
    shows "¬ sinvar G nP  sinvar_all_edges_normal_form P 
    ( (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))   ¬ (P  (nP e2))) 
    ( (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P (nP e1) )) 
    ( (nP::'v  'a) e1 e2. ¬ P  )
     ¬ sinvar G (nP(i := ))"
  proof -
    assume a1: "¬ sinvar G nP"
    and   a2d: "sinvar_all_edges_normal_form P"
    and    a3: " (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P  (nP e2))"
    and    a4: " (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P (nP e1) )"
    and    a5: " (nP::'v  'a) e1 e2. ¬ P  "
  
    from a2d have a2: " G nP. sinvar G nP  = ( (e1, e2)  edges G. P (nP e1) (nP e2))" 
      using sinvar_all_edges_normal_form_def by simp
  
    from ENF_default_update_fst[OF a1 a2d] a3 have subgoal1: "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) (nP e2))" by blast
    
    let ?nP' = "(nP(i := ))"
  
    from subgoal1 have " (e1, e2)  edges G. ¬ P (?nP' e1) (nP e2)" by blast
    from this obtain e11 e21 where s1cond: "(e11, e21)  edges G  ¬ P (?nP' e11) (nP e21)" by blast
  
    from s1cond have "i  e11  ¬ P (nP e11) (nP e21)" by simp
    from s1cond have "e11  e21  ¬ P (?nP' e11) (?nP' e21)"
      apply simp
      apply(rule conjI)
       apply blast
      apply(insert a4)
      by force
    from s1cond a4 fun_upd_apply have ex1: "e11  e21  ¬ P (?nP' e11) (?nP' e21)" by metis
    from s1cond a5 have ex2: "e11 = e21  ¬ P (?nP' e11) (?nP' e21)" by auto
  
    from ex1 ex2 s1cond have " (e1, e2)  edges G. ¬ P (?nP' e1) (?nP' e2)" by blast
    hence "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) ((nP(i := )) e2))" by fast
    from this a2 show "¬ sinvar G (nP(i := ))" by presburger
  qed
  
  (* fsts version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENF_fsts_refl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf_refl: "ENF_refl P"
    and   a3: " (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P  (nP e2))" (*changed ⋀ to ∀*)
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_fsts: "i  fst ` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from a_offending have a_not_eval: "¬ sinvar G nP" by (metis equals0D sinvar_no_offending)
    from valid_without_offending_flows[OF a_offending] have a_offending_rm: "sinvar (delete_edges G f) nP" .

    from a_enf_refl have a_enf: "sinvar_all_edges_normal_form P" using ENF_refl_def by simp
    hence a2: " G nP. sinvar G nP  = ( (e1, e2)  edges G. P (nP e1) (nP e2))" using sinvar_all_edges_normal_form_def by simp
  
    from ENF_offending_members[OF a_not_eval a_enf a_offending] have a_f_3_in_f: " e1 e2. (e1, e2)  f  ¬ P (nP e1) (nP e2)" by fast
  
    let ?nP' = "(nP(i := ))"
  
    (* obain from f *)
    from offending_not_empty[OF a_offending] ENF_offending_members[OF a_not_eval a_enf a_offending] a_i_fsts hd_in_set
      obtain e1 e2 where e1e2cond: "(e1, e2)  f  e1 = i" by force
  
    from conjunct1[OF e1e2cond] a_f_3_in_f have e1e2notP: "¬ P (nP e1) (nP e2)" by simp
    from this a3 have "¬ P  (nP e2)" by simp
    from this e1e2notP have e1e2subgoal1: "¬ P (?nP' e1) (nP e2)" by simp
  
    from ENF_refl_not_offedning[OF a_not_eval a_offending a_enf_refl] conjunct1[OF e1e2cond] have ENF_refl: "e1  e2" by fast
  
    from e1e2subgoal1 have "e1  e2  ¬ P (?nP' e1) (?nP' e2)"
      apply simp
      apply(rule conjI)
       apply blast
      apply(insert conjunct2[OF e1e2cond])
      by simp
  
    from this ENF_refl ENF_offending_members[OF a_not_eval a_enf a_offending]  conjunct1[OF e1e2cond] have 
      " (e1, e2)  edges G. ¬ P (?nP' e1) (?nP' e2)" by blast
    hence "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) ((nP(i := )) e2))" by fast
    from this a2 show "¬ sinvar G (nP(i := ))" by presburger
  qed

  (* snds version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENF_snds_refl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf_refl: "ENF_refl P"
    and   a3: " (nP::'v  'a) e1 e2. ¬ (P (nP e1) (nP e2))  ¬ (P (nP e1) )"
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_snds: "i  snd ` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from a_offending have a_not_eval: "¬ sinvar G nP" by (metis equals0D sinvar_no_offending)
    from valid_without_offending_flows[OF a_offending] have a_offending_rm: "sinvar (delete_edges G f) nP" .
    from a_enf_refl have a_enf: "sinvar_all_edges_normal_form P" using ENF_refl_def by simp
    hence a2: " G nP. sinvar G nP  = ( (e1, e2)  edges G. P (nP e1) (nP e2))" using sinvar_all_edges_normal_form_def by simp
  
    from ENF_offending_members[OF a_not_eval a_enf a_offending] have a_f_3_in_f: " e1 e2. (e1, e2)  f  ¬ P (nP e1) (nP e2)" by fast
  
    let ?nP' = "(nP(i := ))"
  
    (* obain from f *)
    from offending_not_empty[OF a_offending] ENF_offending_members[OF a_not_eval a_enf a_offending] a_i_snds hd_in_set
      obtain e1 e2 where e1e2cond: "(e1, e2)  f  e2 = i" by force
  
    from conjunct1[OF e1e2cond] a_f_3_in_f have e1e2notP: "¬ P (nP e1) (nP e2)" by simp
    from this a3 have "¬ P (nP e1) " by auto
    from this e1e2notP have e1e2subgoal1: "¬ P (nP e1) (?nP' e2)" by simp
  
    from ENF_refl_not_offedning[OF a_not_eval a_offending a_enf_refl] e1e2cond have ENF_refl: "e1  e2" by fast
  
    from e1e2subgoal1 have "e1  e2  ¬ P (?nP' e1) (?nP' e2)"
      apply simp
      apply(rule conjI)
       apply(insert conjunct2[OF e1e2cond])
       by simp_all
  
    from this ENF_refl e1e2cond ENF_offending_members[OF a_not_eval a_enf a_offending]  conjunct1[OF e1e2cond] have 
      " (e1, e2)  edges G. ¬ P (?nP' e1) (?nP' e2)" by blast
    hence "¬ ( (e1, e2)  edges G. P ((nP(i := )) e1) ((nP(i := )) e2))" by fast
    from this a2 show "¬ sinvar G (nP(i := ))" by presburger
  qed





(*ENF_sr*)


subsection ‹edges normal form ENF with sender and receiver names›
  definition (in SecurityInvariant_withOffendingFlows) sinvar_all_edges_normal_form_sr :: "('a  'v  'a  'v  bool)  bool" where
    "sinvar_all_edges_normal_form_sr P   G nP. sinvar G nP = ( (s, r) edges G. P (nP s) s (nP r) r)"
  

  lemma (in SecurityInvariant_withOffendingFlows) ENFsr_monotonicity_sinvar_mono: " sinvar_all_edges_normal_form_sr P  
    sinvar_mono"
    apply(simp add: sinvar_all_edges_normal_form_sr_def sinvar_mono_def)
    by blast

subsubsection ‹Offending Flows:›
  
  theorem (in SecurityInvariant_withOffendingFlows) ENFsr_offending_set:
    assumes ENFsr: "sinvar_all_edges_normal_form_sr P"
    shows "set_offending_flows G nP = (if sinvar G nP then
      {}
     else 
      { {(s,r). (s, r)  edges G  ¬ P (nP s) s (nP r) r} })" (is "?A = ?B")
  proof(cases "sinvar G nP")
  case True thus "?A = ?B" 
    by(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def)
  next
  case False
   from ENFsr have ENFsr_offending_imp_not_P: " F s r. F  set_offending_flows G nP  (s, r)  F   ¬ P (nP s) s (nP r) r"
     unfolding sinvar_all_edges_normal_form_sr_def
     apply(simp add: set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def graph_ops)
     apply clarify
     by fastforce
   from ENFsr have  ENFsr_offending_set_P_representation: 
    " F. F  set_offending_flows G nP   F = {(s,r). (s, r)  edges G  ¬ P (nP s) s (nP r) r}"
      apply -
      apply rule
       apply rule
       apply clarify
       apply(rename_tac a b)
       apply rule
        apply(auto simp add:set_offending_flows_def)[1]
       apply(simp add: ENFsr_offending_imp_not_P)
      unfolding sinvar_all_edges_normal_form_sr_def
      apply(simp add:set_offending_flows_def is_offending_flows_def is_offending_flows_min_set_def graph_ops)
      apply clarify
      apply(rename_tac a b a1 b1)
      apply(blast)
    done
  

    from ENFsr False have ENFsr_offending_flows_exist: "set_offending_flows G nP  {}"
      apply(simp add: set_offending_flows_def is_offending_flows_min_set_def is_offending_flows_def sinvar_all_edges_normal_form_sr_def
            delete_edges_def add_edge_def)
      apply(clarify)
      apply(rename_tac s r)
      apply(rule_tac x="{(s,r). (s,r)  (edges G)  ¬P (nP s) s (nP r) r}" in exI)
      apply(simp)
      by blast

    from ENFsr have ENFsr_offenindg_not_empty_imp_ENF_offending_subseteq_rhs:
      "set_offending_flows G nP  {}  
      { {(s,r). (s, r)  edges G  ¬ P (nP s) s (nP r) r} }  set_offending_flows G nP"
      apply -
      apply rule
      using ENFsr_offending_set_P_representation
      by blast

    from ENFsr have ENFsr_offending_subseteq_lhs:
      "(set_offending_flows G nP)  { {(s,r). (s, r)  edges G  ¬ P (nP s) s (nP r) r} }"
      apply -
      apply rule
      by(simp add: ENFsr_offending_set_P_representation)

    from False ENFsr_offenindg_not_empty_imp_ENF_offending_subseteq_rhs[OF ENFsr_offending_flows_exist] ENFsr_offending_subseteq_lhs show "?A = ?B"
      by force
  qed
  



(*ENFnrSR*)

subsection ‹edges normal form not refl ENFnrSR›
  definition (in SecurityInvariant_withOffendingFlows) sinvar_all_edges_normal_form_not_refl_SR :: "('a  'v  'a  'v  bool)  bool" where
    "sinvar_all_edges_normal_form_not_refl_SR P  
     G nP. sinvar G nP = ( (s, r)  edges G. s  r  P (nP s) s (nP r) r)"



  text‹we derive everything from the ENFnrSR form›
  lemma (in SecurityInvariant_withOffendingFlows) ENFnrSR_to_ENFsr: 
    "sinvar_all_edges_normal_form_not_refl_SR P  sinvar_all_edges_normal_form_sr (λ p1 v1 p2 v2. v1  v2  P p1 v1 p2 v2)"
    by(simp add: sinvar_all_edges_normal_form_sr_def sinvar_all_edges_normal_form_not_refl_SR_def)
    


subsubsection ‹Offending Flows›
   theorem (in SecurityInvariant_withOffendingFlows) ENFnrSR_offending_set:
    " sinvar_all_edges_normal_form_not_refl_SR P  
    set_offending_flows G nP = (if sinvar G nP then
      {}
     else 
      { {(e1,e2). (e1, e2)  edges G  e1  e2  ¬ P (nP e1) e1 (nP e2) e2} })"
    by(auto dest: ENFnrSR_to_ENFsr simp: ENFsr_offending_set)


subsubsection ‹Instance helper›

  (* fsts version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENFnrSR_fsts_weakrefl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf: "sinvar_all_edges_normal_form_not_refl_SR P"
    and   a_weakrefl: " s r. P  s  r"
    and   a_botdefault: " s r. (nP r)    ¬ P (nP s) s (nP r) r  ¬ P  s (nP r) r"
    and   a_alltobot: " s r. P (nP s) s  r"
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_fsts: "i  fst` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from a_offending have a_not_eval: "¬ sinvar G nP" by (metis ex_in_conv sinvar_no_offending)
    from valid_without_offending_flows[OF a_offending] have a_offending_rm: "sinvar (delete_edges G f) nP" .
    from a_enf have a_enf': " G nP. sinvar G nP  = ( (e1, e2) (edges G). e1  e2  P (nP e1) e1 (nP e2) e2)" 
      using sinvar_all_edges_normal_form_not_refl_SR_def by simp
  
    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending have a_f_3_in_f: " e1 e2. (e1, e2)f  ¬ P (nP e1) e1 (nP e2) e2" by(simp)
    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending have a_f_3_neq: " e1 e2. (e1, e2)f  e1  e2" by simp
  
    let ?nP' = "(nP(i := ))"

    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending a_i_fsts
      obtain e1 e2 where e1e2cond: "(e1, e2)  f  e1 = i" by fastforce

    from conjunct1[OF e1e2cond] a_offending have "(e1, e2)  edges G"
      by (metis (lifting, no_types) SecurityInvariant_withOffendingFlows.set_offending_flows_def mem_Collect_eq rev_subsetD)
  
    from conjunct1[OF e1e2cond] a_f_3_in_f have e1e2notP: "¬ P (nP e1) e1 (nP e2) e2" by simp
    from e1e2notP a_weakrefl have e1ore2neqbot: "(nP e1)    (nP e2)  " by fastforce
    from e1e2notP a_alltobot have "(nP e2)  " by fastforce
    from this e1e2notP a_botdefault have "¬ P  e1 (nP e2) e2" by simp
    from this e1e2notP have e1e2subgoal1: "¬ P (?nP' e1) e1 (nP e2) e2" by auto

    from a_f_3_neq e1e2cond have "e2  e1" by blast
  
    from e1e2subgoal1 have "e1  e2  ¬ P (?nP' e1) e1 (?nP' e2) e2"
      apply simp
      apply(rule conjI)
       apply blast
      apply(insert e1e2cond)
      by simp
    from this e2  e1 have "¬ P (?nP' e1) e1 (?nP' e2) e2" by simp
  
    from this e2  e1 ENFnrSR_offending_set[OF a_enf] a_offending (e1, e2)  edges G have 
      " (e1, e2)(edges G). e2  e1  ¬ P (?nP' e1) e1 (?nP' e2) e2" by blast
    hence "¬ ( (e1, e2)(edges G). e2  e1  P ((nP(i := )) e1) e1 ((nP(i := )) e2) e2)" by fast
    from this a_enf' show "¬ sinvar G (nP(i := ))" by fast
  qed



  (* snds version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENFnrSR_snds_weakrefl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf: "sinvar_all_edges_normal_form_not_refl_SR P"
    and   a_weakrefl: " s r. P  s  r"
    and   a_botdefault: " s r. (nP s)    ¬ P (nP s) s (nP r) r  ¬ P (nP s) s  r"
    and   a_bottoall: " s r. P  s (nP r) r"
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_snds: "i  snd` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from a_offending have a_not_eval: "¬ sinvar G nP" by (metis equals0D sinvar_no_offending)
    from valid_without_offending_flows[OF a_offending] have a_offending_rm: "sinvar (delete_edges G f) nP" .
    from a_enf have a_enf': " G nP. sinvar G nP  = ( (e1, e2)(edges G). e1  e2  P (nP e1) e1 (nP e2) e2)" 
      using sinvar_all_edges_normal_form_not_refl_SR_def by simp
  
    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending have a_f_3_in_f: " s r. (s, r)f  ¬ P (nP s) s (nP r) r" by simp
    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending have a_f_3_neq: " s r. (s, r)f  s  r" by simp
  
    let ?nP' = "(nP(i := ))"

    from ENFnrSR_offending_set[OF a_enf] a_not_eval a_offending a_i_snds
      obtain e1 e2 where e1e2cond: "(e1, e2)f  e2 = i" by fastforce

    from conjunct1[OF e1e2cond] a_offending have "(e1, e2)  edges G"
      by (metis (lifting, no_types) SecurityInvariant_withOffendingFlows.set_offending_flows_def mem_Collect_eq rev_subsetD)
  
    from conjunct1[OF e1e2cond] a_f_3_in_f have e1e2notP: "¬ P (nP e1) e1 (nP e2) e2" by simp
    from e1e2notP a_weakrefl have e1ore2neqbot: "(nP e1)    (nP e2)  " by fastforce
    from e1e2notP a_bottoall have x1: "(nP e1)  " by fastforce
    from this e1e2notP a_botdefault have x2: "¬ P (nP e1) e1  e2" by fast
    from this e1e2notP have e1e2subgoal1: "¬ P (nP e1) e1 (?nP' e2) e2" by auto

    from a_f_3_neq e1e2cond have "e2  e1" by blast
  
    from e1e2subgoal1 have "e1  e2  ¬ P (?nP' e1) e1 (?nP' e2) e2" by(simp add: e1e2cond)
  
    from this e2  e1 ENFnrSR_offending_set[OF a_enf] a_offending (e1, e2)  edges G have 
      " (e1, e2)(edges G). e2  e1  ¬ P (?nP' e1) e1 (?nP' e2) e2" by fastforce
    hence "¬ ( (e1, e2)(edges G). e2  e1  P ((nP(i := )) e1) e1 ((nP(i := )) e2) e2)" by fast
    from this a_enf' show "¬ sinvar G (nP(i := ))" by fast
  qed




(*ENFnr*)



subsection ‹edges normal form not refl ENFnr›
  definition (in SecurityInvariant_withOffendingFlows) sinvar_all_edges_normal_form_not_refl :: "('a  'a  bool)  bool" where
    "sinvar_all_edges_normal_form_not_refl P   G nP. sinvar G nP = ( (e1, e2)  edges G. e1  e2  P (nP e1) (nP e2))"
  

  text‹we derive everything from the ENFnrSR form›
  lemma (in SecurityInvariant_withOffendingFlows) ENFnr_to_ENFnrSR: 
    "sinvar_all_edges_normal_form_not_refl P  sinvar_all_edges_normal_form_not_refl_SR (λ v1 _ v2 _. P v1 v2)"
    by(simp add: sinvar_all_edges_normal_form_not_refl_def sinvar_all_edges_normal_form_not_refl_SR_def)

  (*most of results are now implied from previous lemma*)

subsubsection ‹Offending Flows›
   theorem (in SecurityInvariant_withOffendingFlows) ENFnr_offending_set:
    " sinvar_all_edges_normal_form_not_refl P  
    set_offending_flows G nP = (if sinvar G nP then
      {}
     else 
      { {(e1,e2). (e1, e2)  edges G  e1  e2  ¬ P (nP e1) (nP e2)} })"
    apply(drule ENFnr_to_ENFnrSR)
    by(drule(1) ENFnrSR_offending_set)


subsubsection ‹Instance helper›
  (* fsts version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENFnr_fsts_weakrefl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf: "sinvar_all_edges_normal_form_not_refl P"
    and   a_botdefault: " e1 e2. e2    ¬ P e1 e2  ¬ P  e2"
    and   a_alltobot: " e1. P e1 "
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_fsts: "i  fst` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from assms show ?thesis
    apply -
    apply(drule ENFnr_to_ENFnrSR)
    apply(drule ENFnrSR_fsts_weakrefl_instance)
         by auto
  qed
  
  (* snds version *)
  lemma (in SecurityInvariant_withOffendingFlows)  ENFnr_snds_weakrefl_instance:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_enf: "sinvar_all_edges_normal_form_not_refl P"
    and   a_botdefault: " e1 e2. ¬ P e1 e2  ¬ P e1 "
    and   a_bottoall: " e2. P  e2"
    and   a_offending: "f  set_offending_flows G nP"
    and   a_i_snds: "i  snd` f"
    shows
          "¬ sinvar G (nP(i := ))"
  proof -
    from assms show ?thesis
    apply -
    apply(drule ENFnr_to_ENFnrSR)
    apply(drule ENFnrSR_snds_weakrefl_instance)
         by auto
  qed
 



  (* snds version DRAFT*)
  lemma (in SecurityInvariant_withOffendingFlows)  ENF_weakrefl_instance_FALSE:
    fixes "default_node_properties" :: "'a" ("")
    assumes a_wfG: "wf_graph G"
    and   a_not_eval: "¬ sinvar G nP"
    and   a_enf: "sinvar_all_edges_normal_form P"
    and   a_weakrefl: "P  "
    and   a_botisolated: " e2. e2    ¬ P  e2"
    and   a_botdefault: " e1 e2. e1    ¬ P e1 e2  ¬ P e1 "
    and   a_offending: "f  set_offending_flows G nP"
    and   a_offending_rm: "sinvar (delete_edges G f) nP"
    and   a_i_fsts: "i  snd` f"
    and   a_not_eval_upd: "¬ sinvar G (nP(i := ))"
    shows "False"
oops



end

Theory vertex_example_simps

theory vertex_example_simps
imports "Lib/FiniteGraph" TopoS_Vertices
begin
(*<*)
― ‹The follwoing lemmata are used in the @{text "∃"}-style uniqueness proof›
lemma False_set: "{(e1, e2). False} = {}" by blast
lemma succ_tran_empty: "(succ_tran nodes = V, edges = {} v) = {}"
  by(simp add: succ_tran_def)
lemma vertex_1_vertex_2_set_simp: "{vertex_1, vertex_2, vertex_1, vertex_2} = {vertex_1, vertex_2}" by blast
lemma unique_default_example1: "succ_tran nodes = {vertex_1, vertex_2}, edges = {(vertex_1, vertex_2)} vertex_1 = {vertex_2}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma unique_default_example2: "succ_tran nodes = {vertex_1, vertex_2}, edges = {(vertex_2, vertex_1)} vertex_1 = {}"
apply (simp add: succ_tran_def)
by (metis Domain.DomainI Domain_empty Domain_insert distinct_vertices12 singleton_iff trancl_domain)
lemma unique_default_example3: "succ_tran nodes = {vertex_1, vertex_2}, edges = {(vertex_2, vertex_1)} vertex_2 = {vertex_1}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma unique_default_example_simp1: "{(e1, e2). e1 = vertex_1  e2 = vertex_2  (e1 = vertex_1  e2  vertex_2)} = {}" by blast
lemma unique_default_example_simp2: "{(vertex_1, vertex_2)}+ = {(vertex_1, vertex_2)}"
  apply(rule)
   apply(rule)
   apply(clarify)
   apply(rule_tac P="λ a b. a = vertex_1  b = vertex_2" in trancl.induct)
     apply auto
done
lemma unique_default_example_simp3: "{(e1, e2). e1 = vertex_2  e2 = vertex_1  (e1 = vertex_2  e2  vertex_1)} = {}" 
  by(blast)
lemma vertex_set_simp2: "{vertex_2, vertex_1, vertex_2} = {vertex_1, vertex_2}" by blast
lemma canAccessThis_simp1: "canAccessThis  vertex_1  succ_tran nodes = {vertex_1, canAccessThis}, edges = {(vertex_1, canAccessThis)} vertex_1 = {canAccessThis}"
apply (simp add: succ_tran_def)
by (metis (lifting, no_types) Collect_cong Range.intros Range_empty Range_insert mem_Collect_eq singleton_conv singleton_iff trancl.r_into_trancl trancl_range)
lemma canAccessThis_simp2: "canAccessThis  vertex_1  succ_tran nodes = {vertex_1, canAccessThis}, edges = {(vertex_1, canAccessThis)} canAccessThis = {}"
apply (simp add: succ_tran_def)
by (metis Domain.DomainI Domain_empty Domain_insert singleton_iff trancl_domain)
lemma canAccessThis_simp3: 
  "canAccessThis  vertex_1  {(e1, e2). e1 = vertex_1  e2 = canAccessThis  (e1 = vertex_1  e2  canAccessThis)} = {}" by blast
lemma canAccessThis_simp4: 
  "canAccessThis  vertex_1  {vertex_1, canAccessThis, vertex_1, canAccessThis} = {vertex_1, canAccessThis}" by blast
lemmas example_simps = unique_default_example_simp1 unique_default_example2 unique_default_example3 
    unique_default_example_simp2 unique_default_example1 succ_tran_empty vertex_1_vertex_2_set_simp
    unique_default_example_simp3 vertex_set_simp2 canAccessThis_simp1 canAccessThis_simp2 canAccessThis_simp3
    canAccessThis_simp4
(*>*)
end

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 *: "fset_offending_flows nodes = nodesG, edges = edgesG nP"

    from * have 1: "sinvar nodes = nodesG, edges = edgesG - f  nP"
      by (metis (hide_lams, 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 (hide_lams, 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 *: "fset_offending_flows nodes = nodesG, edges = edgesG nP"

    from * have 1: "sinvar nodes = nodesG, edges = edgesG - f  nP"
      by (metis (hide_lams, 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 *: "fset_offending_flows nodes = nodesG, edges = edgesG nP"
    from * have 1: "sinvar nodes = nodesG, edges = edgesG - f  nP"
      by (metis (hide_lams, 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

Theory SINVAR_Subnets2

theory SINVAR_Subnets2
imports"../TopoS_Helper"
begin


(*EXPERIMENTAL!!*)

subsection ‹SecurityInvariant Subnets2›

text‹Warning, This is just a test. Please look at @{file ‹SINVAR_Subnets.thy›}.
This security invariant has the following changes, compared to @{file ‹SINVAR_Subnets.thy›}:
A new BorderRouter' is introduced which can send to the members of its subnet.
A new InboundRouter is accessible by anyone. It can access all other routers and the outside.
›


datatype subnets = Subnet nat | BorderRouter nat | BorderRouter' nat | InboundRouter | Unassigned

definition default_node_properties :: "subnets"
  where "default_node_properties  Unassigned"

fun allowed_subnet_flow :: "subnets  subnets  bool" where
  "allowed_subnet_flow (Subnet s1) (Subnet s2) = (s1 = s2)" | 
  "allowed_subnet_flow (Subnet s1) (BorderRouter s2) = (s1 = s2)" |
  "allowed_subnet_flow (Subnet s1) (BorderRouter' s2) = (s1 = s2)" |
  "allowed_subnet_flow (Subnet _) _ = True" | 
  "allowed_subnet_flow (BorderRouter _) (Subnet _) = False" |
  "allowed_subnet_flow (BorderRouter _) _ = True" |
  "allowed_subnet_flow (BorderRouter' s1) (Subnet s2) = (s1 = s2)" |
  "allowed_subnet_flow (BorderRouter' _) _ = True" | 
  "allowed_subnet_flow InboundRouter (Subnet _) = False" | 
  "allowed_subnet_flow InboundRouter _ = True" | 
  "allowed_subnet_flow Unassigned Unassigned  = True" |
  "allowed_subnet_flow Unassigned InboundRouter  = True" |
  "allowed_subnet_flow Unassigned _  = False"

fun sinvar :: "'v graph  ('v  subnets)  bool" where
  "sinvar G nP = ( (e1,e2)  edges G. allowed_subnet_flow (nP e1) (nP e2))"


definition receiver_violation :: "bool" where "receiver_violation = False"


text‹Only members of the same subnet or their @{const BorderRouter'} can access them.›
lemma "allowed_subnet_flow a (Subnet s1)  a = (BorderRouter' s1)  a = (Subnet s1)"
  apply(cases a)
      apply(simp_all)
  done


subsubsection ‹Preliminaries›
  lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
    apply(simp only: SecurityInvariant_withOffendingFlows.sinvar_mono_def)
    apply(clarify)
    by auto
  
  interpretation SecurityInvariant_preliminaries
  where sinvar = sinvar
    apply unfold_locales
      apply(frule_tac finite_distinct_list[OF wf_graph.finiteE])
      apply(erule_tac exE)
      apply(rename_tac list_edges)
      apply(rule_tac ff="list_edges" in SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono])
         apply(auto)[6]
     apply(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
    apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])
   done




subsubsection‹ENF›
  lemma All_to_Unassigned: " e1. allowed_subnet_flow e1 Unassigned"
    by (rule allI, case_tac e1, simp_all)
  lemma Unassigned_default_candidate: " nP e1 e2. ¬ allowed_subnet_flow (nP e1) (nP e2)  ¬ allowed_subnet_flow Unassigned (nP e2)"
    apply(intro allI)
    apply(case_tac "nP e2")
       apply simp_all
     apply(case_tac "nP e1")
         apply simp_all
    by(simp add: All_to_Unassigned)
  lemma allowed_subnet_flow_refl: " e. allowed_subnet_flow e e"
    by(rule allI, case_tac e, simp_all)
  lemma Subnets_ENF: "SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form sinvar allowed_subnet_flow"
    unfolding SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form_def
    by simp
  lemma Subnets_ENF_refl: "SecurityInvariant_withOffendingFlows.ENF_refl sinvar allowed_subnet_flow"
    unfolding SecurityInvariant_withOffendingFlows.ENF_refl_def
    apply(rule conjI)
     apply(simp add: Subnets_ENF)
    apply(simp add: allowed_subnet_flow_refl)
  done


  definition Subnets_offending_set:: "'v graph  ('v  subnets)  ('v × 'v) set set" where
  "Subnets_offending_set G nP = (if sinvar G nP then
      {}
     else 
      { {e  edges G. case e of (e1,e2)  ¬ allowed_subnet_flow (nP e1) (nP e2)} })"
  lemma Subnets_offending_set: 
  "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = Subnets_offending_set"
    apply(simp only: fun_eq_iff ENF_offending_set[OF Subnets_ENF] Subnets_offending_set_def)
    apply(rule allI)+
    apply(rename_tac G nP)
    apply(auto)
  done


interpretation Subnets: SecurityInvariant_ACS
where default_node_properties = SINVAR_Subnets2.default_node_properties
and sinvar = SINVAR_Subnets2.sinvar
rewrites "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = Subnets_offending_set"
  unfolding SINVAR_Subnets2.default_node_properties_def
  apply unfold_locales
    apply(rule ballI)
    apply (rule SecurityInvariant_withOffendingFlows.ENF_fsts_refl_instance[OF Subnets_ENF_refl Unassigned_default_candidate])[1]
     apply(simp_all)[2]
   apply(erule default_uniqueness_by_counterexample_ACS)
   apply (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_def)
   apply (simp add:graph_ops)
   apply (simp split: prod.split_asm prod.split)
   apply(rule_tac x=" nodes={vertex_1,vertex_2}, edges = {(vertex_1,vertex_2)} " in exI, simp)
   apply(rule conjI)
    apply(simp add: wf_graph_def)
   apply(case_tac otherbot, simp_all)
      apply(rename_tac mysubnetcase)
      apply(rule_tac x="(λ x. Unassigned)(vertex_1 := Unassigned, vertex_2 := BorderRouter mysubnetcase)" in exI, simp)
      apply(rule_tac x="vertex_1" in exI, simp)
      apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
     apply(rule_tac x="(λ x. Unassigned)(vertex_1 := Unassigned, vertex_2 := BorderRouter whatever)" in exI, simp)
     apply(rule_tac x="vertex_1" in exI, simp)
     apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
    apply(rule_tac x="(λ x. Unassigned)(vertex_1 := Unassigned, vertex_2 := BorderRouter whatever)" in exI, simp)
    apply(rule_tac x="vertex_1" in exI, simp)
    apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
   apply(rule_tac x="(λ x. Unassigned)(vertex_1 := Unassigned, vertex_2 := BorderRouter whatever)" in exI, simp)
   apply(rule_tac x="vertex_1" in exI, simp)
   apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
  apply(fact Subnets_offending_set)
 done


  lemma TopoS_Subnets2: "SecurityInvariant sinvar default_node_properties receiver_violation"
  unfolding receiver_violation_def by unfold_locales


hide_fact (open) sinvar_mono   
hide_const (open) sinvar receiver_violation default_node_properties

end

Theory SINVAR_BLPstrict

theory SINVAR_BLPstrict
imports "../TopoS_Helper"
begin

subsection ‹Stricter Bell LaPadula SecurityInvariant›
text‹All unclassified data sources must be labeled, default assumption: all is secret.

Warning: This is considered here an access control strategy.
By default, everything is secret and one explicitly prohibits sending to non-secret hosts.›

datatype security_level = Unclassified | Confidential | Secret

(*total order*)
instantiation security_level :: linorder
  begin
  fun less_eq_security_level :: "security_level  security_level  bool" where
    "(Unclassified  Unclassified) = True" |
    "(Confidential  Confidential) = True" |
    "(Secret  Secret) = True" |
    "(Unclassified  Confidential) = True" |
    "(Confidential  Secret) = True"  |
    "(Unclassified  Secret) = True"  |
    "(Secret  Confidential) = False"  |
    "(Confidential  Unclassified) = False"  |
    "(Secret  Unclassified) = False"

  fun less_security_level :: "security_level  security_level  bool" where
    "(Unclassified < Unclassified) = False" |
    "(Confidential < Confidential) = False" |
    "(Secret < Secret) = False" |
    "(Unclassified < Confidential) = True" |
    "(Confidential < Secret) = True"  |
    "(Unclassified < Secret) = True"  |
    "(Secret < Confidential) = False"  |
    "(Confidential < Unclassified) = False"  |
    "(Secret < Unclassified) = False"
  instance
    apply(intro_classes)
    apply(case_tac [!] x)
    apply(simp_all)
    apply(case_tac  [!] y)
    apply(simp_all)
    apply(case_tac  [!] z)
    apply(simp_all)
    done
  end
  


definition default_node_properties :: "security_level"
  where  "default_node_properties  Secret"



fun sinvar :: "'v graph  ('v  security_level)  bool" where
  "sinvar G nP = ( (e1,e2)  edges G. (nP e1)  (nP e2))"

definition receiver_violation :: "bool" where "receiver_violation  False"


lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
  apply(simp only: SecurityInvariant_withOffendingFlows.sinvar_mono_def)
  apply(clarify)
  by auto


interpretation SecurityInvariant_preliminaries
where sinvar = sinvar
  apply unfold_locales
    apply(frule_tac finite_distinct_list[OF wf_graph.finiteE])
    apply(erule_tac exE)
    apply(rename_tac list_edges)
    apply(rule_tac ff="list_edges" in SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono])
        apply(auto)[6]
   apply(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
  apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])
 done



subsection ‹ENF›
  lemma secret_default_candidate: " (nP::('v  security_level)) e1 e2. ¬ (nP e1)  (nP e2)  ¬ Secret  (nP e2)"
    apply(case_tac "nP e1")
    apply(simp_all)
    apply(case_tac [!] "nP e2")
    apply(simp_all)
    done
  lemma BLP_ENF: "SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form sinvar (≤)"
    unfolding SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form_def
    by simp
  lemma BLP_ENF_refl: "SecurityInvariant_withOffendingFlows.ENF_refl sinvar (≤)"
    unfolding SecurityInvariant_withOffendingFlows.ENF_refl_def
    apply(rule conjI)
     apply(simp add: BLP_ENF)
    apply(simp)
  done

  definition BLP_offending_set:: "'v graph  ('v  security_level)  ('v × 'v) set set" where
  "BLP_offending_set G nP = (if sinvar G nP then
      {}
     else 
      { {e  edges G. case e of (e1,e2)  (nP e1) > (nP e2)} })"
  lemma BLP_offending_set: "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = BLP_offending_set"
    apply(simp only: fun_eq_iff SecurityInvariant_withOffendingFlows.ENF_offending_set[OF BLP_ENF] BLP_offending_set_def)
    apply(rule allI)+
    apply(rename_tac G nP)
    apply(auto)
  done
   
  interpretation BLPstrict: SecurityInvariant_ACS sinvar default_node_properties
  (*TODO: why is there a where and no "rewrites" in the afp?*)
  rewrites "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = BLP_offending_set"
    unfolding default_node_properties_def
    apply(unfold_locales)
      apply(rule ballI)
      apply(rule SecurityInvariant_withOffendingFlows.ENF_fsts_refl_instance[OF BLP_ENF_refl])
         apply(simp_all add: BLP_ENF BLP_ENF_refl)[3]
      apply(simp add: secret_default_candidate; fail)
     apply(erule default_uniqueness_by_counterexample_ACS)
     apply(rule_tac x=" nodes=set [vertex_1,vertex_2], edges = set [(vertex_1,vertex_2)] " in exI, simp)
     apply(simp add: BLP_offending_set graph_ops wf_graph_def)
     apply(rule_tac x="(λ x. Secret)(vertex_1 := Secret, vertex_2 := Confidential)" in exI, simp)
     apply(rule_tac x="vertex_1" in exI, simp)
     apply(rule_tac x="set [(vertex_1,vertex_2)]" in exI, simp)
     apply(simp add: BLP_offending_set_def)
     apply(rule conjI)
      apply fastforce
     apply (case_tac otherbot, simp_all)
    apply(fact BLP_offending_set)
   done


  lemma TopoS_BLPstrict: "SecurityInvariant sinvar default_node_properties receiver_violation"
  unfolding receiver_violation_def by unfold_locales
   
hide_fact (open) sinvar_mono   

hide_const (open) sinvar receiver_violation default_node_properties

end

Theory SINVAR_Tainting

theory SINVAR_Tainting
imports "../TopoS_Helper"
begin

subsection ‹SecurityInvariant Tainting for IFS›

context
begin

  qualified type_synonym taints = "string set"

  text‹Warning: an infinite set has cardinality 0›
  lemma "card (UNIV::taints) = 0" by (simp add: infinite_UNIV_listI) 
  
  qualified definition default_node_properties :: "taints"
    where  "default_node_properties  {}"
  
  
  (*The definition we want to present*)
  text‹For all nodes @{term n} in the graph, for all nodes @{term r} which are reachable from @{term n},
        node @{term n} needs the appropriate tainting fields which are set by @{term r}
  definition sinvar_tainting :: "'v graph  ('v  taints)  bool" where
    "sinvar_tainting G nP   n  (nodes G). r  (succ_tran G n). nP n  nP r"
  
  
  private lemma sinvar_tainting_edges_def: "wf_graph G 
    sinvar_tainting G nP  ( (v1,v2)  edges G. r  (succ_tran G v1). nP v1  nP r)"
    unfolding sinvar_tainting_def
    proof
      assume a1: "wf_graph G"
        and  a2: "nnodes G. rsucc_tran G n. nP n  nP r"
        from a1[simplified wf_graph_def] have f1: "fst ` edges G  nodes G" by simp
        from f1 a2 have "v  (fst ` edges G). rsucc_tran G v. nP v  nP r" by auto
        thus "(v1, _)edges G. rsucc_tran G v1. nP v1  nP r" by fastforce
      next
      assume a1: "wf_graph G"
        and  a2: "(v1, v2)edges G. rsucc_tran G v1. nP v1  nP r"
        from a2 have g1: " v  (fst ` edges G). rsucc_tran G v. nP v  nP r" by fastforce
        from FiniteGraph.succ_tran_empty[OF a1]
        have g2: " v. v  (fst ` edges G)  (rsucc_tran G v. nP v  nP r)" by blast
        from g1 g2 show "nnodes G. rsucc_tran G n. nP n  nP r" by metis
    qed
  
  text‹Alternative definition of the @{const sinvar_tainting}
  
  qualified definition sinvar :: "'v graph  ('v  taints)  bool" where
    "sinvar G nP   (v1,v2)  edges G. nP v1  nP v2"
  
  
  qualified lemma sinvar_preferred_def:
    "wf_graph G  sinvar_tainting G nP = sinvar G nP"
    proof(unfold sinvar_tainting_edges_def sinvar_def, rule iffI, goal_cases)
    case 2
        have "(v, v')  (edges G)+  nP v  nP v'" for v v'
          proof(induction rule: trancl_induct)
          case base thus ?case using 2(2) by fastforce
          next
          case step thus ?case using 2(2) by fastforce
          qed
        thus ?case
        by(simp add: succ_tran_def)
      next
      case 1
        from 1(1)[simplified wf_graph_def] have f1: "fst ` edges G  nodes G" by simp
        from f1 1(2) have "v  (fst ` edges G). v'succ_tran G v. nP v  nP v'" by fastforce
        thus ?case unfolding succ_tran_def by fastforce
    qed
  
  
  text‹Information Flow Security›
  qualified definition receiver_violation :: "bool" where "receiver_violation  True"
  
  
  private lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
    apply(simp add: SecurityInvariant_withOffendingFlows.sinvar_mono_def sinvar_def)
    apply(clarify)
    by blast
  interpretation SecurityInvariant_preliminaries
  where sinvar = sinvar
  proof(unfold_locales, goal_cases)
    case (1 G nP)
      from 1 show ?case
      apply(frule_tac finite_distinct_list[OF wf_graph.finiteE])
      apply(erule_tac exE)
      apply(rename_tac list_edges)
      apply(rule_tac ff="list_edges" in SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono])
          apply(auto simp add: sinvar_def)
       apply(auto simp add: sinvar_def SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
      done
    next
    case (2 N E E' nP) thus ?case by(simp add: sinvar_def) blast
    next
    case 3 thus ?case by(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])
  qed
  
  
  
  private  lemma Taints_def_unique: "otherbot  {} 
      G p i f. wf_graph G  ¬ sinvar G p  f  (SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G p) 
         sinvar (delete_edges G f) p 
          i  snd ` f  sinvar G (p(i := otherbot)) "
    apply(simp)
    apply (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
        SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
        SecurityInvariant_withOffendingFlows.is_offending_flows_def)
    apply (simp add:graph_ops)
    apply (simp split: prod.split_asm prod.split)
    apply(rule_tac x=" nodes=set [vertex_1,vertex_2], edges = set [(vertex_1,vertex_2)] " in exI, simp)
    apply(rule conjI)
     apply(simp add: wf_graph_def; fail)
    apply(subgoal_tac "foo. foo  otherbot")
     prefer 2
     subgoal by fastforce
    apply(erule exE, rename_tac foo)
    apply(rule_tac x="(λ x. {})(vertex_1 := {foo}, vertex_2 := {})" in exI)
    apply(rule conjI)
     apply(simp add: sinvar_def; fail)
    apply(rule_tac x="vertex_2" in exI)
    apply(rule_tac x="set [(vertex_1,vertex_2)]" in exI, simp)
    apply(simp add: sinvar_def)
    done
  
  
  
  subsubsection ‹ENF›
    private lemma Taints_ENF: "SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form sinvar (⊆)"
      unfolding SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form_def sinvar_def
      by simp
    private lemma Taints_ENF_refl: "SecurityInvariant_withOffendingFlows.ENF_refl sinvar (⊆)"
      unfolding SecurityInvariant_withOffendingFlows.ENF_refl_def
       by(auto simp add: Taints_ENF)
  
    qualified definition Taints_offending_set:: "'v graph  ('v  taints)  ('v × 'v) set set" where
    "Taints_offending_set G nP = (if sinvar G nP then
        {}
       else 
        { {e  edges G. case e of (e1,e2)  ¬ (nP e1)  (nP e2)} })"
    lemma Taints_offending_set: "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = Taints_offending_set"
      by(auto simp add: fun_eq_iff
                        SecurityInvariant_withOffendingFlows.ENF_offending_set[OF Taints_ENF]
                        Taints_offending_set_def)
     
  
    interpretation Taints: SecurityInvariant_IFS sinvar default_node_properties
    rewrites "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = Taints_offending_set"
      unfolding receiver_violation_def
      unfolding default_node_properties_def
      proof(unfold_locales, goal_cases)
      case 1
        from 1(2) show ?case
        apply(intro ballI)
        apply(rule SecurityInvariant_withOffendingFlows.ENF_snds_refl_instance[OF Taints_ENF_refl])
          apply(simp_all add: Taints_ENF Taints_ENF_refl)
        by blast
      next
      case 2 thus ?case
        proof(elim default_uniqueness_by_counterexample_IFS)
        qed(fact Taints_def_unique)
      next
      case 3 show "set_offending_flows = Taints_offending_set" by(fact Taints_offending_set)
     qed
  
  
    lemma TopoS_Tainting: "SecurityInvariant sinvar default_node_properties receiver_violation"
    unfolding receiver_violation_def by unfold_locales

end

end

Theory SINVAR_BLPbasic

theory SINVAR_BLPbasic
imports "../TopoS_Helper"
begin

subsection ‹SecurityInvariant Basic Bell LaPadula›

type_synonym security_level = nat

definition default_node_properties :: "security_level"
  where  "default_node_properties  0"

fun sinvar :: "'v graph  ('v  security_level)  bool" where
  "sinvar G nP = ( (e1,e2)  edges G. (nP e1)  (nP e2))"

text‹What we call a