Theory SINVAR_DomainHierarchyNG

theory SINVAR_DomainHierarchyNG
imports "../TopoS_Helper"
  "HOL-Lattice.CompleteLattice" (* markarius lattice *)
begin


subsection‹SecurityInvariant DomainHierarchyNG›

subsubsection ‹Datatype Domain Hierarchy›

  text‹A fully qualified domain name for an entity in a tree-like hierarchy›
    datatype domainNameDept =  Dept "string" domainNameDept (infixr ‹--› 65) |
                               Leaf ― ‹leaf of the tree, end of all domainNames›
    
    text ‹Example: the CoffeeMachine of I8›
    value "''i8''--''CoffeeMachine''--Leaf"

  text‹A tree strucuture to represent the general hierarchy, i.e. possible domainNameDepts›
    datatype domainTree = Department 
        "string"  ― ‹division›
        "domainTree list"  ― ‹sub divisions›

  text‹one step in tree to find matching department›
    fun hierarchy_next :: "domainTree list ⇒ domainNameDept ⇒ domainTree option" where
      "hierarchy_next [] _ = None" | 
      "hierarchy_next (s#ss) Leaf = None" | 
      "hierarchy_next ((Department d ds)#ss) (Dept n ns) = (if d=n then Some (Department d ds) else hierarchy_next ss (Dept n ns))"

    text ‹Examples:›
    lemma "hierarchy_next [Department ''i20'' [], Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []]] 
        (''i8''--Leaf)
        =
        Some (Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []])" by eval
    lemma "hierarchy_next [Department ''i20'' [], Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []]] 
        (''i8''--''whatsoever''--Leaf)
        =
        Some (Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []])" by eval
    lemma "hierarchy_next [Department ''i20'' [], Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []]] 
        Leaf
        = None" by eval
    lemma "hierarchy_next [Department ''i20'' [], Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []]] 
        (''i0''--Leaf)
        = None" by eval

  text ‹Does a given @{typ domainNameDept} match the specified tree structure?›
    fun valid_hierarchy_pos :: "domainTree ⇒ domainNameDept ⇒ bool" where
      "valid_hierarchy_pos (Department d ds) Leaf = True" |
      "valid_hierarchy_pos (Department d ds) (Dept n Leaf) = (d=n)" |
      "valid_hierarchy_pos (Department d ds) (Dept n ns) = (n=d ∧ 
        (case hierarchy_next ds ns of 
          None ⇒ False |
          Some t ⇒ valid_hierarchy_pos t ns))"


     text ‹Examples:›
     lemma "valid_hierarchy_pos (Department ''TUM'' []) Leaf" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' []) Leaf" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' []) (''TUM''--Leaf)" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' []) (''TUM''--''facilityManagement''--Leaf) = False" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' []) (''LMU''--Leaf) = False" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [], (Department ''i20'' [])])  (''TUM''--Leaf)" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [], Department ''i20'' []])  (''TUM''--''i8''--Leaf)" by eval
     lemma "valid_hierarchy_pos 
        (Department ''TUM'' [
           Department ''i8'' [
            Department ''CoffeeMachine'' [],
            Department ''TeaMachine'' []
           ], 
           Department ''i20'' []
        ]) 
        (''TUM''--''i8''--''CoffeeMachine''--Leaf)" by eval
     lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [Department ''CoffeeMachine'' [], Department ''TeaMachine'' []], Department ''i20'' []]) 
        (''TUM''--''i8''--''CleanKitchen''--Leaf) = False" by eval

     (*end tree*)
     
  
  instantiation domainNameDept :: order
  begin
    print_context
    
    fun less_eq_domainNameDept :: "domainNameDept ⇒ domainNameDept ⇒ bool" where
      "Leaf ≤ (Dept _ _) = False" |
      "(Dept _ _) ≤ Leaf = True" |
      "Leaf ≤ Leaf = True" |
      "(Dept n1 n1s) ≤ (Dept n2 n2s) = (n1=n2 ∧ n1s ≤ n2s)"
    
    fun less_domainNameDept :: "domainNameDept ⇒ domainNameDept ⇒ bool" where
      "Leaf < Leaf = False" |
      "Leaf < (Dept _ _) = False" |
      "(Dept _ _) < Leaf = True" |
      "(Dept n1 n1s) < (Dept n2 n2s) = (n1=n2 ∧ n1s < n2s)"
    
    lemma Leaf_Top: "a ≤ Leaf"
      apply(case_tac a)
      by(simp_all)
  
    lemma Leaf_Top_Unique: "Leaf ≤ a = (a = Leaf)"
      apply(case_tac a)
      by(simp_all)
  
    lemma no_Bot: "n1 ≠ n2 ⟹ z ≤ n1 -- n1s ⟹ z ≤ n2 -- n2s ⟹ False"
      apply(case_tac z)
      by(simp_all)
  
    lemma uncomparable_sup_is_Top: "n1 ≠ n2 ⟹ n1 -- x ≤ z ⟹ n2 -- y ≤ z ⟹ z = Leaf"
      apply(case_tac z)
      by(simp_all)

   lemma common_inf_imp_comparable: "(z::domainNameDept) ≤ a ⟹ z ≤ b ⟹ a ≤ b ∨ b ≤ a"
      apply(induction z arbitrary: a b)
       apply(rename_tac zn zdpt a b)
       apply(simp_all add: Leaf_Top_Unique)
      apply(case_tac a)
       apply(rename_tac an adpt)
       apply(simp_all add: Leaf_Top)
      apply(case_tac b)
       apply(rename_tac bn bdpt)
       apply(simp_all add: Leaf_Top)
      done
  
    lemma prepend_domain: "a ≤ b ⟹ x--a ≤ x--b"
      by(simp)
    lemma unfold_dmain_leq: "y ≤ zn -- zns ⟹ ∃yns. y = zn -- yns ∧ yns ≤ zns"
      proof -
        assume a1: "y ≤ zn -- zns"
        obtain sk⇩3⇩0 :: "domainNameDept ⇒ char list" and sk⇩3⇩1 :: "domainNameDept ⇒ domainNameDept" where "∀x⇩0. sk⇩3⇩0 x⇩0 -- sk⇩3⇩1 x⇩0 = x⇩0 ∨ Leaf = x⇩0"
          by (metis domainNameDept.exhaust)
        thus "∃yns. y = zn -- yns ∧ yns ≤ zns"
          using a1 by (metis less_eq_domainNameDept.simps(1) less_eq_domainNameDept.simps(4))
      qed
  
    lemma less_eq_refl: 
      fixes x :: domainNameDept
      shows "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
      proof -
      have "x ≤ y ⟶ y ≤ z ⟶ x ≤ z" (*induction over prems and conclusion*)
        proof(induction z arbitrary:x y)
        case Leaf
          have "x ≤ Leaf" using Leaf_Top by simp
          thus ?case by simp
        next
        case (Dept zn zns)
          show ?case proof(clarify)
            assume a1: "x ≤ y" and a2: "y ≤ zn--zns"
            from unfold_dmain_leq[OF a2] obtain yns where y1: "y = zn--yns" and y2: "yns ≤ zns" by auto
            from unfold_dmain_leq this a1 obtain xns where x1: "x = zn -- xns" and x2: "xns ≤ yns" by blast
            from Dept y2 x2 have "xns ≤ zns" by simp
            from this x1 show "x ≤ zn--zns" by simp
          qed
        qed
      thus "x ≤ y ⟹ y ≤ z ⟹ x ≤ z" by simp
      qed
  
    instance
      proof
        fix x y ::domainNameDept
        show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
          apply(induction rule: less_domainNameDept.induct)
           apply(simp_all)
          by blast
      next
        fix x::domainNameDept
        show "x ≤ x"
          using[[show_types]] apply(induction x)
          by simp_all
      next
        fix x y z :: domainNameDept
        show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z " apply (rule less_eq_refl) by simp_all
      next
        fix x y ::domainNameDept
        show "x ≤ y ⟹ y ≤ x ⟹ x = y"
          apply(induction rule: less_domainNameDept.induct)
             by(simp_all)
    qed
  end

  instantiation domainNameDept :: Orderings.top
  begin
    definition top_domainNameDept where "Orderings.top ≡ Leaf"
    instance
      by intro_classes
  end

    lemma "(''TUM''--''BLUBB''--Leaf) ≤ (''TUM''--Leaf)" by eval

    lemma "(''TUM''--''i8''--Leaf) ≤ (''TUM''--Leaf)" by eval
    lemma "¬ (''TUM''--Leaf) ≤ (''TUM''--''i8''--Leaf)"  by eval
    lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [], Department ''i20'' []]) (''TUM''--''i8''--Leaf)" by eval
    
    lemma "(''TUM''--Leaf) ≤ Leaf" by eval
    lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [], Department ''i20'' []]) (Leaf)" by eval

    lemma "¬ Leaf ≤ (''TUM''--Leaf)" by eval
    lemma "valid_hierarchy_pos (Department ''TUM'' [Department ''i8'' [], Department ''i20'' []]) (''TUM''--Leaf)" by eval

    lemma "¬ (''TUM''--''BLUBB''--Leaf) ≤ (''X''--''TUM''--''BLUBB''--Leaf)" by eval

    lemma "(''TUM''--''i8''--''CoffeeMachine''--Leaf) ≤ (''TUM''--''i8''--Leaf)" by eval
    lemma "(''TUM''--''i8''--Leaf) ≤ (''TUM''--''i8''--Leaf)" by eval
    lemma "(''TUM''--''i8''--''CoffeeMachine''--Leaf) ≤ (''TUM''--Leaf)" by eval
    lemma "(''TUM''--''i8''--''CoffeeMachine''--Leaf) ≤ (Leaf)" by eval
    lemma "¬ (''TUM''--''i8''--Leaf) ≤ (''TUM''--''i20''--Leaf)" by eval
    lemma "¬ (''TUM''--''i20''--Leaf) ≤ (''TUM''--''i8''--Leaf)" by eval



  subsubsection ‹Adding Chop›
  text‹by putting entities higher in the hierarchy.›
    fun domainNameDeptChopOne :: "domainNameDept ⇒ domainNameDept" where
      "domainNameDeptChopOne Leaf = Leaf" |
      "domainNameDeptChopOne (name--Leaf) = Leaf" |
      "domainNameDeptChopOne (name--dpt) = name--(domainNameDeptChopOne dpt)"
    
    
    lemma "domainNameDeptChopOne (''i8''--''CoffeeMachine''--Leaf) = ''i8'' -- Leaf" by eval
    lemma "domainNameDeptChopOne (''i8''--''CoffeeMachine''--''CoffeeSlave''--Leaf) = ''i8'' -- ''CoffeeMachine'' -- Leaf" by eval
    lemma "domainNameDeptChopOne Leaf = Leaf" by(fact domainNameDeptChopOne.simps(1))
    
    theorem chopOne_not_decrease: "dn ≤ domainNameDeptChopOne dn"
      apply(induction dn)
       apply(rename_tac name dpt)
       apply(drule_tac x="name" in prepend_domain)
       apply(case_tac dpt)
        apply simp_all
    done
    
    lemma chopOneContinue: "dpt ≠ Leaf ⟹ domainNameDeptChopOne (name -- dpt) = name -- domainNameDeptChopOne (dpt)"
    apply(case_tac dpt)
     by simp_all
    
    fun domainNameChop :: "domainNameDept ⇒ nat ⇒ domainNameDept" where
      "domainNameChop Leaf _ = Leaf" |
      "domainNameChop namedpt 0 = namedpt" |
      "domainNameChop namedpt (Suc n) = domainNameChop (domainNameDeptChopOne namedpt) n"
    
    lemma "domainNameChop (''i8''--''CoffeeMachine''--Leaf) 2 = Leaf" by eval
    lemma "domainNameChop (''i8''--''CoffeeMachine''--''CoffeeSlave''--Leaf) 2 = ''i8''--Leaf" by eval
    lemma "domainNameChop (''i8''--Leaf) 0 = ''i8''--Leaf" by eval
    lemma "domainNameChop (Leaf) 8 = Leaf" by eval
    
    
    lemma chop0[simp]: "domainNameChop dn 0 = dn"
     apply(case_tac dn)
      by simp_all
    
    
    lemma "(domainNameDeptChopOne^^2) (''d1''--''d2''--''d3''--Leaf) = ''d1''--Leaf" by eval
    
    text ‹domainNameChop is equal to applying n times chop one›
    lemma domainNameChopFunApply: "domainNameChop dn n = (domainNameDeptChopOne^^n) dn"
      apply(induction dn n rule: domainNameChop.induct)
        apply (simp_all)
      apply(rename_tac nat,induct_tac nat, simp_all)
      apply(rename_tac n)
      by (metis funpow_swap1)
    
    lemma domainNameChopRotateSuc: "domainNameChop dn (Suc n) = domainNameDeptChopOne (domainNameChop dn n)"
    by(simp add: domainNameChopFunApply)
    
    lemma domainNameChopRotate: "domainNameChop (domainNameDeptChopOne dn) n = domainNameDeptChopOne (domainNameChop dn n)"
      apply(subgoal_tac "domainNameChop (domainNameDeptChopOne dn) n = domainNameChop dn (Suc n)")
       apply simp
       apply(simp add: domainNameChopFunApply)
      apply(case_tac dn)
       by(simp_all)
    
    
    theorem chop_not_decrease_hierarchy: "dn ≤ domainNameChop dn n"
      apply(induction n)
       apply(simp)
       apply(case_tac dn)
       apply(rename_tac name dpt)
       apply (simp)
       apply(simp add:domainNameChopRotate)
       apply (metis chopOne_not_decrease less_eq_refl)
      apply simp
     done
    
    corollary "dn ≤ domainNameDeptChopOne ((domainNameDeptChopOne ^^ n) (dn))"
    by (metis chop_not_decrease_hierarchy domainNameChopFunApply domainNameChopRotateSuc)
      

   text‹compute maximum common level of both inputs›
   fun chop_sup :: "domainNameDept ⇒ domainNameDept ⇒ domainNameDept" where
      "chop_sup Leaf _ = Leaf" | 
      "chop_sup _ Leaf = Leaf" | 
      "chop_sup (a--as) (b--bs) = (if a ≠ b then Leaf else a--(chop_sup as bs))" 

   lemma "chop_sup (''a''--''b''--''c''--Leaf) (''a''--''b''--''d''--Leaf) = ''a'' -- ''b'' -- Leaf" by eval
   lemma "chop_sup (''a''--''b''--''c''--Leaf) (''a''--''x''--''d''--Leaf) = ''a'' -- Leaf" by eval
   lemma "chop_sup (''a''--''b''--''c''--Leaf) (''x''--''x''--''d''--Leaf) = Leaf" by eval

   lemma chop_sup_commute: "chop_sup a b = chop_sup b a"
    apply(induction a b rule: chop_sup.induct)
      apply(rename_tac a)
      apply(simp_all)
    apply(case_tac a, simp_all)
    done
  lemma chop_sup_max1: "a ≤ chop_sup a b"
    apply(induction a b rule: chop_sup.induct)
      by(simp_all)
  lemma chop_sup_max2: "b ≤ chop_sup a b"
    apply(subst chop_sup_commute)
    by(simp add: chop_sup_max1)

   (* don't need this, preserver ≤ on domainNameDept and ⊑ on domainName
   instantiation domainNameDept :: partial_order
   begin
     fun leq_domainNameDept :: "domainNameDept ⇒ domainNameDept ⇒ bool" (* ⊑ *) where 
      "leq_domainNameDept a b = (a ≤ b)"
   instance
      by(intro_classes,simp_all)
   end
   *)
   lemma chop_sup_is_sup: "∀z. a ≤ z ∧ b ≤ z ⟶ chop_sup a b ≤ z"
    apply(clarify)
    apply(induction a b rule: chop_sup.induct)
      apply(simp_all)
    apply(rule conjI)
     apply(clarify)
     apply(subgoal_tac "z=Leaf")
      apply(simp)
     apply(simp add: uncomparable_sup_is_Top)
    apply(clarify)
    apply(case_tac z)
     by(simp_all)
    


  datatype domainName = DN domainNameDept | Unassigned


  subsubsection ‹Makeing it a complete Lattice›
    instantiation domainName :: partial_order
    begin
      (* adding trust here would violate transitivity or antsymmetry *)
      fun leq_domainName :: "domainName ⇒ domainName ⇒ bool" (* ⊑ *) where 
        "leq_domainName Unassigned _ = True" |
        "leq_domainName _ Unassigned = False" |
        "leq_domainName (DN dnA) (DN dnB) = (dnA ≤ dnB)"
    instance
      apply(intro_classes)
      (* x ⊑ x *)
        apply(case_tac x)
       apply(simp_all)
      (* x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z *)
       apply(case_tac x, rename_tac dnX)
        apply(case_tac y, rename_tac dnY)
         apply(case_tac z, rename_tac dnZ)
          apply(simp_all)
      (* x ⊑ y ⟹ y ⊑ x ⟹ x = y *)
      apply(case_tac x, rename_tac dnX)
       apply(case_tac y, rename_tac dnY)
        apply(simp_all)
      apply(metis domainName.exhaust leq_domainName.simps(2))
      done
    end

    lemma "is_Inf {Unassigned, DN Leaf} Unassigned"
      by(simp add: is_Inf_def)
    
    text ‹The infinum of two elements:›
    fun DN_inf :: "domainName ⇒ domainName ⇒ domainName" where
      "DN_inf Unassigned _ = Unassigned" |
      "DN_inf _ Unassigned = Unassigned" |
      "DN_inf (DN a) (DN b) = (if a ≤ b then DN a else if b ≤ a then DN b else Unassigned)"

    lemma "DN_inf (DN (''TUM''--''i8''--Leaf)) (DN (''TUM''--''i20''--Leaf)) = Unassigned" by eval
    lemma "DN_inf (DN (''TUM''--''i8''--Leaf)) (DN (''TUM''--Leaf)) = DN (''TUM'' -- ''i8'' -- Leaf)" by eval
      

    lemma DN_inf_commute: "DN_inf x y = DN_inf y x"
      apply(induction x y rule: DN_inf.induct)
        apply(rename_tac x)
        apply(case_tac x)
         by (simp_all)

    lemma DN_inf_is_inf: "is_inf x y (DN_inf x y)"
      apply(induction x y rule: DN_inf.induct)
        apply(simp add: is_inf_def)
       apply(simp add: is_inf_def)
      apply(simp add: is_inf_def)
      apply(clarify)
      apply(rename_tac z)
      apply(case_tac z)
       apply(simp)
       apply(rename_tac zn)
       apply(simp_all)
      using common_inf_imp_comparable by blast

    
    fun DN_sup :: "domainName ⇒ domainName ⇒ domainName" where
      "DN_sup Unassigned a = a" | 
      "DN_sup a Unassigned = a" |
      "DN_sup (DN a) (DN b) = DN (chop_sup a b)"

    lemma DN_sup_commute: "DN_sup x y = DN_sup y x"
      apply(induction x y rule: DN_sup.induct)
        apply(rename_tac x)
        apply(case_tac x)
         by(simp_all add: chop_sup_commute)

    lemma DN_sup_is_sup: "is_sup x y (DN_sup x y)"
      apply(induction x y rule: DN_inf.induct)
        apply(simp add: is_sup_def leq_refl)
       apply(simp add: is_sup_def)
      apply(simp add: is_sup_def chop_sup_max1 chop_sup_max2)
      apply(clarify)
      apply(rename_tac z)
      apply(case_tac z)
       apply(simp)
       apply(rename_tac zn)
       apply(simp_all)
      apply(clarify)
      apply(simp add: chop_sup_is_sup)
      done
   
    text ‹domainName is a Lattice:›
    instantiation domainName :: lattice
      begin
      instance
        apply intro_classes
         apply(rule_tac x="DN_inf x y" in exI)
         apply(fact DN_inf_is_inf)
        apply(rule_tac x="DN_sup x y" in exI)
        apply(rule DN_sup_is_sup)
       done
    end
    



