Theory NormalisationGenericProofs

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2017 Université Paris-Sud, France
 *               2015-2017 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection‹Normalisation Proofs (Generic)›
  theory
    NormalisationGenericProofs
    imports 
      FWNormalisationCore
begin
  
text ‹
  This theory contains the generic proofs of the normalisation procedure, i.e. those which 
  are independent from the concrete semantical interpretation function.  
›
    
lemma domNMT: "dom X ≠ {} ⟹ X ≠ ∅"
  by auto
    
lemma denyNMT: "deny_all ≠  ∅"
  apply (rule domNMT)
  by (simp add: deny_all_def dom_def)
    
lemma wellformed_policy1_charn[rule_format]: 
"wellformed_policy1 p ⟶ DenyAll ∈ set p ⟶ (∃ p'. p = DenyAll # p' ∧ DenyAll ∉ set p')"
  by(induct "p",simp_all)
    
lemma singleCombinatorsConc: "singleCombinators (x#xs) ⟹ singleCombinators xs"
  by (case_tac x,simp_all)
    
lemma aux0_0: "singleCombinators x ⟹ ¬ (∃ a b. (a⊕b) ∈ set x)"
  apply (induct "x", simp_all)
  subgoal for a b 
    by (case_tac "a",simp_all)
  done
  
lemma aux0_4: "(a ∈ set x ∨ a ∈ set y) = (a ∈ set (x@y))"
  by auto
    
