Theory IpAddresses
theory IpAddresses
imports IP_Addresses.IP_Address_toString
IP_Addresses.CIDR_Split
"../Common/WordInterval_Lists"
begin
lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 33 = {0}"
by(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def ipset_from_cidr_large_pfxlen)
definition all_but_those_ips :: "('i::len word × nat) list ⇒ ('i word × nat) list" where
"all_but_those_ips cidrips = cidr_split (wordinterval_invert (l2wi (map ipcidr_to_interval cidrips)))"
lemma all_but_those_ips:
"ipcidr_union_set (set (all_but_those_ips cidrips)) =
UNIV - (⋃ (ip,n) ∈ set cidrips. ipset_from_cidr ip n)"
apply simp
unfolding ipcidr_union_set_uncurry all_but_those_ips_def
apply(simp add: cidr_split_prefix)
apply(simp add: l2wi)
apply(simp add: ipcidr_to_interval_def)
using ipset_from_cidr_ipcidr_to_interval by blast
section‹IPv4 Addresses›
subsection‹IPv4 Addresses in IPTables Notation (how we parse it)›
context
notes [[typedef_overloaded]]
begin