(*TRUST*)


  datatype domainNameTrust = DN "(domainNameDept × nat)" | Unassigned

    (*transitivity only if trustA ≥ trust C*)
    fun leq_domainNameTrust :: "domainNameTrust ⇒ domainNameTrust ⇒ bool" (infixr ‹⊑⇩t⇩r⇩u⇩s⇩t› 65)  where 
      "leq_domainNameTrust Unassigned _ = True" |
      "leq_domainNameTrust _ Unassigned = False" |
      "leq_domainNameTrust (DN (dnA, trustA)) (DN (dnB, trustB)) = (dnA ≤ (domainNameChop dnB trustB))"

    lemma leq_domainNameTrust_refl: "x ⊑⇩t⇩r⇩u⇩s⇩t x"
      apply(case_tac x)
       apply(rename_tac prod)
       apply(case_tac prod)
       apply(simp add: chop_not_decrease_hierarchy)
      by(simp)
   
   lemma leq_domainNameTrust_NOT_trans: "∃x y z. x ⊑⇩t⇩r⇩u⇩s⇩t y ∧ y ⊑⇩t⇩r⇩u⇩s⇩t z ∧ ¬ x ⊑⇩t⇩r⇩u⇩s⇩t z"
    apply(rule_tac x="DN (''TUM''--Leaf, 0)" in exI)
    apply(rule_tac x="DN (''TUM''--''i8''--Leaf, 1)" in exI)
    apply(rule_tac x="DN (''TUM''--''i8''--Leaf, 0)" in exI)
    apply(simp)
    done

   lemma leq_domainNameTrust_NOT_antisym: "∃x y. x ⊑⇩t⇩r⇩u⇩s⇩t y ∧ y ⊑⇩t⇩r⇩u⇩s⇩t x ∧ x ≠ y"
    apply(rule_tac x="DN (Leaf, 3)" in exI)
    apply(rule_tac x="DN (Leaf, 4)" in exI)
    apply(simp)
    done

