Session IP_Addresses

Theory NumberWang_IPv4

theory NumberWang_IPv4
imports Main
  "HOL-Library.Word"
begin

lemma zdiv_mult_self:
  m  0  (a + m * n) div m = a div m + n
  for a m n :: int
  by simp

section‹Helper Lemmas for Low-Level Operations on Machine Words›
text‹Needed for IPv4 Syntax›

lemma mod256: "((d::nat) + 256 * c + 65536 * b + 16777216 * a) mod 256 = d mod 256"
proof -
  from mod_mult_self2[where a="d + 256 * c + 65536 * b" and b="256" and c="65536 * a"] have 
    "(d + 256 * c + 65536 * b + 256 * 65536 * a) mod 256 = (d + 256 * c + 65536 * b) mod 256"
    by simp
  also have "  = (d + 256 * c) mod 256"
    using mod_mult_self2[where a="d + 256 * c" and b="256" and c="256 * b"] by simp
  also have " = d mod 256" using mod_mult_self2 by blast
  finally show ?thesis by simp
qed

lemma div65536: assumes "a < 256" "b < 256" "c < 256" "d < 256" 
    shows "nat ((int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 65536 mod 256) = b"
proof -
  from zdiv_mult_self[where a="int d + int (256 * c) + int (65536 * b)" and m=65536 and n="256 * (int a)"] have
    "(int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 65536 =
     ((int d + int (256 * c) + int (65536 * b)) div 65536) + 256 * int a" by linarith
  also from zdiv_mult_self[where a="int d + int (256 * c)" and m="65536" and n="int b"] have
    " = (int d + int (256 * c)) div 65536 + int b + 256 * int a" by linarith
  also from assms have " = int b + 256 * int a" by simp
  finally have helper:
    "(int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 65536 = int b + 256 * int a" .
  with assms show ?thesis
    by simp
qed

lemma div256: assumes "a < 256" "b < 256" "c < 256" "d < 256" 
  shows "nat ((int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 256 mod 256) = c"
proof -
  from zdiv_mult_self[where a="int d + int (256 * c) + int (65536 * b)" and m=256 and n="65536 * (int a)"] have
    "(int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 256 =
     ((int d + int (256 * c) + int (65536 * b)) div 256) + 65536 * int a" by linarith
  also from zdiv_mult_self[where a="int d + int (256 * c)" and m="256" and n="256 * int b"] have
    " = (int d + int (256 * c)) div 256 + 256 * int b + 65536 * int a" by linarith
  also from zdiv_mult_self[where a="int d" and m="256" and n="int c"] have
    " = (int d) div 256 + int c + 256 * int b + 65536 * int a" by linarith
  also from assms have " = int c + 256 * int b + 65536 * int a" by simp
  finally have helper1: "(int d + int (256 * c) + int (65536 * b) + int (16777216 * a)) div 256 =
                          int c + 256 * int b + 65536 * int a" .
  
  from mod_mult_self2[where a="int c + 256 * int b" and c="256 * int a" and b=256] have 
    "(int c + 256 * int b + 65536 * int a) mod 256 = (int c + 256 * int b) mod 256" by simp
  also have " = int c mod 256" using mod_mult_self2[where a="int c" and b=256 and c="int b"] by simp
  also have " = int c" using assms
    apply(subst mod_pos_pos_trivial)
    by(simp_all)
  finally have helper2: "(int c + 256 * int b + 65536 * int a) mod 256 = int c" .
  
  from helper1 helper2 show ?thesis by simp
qed

end

Theory NumberWang_IPv6

theory NumberWang_IPv6
imports 
  Word_Lib.Word_Lemmas
  Word_Lib.Word_Syntax
  Word_Lib.Reversed_Bit_Lists
begin

section‹Helper Lemmas for Low-Level Operations on Machine Words›
text‹Needed for IPv6 Syntax›

lemma length_drop_bl: "length (dropWhile Not (to_bl (of_bl bs)))  length bs"
proof -
  have length_takeWhile_Not_replicate_False:
    "length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)"
  for n ls by(subst takeWhile_append2) simp+
  show ?thesis by(simp add: word_rep_drop dropWhile_eq_drop length_takeWhile_Not_replicate_False)
qed

