# 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

"(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)))"
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

shows "LENGTH('a) - n' = len ⟹ length (dropWhile Not (to_bl (ip AND (mask n << n') >> n'))) ≤ len"
apply(subst shiftl_shiftr1)
apply(simp; fail)
apply(simp)
done
shows "n ≤ LENGTH('a) - n' ⟹ length (dropWhile Not (to_bl (ip AND (mask n << n') >> n'))) ≤ n"
apply(subst shiftl_shiftr3)
apply(simp; fail)
apply(simp)
done

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

(*n small, m large*)
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 shiftr_div_2n_w)
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*)
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
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(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)+
subgoal by (fact aligned)
done
qed

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"
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 shiftl_shiftr3)
apply(simp; fail)
apply(simp)
apply(subst shiftl_shiftr3)
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
(*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
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"
lemma Empty_WordInterval_set_eq[simp]: "wordinterval_to_set Empty_WordInterval = {}"

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"

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)"

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"

lemma wordinterval_optimize_empty_double:
"wordinterval_optimize_empty (wordinterval_optimize_empty r) = wordinterval_optimize_empty r"

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)
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)
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(intro impI conjI)
apply(drule not_disjoint_union)
apply blast
apply(drule_tac C="(⋃x∈set 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(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)
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(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(blast dest: A_in_listwordinterval_compress)+
done
text‹END merging overlapping intervals›

:: "(('a::len) word × ('a::len) word) ⇒ ('a word × 'a word) list ⇒ ('a word × 'a word) list"
where
"merge_adjacent s [] = [s]" |
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

"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(intro impI conjI)
apply(elim conjE)
subgoal by (blast)
by blast

"∃(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)
by blast

:: "(('a::len) word × ('a::len) word) list ⇒ ('a word × 'a word) list" where
if ∀(s',e') ∈ set ss. ¬ (s ≤e ∧ s' ≤ e' ∧ (word_next e = s' ∨ word_next e' = s))
by(pat_completeness, auto)

apply (relation "measure length")
apply(rule wf_measure)
apply(simp)
apply(simp)

"(⋃s ∈ set (listwordinterval_adjacent ss). interval_of s) = (⋃s ∈ set ss. interval_of s)"
apply(simp)
done

lemma "listwordinterval_adjacent [(1::16 word, 3), (5, 10), (10,10), (4,4)] = [(10, 10), (1, 10)]"
by eval

definition wordinterval_compress :: "('a::len) wordinterval ⇒ 'a wordinterval" where
"wordinterval_compress r ≡
(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)

(listwordinterval_compress (wi2l (wordinterval_optimize_empty r)))))) =
(wi2l (wordinterval_optimize_empty r)))). interval_of x)"
by (force simp: interval_of' l2wi)
also have "… =  (⋃s∈set (wi2l (wordinterval_optimize_empty r)). interval_of s)"
also have "… = (⋃(i, j)∈set (wi2l (wordinterval_optimize_empty r)). {i..j})"
also have "… = wordinterval_to_set r" by(simp add: wi2l)
finally show "wordinterval_to_set
(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"
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"
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)
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 ∧ (∀y∈S. y ≤ x ⟶ y = x))"

lemma
fixes x :: "'a :: complete_lattice"
assumes "x ∈ S"
shows " x = Inf S ⟹ is_lowest_element x S"

lemma
fixes x :: "'a :: linorder"
assumes "finite S" and "x ∈ S"
shows "is_lowest_element x S ⟷ x = Min S"
apply(rule)
subgoal
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 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)"