subsubsection‹The network security invariant›

definition default_node_properties :: "domainNameTrust"
  where  "default_node_properties = Unassigned"

text‹The sender is, noticing its trust level, on the same or higher hierarchy level as the receiver.›
fun sinvar :: "'v graph ⇒ ('v ⇒ domainNameTrust) ⇒ bool" where
  "sinvar G nP = (∀ (s, r) ∈ edges G. (nP r) ⊑⇩t⇩r⇩u⇩s⇩t (nP s))"



(*TODO: old legacy function!*)
text‹a domain name must be in the supplied tree›
fun verify_globals :: "'v graph ⇒ ('v ⇒ domainNameTrust) ⇒ domainTree ⇒ bool" where
  "verify_globals G nP tree = (∀ v ∈ nodes G. 
    case (nP v) of Unassigned ⇒ True | DN (level, trust) ⇒ valid_hierarchy_pos tree level
   )"


lemma "verify_globals ⦇ nodes=set [1,2,3], edges=set [] ⦈ (λn. default_node_properties) (Department ''TUM'' [])"
  by (simp add: default_node_properties_def)


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




thm SecurityInvariant_withOffendingFlows.sinvar_mono_def
lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
  apply(rule_tac SecurityInvariant_withOffendingFlows.sinvar_mono_I_proofrule)
   apply(auto)
  apply(rename_tac nP e1 e2 N E' e1' e2' E)
  apply(blast)
 done


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)[4]
   apply(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
  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])
