Theory Iface

section‹Network Interfaces›
theory Iface
imports "HOL-Library.Char_ord" (*WARNING: importing char ord*)
begin

text‹Network interfaces, e.g. \texttt{eth0}, \texttt{wlan1}, ...

iptables supports wildcard matching, e.g. \texttt{eth+} will match \texttt{eth}, \texttt{eth1}, \texttt{ethFOO}, ...
The character `+' is only a wildcard if it appears at the end.
›

datatype iface = Iface (iface_sel: "string")  ― ‹no negation supported, but wildcards›


text‹Just a normal lexicographical ordering on the interface strings. Used only for optimizing code.
     WARNING: not a semantic ordering.›
(*We cannot use List_lexord because it clashed with the Word_Lib imported ordering!*)
instantiation iface :: linorder
begin
  function (sequential) less_eq_iface :: "iface ⇒ iface ⇒ bool" where
    "(Iface []) ≤ (Iface _) ⟷ True" |
    "(Iface _) ≤ (Iface []) ⟷ False" |
    "(Iface (a#as)) ≤ (Iface (b#bs)) ⟷ (if a = b then Iface as ≤ Iface bs else a ≤ b)"
   by(pat_completeness) auto
  termination "less_eq :: iface ⇒ _ ⇒ bool"
    apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
    apply(rule wf_measure, unfold in_measure comp_def)
    apply(simp)
    done
  
  lemma Iface_less_eq_empty: "Iface x ≤ Iface [] ⟹ x = []"
    by(induction "Iface x" "Iface []" rule: less_eq_iface.induct) auto
  lemma less_eq_empty: "Iface [] ≤ q"
    by(induction "Iface []" q rule: less_eq_iface.induct) auto
  lemma iface_cons_less_eq_i:
    "Iface (b # bs) ≤ i ⟹ ∃ q qs. i=Iface (q#qs) ∧ (b < q ∨ (Iface bs) ≤ (Iface qs))"
    apply(induction "Iface (b # bs)" i rule: less_eq_iface.induct)
     apply(simp_all split: if_split_asm)
    apply(clarify)
    apply(simp)
    done

  function (sequential) less_iface :: "iface ⇒ iface ⇒ bool" where
    "(Iface []) < (Iface []) ⟷ False" |
    "(Iface []) < (Iface _) ⟷ True" |
    "(Iface _) < (Iface []) ⟷ False" |
    "(Iface (a#as)) < (Iface (b#bs)) ⟷ (if a = b then Iface as < Iface bs else a < b)"
   by(pat_completeness) auto
  termination "less :: iface ⇒ _ ⇒ bool"
    apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
    apply(rule wf_measure, unfold in_measure comp_def)
    apply(simp)
    done
instance
  proof
    fix n m :: iface
    show "n < m ⟷ n ≤ m ∧ ¬ m ≤ n"
      proof(induction rule: less_iface.induct)
      case 4 thus ?case by simp fastforce
      qed(simp+)
  next
    fix n :: iface have "n = m ⟹ n ≤ m" for m
      by(induction n m rule: less_eq_iface.induct) simp+
    thus "n ≤ n" by simp
  next
    fix n m :: iface
    show "n ≤ m ⟹ m ≤ n ⟹ n = m"
      proof(induction n m rule: less_eq_iface.induct)
      case 1 thus ?case using Iface_less_eq_empty by blast
      next
      case 3 thus ?case by (simp split: if_split_asm)
      qed(simp)+
  next
    fix n m q :: iface show "n ≤ m ⟹ m ≤ q ⟹ n ≤ q" 
      proof(induction n q arbitrary: m rule: less_eq_iface.induct)
      case 1 thus ?case by simp
      next
      case 2 thus ?case
        apply simp
        apply(drule iface_cons_less_eq_i)
        apply(elim exE conjE disjE)
         apply(simp; fail)
        by fastforce
      next
      case 3 thus ?case
        apply simp
        apply(frule iface_cons_less_eq_i)
         by(auto split: if_split_asm)
      qed
  next
    fix n m :: iface show "n ≤ m ∨ m ≤ n"
      apply(induction n m rule: less_eq_iface.induct)
        apply(simp_all)
      by fastforce
  qed
end

definition ifaceAny :: iface where
  "ifaceAny ≡ Iface ''+''"
(* there is no IfaceFalse, proof below *)

text‹If the interface name ends in a ``+'', then any interface which begins with this name will match.
  (man iptables)

Here is how iptables handles this wildcard on my system.
A packet for the loopback interface \texttt{lo} is matched by the following expressions
  ▪ lo
  ▪ lo+
  ▪ l+
  ▪ +

It is not matched by the following expressions
  ▪ lo++
  ▪ lo+++
  ▪ lo1+
  ▪ lo1

By the way: \texttt{Warning: weird characters in interface ` ' ('/' and ' ' are not allowed by the kernel).}
However, happy snowman and shell colors are fine.
›