lemma aux0_1: "⟦singleCombinators xs; singleCombinators [x]⟧ ⟹
               singleCombinators (x#xs)"
  by (case_tac "x",simp_all) 
    
lemma aux0_6: "⟦singleCombinators xs; ¬ (∃ a b. x = a ⊕ b)⟧ ⟹
               singleCombinators(x#xs)"
  apply (rule aux0_1,simp_all)
  apply (case_tac "x",simp_all)
  done
    
lemma aux0_5: " ¬ (∃ a b. (a⊕b) ∈ set x) ⟹ singleCombinators x"
  apply (induct "x")   
   apply simp_all 
  by (metis aux0_6)
    
lemma ANDConc[rule_format]: "allNetsDistinct (a#p) ⟶ allNetsDistinct (p)"
  apply (simp add: allNetsDistinct_def)
  apply (case_tac "a")
  by simp_all
    
lemma aux6: "twoNetsDistinct a1 a2 a b ⟹
            dom (deny_all_from_to a1 a2) ∩ dom (deny_all_from_to a b) = {}"
  by (auto simp: twoNetsDistinct_def netsDistinct_def src_def dest_def 
      in_subnet_def PolicyCombinators.PolicyCombinators dom_def)
    
lemma aux5[rule_format]: "(DenyAllFromTo a b) ∈ set p ⟶ a ∈ set (net_list p)"
  by (rule net_list_aux.induct,simp_all) 
    
lemma aux5a[rule_format]: "(DenyAllFromTo b a) ∈ set p ⟶ a ∈ set (net_list p)"
  by (rule net_list_aux.induct,simp_all) 
    
lemma aux5c[rule_format]:
  "(AllowPortFromTo a b po) ∈ set p ⟶ a ∈ set (net_list p)"
  by (rule net_list_aux.induct,simp_all) 
    
lemma aux5d[rule_format]:
  "(AllowPortFromTo b a po) ∈ set p ⟶ a ∈ set (net_list p)"
  by (rule net_list_aux.induct,simp_all) 
    
lemma aux10[rule_format]: "a ∈ set (net_list p) ⟶ a ∈ set (net_list_aux p)"
  by simp
    
lemma srcInNetListaux[simp]: 
  "⟦x ∈ set p; singleCombinators[x]; x ≠ DenyAll⟧ ⟹ srcNet x ∈ set (net_list_aux p)"
  apply (induct "p")
   apply simp_all
  subgoal for a p   
    apply (case_tac "x = a", simp_all)
     apply (case_tac a, simp_all)
    apply (case_tac a, simp_all)
    done
  done 
    
lemma destInNetListaux[simp]: 
  "⟦x ∈ set p; singleCombinators[x]; x ≠ DenyAll⟧ ⟹ destNet x ∈ set (net_list_aux p)"
  apply (induct p)
   apply simp_all
  subgoal for a p
    apply (case_tac "x = a", simp_all)
     apply (case_tac "a", simp_all)
    apply (case_tac "a", simp_all)
    done 
  done 
    
lemma tND1: "⟦allNetsDistinct p; x ∈ set p; y ∈ set p; a = srcNet x;
             b = destNet x; c = srcNet y; d = destNet y; a ≠ c;
             singleCombinators[x]; x ≠ DenyAll; singleCombinators[y];
             y ≠ DenyAll⟧ ⟹ twoNetsDistinct a b c d"
  by (simp add: allNetsDistinct_def twoNetsDistinct_def)
    
lemma tND2: "⟦allNetsDistinct p; x ∈ set p; y ∈ set p; a = srcNet x;
             b = destNet x; c = srcNet y; d = destNet y; b ≠ d;
             singleCombinators[x]; x ≠ DenyAll; singleCombinators[y];
             y ≠ DenyAll⟧ ⟹ twoNetsDistinct a b c d"
  by (simp add: allNetsDistinct_def twoNetsDistinct_def)
    
lemma tND: "⟦allNetsDistinct p; x ∈ set p; y ∈ set p; a = srcNet x;
            b = destNet x; c = srcNet y; d = destNet y; a ≠ c ∨ b ≠ d;
            singleCombinators[x]; x ≠ DenyAll; singleCombinators[y]; y ≠ DenyAll⟧
            ⟹ twoNetsDistinct a b c d"
  apply (case_tac "a ≠ c", simp_all)
   apply (erule_tac x = x and y =y in tND1, simp_all)
  apply (erule_tac x = x and y =y in tND2, simp_all)
  done
    
lemma aux7: "⟦DenyAllFromTo a b ∈ set p; allNetsDistinct ((DenyAllFromTo c d)#p);
             a≠ c∨ b≠ d⟧ ⟹ twoNetsDistinct a b c d"
  apply (erule_tac x = "DenyAllFromTo a b" and y = "DenyAllFromTo c d" in tND)
  by simp_all
    
lemma aux7a: "⟦DenyAllFromTo a b  ∈ set p;
              allNetsDistinct ((AllowPortFromTo c d po)#p); a ≠ c∨ b ≠ d⟧ ⟹ 
              twoNetsDistinct a b c d"
  apply (erule_tac x = "DenyAllFromTo a b" and
      y = "AllowPortFromTo  c d po" in tND)
  by simp_all
    
lemma nDComm: assumes ab: "netsDistinct a b" shows ba: "netsDistinct b a"
  apply (insert ab)
  by (auto simp: netsDistinct_def  in_subnet_def)
    
lemma tNDComm: 
  assumes abcd: "twoNetsDistinct a b c d" shows "twoNetsDistinct c d a b"
  apply (insert abcd)
  by (metis twoNetsDistinct_def nDComm)
    
lemma aux[rule_format]: "a ∈ set (removeShadowRules2 p) ⟶ a ∈ set p"
  apply (case_tac a)
  by (rule removeShadowRules2.induct, simp_all)+
    
lemma aux12: "⟦a ∈ x; b ∉ x⟧ ⟹ a ≠ b"
  by auto
    
lemma ND0aux1[rule_format]: "DenyAllFromTo x y ∈ set b ⟹  
                             x ∈ set (net_list_aux b)"
  by (metis aux5 net_list.simps set_remdups)
    
lemma ND0aux2[rule_format]: "DenyAllFromTo x y ∈ set b ⟹  
                             y ∈ set (net_list_aux b)"
  by (metis aux5a net_list.simps set_remdups)
    
lemma ND0aux3[rule_format]: "AllowPortFromTo x y p ∈ set b ⟹  
                             x ∈ set (net_list_aux b)"
  by (metis aux5c net_list.simps set_remdups)
    
lemma ND0aux4[rule_format]: "AllowPortFromTo x y p ∈ set b ⟹  
                             y ∈ set (net_list_aux b)"
  by (metis aux5d net_list.simps set_remdups)
    
lemma aNDSubsetaux[rule_format]: "singleCombinators a  ⟶ set a ⊆ set b ⟶ 
                                  set (net_list_aux a) ⊆ set (net_list_aux b)"
  apply (induct a)
   apply simp_all
  apply clarify
  apply (drule mp, erule singleCombinatorsConc)
  subgoal for a a' x
    apply (case_tac "a")
       apply (simp_all add: contra_subsetD)
      apply (metis contra_subsetD)
     apply (metis ND0aux1 ND0aux2 contra_subsetD)
    apply (metis ND0aux3 ND0aux4 contra_subsetD)
    done
  done
    
lemma aNDSetsEqaux[rule_format]: "singleCombinators a ⟶ singleCombinators b ⟶ 
                 set a = set b ⟶ set (net_list_aux a) = set (net_list_aux b)"
  apply (rule impI)+
  apply (rule equalityI)
   apply (rule aNDSubsetaux, simp_all)+
  done
    
lemma aNDSubset: "⟦singleCombinators a;set a ⊆ set b; allNetsDistinct b⟧ ⟹ 
                  allNetsDistinct a"
  apply (simp add: allNetsDistinct_def)
  apply (rule allI)+
  apply (rule impI)+
  subgoal for x y 
    apply (drule_tac x = "x" in spec, drule_tac x = "y" in spec)
    using aNDSubsetaux by blast
  done
    
lemma aNDSetsEq: "⟦singleCombinators a; singleCombinators b; set a = set b; 
                  allNetsDistinct b⟧ ⟹ allNetsDistinct a"
  apply (simp add: allNetsDistinct_def)
  apply (rule allI)+
  apply (rule impI)+
  subgoal for x y 
    apply (drule_tac x = "x" in spec, drule_tac x = "y" in spec)
    using aNDSetsEqaux by auto
  done
    
lemma SCConca: "⟦singleCombinators p; singleCombinators [a]⟧ ⟹ 
                singleCombinators (a#p)" 
  by(metis aux0_1)
    
lemma aux3[simp]: "⟦singleCombinators p; singleCombinators [a];  
                     allNetsDistinct (a#p)⟧ ⟹ allNetsDistinct (a#a#p)"
  by (metis aNDSetsEq aux0_1 insert_absorb2 list.set(2))
    
lemma wp1_aux1a[rule_format]: "xs ≠ [] ⟶ wellformed_policy1_strong (xs @ [x]) ⟶ 
                               wellformed_policy1_strong xs"
  by (induct xs,simp_all)
    
lemma wp1alternative_RS1[rule_format]: "DenyAll ∈ set p ⟶ 
                              wellformed_policy1_strong (removeShadowRules1 p)"
  by (induct p,simp_all)
    
lemma wellformed_eq: "DenyAll ∈ set p ⟶ 
                      ((wellformed_policy1 p) = (wellformed_policy1_strong p))"
  by (induct p,simp_all)
    
lemma set_insort: "set(insort x xs l) = insert x (set xs)"
  by (induct xs) auto
    
lemma set_sort[simp]: "set(sort xs l) = set xs"
  by (induct xs) (simp_all add:set_insort)
    
    
lemma set_sortQ: "set(qsort xs l) = set xs"
  by simp
    
lemma aux79[rule_format]: "y ∈ set (insort x a l) ⟶  y ≠ x ⟶ y ∈ set a"
  apply (induct a)
  by auto
    
lemma aux80: "⟦y ∉ set p; y ≠ x⟧ ⟹ y ∉ set (insort x (sort p l) l)"
  apply (metis aux79 set_sort)
  done
    
    
lemma WP1Conca: "DenyAll ∉ set p ⟹ wellformed_policy1 (a#p)"
  by (case_tac a,simp_all)
    
    
lemma saux[simp]: "(insort DenyAll p l) = DenyAll#p"
  by (induct_tac p,simp_all)
    
lemma saux3[rule_format]: "DenyAllFromTo a b ∈ set list ⟶ 
                          DenyAllFromTo c d ∉ set list ⟶ (a ≠ c) ∨ (b ≠ d)"
  by blast
    
lemma waux2[rule_format]: " (DenyAll ∉ set xs) ⟶ wellformed_policy1 xs"
  by (induct_tac xs,simp_all)
    
lemma waux3[rule_format]: "⟦x ≠ a;  x ∉ set p⟧ ⟹ x ∉ set (insort a p l)"
  by (metis aux79)
    
lemma wellformed1_sorted_aux[rule_format]: "wellformed_policy1 (x#p) ⟹ 
                                            wellformed_policy1 (insort x p l)" 
  by (metis NormalisationGenericProofs.set_insort list.set(2) saux waux2 wellformed_eq 
            wellformed_policy1_strong.simps(2))
    
lemma wellformed1_sorted_auxQ[rule_format]: "wellformed_policy1 (p) ⟹ 
                                            wellformed_policy1 (qsort p l)" 
proof (induct p)
  case Nil show ?case by simp
next
  case (Cons a S) then show ?case
    apply simp_all 
    apply (cases a,simp_all)
    by  (metis Combinators.simps append_Cons append_Nil qsort.simps(2) set_ConsD set_qsort waux2)+
  qed        
    
lemma SR1Subset: "set (removeShadowRules1 p) ⊆ set p"
  apply (induct_tac p, simp_all)
  subgoal for x xs
    apply (case_tac "x", simp_all) 
       apply(auto)
    done
  done
    
lemma SCSubset[rule_format]: " singleCombinators b ⟶ set a ⊆ set b ⟶
                              singleCombinators a"
proof (induct a)
  case Nil thus ?case by simp
next
  case (Cons x xs)  thus ?case
    by (meson aux0_0 aux0_5 subsetCE)
qed
  
lemma setInsert[simp]: "set list ⊆ insert a (set list)"
  by auto
    
lemma SC_RS1[rule_format,simp]: "singleCombinators p ⟶ allNetsDistinct p ⟶
    singleCombinators (removeShadowRules1 p)"
  apply (induct_tac p)
   apply simp_all
  using ANDConc singleCombinatorsConc by blast
    
lemma RS2Set[rule_format]: "set (removeShadowRules2 p) ⊆ set p"
  apply(induct p, simp_all)
  subgoal for a as  
    apply(case_tac a)
    by(auto)
  done
    
lemma WP1: "a ∉ set list ⟹ a ∉ set (removeShadowRules2 list)"
  using RS2Set [of list] by blast
    
    
lemma denyAllDom[simp]: "x ∈ dom (deny_all)"
  by (simp add: UPFDefs(24) domI) 
    
lemma lCdom2: "(list2FWpolicy (a @ (b @ c))) = (list2FWpolicy ((a@b)@c))"
  by auto
    
lemma SCConcEnd: "singleCombinators (xs @ [xa]) ⟹ singleCombinators xs"
  apply (induct "xs", simp_all)
  subgoal for a as
    by  (case_tac "a" , simp_all)
  done   
    
lemma list2FWpolicyconc[rule_format]: "a ≠ [] ⟶
                               (list2FWpolicy (xa # a)) = (xa) ⊕ (list2FWpolicy a)"
  by (induct a,simp_all)
    
lemma wp1n_tl [rule_format]: "wellformed_policy1_strong p ⟶
                              p = (DenyAll#(tl p))"
  by (induct p, simp_all)
    
lemma foo2: "a ∉ set ps ⟹ 
             a ∉ set ss ⟹
             set p = set s ⟹ 
             p = (a#(ps)) ⟹ 
             s = (a#ss) ⟹ 
             set (ps) = set (ss)"
  by auto
    
    
lemma SCnotConc[rule_format,simp]: "a⊕b ∈ set p ⟶ singleCombinators p ⟶False"
  apply (induct p, simp_all)
  subgoal for p ps  
    by(case_tac p, simp_all)
  done
    
lemma auxx8: "removeShadowRules1_alternative_rev [x] = [x]"
  by (case_tac "x", simp_all)
    
lemma RS1End[rule_format]: "x ≠ DenyAll ⟶ removeShadowRules1 (xs @ [x]) = 
                            (removeShadowRules1 xs)@[x]"
  by (induct_tac xs, simp_all)
    
lemma aux114: "x ≠ DenyAll ⟹ removeShadowRules1_alternative_rev (x#xs) = 
               x#(removeShadowRules1_alternative_rev xs)"
  apply (induct_tac xs)
  apply (auto simp: auxx8)
  by (case_tac "x", simp_all)
    
lemma aux115[rule_format]: "x ≠ DenyAll⟹removeShadowRules1_alternative (xs@[x]) 
                            = (removeShadowRules1_alternative xs)@[x]"
  apply (simp add: removeShadowRules1_alternative_def aux114)
  done
    
lemma RS1_DA[simp]: "removeShadowRules1 (xs @ [DenyAll]) = [DenyAll]"
  by (induct_tac xs, simp_all)
    
lemma rSR1_eq: "removeShadowRules1_alternative = removeShadowRules1"
  apply (rule ext)
  apply (simp add: removeShadowRules1_alternative_def)
  subgoal for x 
    apply (rule_tac xs = x in rev_induct)
     apply simp_all
    subgoal for x xs
      apply (case_tac "x = DenyAll", simp_all)
      apply (metis RS1End aux114 rev.simps(2))
      done
    done
  done
    
lemma domInterMT[rule_format]: "⟦dom a ∩ dom b = {}; x ∈ dom a⟧ ⟹ x ∉ dom b"
  by auto
    
lemma domComm: "dom a ∩ dom b = dom b ∩ dom a"
  by auto
        
lemma r_not_DA_in_tl[rule_format]: 
  "wellformed_policy1_strong p ⟶  a ∈ set p⟶ a ≠ DenyAll ⟶ a ∈ set (tl p)"
  by (induct p,simp_all)
    
lemma wp1_aux1aa[rule_format]: "wellformed_policy1_strong p ⟶ DenyAll ∈ set p"
  by (induct p,simp_all)
    
lemma mauxa: "(∃ r. a b = ⌊r⌋) = (a b ≠ ⊥)"
  by auto
    
lemma l2p_aux[rule_format]: "list ≠ [] ⟶
                             list2FWpolicy (a # list) = a ⊕(list2FWpolicy list)"
  by (induct "list", simp_all)
    
lemma l2p_aux2[rule_format]: "list = [] ⟹ list2FWpolicy (a # list) = a"
  by simp
           
lemma aux7aa: 
  assumes 1 : "AllowPortFromTo a b poo ∈ set p" 
    and    2 : "allNetsDistinct ((AllowPortFromTo c d po) # p)"
    and    3 : "a ≠ c ∨ b ≠ d"
  shows       "twoNetsDistinct a b c d" (is "?H")
proof(cases "a ≠ c") print_cases
  case True assume *:"a ≠ c"  show ?H
    by (meson "1" "2" True allNetsDistinct_def aux5c list.set_intros(1) 
        list.set_intros(2) twoNetsDistinct_def)
next
  case False assume *:"¬(a ≠ c)" show "twoNetsDistinct a b c d"
    by (meson "1" "2" "3" False allNetsDistinct_def aux5d list.set_intros(1) 
        list.set_intros(2) twoNetsDistinct_def)
qed
  
lemma ANDConcEnd: "⟦ allNetsDistinct (xs @ [xa]); singleCombinators xs⟧ ⟹ 
                   allNetsDistinct xs"
  by (rule aNDSubset, auto)
    
lemma WP1ConcEnd[rule_format]: 
  "wellformed_policy1 (xs@[xa]) ⟶ wellformed_policy1 xs"
  by (induct xs, simp_all)
    
lemma NDComm: "netsDistinct a b = netsDistinct b a"
  by (auto simp: netsDistinct_def in_subnet_def)
    
    
lemma wellformed1_sorted[simp]: 
  assumes wp1: "wellformed_policy1 p" 
  shows        "wellformed_policy1 (sort p l)"
proof (cases p)
  case Nil thus ?thesis by simp
next
  case (Cons x xs) thus ?thesis
  proof (cases "x = DenyAll") 
    case True thus ?thesis using assms Cons by simp 
  next
    case False thus ?thesis using assms  
      by (metis Cons set_sort False waux2 wellformed_eq 
          wellformed_policy1_strong.simps(2)) 
  qed
qed
  
  
lemma wellformed1_sortedQ[simp]: 
  assumes wp1: "wellformed_policy1 p" 
  shows        "wellformed_policy1 (qsort p l)"
proof (cases p)
  case Nil thus ?thesis by simp
next
  case (Cons x xs) thus ?thesis
  proof (cases "x = DenyAll") 
    case True thus ?thesis using assms Cons by simp 
  next
    case False thus ?thesis using assms  
      by (metis Cons set_qsort False waux2 wellformed_eq 
          wellformed_policy1_strong.simps(2)) 
  qed
qed
  
lemma SC1[simp]: "singleCombinators p ⟹singleCombinators (removeShadowRules1 p)"
  by (erule SCSubset) (rule SR1Subset)
    
lemma SC2[simp]: "singleCombinators p ⟹singleCombinators (removeShadowRules2 p)"
  by (erule SCSubset) (rule RS2Set)
    
lemma SC3[simp]: "singleCombinators p ⟹ singleCombinators (sort p l)"
  by (erule SCSubset) simp
    
lemma SC3Q[simp]: "singleCombinators p ⟹ singleCombinators (qsort p l)"
  by (erule SCSubset) simp
    
lemma aND_RS1[simp]: "⟦singleCombinators p; allNetsDistinct p⟧ ⟹ 
                      allNetsDistinct (removeShadowRules1 p)"
  apply (rule aNDSubset)
  apply (erule SC_RS1, simp_all)
  apply (rule SR1Subset)
  done
    
lemma aND_RS2[simp]: "⟦singleCombinators p; allNetsDistinct p⟧ ⟹ 
                      allNetsDistinct (removeShadowRules2 p)"
  apply (rule aNDSubset)
  apply (erule SC2, simp_all)
  apply (rule RS2Set)
  done
    
lemma aND_sort[simp]: "⟦singleCombinators p; allNetsDistinct p⟧ ⟹  
                       allNetsDistinct (sort p l)"
  apply (rule aNDSubset)
  by (erule SC3, simp_all)
    
    
    
lemma aND_sortQ[simp]: "⟦singleCombinators p; allNetsDistinct p⟧ ⟹  
                       allNetsDistinct (qsort p l)"
  apply (rule aNDSubset)
  by (erule SC3Q, simp_all)
    
lemma inRS2[rule_format,simp]: "x ∉ set p ⟶ x ∉ set (removeShadowRules2 p)"
  apply (insert RS2Set [of p])
  by blast
    
lemma distinct_RS2[rule_format,simp]: "distinct p ⟶ 
                                       distinct (removeShadowRules2 p)"
  apply (induct p)
  apply simp_all
  apply clarify
  subgoal for a p 
    apply (case_tac "a")
    by auto
  done
    
lemma setPaireq: " {x, y} = {a, b} ⟹ x = a ∧ y = b ∨ x = b ∧ y = a"
  by (metis  doubleton_eq_iff)
    
lemma position_positive[rule_format]: "a ∈ set l ⟶ position a l > 0"
  by (induct l, simp_all)
    
lemma pos_noteq[rule_format]: 
  "a ∈ set l ⟶ b ∈ set l ⟶ c ∈ set l ⟶ 
   a ≠ b ⟶ position a l ≤ position b l ⟶ position b l ≤ position c l ⟶ 
   a ≠ c"
proof(induct l)
  case Nil show ?case by simp
next
  case (Cons a R) show ?case 
    by (metis (no_types, lifting) Cons.hyps One_nat_def Suc_le_mono le_antisym 
        length_greater_0_conv list.size(3) nat.inject position.simps(2) 
        position_positive set_ConsD)
qed
  
lemma setPair_noteq: "{a,b} ≠ {c,d} ⟹ ¬ ((a = c) ∧ (b = d))" 
  by auto
    
lemma setPair_noteq_allow: "{a,b} ≠ {c,d} ⟹ ¬ ((a = c) ∧ (b = d) ∧ P)" 
  by auto
    
lemma order_trans:  
  "⟦in_list x l; in_list y l; in_list z l; singleCombinators [x]; 
  singleCombinators [y]; singleCombinators [z]; smaller x y l; smaller y z l⟧ ⟹ 
  smaller x z l"
  apply (case_tac x, simp_all)
   apply (case_tac z, simp_all)
     apply (case_tac y, simp_all)
    apply (case_tac y, simp_all)
     apply (rule conjI|rule impI)+ 
      apply (simp add: setPaireq)
     apply (rule conjI|rule impI)+
     apply (simp_all split: if_splits)
       apply metis+
     apply auto[1]
    apply (simp add: setPaireq)
   apply (rule impI,case_tac y, simp_all)
    apply (simp_all split: if_splits, metis,simp_all add: setPair_noteq setPair_noteq_allow)
  apply (case_tac z, simp_all)
    apply (case_tac y, simp_all)
   apply (case_tac y, simp_all)
    apply (intro impI|rule conjI)+
     apply (simp_all split: if_splits)
     apply (simp add: setPair_noteq)
     apply (erule pos_noteq, simp_all)
    apply auto[1]
   apply (rule conjI,simp add: setPair_noteq_allow)
    apply (erule pos_noteq, simp_all)
   apply auto[1]
  apply (rule impI,rule disjI2) 
  apply (case_tac y, simp_all split: if_splits )
    apply metis
   apply (simp_all add: setPair_noteq_allow)
  done
    
lemma sortedConcStart[rule_format]: 
  "sorted (a # aa # p) l ⟶ in_list a l ⟶ in_list aa l ⟶ all_in_list p l⟶ 
  singleCombinators [a] ⟶ singleCombinators [aa] ⟶ singleCombinators p ⟶ 
  sorted (a#p) l"
  apply (induct p)
   apply simp_all
  apply (rule impI)+
  apply simp
  apply (rule_tac y = "aa" in order_trans)
         apply simp_all
  subgoal for p ps
    apply (case_tac "p", simp_all)
    done
  done
    
lemma singleCombinatorsStart[simp]: "singleCombinators (x#xs) ⟹ 
                                     singleCombinators [x]"
  by (case_tac x, simp_all)
    
    
lemma sorted_is_smaller[rule_format]: 
  "sorted (a # p) l ⟶ in_list a l ⟶ in_list b l ⟶ all_in_list p l ⟶  
  singleCombinators [a] ⟶ singleCombinators p ⟶ b ∈ set p ⟶ smaller a b l"
  apply (induct p)
   apply (auto intro: singleCombinatorsConc sortedConcStart) 
  done
    
lemma sortedConcEnd[rule_format]: "sorted (a # p) l ⟶ in_list a l ⟶ 
                                   all_in_list p l ⟶ singleCombinators [a] ⟶ 
                                   singleCombinators p  ⟶ sorted p l"
  apply (induct p)
   apply (auto intro: singleCombinatorsConc sortedConcStart)
  done
    
lemma in_set_in_list[rule_format]: "a ∈ set p ⟶ all_in_list p l⟶ in_list a l"
  by (induct p) auto
    
lemma sorted_Consb[rule_format]: 
  "all_in_list (x#xs) l ⟶ singleCombinators (x#xs) ⟶ 
    (sorted xs l & (∀y∈set xs. smaller x y l)) ⟶  (sorted (x#xs) l) "
  apply(induct xs arbitrary: x) 
   apply (auto simp: order_trans)
  done
    
lemma sorted_Cons: "⟦all_in_list (x#xs) l; singleCombinators (x#xs)⟧ ⟹ 
              (sorted xs l & (∀y∈set xs. smaller x y l)) =  (sorted (x#xs) l)"
  apply auto
    apply (rule sorted_Consb, simp_all)
   apply (metis singleCombinatorsConc singleCombinatorsStart sortedConcEnd)
  apply (erule sorted_is_smaller)
  apply (auto intro: singleCombinatorsConc singleCombinatorsStart in_set_in_list)
  done
    
lemma smaller_antisym: "⟦¬ smaller a b l; in_list a l; in_list b l; 
                        singleCombinators[a]; singleCombinators [b]⟧ ⟹  
                        smaller b a l"
  apply (case_tac a)
     apply simp_all
   apply (case_tac b)
      apply simp_all
    apply (simp_all split: if_splits)
   apply (rule setPaireq)
   apply simp
  apply (case_tac b)
     apply simp_all
   apply (simp_all split: if_splits)
  done
    
lemma set_insort_insert: "set (insort x xs l) ⊆ insert x (set xs)"
  by (induct xs) auto
    
lemma all_in_listSubset[rule_format]: "all_in_list b l ⟶singleCombinators a ⟶ 
                                      set a ⊆ set b ⟶ all_in_list a l"
  by (induct_tac a) (auto intro: in_set_in_list singleCombinatorsConc)
    
lemma singleCombinators_insort: "⟦singleCombinators [x]; singleCombinators xs⟧ ⟹ 
                                 singleCombinators (insort x xs l)"
  by (metis NormalisationGenericProofs.set_insort aux0_0 aux0_1 aux0_5 list.simps(15))
    
lemma all_in_list_insort: "⟦all_in_list xs l; singleCombinators (x#xs); 
                           in_list x l⟧ ⟹  all_in_list (insort x xs l) l"
  apply (rule_tac b = "x#xs" in all_in_listSubset)
    apply simp_all
   apply (metis singleCombinatorsConc singleCombinatorsStart
      singleCombinators_insort)
  apply (rule set_insort_insert)
  done
    
lemma sorted_ConsA:"⟦all_in_list (x#xs) l; singleCombinators (x#xs)⟧ ⟹ 
              (sorted (x#xs) l)  = (sorted xs l & (∀y∈set xs. smaller x y l))"
  by (metis sorted_Cons)
    
lemma is_in_insort: "y ∈ set xs ⟹ y ∈ set (insort x xs l)"
  by (simp add: NormalisationGenericProofs.set_insort) 
    
lemma sorted_insorta[rule_format]:
  assumes 1 : "sorted (insort x xs l) l"
    and   2 : "all_in_list (x#xs) l" 
    and   3 : "all_in_list (x#xs) l"
    and   4 : "distinct (x#xs)"
    and   5 : "singleCombinators [x]"
    and   6 : "singleCombinators xs"
  shows       "sorted xs l"
proof (insert 1 2 3 4 5 6, induct xs) 
  case Nil show ?case by simp
next 
  case (Cons a xs)
  then show ?case 
    apply simp
    apply (auto intro: is_in_insort sorted_ConsA set_insort singleCombinators_insort 
        singleCombinatorsConc sortedConcEnd all_in_list_insort) [1]
    apply(cases "smaller x a l", simp_all)
    by (metis NormalisationGenericProofs.set_insort NormalisationGenericProofs.sorted_Cons 
        all_in_list.simps(2) all_in_list_insort aux0_1 insert_iff singleCombinatorsConc 
        singleCombinatorsStart singleCombinators_insort) 
qed
  
  
lemma sorted_insortb[rule_format]: 
  "sorted xs l ⟶ all_in_list (x#xs) l ⟶ distinct (x#xs) ⟶ 
   singleCombinators [x] ⟶ singleCombinators xs ⟶ sorted (insort x xs l) l"
proof (induct xs)
  case Nil show ?case by simp_all
next
  case (Cons a xs) 
  have * : "sorted (a # xs) l ⟹      all_in_list (x # a # xs) l ⟹
              distinct (x # a # xs) ⟹  singleCombinators [x] ⟹
              singleCombinators (a # xs) ⟹ sorted (insort x xs l) l" 
    apply(insert Cons.hyps, simp_all)
    apply(metis sorted_Cons all_in_list.simps(2)  singleCombinatorsConc)
    done
  show ?case
    apply (insert Cons.hyps)
    apply (rule impI)+
    apply (insert *, auto intro!: sorted_Consb)    
  proof (rule_tac b = "x#xs" in all_in_listSubset)
    show "in_list x l ⟹ all_in_list xs l ⟹ all_in_list (x # xs) l"
      by simp_all
  next
    show "singleCombinators [x] ⟹
                       singleCombinators (a # xs) ⟹
                       FWNormalisationCore.sorted (FWNormalisationCore.insort x xs l) l ⟹
                       singleCombinators (FWNormalisationCore.insort x xs l)"
      apply (rule singleCombinators_insort, simp_all)
      by (erule singleCombinatorsConc)
  next
    show "set (FWNormalisationCore.insort x xs l) ⊆ set (x # xs)"
      using NormalisationGenericProofs.set_insort_insert by auto
  next
    show "singleCombinators [x] ⟹
                       singleCombinators (a # xs) ⟹
                      singleCombinators (a # FWNormalisationCore.insort x xs l)"
      by (metis SCConca singleCombinatorsConc singleCombinatorsStart  
          singleCombinators_insort)
  next
    fix y
    show "FWNormalisationCore.sorted (a # xs) l ⟹
                       singleCombinators [x] ⟹  singleCombinators (a # xs) ⟹
                       in_list x l ⟹  in_list a l ⟹ all_in_list xs l ⟹
                       ¬ smaller x a l ⟹ y ∈ set (FWNormalisationCore.insort x xs l) ⟹ 
                      smaller a y l"
      by (metis NormalisationGenericProofs.set_insort in_set_in_list insert_iff 
          singleCombinatorsConc singleCombinatorsStart smaller_antisym 
          sorted_is_smaller)
  qed
qed
  
lemma sorted_insort: 
  "⟦all_in_list (x#xs) l; distinct(x#xs); singleCombinators [x];
                     singleCombinators xs⟧ ⟹
                  sorted (insort x xs l) l = sorted xs l"
  by (auto intro: sorted_insorta sorted_insortb)
    
lemma distinct_insort: "distinct (insort x xs l) = (x ∉ set xs ∧ distinct xs)"
  by(induct xs)(auto simp:set_insort)
    
lemma distinct_sort[simp]: "distinct (sort xs l) = distinct xs"
  by(induct xs)(simp_all add:distinct_insort)
    
    
lemma sort_is_sorted[rule_format]: 
  "all_in_list p l ⟶ distinct p ⟶ singleCombinators p ⟶ sorted (sort p l) l"
  apply (induct p)
   apply simp
  by (metis (no_types, lifting) NormalisationGenericProofs.distinct_sort 
      NormalisationGenericProofs.set_sort SC3 all_in_list.simps(2) all_in_listSubset 
      distinct.simps(2) set_subset_Cons singleCombinatorsConc singleCombinatorsStart 
      sort.simps(2) sorted_insortb)
    
lemma smaller_sym[rule_format]: "all_in_list [a] l ⟶ smaller a a l"
  by (case_tac a,simp_all)
    
lemma SC_sublist[rule_format]: 
  "singleCombinators xs ⟹ singleCombinators (qsort [y←xs. P y] l)"
  by (auto intro: SCSubset)
    
lemma all_in_list_sublist[rule_format]: 
  "singleCombinators xs ⟶ all_in_list xs l ⟶ all_in_list (qsort [y←xs. P y] l) l"
  by (auto intro: all_in_listSubset SC_sublist)
    
lemma SC_sublist2[rule_format]: 
  "singleCombinators xs ⟶ singleCombinators ([y←xs. P y])"
  by (auto intro: SCSubset)
    
lemma all_in_list_sublist2[rule_format]: 
  "singleCombinators xs ⟶ all_in_list xs l ⟶ all_in_list ( [y←xs. P y]) l"
  by (auto intro: all_in_listSubset SC_sublist2)
    
lemma all_in_listAppend[rule_format]: 
  "all_in_list (xs) l ⟶ all_in_list (ys) l ⟶ all_in_list (xs @ ys) l"
  by (induct xs) simp_all
    
lemma distinct_sortQ[rule_format]: 
  "singleCombinators xs ⟶ all_in_list xs l ⟶ distinct xs ⟶ distinct (qsort xs l)"
  apply (induct xs l rule: qsort.induct) 
   apply simp
  apply (auto simp: SC_sublist2 singleCombinatorsConc all_in_list_sublist2)
  done
        
lemma singleCombinatorsAppend[rule_format]: 
  "singleCombinators (xs) ⟶ singleCombinators (ys) ⟶ singleCombinators (xs @ ys)"
  apply (induct xs, auto)
  subgoal for a as
    apply (case_tac a,simp_all)
    done 
  subgoal for a as
    apply (case_tac a,simp_all)
    done       
  done
    
lemma sorted_append1[rule_format]:
  "all_in_list xs l  ⟶ singleCombinators xs ⟶
   all_in_list ys l  ⟶ singleCombinators ys ⟶ 
  (sorted (xs@ys) l ⟶ 
  (sorted xs l & sorted ys l & (∀x ∈ set xs. ∀y ∈ set ys. smaller x y l)))"
  apply(induct xs)
   apply(simp_all)
  by (metis NormalisationGenericProofs.sorted_Cons all_in_list.simps(2) all_in_listAppend aux0_1 
      aux0_4 singleCombinatorsAppend singleCombinatorsConc singleCombinatorsStart)
    
lemma sorted_append2[rule_format]:
  "all_in_list xs l⟶ singleCombinators xs ⟶
   all_in_list ys l ⟶ singleCombinators ys ⟶ 
   (sorted xs l & sorted ys l & (∀x ∈ set xs. ∀y ∈ set ys. smaller x y l)) ⟶ 
  (sorted (xs@ys) l)"
  apply (induct xs)
   apply simp_all
  by (metis NormalisationGenericProofs.sorted_Cons all_in_list.simps(2) all_in_listAppend aux0_1 
      aux0_4 singleCombinatorsAppend singleCombinatorsConc singleCombinatorsStart)
    
lemma sorted_append[rule_format]:
  "all_in_list xs l ⟶ singleCombinators xs ⟶
   all_in_list ys l ⟶ singleCombinators ys ⟶ 
   (sorted (xs@ys) l) =
   (sorted xs l & sorted ys l & (∀x ∈ set xs. ∀y ∈ set ys. smaller x y l))"
  apply (rule impI)+
  apply (rule iffI)
   apply (rule sorted_append1,simp_all)
  apply (rule sorted_append2,simp_all)
  done
    
lemma sort_is_sortedQ[rule_format]: 
  "all_in_list p l  ⟶ singleCombinators p ⟶ sorted (qsort p l) l"
proof (induct p l rule: qsort.induct) print_cases
  case 1 show ?case by simp
next
  case 2 fix x::"('a,'b) Combinators" fix xs::"('a,'b) Combinators list" fix l
  show "all_in_list [y←xs . ¬ smaller x y l] l ⟶
                 singleCombinators [y←xs . ¬ smaller x y l] ⟶ 
                 sorted (qsort [y←xs . ¬ smaller x y l] l) l ⟹
                 all_in_list [y←xs . smaller x y l] l ⟶
                 singleCombinators [y←xs . smaller x y l] ⟶ 
                 sorted (qsort [y←xs . smaller x y l] l) l ⟹
                 all_in_list(x#xs) l ⟶  singleCombinators(x#xs) ⟶ sorted (qsort(x#xs) l) l"
    apply (intro impI)
    apply (simp_all add: SC_sublist all_in_list_sublist all_in_list_sublist2 
        singleCombinatorsConc SC_sublist2)
  proof (subst sorted_append)
    show "in_list x l ∧ all_in_list xs l ⟹ 
                       singleCombinators (x # xs) ⟹ 
                       all_in_list (qsort [y←xs . ¬ smaller x y l] l) l"
      by (metis all_in_list_sublist singleCombinatorsConc)
  next
    show "in_list x l ∧ all_in_list xs l ⟹ 
                       singleCombinators (x # xs) ⟹ 
                       singleCombinators (qsort [y←xs . ¬ smaller x y l] l)"
      apply (auto simp: SC_sublist all_in_list_sublist SC_sublist2
          all_in_list_sublist2 sorted_Cons sorted_append not_le)
      apply (metis SC3Q SC_sublist2 singleCombinatorsConc)
      done
  next
    show "sorted (qsort [y←xs . ¬ smaller x y l] l) l ⟹
                       sorted (qsort [y←xs . smaller x y l] l) l ⟹
                       in_list x l ∧ all_in_list xs l ⟹ singleCombinators (x # xs) ⟹ 
                       all_in_list (x # qsort [y←xs . smaller x y l] l) l"
      using all_in_list.simps(2) all_in_list_sublist singleCombinatorsConc by blast
  next
    show "sorted (qsort [y←xs . smaller x y l] l) l ⟹
                       in_list x l ∧ all_in_list xs l ⟹ singleCombinators (x # xs) ⟹ 
                       singleCombinators (x # qsort [y←xs . smaller x y l] l)"
      using SC_sublist aux0_1 singleCombinatorsConc singleCombinatorsStart by blast
  next
    show "sorted (qsort [y←xs . ¬ smaller x y l] l) l ⟹
                       sorted (qsort [y←xs . smaller x y l] l) l ⟹
                       in_list x l ∧ all_in_list xs l ⟹
                       singleCombinators (x # xs) ⟹
                       FWNormalisationCore.sorted (qsort [y←xs . ¬ smaller x y l] l) l ∧
                       FWNormalisationCore.sorted (x # qsort [y←xs . smaller x y l] l) l ∧
                       (∀x'∈set (qsort [y←xs . ¬ smaller x y l] l). 
                                ∀y∈set (x # qsort [y←xs . smaller x y l] l). smaller x' y l)"
      apply(auto)[1]
      apply (metis (mono_tags, lifting) SC_sublist all_in_list.simps(2) 
          all_in_list_sublist aux0_1 mem_Collect_eq set_filter set_qsort 
          singleCombinatorsConc singleCombinatorsStart sorted_Consb)
      apply (metis aux0_0 aux0_6 in_set_in_list singleCombinatorsConc 
          singleCombinatorsStart smaller_antisym)
      by (metis (no_types, lifting) NormalisationGenericProofs.order_trans aux0_0 
          aux0_6 in_set_in_list 
          singleCombinatorsConc singleCombinatorsStart smaller_antisym)
  qed
qed
  
  
lemma inSet_not_MT: "a ∈ set p ⟹ p ≠ []"
  by auto 
    
lemma RS1n_assoc: 
  "x ≠ DenyAll ⟹  removeShadowRules1_alternative xs @ [x] =
                  removeShadowRules1_alternative (xs @ [x])"
  by (simp add: removeShadowRules1_alternative_def aux114)
    
lemma RS1n_nMT[rule_format,simp]: "p ≠ []⟶ removeShadowRules1_alternative p ≠ []"
  apply (simp add: removeShadowRules1_alternative_def)
  apply (rule_tac xs = p in rev_induct, simp_all) 
  subgoal for x xs
    apply (case_tac "xs = []", simp_all)
     apply (case_tac x, simp_all)
    apply (rule_tac xs = "xs" in rev_induct, simp_all)
     apply (case_tac x, simp_all)+
    done
  done
    
lemma RS1N_DA[simp]: "removeShadowRules1_alternative (a@[DenyAll]) = [DenyAll]"
  by (simp add: removeShadowRules1_alternative_def)
    
lemma WP1n_DA_notinSet[rule_format]: "wellformed_policy1_strong p ⟶
                                     DenyAll ∉ set (tl p)"
  by (induct p) (simp_all) 
    
lemma mt_sym: "dom a ∩ dom b = {} ⟹ dom b ∩ dom a = {}"
  by auto
    
lemma DAnotTL[rule_format]: 
  "xs ≠ [] ⟶ wellformed_policy1 (xs @ [DenyAll]) ⟶ False"
  by (induct xs, simp_all)
    
    
lemma AND_tl[rule_format]: "allNetsDistinct ( p) ⟶ allNetsDistinct (tl p)"
  apply (induct p, simp_all)
  by (auto intro: ANDConc)
    
lemma distinct_tl[rule_format]: "distinct p ⟶ distinct (tl p)"
  by (induct p, simp_all)
    
lemma SC_tl[rule_format]: "singleCombinators ( p) ⟶ singleCombinators (tl p)"
  by (induct p, simp_all) (auto intro: singleCombinatorsConc) 
    
lemma Conc_not_MT: "p = x#xs ⟹ p ≠ []"
  by auto
    
lemma wp1_tl[rule_format]: 
  "p ≠ [] ∧ wellformed_policy1 p ⟶ wellformed_policy1 (tl p)"
  by (induct p) (auto intro: waux2)
    
lemma wp1_eq[rule_format]: 
  "wellformed_policy1_strong p ⟹ wellformed_policy1 p"
  apply (case_tac "DenyAll ∈ set p")
   apply (subst wellformed_eq)
    apply (auto elim: waux2)
  done
    
lemma wellformed1_alternative_sorted: 
  "wellformed_policy1_strong p ⟹ wellformed_policy1_strong (sort p l)"
  by (case_tac "p", simp_all)
    
lemma wp1n_RS2[rule_format]: 
  "wellformed_policy1_strong p ⟶ wellformed_policy1_strong (removeShadowRules2 p)"
  by (induct p, simp_all)
    
lemma RS2_NMT[rule_format]: "p ≠ [] ⟶ removeShadowRules2 p ≠ []"
  apply (induct p, simp_all)
  subgoal for a p  
    apply (case_tac "p ≠ []", simp_all)
     apply (case_tac "a", simp_all)+
    done
  done
    
lemma wp1_alternative_not_mt[simp]: "wellformed_policy1_strong p ⟹ p ≠ []"
  by auto
    
lemma AIL1[rule_format,simp]: "all_in_list p l ⟶
                               all_in_list (removeShadowRules1 p) l"
  by (induct_tac p, simp_all)
    
lemma wp1ID: "wellformed_policy1_strong (insertDeny (removeShadowRules1 p))"
  apply (induct p, simp_all)
  subgoal for a p 
    apply (case_tac a, simp_all)
    done
  done
    
lemma dRD[simp]: "distinct (remdups p)"
  by simp
    
lemma AILrd[rule_format,simp]: "all_in_list p l ⟶ all_in_list (remdups p) l"
  by (induct p, simp_all)
    
lemma AILiD[rule_format,simp]: "all_in_list p l ⟶ all_in_list (insertDeny p) l"
  apply (induct p, simp_all)
  apply (rule impI, simp)
  subgoal for a p 
    apply (case_tac a, simp_all)
    done
  done
    
lemma SCrd[rule_format,simp]:"singleCombinators p⟶ singleCombinators(remdups p)"
  apply (induct p, simp_all)
  subgoal for a p 
    apply (case_tac a, simp_all)
    done
  done
    
lemma SCRiD[rule_format,simp]: "singleCombinators p ⟶
                                singleCombinators(insertDeny p)"
  apply (induct p, simp_all)
  subgoal for a p 
    apply (case_tac a, simp_all)
    done
  done
    
lemma WP1rd[rule_format,simp]: 
  "wellformed_policy1_strong p ⟶ wellformed_policy1_strong (remdups p)"
  by (induct p, simp_all)
    
lemma ANDrd[rule_format,simp]: 
  "singleCombinators p ⟶ allNetsDistinct p ⟶ allNetsDistinct (remdups p)"
  apply (rule impI)+
  apply (rule_tac b = p in aNDSubset)
    apply simp_all
  done
    
lemma ANDiD[rule_format,simp]: 
  "allNetsDistinct p ⟶  allNetsDistinct (insertDeny p)"
  apply (induct p, simp_all)
   apply (simp add: allNetsDistinct_def)
  apply (auto intro: ANDConc)
  subgoal for a p 
    apply (case_tac "a",simp_all add: allNetsDistinct_def)
    done
  done
    
lemma mr_iD[rule_format]: 
  "wellformed_policy1_strong p  ⟶ matching_rule x p = matching_rule x (insertDeny p)"
  by (induct p, simp_all)
    
lemma WP1iD[rule_format,simp]: "wellformed_policy1_strong p ⟶
                                wellformed_policy1_strong (insertDeny p)"
  by (induct p, simp_all)
    
lemma DAiniD: "DenyAll ∈ set (insertDeny p)"
  apply (induct p, simp_all)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma p2lNmt: "policy2list p ≠ []"
  by (rule policy2list.induct, simp_all)
    
lemma AIL2[rule_format,simp]: 
  "all_in_list p l ⟶ all_in_list (removeShadowRules2 p) l"
  apply (induct_tac p, simp_all)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma SCConc: "singleCombinators x ⟹  singleCombinators y ⟹ singleCombinators (x@y)"
  apply (rule aux0_5)
  apply (metis aux0_0 aux0_4)
  done 	
    
lemma SCp2l: "singleCombinators (policy2list p)"
  by (induct_tac p) (auto intro: SCConc)
    
lemma subnetAux: "Dd ∩ A ≠ {} ⟹ A ⊆ B ⟹  Dd ∩ B ≠ {}"
  by auto
    
lemma soadisj: "x ∈ subnetsOfAdr a ⟹ y ∈ subnetsOfAdr a ⟹ ¬ netsDistinct x y"
  by(simp add: subnetsOfAdr_def netsDistinct_def,auto)
    
lemma not_member: "¬ member a (x⊕y) ⟹ ¬ member a x"
  by auto
    
lemma soadisj2: "(∀ a x y. x ∈ subnetsOfAdr a ∧ y ∈ subnetsOfAdr a ⟶ ¬ netsDistinct x y)"
  by (simp add: subnetsOfAdr_def netsDistinct_def, auto)
    
lemma ndFalse1: 
  "(∀a b c d. (a,b)∈A  ∧ (c,d)∈B ⟶ netsDistinct a c) ⟹
   ∃(a, b)∈A. a ∈ subnetsOfAdr D ⟹ 
   ∃(a, b)∈B. a ∈ subnetsOfAdr D ⟹ False"
  apply (auto simp: soadisj)
  using soadisj2 by blast
    
lemma ndFalse2: "(∀a b c d. (a,b)∈A  ∧ (c,d)∈B ⟶ netsDistinct b d) ⟹
                 ∃(a, b)∈A. b ∈ subnetsOfAdr D ⟹
                 ∃(a, b)∈B. b ∈ subnetsOfAdr D ⟹ False"
  apply (auto simp: soadisj)
  using soadisj2 by blast
    
lemma tndFalse: "(∀a b c d. (a,b)∈A  ∧ (c,d)∈B ⟶ twoNetsDistinct a b c d) ⟹
        ∃(a, b)∈A. a ∈ subnetsOfAdr (D::('a::adr)) ∧ b ∈ subnetsOfAdr (F::'a) ⟹ 
        ∃(a, b)∈B. a ∈ subnetsOfAdr D∧ b∈ subnetsOfAdr F 
    ⟹ False"
  apply (simp add: twoNetsDistinct_def)
  apply (auto simp: ndFalse1 ndFalse2)
  apply (metis soadisj)
  done
    
lemma sepnMT[rule_format]: "p ≠ [] ⟶ (separate p) ≠ []"
  by (induct p rule: separate.induct)  simp_all
    
lemma sepDA[rule_format]: "DenyAll ∉ set p ⟶ DenyAll ∉ set (separate p)"
  by (induct p rule: separate.induct)  simp_all
    
lemma setnMT: "set a = set b ⟹ a ≠ [] ⟹ b ≠ []"
  by auto
    
lemma sortnMT: "p ≠ [] ⟹ sort p l ≠ []"
  by (metis set_sort setnMT)
    
lemma idNMT[rule_format]: "p ≠ [] ⟶ insertDenies p ≠ []"
  apply (induct p, simp_all)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma OTNoTN[rule_format]: " OnlyTwoNets p ⟶ x ≠ DenyAll ⟶ x ∈ set p ⟶  onlyTwoNets x"
  apply (induct p, simp_all, rename_tac a p)
  apply (intro impI  conjI,  simp)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma first_isIn[rule_format]:  "¬ member DenyAll x ⟶ (first_srcNet x,first_destNet x) ∈ sdnets x"
  by (induct x,case_tac x, simp_all)
    
lemma sdnets2: 
  "∃a b. sdnets x = {(a, b), (b, a)} ⟹ ¬ member DenyAll x ⟹
   sdnets x = {(first_srcNet x, first_destNet x),  (first_destNet x, first_srcNet x)}"
proof -
  have * : "∃a b. sdnets x = {(a, b), (b, a)} ⟹ ¬ member DenyAll x 
            ⟹ (first_srcNet x, first_destNet x) ∈ sdnets x" 
    by (erule first_isIn) 
  show     "∃a b. sdnets x = {(a, b), (b, a)} ⟹ ¬ member DenyAll x ⟹
               sdnets x = {(first_srcNet x, first_destNet x),  (first_destNet x, first_srcNet x)}"
    using * by auto
qed
  
lemma alternativelistconc1[rule_format]: 
  "a ∈ set (net_list_aux [x]) ⟶  a ∈ set (net_list_aux [x,y])"
  by (induct x,simp_all)
    
lemma alternativelistconc2[rule_format]: 
  "a ∈ set (net_list_aux [x]) ⟶ a ∈ set (net_list_aux [y,x])"
  by (induct y, simp_all)
    
lemma noDA[rule_format]:
  "noDenyAll xs ⟶ s ∈ set xs ⟶ ¬ member DenyAll s"
  by (induct xs, simp_all)
    
lemma isInAlternativeList:
  "(aa ∈ set (net_list_aux [a]) ∨ aa ∈ set (net_list_aux p)) ⟹ aa ∈ set (net_list_aux (a # p))"
  by (case_tac a,simp_all)
    
lemma netlistaux: 
  "x ∈ set (net_list_aux (a # p))⟹  x ∈ set (net_list_aux ([a])) ∨ x ∈ set (net_list_aux (p))"
  apply (case_tac " x ∈ set (net_list_aux [a])", simp_all)
  apply (case_tac a, simp_all)
  done
    
lemma firstInNet[rule_format]: 
  "¬ member DenyAll a ⟶  first_destNet a ∈ set (net_list_aux (a # p))"
  apply (rule Combinators.induct, simp_all)
  apply (metis netlistaux)
  done
    
lemma firstInNeta[rule_format]: 
  "¬ member DenyAll a ⟶  first_srcNet a ∈ set (net_list_aux (a # p))"
  apply (rule Combinators.induct, simp_all)
  apply (metis netlistaux)
  done  
    
lemma disjComm: "disjSD_2 a b ⟹ disjSD_2 b a"
  apply (simp add: disjSD_2_def)
  apply (intro allI  impI  conjI)
  using tNDComm apply blast
  by (meson tNDComm twoNetsDistinct_def)
    
lemma disjSD2aux:
  "disjSD_2 a b ⟹ ¬ member DenyAll a ⟹ ¬ member DenyAll b ⟹
  disjSD_2 (DenyAllFromTo (first_srcNet a) (first_destNet a) ⊕
            DenyAllFromTo (first_destNet a) (first_srcNet a) ⊕ a)
           b"
  apply (drule disjComm,rule disjComm)
  apply (simp add: disjSD_2_def)
  using first_isIn by blast
    
lemma noDA1eq[rule_format]: "noDenyAll p ⟶ noDenyAll1 p"
  apply (induct p, simp,rename_tac a p)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma noDA1C[rule_format]: "noDenyAll1 (a#p) ⟶ noDenyAll1 p"
  by (case_tac a, simp_all,rule impI, rule noDA1eq, simp)+
    
lemma disjSD_2IDa: 
  "disjSD_2 x y ⟹
   ¬ member DenyAll x ⟹
   ¬ member DenyAll y ⟹ 
   a = first_srcNet x ⟹ 
   b = first_destNet x ⟹ 
   disjSD_2 (DenyAllFromTo a b ⊕ DenyAllFromTo b a ⊕ x) y"
  by(simp add:disjSD2aux)
    
lemma noDAID[rule_format]: "noDenyAll p ⟶ noDenyAll (insertDenies p)"
  apply (induct p, simp_all)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma isInIDo[rule_format]:  
  "noDenyAll p  ⟶ s ∈ set (insertDenies p) ⟶ 
   (∃! a. s = (DenyAllFromTo (first_srcNet a) (first_destNet a)) ⊕
   (DenyAllFromTo (first_destNet a) (first_srcNet a)) ⊕ a ∧ a ∈ set p)"
  apply (induct p, simp, rename_tac a p)
  subgoal for a p
    apply (case_tac "a = DenyAll", simp)
    apply (case_tac a, auto)
    done
  done
    
lemma id_aux1[rule_format]: "DenyAllFromTo (first_srcNet s) (first_destNet s) ⊕
      DenyAllFromTo (first_destNet s) (first_srcNet s) ⊕ s∈ set (insertDenies p)
    ⟶ s ∈ set p"
  apply (induct p, simp_all, rename_tac a p)
  subgoal for a p
    apply(case_tac a, simp_all)
    done
  done
    
lemma id_aux2:
  "noDenyAll p ⟹
   ∀s. s ∈ set p ⟶ disjSD_2 a s ⟹
   ¬ member DenyAll a ⟹
   DenyAllFromTo (first_srcNet s) (first_destNet s) ⊕ 
   DenyAllFromTo (first_destNet s) (first_srcNet s) ⊕ s ∈ set (insertDenies p) ⟹
   disjSD_2 a (DenyAllFromTo (first_srcNet s) (first_destNet s) ⊕ 
   DenyAllFromTo (first_destNet s) (first_srcNet s) ⊕ s)"
  by (metis disjComm disjSD2aux isInIDo noDA)
    
lemma id_aux4[rule_format]: 
  "noDenyAll p ⟹ ∀s. s ∈ set p ⟶ disjSD_2 a s ⟹ 
   s ∈ set (insertDenies p) ⟹ ¬ member DenyAll a ⟹ 
   disjSD_2 a s"
  apply (subgoal_tac "∃a. s =
          DenyAllFromTo (first_srcNet a) (first_destNet a) ⊕
          DenyAllFromTo (first_destNet a) (first_srcNet a) ⊕ a ∧
          a ∈ set p")
   apply (drule_tac Q = "disjSD_2 a s" in exE, simp_all, rule id_aux2, simp_all)
  using isInIDo by blast
    
lemma sepNetsID[rule_format]: 
  "noDenyAll1 p ⟶ separated p ⟶ separated (insertDenies p)"
  apply (induct p, simp)
  apply (rename_tac a p, auto)
  using noDA1C apply blast
  subgoal for a p
    apply (case_tac "a = DenyAll", auto)
     apply (simp add: disjSD_2_def)
    apply (case_tac a,auto)
      apply (rule disjSD_2IDa, simp_all, rule id_aux4, simp_all, metis noDA noDAID)+
    done
  done
    
lemma aNDDA[rule_format]: "allNetsDistinct p ⟶ allNetsDistinct(DenyAll#p)"
  by (case_tac p,auto simp: allNetsDistinct_def)
    
lemma OTNConc[rule_format]: "OnlyTwoNets (y # z) ⟶  OnlyTwoNets z"
  by (case_tac y, simp_all)
    
lemma first_bothNetsd: "¬ member DenyAll x ⟹ first_bothNet x = {first_srcNet x, first_destNet x}"
  by (induct x) simp_all
    
lemma bNaux:
  "¬ member DenyAll x ⟹ ¬ member DenyAll y ⟹
   first_bothNet x = first_bothNet y ⟹
   {first_srcNet x, first_destNet x} = {first_srcNet y, first_destNet y}"
  by (simp add: first_bothNetsd)
    
lemma setPair: "{a,b} = {a,d} ⟹ b = d"
  by (metis setPaireq)
    
lemma setPair1: "{a,b} = {d,a} ⟹ b = d"
  by (metis Un_empty_right Un_insert_right insert_absorb2 setPaireq)
    
lemma setPair4: "{a,b} = {c,d} ⟹ a ≠ c ⟹ a = d"
  by auto
    
lemma otnaux1: " {x, y, x, y} = {x,y}"
  by auto
        
lemma OTNIDaux4: "{x,y,x} = {y,x}"
  by auto
    
lemma setPair5: "{a,b} = {c,d} ⟹ a ≠ c ⟹ a = d"
  by auto
    
lemma otnaux: "   
  ⟦first_bothNet x = first_bothNet y; ¬ member DenyAll x; ¬ member DenyAll y; 
   onlyTwoNets y; onlyTwoNets x⟧ ⟹ 
   onlyTwoNets (x ⊕ y)"
  apply (simp add: onlyTwoNets_def)
  apply (subgoal_tac "{first_srcNet x, first_destNet x} =
                     {first_srcNet y, first_destNet y}")
   apply (case_tac "(∃a b. sdnets y = {(a, b)})")
    apply simp_all
    apply (case_tac "(∃a b. sdnets x = {(a, b)})")
     apply simp_all
     apply (subgoal_tac "sdnets x = {(first_srcNet x, first_destNet x)}")
      apply (subgoal_tac "sdnets y = {(first_srcNet y, first_destNet y)}")
       apply simp
       apply (case_tac "first_srcNet x = first_srcNet y")
        apply simp_all
        apply (rule disjI1)
        apply (rule setPair)
        apply simp
       apply (subgoal_tac "first_srcNet x = first_destNet y")
        apply simp
        apply (subgoal_tac "first_destNet x = first_srcNet y")
         apply simp
         apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI,simp)
        apply (rule setPair1)
        apply simp
       apply (rule setPair4)
        apply simp_all
      apply (metis first_isIn singletonE)
     apply (metis first_isIn singletonE)
    apply (subgoal_tac "sdnets x = {(first_srcNet x, first_destNet x),
                                    (first_destNet x, first_srcNet x)}")
     apply (subgoal_tac "sdnets y = {(first_srcNet y, first_destNet y)}")
      apply simp
      apply (case_tac "first_srcNet x = first_srcNet y")
       apply simp_all
       apply (subgoal_tac "first_destNet x = first_destNet y")
        apply simp
       apply (rule setPair)
       apply simp
      apply (subgoal_tac "first_srcNet x = first_destNet y")
       apply simp
       apply (subgoal_tac "first_destNet x = first_srcNet y")
        apply simp
        apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
        apply (metis OTNIDaux4 insert_commute )
       apply (rule setPair1)
       apply simp
      apply (rule setPair5)
       apply assumption
      apply simp
     apply (metis first_isIn singletonE)
    apply (rule sdnets2)
     apply simp_all
   apply (case_tac "(∃a b. sdnets x = {(a, b)})")
    apply simp_all
    apply (subgoal_tac "sdnets x = {(first_srcNet x, first_destNet x)}")
     apply (subgoal_tac "sdnets y = {(first_srcNet y, first_destNet y),
                                 (first_destNet y, first_srcNet y)}")
      apply simp
      apply (case_tac "first_srcNet x = first_srcNet y")
       apply simp_all
       apply (subgoal_tac "first_destNet x = first_destNet y")
        apply simp
        apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
        apply (metis OTNIDaux4 insert_commute )
       apply (rule setPair)
       apply simp
      apply (subgoal_tac "first_srcNet x = first_destNet y")
       apply simp
       apply (subgoal_tac "first_destNet x = first_srcNet y")
        apply simp
       apply (rule setPair1)
       apply simp
      apply (rule setPair4)
       apply assumption
      apply simp
     apply (rule sdnets2)
      apply simp
     apply simp
    apply (metis singletonE first_isIn)
   apply (subgoal_tac "sdnets x = {(first_srcNet x, first_destNet x),
                                 (first_destNet x, first_srcNet x)}")
    apply (subgoal_tac "sdnets y = {(first_srcNet y, first_destNet y),
                                (first_destNet y, first_srcNet y)}")
     apply simp
     apply (case_tac "first_srcNet x = first_srcNet y")
      apply simp_all
      apply (subgoal_tac "first_destNet x = first_destNet y")
       apply simp
       apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
       apply (rule otnaux1)
      apply (rule setPair)
      apply simp
     apply (subgoal_tac "first_srcNet x = first_destNet y")
      apply simp
      apply (subgoal_tac "first_destNet x = first_srcNet y")
       apply simp
       apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
       apply (metis OTNIDaux4 insert_commute)
      apply (rule setPair1)
      apply simp
     apply (rule setPair4)
      apply assumption
     apply simp
    apply (rule sdnets2,simp_all)+
  apply (rule bNaux, simp_all)
  done
    
lemma OTNSepaux: 
  "onlyTwoNets (a ⊕ y) ∧ OnlyTwoNets z ⟶ OnlyTwoNets (separate (a ⊕ y # z)) ⟹
    ¬ member DenyAll a ⟹  ¬ member DenyAll y ⟹
    noDenyAll z ⟹ onlyTwoNets a ⟹ OnlyTwoNets (y # z) ⟹ first_bothNet a = first_bothNet y ⟹ 
    OnlyTwoNets (separate (a ⊕ y # z))"
  apply (drule mp)
   apply simp_all
  apply (rule conjI)
   apply (rule otnaux)
       apply simp_all
   apply (rule_tac p = "(y # z)" in OTNoTN)
     apply simp_all
   apply (metis member.simps(2))
  apply (simp add: onlyTwoNets_def)
  apply (rule_tac y = y in OTNConc,simp)
  done
    
lemma OTNSEp[rule_format]: 
  "noDenyAll1 p ⟶ OnlyTwoNets p  ⟶  OnlyTwoNets (separate p)"
  apply (induct p rule: separate.induct)  
  by (simp_all add: OTNSepaux noDA1eq)
    
lemma nda[rule_format]: 
  "singleCombinators (a#p) ⟶ noDenyAll p ⟶ noDenyAll1 (a # p)"
  apply (induct p,simp_all)
   apply (case_tac a, simp_all)+
  done
    
lemma nDAcharn[rule_format]: "noDenyAll p = (∀ r ∈ set p. ¬ member DenyAll r)"
  by (induct p, simp_all)
    
lemma nDAeqSet: "set p = set s ⟹ noDenyAll p = noDenyAll s"
  by (simp add: nDAcharn)
    
lemma nDASCaux[rule_format]: 
  "DenyAll ∉ set p ⟶ singleCombinators p ⟶  r ∈ set p ⟶  ¬ member DenyAll r"
  apply (case_tac r, simp_all) 
  using SCnotConc by blast
    
    
lemma nDASC[rule_format]: 
  "wellformed_policy1 p ⟶ singleCombinators p ⟶  noDenyAll1 p"
  apply (induct p, simp_all)
  using nDASCaux nDAcharn nda singleCombinatorsConc by blast
    
lemma noDAAll[rule_format]: "noDenyAll p = (¬ memberP DenyAll p)"
  by (induct p) simp_all
    
lemma memberPsep[symmetric]: "memberP x p = memberP x (separate p)"
  by (induct p rule: separate.induct)  simp_all
    
lemma noDAsep[rule_format]: "noDenyAll p ⟹ noDenyAll (separate p)"
  by (simp add:noDAAll,subst memberPsep, simp)
    
lemma noDA1sep[rule_format]: "noDenyAll1 p ⟶ noDenyAll1 (separate p)"
  by (induct p rule:separate.induct, simp_all add: noDAsep)
    
lemma isInAlternativeLista: 
  "(aa ∈ set (net_list_aux [a]))⟹  aa ∈ set (net_list_aux (a # p))"
  by (case_tac a,auto)
    
lemma isInAlternativeListb: 
  "(aa ∈ set (net_list_aux p))⟹  aa ∈ set (net_list_aux (a # p))"
  by (case_tac a,simp_all)
    
lemma ANDSepaux: "allNetsDistinct (x # y # z) ⟹ allNetsDistinct (x ⊕ y # z)"
  apply (simp add: allNetsDistinct_def)
  apply (intro allI impI, rename_tac a b)
  subgoal for a b
    apply (drule_tac x = a in spec, drule_tac x = b in spec)
    by (meson isInAlternativeList)
  done
    
lemma netlistalternativeSeparateaux:
  "net_list_aux [y] @ net_list_aux z = net_list_aux (y # z)"
  by (case_tac y, simp_all)
    
lemma netlistalternativeSeparate: "net_list_aux p = net_list_aux (separate p)"
  by (induct p rule:separate.induct, simp_all) (simp_all add: netlistalternativeSeparateaux)
    
lemma  ANDSepaux2: 
  "allNetsDistinct(x#y#z) ⟹ allNetsDistinct(separate(y#z)) ⟹ allNetsDistinct(x#separate(y#z))"
  apply (simp add: allNetsDistinct_def)
  by (metis isInAlternativeList netlistalternativeSeparate netlistaux)
    
lemma ANDSep[rule_format]: "allNetsDistinct p ⟶ allNetsDistinct(separate p)"
  apply (induct p rule: separate.induct, simp_all) 
     apply (metis ANDConc aNDDA)
    apply (metis ANDConc ANDSepaux ANDSepaux2)
   apply (metis ANDConc ANDSepaux ANDSepaux2)
  apply (metis ANDConc ANDSepaux ANDSepaux2)
  done
    
lemma wp1_alternativesep[rule_format]: 
  "wellformed_policy1_strong p ⟶ wellformed_policy1_strong (separate p)"
  by (metis sepDA separate.simps(1) wellformed_policy1_strong.simps(2) wp1n_tl)
    
    
lemma noDAsort[rule_format]: "noDenyAll1 p ⟶ noDenyAll1 (sort p l)"
  apply (case_tac "p",simp_all)
  subgoal for a as
    apply (case_tac "a = DenyAll", auto) 
    using NormalisationGenericProofs.set_sort nDAeqSet apply blast
  proof -
    fix a::"('a,'b)Combinators" fix list 
    have * : "a ≠ DenyAll ⟹ noDenyAll1 (a # list) ⟹ noDenyAll (a#list)" by (case_tac a, simp_all)
    show "a ≠ DenyAll ⟹ noDenyAll1 (a # list) ⟹ noDenyAll1 (insort a (sort list l) l)"
      apply(cases "insort a (sort list l) l", simp_all)
      by (metis "*" NormalisationGenericProofs.set_insort NormalisationGenericProofs.set_sort 
          list.simps(15) nDAeqSet noDA1eq)
  qed
  done
  
lemma OTNSC[rule_format]: "singleCombinators p ⟶ OnlyTwoNets p"
  apply (induct p,simp_all)
  apply (rename_tac a p)
  apply (rule impI,drule mp)
   apply (erule singleCombinatorsConc)
  subgoal for a b
    apply (case_tac a, simp_all)
     apply (simp add: onlyTwoNets_def)+
    done
  done
    
lemma fMTaux: "¬ member DenyAll x ⟹ first_bothNet x ≠ {}"
  by (metis first_bothNetsd insert_commute insert_not_empty)
    
lemma fl2[rule_format]: "firstList (separate p) = firstList p"
  by (rule separate.induct) simp_all
    
    
lemma fl3[rule_format]: "NetsCollected p ⟶ (first_bothNet x ≠ firstList p ⟶
          (∀a∈set p. first_bothNet x ≠ first_bothNet a))⟶ NetsCollected (x#p)"
  by (induct p) simp_all
        
lemma sortedConc[rule_format]: " sorted (a # p) l ⟶  sorted p l"
  by (induct p) simp_all
    
lemma smalleraux2: 
  "{a,b} ∈ set l ⟹ {c,d} ∈ set l ⟹ {a,b} ≠ {c,d} ⟹ 
   smaller (DenyAllFromTo a b) (DenyAllFromTo c d) l ⟹ 
  ¬ smaller (DenyAllFromTo c d) (DenyAllFromTo a b) l"
  by (metis bothNet.simps(2) pos_noteq smaller.simps(5))
    
lemma smalleraux2a: 
  "{a,b} ∈ set l ⟹ {c,d} ∈ set l ⟹ {a,b} ≠ {c,d} ⟹ 
   smaller (DenyAllFromTo a b) (AllowPortFromTo c d p) l ⟹ 
  ¬ smaller (AllowPortFromTo c d p) (DenyAllFromTo a b) l"
  by (simp) (metis eq_imp_le pos_noteq)
    
lemma smalleraux2b: 
  "{a,b} ∈ set l ⟹ {c,d} ∈ set l ⟹ {a,b} ≠ {c,d} ⟹ y = DenyAllFromTo a b ⟹
   smaller (AllowPortFromTo  c d p) y l ⟹ 
  ¬ smaller y (AllowPortFromTo  c d p) l"
  by (simp) (metis eq_imp_le pos_noteq)
    
lemma smalleraux2c: 
  "{a,b} ∈ set l⟹{c,d}∈set l⟹{a,b} ≠ {c,d} ⟹ y = AllowPortFromTo a b q ⟹ 
    smaller (AllowPortFromTo  c d p) y l ⟹ ¬ smaller y (AllowPortFromTo  c d p) l"
  by (simp) (metis pos_noteq)
    
lemma smalleraux3: 
  assumes "x ∈ set l" and " y ∈ set l" and "x ≠ y" and "x = bothNet a" and "y = bothNet b"
    and "smaller a b l" and "singleCombinators [a]" and "singleCombinators [b]"  
  shows "¬ smaller b a l"
proof (cases a)
  case DenyAll thus ?thesis using assms by (case_tac b,simp_all)  
next
  case (DenyAllFromTo c d) thus ?thesis 
  proof (cases b)
    case DenyAll thus ?thesis using assms DenyAll DenyAllFromTo by simp
  next
    case (DenyAllFromTo e f) thus ?thesis using assms  DenyAllFromTo  
      by (metis DenyAllFromTo ‹a = DenyAllFromTo c d›  bothNet.simps(2) smalleraux2)
  next
    case (AllowPortFromTo e f g) thus ?thesis 
      using assms DenyAllFromTo AllowPortFromTo by simp (metis eq_imp_le pos_noteq)
  next
    case (Conc e f) thus ?thesis using assms by simp
  qed
next
  case (AllowPortFromTo c d p) thus ?thesis
  proof (cases b)
    case DenyAll thus ?thesis using assms AllowPortFromTo DenyAll by simp
  next
    case (DenyAllFromTo e f) thus ?thesis 
      using assms by simp (metis AllowPortFromTo DenyAllFromTo bothNet.simps(3) smalleraux2a)
  next
    case (AllowPortFromTo e f g) thus ?thesis 
      using assms by(simp)(metis AllowPortFromTo ‹a = AllowPortFromTo c d p› 
          bothNet.simps(3) smalleraux2c)
  next
    case (Conc e f) thus ?thesis using assms by simp
  qed
next
  case (Conc c d) thus ?thesis using assms by simp
qed
  
lemma smalleraux3a: 
  "a ≠ DenyAll ⟹ b ≠ DenyAll ⟹ in_list b l ⟹ in_list a l ⟹  
   bothNet a ≠ bothNet b ⟹ smaller a b l ⟹ singleCombinators [a] ⟹
    singleCombinators [b] ⟹ ¬ smaller b a l"
  apply (rule smalleraux3,simp_all)
   apply (case_tac a, simp_all)
  apply (case_tac b, simp_all)
  done
    
lemma posaux[rule_format]: "position a l < position b l ⟶ a ≠ b"
  by (induct l, simp_all)
    
lemma posaux6[rule_format]: 
  "a ∈ set l ⟶ b ∈ set l ⟶ a ≠ b ⟶ position a l ≠  position b l"
  by (induct l) (simp_all add: position_positive)
    
lemma notSmallerTransaux[rule_format]: 
  "x ≠ DenyAll ⟹ r ≠ DenyAll ⟹
  singleCombinators [x] ⟹  singleCombinators [y] ⟹  singleCombinators [r] ⟹
  ¬ smaller y x l ⟹ smaller x y l ⟹ smaller x r l ⟹ smaller y r l ⟹ 
   in_list x l ⟹ in_list y l ⟹ in_list r l ⟹ ¬ smaller r x l"
  by (metis order_trans)
    
lemma notSmallerTrans[rule_format]: 
  "x ≠ DenyAll ⟶ r ≠ DenyAll ⟶ singleCombinators (x#y#z) ⟶ 
  ¬ smaller y x l ⟶ sorted (x#y#z) l ⟶ r ∈ set z ⟶ 
  all_in_list (x#y#z) l ⟶ ¬ smaller r x l"
  apply (rule impI)+
  apply (rule notSmallerTransaux, simp_all)
        apply (metis singleCombinatorsConc singleCombinatorsStart)
       apply (metis SCSubset equalityE remdups.simps(2) set_remdups
                    singleCombinatorsConc singleCombinatorsStart)
      apply metis
     apply (metis sorted.simps(3) in_set_in_list singleCombinatorsConc
                  singleCombinatorsStart sortedConcStart sorted_is_smaller)
    apply (metis sorted_Cons all_in_list.simps(2)
                 singleCombinatorsConc)
   apply (metis,metis in_set_in_list)
  done
    
lemma  NCSaux1[rule_format]:
  "noDenyAll p ⟶ {x, y} ∈ set l ⟶  all_in_list p l⟶ singleCombinators p ⟶ 
  sorted (DenyAllFromTo x y # p) l ⟶ {x, y} ≠ firstList p ⟶
  DenyAllFromTo u v ∈ set p ⟶ {x, y} ≠ {u, v}"
proof (cases p)
  case Nil thus ?thesis by simp 
next
  case (Cons a list) 
  then show ?thesis apply simp
    apply (intro impI conjI)
     apply (metis bothNet.simps(2) first_bothNet.simps(3))
  proof -
    assume 1: "{x, y} ∈ set l" and 2: "in_list a l ∧ all_in_list list l"
      and 3 : "singleCombinators (a # list)"
      and 4 : "smaller (DenyAllFromTo x y) a l ∧ sorted (a # list) l"
      and 5 : "DenyAllFromTo u v ∈ set list"
      and 6 : "¬ member DenyAll a ∧ noDenyAll list"
    have * : "smaller ((DenyAllFromTo x y)::(('a,'b)Combinators)) (DenyAllFromTo u v) l" 
      apply (insert 1 2 3 4 5, rule_tac y = a in order_trans, simp_all)
      using in_set_in_list apply fastforce
      by (simp add: sorted_ConsA)
        
    have ** :"{x, y} ≠ first_bothNet a ⟹  
                       ¬ smaller ((DenyAllFromTo u v)::('a, 'b) Combinators) (DenyAllFromTo x y) l" 
      apply (insert 1 2 3 4 5 6, 
          rule_tac y = "a" and z = "list"  in  notSmallerTrans, 
          simp_all del: smaller.simps)
      apply (rule smalleraux3a,simp_all del: smaller.simps)
       apply (case_tac a, simp_all del: smaller.simps)
      by (metis aux0_0 first_bothNet.elims list.set_intros(1))
    show " {x, y} ≠ first_bothNet a ⟹  {x, y} ≠ {u, v}"
      using  3  "*" "**" by force
  qed
qed
  
lemma posaux3[rule_format]:"a ∈ set l ⟶ b ∈ set l ⟶ a ≠ b ⟶ position a l ≠ position b l"
  apply (induct l, auto)
  by(metis position_positive)+
    
lemma posaux4[rule_format]: 
  "singleCombinators [a] ⟶ a≠ DenyAll ⟶ b ≠ DenyAll ⟶ in_list a l ⟶in_list b l ⟶
    smaller a b  l⟶ x = (bothNet a) ⟶  y = (bothNet b) ⟶ 
    position x l <= position y l"
proof (cases a) 
  case DenyAll then show ?thesis by simp
next
  case (DenyAllFromTo c d) thus ?thesis
  proof (cases b)
    case DenyAll thus ?thesis by simp 
  next
    case (DenyAllFromTo e f) thus ?thesis using  DenyAllFromTo
      by (auto simp: eq_imp_le  ‹a = DenyAllFromTo c d›)
  next
    case (AllowPortFromTo e f p) thus ?thesis using ‹a = DenyAllFromTo c d› by simp 
  next
    case (Conc e f) thus ?thesis using Conc ‹a = DenyAllFromTo c d› by simp
  qed
next
  case (AllowPortFromTo c d p) thus ?thesis
  proof (cases b)
    case DenyAll thus ?thesis by simp 
  next
    case (DenyAllFromTo e f) thus ?thesis using AllowPortFromTo by simp 
  next
    case (AllowPortFromTo e f p2) thus ?thesis using ‹a = AllowPortFromTo c d p› by simp 
  next
    case (Conc e f) thus ?thesis using AllowPortFromTo by simp
  qed
next
  case (Conc c d) thus ?thesis by simp
qed
  
lemma  NCSaux2[rule_format]:
  "noDenyAll p ⟶ {a, b} ∈ set l ⟶ all_in_list p l ⟶singleCombinators p ⟶
   sorted (DenyAllFromTo a b # p) l ⟶ {a, b} ≠ firstList p ⟶
   AllowPortFromTo u v w ∈ set p ⟶  {a, b} ≠ {u, v}"
proof (cases p) 
  case Nil then show ?thesis by simp
next
  case (Cons aa list) 
  have *  : "{a, b} ∈ set l ⟹  in_list aa l ∧ all_in_list list l ⟹
                   singleCombinators (aa # list) ⟹  AllowPortFromTo u v w ∈ set list ⟹ 
                   smaller (DenyAllFromTo a b) aa l ∧ sorted (aa # list) l ⟹
                   smaller (DenyAllFromTo a b) (AllowPortFromTo u v w) l" 
    apply (rule_tac y = aa in order_trans,simp_all del: smaller.simps)
    using in_set_in_list apply fastforce
    using NormalisationGenericProofs.sorted_Cons all_in_list.simps(2) by blast                   
  have **: "AllowPortFromTo u v w ∈ set list ⟹
                    in_list aa l ⟹   all_in_list list l ⟹ 
                    in_list (AllowPortFromTo u v w) l"
    apply (rule_tac p = list in in_set_in_list)
     apply simp_all
    done
  assume  "p = aa # list" 
  then show ?thesis 
    apply simp
    apply (intro impI conjI,hypsubst, simp)
    apply (subgoal_tac "smaller (DenyAllFromTo a b) (AllowPortFromTo u v w) l")
     apply (subgoal_tac "¬ smaller (AllowPortFromTo u v w) (DenyAllFromTo a b) l")
      apply (rule_tac l = l in posaux) 
      apply (rule_tac y = "position (first_bothNet aa) l" in basic_trans_rules(22))
       apply (simp_all split: if_splits)
         apply (case_tac aa, simp_all)
    subgoal for x x'
      apply (case_tac "a = x ∧ b = x'", simp_all)
      apply (case_tac "a = x", simp_all)
       apply (simp add: order.not_eq_order_implies_strict posaux6)
      apply (simp add: order.not_eq_order_implies_strict posaux6)
      done
         apply (simp add: order.not_eq_order_implies_strict posaux6)  
        apply (rule basic_trans_rules(18))
         apply (rule_tac a = "DenyAllFromTo a b" and b = aa in posaux4, simp_all)
          apply (case_tac aa,simp_all)
         apply (case_tac aa, simp_all)
        apply (rule posaux3, simp_all)
        apply (case_tac aa, simp_all)
       apply (rule_tac a = aa and b = "AllowPortFromTo u v w" in posaux4, simp_all)
         apply (case_tac aa,simp_all)
        apply (rule_tac p = list in sorted_is_smaller, simp_all)
        apply (case_tac aa, simp_all)
       apply (case_tac aa, simp_all)
      apply (rule_tac a = aa and b = "AllowPortFromTo u v w" in posaux4, simp_all)
         apply (case_tac aa,simp_all)
    using ** apply auto[1]       
       apply (metis all_in_list.simps(2) sorted_Cons)
      apply (case_tac aa, simp_all)
     apply (metis ** bothNet.simps(3) in_list.simps(3) posaux6)
    using * by force  
qed
  
lemma  NCSaux3[rule_format]:
  "noDenyAll p ⟶ {a, b} ∈ set l ⟶  all_in_list p l ⟶singleCombinators p ⟶ 
  sorted (AllowPortFromTo a b w # p) l ⟶ {a, b} ≠ firstList p ⟶
  DenyAllFromTo u v ∈ set p ⟶ {a, b} ≠ {u, v}"
  apply (case_tac p, simp_all,intro impI conjI,hypsubst,simp)
proof -
  fix aa::"('a, 'b) Combinators" fix list::"('a, 'b) Combinators list"
  assume 1 : "¬ member DenyAll aa ∧ noDenyAll list" and 2: "{a, b} ∈ set l "
    and  3 : "in_list aa l ∧ all_in_list list l" and 4: "singleCombinators (aa # list)"
    and  5 : "smaller (AllowPortFromTo a b w) aa l ∧ sorted (aa # list) l"
    and  6 : "{a, b} ≠ first_bothNet aa" and 7: "DenyAllFromTo u v ∈ set list"
  have *: "¬ smaller (DenyAllFromTo u v) (AllowPortFromTo a b w) l"
    apply (insert 1 2 3 4 5 6 7, rule_tac y = aa and z = list in notSmallerTrans)
          apply (simp_all del: smaller.simps)
    apply (rule smalleraux3a,simp_all del: smaller.simps)
     apply (case_tac aa, simp_all del: smaller.simps)
    apply (case_tac aa, simp_all del: smaller.simps)
    done
  have **: "smaller (AllowPortFromTo a b w) (DenyAllFromTo u v) l"        
    apply (insert 1 2 3 4 5 6 7,rule_tac y = aa in order_trans,simp_all del: smaller.simps)
     apply (subgoal_tac "in_list (DenyAllFromTo u v) l", simp)
     apply (rule_tac p = list in in_set_in_list, simp_all)
    apply (rule_tac p = list in sorted_is_smaller,simp_all del: smaller.simps)
     apply (subgoal_tac "in_list (DenyAllFromTo u v) l", simp)
    apply (rule_tac p = list in in_set_in_list, simp_all)
    apply (erule singleCombinatorsConc)
    done
  show       "{a, b} ≠ {u, v}" by (insert * **, simp split: if_splits)
qed
  
lemma  NCSaux4[rule_format]:
  "noDenyAll p ⟶ {a, b} ∈ set l ⟶  all_in_list p l ⟶ singleCombinators p ⟶ 
 sorted (AllowPortFromTo a b c # p) l ⟶ {a, b} ≠ firstList p ⟶
 AllowPortFromTo u v w ∈ set p ⟶ {a, b} ≠ {u, v}"
  apply (cases p, simp_all)
  apply (intro impI conjI)
   apply (hypsubst,simp_all)
proof -
  fix aa::"('a, 'b) Combinators" fix list::"('a, 'b) Combinators list"
  assume 1 : "¬ member DenyAll aa ∧ noDenyAll list" and 2: "{a, b} ∈ set l "
    and  3 : "in_list aa l ∧ all_in_list list l" and 4: "singleCombinators (aa # list)"
    and  5 : "smaller (AllowPortFromTo a b c) aa l ∧ sorted (aa # list) l"
    and  6 : "{a, b} ≠ first_bothNet aa" and 7: "AllowPortFromTo u v w ∈ set list"
  have *: "¬ smaller (AllowPortFromTo u v w) (AllowPortFromTo a b c) l"
    apply (insert 1 2 3 4 5 6 7, rule_tac y = aa and z = list in notSmallerTrans)
          apply (simp_all del: smaller.simps)
    apply (rule smalleraux3a,simp_all del: smaller.simps)
     apply (case_tac aa, simp_all del: smaller.simps)
    apply (case_tac aa, simp_all del: smaller.simps)
    done
  have **: "smaller (AllowPortFromTo a b c) (AllowPortFromTo u v w) l"        
    apply(insert 1 2 3 4 5 6 7)
    apply (case_tac aa, simp_all del: smaller.simps)
     apply (rule_tac y = aa in order_trans,simp_all del: smaller.simps)
      apply (subgoal_tac "in_list (AllowPortFromTo u v w) l", simp)
      apply (rule_tac p = list in in_set_in_list, simp)
      apply (case_tac aa, simp_all del: smaller.simps)
     apply (rule_tac p = list in sorted_is_smaller,simp_all del: smaller.simps)
     apply (subgoal_tac "in_list (AllowPortFromTo u v w) l", simp)
     apply (rule_tac p = list in in_set_in_list, simp, simp)
    apply (rule_tac y = aa in order_trans,simp_all del: smaller.simps)
     apply (subgoal_tac "in_list (AllowPortFromTo u v w) l", simp)
    using in_set_in_list apply blast
    by (metis all_in_list.simps(2) bothNet.simps(3) in_list.simps(3) 
        singleCombinators.simps(5) sorted_ConsA)
  show       "{a, b} ≠ {u, v}"  by (insert * **, simp_all split: if_splits)
qed

lemma NetsCollectedSorted[rule_format]: 
  "noDenyAll1 p ⟶ all_in_list p l ⟶ singleCombinators p ⟶ sorted p l ⟶  NetsCollected p"
  apply (induct p)
   apply simp
  apply (intro impI,drule mp,erule noDA1C,drule mp,simp)
  apply (drule mp,erule singleCombinatorsConc)
  apply (drule mp,erule sortedConc) 
proof -
  fix a::" ('a, 'b) Combinators" fix p:: " ('a, 'b) Combinators list" 
  assume 1: "noDenyAll1 (a # p)"        and 2:"all_in_list (a # p) l" 
    and  3: "singleCombinators (a # p)" and 4: "sorted (a # p) l"  and   5: "NetsCollected p"
  show "NetsCollected (a # p)"
    apply(insert 1 2 3 4 5, rule fl3)
     apply(simp, rename_tac "aa")
  proof (cases a)
    case DenyAll
    fix aa::"('a, 'b) Combinators" 
    assume 6: "aa ∈ set p" 
    show "first_bothNet a ≠ first_bothNet aa"
      apply(insert 1 2 3 4 5 6 ‹a = DenyAll›, simp_all)
      using fMTaux noDA by blast
  next
    case (DenyAllFromTo x21 x22)
    fix aa::"('a, 'b) Combinators"
    assume 6: "first_bothNet a ≠ firstList p" and 7 :"aa ∈ set p"                
    show "first_bothNet a ≠ first_bothNet aa"
      apply(insert 1 2 3 4 5 6 7 ‹a = DenyAllFromTo x21 x22›)
      apply(case_tac aa, simp_all)
        apply (meson NCSaux1)
       apply (meson NCSaux2)
      using SCnotConc by auto[1]
  next
    case (AllowPortFromTo x31 x32 x33) 
    fix aa::"('a, 'b) Combinators" 
    assume 6: "first_bothNet a ≠ firstList p" and 7 :"aa ∈ set p"                
    show "first_bothNet a ≠ first_bothNet aa"
      apply(insert 1 2 3 4 6 7 ‹a = AllowPortFromTo x31 x32 x33›)
      apply(case_tac aa, simp_all)
        apply (meson NCSaux3)
       apply (meson NCSaux4)
      using SCnotConc by auto
  next
    case (Conc x41 x42) 
    fix aa::"('a, 'b) Combinators"
    show "first_bothNet a ≠ first_bothNet aa"
      by(insert 3 4   ‹a = x41 ⊕ x42›,simp)
  qed
qed
  
lemma NetsCollectedSort: "distinct p ⟹noDenyAll1 p ⟹ all_in_list p l ⟹
                          singleCombinators p ⟹ NetsCollected (sort p l)"
  apply (rule_tac l = l in NetsCollectedSorted,rule noDAsort, simp_all)
   apply (rule_tac b=p in all_in_listSubset)
  by (auto intro: sort_is_sorted)
    
lemma fBNsep[rule_format]: "(∀a∈set z. {b,c} ≠ first_bothNet a) ⟶
                           (∀a∈set (separate z). {b,c} ≠ first_bothNet a)"
  apply (induct z rule: separate.induct, simp)
  by (rule impI, simp)+
    
lemma fBNsep1[rule_format]: " (∀a∈set z. first_bothNet x ≠ first_bothNet a) ⟶
                        (∀a∈set (separate z). first_bothNet x ≠ first_bothNet a)"
  apply (induct z rule: separate.induct, simp)
  by (rule impI, simp)+
    
lemma NetsCollectedSepauxa:
  "{b,c}≠firstList z ⟹  noDenyAll1 z ⟹ ∀a∈set z. {b,c}≠first_bothNet a ⟹ NetsCollected z ⟹  
   NetsCollected (separate z) ⟹ {b, c} ≠ firstList (separate z) ⟹   a ∈ set (separate z) ⟹ 
   {b, c} ≠ first_bothNet a"
  by (rule fBNsep) simp_all
    
lemma NetsCollectedSepaux:
  "first_bothNet (x::('a,'b)Combinators) ≠ first_bothNet y ⟹ ¬ member DenyAll y ∧ noDenyAll z ⟹  
   (∀a∈set z. first_bothNet x ≠ first_bothNet a) ∧ NetsCollected (y # z) ⟹
   NetsCollected (separate (y # z)) ⟹ first_bothNet x ≠ firstList (separate (y # z)) ⟹
   a ∈ set (separate (y # z)) ⟹
   first_bothNet (x::('a,'b)Combinators) ≠ first_bothNet (a::('a,'b)Combinators)"
  by (rule fBNsep1) auto
    
    
lemma NetsCollectedSep[rule_format]: 
  "noDenyAll1 p ⟶ NetsCollected p ⟶  NetsCollected (separate p)"
proof (induct p rule: separate.induct, simp_all, goal_cases)
  fix x::"('a, 'b) Combinators list" 
  case 1 then show ?case
    by (metis fMTaux noDA noDA1eq noDAsep)
next
  fix v va y fix z::"('a, 'b) Combinators list"
  case 2 then show ?case 
    apply (intro conjI impI, simp)
     apply (metis NetsCollectedSepaux fl3 noDA1eq noDenyAll.simps(1))
    by (metis noDA1eq noDenyAll.simps(1))
next 
  fix v va vb y fix z::"('a, 'b) Combinators list"
  case 3 then show ?case 
    apply (intro conjI impI)
     apply (metis NetsCollectedSepaux fl3 noDA1eq noDenyAll.simps(1))
    by (metis noDA1eq noDenyAll.simps(1))
next 
  fix v va y fix z::"('a, 'b) Combinators list"
  case 4 then show ?case 
    by (metis NetsCollectedSepaux fl3 noDA1eq noDenyAll.simps(1))
qed
  
lemma OTNaux: 
  "onlyTwoNets a ⟹ ¬ member DenyAll a ⟹ (x,y) ∈ sdnets a ⟹ 
   (x = first_srcNet a ∧ y = first_destNet a) ∨   (x = first_destNet a ∧ y = first_srcNet a)"
  apply (case_tac "(x = first_srcNet a ∧ y = first_destNet a)",simp_all add: onlyTwoNets_def)
  apply (case_tac "(∃aa b. sdnets a = {(aa, b)})", simp_all)
   apply (subgoal_tac "sdnets a = {(first_srcNet a,first_destNet a)}", simp_all)
   apply (metis singletonE first_isIn)
  apply (subgoal_tac"sdnets a = {(first_srcNet a,first_destNet a),(first_destNet a, first_srcNet a)}")
  by(auto intro!: sdnets2)
    
lemma sdnets_charn: "onlyTwoNets a ⟹ ¬ member DenyAll a ⟹
sdnets a = {(first_srcNet a,first_destNet a)} ∨ 
sdnets a = {(first_srcNet a, first_destNet a),(first_destNet a, first_srcNet a)}"
  apply (case_tac "sdnets a = {(first_srcNet a, first_destNet a)}", simp_all add: onlyTwoNets_def)
  apply (case_tac "(∃aa b. sdnets a = {(aa, b)})", simp_all)
   apply (metis singletonE first_isIn)
  apply (subgoal_tac "sdnets a = {(first_srcNet a,first_destNet a),(first_destNet a,first_srcNet a)}")
  by( auto intro!: sdnets2)
    
lemma first_bothNet_charn[rule_format]: 
  "¬ member DenyAll a ⟶ first_bothNet a = {first_srcNet a, first_destNet a}"
  by (induct a) simp_all
    
    
lemma sdnets_noteq:
  "onlyTwoNets a ⟹ onlyTwoNets aa ⟹ first_bothNet a ≠ first_bothNet aa ⟹ 
   ¬ member DenyAll a ⟹ ¬ member DenyAll aa ⟹ sdnets a ≠ sdnets aa"
  apply (insert sdnets_charn [of a])
  apply (insert sdnets_charn [of aa])
  apply (insert first_bothNet_charn [of a])
  apply (insert first_bothNet_charn [of aa])
  by(metis OTNaux first_isIn insert_absorb2 insert_commute)

lemma fbn_noteq: 
  "onlyTwoNets a ⟹  onlyTwoNets aa ⟹  first_bothNet a ≠ first_bothNet aa ⟹
    ¬ member DenyAll a ⟹  ¬ member DenyAll aa ⟹  allNetsDistinct [a, aa] ⟹
    first_srcNet a ≠ first_srcNet aa ∨ first_srcNet a ≠ first_destNet aa ∨ 
    first_destNet a ≠ first_srcNet aa ∨ first_destNet a ≠ first_destNet aa" 
  apply (insert sdnets_charn [of a])
  apply (insert sdnets_charn [of aa])
  by (metis first_bothNet_charn)    
    
lemma NCisSD2aux: 
  assumes 1: "onlyTwoNets a" and 2 : "onlyTwoNets aa" and 3 : "first_bothNet a ≠ first_bothNet aa"
    and   4: "¬ member DenyAll a" and 5: "¬ member DenyAll aa" and 6:" allNetsDistinct [a, aa]"
  shows   "disjSD_2 a aa"
  apply (insert 1 2 3 4 5 6) 
  apply (simp add: disjSD_2_def)
  apply (intro allI impI)
  apply (insert sdnets_charn [of a]  sdnets_charn [of aa], simp)
  apply (insert sdnets_noteq [of a aa]  fbn_noteq [of a aa], simp)
  apply (simp add: allNetsDistinct_def twoNetsDistinct_def)
proof -
  fix ab b c d
  assume 7: "∀ab b. ab≠b ∧ ab∈set(net_list_aux[a,aa]) ∧ b∈set(net_list_aux [a,aa]) ⟶ netsDistinct ab b"
    and    8: "(ab, b) ∈ sdnets a ∧ (c, d) ∈ sdnets aa "
    and    9: "sdnets a = {(first_srcNet a, first_destNet a)} ∨
              sdnets a = {(first_srcNet a, first_destNet a), (first_destNet a, first_srcNet a)} "
    and   10: "sdnets aa = {(first_srcNet aa, first_destNet aa)} ∨
              sdnets aa = {(first_srcNet aa, first_destNet aa), (first_destNet aa, first_srcNet aa)}"
    and   11: "sdnets a ≠ sdnets aa "
    and   12: "first_destNet a = first_srcNet aa ⟶ first_srcNet a = first_destNet aa ⟶ 
              first_destNet aa ≠ first_srcNet aa"
  show      "(netsDistinct ab c ∨ netsDistinct b d) ∧ (netsDistinct ab d ∨ netsDistinct b c)"
    
  proof (rule conjI)
    show "netsDistinct ab c ∨ netsDistinct b d"         
      apply(insert       7 8 9 10 11 12)
      apply (cases "sdnets a = {(first_srcNet a, first_destNet a)}")
       apply (cases "sdnets aa = {(first_srcNet aa, first_destNet aa)}", simp_all)
        apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
       apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
        apply (case_tac "(first_srcNet a) ≠ (first_srcNet aa)",simp_all)
         apply (metis 4 5 firstInNeta alternativelistconc2)
        apply (subgoal_tac "first_destNet a ≠ first_destNet aa") 
         apply (metis 4 5 firstInNet alternativelistconc2)
        apply (metis 3 4 5 first_bothNetsd)
       apply (case_tac "(first_destNet aa) ≠ (first_srcNet a)",simp_all)
        apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
       apply (case_tac "first_destNet aa ≠ first_destNet a",simp_all)
        apply (subgoal_tac "first_srcNet aa ≠ first_destNet a")
         apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
        apply (metis 3 4 5 first_bothNetsd insert_commute)
       apply (metis 5 firstInNeta firstInNet alternativelistconc2)
      apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
       apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)", simp_all)
        apply (case_tac "(first_srcNet a) ≠ (first_srcNet aa)",simp_all)
         apply (metis 4 5 firstInNeta alternativelistconc2)
        apply (subgoal_tac "first_destNet a ≠ first_destNet aa")
         apply (metis  4 5 firstInNet alternativelistconc2)
        apply (metis 3 4 5 first_bothNetsd )
       apply (case_tac "(first_destNet aa) ≠ (first_srcNet a)",simp_all)
        apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
       apply (case_tac "first_destNet aa ≠ first_destNet a", simp)
        apply (subgoal_tac "first_srcNet aa ≠ first_destNet a")
         apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
        apply (metis 3 4 5 first_bothNetsd insert_commute)
       apply (metis)        
    proof - 
      assume  14 : "(ab = first_srcNet a ∧ b = first_destNet a ∨ ab = first_destNet a ∧ b = first_srcNet a) ∧ (c, d) ∈ sdnets aa "
        and     15 : "sdnets a = {(first_srcNet a, first_destNet a), (first_destNet a, first_srcNet a)} "
        and     16 : "sdnets aa = {(first_srcNet aa, first_destNet aa)} ∨ sdnets aa = {(first_srcNet aa, first_destNet aa), (first_destNet aa, first_srcNet aa)} "
        and     17 : "{(first_srcNet a, first_destNet a), (first_destNet a, first_srcNet a)} ≠ sdnets aa "
        and     18 : "first_destNet a = first_srcNet aa ⟶ first_srcNet a = first_destNet aa ⟶ first_destNet aa ≠ first_srcNet aa "
        and     19 : "first_destNet a ≠ first_srcNet a"
        and     20 : "c = first_srcNet aa ⟶ d ≠ first_destNet aa" 
      show " netsDistinct ab c ∨ netsDistinct b d"
        apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)",simp_all)
         apply (case_tac "c = first_srcNet aa", simp_all)
          apply (metis 2 5 14 20 OTNaux)
         apply (subgoal_tac "c = first_destNet aa", simp)
          apply (subgoal_tac "d = first_srcNet aa", simp)
           apply (case_tac "(first_srcNet a) ≠ (first_destNet aa)",simp_all)
            apply (metis 4 5 7 firstInNeta firstInNet alternativelistconc2)
           apply (subgoal_tac "first_destNet a ≠ first_srcNet aa")
            apply (metis 4 5 7 firstInNeta firstInNet alternativelistconc2)
           apply (metis 3 4 5 first_bothNetsd insert_commute)
          apply (metis 2 5 14 OTNaux)
         apply (metis 2 5 14 OTNaux)
        apply (case_tac "c = first_srcNet aa", simp_all)
         apply (metis 2 5 14 20 OTNaux)
        apply (subgoal_tac "c = first_destNet aa", simp)
         apply (subgoal_tac "d = first_srcNet aa", simp)
          apply (case_tac "(first_destNet a) ≠ (first_destNet aa)",simp_all)
           apply (metis 4 5 7 14 firstInNet alternativelistconc2)
          apply (subgoal_tac "first_srcNet a ≠ first_srcNet aa")
           apply (metis 4 5 7 14 firstInNeta alternativelistconc2)
          apply (metis 3 4 5 first_bothNetsd  insert_commute)
         apply (metis 2 5 14 OTNaux)
        apply (metis 2 5 14 OTNaux)
        done
    qed
  next 
    show "netsDistinct ab d ∨ netsDistinct b c"   
      apply (insert 1 2 3 4 5 6 7 8 9 10 11 12)           
      apply (cases "sdnets a = {(first_srcNet a, first_destNet a)}")
       apply (cases "sdnets aa = {(first_srcNet aa, first_destNet aa)}", simp_all)
        apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
        apply (case_tac "(first_srcNet a) ≠ (first_destNet aa)", simp_all)
         apply (metis firstInNeta firstInNet alternativelistconc2)
        apply (subgoal_tac "first_destNet a ≠ first_srcNet aa")
         apply (metis firstInNeta firstInNet alternativelistconc2)
        apply (metis first_bothNetsd insert_commute)
       apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
        apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)", simp_all)
        apply (case_tac "(first_destNet a) ≠ (first_srcNet aa)",simp_all)
         apply (metis firstInNeta firstInNet alternativelistconc2)
        apply (subgoal_tac "first_srcNet a ≠ first_destNet aa")
         apply (metis firstInNeta firstInNet alternativelistconc2)
        apply (metis first_bothNetsd insert_commute)
       apply (case_tac "(first_srcNet aa) ≠ (first_srcNet a)",simp_all)
        apply (metis firstInNeta alternativelistconc2)
       apply (case_tac "first_destNet aa ≠ first_destNet a",simp_all)
        apply (metis firstInNet alternativelistconc2)
       apply (metis first_bothNetsd)    
    proof - 
      assume 13:" ∀ab b. ab ≠ b ∧ ab∈set(net_list_aux[a,aa]) ∧ b ∈ set(net_list_aux[a,aa])
                             ⟶ netsDistinct ab b "
        and    14 : "(ab = first_srcNet a ∧ b = first_destNet a ∨ 
                        ab = first_destNet a ∧ b = first_srcNet a) ∧ (c, d) ∈ sdnets aa "
        and    15 : " sdnets a = {(first_srcNet a, first_destNet a), 
                                    (first_destNet a, first_srcNet a)} "
        and    16 : " sdnets aa = {(first_srcNet aa, first_destNet aa)} ∨ 
                        sdnets aa = {(first_srcNet aa, first_destNet aa), 
                                     (first_destNet aa, first_srcNet aa)} "
        and    17 : " {(first_srcNet a, first_destNet a), 
                         (first_destNet a, first_srcNet a)} ≠ sdnets aa "
      show   "first_destNet a ≠ first_srcNet a ⟹ netsDistinct ab d ∨ netsDistinct b c"
        apply (insert 1 2 3 4 5 6   13 14 15 16 17)
        apply (cases "sdnets aa = {(first_srcNet aa, first_destNet aa)}", simp_all)
         apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
         apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)", simp_all)
          apply (case_tac "(first_destNet a) ≠ (first_srcNet aa)",simp_all)
           apply (metis firstInNeta firstInNet alternativelistconc2)
          apply (subgoal_tac "first_srcNet a ≠ first_destNet aa")
           apply (metis firstInNeta firstInNet alternativelistconc2)
          apply (metis first_bothNetsd insert_commute)
         apply (case_tac "(first_srcNet aa) ≠ (first_srcNet a)",simp_all)
          apply (metis firstInNeta alternativelistconc2)
         apply (case_tac "first_destNet aa ≠ first_destNet a",simp_all)
          apply (metis firstInNet alternativelistconc2)
         apply (metis first_bothNetsd)
      proof -
        assume 20: "{(first_srcNet a, first_destNet a), (first_destNet a, first_srcNet a)} ≠
                        {(first_srcNet aa, first_destNet aa), (first_destNet aa, first_srcNet aa)}"
          and    21: "first_destNet a ≠ first_srcNet a"
        show       "netsDistinct ab d ∨ netsDistinct b c"
          apply (case_tac "(c = first_srcNet aa ∧ d = first_destNet aa)", simp_all)
           apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)", simp_all)
            apply (case_tac "(first_destNet a) ≠ (first_srcNet aa)", simp_all)
             apply (metis 4 5 7 firstInNeta firstInNet alternativelistconc2)
            apply (subgoal_tac "first_srcNet a ≠ first_destNet aa")
             apply (metis 4 5 7 firstInNeta firstInNet alternativelistconc2)
            apply (metis 20 insert_commute)
           apply (case_tac "(first_srcNet aa) ≠ (first_srcNet a)", simp_all)
            apply (metis 4 5 13 14  firstInNeta alternativelistconc2)
           apply (case_tac "first_destNet aa ≠ first_destNet a", simp_all)
            apply (metis 4 5 13 14  firstInNet alternativelistconc2)
           apply (case_tac "(ab = first_srcNet a ∧ b = first_destNet a)", simp_all)
           apply (case_tac "(first_destNet a) ≠ (first_srcNet aa)", simp_all)
            apply (metis  20)
          apply (subgoal_tac "first_srcNet a ≠ first_srcNet aa")
            apply (metis  20)
           apply (metis 21)
          apply (case_tac "(first_srcNet aa) ≠ (first_destNet a)")
           apply (metis (no_types, lifting)  2 3 4 5 7 14 OTNaux 
              firstInNet firstInNeta first_bothNetsd isInAlternativeList) 
          by (metis 2 4 5 7 20 14 OTNaux doubleton_eq_iff firstInNet 
              firstInNeta isInAlternativeList)
      qed
    qed
  qed
qed
  
lemma ANDaux3[rule_format]: 
  "y ∈ set xs ⟶ a ∈ set (net_list_aux [y]) ⟶  a ∈ set (net_list_aux xs)"
  by (induct xs) (simp_all add: isInAlternativeList)
    
lemma ANDaux2: 
  "allNetsDistinct (x # xs) ⟹ y ∈ set xs ⟹ allNetsDistinct [x,y]"
  apply (simp add: allNetsDistinct_def)
  by (meson ANDaux3 isInAlternativeList netlistaux)
    
lemma NCisSD2[rule_format]: 
  "¬ member DenyAll a     ⟹  OnlyTwoNets (a#p) ⟹ 
  NetsCollected2 (a # p) ⟹ NetsCollected (a#p) ⟹
  noDenyAll ( p) ⟹ allNetsDistinct (a # p) ⟹ s ∈ set p ⟹
  disjSD_2 a s"
  by (metis ANDaux2 FWNormalisationCore.member.simps(2) NCisSD2aux NetsCollected.simps(1) 
      NetsCollected2.simps(1) OTNConc OTNoTN empty_iff empty_set list.set_intros(1) noDA)
    
    
lemma separatedNC[rule_format]: 
  "OnlyTwoNets p ⟶ NetsCollected2 p ⟶ NetsCollected p ⟶ noDenyAll1 p ⟶  
   allNetsDistinct p  ⟶ separated p"
proof (induct p, simp_all, rename_tac a b, case_tac "a = DenyAll", simp_all, goal_cases)
  fix a fix p::"('a set set, 'b) Combinators list"
  show  "OnlyTwoNets p ⟶ NetsCollected2 p ⟶ NetsCollected p ⟶ noDenyAll1 p ⟶ 
          allNetsDistinct p ⟶ separated p ⟹ a ≠ DenyAll ⟹  OnlyTwoNets (a # p) ⟶
          first_bothNet a ≠ firstList p ∧ NetsCollected2 p ⟶
          (∀aa∈set p. first_bothNet a ≠ first_bothNet aa) ∧ NetsCollected p ⟶
          noDenyAll1 (a # p) ⟶ allNetsDistinct (a # p) ⟶ (∀s. s ∈ set p ⟶ 
          disjSD_2 a s) ∧ separated p"
    apply (intro impI,drule mp, erule OTNConc,drule mp)
     apply (case_tac p, simp_all) 
    apply (drule mp,erule noDA1C, intro conjI  allI impI  NCisSD2, simp_all)
      apply (case_tac a, simp_all)
     apply (case_tac a, simp_all)
    using ANDConc by auto
next
  fix a::"('a set set,'b) Combinators " fix p ::"('a set set,'b) Combinators list"
  show  "OnlyTwoNets p ⟶ NetsCollected2 p ⟶ NetsCollected p ⟶ noDenyAll1 p ⟶ 
          allNetsDistinct p ⟶ separated p ⟹  a = DenyAll ⟹  OnlyTwoNets p ⟶
          {}≠firstList p ∧ NetsCollected2 p ⟶ (∀a∈set p. {}≠first_bothNet a)∧NetsCollected p ⟶
          noDenyAll p ⟶ allNetsDistinct (DenyAll # p) ⟶ 
          (∀s. s ∈ set p ⟶ disjSD_2 DenyAll s) ∧ separated p"
    by (simp add: ANDConc disjSD_2_def noDA1eq)
qed
  
lemma separatedNC'[rule_format]: 
  "OnlyTwoNets p ⟶ NetsCollected2 p ⟶ NetsCollected p ⟶ noDenyAll1 p ⟶  
   allNetsDistinct p  ⟶ separated p"
proof (induct p)
  case Nil show ?case by simp
next
  case (Cons a p) then show ?case
    apply simp
  proof (cases "a = DenyAll") print_cases 
    case True 
    then show "OnlyTwoNets (a # p) ⟶  first_bothNet a ≠ firstList p ∧ NetsCollected2 p ⟶
                      (∀aa∈set p. first_bothNet a ≠ first_bothNet aa) ∧ NetsCollected p ⟶
                      noDenyAll1 (a # p) ⟶ allNetsDistinct (a # p) ⟶ 
                      (∀s. s ∈ set p ⟶ disjSD_2 a s) ∧ separated p"
      apply(insert Cons.hyps ‹a = DenyAll›)
      apply (intro impI,drule mp, erule OTNConc,drule mp)
       apply (case_tac p, simp_all) 
      apply (case_tac a, simp_all)
      apply (case_tac a, simp_all)
      by (simp add: ANDConc disjSD_2_def noDA1eq)
  next
    case False 
    then show "OnlyTwoNets (a # p) ⟶  first_bothNet a ≠ firstList p ∧ NetsCollected2 p ⟶
                      (∀aa∈set p. first_bothNet a ≠ first_bothNet aa) ∧ NetsCollected p ⟶
                      noDenyAll1 (a # p) ⟶ allNetsDistinct (a # p) ⟶ (∀s. s ∈ set p ⟶ 
                      disjSD_2 a s) ∧ separated p" 
      apply(insert Cons.hyps ‹a ≠ DenyAll›)
      by (metis NetsCollected.simps(1) NetsCollected2.simps(1) separated.simps(1) separatedNC)
  qed
qed
  
lemma NC2Sep[rule_format]: "noDenyAll1 p ⟶ NetsCollected2 (separate p)"
proof (induct p rule: separate.induct, simp_all, goal_cases)
  fix x :: "('a, 'b) Combinators list"
  case 1 then show ?case
    by (metis fMTaux firstList.simps(1) fl2 noDA1eq noDenyAll.elims(2) separate.simps(5))
next
  fix v va fix y::" ('a, 'b) Combinators" fix z
  case 2 then show ?case   
    by (simp add: fl2 noDA1eq)
next
  fix v va vb fix y::" ('a, 'b) Combinators" fix z
  case 3 then show ?case
    by (simp add: fl2 noDA1eq)
next
  fix v va fix y::" ('a, 'b) Combinators" fix z
  case 4 then show ?case
    by (simp add: fl2 noDA1eq)         
qed         
  
lemma separatedSep[rule_format]: 
  "OnlyTwoNets p ⟶ NetsCollected2 p   ⟶ NetsCollected p ⟶ 
   noDenyAll1 p  ⟶ allNetsDistinct p  ⟶ separated (separate p)"
  by (simp add: ANDSep NC2Sep NetsCollectedSep OTNSEp noDA1sep separatedNC)
    
    
lemma rADnMT[rule_format]: "p ≠ []  ⟶ removeAllDuplicates p ≠ []"
  by (induct p) simp_all
        
lemma remDupsNMT[rule_format]: "p ≠ [] ⟶ remdups p ≠ []"
  by (metis remdups_eq_nil_iff) 
    
lemma sets_distinct1: "(n::int) ≠ m ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto
    
lemma sets_distinct2: "(m::int) ≠ n ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto
    
lemma sets_distinct5: "(n::int) < m ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto
    
lemma sets_distinct6: "(m::int) < n ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
  by auto
end