done


subsubsection ‹ENF›
  lemma DomainHierarchyNG_ENF: "SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form sinvar (λ s r. r ⊑⇩t⇩r⇩u⇩s⇩t s)"
    unfolding SecurityInvariant_withOffendingFlows.sinvar_all_edges_normal_form_def
    by simp
  lemma DomainHierarchyNG_ENF_refl: "SecurityInvariant_withOffendingFlows.ENF_refl sinvar (λ s r. r ⊑⇩t⇩r⇩u⇩s⇩t s)"
    unfolding SecurityInvariant_withOffendingFlows.ENF_refl_def
    apply(rule conjI)
     apply(simp add: DomainHierarchyNG_ENF)
    apply(simp add: leq_domainNameTrust_refl)
  done
  lemma unassigned_default_candidate: "∀nP s r. ¬ (nP r)  ⊑⇩t⇩r⇩u⇩s⇩t (nP s) ⟶ ¬ (nP r)  ⊑⇩t⇩r⇩u⇩s⇩t default_node_properties"
    apply(clarify)
    apply (simp add: default_node_properties_def) 
    by (metis leq_domainNameTrust.elims(3) leq_domainNameTrust.simps(2))

  definition DomainHierarchyNG_offending_set:: "'v graph ⇒ ('v ⇒ domainNameTrust) ⇒ ('v × 'v) set set" where
  "DomainHierarchyNG_offending_set G nP = (if sinvar G nP then
      {}
     else 
      { {e ∈ edges G. case e of (e1,e2) ⇒ ¬ (nP e2) ⊑⇩t⇩r⇩u⇩s⇩t (nP e1)} })"
  lemma DomainHierarchyNG_offending_set: "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = DomainHierarchyNG_offending_set"
    apply(simp only: fun_eq_iff SecurityInvariant_withOffendingFlows.ENF_offending_set[OF DomainHierarchyNG_ENF] DomainHierarchyNG_offending_set_def)
    apply(rule allI)+
    apply(rename_tac G nP)
    apply(auto split:prod.split_asm prod.split simp add: Let_def)
  done


  lemma Unassigned_unique_default: "otherbot ≠ default_node_properties ⟹
         ∃G nP gP 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)))"
    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 domainNameTrust.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)
     apply(rename_tac prod)
     apply(case_tac prod)
     apply(rename_tac dn trustlevel)
     apply(clarify)

     apply(case_tac dn)
  
    (* case (name -- dpt, trustlevel)  *)
      apply(rename_tac name dpt)
      apply(simp)
      apply(rule_tac x="(λ x. default_node_properties)(vertex_1 := Unassigned, vertex_2 := DN (name--dpt, 0 ))" in exI, simp)
      apply(rule_tac x="vertex_1" in exI, simp)
      apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
      apply(simp add:chop_not_decrease_hierarchy)
  
    (* case (Leaf, trustlevel)*)
     apply(simp)
     apply(rule_tac x="(λ x. default_node_properties)(vertex_1 := Unassigned, vertex_2 := DN (Leaf, 0))" in exI, simp)
     apply(rule_tac x="vertex_1" in exI, simp)
     apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
  
    (* case Unassigned *)
    apply(simp add: default_node_properties_def)
   done

interpretation DomainHierarchyNG: SecurityInvariant_ACS
where default_node_properties = default_node_properties
and sinvar = sinvar
rewrites "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar = DomainHierarchyNG_offending_set"
  apply unfold_locales
    apply(rule ballI)
    apply(drule SecurityInvariant_withOffendingFlows.ENF_fsts_refl_instance[OF DomainHierarchyNG_ENF_refl unassigned_default_candidate], simp_all)[1]
   apply(erule default_uniqueness_by_counterexample_ACS)
   apply(drule Unassigned_unique_default) 
   apply(simp)
  apply(fact DomainHierarchyNG_offending_set)
 done




lemma TopoS_DomainHierarchyNG: "SecurityInvariant sinvar default_node_properties receiver_violation"
  unfolding receiver_violation_def by(unfold_locales)




hide_const (open) sinvar receiver_violation

end