lemma bl_drop_leading_zeros: 
      "(of_bl:: bool list  'a::len word) (dropWhile Not bs) =
       (of_bl:: bool list  'a::len word) bs"
by(induction bs) simp_all


lemma bl_length_drop_bound: assumes "length (dropWhile Not bs)  n"
  shows "length (dropWhile Not (to_bl ((of_bl:: bool list  'a::len word) bs)))  n"
proof -
  have bl_length_drop_twice: 
      "length (dropWhile Not (to_bl ((of_bl:: bool list  'a::len word) (dropWhile Not bs)))) =
       length (dropWhile Not (to_bl ((of_bl:: bool list  'a::len word) bs)))"
    by(simp add: bl_drop_leading_zeros)
  from length_drop_bl
  have *: "length (dropWhile Not (to_bl ((of_bl:: bool list  'a::len word) bs)))  length (dropWhile Not bs)"
   apply(rule dual_order.trans)
   apply(subst bl_length_drop_twice)
   ..
  show ?thesis
  apply(rule order.trans, rule *)
  using assms by(simp)
qed

lemma length_drop_mask_outer: fixes ip::"'a::len word"
  shows "LENGTH('a) - n' = len  length (dropWhile Not (to_bl (ip AND (mask n << n') >> n')))  len"
  apply(subst word_and_mask_shiftl)
  apply(subst shiftl_shiftr1)
   apply(simp; fail)
  apply(simp)
  apply(subst and_mask)
  apply(simp add: word_size)
  apply(simp add: length_drop_mask)
  done
lemma length_drop_mask_inner: fixes ip::"'a::len word"
  shows "n  LENGTH('a) - n'  length (dropWhile Not (to_bl (ip AND (mask n << n') >> n')))  n"
  apply(subst word_and_mask_shiftl)
  apply(subst shiftl_shiftr3)
   apply(simp; fail)
  apply(simp)
  apply(simp add: word_size)
  apply(simp add: mask_twice)
  apply(simp add: length_drop_mask)
  done


lemma mask128: "0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF = (mask 128 :: 'a::len word)"
  by (simp add: mask_eq)


(*-------------- things for ipv6 syntax round trip property two ------------------*)

(*n small, m large*)
lemma helper_masked_ucast_generic:
  fixes b::"16 word"
  assumes "n + 16  m" and "m < 128"
  shows "((ucast:: 16 word  128 word) b << n) && (mask 16 << m) = 0"
proof -
  have "x < 2 ^ (m - n)" if mnh2: "x < 0x10000"
    for x::"128 word"
  proof -
    from assms(1) have mnh3: "16  m - n" by fastforce
    have power_2_16_nat: "(16::nat)  n  (65535::nat) < 2 ^ n" if a:"16  n"for n
    proof -
      have power2_rule: "a  b  (2::nat)^a  2 ^ b" for a b by fastforce
      show ?thesis
       apply(subgoal_tac "65536  2 ^ n")
        apply(subst Nat.less_eq_Suc_le)
        apply(simp; fail)
       apply(subgoal_tac "(65536::nat) = 2^16")
        subgoal using power2_rule 16  n by presburger
       by(simp)
    qed
    have "65536 = unat (65536::128 word)" by auto
    moreover from mnh2 have "unat x <  unat (65536::128 word)" by(rule Word.unat_mono)
    ultimately have x: "unat x < 65536" by simp
    with mnh3 have "unat x < 2 ^ (m - n)" 
      using power_2_16_nat [of m - n] by simp
    with assms(2) show ?thesis by(subst word_less_nat_alt) simp
  qed
  hence mnhelper2: "(of_bl::bool list  128 word) (to_bl b) < 2 ^ (m - n)"
    apply(subgoal_tac "(of_bl::bool list  128 word) (to_bl b) < 2^(LENGTH(16))")
     apply(simp; fail)
    by(rule of_bl_length_less) simp+
  have mnhelper3: "(of_bl::bool list  128 word) (to_bl b) * 2 ^ n < 2 ^ m"
    apply(rule div_lt_mult)
     apply(rule word_less_two_pow_divI)
       using assms by(simp_all add: mnhelper2 p2_gt_0)

  from assms show ?thesis
    apply(subst ucast_bl)+
    apply(subst shiftl_of_bl)
    apply(subst of_bl_append)
    apply simp
    apply(subst word_and_mask_shiftl)
    apply(subst shiftr_div_2n_w)
     subgoal by(simp add: word_size; fail)
    apply(subst word_div_less)
     subgoal by(rule mnhelper3)
    apply simp
    done
qed


lemma unat_of_bl_128_16_less_helper:
  fixes b::"16 word"
  shows "unat ((of_bl::bool list  128 word) (to_bl b)) < 2^16"
proof -
  from word_bl_Rep' have 1: "length (to_bl b) = 16" by simp
  have "unat ((of_bl::bool list  128 word) (to_bl b)) < 2^(length (to_bl b))"
    by(fact unat_of_bl_length)
  with 1 show ?thesis by auto
qed
lemma unat_of_bl_128_16_le_helper: "unat ((of_bl:: bool list  128 word) (to_bl (b::16 word)))  65535"
proof -
  from unat_of_bl_128_16_less_helper[of b] have
    "unat ((of_bl:: bool list  128 word) (to_bl b)) < 65536" by simp 
  from Suc_leI[OF this] show ?thesis by simp
qed


(*reverse*)
 lemma helper_masked_ucast_reverse_generic:
   fixes b::"16 word"
   assumes "m + 16  n" and "n  128 - 16"
   shows "((ucast:: 16 word  128 word) b << n) && (mask 16 << m) = 0"
 proof -

   have power_less_128_helper: "2 ^ n * unat ((of_bl::bool list  128 word) (to_bl b)) < 2 ^ LENGTH(128)"
     if n: "n  128 - 16" for n
   proof -
     have help_mult: "n  l  2 ^ n * x < 2 ^ l  x < 2 ^ (l - n)" for x::nat and l
       by (simp add: nat_mult_power_less_eq semiring_normalization_rules(7))
     from n show ?thesis
       apply(subst help_mult)
        subgoal by (simp)
       apply(rule order_less_le_trans)
        apply(rule unat_of_bl_128_16_less_helper)
       apply(rule Power.power_increasing)
        apply(simp_all)
       done
   qed

   have *: "2 ^ m * (2 ^ (n - m) * unat ((of_bl::bool list  128 word) (to_bl b))) = 
            2 ^ n * unat ((of_bl::bool list  128 word) (to_bl b))"
   proof(cases "unat ((of_bl::bool list  128 word) (to_bl b)) = 0")
   case True thus ?thesis by simp
   next
   case False
    have help_mult: "x  0  b * (c * x) = a * (x::nat)   b * c = a" for x a b c by simp
    from assms show ?thesis
     apply(subst help_mult[OF False])
     apply(subst Power.monoid_mult_class.power_add[symmetric])
     apply(simp)
     done
   qed

  from assms have "unat ((2 ^ n)::128 word) * unat ((of_bl::bool list  128 word) (to_bl b)) mod 2 ^ LENGTH(128) =
        2 ^ m * (2 ^ (n - m) * unat ((of_bl::bool list  128 word) (to_bl b)) mod 2 ^ LENGTH(128))"
     apply(subst nat_mod_eq')
      subgoal apply(subst unat_power_lower)
       subgoal by(simp; fail)
      subgoal by (rule power_less_128_helper) simp
      done
     apply(subst nat_mod_eq')
      subgoal by(rule power_less_128_helper) simp
     apply(subst unat_power_lower)
      apply(simp; fail)
     apply(simp only: *)
     done
   hence ex_k: "k. unat ((2 ^ n)::128 word) * unat ((of_bl::bool list  128 word) (to_bl b)) mod 2 ^ LENGTH(128) = 2 ^ m * k"
     by blast

   hence aligned: "is_aligned ((of_bl::bool list  128 word) (to_bl b) << n) m"
     unfolding is_aligned_iff_dvd_nat
     unfolding dvd_def
     unfolding shiftl_t2n
     unfolding Word.unat_word_ariths(2)
     by assumption

   from assms have of_bl_to_bl_shift_mask: "((of_bl::bool list  128 word) (to_bl b) << n) && mask (16 + m) = 0"
    using is_aligned_mask is_aligned_shiftl by force (*sledgehammer*)

   show ?thesis
    apply(subst ucast_bl)+
    apply(subst word_and_mask_shiftl)
    apply(subst aligned_shiftr_mask_shiftl)
     subgoal by (fact aligned)
    subgoal by (fact of_bl_to_bl_shift_mask)
    done
qed


lemma helper_masked_ucast_equal_generic:
  fixes b::"16 word"
  assumes "n  128 - 16"
  shows "ucast (((ucast:: 16 word  128 word) b << n) && (mask 16 << n) >> n) = b"
proof -
  have ucast_mask: "(ucast:: 16 word  128 word) b && mask 16 = ucast b" 
    by transfer (simp flip: take_bit_eq_mask)
  from assms have "ucast (((ucast:: 16 word  128 word) b && mask (128 - n) && mask 16) && mask (128 - n)) = b"
    by (auto simp add: nth_ucast word_size intro: word_eqI)
  thus ?thesis
  apply(subst word_and_mask_shiftl)
  apply(subst shiftl_shiftr3)
   apply(simp; fail)
  apply(simp)
  apply(subst shiftl_shiftr3)
    apply(simp_all add: word_size and.assoc)
  done
qed

end

Theory WordInterval

(*  Title:      WordInterval.thy
    Authors:    Julius Michaelis, Cornelius Diekmann
*)
theory WordInterval
  imports
  Main
  "Word_Lib.Word_Lemmas"
  "Word_Lib.Next_and_Prev"
begin

section‹WordInterval: Executable datatype for Machine Word Sets›
text‹Stores ranges of machine words as interval. This has been proven quite efficient for
     IP Addresses.›
(*NOTE: All algorithms here use a straight-forward implementation. There is a lot of room for
        improving the computation complexity, for example by making the WordInterval a balanced,
        sorted tree.*)

subsection‹Syntax›
context
  notes [[typedef_overloaded]]
begin
  datatype ('a::len) wordinterval = WordInterval
                                        "('a::len) word" ― ‹start (inclusive)›
                                        "('a::len) word" ― ‹end (inclusive)›
                                  | RangeUnion "'a wordinterval" "'a wordinterval"
end

subsection‹Semantics›
  fun wordinterval_to_set :: "'a::len wordinterval  ('a::len word) set"
  where
    "wordinterval_to_set (WordInterval start end) =
        {start .. end}" |
    "wordinterval_to_set (RangeUnion r1 r2) =
        wordinterval_to_set r1  wordinterval_to_set r2"

(*Note: The runtime of all the operations could be improved, for example by keeping the tree sorted
  and balanced.*)

subsection‹Basic operations›
  text∈›
  fun wordinterval_element :: "'a::len word  'a::len wordinterval  bool" where
    "wordinterval_element el (WordInterval s e)  s  el  el  e" |
    "wordinterval_element el (RangeUnion r1 r2) 
                                            wordinterval_element el r1  wordinterval_element el r2"
  lemma wordinterval_element_set_eq[simp]:
    "wordinterval_element el rg = (el  wordinterval_to_set rg)"
    by(induction rg rule: wordinterval_element.induct) simp_all

  definition wordinterval_union
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_union r1 r2 = RangeUnion r1 r2"
  lemma wordinterval_union_set_eq[simp]:
    "wordinterval_to_set (wordinterval_union r1 r2) = wordinterval_to_set r1  wordinterval_to_set r2"
    unfolding wordinterval_union_def by simp

  fun wordinterval_empty :: "'a::len wordinterval  bool" where
    "wordinterval_empty (WordInterval s e)  e < s" |
    "wordinterval_empty (RangeUnion r1 r2)  wordinterval_empty r1  wordinterval_empty r2"
  lemma wordinterval_empty_set_eq[simp]: "wordinterval_empty r  wordinterval_to_set r = {}"
    by(induction r) auto

  definition Empty_WordInterval :: "'a::len wordinterval" where
    "Empty_WordInterval  WordInterval 1 0"
  lemma wordinterval_empty_Empty_WordInterval: "wordinterval_empty Empty_WordInterval"
    by(simp add: Empty_WordInterval_def)
  lemma Empty_WordInterval_set_eq[simp]: "wordinterval_to_set Empty_WordInterval = {}"
    by(simp add: Empty_WordInterval_def)



subsection‹WordInterval and Lists›
  text‹A list of (start, end)› tuples.›

  text‹wordinterval to list›
  fun wi2l :: "'a::len wordinterval  ('a::len word × 'a::len word) list" where
    "wi2l (RangeUnion r1 r2) = wi2l r1 @ wi2l r2" |
    "wi2l (WordInterval s e) = (if e < s then [] else [(s,e)])"

  text‹list to wordinterval›
  fun l2wi :: "('a::len word × 'a word) list  'a wordinterval" where
    "l2wi [] = Empty_WordInterval" |
    "l2wi [(s,e)] = (WordInterval s e)" |
    "l2wi ((s,e)#rs) = (RangeUnion (WordInterval s e) (l2wi rs))"


  lemma l2wi_append: "wordinterval_to_set (l2wi (l1@l2)) =
                      wordinterval_to_set (l2wi l1)  wordinterval_to_set (l2wi l2)"
    proof(induction l1 arbitrary: l2 rule:l2wi.induct)
    case 1 thus ?case by simp
    next
    case (2 s e l2) thus ?case by (cases l2) simp_all
    next
    case 3 thus ?case by force
    qed

  lemma l2wi_wi2l[simp]: "wordinterval_to_set (l2wi (wi2l r)) = wordinterval_to_set r"
    by(induction r) (simp_all add: l2wi_append)

  lemma l2wi: "wordinterval_to_set (l2wi l) = ( (i,j)  set l. {i .. j})"
    by(induction l rule: l2wi.induct, simp_all)

  lemma wi2l: "((i,j)set (wi2l r). {i .. j}) = wordinterval_to_set r"
    by(induction r rule: wi2l.induct, simp_all)

  lemma l2wi_remdups[simp]: "wordinterval_to_set (l2wi (remdups ls)) = wordinterval_to_set (l2wi ls)"
    by(simp add: l2wi)

  lemma wi2l_empty[simp]: "wi2l Empty_WordInterval = []"
    unfolding Empty_WordInterval_def
    by simp


subsection‹Optimizing and minimizing @{typ "('a::len) wordinterval"}s›
text‹Removing empty intervals›
context
begin
  fun wordinterval_optimize_empty :: "'a::len wordinterval  'a wordinterval" where
    "wordinterval_optimize_empty (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1;
                                                           r2o = wordinterval_optimize_empty r2
      in if
        wordinterval_empty r1o
      then
        r2o
      else if
        wordinterval_empty r2o
      then
        r1o
      else
        RangeUnion r1o r2o)" |
    "wordinterval_optimize_empty r = r"
  lemma wordinterval_optimize_empty_set_eq[simp]:
    "wordinterval_to_set (wordinterval_optimize_empty r) = wordinterval_to_set r"
    by(induction r) (simp_all add: Let_def)

  lemma wordinterval_optimize_empty_double:
    "wordinterval_optimize_empty (wordinterval_optimize_empty r) = wordinterval_optimize_empty r"
    by(induction r) (simp_all add: Let_def)

  private fun wordinterval_empty_shallow :: "'a::len wordinterval  bool"  where
    "wordinterval_empty_shallow (WordInterval s e)  e < s" |
    "wordinterval_empty_shallow (RangeUnion _ _)  False"
  private lemma helper_optimize_shallow:
    "wordinterval_empty_shallow (wordinterval_optimize_empty r) =
      wordinterval_empty (wordinterval_optimize_empty r)"
    by(induction r) fastforce+
  private fun wordinterval_optimize_empty2 where
    "wordinterval_optimize_empty2 (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1;
                                                            r2o = wordinterval_optimize_empty r2
      in if
        wordinterval_empty_shallow r1o
      then
        r2o
      else if
        wordinterval_empty_shallow r2o
      then
        r1o
      else
        RangeUnion r1o r2o)" |
    "wordinterval_optimize_empty2 r = r"
  lemma wordinterval_optimize_empty_code[code_unfold]:
    "wordinterval_optimize_empty = wordinterval_optimize_empty2"
    by (subst fun_eq_iff, clarify, rename_tac r, induct_tac r)
       (unfold wordinterval_optimize_empty.simps wordinterval_optimize_empty2.simps
               Let_def helper_optimize_shallow, simp_all)
end



text‹Merging overlapping intervals›
context
begin

  private definition disjoint :: "'a set  'a set  bool" where
    "disjoint A B  A  B = {}"

  private primrec interval_of :: "('a::len) word × 'a word  'a word set" where
    "interval_of (s,e) = {s .. e}"
  declare interval_of.simps[simp del]

  private definition disjoint_intervals
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word)  bool"
  where
    "disjoint_intervals A B  disjoint (interval_of A) (interval_of B)"

  private definition not_disjoint_intervals
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word)  bool"
  where
    "not_disjoint_intervals A B  ¬ disjoint (interval_of A) (interval_of B)"

  private lemma [code]:
    "not_disjoint_intervals A B =
      (case A of (s,e)  case B of (s',e')  s  e'  s'  e  s  e  s'  e')"
    apply(cases A, cases B)
    apply(simp add: not_disjoint_intervals_def interval_of.simps disjoint_def)
    done

  private lemma [code]:
    "disjoint_intervals A B =
      (case A of (s,e)  case B of (s',e')  s > e'  s' > e  s > e  s' > e')"
    apply(cases A, cases B)
    apply(simp add: disjoint_intervals_def interval_of.simps disjoint_def)
    by fastforce


  text‹BEGIN merging overlapping intervals›
  (*result has no empty intervals and all are disjoint.
    merging things such as [1,7] [8,10] would still be possible*)
  private fun merge_overlap
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word) list  ('a word × 'a word) list"
  where
    "merge_overlap s [] = [s]" |
    "merge_overlap (s,e) ((s',e')#ss) = (
       if not_disjoint_intervals (s,e) (s',e')
       then (min s s', max e e')#ss
       else (s',e')#merge_overlap (s,e) ss)"

  private lemma not_disjoint_union:
      fixes s :: "('a::len) word"
      shows "¬ disjoint {s..e} {s'..e'}  {s..e}  {s'..e'} = {min s s' .. max e e'}"
    by(auto simp add: disjoint_def min_def max_def)

  private lemma disjoint_subset: "disjoint A B  A  B  C  A  C"
    unfolding disjoint_def
    by blast

  private lemma merge_overlap_helper1: "interval_of A  (s  set ss. interval_of s) 
      (s  set (merge_overlap A ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    apply(intro impI conjI)
     apply(drule not_disjoint_union)
     apply blast
    apply(drule_tac C="(xset xs. interval_of x)" in disjoint_subset)
     apply(simp_all)
    done

  private lemma merge_overlap_helper2: "s'set ss. ¬ disjoint (interval_of A) (interval_of s') 
          interval_of A  (s  set ss. interval_of s) = (s  set (merge_overlap A ss). interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    apply(intro impI conjI)
     apply(drule not_disjoint_union)
     apply blast
    apply(simp)
    by blast

  private lemma merge_overlap_length:
    "s'  set ss. ¬ disjoint (interval_of A) (interval_of s') 
      length (merge_overlap A ss) = length ss"
    apply(induction ss)
     apply(simp)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    done

  lemma "merge_overlap (1:: 16 word,2) [(1, 7)] = [(1, 7)]" by eval
  lemma "merge_overlap (1:: 16 word,2) [(2, 7)] = [(1, 7)]" by eval
  lemma "merge_overlap (1:: 16 word,2) [(3, 7)] = [(3, 7), (1,2)]" by eval

  private function listwordinterval_compress
    :: "(('a::len) word × ('a::len) word) list  ('a word × 'a word) list" where
    "listwordinterval_compress [] = []" |
    "listwordinterval_compress (s#ss) = (
            if s'  set ss. disjoint_intervals s s'
            then s#listwordinterval_compress ss
            else listwordinterval_compress (merge_overlap s ss))"
  by(pat_completeness, auto)

  private termination listwordinterval_compress
  apply (relation "measure length")
    apply(rule wf_measure)
   apply(simp)
  using disjoint_intervals_def merge_overlap_length by fastforce

  private lemma listwordinterval_compress:
    "(s  set (listwordinterval_compress ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss rule: listwordinterval_compress.induct)
     apply(simp)
    apply(simp)
    apply(intro impI)
    apply(simp add: disjoint_intervals_def)
    apply(drule merge_overlap_helper2)
    apply(simp)
    done

  lemma "listwordinterval_compress [(1::32 word,3), (8,10), (2,5), (3,7)] = [(8, 10), (1, 7)]"
    by eval

  private lemma A_in_listwordinterval_compress: "A  set (listwordinterval_compress ss) 
    interval_of A  (s  set ss. interval_of s)"
    using listwordinterval_compress by blast

  private lemma listwordinterval_compress_disjoint:
    "A  set (listwordinterval_compress ss)  B  set (listwordinterval_compress ss) 
      A  B  disjoint (interval_of A) (interval_of B)"
    apply(induction ss arbitrary: rule: listwordinterval_compress.induct)
     apply(simp)
    apply(simp split: if_split_asm)
    apply(elim disjE)
       apply(simp_all)
     apply(simp_all add: disjoint_intervals_def disjoint_def)
     apply(blast dest: A_in_listwordinterval_compress)+
    done
  text‹END merging overlapping intervals›


  text‹BEGIN merging adjacent intervals›
  private fun merge_adjacent
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word) list  ('a word × 'a word) list"
  where
    "merge_adjacent s [] = [s]" |
    "merge_adjacent (s,e) ((s',e')#ss) = (
       if s e  s'  e'  word_next e = s'
       then (s, e')#ss
       else if s e  s'  e'  word_next e' = s
       then (s', e)#ss
       else (s',e')#merge_adjacent (s,e) ss)"

  private lemma merge_adjacent_helper:
  "interval_of A  (s  set ss. interval_of s) = (s  set (merge_adjacent A ss). interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add:  interval_of.simps)
    apply(intro impI conjI)
       apply (metis Un_assoc word_adjacent_union)
      apply(elim conjE)
      apply(drule(2) word_adjacent_union)
      subgoal by (blast)
     subgoal by (metis word_adjacent_union Un_assoc)
    by blast

  private lemma merge_adjacent_length:
    "(s', e')set ss. s  e  s'  e'  (word_next e = s'  word_next e' = s)
      length (merge_adjacent (s,e) ss) = length ss"
    apply(induction ss)
     apply(simp)
    apply(rename_tac x xs)
    apply(case_tac x)
    apply(simp add: )
    by blast

  private function listwordinterval_adjacent
    :: "(('a::len) word × ('a::len) word) list  ('a word × 'a word) list" where
    "listwordinterval_adjacent [] = []" |
    "listwordinterval_adjacent ((s,e)#ss) = (
            if (s',e')  set ss. ¬ (s e  s'  e'  (word_next e = s'  word_next e' = s))
            then (s,e)#listwordinterval_adjacent ss
            else listwordinterval_adjacent (merge_adjacent (s,e) ss))"
  by(pat_completeness, auto)

  private termination listwordinterval_adjacent
  apply (relation "measure length")
    apply(rule wf_measure)
   apply(simp)
  apply(simp)
  using merge_adjacent_length by fastforce

  private lemma listwordinterval_adjacent:
    "(s  set (listwordinterval_adjacent ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss rule: listwordinterval_adjacent.induct)
     apply(simp)
    apply(simp add: merge_adjacent_helper)
    done

  lemma "listwordinterval_adjacent [(1::16 word, 3), (5, 10), (10,10), (4,4)] = [(10, 10), (1, 10)]"
    by eval
  text‹END merging adjacent intervals›


  definition wordinterval_compress :: "('a::len) wordinterval  'a wordinterval" where
    "wordinterval_compress r 
      l2wi (remdups (listwordinterval_adjacent (listwordinterval_compress
        (wi2l (wordinterval_optimize_empty r)))))"

  text‹Correctness: Compression preserves semantics›
  lemma wordinterval_compress:
    "wordinterval_to_set (wordinterval_compress r) = wordinterval_to_set r"
    unfolding wordinterval_compress_def
    proof -
      have interval_of': "interval_of s = (case s of (s,e)  {s .. e})" for s
        by (cases s) (simp add: interval_of.simps)

      have "wordinterval_to_set (l2wi (remdups (listwordinterval_adjacent
              (listwordinterval_compress (wi2l (wordinterval_optimize_empty r)))))) =
            (xset (listwordinterval_adjacent (listwordinterval_compress
                (wi2l (wordinterval_optimize_empty r)))). interval_of x)"
        by (force simp: interval_of' l2wi)
      also have " =  (sset (wi2l (wordinterval_optimize_empty r)). interval_of s)"
        by(simp add: listwordinterval_compress listwordinterval_adjacent)
      also have " = ((i, j)set (wi2l (wordinterval_optimize_empty r)). {i..j})"
        by(simp add: interval_of')
      also have " = wordinterval_to_set r" by(simp add: wi2l)
      finally show "wordinterval_to_set
        (l2wi (remdups (listwordinterval_adjacent (listwordinterval_compress
            (wi2l (wordinterval_optimize_empty r))))))
          = wordinterval_to_set r" .
  qed

end

text‹Example›
lemma "(wi2l  (wordinterval_compress :: 32 wordinterval  32 wordinterval)  l2wi)
          [(70, 80001), (0,0), (150, 8000), (1,3), (42,41), (3,7), (56, 200), (8,10)] =
          [(56, 80001), (0, 10)]" by eval

lemma "wordinterval_compress (RangeUnion (RangeUnion (WordInterval (1::32 word) 5)
                                                        (WordInterval 8 10)) (WordInterval 3 7)) =
       WordInterval 1 10" by eval



subsection‹Further operations›

  text⋃›
  definition wordinterval_Union :: "('a::len) wordinterval list  'a wordinterval" where
    "wordinterval_Union ws = wordinterval_compress (foldr wordinterval_union ws Empty_WordInterval)"

  lemma wordinterval_Union:
    "wordinterval_to_set (wordinterval_Union ws) = ( w  (set ws). wordinterval_to_set w)"
    by(induction ws) (simp_all add: wordinterval_compress wordinterval_Union_def)


context
begin
  private fun wordinterval_setminus'
    :: "'a::len wordinterval  'a wordinterval  'a wordinterval" where
    "wordinterval_setminus' (WordInterval s e) (WordInterval ms me) = (
      if s > e  ms > me then WordInterval s e else
      if me  e
        then
          WordInterval (if ms = 0 then 1 else s) (min e (word_prev ms))
        else if ms  s
        then
          WordInterval (max s (word_next me)) (if me = max_word then 0 else e)
        else
          RangeUnion (WordInterval (if ms = 0 then 1 else s) (word_prev ms))
                     (WordInterval (word_next me) (if me = max_word then 0 else e))
        )" |
     "wordinterval_setminus' (RangeUnion r1 r2) t =
        RangeUnion (wordinterval_setminus' r1 t) (wordinterval_setminus' r2 t)"|
     "wordinterval_setminus' t (RangeUnion r1 r2) =
        wordinterval_setminus' (wordinterval_setminus' t r1) r2"

  private lemma wordinterval_setminus'_rr_set_eq:
    "wordinterval_to_set(wordinterval_setminus' (WordInterval s e) (WordInterval ms me)) =
    wordinterval_to_set (WordInterval s e) - wordinterval_to_set (WordInterval ms me)"
     apply(simp only: wordinterval_setminus'.simps)
     apply(case_tac "e < s")
      apply simp
     apply(case_tac "me < ms")
      apply simp
     apply(case_tac [!] "e  me")
      apply(case_tac [!] "ms = 0")
        apply(case_tac [!] "ms  s")
            apply(case_tac [!] "me = max_word")
                    apply(simp_all add: word_next_unfold word_prev_unfold min_def max_def)
            apply(safe)
                                  apply(auto)
                          apply(uint_arith)
                         apply(uint_arith)
                        apply(uint_arith)
                       apply(uint_arith)
                      apply(uint_arith)
                     apply(uint_arith)
                    apply(uint_arith)
                   apply(uint_arith)
                  apply(uint_arith)
                 apply(uint_arith)
                apply(uint_arith)
               apply(uint_arith)
              apply(uint_arith)
             apply(uint_arith)
            apply(uint_arith)
           apply(uint_arith)
          apply(uint_arith)
         apply(uint_arith)
        apply(uint_arith)
       apply(uint_arith)
      apply(uint_arith)
     apply(uint_arith)
   done

  private lemma wordinterval_setminus'_set_eq:
    "wordinterval_to_set (wordinterval_setminus' r1 r2) =
      wordinterval_to_set r1 - wordinterval_to_set r2"
    apply(induction rule: wordinterval_setminus'.induct)
      using wordinterval_setminus'_rr_set_eq apply blast
     apply auto
    done
  lemma wordinterval_setminus'_empty_struct:
    "wordinterval_empty r2  wordinterval_setminus' r1 r2 = r1"
    by(induction r1 r2 rule: wordinterval_setminus'.induct) auto


  definition wordinterval_setminus
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_setminus r1 r2 = wordinterval_compress (wordinterval_setminus' r1 r2)"

  lemma wordinterval_setminus_set_eq[simp]: "wordinterval_to_set (wordinterval_setminus r1 r2) =
    wordinterval_to_set r1 - wordinterval_to_set r2"
    by(simp add: wordinterval_setminus_def wordinterval_compress wordinterval_setminus'_set_eq)
end

definition wordinterval_UNIV :: "'a::len wordinterval" where
  "wordinterval_UNIV  WordInterval 0 max_word"
lemma wordinterval_UNIV_set_eq[simp]: "wordinterval_to_set wordinterval_UNIV = UNIV"
  unfolding wordinterval_UNIV_def
  using max_word_max by fastforce

fun wordinterval_invert :: "'a::len wordinterval  'a::len wordinterval" where
  "wordinterval_invert r = wordinterval_setminus wordinterval_UNIV r"
lemma wordinterval_invert_set_eq[simp]:
  "wordinterval_to_set (wordinterval_invert r) = UNIV - wordinterval_to_set r" by(auto)

lemma wordinterval_invert_UNIV_empty:
  "wordinterval_empty (wordinterval_invert wordinterval_UNIV)" by simp

lemma wi2l_univ[simp]: "wi2l wordinterval_UNIV = [(0, max_word)]"
  unfolding wordinterval_UNIV_def
  by simp

text∩›
context
begin
  private lemma "{(s::nat) .. e}  {s' .. e'} = {}  s > e'  s' > e  s > e  s' > e'"
    by simp linarith
  private fun wordinterval_intersection'
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_intersection' (WordInterval s e) (WordInterval s' e') = (
        if s > e  s' > e'  s > e'  s' > e  s > e  s' > e'
        then
          Empty_WordInterval
        else
          WordInterval (max s s') (min e e')
        )" |
    "wordinterval_intersection' (RangeUnion r1 r2) t =
        RangeUnion (wordinterval_intersection' r1 t) (wordinterval_intersection' r2 t)"|
    "wordinterval_intersection' t (RangeUnion r1 r2) =
        RangeUnion (wordinterval_intersection' t r1) (wordinterval_intersection' t r2)"

  private lemma wordinterval_intersection'_set_eq:
    "wordinterval_to_set (wordinterval_intersection' r1 r2) =
      wordinterval_to_set r1  wordinterval_to_set r2"
    by(induction r1 r2 rule: wordinterval_intersection'.induct) (auto)

  lemma "wordinterval_intersection'
          (RangeUnion (RangeUnion (WordInterval (1::32 word) 3) (WordInterval 8 10))
                      (WordInterval 1 3)) (WordInterval 1 3) =
          RangeUnion (RangeUnion (WordInterval 1 3) (WordInterval 1 0)) (WordInterval 1 3)" by eval

  definition wordinterval_intersection
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_intersection r1 r2  wordinterval_compress (wordinterval_intersection' r1 r2)"

  lemma wordinterval_intersection_set_eq[simp]:
    "wordinterval_to_set (wordinterval_intersection r1 r2) =
      wordinterval_to_set r1  wordinterval_to_set r2"
    by(simp add: wordinterval_intersection_def
                 wordinterval_compress wordinterval_intersection'_set_eq)

  lemma "wordinterval_intersection
          (RangeUnion (RangeUnion (WordInterval (1::32 word) 3) (WordInterval 8 10))
                      (WordInterval 1 3)) (WordInterval 1 3) =
          WordInterval 1 3" by eval
end


definition wordinterval_subset :: "'a::len wordinterval  'a::len wordinterval  bool" where
  "wordinterval_subset r1 r2  wordinterval_empty (wordinterval_setminus r1 r2)"
lemma wordinterval_subset_set_eq[simp]:
  "wordinterval_subset r1 r2 = (wordinterval_to_set r1  wordinterval_to_set r2)"
  unfolding wordinterval_subset_def by simp

definition wordinterval_eq :: "'a::len wordinterval  'a::len wordinterval  bool" where
  "wordinterval_eq r1 r2 = (wordinterval_subset r1 r2  wordinterval_subset r2 r1)"
lemma wordinterval_eq_set_eq:
  "wordinterval_eq r1 r2  wordinterval_to_set r1 = wordinterval_to_set r2"
  unfolding wordinterval_eq_def by auto

thm iffD1[OF wordinterval_eq_set_eq]
(*declare iffD1[OF wordinterval_eq_set_eq, simp]*)

lemma wordinterval_eq_comm: "wordinterval_eq r1 r2  wordinterval_eq r2 r1"
  unfolding wordinterval_eq_def by fast
lemma wordinterval_to_set_alt: "wordinterval_to_set r = {x. wordinterval_element x r}"
  unfolding wordinterval_element_set_eq by blast

lemma wordinterval_un_empty:
  "wordinterval_empty r1  wordinterval_eq (wordinterval_union r1 r2) r2"
  by(subst wordinterval_eq_set_eq, simp)
lemma wordinterval_un_emty_b:
  "wordinterval_empty r2  wordinterval_eq (wordinterval_union r1 r2) r1"
  by(subst wordinterval_eq_set_eq, simp)

lemma wordinterval_Diff_triv:
  "wordinterval_empty (wordinterval_intersection a b)  wordinterval_eq (wordinterval_setminus a b) a"
  unfolding wordinterval_eq_set_eq
  by simp blast



text‹A size of the datatype, does not correspond to the cardinality of the corresponding set›
fun wordinterval_size :: "('a::len) wordinterval  nat" where
  "wordinterval_size (RangeUnion a b) = wordinterval_size a + wordinterval_size b" |
  "wordinterval_size (WordInterval s e) = (if s  e then 1 else 0)"

lemma wordinterval_size_length: "wordinterval_size r = length (wi2l r)"
  by(induction r) (auto)

lemma Ex_wordinterval_nonempty: "x::('a::len wordinterval). y  wordinterval_to_set x"
  proof show "y  wordinterval_to_set wordinterval_UNIV" by simp qed

lemma wordinterval_eq_reflp:
  "reflp wordinterval_eq"
  apply(rule reflpI)
  by(simp only: wordinterval_eq_set_eq)
lemma wordintervalt_eq_symp:
  "symp wordinterval_eq"
  apply(rule sympI)
  by(simp add: wordinterval_eq_comm)
lemma wordinterval_eq_transp:
  "transp wordinterval_eq"
  apply(rule transpI)
  by(simp only: wordinterval_eq_set_eq)

lemma wordinterval_eq_equivp:
  "equivp wordinterval_eq"
  by (auto intro: equivpI wordinterval_eq_reflp wordintervalt_eq_symp wordinterval_eq_transp)


text‹The smallest element in the interval›
  definition is_lowest_element :: "'a::ord  'a set  bool" where
    "is_lowest_element x S = (x  S  (yS. y  x  y = x))"

  lemma
  	fixes x :: "'a :: complete_lattice"
  	assumes "x  S"
  	shows " x = Inf S  is_lowest_element x S"
  using assms apply(simp add: is_lowest_element_def)
   by (simp add: Inf_lower eq_iff)

  lemma
  	fixes x :: "'a :: linorder"
  	assumes "finite S" and "x  S"
  	shows "is_lowest_element x S  x = Min S"
  apply(rule)
  subgoal
   apply(simp add: is_lowest_element_def)
   apply(subst Min_eqI[symmetric])
   using assms by(auto)
  by (metis Min.coboundedI assms(1) assms(2) dual_order.antisym is_lowest_element_def)

text‹Smallest element in the interval›
  fun wordinterval_lowest_element :: "'a::len wordinterval  'a word option" where
    "wordinterval_lowest_element (WordInterval s e) = (if s  e then Some s else None)" |
    "wordinterval_lowest_element (RangeUnion A B) =
      (case (wordinterval_lowest_element A, wordinterval_lowest_element B) of
          (Some a, Some b)  Some (if a < b then a else b) |
          (None, Some b)  Some b |
          (Some a, None)  Some a |
          (None, None)  None)"

  lemma wordinterval_lowest_none_empty: "wordinterval_lowest_element r = None  wordinterval_empty r"
    proof(induction r)
    case WordInterval thus ?case by simp
    next
    case RangeUnion thus ?case by fastforce
    qed


  lemma wordinterval_lowest_element_correct_A:
    "wordinterval_lowest_element r = Some x  is_lowest_element x (wordinterval_to_set r)"
    unfolding is_lowest_element_def
    apply(induction r arbitrary: x rule: wordinterval_lowest_element.induct)
     apply(rename_tac rs re x, case_tac "rs  re", auto)[1]
    apply(subst(asm) wordinterval_lowest_element.simps(2))
    apply(rename_tac A B x)
    apply(case_tac     "wordinterval_lowest_element B")
     apply(case_tac[!] "wordinterval_lowest_element A")
       apply(simp_all add: wordinterval_lowest_none_empty)[3]
    apply fastforce
  done


  lemma wordinterval_lowest_element_set_eq: assumes "¬ wordinterval_empty r"
    shows "(wordinterval_lowest_element r = Some x) = (is_lowest_element x (wordinterval_to_set r))"
    (*unfolding is_lowest_element_def*)
    proof(rule iffI)
      assume "wordinterval_lowest_element r = Some x"
      thus "is_lowest_element x (wordinterval_to_set r)"
     using wordinterval_lowest_element_correct_A wordinterval_lowest_none_empty by simp
    next
      assume "is_lowest_element x (wordinterval_to_set r)"
      with assms show "(wordinterval_lowest_element r = Some x)"
        proof(induction r arbitrary: x rule: wordinterval_lowest_element.induct)
        case 1 thus ?case by(simp add: is_lowest_element_def)
        next
        case (2 A B x)

        have is_lowest_RangeUnion: "is_lowest_element x (wordinterval_to_set A  wordinterval_to_set B) 
          is_lowest_element x (wordinterval_to_set A)  is_lowest_element x (wordinterval_to_set B)"
          by(simp add: is_lowest_element_def)

         (*why ⋀ A B?*)
         have wordinterval_lowest_element_RangeUnion:
          "a b A B. wordinterval_lowest_element A = Some a 
                  wordinterval_lowest_element B = Some b 
                  wordinterval_lowest_element (RangeUnion A B) = Some (min a b)"
           by(auto dest!: wordinterval_lowest_element_correct_A simp add: is_lowest_element_def min_def)

        from 2 show ?case
        apply(case_tac     "wordinterval_lowest_element B")
         apply(case_tac[!] "wordinterval_lowest_element A")
           apply(auto simp add: is_lowest_element_def)[3]
        apply(subgoal_tac "¬ wordinterval_empty A  ¬ wordinterval_empty B")
         prefer 2
         using arg_cong[where f = Not, OF wordinterval_lowest_none_empty] apply blast
        apply(drule(1) wordinterval_lowest_element_RangeUnion)
        apply(simp split: option.split_asm add: min_def)
         apply(drule is_lowest_RangeUnion)
         apply(elim disjE)
          apply(simp add: is_lowest_element_def)
         apply(clarsimp simp add: wordinterval_lowest_none_empty)

        apply(simp add: is_lowest_element_def)
        apply(clarsimp simp add: wordinterval_lowest_none_empty)
        using wordinterval_lowest_element_correct_A[simplified is_lowest_element_def]
        by (metis Un_iff not_le)
      qed
    qed


text‹Cardinality approximation for @{typ "('a::len) wordinterval"}s›
context
begin
  lemma card_atLeastAtMost_word: fixes s::"('a::len) word" shows "card {s..e} = Suc (unat e) - (unat s)"
    apply(cases "s > e")
     apply(simp)
     apply(subst(asm) Word.word_less_nat_alt)
     apply simp
    apply(subst upto_enum_set_conv2[symmetric])
    apply(subst List.card_set)
    apply(simp add: remdups_enum_upto)
    done

  fun wordinterval_card :: "('a::len) wordinterval  nat" where
    "wordinterval_card (WordInterval s e) = Suc (unat e) - (unat s)" |
    "wordinterval_card (RangeUnion a b) = wordinterval_card a + wordinterval_card b"

  lemma wordinterval_card: "wordinterval_card r  card (wordinterval_to_set r)"
    proof(induction r)
    case WordInterval thus ?case by (simp add: card_atLeastAtMost_word)
    next
    case (RangeUnion r1 r2)
      have "card (wordinterval_to_set r1  wordinterval_to_set r2) 
              card (wordinterval_to_set r1) + card (wordinterval_to_set r2)"
        using Finite_Set.card_Un_le by blast
      with RangeUnion show ?case by(simp)
    qed

  text‹With @{thm wordinterval_compress} it should be possible to get the exact cardinality›
end

end

Theory Hs_Compat

theory Hs_Compat
imports Main
begin

section‹Definitions inspired by the Haskell World.›

definition uncurry :: "('b  'c  'a)  'b × 'c  'a"
where
  "uncurry f a  (case a of (x,y)  f x y)"

lemma uncurry_simp[simp]: "uncurry f (a,b) = f a b" 
  by(simp add: uncurry_def)

lemma uncurry_curry_id: "uncurry  curry = id" "curry  uncurry = id" 
  by(simp_all add: fun_eq_iff)

lemma uncurry_split: "P (uncurry f p)  (x1 x2. p = (x1, x2)  P (f x1 x2))"
  by(cases p) simp

lemma uncurry_split_asm: "P (uncurry f a)  ¬(x y. a = (x,y)  ¬P (f x y))" 
  by(simp split: uncurry_split)

lemmas uncurry_splits = uncurry_split uncurry_split_asm

lemma uncurry_case_stmt: "(case x of (a, b)  f a b) = uncurry f x"
  by(cases x, simp)

end

Theory IP_Address

(*  Title:      IP_Address.thy
    Authors:    Cornelius Diekmann
*)
theory IP_Address
  imports
    Word_Lib.Word_Lemmas
    Word_Lib.Word_Syntax
    Word_Lib.Reversed_Bit_Lists
    Hs_Compat
    WordInterval
begin

section ‹Modelling IP Adresses›
  text‹An IP address is basically an unsigned integer.
    We model IP addresses of arbitrary lengths.

    We will write @{typ "'i::len word"} for IP addresses of length @{term "LENGTH('i::len)"}.
    We use the convention to write @{typ 'i} whenever we mean IP addresses instead of generic words.
    When we will later have theorems with several polymorphic types in it (e.g. arbitrarily
    extensible packets), this notation makes it easier to spot that type @{typ 'i} is for
    IP addresses.

    The files @{file ‹IPv4.thy›} @{file ‹IPv6.thy›} concrete this for IPv4 and IPv6.›

  text‹The maximum IP address›
  definition max_ip_addr :: "'i::len word" where
    "max_ip_addr  of_nat ((2^(len_of(TYPE('i)))) - 1)"

  lemma max_ip_addr_max_word: "max_ip_addr = max_word"
    by (simp only: max_ip_addr_def of_nat_mask_eq flip: mask_eq_exp_minus_1) simp

  lemma max_ip_addr_max: "a. a  max_ip_addr"
    by(simp add: max_ip_addr_max_word)
  lemma range_0_max_UNIV: "UNIV = {0 .. max_ip_addr}" (*not in the simp set, for a reason*)
    by(simp add: max_ip_addr_max_word) fastforce

  lemma "size (x::'i::len word) = len_of(TYPE('i))" by(simp add:word_size)

subsection‹Sets of IP Addresses›
  (*Warning, not executable!*)
  text‹Specifying sets with network masks: 192.168.0.0 255.255.255.0›
  definition ipset_from_netmask::"'i::len word  'i::len word  'i::len word set" where
    "ipset_from_netmask addr netmask 
      let
        network_prefix = (addr AND netmask)
      in
        {network_prefix .. network_prefix OR (NOT netmask)}"

  text‹Example (pseudo syntax):
    @{const ipset_from_netmask} 192.168.1.129  255.255.255.0› =
        {192.168.1.0 .. 192.168.1.255}›

  text‹A network mask of all ones (i.e. @{term "(- 1)::'i::len word"}).›
  lemma ipset_from_netmask_minusone:
    "ipset_from_netmask ip (- 1) = {ip}" by (simp add: ipset_from_netmask_def)
  lemma ipset_from_netmask_maxword:
    "ipset_from_netmask ip max_word = {ip}" by (simp add: ipset_from_netmask_def)

  lemma ipset_from_netmask_zero:
    "ipset_from_netmask ip 0 = UNIV" by (auto simp add: ipset_from_netmask_def)


  text‹Specifying sets in Classless Inter-domain Routing (CIDR) notation: 192.168.0.0/24›
  definition ipset_from_cidr ::"'i::len word  nat  'i::len word set" where
    "ipset_from_cidr addr pflength 
       ipset_from_netmask addr ((mask pflength) << (len_of(TYPE('i)) - pflength))"

  text‹Example (pseudo syntax):
    @{const ipset_from_cidr} 192.168.1.129 24› = {192.168.1.0 .. 192.168.1.255}›

  (*does this simplify stuff?*)
  lemma "(case ipcidr of (base, len)  ipset_from_cidr base len) = uncurry ipset_from_cidr ipcidr"
    by(simp add: uncurry_case_stmt)

  lemma ipset_from_cidr_0: "ipset_from_cidr ip 0 = UNIV"
    by(auto simp add: ipset_from_cidr_def ipset_from_netmask_def Let_def)

  text‹A prefix length of word size gives back the singleton set with the IP address.
       Example: 192.168.1.2/32 = {192.168.1.2}›
  lemma ipset_from_cidr_wordlength:
    fixes ip :: "'i::len word"
    shows "ipset_from_cidr ip (LENGTH('i)) = {ip}"
    by (simp add: ipset_from_cidr_def ipset_from_netmask_def)

  text‹Alternative definition: Considering words as bit lists:›
  lemma ipset_from_cidr_bl:
    fixes addr :: "'i::len word"
    shows "ipset_from_cidr addr pflength 
            ipset_from_netmask addr (of_bl ((replicate pflength True) @
                                            (replicate ((len_of(TYPE('i))) - pflength)) False))"
    by(simp add: ipset_from_cidr_def mask_bl shiftl_of_bl)

  lemma ipset_from_cidr_alt:
    fixes pre :: "'i::len word"
    shows "ipset_from_cidr pre len =
            {pre AND (mask len << LENGTH('i) - len)
             ..
             pre OR mask (LENGTH('i) - len)}"
    apply(simp add: ipset_from_cidr_def ipset_from_netmask_def Let_def)
    apply(simp add: word_oa_dist)
    apply(simp add: NOT_mask_shifted_lenword)
    done

  lemma ipset_from_cidr_alt2:
    fixes base ::"'i::len word"
    shows "ipset_from_cidr base len =
           ipset_from_netmask base (NOT (mask (LENGTH('i) - len)))"
    apply(simp add: ipset_from_cidr_def)
    using NOT_mask_shifted_lenword by(metis word_not_not)

  text‹In CIDR notation, we cannot express the empty set.›
  lemma ipset_from_cidr_not_empty: "ipset_from_cidr base len  {}"
    by(simp add: ipset_from_cidr_alt bitmagic_zeroLast_leq_or1Last)

  text‹Though we can write 192.168.1.2/24, we say that 192.168.0.0/24 is well-formed.›
  lemma ipset_from_cidr_base_wellforemd: fixes base:: "'i::len word"
    assumes "mask (LENGTH('i) - l) AND base = 0"
      shows "ipset_from_cidr base l = {base .. base OR mask (LENGTH('i) - l)}"
  proof -
    have maskshift_eq_not_mask_generic:
      "((mask l << LENGTH('i) - l) :: 'i::len word) = NOT (mask (LENGTH('i) - l))"
      using NOT_mask_shifted_lenword by (metis word_not_not)
    have *: "base AND NOT (mask (LENGTH('i) - l)) = base"
      unfolding mask_eq_0_eq_x[symmetric] using assms word_bw_comms(1)[of base] by simp
    hence **: "base AND NOT (mask (LENGTH('i) - l)) OR mask (LENGTH('i) - l) =
                base OR mask (LENGTH('i) - l)" by simp
    have "ipset_from_netmask base (NOT (mask (LENGTH('i) - l))) =
            {base .. base || mask (LENGTH('i) - l)}"
      by(simp add: ipset_from_netmask_def Let_def ** *)
    thus ?thesis by(simp add: ipset_from_cidr_def maskshift_eq_not_mask_generic)
  qed


  lemma ipset_from_cidr_large_pfxlen:
    fixes ip:: "'i::len word"
    assumes "n  LENGTH('i)"
    shows "ipset_from_cidr ip n = {ip}"
  proof -
    have obviously: "mask (LENGTH('i) - n) = 0" by (simp add: assms)
    show ?thesis
      apply(subst ipset_from_cidr_base_wellforemd)
       subgoal using assms by simp
      by (simp add: obviously)
  qed

  lemma ipset_from_netmask_base_mask_consume:
    fixes base :: "'i::len word"
    shows "ipset_from_netmask (base AND NOT (mask (LENGTH('i) - m)))
                              (NOT (mask (LENGTH('i) - m)))
            =
             ipset_from_netmask base (NOT (mask (LENGTH('i) - m)))"
    unfolding ipset_from_netmask_def by(simp)


  text‹Another definition of CIDR notation:
       All IP address which are equal on the first @{term "len - n"} bits›
  definition ip_cidr_set :: "'i::len word  nat  'i word set" where
    "ip_cidr_set i r 
      {j . i AND NOT (mask (LENGTH('i) - r)) = j AND NOT (mask (LENGTH('i) - r))}"

  text‹The definitions are equal›
  lemma ipset_from_cidr_eq_ip_cidr_set:
    fixes base::"'i::len word"
    shows "ipset_from_cidr base len = ip_cidr_set base len"
  proof -
    have maskshift_eq_not_mask_generic:
      "((mask len << LENGTH('a) - len) :: 'a::len word) = NOT (mask (LENGTH('a) - len))"
      using NOT_mask_shifted_lenword by (metis word_not_not)
    have 1: "mask (len - m) AND base AND NOT (mask (len - m)) = 0"
      for len m and base::"'i::len word"
      by(simp add: word_bw_lcs)
    have 2: "mask (LENGTH('i) - len) AND pfxm_p = 0 
           (a  ipset_from_netmask pfxm_p (NOT (mask (LENGTH('i) - len)))) 
           (pfxm_p = NOT (mask (LENGTH('i) - len)) AND a)" for a::"'i::len word" and pfxm_p
    apply(subst ipset_from_cidr_alt2[symmetric])
    apply(subst zero_base_lsb_imp_set_eq_as_bit_operation)
     apply(simp; fail)
    apply(subst ipset_from_cidr_base_wellforemd)
     apply(simp; fail)
    apply(simp)
    done
    from 2[OF 1, of _ base] have
      "(x  ipset_from_netmask base (~~ (mask (LENGTH('i) - len)))) 
       (base && ~~ (mask (LENGTH('i) - len)) = x && ~~ (mask (LENGTH('i) - len)))" for x
    apply(simp add: ipset_from_netmask_base_mask_consume)
    unfolding word_bw_comms(1)[of _ " ~~ (mask (LENGTH('i) - len))"] by simp
    then show ?thesis
      unfolding ip_cidr_set_def ipset_from_cidr_def
      by(auto simp add:  maskshift_eq_not_mask_generic)
  qed

  lemma ip_cidr_set_change_base: "j  ip_cidr_set i r  ip_cidr_set j r = ip_cidr_set i r"
    by (auto simp: ip_cidr_set_def)



subsection‹IP Addresses as WordIntervals›
  text‹The nice thing is: @{typ "'i wordinterval"}s are executable.›

  definition iprange_single :: "'i::len word  'i wordinterval" where
    "iprange_single ip  WordInterval ip ip"

  fun iprange_interval :: "('i::len word × 'i::len word)  'i wordinterval" where
    "iprange_interval (ip_start, ip_end) = WordInterval ip_start ip_end"
  declare iprange_interval.simps[simp del]

  lemma iprange_interval_uncurry: "iprange_interval ipcidr = uncurry WordInterval ipcidr"
    by(cases ipcidr) (simp add: iprange_interval.simps)

  lemma "wordinterval_to_set (iprange_single ip) = {ip}"
    by(simp add: iprange_single_def)
  lemma "wordinterval_to_set (iprange_interval (ip1, ip2)) = {ip1 .. ip2}"
    by(simp add: iprange_interval.simps)

  text‹Now we can use the set operations on @{typ "'i::len wordinterval"}s›
  term wordinterval_to_set
  term wordinterval_element
  term wordinterval_union
  term wordinterval_empty
  term wordinterval_setminus
  term wordinterval_UNIV
  term wordinterval_invert
  term wordinterval_intersection
  term wordinterval_subset
  term wordinterval_eq


subsection‹IP Addresses in CIDR Notation›
  text‹We want to convert IP addresses in CIDR notation to intervals.
    We already have @{const ipset_from_cidr}, which gives back a non-executable set.
    We want to convert to something we can store in an @{typ "'i wordinterval"}.›

  fun ipcidr_to_interval_start :: "('i::len word × nat)  'i::len word" where
    "ipcidr_to_interval_start (pre, len) = (
      let netmask = (mask len) << (LENGTH('i) - len);
          network_prefix = (pre AND netmask)
      in network_prefix)"
  fun ipcidr_to_interval_end :: "('i::len word × nat)  'i::len word" where
    "ipcidr_to_interval_end (pre, len) = (
      let netmask = (mask len) << (LENGTH('i) - len);
          network_prefix = (pre AND netmask)
      in network_prefix OR (NOT netmask))"
  definition ipcidr_to_interval :: "('i::len word × nat)  ('i word × 'i word)" where
    "ipcidr_to_interval cidr  (ipcidr_to_interval_start cidr, ipcidr_to_interval_end cidr)"


  lemma ipset_from_cidr_ipcidr_to_interval:
    "ipset_from_cidr base len =
      {ipcidr_to_interval_start (base,len) .. ipcidr_to_interval_end (base,len)}"
    by(simp add: Let_def ipcidr_to_interval_def ipset_from_cidr_def ipset_from_netmask_def)
  declare ipcidr_to_interval_start.simps[simp del] ipcidr_to_interval_end.simps[simp del]

  lemma ipcidr_to_interval:
    "ipcidr_to_interval (base, len) = (s,e)  ipset_from_cidr base len = {s .. e}"
    by (simp add: ipcidr_to_interval_def ipset_from_cidr_ipcidr_to_interval)

  definition ipcidr_tuple_to_wordinterval :: "('i::len word × nat)  'i wordinterval" where
    "ipcidr_tuple_to_wordinterval iprng  iprange_interval (ipcidr_to_interval iprng)"

  lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval:
    "wordinterval_to_set (ipcidr_tuple_to_wordinterval (b, m)) = ipset_from_cidr b m"
    unfolding ipcidr_tuple_to_wordinterval_def ipset_from_cidr_ipcidr_to_interval
              ipcidr_to_interval_def
    by(simp add: iprange_interval.simps)

  lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry:
    "wordinterval_to_set (ipcidr_tuple_to_wordinterval ipcidr) = uncurry ipset_from_cidr ipcidr"
    by(cases ipcidr, simp add: wordinterval_to_set_ipcidr_tuple_to_wordinterval)

  definition ipcidr_union_set :: "('i::len word × nat) set  ('i word) set" where
    "ipcidr_union_set ips  (base, len)  ips. ipset_from_cidr base len"

  lemma ipcidr_union_set_uncurry:
    "ipcidr_union_set ips = ( ipcidr  ips. uncurry ipset_from_cidr ipcidr)"
    by(simp add: ipcidr_union_set_def uncurry_case_stmt)


subsection‹Clever Operations on IP Addresses in CIDR Notation›
  text‹Intersecting two intervals may result in a new interval.
    Example: {1..10} ∩ {5..20} = {5..10}›

    Intersecting two IP address ranges represented as CIDR ranges results either in the empty set
    or the smaller of the two ranges. It will never create a new range.
    ›
  context
  begin
    (*contributed by Lars Noschinski*)
    private lemma less_and_not_mask_eq:
      fixes i :: "('a :: len) word"
      assumes "r2  r1" "i && ~~ (mask r2) = x && ~~ (mask r2)"
      shows "i && ~~ (mask r1) = x && ~~ (mask r1)"
    proof -
      have "i AND NOT (mask r1) = (i && ~~ (mask r2)) && ~~ (mask r1)" (is "_ = ?w && _")
        using r2  r1 by (simp add: and_not_mask_twice max_def)
      also have "?w = x && ~~ (mask r2)" by fact
      also have " && ~~ (mask r1) = x && ~~ (mask r1)"
        using r2  r1 by (simp add: and_not_mask_twice max_def)
      finally show ?thesis .
    qed

    lemma ip_cidr_set_less:
      fixes i :: "'i::len word"
      shows "r1  r2  ip_cidr_set i r2  ip_cidr_set i r1"
      unfolding ip_cidr_set_def
      apply auto
      apply (rule less_and_not_mask_eq[where ?r2.0="LENGTH('i) - r2"])
      apply auto
      done

    private lemma ip_cidr_set_intersect_subset_helper:
      fixes i1 r1 i2 r2
      assumes disj: "ip_cidr_set i1 r1  ip_cidr_set i2 r2  {}" and  "r1  r2"
      shows "ip_cidr_set i2 r2  ip_cidr_set i1 r1"
      proof -
      from disj obtain j where "j  ip_cidr_set i1 r1" "j  ip_cidr_set i2 r2" by auto
      with r1  r2 have "j  ip_cidr_set j r1" "j  ip_cidr_set j r1"
        using ip_cidr_set_change_base ip_cidr_set_less by blast+

      show "ip_cidr_set i2 r2  ip_cidr_set i1 r1"
      proof
        fix i assume "i  ip_cidr_set i2 r2"
        with j  ip_cidr_set i2 r2 have "i  ip_cidr_set j r2" using ip_cidr_set_change_base by auto
        also have "ip_cidr_set j r2  ip_cidr_set j r1" using r1  r2 ip_cidr_set_less by blast
        also have " = ip_cidr_set i1 r1" using j  ip_cidr_set i1 r1 ip_cidr_set_change_base by blast
        finally show "i  ip_cidr_set i1 r1" .
      qed
    qed

    lemma ip_cidr_set_notsubset_empty_inter:
      "¬ ip_cidr_set i1 r1  ip_cidr_set i2 r2 
       ¬ ip_cidr_set i2 r2  ip_cidr_set i1 r1 
       ip_cidr_set i1 r1  ip_cidr_set i2 r2 = {}"
      apply(cases "r1  r2")
       subgoal using ip_cidr_set_intersect_subset_helper by blast
      apply(cases "r2  r1")
       subgoal using ip_cidr_set_intersect_subset_helper by blast
      by(simp)
  end


  lemma ip_cidr_intersect:
     "¬ ipset_from_cidr b2 m2  ipset_from_cidr b1 m1 
      ¬ ipset_from_cidr b1 m1  ipset_from_cidr b2 m2 
      ipset_from_cidr b1 m1  ipset_from_cidr b2 m2 = {}"
    apply(simp add: ipset_from_cidr_eq_ip_cidr_set)
    using ip_cidr_set_notsubset_empty_inter by blast

  text‹Computing the intersection of two IP address ranges in CIDR notation›
  fun ipcidr_conjunct :: "('i::len word × nat)  ('i word × nat)  ('i word × nat) option" where
    "ipcidr_conjunct (base1, m1) (base2, m2) = (
       if
         ipset_from_cidr base1 m1  ipset_from_cidr base2 m2 = {}
       then
         None
       else if
         ipset_from_cidr base1 m1  ipset_from_cidr base2 m2
       then
         Some (base1, m1)
       else
         Some (base2, m2)
      )"

  text‹Intersecting with an address with prefix length zero always yields a non-empty result.›
  lemma ipcidr_conjunct_any: "ipcidr_conjunct a (x,0)  None" "ipcidr_conjunct (y,0) b  None"
     apply(cases a, simp add: ipset_from_cidr_0 ipset_from_cidr_not_empty)
    by(cases b, simp add: ipset_from_cidr_0 ipset_from_cidr_not_empty)

  lemma ipcidr_conjunct_correct: "(case ipcidr_conjunct (b1, m1) (b2, m2)
                                          of Some (bx, mx)  ipset_from_cidr bx mx
                                          |  None  {}) =
                                   (ipset_from_cidr b1 m1)  (ipset_from_cidr b2 m2)"
    apply(simp split: if_split_asm)
    using ip_cidr_intersect by fast
  declare ipcidr_conjunct.simps[simp del]


subsection‹Code Equations›
  text‹Executable definition using word intervals›
  lemma ipcidr_conjunct_word[code_unfold]:
  "ipcidr_conjunct ips1 ips2 = (
     if
      wordinterval_empty (wordinterval_intersection
                            (ipcidr_tuple_to_wordinterval ips1) (ipcidr_tuple_to_wordinterval ips2))
     then
       None
     else if
       wordinterval_subset (ipcidr_tuple_to_wordinterval ips1) (ipcidr_tuple_to_wordinterval ips2)
     then
       Some ips1
     else
       Some ips2
     )"
  apply(simp)
  apply(cases ips1, cases ips2, rename_tac b1 m1 b2 m2, simp)
  apply(auto simp add: wordinterval_to_set_ipcidr_tuple_to_wordinterval ipcidr_conjunct.simps
             split: if_split_asm)
  done

  (*with the code_unfold lemma before, this works!*)
  lemma "ipcidr_conjunct (0::32 word,0) (8,1) = Some (8, 1)" by eval
  export_code ipcidr_conjunct checking SML

  text‹making element check executable›
  lemma addr_in_ipset_from_netmask_code[code_unfold]:
    "addr  (ipset_from_netmask base netmask) 
      (base AND netmask)  addr  addr  (base AND netmask) OR (NOT netmask)"
    by(simp add: ipset_from_netmask_def Let_def)
  lemma addr_in_ipset_from_cidr_code[code_unfold]:
    "(addr::'i::len word)  (ipset_from_cidr pre len) 
       (pre AND ((mask len) << (LENGTH('i) - len)))  addr 
        addr  pre OR (mask (LENGTH('i) - len))"
  unfolding ipset_from_cidr_alt by simp


end

Theory IPv4

(*  Title:      IPv4.thy
    Authors:    Cornelius Diekmann, Julius Michaelis
*)
theory IPv4
imports IP_Address
        NumberWang_IPv4
        (* include "HOL-Library.Code_Target_Nat" if you need to work with actual numbers.*)
begin

lemma take_bit_word_beyond_length_eq:
  ‹take_bit n w = w if LENGTH('a)  n for w :: 'a::len word›
  using that by transfer simp


section ‹IPv4 Adresses›
  text‹An IPv4 address is basically a 32 bit unsigned integer.›
  type_synonym ipv4addr = "32 word"

  text‹Conversion between natural numbers and IPv4 adresses›
  definition nat_of_ipv4addr :: "ipv4addr  nat" where
    "nat_of_ipv4addr a = unat a"
  definition ipv4addr_of_nat :: "nat  ipv4addr" where
    "ipv4addr_of_nat n =  of_nat n"

  text‹The maximum IPv4 addres›
  definition max_ipv4_addr :: "ipv4addr" where
    "max_ipv4_addr  ipv4addr_of_nat ((2^32) - 1)"

  lemma max_ipv4_addr_number: "max_ipv4_addr = 4294967295"
    unfolding max_ipv4_addr_def ipv4addr_of_nat_def by(simp)
  lemma "max_ipv4_addr = 0b11111111111111111111111111111111"
    by(fact max_ipv4_addr_number)
  lemma max_ipv4_addr_max_word: "max_ipv4_addr = max_word"
    by(simp add: max_ipv4_addr_number)
  lemma max_ipv4_addr_max[simp]: "a. a  max_ipv4_addr"
    by(simp add: max_ipv4_addr_max_word)
  lemma UNIV_ipv4addrset: "UNIV = {0 .. max_ipv4_addr}" (*not in the simp set, for a reason*)
    by(simp add: max_ipv4_addr_max_word) fastforce

  text‹identity functions›
  lemma nat_of_ipv4addr_ipv4addr_of_nat_mod: "nat_of_ipv4addr (ipv4addr_of_nat n) = n mod 2^32"
    by (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def unat_of_nat take_bit_eq_mod)
  lemma nat_of_ipv4addr_ipv4addr_of_nat:
    " n  nat_of_ipv4addr max_ipv4_addr   nat_of_ipv4addr (ipv4addr_of_nat n) = n"
    by (simp add: nat_of_ipv4addr_ipv4addr_of_nat_mod max_ipv4_addr_def)
  lemma ipv4addr_of_nat_nat_of_ipv4addr: "ipv4addr_of_nat (nat_of_ipv4addr addr) = addr"
    by(simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)

subsection‹Representing IPv4 Adresses (Syntax)›
  fun ipv4addr_of_dotdecimal :: "nat × nat × nat × nat  ipv4addr" where
    "ipv4addr_of_dotdecimal (a,b,c,d) = ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a )"

  fun dotdecimal_of_ipv4addr :: "ipv4addr  nat × nat × nat × nat" where
    "dotdecimal_of_ipv4addr a = (nat_of_ipv4addr ((a >> 24) AND 0xFF),
                                    nat_of_ipv4addr ((a >> 16) AND 0xFF),
                                    nat_of_ipv4addr ((a >> 8) AND 0xFF),
                                    nat_of_ipv4addr (a AND 0xff))"

  declare ipv4addr_of_dotdecimal.simps[simp del]
  declare dotdecimal_of_ipv4addr.simps[simp del]

  text‹Examples:›
  lemma "ipv4addr_of_dotdecimal (192, 168, 0, 1) = 3232235521"
    by(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
    (*could be solved by eval, but needs "HOL-Library.Code_Target_Nat"*)
  lemma "dotdecimal_of_ipv4addr 3232235521 = (192, 168, 0, 1)"
    by(simp add: dotdecimal_of_ipv4addr.simps nat_of_ipv4addr_def)

  text‹a different notation for @{term ipv4addr_of_dotdecimal}
  lemma ipv4addr_of_dotdecimal_bit:
    "ipv4addr_of_dotdecimal (a,b,c,d) =
      (ipv4addr_of_nat a << 24) + (ipv4addr_of_nat b << 16) +
       (ipv4addr_of_nat c << 8) + ipv4addr_of_nat d"
  proof -
    have a: "(ipv4addr_of_nat a) << 24 = ipv4addr_of_nat (a * 16777216)"
      by(simp add: ipv4addr_of_nat_def shiftl_t2n)
    have b: "(ipv4addr_of_nat b) << 16 = ipv4addr_of_nat (b * 65536)"
      by(simp add: ipv4addr_of_nat_def shiftl_t2n)
    have c: "(ipv4addr_of_nat c) << 8 = ipv4addr_of_nat (c * 256)"
      by(simp add: ipv4addr_of_nat_def shiftl_t2n)
    have ipv4addr_of_nat_suc: "x. ipv4addr_of_nat (Suc x) = word_succ (ipv4addr_of_nat (x))"
      by(simp add: ipv4addr_of_nat_def, metis Abs_fnat_hom_Suc of_nat_Suc)
    { fix x y
      have "ipv4addr_of_nat x + ipv4addr_of_nat y = ipv4addr_of_nat (x+y)"
        apply(induction x arbitrary: y)
         apply(simp add: ipv4addr_of_nat_def; fail)
        by(simp add: ipv4addr_of_nat_suc word_succ_p1)
    } from this a b c
    show ?thesis
      apply(simp add: ipv4addr_of_dotdecimal.simps)
      apply(rule arg_cong[where f=ipv4addr_of_nat])
      apply(thin_tac _)+
      by presburger
  qed

  lemma size_ipv4addr: "size (x::ipv4addr) = 32" by(simp add:word_size)

  lemma dotdecimal_of_ipv4addr_ipv4addr_of_dotdecimal:
  " a < 256; b < 256; c < 256; d < 256  
    dotdecimal_of_ipv4addr (ipv4addr_of_dotdecimal (a,b,c,d)) = (a,b,c,d)"
  proof -
    assume  "a < 256" and "b < 256" and "c < 256" and "d < 256"
    note assms= a < 256 b < 256 c < 256 d < 256
    hence a:  "nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 24) AND mask 8) = a"
      apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
      apply transfer
      apply (simp add: drop_bit_take_bit nat_take_bit_eq flip: take_bit_eq_mask)
      apply (simp add: drop_bit_eq_div take_bit_eq_mod)
      done
    have ipv4addr_of_nat_AND_mask8: "(ipv4addr_of_nat a) AND mask 8 = (ipv4addr_of_nat (a mod 256))"
      for a
      apply (simp add: ipv4addr_of_nat_def)
      apply transfer
      apply (simp flip: take_bit_eq_mask)
      apply (simp add: take_bit_eq_mod of_nat_mod)
      done
    from assms have b:
      "nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 16) AND mask 8) = b"
      apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
      apply transfer
      apply (simp add: drop_bit_take_bit flip: take_bit_eq_mask)
      using div65536
      apply (simp add: drop_bit_eq_div take_bit_eq_mod)
      done
    from assms have c:
      "nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 8) AND mask 8) = c"
      apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
      apply transfer
      apply (simp add: drop_bit_take_bit flip: take_bit_eq_mask)
      using div256
      apply (simp add: drop_bit_eq_div take_bit_eq_mod)
      done
    from d < 256 have d: "nat_of_ipv4addr (ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) AND mask 8) = d"
      apply (simp add: ipv4addr_of_nat_AND_mask8 ipv4addr_of_nat_def nat_of_ipv4addr_def)
      apply transfer
      apply (simp flip: take_bit_eq_mask)
      apply (simp add: take_bit_eq_mod nat_mod_distrib nat_add_distrib nat_mult_distrib mod256)
      done
    from a b c d show ?thesis
      apply (simp add: ipv4addr_of_dotdecimal.simps dotdecimal_of_ipv4addr.simps)
      apply (simp add: mask_eq)
      done
  qed

  lemma ipv4addr_of_dotdecimal_dotdecimal_of_ipv4addr:
    "(ipv4addr_of_dotdecimal (dotdecimal_of_ipv4addr ip)) = ip"
  proof -
    have ip_and_mask8_bl_drop24: "(ip::ipv4addr) AND mask 8 = of_bl (drop 24 (to_bl ip))"
      by(simp add: of_drop_to_bl size_ipv4addr)
    have List_rev_drop_geqn: "length x  n  (take n (rev x)) = rev (drop (length x - n) x)"
      for x :: "'a list" and n by(simp add: List.rev_drop)
    have and_mask_bl_take: "length x  n  ((of_bl x) AND mask n) = (of_bl (rev (take n (rev (x)))))"
      for x n by(simp add: List_rev_drop_geqn of_bl_drop)
    have ipv4addr_and_255: "x AND 255 = x AND mask 8" for x :: ipv4addr
      by(simp add: mask_eq)
    have bit_equality:
      "((ip >> 24) AND 0xFF << 24) + ((ip >> 16) AND 0xFF << 16) + ((ip >> 8) AND 0xFF << 8) + (ip AND 0xFF) =
       of_bl (take 8 (to_bl ip) @ take 8 (drop 8 (to_bl ip)) @ take 8 (drop 16 (to_bl ip)) @ drop 24 (to_bl ip))"
      apply(simp add: ipv4addr_and_255)
      apply(simp add: shiftr_slice)
      apply(simp add: slice_take' size_ipv4addr)
      apply(simp add: and_mask_bl_take)
      apply(simp add: List_rev_drop_geqn)
      apply(simp add: drop_take)
      apply(simp add: shiftl_of_bl)
      apply(simp add: of_bl_append)
      apply(simp add: ip_and_mask8_bl_drop24)
      done
    have blip_split: " blip. length blip = 32 
      blip = (take 8 blip) @ (take 8 (drop 8 blip)) @ (take 8 (drop 16 blip)) @ (take 8 (drop 24 blip))"
      by(rename_tac blip,case_tac blip,simp_all)+ (*I'm so sorry for this ...*)
    have "ipv4addr_of_dotdecimal (dotdecimal_of_ipv4addr ip) = of_bl (to_bl ip)"
      apply(subst blip_split)
       apply(simp; fail)
      apply(simp add: ipv4addr_of_dotdecimal_bit dotdecimal_of_ipv4addr.simps)
      apply(simp add: ipv4addr_of_nat_nat_of_ipv4addr)
      apply(simp add: bit_equality)
      done
    thus ?thesis using word_bl.Rep_inverse[symmetric] by simp
  qed

  lemma ipv4addr_of_dotdecimal_eqE:
    " ipv4addr_of_dotdecimal (a,b,c,d) = ipv4addr_of_dotdecimal (e,f,g,h);
       a < 256; b < 256; c < 256; d < 256; e < 256; f < 256; g < 256; h < 256  
         a = e  b = f  c = g  d = h"
     by (metis Pair_inject dotdecimal_of_ipv4addr_ipv4addr_of_dotdecimal)

subsection‹IP Ranges: Examples›
  lemma "(UNIV :: ipv4addr set) = {0 .. max_ipv4_addr}" by(simp add: UNIV_ipv4addrset)
  lemma "(42::ipv4addr)  UNIV" by(simp)

  (*Warning, not executable!*)

  lemma "ipset_from_netmask (ipv4addr_of_dotdecimal (192,168,0,42)) (ipv4addr_of_dotdecimal (255,255,0,0)) =
          {ipv4addr_of_dotdecimal (192,168,0,0) .. ipv4addr_of_dotdecimal (192,168,255,255)}"
   by(simp add: ipset_from_netmask_def ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)

  lemma "ipset_from_netmask (ipv4addr_of_dotdecimal (192,168,0,42)) (ipv4addr_of_dotdecimal (0,0,0,0)) = UNIV"
    by(simp add: UNIV_ipv4addrset ipset_from_netmask_def ipv4addr_of_dotdecimal.simps
                 ipv4addr_of_nat_def max_ipv4_addr_max_word)

  text‹192.168.0.0/24›

  lemma fixes addr :: ipv4addr
    shows "ipset_from_cidr addr pflength =
            ipset_from_netmask addr ((mask pflength) << (32 - pflength))"
    by(simp add: ipset_from_cidr_def)

  lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,42)) 16 =
          {ipv4addr_of_dotdecimal (192,168,0,0) .. ipv4addr_of_dotdecimal (192,168,255,255)}"
   by(simp add: ipset_from_cidr_alt mask_eq ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)

  lemma "ip  (ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 0)"
    by(simp add: ipset_from_cidr_0)

  lemma ipv4set_from_cidr_32: fixes addr :: ipv4addr
    shows "ipset_from_cidr addr 32 = {addr}"
    by (simp add: ipset_from_cidr_alt take_bit_word_beyond_length_eq flip: take_bit_eq_mask)

  lemma  fixes pre :: ipv4addr
    shows "ipset_from_cidr pre len = {(pre AND ((mask len) << (32 - len))) .. pre OR (mask (32 - len))}"
    by (simp add: ipset_from_cidr_alt ipset_from_cidr_def)

  text‹making element check executable›
  lemma addr_in_ipv4set_from_netmask_code[code_unfold]:
    fixes addr :: ipv4addr
    shows "addr  (ipset_from_netmask base netmask) 
            (base AND netmask)  addr  addr  (base AND netmask) OR (NOT netmask)"
    by (simp add: addr_in_ipset_from_netmask_code)
  lemma addr_in_ipv4set_from_cidr_code[code_unfold]:
    fixes addr :: ipv4addr
    shows "addr  (ipset_from_cidr pre len) 
              (pre AND ((mask len) << (32 - len)))  addr  addr  pre OR (mask (32 - len))"
    by(simp add: addr_in_ipset_from_cidr_code)

  (*small numbers because we didn't load Code_Target_Nat. Should work by eval*)
lemma "ipv4addr_of_dotdecimal (192,168,42,8)  (ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,0)) 16)"
  by (simp add: ipv4addr_of_nat_def ipset_from_cidr_def ipv4addr_of_dotdecimal.simps
    ipset_from_netmask_def mask_eq_exp_minus_1 word_le_def take_bit_minus_one_eq_mask)

  definition ipv4range_UNIV :: "32 wordinterval" where "ipv4range_UNIV  wordinterval_UNIV"

  lemma ipv4range_UNIV_set_eq: "wordinterval_to_set ipv4range_UNIV = UNIV"
    by(simp only: ipv4range_UNIV_def wordinterval_UNIV_set_eq)


  thm iffD1[OF wordinterval_eq_set_eq]
  (*TODO: probably the following is a good idea?*)
  (*
  declare iffD1[OF wordinterval_eq_set_eq, cong]
  *)


  text‹This LENGTH('a)› is 32 for IPv4 addresses.›
  lemma ipv4cidr_to_interval_simps[code_unfold]: "ipcidr_to_interval ((pre::ipv4addr), len) = (
      let netmask = (mask len) << (32 - len);
          network_prefix = (pre AND netmask)
      in (network_prefix, network_prefix OR (NOT netmask)))"
  by(simp add: ipcidr_to_interval_def Let_def ipcidr_to_interval_start.simps ipcidr_to_interval_end.simps)

end

Theory IPv6

(*  Title:      IPv6.thy
    Authors:    Cornelius Diekmann
*)
theory IPv6
  imports
    IP_Address
    NumberWang_IPv6
    (* include "HOL-Library.Code_Target_Nat" if you need to work with actual numbers.*)
begin


section ‹IPv6 Addresses›
  text‹An IPv6 address is basically a 128 bit unsigned integer. RFC 4291, Section 2.›
  type_synonym ipv6addr = "128 word"
 
  text‹Conversion between natural numbers and IPv6 adresses›
  definition nat_of_ipv6addr :: "ipv6addr  nat" where
    "nat_of_ipv6addr a = unat a"
  definition ipv6addr_of_nat :: "nat  ipv6addr" where
    "ipv6addr_of_nat n =  of_nat n"

lemma "ipv6addr_of_nat n = word_of_int (int n)"
    by(simp add: ipv6addr_of_nat_def)

  text‹The maximum IPv6 address›
  definition max_ipv6_addr :: "ipv6addr" where 
    "max_ipv6_addr  ipv6addr_of_nat ((2^128) - 1)"

  lemma max_ipv6_addr_number: "max_ipv6_addr = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
    unfolding max_ipv6_addr_def ipv6addr_of_nat_def by(simp)
  lemma "max_ipv6_addr = 340282366920938463463374607431768211455"
    by(fact max_ipv6_addr_number)
  lemma max_ipv6_addr_max_word: "max_ipv6_addr = max_word"
    by(simp add: max_ipv6_addr_number)
  lemma max_ipv6_addr_max: "a. a  max_ipv6_addr"
    by(simp add: max_ipv6_addr_max_word)
  lemma UNIV_ipv6addrset: "UNIV = {0 .. max_ipv6_addr}" (*not in the simp set, for a reason*)
    by(simp add: max_ipv6_addr_max_word) fastforce

  text‹identity functions›
  lemma nat_of_ipv6addr_ipv6addr_of_nat_mod: "nat_of_ipv6addr (ipv6addr_of_nat n) = n mod 2^128"
    by (simp add: ipv6addr_of_nat_def nat_of_ipv6addr_def unat_of_nat take_bit_eq_mod)
  lemma nat_of_ipv6addr_ipv6addr_of_nat:
    "n  nat_of_ipv6addr max_ipv6_addr  nat_of_ipv6addr (ipv6addr_of_nat n) = n"
    by (simp add: nat_of_ipv6addr_ipv6addr_of_nat_mod max_ipv6_addr_def)
  lemma ipv6addr_of_nat_nat_of_ipv6addr: "ipv6addr_of_nat (nat_of_ipv6addr addr) = addr"
    by(simp add: ipv6addr_of_nat_def nat_of_ipv6addr_def)

subsection‹Syntax of IPv6 Adresses›
  text‹RFC 4291, Section 2.2.: Text Representation of Addresses›

  text‹Quoting the RFC (note: errata exists):›
  text_raw‹
  \begin{verbatim}
   1. The preferred form is x:x:x:x:x:x:x:x, where the 'x's are one to
      four hexadecimal digits of the eight 16-bit pieces of the address.
      Examples:
         ABCD:EF01:2345:6789:ABCD:EF01:2345:6789
         2001:DB8:0:0:8:800:200C:417A
  \end{verbatim}
›
  datatype ipv6addr_syntax = 
    IPv6AddrPreferred "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  text_raw‹
  \begin{verbatim}
   2. [...] In order to make writing addresses containing zero
      bits easier, a special syntax is available to compress the zeros.
      The use of "::" indicates one or more groups of 16 bits of zeros.
      The "::" can only appear once in an address.  The "::" can also be
      used to compress leading or trailing zeros in an address.

      For example, the following addresses
         2001:DB8:0:0:8:800:200C:417A   a unicast address
         FF01:0:0:0:0:0:0:101           a multicast address
         0:0:0:0:0:0:0:1                the loopback address
         0:0:0:0:0:0:0:0                the unspecified address

      may be represented as
         2001:DB8::8:800:200C:417A      a unicast address
         FF01::101                      a multicast address
         ::1                            the loopback address
         ::                             the unspecified address
  \end{verbatim}
›
  (*datatype may take some minutes to load*)
  datatype ipv6addr_syntax_compressed =
  ― ‹using @{typ unit} for the omission @{text "::"}. 

     Naming convention of the datatype: 
      The first number is the position where the omission occurs.
      The second number is the length of the specified address pieces.
        I.e. `8 minus the second number' pieces are omitted.›
    IPv6AddrCompressed1_0 unit
  | IPv6AddrCompressed1_1 unit "16 word"
  | IPv6AddrCompressed1_2 unit "16 word" "16 word"
  | IPv6AddrCompressed1_3 unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_4 unit "16 word" "16 word" "16 word" "16 word" 
  | IPv6AddrCompressed1_5 unit "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_6 unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_7 unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed2_1 "16 word" unit
  | IPv6AddrCompressed2_2 "16 word" unit "16 word"
  | IPv6AddrCompressed2_3 "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed2_4 "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_5 "16 word" unit "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_6 "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_7 "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed3_2 "16 word" "16 word" unit
  | IPv6AddrCompressed3_3 "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed3_4 "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed3_5 "16 word" "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed3_6 "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed3_7 "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed4_3 "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed4_4 "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed4_5 "16 word" "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed4_6 "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed4_7 "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed5_4 "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed5_5 "16 word" "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed5_6 "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed5_7 "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word"

  | IPv6AddrCompressed6_5 "16 word" "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed6_6 "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed6_7 "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word"

  | IPv6AddrCompressed7_6 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed7_7 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word"

  | IPv6AddrCompressed8_7 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit

  (*RFC 5952:
    """
    4.  A Recommendation for IPv6 Text Representation
    4.2.2.  Handling One 16-Bit 0 Field
       The symbol "::" MUST NOT be used to shorten just one 16-bit 0 field.
       For example, the representation 2001:db8:0:1:1:1:1:1 is correct, but
       2001:db8::1:1:1:1:1 is not correct.
    """

    So we could remove all IPv6AddrCompressed*_7 constructors.
    But these are `recommendations', we might still see these non-recommended definitions.
    "[...] all implementations must accept and be able to handle any legitimate RFC 4291 format."
  *)

  (*More convenient parser helper function for compressed IPv6 addresses:
    Input list (from parser):
      Some 16word ⟶ address piece
      None ⟶ omission '::'
    
  
   Basically, the parser must only do the following (python syntax):
     split the string which is an ipv6 address at ':'
     map empty string to None
     map everything else to Some (string_to_16word str)
     sanitize empty strings at the start and the end (see toString and parser theories)
   Example:
     "1:2:3".split(":")  = ['1', '2', '3']
     ":2:3:4".split(":") = ['', '2', '3', '4']
     ":2::3".split(":")  = ['', '2', '', '3']
     "1:2:3:".split(":") = ['1', '2', '3', '']
  *)
  definition parse_ipv6_address_compressed :: "((16 word) option) list  ipv6addr_syntax_compressed option" where
    "parse_ipv6_address_compressed as = (case as of 
      [None]  Some (IPv6AddrCompressed1_0 ())
    | [None, Some a]  Some (IPv6AddrCompressed1_1 () a)
    | [None, Some a, Some b]  Some (IPv6AddrCompressed1_2 () a b)
    | [None, Some a, Some b, Some c]  Some (IPv6AddrCompressed1_3 () a b c)
    | [None, Some a, Some b, Some c, Some d]  Some (IPv6AddrCompressed1_4 () a b c d)
    | [None, Some a, Some b, Some c, Some d, Some e]  Some (IPv6AddrCompressed1_5 () a b c d e)
    | [None, Some a, Some b, Some c, Some d, Some e, Some f]  Some (IPv6AddrCompressed1_6 () a b c d e f)
    | [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g]  Some (IPv6AddrCompressed1_7 () a b c d e f g)
  
    | [Some a, None]  Some (IPv6AddrCompressed2_1 a ())
    | [Some a, None, Some b]  Some (IPv6AddrCompressed2_2 a () b)
    | [Some a, None, Some b, Some c]  Some (IPv6AddrCompressed2_3 a () b c)
    | [Some a, None, Some b, Some c, Some d]  Some (IPv6AddrCompressed2_4 a () b c d)
    | [Some a, None, Some b, Some c, Some d, Some e]  Some (IPv6AddrCompressed2_5 a () b c d e)
    | [Some a, None, Some b, Some c, Some d, Some e, Some f]  Some (IPv6AddrCompressed2_6 a () b c d e f)
    | [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g]  Some (IPv6AddrCompressed2_7 a () b c d e f g)
  
    | [Some a, Some b, None]  Some (IPv6AddrCompressed3_2 a b ())
    | [Some a, Some b, None, Some c]  Some (IPv6AddrCompressed3_3 a b () c)
    | [Some a, Some b, None, Some c, Some d]  Some (IPv6AddrCompressed3_4 a b () c d)
    | [Some a, Some b, None, Some c, Some d, Some e]  Some (IPv6AddrCompressed3_5 a b () c d e)
    | [Some a, Some b, None, Some c, Some d, Some e, Some f]  Some (IPv6AddrCompressed3_6 a b () c d e f)
    | [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g]  Some (IPv6AddrCompressed3_7 a b () c d e f g)
  
    | [Some a, Some b, Some c, None]  Some (IPv6AddrCompressed4_3 a b c ())
    | [Some a, Some b, Some c, None, Some d]  Some (IPv6AddrCompressed4_4 a b c () d)
    | [Some a, Some b, Some c, None, Some d, Some e]  Some (IPv6AddrCompressed4_5 a b c () d e)
    | [Some a, Some b, Some c, None, Some d, Some e, Some f]  Some (IPv6AddrCompressed4_6 a b c () d e f)
    | [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g]  Some (IPv6AddrCompressed4_7 a b c () d e f g)
  
    | [Some a, Some b, Some c, Some d, None]  Some (IPv6AddrCompressed5_4 a b c d ())
    | [Some a, Some b, Some c, Some d, None, Some e]  Some (IPv6AddrCompressed5_5 a b c d () e)
    | [Some a, Some b, Some c, Some d, None, Some e, Some f]  Some (IPv6AddrCompressed5_6 a b c d () e f)
    | [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g]  Some (IPv6AddrCompressed5_7 a b c d () e f g)
  
    | [Some a, Some b, Some c, Some d, Some e, None]  Some (IPv6AddrCompressed6_5 a b c d e ())
    | [Some a, Some b, Some c, Some d, Some e, None, Some f]  Some (IPv6AddrCompressed6_6 a b c d e () f)
    | [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g]  Some (IPv6AddrCompressed6_7 a b c d e () f g)
  
    | [Some a, Some b, Some c, Some d, Some e, Some f, None]  Some (IPv6AddrCompressed7_6 a b c d e f ())
    | [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g]  Some (IPv6AddrCompressed7_7 a b c d e f () g)

    | [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None]  Some (IPv6AddrCompressed8_7 a b c d e f g ())
    | _  None ― ‹invalid ipv6 copressed address.›
)"

  fun ipv6addr_syntax_compressed_to_list :: "ipv6addr_syntax_compressed  ((16 word) option) list"
    where 
      "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_0 _) =
                                     [None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_1 () a) =
                                     [None, Some a]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_2 () a b) =
                                     [None, Some a, Some b]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_3 () a b c) =
                                     [None, Some a, Some b, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_4 () a b c d) =
                                     [None, Some a, Some b, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_5 () a b c d e) =
                                     [None, Some a, Some b, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_6 () a b c d e f) =
                                     [None, Some a, Some b, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_7 () a b c d e f g) =
                                     [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_1 a ()) =
                                     [Some a, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_2 a () b) =
                                     [Some a, None, Some b]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_3 a () b c) =
                                     [Some a, None, Some b, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_4 a () b c d) =
                                     [Some a, None, Some b, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_5 a () b c d e) =
                                     [Some a, None, Some b, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_6 a () b c d e f) =
                                     [Some a, None, Some b, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_7 a () b c d e f g) =
                                     [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_2 a b ()) = [Some a, Some b, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_3 a b () c) =
                                     [Some a, Some b, None, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_4 a b () c d) =
                                     [Some a, Some b, None, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_5 a b () c d e) =
                                     [Some a, Some b, None, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_6 a b () c d e f) =
                                     [Some a, Some b, None, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_7 a b () c d e f g) =
                                     [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_3 a b c ()) =
                                     [Some a, Some b, Some c, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_4 a b c () d) =
                                     [Some a, Some b, Some c, None, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_5 a b c () d e) =
                                     [Some a, Some b, Some c, None, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_6 a b c () d e f) =
                                     [Some a, Some b, Some c, None, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_7 a b c () d e f g) =
                                     [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_4 a b c d ()) =
                                     [Some a, Some b, Some c, Some d, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_5 a b c d () e) =
                                     [Some a, Some b, Some c, Some d, None, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_6 a b c d () e f) =
                                     [Some a, Some b, Some c, Some d, None, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_7 a b c d () e f g) =
                                     [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_5 a b c d e ()) =
                                     [Some a, Some b, Some c, Some d, Some e, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_6 a b c d e () f) =
                                     [Some a, Some b, Some c, Some d, Some e, None, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_7 a b c d e () f g) =
                                     [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed7_6 a b c d e f ()) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed7_7 a b c d e f () g) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g]"

    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed8_7 a b c d e f g ()) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None]"


(*for all ipv6_syntax, there is a corresponding list representation*)
lemma parse_ipv6_address_compressed_exists:
  obtains ss where "parse_ipv6_address_compressed ss = Some ipv6_syntax"
proof
  define ss where "ss = ipv6addr_syntax_compressed_to_list ipv6_syntax"
  thus "parse_ipv6_address_compressed ss = Some ipv6_syntax"
    by (cases ipv6_syntax; simp add: parse_ipv6_address_compressed_def)
qed

lemma parse_ipv6_address_compressed_identity:
      "parse_ipv6_address_compressed (ipv6addr_syntax_compressed_to_list (ipv6_syntax)) = Some ipv6_syntax"
  by(cases ipv6_syntax; simp add: parse_ipv6_address_compressed_def)


lemma parse_ipv6_address_compressed_someE:
  assumes "parse_ipv6_address_compressed as = Some ipv6"
  obtains
    "as = [None]" "ipv6 = (IPv6AddrCompressed1_0 ())"  |
    a where "as = [None, Some a]" "ipv6 = (IPv6AddrCompressed1_1 () a)"  |
    a b where "as = [None, Some a, Some b]" "ipv6 = (IPv6AddrCompressed1_2 () a b)"  |
    a b c where "as = [None, Some a, Some b, Some c]" "ipv6 = (IPv6AddrCompressed1_3 () a b c)" |
    a b c d where "as = [None, Some a, Some b, Some c, Some d]" "ipv6 = (IPv6AddrCompressed1_4 () a b c d)" |
    a b c d e where "as = [None, Some a, Some b, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed1_5 () a b c d e)" |
    a b c d e f where "as = [None, Some a, Some b, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed1_6 () a b c d e f)" |
    a b c d e f g where "as = [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed1_7 () a b c d e f g)" |
  
    a where "as = [Some a, None]" "ipv6 = (IPv6AddrCompressed2_1 a ())" |
    a b where "as = [Some a, None, Some b]" "ipv6 = (IPv6AddrCompressed2_2 a () b)" |
    a b c where "as = [Some a, None, Some b, Some c]" "ipv6 = (IPv6AddrCompressed2_3 a () b c)" |
    a b c d where "as = [Some a, None, Some b, Some c, Some d]" "ipv6 = (IPv6AddrCompressed2_4 a () b c d)" |
    a b c d e where "as = [Some a, None, Some b, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed2_5 a () b c d e)" |
    a b c d e f where "as = [Some a, None, Some b, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed2_6 a () b c d e f)" |
    a b c d e f g where "as = [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed2_7 a () b c d e f g)" |
  
    a b where "as = [Some a, Some b, None]" "ipv6 = (IPv6AddrCompressed3_2 a b ())" |
    a b c where "as = [Some a, Some b, None, Some c]" "ipv6 = (IPv6AddrCompressed3_3 a b () c)" |
    a b c d where "as = [Some a, Some b, None, Some c, Some d]" "ipv6 = (IPv6AddrCompressed3_4 a b () c d)" |
    a b c d e where "as = [Some a, Some b, None, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed3_5 a b () c d e)" |
    a b c d e f where "as = [Some a, Some b, None, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed3_6 a b () c d e f)" |
    a b c d e f g where "as = [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed3_7 a b () c d e f g)" |
  
    a b c where "as = [Some a, Some b, Some c, None]" "ipv6 = (IPv6AddrCompressed4_3 a b c ())" |
    a b c d where "as = [Some a, Some b, Some c, None, Some d]" "ipv6 = (IPv6AddrCompressed4_4 a b c () d)" |
    a b c d e where "as = [Some a, Some b, Some c, None, Some d, Some e]" "ipv6 = (IPv6AddrCompressed4_5 a b c () d e)" |
    a b c d e f where "as = [Some a, Some b, Some c, None, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed4_6 a b c () d e f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed4_7 a b c () d e f g)" |
  
    a b c d where "as = [Some a, Some b, Some c, Some d, None]" "ipv6 = (IPv6AddrCompressed5_4 a b c d ())" |
    a b c d e where "as = [Some a, Some b, Some c, Some d, None, Some e]" "ipv6 = (IPv6AddrCompressed5_5 a b c d () e)" |
    a b c d e f where "as = [Some a, Some b, Some c, Some d, None, Some e, Some f]" "ipv6 = (IPv6AddrCompressed5_6 a b c d () e f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed5_7 a b c d () e f g)" |
  
    a b c d e where "as = [Some a, Some b, Some c, Some d, Some e, None]" "ipv6 = (IPv6AddrCompressed6_5 a b c d e ())" |
    a b c d e f where "as = [Some a, Some b, Some c, Some d, Some e, None, Some f]" "ipv6 = (IPv6AddrCompressed6_6 a b c d e () f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g]" "ipv6 = (IPv6AddrCompressed6_7 a b c d e () f g)" |
  
    a b c d e f where "as = [Some a, Some b, Some c, Some d, Some e, Some f, None]" "ipv6 = (IPv6AddrCompressed7_6 a b c d e f ())" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g]" "ipv6 = (IPv6AddrCompressed7_7 a b c d e f () g)" |

    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None]" "ipv6 = (IPv6AddrCompressed8_7 a b c d e f g ())"
using assms
unfolding parse_ipv6_address_compressed_def
by (auto split: list.split_asm option.split_asm) (* takes a minute *)

lemma parse_ipv6_address_compressed_identity2:
      "ipv6addr_syntax_compressed_to_list ipv6_syntax = ls 
        (parse_ipv6_address_compressed ls) = Some ipv6_syntax"
      (is "?lhs = ?rhs")
proof
  assume ?rhs
  thus ?lhs
    by (auto elim: parse_ipv6_address_compressed_someE)
next
  assume ?lhs
  thus ?rhs
    by (cases ipv6_syntax) (auto simp: parse_ipv6_address_compressed_def)
qed

text‹Valid IPv6 compressed notation:
   at most one omission
   at most 7 pieces
›
lemma RFC_4291_format: "parse_ipv6_address_compressed as  None 
       length (filter (λp. p = None) as) = 1  length (filter (λp. p  None) as)  7"
       (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain addr where "parse_ipv6_address_compressed as = Some addr"
    by blast
  thus ?rhs
    by (elim parse_ipv6_address_compressed_someE; simp)
next
  assume ?rhs
  thus ?lhs
    unfolding parse_ipv6_address_compressed_def
    by (auto split: option.split list.split if_split_asm)
qed

  text_raw‹
  \begin{verbatim}
  3. An alternative form that is sometimes more convenient when dealing
      with a mixed environment of IPv4 and IPv6 nodes is
      x:x:x:x:x:x:d.d.d.d, where the 'x's are the hexadecimal values of
      the six high-order 16-bit pieces of the address, and the 'd's are
      the decimal values of the four low-order 8-bit pieces of the
      address (standard IPv4 representation).  Examples:

         0:0:0:0:0:0:13.1.68.3
         0:0:0:0:0:FFFF:129.144.52.38

      or in compressed form:

         ::13.1.68.3
         ::FFFF:129.144.52.38
  \end{verbatim}

  This is currently not supported by our library!
›
  (*TODO*)
  (*TODO: oh boy, they can also be compressed*)

subsection‹Semantics›
  fun ipv6preferred_to_int :: "ipv6addr_syntax  ipv6addr" where
    "ipv6preferred_to_int (IPv6AddrPreferred a b c d e f g h) = (ucast a << (16 * 7)) OR
                                                                (ucast b << (16 * 6)) OR
                                                                (ucast c << (16 * 5)) OR
                                                                (ucast d << (16 * 4)) OR
                                                                (ucast e << (16 * 3)) OR
                                                                (ucast f << (16 * 2)) OR
                                                                (ucast g << (16 * 1)) OR
                                                                (ucast h << (16 * 0))"

  lemma "ipv6preferred_to_int (IPv6AddrPreferred 0x2001 0xDB8 0x0 0x0 0x8 0x800 0x200C 0x417A) = 
          42540766411282592856906245548098208122" by eval

  lemma "ipv6preferred_to_int (IPv6AddrPreferred 0xFF01 0x0 0x0 0x0 0x0 0x0 0x0 0x101) = 
          338958331222012082418099330867817087233" by eval

  declare ipv6preferred_to_int.simps[simp del]


  definition int_to_ipv6preferred :: "ipv6addr  ipv6addr_syntax" where
    "int_to_ipv6preferred i = IPv6AddrPreferred (ucast ((i AND 0xFFFF0000000000000000000000000000) >> 16*7))
                                                (ucast ((i AND 0xFFFF000000000000000000000000) >> 16*6))
                                                (ucast ((i AND 0xFFFF00000000000000000000) >> 16*5))
                                                (ucast ((i AND 0xFFFF0000000000000000) >> 16*4))
                                                (ucast ((i AND 0xFFFF000000000000) >> 16*3))
                                                (ucast ((i AND 0xFFFF00000000) >> 16*2))
                                                (ucast ((i AND 0xFFFF0000) >> 16*1))
                                                (ucast ((i AND 0xFFFF)))"

  lemma "int_to_ipv6preferred 42540766411282592856906245548098208122 =
         IPv6AddrPreferred 0x2001 0xDB8 0x0 0x0 0x8 0x800 0x200C 0x417A" by eval

  lemma word128_masks_ipv6pieces:
    "(0xFFFF0000000000000000000000000000::ipv6addr) = (mask 16) << 112"
    "(0xFFFF000000000000000000000000::ipv6addr) = (mask 16) << 96"
    "(0xFFFF00000000000000000000::ipv6addr) = (mask 16) << 80"
    "(0xFFFF0000000000000000::ipv6addr) = (mask 16) << 64"
    "(0xFFFF000000000000::ipv6addr) = (mask 16) << 48"
    "(0xFFFF00000000::ipv6addr) = (mask 16) << 32"
    "(0xFFFF0000::ipv6addr) = (mask 16) << 16"
    "(0xFFFF::ipv6addr) = (mask 16)"
    by(simp add: mask_eq)+


  text‹Correctness: round trip property one›
  lemma ipv6preferred_to_int_int_to_ipv6preferred:
    "ipv6preferred_to_int (int_to_ipv6preferred ip) = ip"
  proof -
    have and_mask_shift_helper: "w AND (mask m << n) >> n << n = w AND (mask m << n)"
      for m n::nat and w::ipv6addr
      by (metis is_aligned_shift is_aligned_shiftr_shiftl shiftr_and_eq_shiftl)
    have ucast_ipv6_piece_rule:
      "length (dropWhile Not (to_bl w))  16  (ucast::16 word  128 word) ((ucast::128 word  16 word) w) = w"
      for w::ipv6addr 
      by(rule ucast_short_ucast_long_ingoreLeadingZero) (simp_all)
    have ucast_ipv6_piece: "16  128 - n  
      (ucast::16 word  128 word) ((ucast::128 word  16 word) (w AND (mask 16 << n) >> n)) << n = w AND (mask 16 << n)"
      for w::ipv6addr and n::nat
      apply(subst ucast_ipv6_piece_rule)
       apply(rule length_drop_mask_inner)
       apply(simp; fail)
      apply(subst and_mask_shift_helper)
      apply simp
      done

    have ucast16_ucast128_masks_highest_bits:
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF0000000000000000000000000000 >> 112)) << 112) = 
             (ip AND 0xFFFF0000000000000000000000000000)"
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF000000000000000000000000 >> 96)) << 96) =
           ip AND 0xFFFF000000000000000000000000"
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF00000000000000000000 >> 80)) << 80) =
           ip AND 0xFFFF00000000000000000000" 
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF0000000000000000 >> 64)) << 64) =
           ip AND 0xFFFF0000000000000000"
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF000000000000 >> 48)) << 48) =
           ip AND 0xFFFF000000000000"
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF00000000 >> 32)) << 32) =
           ip AND 0xFFFF00000000"
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF0000 >> 16)) << 16) =
           ip AND 0xFFFF0000"
      by((subst word128_masks_ipv6pieces)+, subst ucast_ipv6_piece, simp_all)+

    have ucast16_ucast128_masks_highest_bits0: 
      "(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF))) = ip AND 0xFFFF"
      apply(subst word128_masks_ipv6pieces)+
      apply(subst ucast_short_ucast_long_ingoreLeadingZero)
        apply simp_all
      by (simp add: length_drop_mask)

    have mask_len_word:"n = (LENGTH('a))  w AND mask n = w"
      for n and w::"'a::len word" by (simp add: mask_eq_iff) 

    have ipv6addr_16word_pieces_compose_or:
            "ip && (mask 16 << 112) ||
             ip && (mask 16 << 96) ||
             ip && (mask 16 << 80) ||
             ip && (mask 16 << 64) ||
             ip && (mask 16 << 48) ||
             ip && (mask 16 << 32) ||
             ip && (mask 16 << 16) ||
             ip && mask 16 =
             ip"
      apply(subst word_ao_dist2[symmetric])+
      apply(simp add: mask_eq)
      apply(subst mask128)
      apply(rule mask_len_word)
      apply simp
      done

    show ?thesis
      apply(simp add: ipv6preferred_to_int.simps int_to_ipv6preferred_def)
      apply(simp add: ucast16_ucast128_masks_highest_bits ucast16_ucast128_masks_highest_bits0)
      apply(simp add: word128_masks_ipv6pieces)
      apply(rule ipv6addr_16word_pieces_compose_or)
      done
  qed


  text‹Correctness: round trip property two›
  lemma int_to_ipv6preferred_ipv6preferred_to_int: "int_to_ipv6preferred (ipv6preferred_to_int ip) = ip"
  proof -
    note ucast_shift_simps=helper_masked_ucast_generic helper_masked_ucast_reverse_generic
                           helper_masked_ucast_generic[where n=0, simplified]
                           helper_masked_ucast_equal_generic 
    note ucast_simps=helper_masked_ucast_reverse_generic[where m=0, simplified]
                     helper_masked_ucast_equal_generic[where n=0, simplified]
    show ?thesis
    apply(cases ip, rename_tac a b c d e f g h)
    apply(simp add: ipv6preferred_to_int.simps int_to_ipv6preferred_def)
    apply(simp add: word128_masks_ipv6pieces)
    apply(simp add: word_ao_dist ucast_shift_simps ucast_simps)
    done
  qed



text‹compressed to preferred format›
fun ipv6addr_c2p :: "ipv6addr_syntax_compressed  ipv6addr_syntax" where
    "ipv6addr_c2p (IPv6AddrCompressed1_0 ()) = IPv6AddrPreferred 0 0 0 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed1_1 () h) = IPv6AddrPreferred 0 0 0 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_2 () g h) = IPv6AddrPreferred 0 0 0 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_3 () f g h) = IPv6AddrPreferred 0 0 0 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_4 () e f g h) = IPv6AddrPreferred 0 0 0 0 e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_5 () d e f g h) = IPv6AddrPreferred 0 0 0 d e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_6 () c d e f g h) = IPv6AddrPreferred 0 0 c d e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_7 () b c d e f g h) = IPv6AddrPreferred 0 b c d e f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed2_1 a ()) = IPv6AddrPreferred a 0 0 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed2_2 a () h) = IPv6AddrPreferred a 0 0 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_3 a () g h) = IPv6AddrPreferred a 0 0 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_4 a () f g h) = IPv6AddrPreferred a 0 0 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_5 a () e f g h) = IPv6AddrPreferred a 0 0 0 e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_6 a () d e f g h) = IPv6AddrPreferred a 0 0 d e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_7 a () c d e f g h) = IPv6AddrPreferred a 0 c d e f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed3_2 a b ()) = IPv6AddrPreferred a b 0 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed3_3 a b () h) = IPv6AddrPreferred a b 0 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed3_4 a b () g h) = IPv6AddrPreferred a b 0 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed3_5 a b () f g h) = IPv6AddrPreferred a b 0 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed3_6 a b () e f g h) = IPv6AddrPreferred a b 0 0 e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed3_7 a b () d e f g h) = IPv6AddrPreferred a b 0 d e f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed4_3 a b c ()) = IPv6AddrPreferred a b c 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed4_4 a b c () h) = IPv6AddrPreferred a b c 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed4_5 a b c () g h) = IPv6AddrPreferred a b c 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed4_6 a b c () f g h) = IPv6AddrPreferred a b c 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed4_7 a b c () e f g h) = IPv6AddrPreferred a b c 0 e f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed5_4 a b c d ()) = IPv6AddrPreferred a b c d 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed5_5 a b c d () h) = IPv6AddrPreferred a b c d 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed5_6 a b c d () g h) = IPv6AddrPreferred a b c d 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed5_7 a b c d () f g h) = IPv6AddrPreferred a b c d 0 f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed6_5 a b c d e ()) = IPv6AddrPreferred a b c d e 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed6_6 a b c d e () h) = IPv6AddrPreferred a b c d e 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed6_7 a b c d e () g h) = IPv6AddrPreferred a b c d e 0 g h"

  | "ipv6addr_c2p (IPv6AddrCompressed7_6 a b c d e f ()) = IPv6AddrPreferred a b c d e f 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed7_7 a b c d e f () h) = IPv6AddrPreferred a b c d e f 0 h"

  | "ipv6addr_c2p (IPv6AddrCompressed8_7 a b c d e f g ()) = IPv6AddrPreferred a b c d e f g 0"


definition ipv6_unparsed_compressed_to_preferred :: "((16 word) option) list  ipv6addr_syntax option" where
  "ipv6_unparsed_compressed_to_preferred ls = (
    if
      length (filter (λp. p = None) ls)  1  length (filter (λp. p  None) ls) > 7
    then
      None
    else
      let
        before_omission = map the (takeWhile (λx. x  None) ls);
        after_omission = map the (drop 1 (dropWhile (λx. x  None) ls));
        num_omissions = 8 - (length before_omission + length after_omission);
        expanded = before_omission @ (replicate num_omissions 0) @ after_omission
      in
        case expanded of [a,b,c,d,e,f,g,h]  Some (IPv6AddrPreferred a b c d e f g h)
                         | _                None
      )"

  lemma "ipv6_unparsed_compressed_to_preferred
    [Some 0x2001, Some 0xDB8, None, Some 0x8, Some 0x800, Some 0x200C, Some 0x417A]
      = Some (IPv6AddrPreferred 0x2001 0xDB8 0 0 8 0x800 0x200C 0x417A)" by eval

  lemma "ipv6_unparsed_compressed_to_preferred [None] = Some (IPv6AddrPreferred 0 0 0 0 0 0 0 0)" by eval

  lemma "ipv6_unparsed_compressed_to_preferred [] = None" by eval


  lemma ipv6_unparsed_compressed_to_preferred_identity1:
   "ipv6_unparsed_compressed_to_preferred (ipv6addr_syntax_compressed_to_list ipv6compressed) = Some ipv6prferred
     ipv6addr_c2p ipv6compressed = ipv6prferred"
    by (cases ipv6compressed) (simp_all add: ipv6_unparsed_compressed_to_preferred_def numeral_eq_Suc) (*1s*)
 
  lemma ipv6_unparsed_compressed_to_preferred_identity2: 
    "ipv6_unparsed_compressed_to_preferred ls = Some ipv6prferred
      (ipv6compressed. parse_ipv6_address_compressed ls = Some ipv6compressed 
                           ipv6addr_c2p ipv6compressed = ipv6prferred)"
  apply(rule iffI)
   apply(subgoal_tac "parse_ipv6_address_compressed ls  None")
    prefer 2
    apply(subst RFC_4291_format)
    apply(simp add: ipv6_unparsed_compressed_to_preferred_def split: if_split_asm; fail)
   apply(simp)
   apply(erule exE, rename_tac ipv6compressed)
   apply(rule_tac x="ipv6compressed" in exI)
   apply(simp)
   apply(subgoal_tac "(ipv6addr_syntax_compressed_to_list ipv6compressed = ls)")
    prefer 2
    using parse_ipv6_address_compressed_identity2 apply presburger
   using ipv6_unparsed_compressed_to_preferred_identity1 apply blast
  apply(erule exE, rename_tac ipv6compressed)
  apply(subgoal_tac "(ipv6addr_syntax_compressed_to_list ipv6compressed = ls)")
   prefer 2
   using parse_ipv6_address_compressed_identity2 apply presburger
  using ipv6_unparsed_compressed_to_preferred_identity1 apply blast
  done
  

subsection‹IPv6 Pretty Printing (converting to compressed format)›
text_raw‹
RFC5952:
\begin{verbatim}
4.  A Recommendation for IPv6 Text Representation

   A recommendation for a canonical text representation format of IPv6
   addresses is presented in this section.  The recommendation in this
   document is one that complies fully with [RFC4291], is implemented by
   various operating systems, and is human friendly.  The recommendation
   in this section SHOULD be followed by systems when generating an
   address to be represented as text, but all implementations MUST
   accept and be able to handle any legitimate [RFC4291] format.  It is
   advised that humans also follow these recommendations when spelling
   an address.

4.1.  Handling Leading Zeros in a 16-Bit Field

   Leading zeros MUST be suppressed.  For example, 2001:0db8::0001 is
   not acceptable and must be represented as 2001:db8::1.  A single 16-
   bit 0000 field MUST be represented as 0.

4.2.  "::" Usage

4.2.1.  Shorten as Much as Possible

   The use of the symbol "::" MUST be used to its maximum capability.
   For example, 2001:db8:0:0:0:0:2:1 must be shortened to 2001:db8::2:1.
   Likewise, 2001:db8::0:1 is not acceptable, because the symbol "::"
   could have been used to produce a shorter representation 2001:db8::1.

4.2.2.  Handling One 16-Bit 0 Field

   The symbol "::" MUST NOT be used to shorten just one 16-bit 0 field.
   For example, the representation 2001:db8:0:1:1:1:1:1 is correct, but
   2001:db8::1:1:1:1:1 is not correct.

4.2.3.  Choice in Placement of "::"

   When there is an alternative choice in the placement of a "::", the
   longest run of consecutive 16-bit 0 fields MUST be shortened (i.e.,
   the sequence with three consecutive zero fields is shortened in 2001:
   0:0:1:0:0:0:1).  When the length of the consecutive 16-bit 0 fields
   are equal (i.e., 2001:db8:0:0:1:0:0:1), the first sequence of zero
   bits MUST be shortened.  For example, 2001:db8::1:0:0:1 is correct
   representation.

4.3.  Lowercase

   The characters "a", "b", "c", "d", "e", and "f" in an IPv6 address
   MUST be represented in lowercase.
\end{verbatim}
›
text‹See @{file ‹IP_Address_toString.thy›} for examples and test cases.›
context
begin
  private function goup_by_zeros :: "16 word list  16 word list list" where
    "goup_by_zeros [] = []" |
    "goup_by_zeros (x#xs) = (
        if x = 0
        then takeWhile (λx. x = 0) (x#xs) # (goup_by_zeros (dropWhile (λx. x = 0) xs))
        else [x]#(goup_by_zeros xs))"
  by(pat_completeness, auto)
  
  termination goup_by_zeros
	 apply(relation "measure (λxs. length xs)")
	   apply(simp_all)
	 by (simp add: le_imp_less_Suc length_dropWhile_le)
	
	private lemma "goup_by_zeros [0,1,2,3,0,0,0,0,3,4,0,0,0,2,0,0,2,0,3,0] =
	        [[0], [1], [2], [3], [0, 0, 0, 0], [3], [4], [0, 0, 0], [2], [0, 0], [2], [0], [3], [0]]"
	by eval
	
	private lemma "concat (goup_by_zeros ls) = ls"
	  by(induction ls rule:goup_by_zeros.induct) simp+
	
	private lemma "[]  set (goup_by_zeros ls)"
	  by(induction ls rule:goup_by_zeros.induct) simp+
	  
  private primrec List_replace1 :: "'a  'a  'a list  'a list" where
    "List_replace1 _ _ [] = []" |
    "List_replace1 a b (x#xs) = (if a = x then b#xs else x#List_replace1 a b xs)"
    
	private lemma "List_replace1 a a ls = ls"
	  by(induction ls) simp_all
	
	private lemma "a  set ls  List_replace1 a b ls = ls"
	  by(induction ls) simp_all
	
	private lemma "a  set ls  b  set (List_replace1 a b ls)"
	  apply(induction ls)
	   apply(simp)
	  apply(simp)
	  by blast
  
	private fun List_explode :: "'a list list  ('a option) list" where
	  "List_explode [] = []" |
	  "List_explode ([]#xs) = None#List_explode xs" |
	  "List_explode (xs1#xs2) = map Some xs1@List_explode xs2"
	  
  private lemma "List_explode [[0::int], [2,3], [], [3,4]] = [Some 0, Some 2, Some 3, None, Some 3, Some 4]"
  by eval

  private lemma List_explode_def: 
    "List_explode xss = concat (map (λxs. if xs = [] then [None] else map Some xs) xss)"
    by(induction xss rule: List_explode.induct) simp+
	  
  private lemma List_explode_no_empty: "[]  set xss  List_explode xss = map Some (concat xss)"
    by(induction xss rule: List_explode.induct) simp+

  private lemma List_explode_replace1: "[]  set xss  foo  set xss 
          List_explode (List_replace1 foo [] xss) =
            map Some (concat (takeWhile (λxs. xs  foo) xss)) @ [None] @
              map Some (concat (tl (dropWhile (λxs. xs  foo) xss)))"
    apply(induction xss rule: List_explode.induct)
      apply(simp; fail)
     apply(simp; fail)
    apply(simp)
    apply safe
      apply(simp_all add: List_explode_no_empty)
    done
    
  fun ipv6_preferred_to_compressed :: "ipv6addr_syntax  ((16 word) option) list" where
  "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (
    let lss = goup_by_zeros [a,b,c,d,e,f,g,h];
        max_zero_seq = foldr (λxs. max (length xs)) lss 0;
        shortened = if max_zero_seq > 1 then List_replace1 (replicate max_zero_seq 0) [] lss else lss
    in
      List_explode shortened
    )"
  declare ipv6_preferred_to_compressed.simps[simp del]

  private lemma foldr_max_length: "foldr (λxs. max (length xs)) lss n = fold max (map length lss) n"
    apply(subst List.foldr_fold)
     apply fastforce
    apply(induction lss arbitrary: n)
     apply(simp; fail)
    apply(simp)
    done

  private lemma List_explode_goup_by_zeros: "List_explode (goup_by_zeros xs) = map Some xs"
    apply(induction xs rule: goup_by_zeros.induct)
     apply(simp; fail)
    apply(simp)
    apply(safe)
     apply(simp)
    by (metis map_append takeWhile_dropWhile_id)
  
  private definition "max_zero_streak xs  foldr (λxs. max (length xs)) (goup_by_zeros xs) 0"    

  private lemma max_zero_streak_def2: "max_zero_streak xs = fold max (map length (goup_by_zeros xs)) 0"
    unfolding max_zero_streak_def
    by(simp add: foldr_max_length)

  private lemma ipv6_preferred_to_compressed_pull_out_if:
    "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (
    if max_zero_streak [a,b,c,d,e,f,g,h] > 1 then
      List_explode (List_replace1 (replicate (max_zero_streak [a,b,c,d,e,f,g,h]) 0) [] (goup_by_zeros [a,b,c,d,e,f,g,h]))
    else
      map Some [a,b,c,d,e,f,g,h]
    )"
  by(simp add: ipv6_preferred_to_compressed.simps max_zero_streak_def List_explode_goup_by_zeros)

    
  private lemma "ipv6_preferred_to_compressed (IPv6AddrPreferred 0 0 0 0 0 0 0 0) = [None]" by eval
  private lemma "ipv6_preferred_to_compressed (IPv6AddrPreferred 0x2001 0xDB8 0 0 8 0x800 0x200C 0x417A) =
                [Some 0x2001, Some 0xDB8, None,           Some 8, Some 0x800, Some 0x200C, Some 0x417A]" by eval
  private lemma "ipv6_preferred_to_compressed (IPv6AddrPreferred 0x2001 0xDB8 0 3 8 0x800 0x200C 0x417A) =
                [Some 0x2001, Some 0xDB8, Some 0, Some 3, Some 8, Some 0x800, Some 0x200C, Some 0x417A]" by eval

  (*the output should even conform to RFC5952, ...*)
  lemma ipv6_preferred_to_compressed_RFC_4291_format:
    "ipv6_preferred_to_compressed ip = as  
          length (filter (λp. p = None) as) = 0  length as = 8
          
          length (filter (λp. p = None) as) = 1  length (filter (λp. p  None) as)  7"
  apply(cases ip)
  apply(simp add: ipv6_preferred_to_compressed_pull_out_if)
  apply(simp only: split: if_split_asm)
   subgoal for a b c d e f g h
   apply(rule disjI2)
   apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
         case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
   by(auto simp add: max_zero_streak_def) (*1min*)
  subgoal
  apply(rule disjI1)
  apply(simp)
  by force
  done

  ― ‹Idea for the following proof:›
  private lemma "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = None#xs 
      xs = map Some (dropWhile (λx. x=0) [a,b,c,d,e,f,g,h])"
    apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
          case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
    by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*20s*)


 
  lemma ipv6_preferred_to_compressed:
    assumes "ipv6_unparsed_compressed_to_preferred (ipv6_preferred_to_compressed ip) = Some ip'"
    shows "ip = ip'"
  proof -
    from assms have 1: "ipv6compressed.
         parse_ipv6_address_compressed (ipv6_preferred_to_compressed ip) = Some ipv6compressed 
         ipv6addr_c2p ipv6compressed = ip'" using ipv6_unparsed_compressed_to_preferred_identity2 by simp
  
    obtain a b c d e f g h where ip: "ip = IPv6AddrPreferred a b c d e f g h" by(cases ip)
  
    have ipv6_preferred_to_compressed_None1:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = None#xs 
        (map Some (dropWhile (λx. x=0) [a,b,c,d,e,f,g,h]) = xs  (IPv6AddrPreferred a b c d e f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None2:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#None#xs 
        (map Some (dropWhile (λx. x=0) [b,c,d,e,f,g,h]) = xs  (IPv6AddrPreferred a' b c d e f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None3:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#None#xs 
        (map Some (dropWhile (λx. x=0) [c,d,e,f,g,h]) = xs  (IPv6AddrPreferred a' b' c d e f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a' b'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None4:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#(Some c')#None#xs 
        (map Some (dropWhile (λx. x=0) [d,e,f,g,h]) = xs  (IPv6AddrPreferred a' b' c' d e f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a' b' c'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None5:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#(Some c')#(Some d')#None#xs 
        (map Some (dropWhile (λx. x=0) [e,f,g,h]) = xs  (IPv6AddrPreferred a' b' c' d' e f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a' b' c' d'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None6:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#(Some c')#(Some d')#(Some e')#None#xs 
        (map Some (dropWhile (λx. x=0) [f,g,h]) = xs  (IPv6AddrPreferred a' b' c' d' e' f g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a' b' c' d' e'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None7:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#(Some c')#(Some d')#(Some e')#(Some f')#None#xs 
        (map Some (dropWhile (λx. x=0) [g,h]) = xs  (IPv6AddrPreferred a' b' c' d' e' f' g h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'"  for xs a' b' c' d' e' f'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "e=0",case_tac [!] "f=0",case_tac [!] "g=0",case_tac [!] "h=0")
      by(simp_all add: ipv6_preferred_to_compressed_pull_out_if max_zero_streak_def) (*5s*)
    have ipv6_preferred_to_compressed_None8:
      "ipv6_preferred_to_compressed (IPv6AddrPreferred a b c d e f g h) = (Some a')#(Some b')#(Some c')#(Some d')#(Some e')#(Some f')#(Some g')#None#xs 
        (map Some (dropWhile (λx. x=0) [h]) = xs  (IPv6AddrPreferred a' b' c' d' e' f' g' h) = ip') 
        (IPv6AddrPreferred a b c d e f g h) = ip'" for xs a' b' c' d' e' f' g'
      apply(case_tac "a=0",case_tac [!] "b=0",case_tac [!] "c=0",case_tac [!] "d=0",
            case_tac [!] "