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