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 ‹∀ (v⇩1, v⇩2) ∈ 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