(*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(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(drule is_lowest_RangeUnion)
apply(elim disjE)

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)
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"

lemma uncurry_curry_id: "uncurry ∘ curry = id" "curry ∘ uncurry = id"

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


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

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

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

definition max_ip_addr :: "'i::len word" where
"max_ip_addr ≡ of_nat ((2^(len_of(TYPE('i)))) - 1)"

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

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

(*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
let
in
{network_prefix .. network_prefix OR (NOT netmask)}"

text‹Example (pseudo syntax):
‹{192.168.1.0 .. 192.168.1.255}››

text‹A network mask of all ones (i.e. @{term "(- 1)::'i::len word"}).›

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

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"

lemma ipset_from_cidr_0: "ipset_from_cidr ip 0 = UNIV"

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}"

text‹Alternative definition: Considering words as bit lists:›
lemma ipset_from_cidr_bl:
(replicate ((len_of(TYPE('i))) - pflength)) False))"

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)}"
done

lemma ipset_from_cidr_alt2:
fixes base ::"'i::len word"
shows "ipset_from_cidr base len =

text‹In CIDR notation, we cannot express the empty set.›
lemma ipset_from_cidr_not_empty: "ipset_from_cidr base len ≠ {}"

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 -
"((mask l << LENGTH('i) - l) :: 'i::len word) = NOT (mask (LENGTH('i) - l))"
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
{base .. base || mask (LENGTH('i) - l)}"
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
qed

fixes base :: "'i::len word"
=

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 -
"((mask len << LENGTH('a) - len) :: 'a::len word) = NOT (mask (LENGTH('a) - len))"
have 1: "mask (len - m) AND base AND NOT (mask (len - m)) = 0"
for len m and base::"'i::len word"
have 2: "mask (LENGTH('i) - len) AND pfxm_p = 0 ⟹
(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
(base && ~~ (mask (LENGTH('i) - len)) = x && ~~ (mask (LENGTH('i) - len)))" for x
unfolding word_bw_comms(1)[of _ " ~~ (mask (LENGTH('i) - len))"] by simp
then show ?thesis
unfolding ip_cidr_set_def ipset_from_cidr_def
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)

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"

lemma "wordinterval_to_set (iprange_single ip) = {ip}"
lemma "wordinterval_to_set (iprange_interval (ip1, ip2)) = {ip1 .. ip2}"

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

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) = (
in network_prefix)"
fun ipcidr_to_interval_end :: "('i::len word × nat) ⇒ 'i::len word" where
"ipcidr_to_interval_end (pre, len) = (
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)}"
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}"

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

lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry:
"wordinterval_to_set (ipcidr_tuple_to_wordinterval ipcidr) = uncurry ipset_from_cidr ipcidr"

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)"

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*)
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 && _")
also have "?w = x && ~~ (mask r2)" by fact
also have "… && ~~ (mask r1) = x && ~~ (mask r1)"
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 = {}"
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)
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›
"(addr::'i::len word) ∈ (ipset_from_cidr pre len) ⟷
unfolding ipset_from_cidr_alt by simp

end


# Theory IPv4

(*  Title:      IPv4.thy
Authors:    Cornelius Diekmann, Julius Michaelis
*)
theory IPv4
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

text‹An IPv4 address is basically a 32 bit unsigned integer.›

text‹Conversion between natural numbers and IPv4 adresses›

lemma UNIV_ipv4addrset: "UNIV = {0 .. max_ipv4_addr}" (*not in the simp set, for a reason*)

text‹identity functions›

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
nat_of_ipv4addr ((a >> 16) AND 0xFF),
nat_of_ipv4addr ((a >> 8) AND 0xFF),

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

text‹a different notation for @{term ipv4addr_of_dotdecimal}›
proof -
{ fix x y
apply(induction x arbitrary: y)
} from this a b c
show ?thesis
apply(thin_tac _)+
by presburger
qed

"⟦ a < 256; b < 256; c < 256; d < 256 ⟧ ⟹
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 transfer
done
for a
apply transfer
done
from assms have b:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 16) AND mask 8) = b"
apply transfer
using div65536
done
from assms have c:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 8) AND mask 8) = c"
apply transfer
using div256
done
from ‹d < 256› have d: "nat_of_ipv4addr (ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) AND mask 8) = d"
apply transfer
done
from a b c d show ?thesis
done
qed

proof -
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 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))"
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 ...*)
apply(subst blip_split)
apply(simp; fail)
done
thus ?thesis using word_bl.Rep_inverse[symmetric] by simp
qed