context
begin
  subsection‹Helpers for the interface name (@{typ string})›
    (*Do not use outside this thy! Type is really misleading.*)
    text‹
      argument 1: interface as in firewall rule - Wildcard support
      argument 2: interface a packet came from - No wildcard support›
    fun internal_iface_name_match :: "string ⇒ string ⇒ bool" where
      "internal_iface_name_match []     []         ⟷ True" |
      "internal_iface_name_match (i#is) []         ⟷ (i = CHR ''+'' ∧ is = [])" |
      "internal_iface_name_match []     (_#_)      ⟷ False" |
      "internal_iface_name_match (i#is) (p_i#p_is) ⟷ (if (i = CHR ''+'' ∧ is = []) then True else (
            (p_i = i) ∧ internal_iface_name_match is p_is
      ))"
    
    (*<*)
    ― ‹Examples›
      lemma "internal_iface_name_match ''lo'' ''lo''" by eval
      lemma "internal_iface_name_match ''lo+'' ''lo''" by eval
      lemma "internal_iface_name_match ''l+'' ''lo''" by eval
      lemma "internal_iface_name_match ''+'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo++'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo+++'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo1+'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo1'' ''lo''" by eval
      text‹The wildcard interface name›
      lemma "internal_iface_name_match ''+'' ''''" by eval (*>*)
  
  
    fun iface_name_is_wildcard :: "string ⇒ bool" where
      "iface_name_is_wildcard [] ⟷ False" |
      "iface_name_is_wildcard [s] ⟷ s = CHR ''+''" |
      "iface_name_is_wildcard (_#ss) ⟷ iface_name_is_wildcard ss"
    private lemma iface_name_is_wildcard_alt: "iface_name_is_wildcard eth ⟷ eth ≠ [] ∧ last eth = CHR ''+''"
      proof(induction eth rule: iface_name_is_wildcard.induct)
      qed(simp_all)
    private lemma iface_name_is_wildcard_alt': "iface_name_is_wildcard eth ⟷ eth ≠ [] ∧ hd (rev eth) = CHR ''+''"
      unfolding iface_name_is_wildcard_alt by (simp add: hd_rev)
    private lemma iface_name_is_wildcard_fst: "iface_name_is_wildcard (i # is) ⟹ is ≠ [] ⟹ iface_name_is_wildcard is"
      by(simp add: iface_name_is_wildcard_alt)
  
    private fun internal_iface_name_to_set :: "string ⇒ string set" where
      "internal_iface_name_to_set i = (if ¬ iface_name_is_wildcard i
        then
          {i}
        else
          {(butlast i)@cs | cs. True})"
    private lemma "{(butlast i)@cs | cs. True} = (λs. (butlast i)@s) ` (UNIV::string set)" by fastforce
    private lemma internal_iface_name_to_set: "internal_iface_name_match i p_iface ⟷ p_iface ∈ internal_iface_name_to_set i"
      proof(induction i p_iface rule: internal_iface_name_match.induct)
      case 4 thus ?case
        apply(simp)
        apply(safe)
               apply(simp_all add: iface_name_is_wildcard_fst)
         apply (metis (full_types) iface_name_is_wildcard.simps(3) list.exhaust)
        by (metis append_butlast_last_id)
      qed(simp_all)
    private lemma internal_iface_name_to_set2: "internal_iface_name_to_set ifce = {i. internal_iface_name_match ifce i}"
      by (simp add: internal_iface_name_to_set)
      
  
    private lemma internal_iface_name_match_refl: "internal_iface_name_match i i"
     proof -
     { fix i j
       have "i=j ⟹ internal_iface_name_match i j"
         by(induction i j rule: internal_iface_name_match.induct)(simp_all)
     } thus ?thesis by simp
     qed
  
  subsection‹Matching›
    fun match_iface :: "iface ⇒ string ⇒ bool" where
      "match_iface (Iface i) p_iface ⟷ internal_iface_name_match i p_iface"
    
    ― ‹Examples›
      lemma "  match_iface (Iface ''lo'')    ''lo''"
            "  match_iface (Iface ''lo+'')   ''lo''"
            "  match_iface (Iface ''l+'')    ''lo''"
            "  match_iface (Iface ''+'')     ''lo''"
            "¬ match_iface (Iface ''lo++'')  ''lo''"
            "¬ match_iface (Iface ''lo+++'') ''lo''"
            "¬ match_iface (Iface ''lo1+'')  ''lo''"
            "¬ match_iface (Iface ''lo1'')   ''lo''"
            "  match_iface (Iface ''+'')     ''eth0''"
            "  match_iface (Iface ''+'')     ''eth0''"
            "  match_iface (Iface ''eth+'')  ''eth0''"
            "¬ match_iface (Iface ''lo+'')   ''eth0''"
            "  match_iface (Iface ''lo+'')   ''loX''"
            "¬ match_iface (Iface '''')      ''loX''"
            (*<*)by eval+(*>*)
  
    lemma match_ifaceAny: "match_iface ifaceAny i"
      by(cases i, simp_all add: ifaceAny_def)
    lemma match_IfaceFalse: "¬(∃ IfaceFalse. (∀i. ¬ match_iface IfaceFalse i))"
      apply(simp)
      apply(intro allI, rename_tac IfaceFalse)
      apply(case_tac IfaceFalse, rename_tac name)
      apply(rule_tac x="name" in exI)
      by(simp add: internal_iface_name_match_refl)
      

    ― ‹@{const match_iface} explained by the individual cases›
    lemma match_iface_case_nowildcard: "¬ iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ i = p_i"
      proof(induction i p_i rule: internal_iface_name_match.induct)
      qed(auto simp add: iface_name_is_wildcard_alt split: if_split_asm)
    lemma match_iface_case_wildcard_prefix:
      "iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ butlast i = take (length i - 1) p_i"
      apply(induction i p_i rule: internal_iface_name_match.induct)
         apply(simp; fail)
        apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
       apply(simp; fail)
      apply(simp)
      apply(intro conjI)
       apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
      apply(simp add: iface_name_is_wildcard_fst)
      by (metis One_nat_def length_0_conv list.sel(1) list.sel(3) take_Cons')
    lemma match_iface_case_wildcard_length: "iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟹ length p_i ≥ (length i - 1)"
      proof(induction i p_i rule: internal_iface_name_match.induct)
      qed(simp_all add: iface_name_is_wildcard_alt split: if_split_asm)
    corollary match_iface_case_wildcard:
      "iface_name_is_wildcard i ⟹ match_iface (Iface i) p_i ⟷ butlast i = take (length i - 1) p_i ∧ length p_i ≥ (length i - 1)"
      using match_iface_case_wildcard_length match_iface_case_wildcard_prefix by blast
  
  
    lemma match_iface_set: "match_iface (Iface i) p_iface ⟷ p_iface ∈ internal_iface_name_to_set i"
      using internal_iface_name_to_set by simp
  
    private definition internal_iface_name_wildcard_longest :: "string ⇒ string ⇒ string option" where
      "internal_iface_name_wildcard_longest i1 i2 = (
        if 
          take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2
        then
          Some (if length i1 ≤ length i2 then i2 else i1)
        else
          None)"
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''eth3+'' = Some ''eth3+''" by eval
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''e+'' = Some ''eth+''" by eval
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''lo'' = None" by eval
  
    private  lemma internal_iface_name_wildcard_longest_commute: "iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹ 
      internal_iface_name_wildcard_longest i1 i2 = internal_iface_name_wildcard_longest i2 i1"
      by (cases i1 rule: rev_cases; cases i2 rule: rev_cases)
        (simp_all add: internal_iface_name_wildcard_longest_def iface_name_is_wildcard_alt)

    private  lemma internal_iface_name_wildcard_longest_refl: "internal_iface_name_wildcard_longest i i = Some i"
      by(simp add: internal_iface_name_wildcard_longest_def)
  
  
    private lemma internal_iface_name_wildcard_longest_correct:
      "iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹ 
       match_iface (Iface i1) p_i ∧ match_iface (Iface i2) p_i ⟷
       (case internal_iface_name_wildcard_longest i1 i2 of None ⇒ False | Some x ⇒ match_iface (Iface x) p_i)"
    proof -
      assume assm1: "iface_name_is_wildcard i1"
         and assm2: "iface_name_is_wildcard i2"
      { assume assm3: "internal_iface_name_wildcard_longest i1 i2 = None" 
        have "¬ (internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i)"
        proof -
          from match_iface_case_wildcard_prefix[OF assm1] have 1:
            "internal_iface_name_match i1 p_i = (take (length i1 - 1) i1 = take (length i1 - 1) p_i)" by(simp add: butlast_conv_take)
          from match_iface_case_wildcard_prefix[OF assm2] have 2:
            "internal_iface_name_match i2 p_i = (take (length i2 - 1) i2 = take (length i2 - 1) p_i)" by(simp add: butlast_conv_take)
          from assm3 have 3: "take (min (length i1 - 1) (length i2 - 1)) i1 ≠ take (min (length i1 - 1) (length i2 - 1)) i2"
           by(simp add: internal_iface_name_wildcard_longest_def split: if_split_asm)
          from 3 show ?thesis using 1 2 min.commute take_take by metis
        qed
      } note internal_iface_name_wildcard_longest_correct_None=this
    
      { fix X
        assume assm3: "internal_iface_name_wildcard_longest i1 i2 = Some X"
        have "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i"
        proof -
          from assm3 have assm3': "take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2"
            unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
      
          { fix i1 i2
            assume iw1: "iface_name_is_wildcard i1" and iw2: "iface_name_is_wildcard i2" and len: "length i1 ≤ length i2" and
                   take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2"
            from len have len': "length i1 - 1 ≤ length i2 - 1" by fastforce
            { fix x::string
             from len' have "take (length i1 - 1) x = take (length i1 - 1) (take (length i2 - 1) x)" by(simp add: min_def)
            } note takei1=this
        
            { fix m::nat and n::nat and a::string and b c
              have "m ≤ n ⟹ take n a = take n b ⟹ take m a = take m c ⟹ take m c = take m b" by (metis min_absorb1 take_take)
            } note takesmaller=this
        
            from match_iface_case_wildcard_prefix[OF iw1, simplified] have 1:
                "internal_iface_name_match i1 p_i ⟷ take (length i1 - 1) i1 = take (length i1 - 1) p_i" by(simp add: butlast_conv_take)
            also have "… ⟷ take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i)" using takei1 by simp
            finally have  "internal_iface_name_match i1 p_i = (take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i))" .
            from match_iface_case_wildcard_prefix[OF iw2, simplified] have 2:
                "internal_iface_name_match i2 p_i ⟷ take (length i2 - 1) i2 = take (length i2 - 1) p_i" by(simp add: butlast_conv_take)
        
            have "internal_iface_name_match i2 p_i ⟹ internal_iface_name_match i1 p_i"
              unfolding 1 2 
              apply(rule takesmaller[of "(length i1 - 1)" "(length i2 - 1)" i2 p_i])
                using len' apply (simp; fail)
               apply (simp; fail)
              using take_i1i2 by simp
          } note longer_iface_imp_shorter=this
        
         show ?thesis
          proof(cases "length i1 ≤ length i2")
          case True
            with assm3 have "X = i2" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
            from True assm3' have take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2" by linarith
            from longer_iface_imp_shorter[OF assm1 assm2 True take_i1i2] ‹X = i2›
            show "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i" by fastforce
          next
          case False
            with assm3 have "X = i1" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
            from False assm3' have take_i1i2: "take (length i2 - 1) i2 = take (length i2 - 1) i1" by (metis min_def min_diff)
            from longer_iface_imp_shorter[OF assm2 assm1 _ take_i1i2] False ‹X = i1›
            show "(internal_iface_name_match i1 p_i ∧ internal_iface_name_match i2 p_i) ⟷ internal_iface_name_match X p_i" by auto
          qed
        qed
      } note internal_iface_name_wildcard_longest_correct_Some=this
    
      from internal_iface_name_wildcard_longest_correct_None internal_iface_name_wildcard_longest_correct_Some show ?thesis
        by(simp split:option.split)
    qed
  
    fun iface_conjunct :: "iface ⇒ iface ⇒ iface option" where
      "iface_conjunct (Iface i1) (Iface i2) = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
        (True,  True) ⇒ map_option Iface  (internal_iface_name_wildcard_longest i1 i2) |
        (True,  False) ⇒ (if match_iface (Iface i1) i2 then Some (Iface i2) else None) |
        (False, True) ⇒ (if match_iface (Iface i2) i1 then Some (Iface i1) else None) |
        (False, False) ⇒ (if i1 = i2 then Some (Iface i1) else None))"

    
    lemma iface_conjunct_Some: "iface_conjunct i1 i2 = Some x ⟹ 
          match_iface x p_i ⟷ match_iface i1 p_i ∧ match_iface i2 p_i"
      apply(cases i1, cases i2, rename_tac i1name i2name)
      apply(simp)
      apply(case_tac "iface_name_is_wildcard i1name")
       apply(case_tac [!] "iface_name_is_wildcard i2name")
         apply(simp_all)
         using internal_iface_name_wildcard_longest_correct apply auto[1]
        apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
       apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
      by (metis match_iface.simps option.distinct(1) option.inject)
    lemma iface_conjunct_None: "iface_conjunct i1 i2 = None ⟹ ¬ (match_iface i1 p_i ∧ match_iface i2 p_i)"
      apply(cases i1, cases i2, rename_tac i1name i2name)
      apply(simp split: bool.split_asm if_split_asm)
         using internal_iface_name_wildcard_longest_correct apply fastforce
        apply (metis match_iface.simps match_iface_case_nowildcard)+
      done
    lemma iface_conjunct: "match_iface i1 p_i ∧ match_iface i2 p_i ⟷
           (case iface_conjunct i1 i2 of None ⇒ False | Some x ⇒ match_iface x p_i)"
    apply(simp split: option.split)
    by(blast dest: iface_conjunct_Some iface_conjunct_None)

    lemma match_iface_refl: "match_iface (Iface x) x" by (simp add: internal_iface_name_match_refl)
    lemma match_iface_eqI: assumes "x = Iface y" shows "match_iface x y"
      unfolding assms using match_iface_refl .


    lemma iface_conjunct_ifaceAny: "iface_conjunct ifaceAny i = Some i"
      apply(simp add: ifaceAny_def)
      apply(case_tac i, rename_tac iname)
      apply(simp)
      apply(case_tac "iface_name_is_wildcard iname")
       apply(simp add: internal_iface_name_wildcard_longest_def iface_name_is_wildcard_alt Suc_leI; fail)
      apply(simp)
      using internal_iface_name_match.elims(3) by fastforce
       
    lemma iface_conjunct_commute: "iface_conjunct i1 i2 = iface_conjunct i2 i1"
    apply(induction i1 i2 rule: iface_conjunct.induct)
    apply(rename_tac i1 i2, simp)
    apply(case_tac "iface_name_is_wildcard i1")
     apply(case_tac [!] "iface_name_is_wildcard i2")
       apply(simp_all)
    by (simp add: internal_iface_name_wildcard_longest_commute)


    private definition internal_iface_name_subset :: "string ⇒ string ⇒ bool" where
      "internal_iface_name_subset i1 i2 = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
        (True,  True) ⇒ length i1 ≥ length i2 ∧ take ((length i2) - 1) i1 = butlast i2 |
        (True,  False) ⇒ False |
        (False, True) ⇒ take (length i2 - 1) i1 = butlast i2 |
        (False, False) ⇒ i1 = i2
        )"

    private lemma butlast_take_length_helper:
      fixes x ::"char list"
      assumes a1: "length i2 ≤ length i1"
      assumes a2: "take (length i2 - Suc 0) i1 = butlast i2"
      assumes a3: "butlast i1 = take (length i1 - Suc 0) x"
      shows "butlast i2 = take (length i2 - Suc 0) x"
    proof - (*sledgehammer spass Isar proof*)
      have f4: "List.gen_length 0 i2 ≤ List.gen_length 0 i1"
        using a1 by (simp add: length_code)
      have f5: "⋀cs. List.gen_length 0 (cs::char list) - Suc 0 = List.gen_length 0 (tl cs)"
        by (metis (no_types) One_nat_def length_code length_tl)
      obtain nn :: "(nat ⇒ nat) ⇒ nat" where
        "⋀f. ¬ f (nn f) ≤ f (Suc (nn f)) ∨ f (List.gen_length 0 i2) ≤ f (List.gen_length 0 i1)"
        using f4 by (meson lift_Suc_mono_le)
      hence "¬ nn (λn. n - Suc 0) - Suc 0 ≤ nn (λn. n - Suc 0) ∨ List.gen_length 0 (tl i2) ≤ List.gen_length 0 (tl i1)"
        using f5 by (metis (lifting) diff_Suc_Suc diff_zero)
      hence f6: "min (List.gen_length 0 (tl i2)) (List.gen_length 0 (tl i1)) = List.gen_length 0 (tl i2)"
        using diff_le_self min.absorb1 by blast
      { assume "take (List.gen_length 0 (tl i2)) i1 ≠ take (List.gen_length 0 (tl i2)) x"
        have "List.gen_length 0 (tl i2) = 0 ∨ take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
          using f6 f5 a3 by (metis (lifting) One_nat_def butlast_conv_take length_code take_take)
        hence "take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
          by force }
      thus "butlast i2 = take (length i2 - Suc 0) x"
        using f5 a2 by (metis (full_types) length_code)
    qed

    private lemma internal_iface_name_subset: "internal_iface_name_subset i1 i2 ⟷ 
        {i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i}"
      unfolding internal_iface_name_subset_def
      proof(cases "iface_name_is_wildcard i1", case_tac [!] "iface_name_is_wildcard i2", simp_all)
        assume a1: "iface_name_is_wildcard i1"
        assume a2: "iface_name_is_wildcard i2"
        show "(length i2 ≤ length i1 ∧ take (length i2 - Suc 0) i1 = butlast i2) ⟷
            ({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})" (is "?l ⟷ ?r")
          proof(rule iffI)
            assume ?l with a1 a2 show ?r
             apply(clarify, rename_tac x)
             apply(drule_tac p_i=x in match_iface_case_wildcard_prefix)+
             apply(simp)
             using butlast_take_length_helper by blast
          next
            assume ?r hence r': "internal_iface_name_to_set i1 ⊆ internal_iface_name_to_set i2 "
              apply -
              apply(subst(asm) internal_iface_name_to_set2[symmetric])+
              by assumption
            have hlp1: "⋀i1 i2. {x. ∃cs. x = i1 @ cs} ⊆ {x. ∃cs. x = i2 @ cs} ⟹ length i2 ≤ length i1"
              apply(simp add: Set.Collect_mono_iff)
              by force
            have hlp2: "⋀i1 i2. {x. ∃cs. x = i1 @ cs} ⊆ {x. ∃cs. x = i2 @ cs} ⟹ take (length i2) i1 = i2"
              apply(simp add: Set.Collect_mono_iff)
              by force
            from r' a1 a2 show ?l
              apply(simp add: internal_iface_name_to_set)
              apply(safe)
               apply(drule hlp1)
               apply(simp)
               apply (metis One_nat_def Suc_pred diff_Suc_eq_diff_pred diff_is_0_eq iface_name_is_wildcard.simps(1) length_greater_0_conv)
              apply(drule hlp2)
              apply(simp)
              by (metis One_nat_def butlast_conv_take length_butlast length_take take_take)
          qed
      next
      show "iface_name_is_wildcard i1 ⟹ ¬ iface_name_is_wildcard i2 ⟹
            ¬ Collect (internal_iface_name_match i1) ⊆ Collect (internal_iface_name_match i2)"
        using internal_iface_name_match_refl match_iface_case_nowildcard by fastforce
      next
      show "¬ iface_name_is_wildcard i1 ⟹ iface_name_is_wildcard i2 ⟹
            (take (length i2 - Suc 0) i1 = butlast i2) ⟷ ({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})"
        using match_iface_case_nowildcard match_iface_case_wildcard_prefix by force
      next
      show " ¬ iface_name_is_wildcard i1 ⟹ ¬ iface_name_is_wildcard i2 ⟹
           (i1 = i2) ⟷ ({i. internal_iface_name_match i1 i} ⊆ {i. internal_iface_name_match i2 i})"
        using match_iface_case_nowildcard  by force
      qed
      
       
    
    definition iface_subset :: "iface ⇒ iface ⇒ bool" where
      "iface_subset i1 i2 ⟷ internal_iface_name_subset (iface_sel i1) (iface_sel i2)"
    
    lemma iface_subset: "iface_subset i1 i2 ⟷ {i. match_iface i1 i} ⊆ {i. match_iface i2 i}"
      unfolding iface_subset_def
      apply(cases i1, cases i2)
      by(simp add: internal_iface_name_subset)


    definition iface_is_wildcard :: "iface ⇒ bool" where
      "iface_is_wildcard ifce ≡ iface_name_is_wildcard (iface_sel ifce)"
   
    lemma iface_is_wildcard_ifaceAny: "iface_is_wildcard ifaceAny"
      by(simp add: iface_is_wildcard_def ifaceAny_def)




  subsection‹Enumerating Interfaces›
    private definition all_chars :: "char list" where
      "all_chars ≡ Enum.enum"
    private lemma all_chars: "set all_chars = (UNIV::char set)"
       by(simp add: all_chars_def enum_UNIV)
  
    text‹we can compute this, but its horribly inefficient!›
    (*valid chars in an interface are NOT limited to the printable ones!*)
    private lemma strings_of_length_n: "set (List.n_lists n all_chars) = {s::string. length s = n}"
      apply(induction n)
       apply(simp; fail)
      apply(simp add: all_chars)
      apply(safe)
       apply(simp; fail)
      apply(simp)
      apply(rename_tac n x)
      apply(rule_tac x="drop 1 x" in exI)
      apply(simp)
      apply(case_tac x)
       apply(simp_all)
      done
  
    text‹Non-wildacrd interfaces of length @{term n}›
    private definition non_wildcard_ifaces :: "nat ⇒ string list" where
     "non_wildcard_ifaces n ≡ filter (λi. ¬ iface_name_is_wildcard i) (List.n_lists n all_chars)"

    text‹Example: (any number higher than zero are probably too inefficient)›
    private lemma "non_wildcard_ifaces 0 = ['''']" by eval

    private lemma non_wildcard_ifaces: "set (non_wildcard_ifaces n) = {s::string. length s = n ∧ ¬ iface_name_is_wildcard s}"
      using strings_of_length_n non_wildcard_ifaces_def by auto
  
    private lemma "(⋃ i ∈ set (non_wildcard_ifaces n). internal_iface_name_to_set i) = {s::string. length s = n ∧ ¬ iface_name_is_wildcard s}"
     by(simp add: non_wildcard_ifaces)
  
    text‹Non-wildacrd interfaces up to length @{term n}›
    private fun non_wildcard_ifaces_upto :: "nat ⇒ string list" where
      "non_wildcard_ifaces_upto 0 = [[]]" |
      "non_wildcard_ifaces_upto (Suc n) = (non_wildcard_ifaces (Suc n)) @ non_wildcard_ifaces_upto n"
    private lemma non_wildcard_ifaces_upto: "set (non_wildcard_ifaces_upto n) = {s::string. length s ≤ n ∧ ¬ iface_name_is_wildcard s}"
      apply(induction n)
       apply fastforce
      using non_wildcard_ifaces by fastforce


  subsection‹Negating Interfaces›
    private lemma inv_iface_name_set: "- (internal_iface_name_to_set i) = (
      if iface_name_is_wildcard i
      then
        {c |c. length c < length (butlast i)} ∪ {c @ cs |c cs. length c = length (butlast i) ∧ c ≠ butlast i}
      else
        {c | c. length c < length i} ∪ {c@cs | c cs. length c ≥ length i ∧ c ≠ i}
    )"
    proof -
      { fix i::string
        have inv_i_wildcard: "- {i@cs | cs. True} = {c | c. length c < length i} ∪ {c@cs | c cs. length c = length i ∧ c ≠ i}"
          apply(rule Set.equalityI)
           prefer 2
           apply(safe)[1]
            apply(simp;fail)
           apply(simp;fail)
          apply(simp)
          apply(rule Compl_anti_mono[where B="{i @ cs |cs. True}" and A="- ({c | c. length c < length i} ∪ {c@cs | c cs. length c = length i ∧ c ≠ i})", simplified])
          apply(safe)
          apply(simp)
          apply(case_tac "(length i) = length x")
           apply(erule_tac x=x in allE, simp)
          apply(erule_tac x="take (length i) x" in allE)
          apply(simp add: min_def)
          by (metis append_take_drop_id)
      } note inv_i_wildcard=this
      { fix i::string
        have inv_i_nowildcard: "- {i::string} = {c | c. length c < length i} ∪ {c@cs | c cs. length c ≥ length i ∧ c ≠ i}"
        proof -
          have x: "{c | c. length c = length i ∧ c ≠ i}  ∪ {c | c. length c > length i} = {c@cs | c cs. length c ≥ length i ∧ c ≠ i}"
            apply(safe)
              apply force+
            done
          have "- {i::string} = {c |c . c ≠ i}"
           by(safe, simp)
          also have "… = {c | c. length c < length i} ∪ {c | c. length c = length i ∧ c ≠ i}  ∪ {c | c. length c > length i}"
            by(auto)
          finally show ?thesis using x by auto
        qed
      } note inv_i_nowildcard=this
    show ?thesis
      proof(cases "iface_name_is_wildcard i")
      case True with inv_i_wildcard show ?thesis by force
      next
      case False with inv_i_nowildcard show ?thesis by force
      qed
    qed

    text‹Negating is really not intuitive.
          The Interface @{term "''et''"} is in the negated set of @{term "''eth+''"}.
          And the Interface @{term "''et+''"} is also in this set! This is because @{term "''+''"}
          is a normal interface character and not a wildcard here!
          In contrast, the set described by @{term "''et+''"} (with @{term "''+''"} a wildcard)
          is not a subset of the previously negated set.›
    lemma "''et'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "''et+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "''+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "¬ {i. match_iface (Iface ''et+'') i} ⊆ - (internal_iface_name_to_set ''eth+'')" by force

    text‹Because @{term "''+''"} can appear as interface wildcard and normal interface character,
          we cannot take negate an @{term "Iface i"} such that we get back @{typ "iface list"} which
          describe the negated interface.›
    lemma "''+'' ∈ - (internal_iface_name_to_set ''eth+'')" by(simp)




  fun compress_pos_interfaces :: "iface list ⇒ iface option" where
    "compress_pos_interfaces [] = Some ifaceAny" |
    "compress_pos_interfaces [i] = Some i" |
    "compress_pos_interfaces (i1#i2#is) = (case iface_conjunct i1 i2 of None ⇒ None | Some i ⇒ compress_pos_interfaces (i#is))"

  lemma compress_pos_interfaces_Some: "compress_pos_interfaces ifces = Some ifce ⟹ 
          match_iface ifce p_i ⟷ (∀ i∈ set ifces. match_iface i p_i)"
  proof(induction ifces rule: compress_pos_interfaces.induct)
    case 1 thus ?case by (simp add: match_ifaceAny)
    next
    case 2 thus ?case by simp
    next
    case (3 i1 i2) thus ?case
    apply(simp)
    apply(case_tac "iface_conjunct i1 i2")
     apply(simp; fail)
    apply(simp)
    using iface_conjunct_Some by presburger
  qed

  lemma compress_pos_interfaces_None: "compress_pos_interfaces ifces = None ⟹ 
          ¬ (∀ i∈ set ifces. match_iface i p_i)"
  proof(induction ifces rule: compress_pos_interfaces.induct)
    case 1 thus ?case by (simp add: match_ifaceAny)
    next
    case 2 thus ?case by simp
    next
    case (3 i1 i2) thus ?case
      apply(cases "iface_conjunct i1 i2", simp_all)
       apply (blast dest: iface_conjunct_None)
      by (blast dest: iface_conjunct_Some)
  qed
end

end