Theory TopoS_Composition_Theory

theory TopoS_Composition_Theory
imports TopoS_Interface TopoS_Helper
begin

section‹Composition Theory›

text‹Several invariants may apply to one policy.›

text‹The security invariants are all collected in a list. 
The list corresponds to the security requirements. 
The list should have the type @{typ "('v graph ⇒ bool) list"}, i.e.\ a list of predicates over the policy. 
We need in instantiated security invariant, i.e.\ get rid of @{typ "'a"} and @{typ "'b"}›

 ― ‹An instance (configured) a security invariant I.e.\ a concrete security requirement, in different terminology.›
 record ('v) SecurityInvariant_configured =
    c_sinvar::"('v) graph ⇒ bool"
    c_offending_flows::"('v) graph ⇒ ('v × 'v) set set"
    c_isIFS::"bool"

  ― ‹parameters 1-3 are the @{text "SecurityInvariant"}:
      @{text sinvar} @{text "⊥"} @{text "receiver_violation"}

      Fourth parameter is the host attribute mapping @{text nP}

      
      TODO: probably check @{text "wf_graph"} here and optionally some host-attribute sanity checker as in DomainHierachy.›
  fun new_configured_SecurityInvariant ::
    "((('v::vertex) graph ⇒ ('v ⇒ 'a) ⇒ bool) × 'a × bool × ('v ⇒ 'a)) ⇒ ('v SecurityInvariant_configured) option" where 
      "new_configured_SecurityInvariant (sinvar, defbot, receiver_violation, nP) = 
        ( 
        if SecurityInvariant sinvar defbot receiver_violation then 
          Some ⦇ 
            c_sinvar = (λG. sinvar G nP),
            c_offending_flows = (λG. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP),
            c_isIFS = receiver_violation
          ⦈
        else None
        )"

   declare new_configured_SecurityInvariant.simps[simp del]

   lemma new_configured_TopoS_sinvar_correct:
   "SecurityInvariant sinvar defbot receiver_violation ⟹ 
   c_sinvar (the (new_configured_SecurityInvariant (sinvar, defbot, receiver_violation, nP))) = (λG. sinvar G nP)"
   by(simp add: Let_def new_configured_SecurityInvariant.simps)

   lemma new_configured_TopoS_offending_flows_correct:
   "SecurityInvariant sinvar defbot receiver_violation ⟹ 
   c_offending_flows (the (new_configured_SecurityInvariant (sinvar, defbot, receiver_violation, nP))) = 
   (λG. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP)"
   by(simp add: Let_def new_configured_SecurityInvariant.simps)


text‹We now collect all the core properties of a security invariant, but without the @{typ "'a"} @{typ "'b"} 
      types, so it is instantiated with a concrete configuration.›
locale configured_SecurityInvariant =
  fixes m :: "('v::vertex) SecurityInvariant_configured"
  assumes
    ― ‹As in SecurityInvariant definition›
    valid_c_offending_flows:
    "c_offending_flows m G = {F. F ⊆ (edges G) ∧ ¬ c_sinvar m G ∧ c_sinvar m (delete_edges G F) ∧ 
      (∀ (e1, e2) ∈ F. ¬ c_sinvar m (add_edge e1 e2 (delete_edges G F)))}"
  and
    ― ‹A empty network can have no security violations›
    defined_offending:
    "⟦ wf_graph ⦇ nodes = N, edges = {} ⦈ ⟧ ⟹ c_sinvar m ⦇ nodes = N, edges = {}⦈"
  and
    ― ‹prohibiting more does not decrease security›
    mono_sinvar:
    "⟦ wf_graph ⦇ nodes = N, edges = E ⦈; E' ⊆ E; c_sinvar m ⦇ nodes = N, edges = E ⦈ ⟧ ⟹ 
      c_sinvar m ⦇ nodes = N, edges = E' ⦈"
  begin
    (*compatibility with other definitions*)
    lemma sinvar_monoI: 
    "SecurityInvariant_withOffendingFlows.sinvar_mono (λ (G::('v::vertex) graph) (nP::'v ⇒ 'a). c_sinvar m G)"
      apply(simp add: SecurityInvariant_withOffendingFlows.sinvar_mono_def, clarify)
      by(fact mono_sinvar)

    text‹if the network where nobody communicates with anyone fulfilles its security requirement,
          the offending flows are always defined.›
    lemma defined_offending': 
      "⟦ wf_graph G; ¬ c_sinvar m G ⟧ ⟹ c_offending_flows m G ≠ {}"
      proof -
        assume a1: "wf_graph G"
        and    a2: "¬ c_sinvar m G"
        have subst_set_offending_flows: 
        "⋀nP. SecurityInvariant_withOffendingFlows.set_offending_flows (λG nP. c_sinvar m G) G nP = c_offending_flows m G"
        by(simp add: valid_c_offending_flows fun_eq_iff 
            SecurityInvariant_withOffendingFlows.set_offending_flows_def
            SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
            SecurityInvariant_withOffendingFlows.is_offending_flows_def)

        from a1 have wfG_empty: "wf_graph ⦇nodes = nodes G, edges = {}⦈" by(simp add:wf_graph_def)

        from a1 have "⋀nP. ¬ c_sinvar m G ⟹ SecurityInvariant_withOffendingFlows.set_offending_flows (λG nP. c_sinvar m G) G nP ≠ {}"
          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_monoI])
          by(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def delete_edges_simp2 defined_offending[OF wfG_empty])
      
          thus ?thesis by(simp add: a2 subst_set_offending_flows)
    qed

    (* The offending flows definitions are equal, compatibility *)
    lemma subst_offending_flows: "⋀ nP. SecurityInvariant_withOffendingFlows.set_offending_flows (λG nP. c_sinvar m G) G nP = c_offending_flows m G"
      apply (unfold SecurityInvariant_withOffendingFlows.set_offending_flows_def
            SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
            SecurityInvariant_withOffendingFlows.is_offending_flows_def)
      by(simp add: valid_c_offending_flows)

    text‹all the @{term SecurityInvariant_preliminaries} stuff must hold, for an arbitrary @{term nP}›
    lemma SecurityInvariant_preliminariesD:
      "SecurityInvariant_preliminaries (λ (G::('v::vertex) graph) (nP::'v ⇒ 'a). c_sinvar m G)"
      proof(unfold_locales, goal_cases)
      case 1 thus ?case using defined_offending' by(simp add: subst_offending_flows)
      next case 2 thus ?case by(fact mono_sinvar)
      next case 3 thus ?case by(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_monoI])
      qed

    lemma negative_mono:
     "⋀ N E' E. wf_graph ⦇ nodes = N, edges = E ⦈ ⟹ 
        E' ⊆ E ⟹ ¬ c_sinvar m ⦇ nodes = N, edges = E' ⦈ ⟹ ¬ c_sinvar m ⦇ nodes = N, edges = E ⦈"
     by(blast dest: mono_sinvar)

    
    subsection‹Reusing Lemmata›
      lemmas mono_extend_set_offending_flows =
      SecurityInvariant_preliminaries.mono_extend_set_offending_flows[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm mono_extend_set_offending_flows [no_vars]}›

      lemmas offending_flows_union_mono =
      SecurityInvariant_preliminaries.offending_flows_union_mono[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm offending_flows_union_mono [no_vars]}›

      lemmas sinvar_valid_remove_flattened_offending_flows =
      SecurityInvariant_preliminaries.sinvar_valid_remove_flattened_offending_flows[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm sinvar_valid_remove_flattened_offending_flows [no_vars]}›

      lemmas sinvar_valid_remove_SOME_offending_flows =
      SecurityInvariant_preliminaries.sinvar_valid_remove_SOME_offending_flows[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm sinvar_valid_remove_SOME_offending_flows [no_vars]}›


      lemmas sinvar_valid_remove_minimalize_offending_overapprox =
      SecurityInvariant_preliminaries.sinvar_valid_remove_minimalize_offending_overapprox[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm sinvar_valid_remove_minimalize_offending_overapprox [no_vars]}›
      

      lemmas empty_offending_contra =
      SecurityInvariant_withOffendingFlows.empty_offending_contra[where sinvar="(λG nP. c_sinvar m G)", simplified subst_offending_flows]
      text‹@{thm empty_offending_contra [no_vars]}›

      lemmas Un_set_offending_flows_bound_minus_subseteq = 
      SecurityInvariant_preliminaries.Un_set_offending_flows_bound_minus_subseteq[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm Un_set_offending_flows_bound_minus_subseteq [no_vars]}›

      lemmas Un_set_offending_flows_bound_minus_subseteq' = 
      SecurityInvariant_preliminaries.Un_set_offending_flows_bound_minus_subseteq'[OF SecurityInvariant_preliminariesD, simplified subst_offending_flows]
      text‹@{thm Un_set_offending_flows_bound_minus_subseteq' [no_vars]}›
end

thm configured_SecurityInvariant_def
text‹@{thm configured_SecurityInvariant_def [no_vars]}›

thm configured_SecurityInvariant.mono_sinvar
text‹@{thm configured_SecurityInvariant.mono_sinvar [no_vars]}›



text‹
  Naming convention:
    m :: network security requirement
    M :: network security requirement list
›

  text‹The function @{term new_configured_SecurityInvariant} takes some tuple and if it returns a result,
         the locale assumptions are automatically fulfilled.›
  theorem new_configured_SecurityInvariant_sound: 
  "⟦ new_configured_SecurityInvariant (sinvar, defbot, receiver_violation, nP) = Some m ⟧ ⟹
    configured_SecurityInvariant m"
    proof -
      assume a: "new_configured_SecurityInvariant (sinvar, defbot, receiver_violation, nP) = Some m"
      hence NetModel: "SecurityInvariant sinvar defbot receiver_violation"
        by(simp add: new_configured_SecurityInvariant.simps split: if_split_asm)
      hence NetModel_p: "SecurityInvariant_preliminaries sinvar" by(simp add: SecurityInvariant_def)

      from a have c_eval: "c_sinvar m = (λG. sinvar G nP)"
         and c_offending: "c_offending_flows m = (λG. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar G nP)"
         and "c_isIFS m = receiver_violation"
        by(auto simp add: new_configured_SecurityInvariant.simps NetModel split: if_split_asm)

      have monoI: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
        apply(simp add: SecurityInvariant_withOffendingFlows.sinvar_mono_def, clarify)
        by(fact SecurityInvariant_preliminaries.mono_sinvar[OF NetModel_p])
      from SecurityInvariant_withOffendingFlows.valid_empty_edges_iff_exists_offending_flows[OF monoI, symmetric]
            SecurityInvariant_preliminaries.defined_offending[OF NetModel_p]
      have eval_empty_graph: "⋀ N nP. wf_graph ⦇nodes = N, edges = {}⦈ ⟹ sinvar ⦇nodes = N, edges = {}⦈ nP"
      by fastforce

       show ?thesis
        apply(unfold_locales)
          apply(simp add: c_eval c_offending SecurityInvariant_withOffendingFlows.set_offending_flows_def SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def SecurityInvariant_withOffendingFlows.is_offending_flows_def)
         apply(simp add: c_eval eval_empty_graph)
        apply(simp add: c_eval,drule(3) SecurityInvariant_preliminaries.mono_sinvar[OF NetModel_p])
        done
   qed

text‹All security invariants are valid according to the definition›
definition valid_reqs :: "('v::vertex) SecurityInvariant_configured list ⇒ bool" where
  "valid_reqs M ≡ ∀ m ∈ set M. configured_SecurityInvariant m"

 subsection ‹Algorithms›
    text‹A (generic) security invariant corresponds to a type of security requirements (type: @{typ "'v graph ⇒ ('v ⇒ 'a) ⇒ bool"}).
          A configured security invariant is a security requirement in a scenario specific setting (type: @{typ "'v graph ⇒ bool"}).
          I.e., it is a security requirement as listed in the requirements document.
          All security requirements are fulfilled for a fixed policy @{term G} if all security requirements are fulfilled for @{term G}.›


    text‹Get all possible offending flows from all security requirements›
    definition get_offending_flows :: "'v SecurityInvariant_configured list ⇒ 'v graph ⇒ (('v × 'v) set set)" where
      "get_offending_flows M G = (⋃m∈set M. c_offending_flows m G)"  

    (*Note: only checks sinvar, not eval!! No 'a 'b type variables here*)
    definition all_security_requirements_fulfilled :: "('v::vertex) SecurityInvariant_configured list ⇒ 'v graph ⇒ bool" where
      "all_security_requirements_fulfilled M G ≡ ∀m ∈ set M. (c_sinvar m) G"
    
    text‹Generate a valid topology from the security requirements›
    (*constant G, remove after algorithm*)
    fun generate_valid_topology :: "'v SecurityInvariant_configured list ⇒ 'v graph ⇒ 'v graph" where
      "generate_valid_topology [] G = G" |
      "generate_valid_topology (m#Ms) G = delete_edges (generate_valid_topology Ms G) (⋃ (c_offending_flows m G))"

     ― ‹return all Access Control Strategy models from a list of models›
    definition get_ACS :: "('v::vertex) SecurityInvariant_configured list ⇒ 'v SecurityInvariant_configured list" where
      "get_ACS M ≡ [m ← M. ¬ c_isIFS m]"
     ― ‹return all Information Flows Strategy models from a list of models›
    definition get_IFS :: "('v::vertex) SecurityInvariant_configured list ⇒ 'v SecurityInvariant_configured list" where
      "get_IFS M ≡ [m ← M. c_isIFS m]"
    lemma get_ACS_union_get_IFS: "set (get_ACS M) ∪ set (get_IFS M) = set M"
      by(auto simp add: get_ACS_def get_IFS_def)
  

   subsection‹Lemmata›
    lemma valid_reqs1: "valid_reqs (m # M) ⟹ configured_SecurityInvariant m"
      by(simp add: valid_reqs_def)
    lemma valid_reqs2: "valid_reqs (m # M) ⟹ valid_reqs M"
      by(simp add: valid_reqs_def)
    lemma get_offending_flows_alt1: "get_offending_flows M G = ⋃ {c_offending_flows m G | m. m ∈ set M}"
      apply(simp add: get_offending_flows_def)
      by fastforce
    lemma get_offending_flows_un: "⋃(get_offending_flows M G) = (⋃m∈set M. ⋃(c_offending_flows m G))"
      apply(simp add: get_offending_flows_def)
      by blast
  
  
    lemma all_security_requirements_fulfilled_mono:
      "⟦ valid_reqs M; E' ⊆ E; wf_graph ⦇ nodes = V, edges = E ⦈ ⟧ ⟹  
        all_security_requirements_fulfilled M ⦇ nodes = V, edges = E ⦈ ⟹
        all_security_requirements_fulfilled M ⦇ nodes = V, edges = E' ⦈"
        apply(induction M arbitrary: E' E)
         apply(simp_all add: all_security_requirements_fulfilled_def)
        apply(rename_tac m M E' E)
        apply(rule conjI)
         apply(erule(2) configured_SecurityInvariant.mono_sinvar[OF valid_reqs1])
         apply(simp_all)
        apply(drule valid_reqs2)
        apply blast
        done

    subsection‹generate valid topology›
    (*
      lemma generate_valid_topology_def_delete_multiple: 
        "generate_valid_topology M G = delete_edges (generate_valid_topology M G) (⋃ (get_offending_flows M G))"
        proof(induction M arbitrary: G)
          case Nil
            thus ?case by(simp add: get_offending_flows_def)
          next
          case (Cons m M)
            from Cons[simplified delete_edges_simp2 get_offending_flows_def] 
            have "edges (generate_valid_topology M G) = edges (generate_valid_topology M G) - ⋃(⋃m∈set M. c_offending_flows m G)"
              by (metis graph.select_convs(2))
            thus ?case
              apply(simp add: get_offending_flows_def delete_edges_simp2)
              by blast
        qed*)
      lemma generate_valid_topology_nodes:
      "nodes (generate_valid_topology M G) = (nodes G)"
        apply(induction M arbitrary: G)
         by(simp_all add: graph_ops)

      lemma generate_valid_topology_def_alt:
        "generate_valid_topology M G = delete_edges G (⋃ (get_offending_flows M G))"
        proof(induction M arbitrary: G)
          case Nil
            thus ?case by(simp add: get_offending_flows_def)
          next
          case (Cons m M)
            from Cons[simplified delete_edges_simp2 get_offending_flows_def] 
            have "edges (generate_valid_topology M G) = edges G - ⋃(⋃m∈set M. c_offending_flows m G)"
              by (metis graph.select_convs(2))
            thus ?case
              apply(simp add: get_offending_flows_def delete_edges_simp2)
              apply(rule)
               apply(simp add: generate_valid_topology_nodes)
              by blast
        qed
    
      lemma wf_graph_generate_valid_topology: "wf_graph G ⟹ wf_graph (generate_valid_topology M G)"
        proof(induction M arbitrary: G)
        qed(simp_all)
  
     lemma generate_valid_topology_mono_models:
      "edges (generate_valid_topology (m#M) ⦇ nodes = V, edges = E ⦈) ⊆ edges (generate_valid_topology M ⦇ nodes = V, edges = E ⦈)"
        proof(induction M arbitrary: E m)
        case Nil thus ?case by(simp add: delete_edges_simp2)
        case Cons thus ?case by(simp add: delete_edges_simp2)
      qed
     
      lemma generate_valid_topology_subseteq_edges:
      "edges (generate_valid_topology M G) ⊆ (edges G)"
        proof(induction M arbitrary: G)
        case Cons thus ?case by (simp add: delete_edges_simp2) blast
        qed(simp)

      text‹@{term generate_valid_topology} generates a valid topology (Policy)!›
      theorem generate_valid_topology_sound:
      "⟦ valid_reqs M; wf_graph ⦇nodes = V, edges = E⦈ ⟧ ⟹ 
      all_security_requirements_fulfilled M (generate_valid_topology M ⦇nodes = V, edges = E⦈)"
        proof(induction M arbitrary: V E)
          case Nil
          thus ?case by(simp add: all_security_requirements_fulfilled_def)
        next
          case (Cons m M)
          from valid_reqs1[OF Cons(2)] have validReq: "configured_SecurityInvariant m" .

          from Cons(3) have valid_rmUnOff: "wf_graph ⦇nodes = V, edges = E - ⋃(c_offending_flows m ⦇nodes = V, edges = E⦈) ⦈"
            by(simp add: wf_graph_remove_edges)
          
          from configured_SecurityInvariant.sinvar_valid_remove_flattened_offending_flows[OF validReq Cons(3)]
          have valid_eval_rmUnOff: "c_sinvar m ⦇nodes = V, edges = E - ⋃(c_offending_flows m ⦇nodes = V, edges = E⦈) ⦈" .
    
          from generate_valid_topology_subseteq_edges have edges_gentopo_subseteq: 
            "edges (generate_valid_topology M ⦇nodes = V, edges = E⦈) - ⋃(c_offending_flows m ⦇nodes = V, edges = E⦈)
               ⊆
            E - ⋃(c_offending_flows m ⦇nodes = V, edges = E⦈)"  by fastforce
    
          from configured_SecurityInvariant.mono_sinvar[OF validReq valid_rmUnOff edges_gentopo_subseteq valid_eval_rmUnOff]
          have "c_sinvar m ⦇nodes = V, edges = (edges (generate_valid_topology M ⦇nodes = V, edges = E⦈)) - ⋃(c_offending_flows m ⦇nodes = V, edges = E⦈) ⦈" .
          from this have goal1: 
            "c_sinvar m (delete_edges (generate_valid_topology M ⦇nodes = V, edges = E⦈) (⋃(c_offending_flows m ⦇nodes = V, edges = E⦈)))"
               by(simp add: delete_edges_simp2 generate_valid_topology_nodes)
    
          from valid_reqs2[OF Cons(2)] have "valid_reqs M" .
          from Cons.IH[OF ‹valid_reqs M› Cons(3)] have IH:
            "all_security_requirements_fulfilled M (generate_valid_topology M ⦇nodes = V, edges = E⦈)" .

          have generate_valid_topology_EX_graph_record:
            "∃ hypE. (generate_valid_topology M ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = hypE⦈ "
              apply(induction M arbitrary: V E)
               by(simp_all add: delete_edges_simp2 generate_valid_topology_nodes)
              
          from generate_valid_topology_EX_graph_record obtain E_IH where  E_IH_prop:
            "(generate_valid_topology M ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = E_IH⦈" by blast
    
          from wf_graph_generate_valid_topology[OF Cons(3)] E_IH_prop
          have valid_G_E_IH: "wf_graph ⦇nodes = V, edges = E_IH⦈" by metis
    
          ― ‹@{thm IH[simplified E_IH_prop]}›
          ― ‹@{thm all_security_requirements_fulfilled_mono[OF `valid_reqs M` _  valid_G_E_IH IH[simplified E_IH_prop]]}›
    
          from all_security_requirements_fulfilled_mono[OF ‹valid_reqs M› _  valid_G_E_IH IH[simplified E_IH_prop]] have mono_rule:
            "⋀ E'. E' ⊆ E_IH ⟹ all_security_requirements_fulfilled M ⦇nodes = V, edges = E'⦈" .
    
          have "all_security_requirements_fulfilled M 
            (delete_edges (generate_valid_topology M ⦇nodes = V, edges = E⦈) (⋃(c_offending_flows m ⦇nodes = V, edges = E⦈)))"
            apply(subst E_IH_prop)
            apply(simp add: delete_edges_simp2)
            apply(rule mono_rule)
            by fast
    
          from this have goal2:
            "(∀ma∈set M.
            c_sinvar ma (delete_edges (generate_valid_topology M ⦇nodes = V, edges = E⦈) (⋃(c_offending_flows m ⦇nodes = V, edges = E⦈))))"
            by(simp add: all_security_requirements_fulfilled_def)
    
          from goal1 goal2 
          show  "all_security_requirements_fulfilled (m # M) (generate_valid_topology (m # M) ⦇nodes = V, edges = E⦈)" 
          by (simp add: all_security_requirements_fulfilled_def)
       qed


  lemma generate_valid_topology_as_set: 
  "generate_valid_topology M G = delete_edges G (⋃m ∈ set M. (⋃ (c_offending_flows m G)))"
   apply(induction M arbitrary: G)
    apply(simp_all add: delete_edges_simp2 generate_valid_topology_nodes) by fastforce

  lemma c_offending_flows_subseteq_edges: "configured_SecurityInvariant m ⟹ ⋃(c_offending_flows m G) ⊆ edges G"
    apply(clarify)
    apply(simp only: configured_SecurityInvariant.valid_c_offending_flows)
    apply(thin_tac "configured_SecurityInvariant x" for x)
    by auto


  text‹Does it also generate a maximum topology? It does, if the security invariants are in ENF-form. That means, if 
        all security invariants can be expressed as a predicate over the edges, 
        @{term "∃P. ∀G. c_sinvar m G = (∀(v1,v2) ∈ edges G. P (v1,v2))"}›
  definition max_topo :: "('v::vertex) SecurityInvariant_configured list ⇒ 'v graph ⇒ bool" where
    "max_topo M G ≡ all_security_requirements_fulfilled M G ∧ (
      ∀ (v1, v2) ∈ (nodes G × nodes G) - (edges G). ¬ all_security_requirements_fulfilled M (add_edge v1 v2 G))"

  lemma unique_offending_obtain: 
    assumes m: "configured_SecurityInvariant m" and unique: "c_offending_flows m G = {F}"
    obtains P where "F = {(v1, v2) ∈ edges G. ¬ P (v1, v2)}" and "c_sinvar m G = (∀(v1,v2) ∈ edges G. P (v1, v2))" and 
                    "(∀(v1,v2) ∈ edges G - F. P (v1, v2))"
    proof -
    assume EX: "(⋀P. F = {(v1, v2). (v1, v2) ∈ edges G ∧ ¬ P (v1, v2)} ⟹ c_sinvar m G = (∀(v1, v2)∈edges G. P (v1, v2)) ⟹ ∀(v1, v2)∈edges G - F. P (v1, v2) ⟹ thesis)"

    from unique c_offending_flows_subseteq_edges[OF m] have "F ⊆ edges G" by force
    from this obtain P where "F = {e ∈ edges G. ¬ P e}" by (metis double_diff set_diff_eq subset_refl)
    hence 1: "F = {(v1, v2) ∈ edges G. ¬ P (v1, v2)}" by auto

    from configured_SecurityInvariant.valid_c_offending_flows[OF m] have "c_offending_flows m G =
          {F. F ⊆ edges G ∧ ¬ c_sinvar m G ∧ c_sinvar m (delete_edges G F) ∧ 
              (∀(e1, e2)∈F. ¬ c_sinvar m (add_edge e1 e2 (delete_edges G F)))}" .

    from this unique have "¬ c_sinvar m G" and 2: "c_sinvar m (delete_edges G F)" and 
                          3: "(∀(e1, e2)∈F. ¬ c_sinvar m (add_edge e1 e2 (delete_edges G F)))" by auto

    from this ‹F = {e ∈ edges G. ¬ P e}› have x3: "∀ e ∈ edges G - F. P e" by (metis (lifting) mem_Collect_eq set_diff_eq)
    hence 4: "∀(v1,v2) ∈ edges G - F. P (v1, v2)" by blast

    have "F ≠ {}" by (metis assms(1) assms(2) configured_SecurityInvariant.empty_offending_contra insertCI)
    from this ‹F = {e ∈ edges G. ¬ P e}› ‹¬ c_sinvar m G› have 5: "c_sinvar m G = (∀(v1,v2) ∈ edges G. P (v1, v2))"
      apply(simp add: graph_ops)
      by(blast)

    from EX[of P] unique 1 x3 5 show ?thesis by fast
  qed

  lemma enf_offending_flows:
    assumes vm: "configured_SecurityInvariant m" and enf: "∀G. c_sinvar m G = (∀e ∈ edges G. P e)"
    shows "∀G. c_offending_flows m G = (if c_sinvar m G then {} else {{e ∈ edges G. ¬ P e}})"
    proof -
      { fix G
        from vm configured_SecurityInvariant.valid_c_offending_flows have offending_formaldef:
          "c_offending_flows m G =
            {F. F ⊆ edges G ∧ ¬ c_sinvar m G ∧ c_sinvar m (delete_edges G F) ∧
                (∀(e1, e2)∈F. ¬ c_sinvar m (add_edge e1 e2 (delete_edges G F)))}" by auto
        have "c_offending_flows m G = (if c_sinvar m G then {} else {{e ∈ edges G. ¬ P e}})"
          proof(cases "c_sinvar m G")
          case True thus ?thesis ― ‹@{term "{}"}›
            by(simp add: offending_formaldef)
          next
          case False thus ?thesis by(auto simp add: offending_formaldef graph_ops enf)
        qed
      } thus ?thesis by simp
    qed
      
      
lemma enf_not_fulfilled_if_in_offending:
  assumes validRs: "valid_reqs M"
    and   wfG:     "wf_graph G"
    and   enf:     "∀m ∈ set M. ∃P. ∀G. c_sinvar m G = (∀e ∈ edges G. P e)"
    shows "∀x ∈ (⋃m∈set M. ⋃(c_offending_flows m (fully_connected G))).
                ¬ all_security_requirements_fulfilled M ⦇ nodes = V, edges = insert x E⦈"
   unfolding all_security_requirements_fulfilled_def
   proof(simp, clarify, rename_tac m F a b)
     let ?G="(fully_connected G)"
     fix m F v1 v2
     assume "m ∈ set M" and "F ∈ c_offending_flows m ?G" and "(v1, v2) ∈ F"
       
    from validRs have valid_mD:"⋀m. m ∈ set M ⟹ configured_SecurityInvariant m " 
      by(simp add: valid_reqs_def)
    
     from ‹m ∈ set M› valid_mD have "configured_SecurityInvariant m" by simp

     from enf ‹m ∈ set M› obtain P where enf_m: "∀G. c_sinvar m G = (∀e∈edges G. P e)" by blast
     
     from ‹(v1, v2) ∈ F› have "F ≠ {}" by auto

     from enf_offending_flows[OF ‹configured_SecurityInvariant m› ‹∀G. c_sinvar m G = (∀e∈edges G. P e)›] have
      offending: "⋀G. c_offending_flows m G = (if c_sinvar m G then {} else {{e ∈ edges G. ¬ P e}})" by simp
     from ‹F ∈ c_offending_flows m ?G› ‹F ≠ {}› have "F = {e ∈ edges ?G. ¬ P e}"
       by(simp split: if_split_asm add: offending)
     from this ‹(v1, v2) ∈ F›  have "¬ P (v1, v2)" by simp

     from this enf_m have "¬ c_sinvar m ⦇nodes = V, edges = insert (v1, v2) E⦈" by(simp)
     thus "∃m∈set M. ¬ c_sinvar m ⦇nodes = V, edges = insert (v1, v2) E⦈" using ‹m ∈ set M›
      apply(rule_tac x="m" in bexI)
       by simp_all
qed
        

 theorem generate_valid_topology_max_topo: "⟦ valid_reqs M; wf_graph G;
      ∀m ∈ set M. ∃P. ∀G. c_sinvar m G = (∀e ∈ edges G. P e)⟧ ⟹ 
      max_topo M (generate_valid_topology M (fully_connected G))"
  proof -
    let ?G="(fully_connected G)"
    assume validRs: "valid_reqs M"
    and    wfG:       "wf_graph G"
    and enf: "∀m ∈ set M. ∃P. ∀G. c_sinvar m G = (∀e ∈ edges G. P e)"

    obtain V E where VE_prop: "⦇ nodes = V, edges = E ⦈ = generate_valid_topology M ?G" by (metis graph.cases)
    hence VE_prop_asset:
      "⦇ nodes = V, edges = E ⦈ = ⦇ nodes = V, edges = V × V - (⋃m∈set M. ⋃(c_offending_flows m ?G))⦈"
      by(simp add: fully_connected_def generate_valid_topology_as_set delete_edges_simp2)

    from VE_prop_asset have E_prop: "E =  V × V - (⋃m∈set M. ⋃(c_offending_flows m ?G))" by fast
    from VE_prop have V_prop: "nodes G = V"
      by (simp add: fully_connected_def delete_edges_simp2 generate_valid_topology_def_alt)
    from VE_prop have V_full_prop: "nodes (generate_valid_topology M ?G) = V" by (metis graph.select_convs(1))
    from VE_prop have E_full_prop: "edges (generate_valid_topology M ?G) = E" by (metis graph.select_convs(2))

    from VE_prop wf_graph_generate_valid_topology[OF fully_connected_wf[OF wfG]]
    have wfG_VE: "wf_graph ⦇ nodes = V, edges = E ⦈" by force

    from generate_valid_topology_sound[OF validRs wfG_VE] fully_connected_wf[OF wfG] have VE_all_valid: 
      "all_security_requirements_fulfilled M ⦇ nodes = V, edges = V × V - (⋃m∈set M. ⋃(c_offending_flows m ?G))⦈"
      by (metis VE_prop VE_prop_asset fully_connected_def generate_valid_topology_sound validRs)
    hence goal1: "all_security_requirements_fulfilled M (generate_valid_topology M (fully_connected G))" by (metis VE_prop VE_prop_asset)

    from validRs have valid_mD:"⋀m. m ∈ set M ⟹ configured_SecurityInvariant m " 
      by(simp add: valid_reqs_def)

    from c_offending_flows_subseteq_edges[where G="?G"] validRs have hlp1: "(⋃m∈set M. ⋃(c_offending_flows m ?G)) ⊆ V × V"
      apply(simp add: fully_connected_def V_prop)
      using valid_reqs_def by blast
    have "⋀A B. A - (A - B) = B ∩ A" by fast 
    from E_prop hlp1 have "V × V - E = (⋃m∈set M. ⋃(c_offending_flows m ?G))" by force


    from enf_not_fulfilled_if_in_offending[OF validRs wfG enf]
    have "∀(v1, v2) ∈ (⋃m∈set M. ⋃(c_offending_flows m ?G)).
       ¬ all_security_requirements_fulfilled M ⦇ nodes = V, edges = E ∪ {(v1, v2)}⦈" by simp
          
    from this ‹V × V - E = (⋃m∈set M. ⋃(c_offending_flows m ?G))› have "∀(v1, v2) ∈ V × V - E.
         ¬ all_security_requirements_fulfilled M ⦇ nodes = V, edges = E ∪ {(v1, v2)}⦈" by simp
    hence goal2: "(∀(v1, v2)∈nodes (generate_valid_topology M ?G) × nodes (generate_valid_topology M ?G) -
                edges (generate_valid_topology M ?G).
        ¬ all_security_requirements_fulfilled M (add_edge v1 v2 (generate_valid_topology M ?G)))"
    proof(unfold V_full_prop E_full_prop graph_ops)
      assume a: "∀(v1, v2)∈V × V - E. ¬ all_security_requirements_fulfilled M ⦇nodes = V, edges = E ∪ {(v1, v2)}⦈"
      have "∀(v1, v2)∈V × V - E.  V ∪ {v1, v2} = V" by blast
      hence "∀(v1, v2)∈V × V - E. ⦇nodes = V ∪ {v1, v2}, edges = {(v1, v2)} ∪ E⦈ = ⦇nodes = V, edges = E ∪ {(v1, v2)}⦈" by blast
      from this a show "∀(v1, v2)∈V × V - E. ¬ all_security_requirements_fulfilled M ⦇nodes = V ∪ {v1, v2}, edges = {(v1, v2)} ∪ E⦈"
        ― ‹TODO: this should be trivial ...›
        apply(simp)
        apply(rule ballI)
        apply(erule_tac x=x and A="V × V - E" in ballE)
         prefer 2 apply(simp; fail)
        apply(erule_tac x=x and A="V × V - E" in ballE)
         prefer 2 apply(simp; fail)
        apply(clarify)
        by presburger
    qed
     
    from goal1 goal2 show ?thesis
      unfolding max_topo_def by presburger
  qed

  lemma enf_all_valid_policy_subset_of_max:
    assumes validRs: "valid_reqs M"
    and     wfG:     "wf_graph G"
    and     enf:     "∀m ∈ set M. ∃P. ∀G. c_sinvar m G = (∀e ∈ edges G. P e)"
    and     nodesG': "nodes G = nodes G'"
    shows "⟦ wf_graph G';
        all_security_requirements_fulfilled M G'⟧ ⟹ 
        edges G' ⊆ edges (generate_valid_topology M (fully_connected G))"
    using nodesG' apply(cases "generate_valid_topology M (fully_connected G)", rename_tac V E, simp)
    apply(cases "G'", rename_tac V' E', simp)
    apply(subgoal_tac "nodes G = V")
     prefer 2
     apply (metis fully_connected_def generate_valid_topology_nodes graph.select_convs(1))
    apply(simp)
  proof(rule ccontr)
    fix V E V' E'
    assume a5: "all_security_requirements_fulfilled M ⦇nodes = V, edges = E'⦈" and
           a6: "generate_valid_topology M (fully_connected G) = ⦇nodes = V, edges = E⦈" and
           a10: "wf_graph ⦇nodes = V, edges = E'⦈" and
           contr: "¬ E' ⊆ E"
    
    from wfG a6 have "wf_graph ⦇nodes = V, edges = E⦈"
      by (metis fully_connected_wf wf_graph_generate_valid_topology)
    with a10 have EE'subsets: "fst ` E ⊆ V ∧ snd ` E ⊆ V ∧ fst ` E' ⊆ V ∧ snd ` E' ⊆ V"
      by(simp add: wf_graph_def)
    hence EE'subsets': "E ⊆ V × V ∧ E' ⊆ V × V" by auto
    
    from generate_valid_topology_max_topo[OF validRs wfG enf]
      have m1: "all_security_requirements_fulfilled M ⦇nodes = V, edges = E⦈" and
           m2: "(∀x∈V × V - E. case x of (v1, v2) ⇒ ¬ all_security_requirements_fulfilled M (add_edge v1 v2 ⦇nodes = V, edges = E⦈))"
      by(simp add: max_topo_def a6)+
        
    from m2 have m2': "∀x∈V × V - E. ¬ all_security_requirements_fulfilled M ⦇nodes = V, edges = insert x E⦈"
      apply(simp add: add_edge_def)
      apply(rule ballI, rename_tac x)
      apply(erule_tac x=x in ballE, simp_all)
      apply(case_tac x, simp)
      by (simp add: insert_absorb)
    
     show False
       proof(cases "V = {}")
         case True
         with EE'subsets a10 have "E = {}" and "E' = {}"
           by(simp add: wf_graph_def)+
         with True contr show ?thesis by simp
       next
         case False
         with EE'subsets' contr obtain x where x: "x ∈ E' ∧ x ∉ E ∧ x ∈ V × V"
           by blast
         from m2' x have "¬ all_security_requirements_fulfilled M ⦇nodes = V, edges = insert x E⦈"
           by (simp)
         
         from a6 x have x_offedning: "x ∈ (⋃m∈set M. ⋃(c_offending_flows m (fully_connected G)))"
           apply(simp add: generate_valid_topology_as_set delete_edges_simp2 fully_connected_def)
           by blast
  
         from enf_not_fulfilled_if_in_offending[OF validRs wfG enf] x_offedning have
           1: "¬ all_security_requirements_fulfilled M ⦇nodes = V, edges = insert x myE⦈" for myE by blast
         
         from x have insertxE': "insert x E' = E'" by blast
         with a5 have
           "all_security_requirements_fulfilled M ⦇nodes = V, edges = insert x E'⦈" by simp
         with insertxE' all_security_requirements_fulfilled_mono[OF validRs _ a10 a5] have 
           2: "all_security_requirements_fulfilled M ⦇nodes = V, edges = insert x {}⦈" by blast
         from 1 2 show ?thesis by blast
       qed
  qed
    


   subsection‹More Lemmata›
     lemma (in configured_SecurityInvariant) c_sinvar_valid_imp_no_offending_flows: 
      "c_sinvar m G ⟹ c_offending_flows m G = {}"
        by(simp add: valid_c_offending_flows)

     lemma all_security_requirements_fulfilled_imp_no_offending_flows:
        "valid_reqs M ⟹ all_security_requirements_fulfilled M G ⟹ (⋃m∈set M. ⋃(c_offending_flows m G)) = {}"
        proof(induction M)
        case Cons thus ?case
          unfolding all_security_requirements_fulfilled_def
          apply(simp)
          by(blast dest: valid_reqs2 valid_reqs1 configured_SecurityInvariant.c_sinvar_valid_imp_no_offending_flows)
        qed(simp)

    corollary all_security_requirements_fulfilled_imp_get_offending_empty:
      "valid_reqs M ⟹ all_security_requirements_fulfilled M G ⟹ get_offending_flows M G = {}"
      apply(frule(1) all_security_requirements_fulfilled_imp_no_offending_flows)
      apply(simp add: get_offending_flows_def)
      apply(thin_tac "all_security_requirements_fulfilled M G")
      apply(simp add: valid_reqs_def)
      apply(clarify)
      using configured_SecurityInvariant.empty_offending_contra by fastforce
  
    corollary generate_valid_topology_does_nothing_if_valid:
      "⟦ valid_reqs M; all_security_requirements_fulfilled M G⟧ ⟹ 
          generate_valid_topology M G = G"
      by(simp add: generate_valid_topology_as_set graph_ops all_security_requirements_fulfilled_imp_no_offending_flows)


    lemma mono_extend_get_offending_flows: "⟦ valid_reqs M;
         wf_graph ⦇nodes = V, edges = E⦈;
         E' ⊆ E;
         F' ∈ get_offending_flows M ⦇nodes = V, edges = E'⦈ ⟧ ⟹
       ∃F∈get_offending_flows M ⦇nodes = V, edges = E⦈. F' ⊆ F"
     proof(induction M)
     case Nil thus ?case by(simp add: get_offending_flows_def)
     next
     case (Cons m M)
      from Cons.prems have "configured_SecurityInvariant m"
                       and "valid_reqs M" using valid_reqs2 valid_reqs1 by blast+
      from Cons.prems(4) have
        "F' ∈ c_offending_flows m ⦇nodes = V, edges = E'⦈ ∨
         (F' ∈ get_offending_flows M ⦇nodes = V, edges = E'⦈)"
       by(simp add: get_offending_flows_def)
      from this show ?case
       proof(elim disjE, goal_cases)
       case 1
         with ‹configured_SecurityInvariant m› Cons.prems(2,3,4) obtain F where
           "F∈c_offending_flows m ⦇nodes = V, edges = E⦈" and "F' ⊆ F"
           by(blast dest: configured_SecurityInvariant.mono_extend_set_offending_flows)
         hence "F∈get_offending_flows (m # M) ⦇nodes = V, edges = E⦈"
           by (simp add: get_offending_flows_def)
         with ‹F' ⊆ F› show ?case by blast
       next
       case 2 with Cons ‹valid_reqs M› show ?case by(simp add: get_offending_flows_def) blast
       qed
     qed

     lemma get_offending_flows_subseteq_edges: "valid_reqs M ⟹ F ∈ get_offending_flows M ⦇nodes = V, edges = E⦈ ⟹ F ⊆ E"
      apply(induction M)
       apply(simp add: get_offending_flows_def)
      apply(simp add: get_offending_flows_def)
      apply(frule valid_reqs2, drule valid_reqs1)
      apply(simp add: configured_SecurityInvariant.valid_c_offending_flows)
      by blast

    thm configured_SecurityInvariant.offending_flows_union_mono
    lemma get_offending_flows_union_mono: "⟦valid_reqs M; 
      wf_graph ⦇nodes = V, edges = E⦈; E' ⊆ E ⟧ ⟹
      ⋃(get_offending_flows M ⦇nodes = V, edges = E'⦈) ⊆ ⋃(get_offending_flows M ⦇nodes = V, edges = E⦈)"
      apply(induction M)
       apply(simp add: get_offending_flows_def)
      apply(frule valid_reqs2, drule valid_reqs1)
      apply(drule(2) configured_SecurityInvariant.offending_flows_union_mono)
      apply(simp add: get_offending_flows_def)
      by auto

    thm configured_SecurityInvariant.Un_set_offending_flows_bound_minus_subseteq'
    lemma Un_set_offending_flows_bound_minus_subseteq':"⟦valid_reqs M; 
      wf_graph ⦇nodes = V, edges = E⦈; E' ⊆ E;
      ⋃(get_offending_flows M ⦇nodes = V, edges = E⦈) ⊆ X ⟧ ⟹ ⋃(get_offending_flows M ⦇nodes = V, edges = E - E'⦈) ⊆ X - E'"
      proof(induction M)
      case Nil thus ?case by (simp add: get_offending_flows_def)
      next
      case (Cons m M)
        from Cons.prems(1) valid_reqs2 have "valid_reqs M" by force
        from Cons.prems(1) valid_reqs1 have "configured_SecurityInvariant m" by force
        from Cons.prems(4) have "⋃(get_offending_flows M ⦇nodes = V, edges = E⦈) ⊆ X" by(simp add: get_offending_flows_def)
        from Cons.IH[OF ‹valid_reqs M› Cons.prems(2) Cons.prems(3) ‹⋃(get_offending_flows M ⦇nodes = V, edges = E⦈) ⊆ X›] have IH: "⋃(get_offending_flows M ⦇nodes = V, edges = E - E'⦈) ⊆ X - E'" .
        from Cons.prems(4) have "⋃(c_offending_flows m ⦇nodes = V, edges = E⦈) ⊆ X" by(simp add: get_offending_flows_def)
        from configured_SecurityInvariant.Un_set_offending_flows_bound_minus_subseteq'[OF ‹configured_SecurityInvariant m› Cons.prems(2) ‹⋃(c_offending_flows m ⦇nodes = V, edges = E⦈) ⊆ X›] have "⋃(c_offending_flows m ⦇nodes = V, edges = E - E'⦈) ⊆ X - E'" .
        from this IH show ?case by(simp add: get_offending_flows_def)
      qed

 


 (*ENF has uniquely defined offending flows*)
 lemma ENF_uniquely_defined_offedning: "valid_reqs M ⟹ wf_graph G ⟹ 
      ∀m ∈ set M. ∃P. ∀G. c_sinvar m G = (∀e ∈ edges G. P e) ⟹ 
      ∀m ∈ set M. ∀G. ¬ c_sinvar m G ⟶  (∃OFF. c_offending_flows m G = {OFF})"
 apply -
 apply(induction M)
  apply(simp; fail)
 apply(rename_tac m M)
 apply(frule valid_reqs1)
 apply(drule valid_reqs2)
 apply(simp)
 apply(elim conjE)
 apply(erule_tac x=m in ballE)
  apply(simp_all; fail)
 apply(erule exE, rename_tac P)
 apply(drule_tac P=P in enf_offending_flows)
  apply(simp; fail)
 apply(simp; fail)
 done

 lemma assumes "configured_SecurityInvariant m"
       and "∀G. ¬ c_sinvar m G ⟶ (∃OFF. c_offending_flows m G = {OFF})"
       shows "∃OFF_P. ∀G. c_offending_flows m G = (if c_sinvar m G then {} else {OFF_P G})"
 proof -
   from assms have "∃OFF_P. 
          c_offending_flows m G = (if c_sinvar m G then {} else {OFF_P G})" for G
     apply(erule_tac x=G in allE)
     apply(cases "c_sinvar m G")
      apply(drule configured_SecurityInvariant.c_sinvar_valid_imp_no_offending_flows, simp)
      apply(simp; fail)
     apply(simp)
     by meson
   with assms show ?thesis by metis
 qed
 (*TODO: generate_valid_topology_max_topo for sinvars with unique offending flows in general*)



   text‹Hilber's eps operator example›
   lemma "(SOME x. x : {1::nat, 2, 3}) = x ⟹ x = 1 ∨ x = 2 ∨ x = 3"
     proof -
      have "(SOME x. x ∈ {1::nat, 2, 3}) ∈ {1::nat, 2, 3}" unfolding some_in_eq by simp
      thus "(SOME x. x : {1::nat, 2, 3}) = x ⟹ x = 1 ∨ x = 2 ∨ x = 3" by fast
     qed

  (*TODO: remove the offending flows from the graph for each iteration. requires proof arbitrary: G
          allows to put expensive invariants at back of list and hope that sinvar is true until the are evaluated*)
  text‹Only removing one offending flow should be enough›
  fun generate_valid_topology_SOME :: "'v SecurityInvariant_configured list ⇒ 'v graph ⇒ 'v graph" where
    "generate_valid_topology_SOME [] G = G" |
    "generate_valid_topology_SOME (m#Ms) G = (if c_sinvar m G
      then generate_valid_topology_SOME Ms G
      else delete_edges (generate_valid_topology_SOME Ms G) (SOME F. F ∈ c_offending_flows m G)
      )"

  lemma generate_valid_topology_SOME_nodes: "nodes (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) = V"
    proof(induction M)
    qed(simp_all add: delete_edges_simp2)

  theorem generate_valid_topology_SOME_sound:
    "⟦ valid_reqs M; wf_graph ⦇nodes = V, edges = E⦈ ⟧ ⟹ 
    all_security_requirements_fulfilled M (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)"
      proof(induction M)
        case Nil
        thus ?case by(simp add: all_security_requirements_fulfilled_def)
      next
        case (Cons m M)
        from valid_reqs1[OF Cons(2)] have validReq: "configured_SecurityInvariant m" .
        
        from configured_SecurityInvariant.sinvar_valid_remove_SOME_offending_flows[OF validReq] have
         "c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {} ⟹
           c_sinvar m ⦇nodes = V, edges = E - (SOME F. F ∈ c_offending_flows m ⦇nodes = V, edges = E⦈)⦈" .

        have generate_valid_topology_SOME_edges: "edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) ⊆ E"
          for M::"'a SecurityInvariant_configured list" and V E
          proof(induction M)
          qed(auto simp add: delete_edges_simp2)

        from configured_SecurityInvariant.mono_sinvar[OF validReq Cons.prems(2),
              of "edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)"]
            generate_valid_topology_SOME_edges
          have "c_sinvar m ⦇nodes = V, edges = E⦈ ⟹
            c_sinvar m ⦇nodes = V, edges = edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)⦈"
          by simp
        moreover from configured_SecurityInvariant.defined_offending'[OF validReq Cons.prems(2)] have not_sinvar_off:
          "¬ c_sinvar m ⦇nodes = V, edges = E⦈ ⟹ c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {}" by blast
        ultimately have goal_sinvar_m:
          "c_offending_flows m ⦇nodes = V, edges = E⦈ = {} ⟹ 
              c_sinvar m (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)"
           using generate_valid_topology_SOME_nodes 
           by (metis graph.select_convs(1) graph.select_convs(2) graph_eq_intro)

        from valid_reqs2[OF Cons(2)] have "valid_reqs M" .
        from Cons.IH[OF ‹valid_reqs M› Cons(3)] have IH:
          "all_security_requirements_fulfilled M (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)" .

        have goal_rm_SOME_m: "c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {} ⟹
            c_sinvar m (delete_edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)
                                      (SOME F. F ∈ c_offending_flows m ⦇nodes = V, edges = E⦈))"
        proof - (*sledgehammered*)
          assume a1: "c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {}"
          have f2: "(∀r ra p. ¬ r ⊆ ra ∨ (p::'a × 'a) ∉ r ∨ p ∈ ra) = (∀r ra p. ¬ r ⊆ ra ∨ (p::'a × 'a) ∉ r ∨ p ∈ ra)"
            by meson
          have f3: "wf_graph ⦇nodes = V, edges = E - (SOME r. r ∈ c_offending_flows m ⦇nodes = V, edges = E⦈)⦈"
            by (simp add: Cons.prems(2) wf_graph_remove_edges)
          have "edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) - (SOME r. r ∈ c_offending_flows m ⦇nodes = V, edges = E⦈) ⊆ E - (SOME r. r ∈ c_offending_flows m ⦇nodes = V, edges = E⦈)"
            using f2 generate_valid_topology_SOME_edges[of M V E] by blast
          then have "c_sinvar m ⦇nodes = V, edges = edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) - (SOME r. r ∈ c_offending_flows m ⦇nodes = V, edges = E⦈)⦈"
            using f3 a1 ‹c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {} ⟹ c_sinvar m ⦇nodes = V, edges = E - (SOME F. F ∈ c_offending_flows m ⦇nodes = V, edges = E⦈)⦈› configured_SecurityInvariant.negative_mono validReq by blast
          then show "c_sinvar m (delete_edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) (SOME r. r ∈ c_offending_flows m ⦇nodes = V, edges = E⦈))"
            by (simp add: generate_valid_topology_SOME_nodes graph_ops(5))
        qed

        have wf_graph_generate_valid_topology_SOME: "wf_graph G ⟹ wf_graph (generate_valid_topology_SOME M G)"
          for G (*TODO: tune*)
          apply(cases G)
          apply(simp add: wf_graph_def generate_valid_topology_SOME_nodes)
          using generate_valid_topology_SOME_edges by (meson dual_order.trans image_mono rev_finite_subset) 

        { assume notempty: "c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {}"
          hence "∃ hypE. (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = hypE⦈"
            proof(induction M arbitrary: V E)
            qed(simp_all add: delete_edges_simp2 generate_valid_topology_SOME_nodes)
          from this obtain E_IH where E_IH_prop:
            "(generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = E_IH⦈" by blast
    
          from wf_graph_generate_valid_topology_SOME[OF Cons(3)] E_IH_prop
          have valid_G_E_IH: "wf_graph ⦇nodes = V, edges = E_IH⦈" by simp
    
          from all_security_requirements_fulfilled_mono[OF ‹valid_reqs M› _ valid_G_E_IH ] IH E_IH_prop
          have mono_rule: "E' ⊆ E_IH ⟹ all_security_requirements_fulfilled M ⦇nodes = V, edges = E'⦈" for E' by simp
  
          have "all_security_requirements_fulfilled M
            (delete_edges (generate_valid_topology_SOME M ⦇nodes = V, edges = E⦈)
                          (SOME F. F ∈ c_offending_flows m ⦇nodes = V, edges = E⦈))"
            unfolding E_IH_prop by(auto simp add: delete_edges_simp2 intro:mono_rule)
        } note goal_fulfilled_M=this

        have no_offending: "c_sinvar m ⦇nodes = V, edges = E⦈ ⟹ c_offending_flows m ⦇nodes = V, edges = E⦈ = {}"
          by (simp add: configured_SecurityInvariant.c_sinvar_valid_imp_no_offending_flows validReq)

        show "all_security_requirements_fulfilled (m # M) (generate_valid_topology_SOME (m # M) ⦇nodes = V, edges = E⦈)"
        apply(simp add: all_security_requirements_fulfilled_def)
        apply(intro conjI impI)
           subgoal using goal_sinvar_m no_offending by blast
          subgoal using IH by(simp add: all_security_requirements_fulfilled_def; fail)
         subgoal using goal_rm_SOME_m not_sinvar_off by blast 
        subgoal using goal_fulfilled_M not_sinvar_off by(simp add: all_security_requirements_fulfilled_def)
        done
     qed

    
   lemma generate_valid_topology_SOME_def_alt:
      "generate_valid_topology_SOME M G = delete_edges G (⋃m ∈ set M. if c_sinvar m G then {} else (SOME F. F ∈ c_offending_flows m G))"
      proof(induction M arbitrary: G)
        case Nil
          thus ?case by(simp add: get_offending_flows_def)
        next
        case (Cons m M)
          from Cons[simplified delete_edges_simp2 get_offending_flows_def] 
          have IH :"edges (generate_valid_topology_SOME M G) =
                   edges G - (⋃m∈set M. if c_sinvar m G then {} else SOME F. F ∈ c_offending_flows m G)"
            by simp
          hence "¬ c_sinvar m G ⟹ 
                    edges (generate_valid_topology_SOME (m # M) G) =
                    (edges G) - (⋃m∈set (m#M). if c_sinvar m G then {} else SOME F. F ∈ c_offending_flows m G)"
            apply(simp add: get_offending_flows_def delete_edges_simp2)
            by blast
          with Cons.IH show ?case by(simp add: get_offending_flows_def delete_edges_simp2)
      qed

    lemma generate_valid_topology_SOME_superset:
      "⟦ valid_reqs M; wf_graph G ⟧ ⟹ 
      edges (generate_valid_topology M G) ⊆ edges (generate_valid_topology_SOME M G)"
    proof -
      have isabelle2016_1_helper:
        "x ∈ (⋃m∈set M. if c_sinvar m G then {} else SOME F. F ∈ c_offending_flows m G) ⟷
          (∃m∈set M. ¬ c_sinvar m G ∧ (c_sinvar m G ∨ x ∈ (SOME F. F ∈ c_offending_flows m G)))"
        for x by auto
      have 1: "m∈set M ⟹ ¬ c_sinvar m G ∧ (c_sinvar m G ∨ x ∈ (SOME F. F ∈ c_offending_flows m G)) ⟹
            c_offending_flows m G ≠ {} ⟹
            x ∈ ⋃(⋃m∈set M. c_offending_flows m G)"
      for x m
      apply(simp)
      apply(rule_tac x=m in bexI)
      apply(simp_all)
       using some_in_eq by blast
     
      show "valid_reqs M ⟹ wf_graph G ⟹ ?thesis"
      unfolding generate_valid_topology_SOME_def_alt generate_valid_topology_def_alt
      apply (rule delete_edges_edges_mono)
      apply (auto simp add: delete_edges_simp2 get_offending_flows_def valid_reqs_def)
      apply (metis (full_types) configured_SecurityInvariant.defined_offending' some_in_eq)
      done
    qed




  text‹Notation:
    @{const generate_valid_topology_SOME}: non-deterministic choice
    ‹generate_valid_topology_some›: executable which selects always the same
›
  fun generate_valid_topology_some :: "'v SecurityInvariant_configured list ⇒ ('v×'v) list ⇒ 'v graph ⇒ 'v graph" where
    "generate_valid_topology_some [] _ G = G" |
    "generate_valid_topology_some (m#Ms) Es G = (if c_sinvar m G
      then generate_valid_topology_some Ms Es G
      else delete_edges (generate_valid_topology_some Ms Es G) (set (minimalize_offending_overapprox (c_sinvar m) Es [] G))
      )"
  theorem generate_valid_topology_some_sound:
    "⟦ valid_reqs M; wf_graph ⦇nodes = V, edges = E⦈; set Es = E; distinct Es ⟧ ⟹ 
    all_security_requirements_fulfilled M (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)"
      proof(induction M)
        case Nil
        thus ?case by(simp add: all_security_requirements_fulfilled_def)
      next
        case (Cons m M)
        from valid_reqs1[OF Cons(2)] have validReq: "configured_SecurityInvariant m" .
         
        from configured_SecurityInvariant.sinvar_valid_remove_minimalize_offending_overapprox[OF
          validReq Cons.prems(2) _  Cons.prems(3) Cons.prems(4)] have rm_off_valid:
         "¬ c_sinvar m ⦇nodes = V, edges = E⦈⟹
           c_sinvar m ⦇nodes = V, edges = E - (set (minimalize_offending_overapprox (c_sinvar m) Es [] ⦇nodes = V, edges = E⦈))⦈"
        apply(subst(asm) minimalize_offending_overapprox_boundnP[symmetric]) (*TODO: type for nP unspecified!*)
        by blast

        have generate_valid_topology_some_nodes: "nodes (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈) = V"
          for M::"'a SecurityInvariant_configured list" and V E
          proof(induction M)
          qed(simp_all add: delete_edges_simp2)


        have generate_valid_topology_some_edges: "edges (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈) ⊆ E"
          for M::"'a SecurityInvariant_configured list" and V E
          proof(induction M)
          qed(auto simp add: delete_edges_simp2)
        
        from configured_SecurityInvariant.mono_sinvar[OF validReq Cons.prems(2),
              of "edges (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)"]
            generate_valid_topology_some_edges
          have "c_sinvar m ⦇nodes = V, edges = E⦈ ⟹
            c_sinvar m ⦇nodes = V, edges = edges (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)⦈"
          by simp
        moreover from configured_SecurityInvariant.defined_offending'[OF validReq Cons.prems(2)] have not_sinvar_off:
          "¬ c_sinvar m ⦇nodes = V, edges = E⦈ ⟹ c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {}" by blast
        ultimately have goal_sinvar_m:
          "c_offending_flows m ⦇nodes = V, edges = E⦈ = {} ⟹ 
              c_sinvar m (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)"
           using generate_valid_topology_some_nodes 
           by (metis graph.select_convs(1) graph.select_convs(2) graph_eq_intro)

  
        from valid_reqs2[OF Cons(2)] have "valid_reqs M" .
        from Cons.IH[OF ‹valid_reqs M› Cons(3)] Cons.prems have IH:
          "all_security_requirements_fulfilled M (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)" by simp

 


        have wf_graph_generate_valid_topology_some: "wf_graph G ⟹ wf_graph (generate_valid_topology_some M Es G)"
          for G (*TODO: tune*)
          apply(cases G)
          apply(simp add: wf_graph_def generate_valid_topology_some_nodes)
          using generate_valid_topology_some_edges by (meson dual_order.trans image_mono rev_finite_subset) 

        
        { assume notempty: "c_offending_flows m ⦇nodes = V, edges = E⦈ ≠ {}"
          hence "∃ hypE. (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = hypE⦈"
            proof(induction M arbitrary: V E)
            qed(simp_all add: delete_edges_simp2 generate_valid_topology_some_nodes)
          from this obtain E_IH where E_IH_prop:
            "(generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈) = ⦇nodes = V, edges = E_IH⦈" by blast
    
          from wf_graph_generate_valid_topology_some[OF Cons(3)] E_IH_prop
          have valid_G_E_IH: "wf_graph ⦇nodes = V, edges = E_IH⦈" by simp
    
          from all_security_requirements_fulfilled_mono[OF ‹valid_reqs M› _ valid_G_E_IH ] IH E_IH_prop
          have mono_rule: "E' ⊆ E_IH ⟹ all_security_requirements_fulfilled M ⦇nodes = V, edges = E'⦈" for E' by simp
  
          have "all_security_requirements_fulfilled M
            (delete_edges (generate_valid_topology_some M Es ⦇nodes = V, edges = E⦈)
                          (set (minimalize_offending_overapprox (c_sinvar m) Es [] ⦇nodes = V, edges = E⦈)))"
            unfolding E_IH_prop by(auto simp add: delete_edges_simp2 intro:mono_rule)
        } note goal_fulfilled_M=this

        have no_offending: "c_sinvar m ⦇nodes = V, edges = E⦈ ⟹ c_offending_flows m ⦇nodes = V, edges = E⦈ = {}"
          by (simp add: configured_SecurityInvariant.c_sinvar_valid_imp_no_offending_flows validReq)

        show "all_security_requirements_fulfilled (m # M) (generate_valid_topology_some (m # M) Es ⦇nodes = V, edges = E⦈)"
        apply(simp add: all_security_requirements_fulfilled_def)
        apply(intro conjI impI)
           subgoal using goal_sinvar_m no_offending by blast
          subgoal using IH by(simp add: all_security_requirements_fulfilled_def; fail)
         subgoal using rm_off_valid by (metis (no_types, lifting) Cons.prems(2) Diff_mono 
            configured_SecurityInvariant.mono_sinvar delete_edges_simp2 generate_valid_topology_some_edges
            generate_valid_topology_some_nodes order_refl validReq wf_graph_remove_edges) (*TODO!*)
        subgoal using goal_fulfilled_M not_sinvar_off by(simp add: all_security_requirements_fulfilled_def)
        done
     qed



end