a < 256; b < 256; c < 256; d < 256; e < 256; f < 256; g < 256; h < 256 ⟧ ⟹
a = e ∧ b = f ∧ c = g ∧ d = h"

subsection‹IP Ranges: Examples›

(*Warning, not executable!*)

text‹192.168.0.0/24›

lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,42)) 16 =

lemma "ip ∈ (ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 0)"

shows "ipset_from_cidr pre len = {(pre AND ((mask len) << (32 - len))) .. pre OR (mask (32 - len))}"

text‹making element check executable›
shows "addr ∈ (ipset_from_cidr pre len) ⟷

(*small numbers because we didn't load Code_Target_Nat. Should work by eval*)

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) = (
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
NumberWang_IPv6
(* include "HOL-Library.Code_Target_Nat" if you need to work with actual numbers.*)
begin

text‹An IPv6 address is basically a 128 bit unsigned integer. RFC 4291, Section 2.›

text‹Conversion between natural numbers and IPv6 adresses›

lemma "ipv6addr_of_nat n = word_of_int (int n)"

lemma UNIV_ipv6addrset: "UNIV = {0 .. max_ipv6_addr}" (*not in the simp set, for a reason*)

text‹identity functions›

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
Examples:
ABCD:EF01:2345:6789:ABCD:EF01:2345:6789
2001:DB8:0:0:8:800:200C:417A
\end{verbatim}
›
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

may be represented as
\end{verbatim}
›
(*datatype may take some minutes to load*)
― ‹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_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_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):
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', '']
*)
"parse_ipv6_address_compressed as = (case as of
| [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.›
)"

where
[None]"
[None, Some a]"
[None, Some a, Some b]"
[None, Some a, Some b, Some c]"
[None, Some a, Some b, Some c, Some d]"
[None, Some a, Some b, Some c, Some d, Some e]"
[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]"

[Some a, None]"
[Some a, None, Some b]"
[Some a, None, Some b, Some c]"
[Some a, None, Some b, Some c, Some d]"
[Some a, None, Some b, Some c, Some d, Some e]"
[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]"
[Some a, Some b, None, Some c]"
[Some a, Some b, None, Some c, Some d]"
[Some a, Some b, None, Some c, Some d, Some e]"
[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]"

[Some a, Some b, Some c, None]"
[Some a, Some b, Some c, None, Some d]"
[Some a, Some b, Some c, None, Some d, Some e]"
[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]"

[Some a, Some b, Some c, Some d, None]"
[Some a, Some b, Some c, Some d, None, Some e]"
[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]"

[Some a, Some b, Some c, Some d, Some e, None]"
[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]"

[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*)
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"
qed

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
by (auto split: list.split_asm option.split_asm) (* takes a minute *)

(is "?lhs = ?rhs")
proof
assume ?rhs
thus ?lhs
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
by blast
thus ?rhs
next
assume ?rhs
thus ?lhs
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

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›
"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]

"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

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)"
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"
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)"
apply(subst ucast_ipv6_piece_rule)
apply(simp; fail)
apply simp
done

"(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"

"(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF))) = ip AND 0xFFFF"
apply simp_all

"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"
apply(subst word_ao_dist2[symmetric])+
apply simp
done

show ?thesis
done
qed

text‹Correctness: round trip property two›
lemma int_to_ipv6preferred_ipv6preferred_to_int: "int_to_ipv6preferred (ipv6preferred_to_int ip) = ip"
proof -
show ?thesis
apply(cases ip, rename_tac a b c d e f g h)
done
qed

text‹compressed to preferred format›
| "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_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_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
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 ∧
apply(rule iffI)
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)
prefer 2
using ipv6_unparsed_compressed_to_preferred_identity1 apply blast
apply(erule exE, rename_tac ipv6compressed)
prefer 2
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

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)

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
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

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]
)"

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 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")
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")

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")
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")
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")
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")
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")
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")
case_tac [!] "