[STATEMENT]
lemma src_ipPart_motivation:
fixes   rs
defines "X \<equiv> (\<lambda>(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs"
assumes "\<forall>A \<in> X. B \<subseteq> A \<or> B \<inter> A = {}" and "s1 \<in> B" and "s2 \<in> B"
shows "simple_fw rs (p\<lparr>p_src:=s1\<rparr>) = simple_fw rs (p\<lparr>p_src:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
have "\<forall>A \<in> (\<lambda>(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw [] (p\<lparr>p_src := s1\<rparr>) = simple_fw [] (p\<lparr>p_src := s2\<rparr>)
 2. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {}

goal (2 subgoals):
 1. \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw [] (p\<lparr>p_src := s1\<rparr>) = simple_fw [] (p\<lparr>p_src := s2\<rparr>)
 2. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. simple_fw [] (p\<lparr>p_src := s1\<rparr>) = simple_fw [] (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
simple_fw [] (p\<lparr>p_src := s1\<rparr>) = simple_fw [] (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` src ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
from \<open>s1 \<in> B\<close> \<open>s2 \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> B
s2 \<in> B
[PROOF STEP]
have
        "B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa)
                      \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow>
             simple_matches m (p\<lparr>p_src := s1\<rparr>) \<longleftrightarrow> simple_matches m (p\<lparr>p_src := s2\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> B
s2 \<in> B

goal (1 subgoal):
 1. B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches m (p\<lparr>p_src := s1\<rparr>) = simple_matches m (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(cases m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface srca dst proto sports dports. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = srca, dst = dst, proto = proto, sports = sports, dports = dports\<rparr>\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_src := s1\<rparr>) = simple_matches m (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(rename_tac iiface oiface srca dst proto sports dports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface srca dst proto sports dports. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = srca, dst = dst, proto = proto, sports = sports, dports = dports\<rparr>\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_src := s1\<rparr>) = simple_matches m (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(case_tac srca)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface srca dst proto sports dports a b. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = srca, dst = dst, proto = proto, sports = sports, dports = dports\<rparr>; srca = (a, b)\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_src := s1\<rparr>) = simple_matches m (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(simp add: simple_matches.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface srca dst proto sports dports a b. \<lbrakk>B \<subseteq> ipset_from_cidr a b \<or> B \<inter> ipset_from_cidr a b = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = (a, b), dst = dst, proto = proto, sports = sports, dports = dports\<rparr>; srca = (a, b)\<rbrakk> \<Longrightarrow> (match_iface iiface (p_iiface p) \<and> match_iface oiface (p_oiface p) \<and> s1 \<in> ipset_from_cidr a b \<and> simple_match_ip dst (p_dst p) \<and> match_proto proto (p_proto p) \<and> simple_match_port sports (p_sport p) \<and> simple_match_port dports (p_dport p)) = (match_iface iiface (p_iiface p) \<and> match_iface oiface (p_oiface p) \<and> s2 \<in> ipset_from_cidr a b \<and> simple_match_ip dst (p_dst p) \<and> match_proto proto (p_proto p) \<and> simple_match_port sports (p_sport p) \<and> simple_match_port dports (p_dport p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches m (p\<lparr>p_src := s1\<rparr>) = simple_matches m (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_src := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
note helper=this
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_src := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` src ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
from Cons[simplified]
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
(B \<subseteq> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
(B \<subseteq> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {})

goal (1 subgoal):
 1. simple_fw (r # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(cases r, rename_tac m a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); (B \<subseteq> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a; \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); (B \<subseteq> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {})\<rbrakk> \<Longrightarrow> simple_fw (r # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; r = SimpleRule m a; simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; r = SimpleRule m a; simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; a = Accept\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s2\<rparr>)
 2. \<And>m a. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; r = SimpleRule m a; simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; a = Drop\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
using helper
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_src := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_src := s2\<rparr>)

goal (2 subgoals):
 1. \<And>m a. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; r = SimpleRule m a; simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; a = Accept\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s2\<rparr>)
 2. \<And>m a. \<lbrakk>B \<subseteq> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; r = SimpleRule m a; simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>); \<forall>A\<in>set rs. B \<subseteq> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case src (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; a = Drop\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
simple_fw (r # rs) (p\<lparr>p_src := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_src := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
X \<equiv> (\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs
\<forall>A\<in>X. B \<subseteq> A \<or> B \<inter> A = {}
s1 \<in> B
s2 \<in> B
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<equiv> (\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs
\<forall>A\<in>X. B \<subseteq> A \<or> B \<inter> A = {}
s1 \<in> B
s2 \<in> B
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma src_ipPart:
  assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) A"
          "B \<in> A" "s1 \<in> B" "s2 \<in> B"
  shows "simple_fw rs (p\<lparr>p_src:=s1\<rparr>) = simple_fw rs (p\<lparr>p_src:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
from src_ipPart_motivation[OF _ assms(3) assms(4)]
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set ?rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw ?rs (?p\<lparr>p_src := s1\<rparr>) = simple_fw ?rs (?p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
have "\<forall>A \<in> (\<lambda>(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow>
      simple_fw rs (p\<lparr>p_src:=s1\<rparr>) = simple_fw rs (p\<lparr>p_src:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set ?rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw ?rs (?p\<lparr>p_src := s1\<rparr>) = simple_fw ?rs (?p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. \<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) A
B \<in> A

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
unfolding ipPartition_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
\<forall>a\<in>set (map wordinterval_to_set (extract_IPSets_generic0 src rs)). \<forall>b\<in>A. a \<inter> b = {} \<or> b \<subseteq> a
B \<in> A

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)
[PROOF STEP]
by (metis (full_types) Int_commute extract_equi0)
[PROOF STATE]
proof (state)
this:
simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dst_ipPart:
  assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) A"
          "B \<in> A" "s1 \<in> B" "s2 \<in> B"
  shows "simple_fw rs (p\<lparr>p_dst:=s1\<rparr>) = simple_fw rs (p\<lparr>p_dst:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
have "\<forall>A \<in> (\<lambda>(base,len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow>
      simple_fw rs (p\<lparr>p_dst:=s1\<rparr>) = simple_fw rs (p\<lparr>p_dst:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw [] (p\<lparr>p_dst := s1\<rparr>) = simple_fw [] (p\<lparr>p_dst := s2\<rparr>)
 2. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {}

goal (2 subgoals):
 1. \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw [] (p\<lparr>p_dst := s1\<rparr>) = simple_fw [] (p\<lparr>p_dst := s2\<rparr>)
 2. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set []. B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. simple_fw [] (p\<lparr>p_dst := s1\<rparr>) = simple_fw [] (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
simple_fw [] (p\<lparr>p_dst := s1\<rparr>) = simple_fw [] (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
from \<open>s1 \<in> B\<close> \<open>s2 \<in> B\<close>
[PROOF STATE]
proof (chain)
picking this:
s1 \<in> B
s2 \<in> B
[PROOF STEP]
have
        "B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa)
                  \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow>
         simple_matches m (p\<lparr>p_dst := s1\<rparr>) \<longleftrightarrow> simple_matches m (p\<lparr>p_dst := s2\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
s1 \<in> B
s2 \<in> B

goal (1 subgoal):
 1. B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches m (p\<lparr>p_dst := s1\<rparr>) = simple_matches m (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(cases m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface src dsta proto sports dports. \<lbrakk>B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = src, dst = dsta, proto = proto, sports = sports, dports = dports\<rparr>\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_dst := s1\<rparr>) = simple_matches m (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(rename_tac iiface oiface src dsta proto sports dports)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface src dsta proto sports dports. \<lbrakk>B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = src, dst = dsta, proto = proto, sports = sports, dports = dports\<rparr>\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_dst := s1\<rparr>) = simple_matches m (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(case_tac dsta)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface src dsta proto sports dports a b. \<lbrakk>B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = src, dst = dsta, proto = proto, sports = sports, dports = dports\<rparr>; dsta = (a, b)\<rbrakk> \<Longrightarrow> simple_matches m (p\<lparr>p_dst := s1\<rparr>) = simple_matches m (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(simp add: simple_matches.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>iiface oiface src dsta proto sports dports a b. \<lbrakk>B \<subseteq> ipset_from_cidr a b \<or> B \<inter> ipset_from_cidr a b = {}; s1 \<in> B; s2 \<in> B; m = \<lparr>iiface = iiface, oiface = oiface, src = src, dst = (a, b), proto = proto, sports = sports, dports = dports\<rparr>; dsta = (a, b)\<rbrakk> \<Longrightarrow> (match_iface iiface (p_iiface p) \<and> match_iface oiface (p_oiface p) \<and> simple_match_ip src (p_src p) \<and> s1 \<in> ipset_from_cidr a b \<and> match_proto proto (p_proto p) \<and> simple_match_port sports (p_sport p) \<and> simple_match_port dports (p_dport p)) = (match_iface iiface (p_iiface p) \<and> match_iface oiface (p_oiface p) \<and> simple_match_ip src (p_src p) \<and> s2 \<in> ipset_from_cidr a b \<and> match_proto proto (p_proto p) \<and> simple_match_port sports (p_sport p) \<and> simple_match_port dports (p_dport p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches m (p\<lparr>p_dst := s1\<rparr>) = simple_matches m (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_dst := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
note helper=this
[PROOF STATE]
proof (state)
this:
B \<subseteq> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_dst := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); \<forall>A\<in>(\<lambda>(x, y). ipset_from_cidr x y) ` dst ` match_sel ` set (a # rs). B \<subseteq> A \<or> B \<inter> A = {}\<rbrakk> \<Longrightarrow> simple_fw (a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
\<forall>A\<in>(\<lambda>a. case a of (a, b) \<Rightarrow> ipset_from_cidr a b) ` dst ` match_sel ` set (r # rs). B \<subseteq> A \<or> B \<inter> A = {}

goal (1 subgoal):
 1. simple_fw (r # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {})\<rbrakk> \<Longrightarrow> simple_fw (r # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(case_tac r, rename_tac m a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel r) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a\<rbrakk> \<Longrightarrow> simple_fw (r # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a; a = Accept\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s2\<rparr>)
 2. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a; a = Drop\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
using helper
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst ?m2 of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {} \<Longrightarrow> simple_matches ?m2 (p\<lparr>p_dst := s1\<rparr>) = simple_matches ?m2 (p\<lparr>p_dst := s2\<rparr>)

goal (2 subgoals):
 1. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a; a = Accept\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s2\<rparr>)
 2. \<And>m a. \<lbrakk>simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>); (B \<subseteq> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst m of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}) \<and> (\<forall>A\<in>set rs. B \<subseteq> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) \<or> B \<inter> (case dst (match_sel A) of (x, xa) \<Rightarrow> ipset_from_cidr x xa) = {}); r = SimpleRule m a; a = Drop\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (SimpleRule m a # rs) (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
simple_fw (r # rs) (p\<lparr>p_dst := s1\<rparr>) = simple_fw (r # rs) (p\<lparr>p_dst := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) A
B \<in> A

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
unfolding ipPartition_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>(\<lambda>(base, len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B \<subseteq> A \<or> B \<inter> A = {} \<Longrightarrow> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
\<forall>a\<in>set (map wordinterval_to_set (extract_IPSets_generic0 dst rs)). \<forall>b\<in>A. a \<inter> b = {} \<or> b \<subseteq> a
B \<in> A

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
by (metis (full_types) Int_commute extract_equi0)
[PROOF STATE]
proof (state)
this:
simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wordinterval_list_to_set_compressed:
  "wordinterval_to_set (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)) =
          wordinterval_list_to_set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)) = wordinterval_list_to_set xs
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wordinterval_to_set (wordinterval_compress (foldr wordinterval_union [] Empty_WordInterval)) = wordinterval_list_to_set []
 2. \<And>a xs. wordinterval_to_set (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)) = wordinterval_list_to_set xs \<Longrightarrow> wordinterval_to_set (wordinterval_compress (foldr wordinterval_union (a # xs) Empty_WordInterval)) = wordinterval_list_to_set (a # xs)
[PROOF STEP]
qed(simp_all add: wordinterval_compress wordinterval_list_to_set_def)


[STATEMENT]
lemma "partIps (WordInterval (1::ipv4addr) 1) [WordInterval 0 1] = [WordInterval 1 1, WordInterval 0 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partIps (WordInterval 1 1) [WordInterval 0 1] = [WordInterval 1 1, WordInterval 0 0]
[PROOF STEP]
by eval


[STATEMENT]
lemma partIps_length: "length (partIps s ts) \<le> (length ts) * 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partIps s ts) \<le> length ts * 2
[PROOF STEP]
proof(induction ts arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. length (partIps s []) \<le> length [] * 2
 2. \<And>a ts s. (\<And>s. length (partIps s ts) \<le> length ts * 2) \<Longrightarrow> length (partIps s (a # ts)) \<le> length (a # ts) * 2
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
length (partIps ?s ts_) \<le> length ts_ * 2

goal (2 subgoals):
 1. \<And>s. length (partIps s []) \<le> length [] * 2
 2. \<And>a ts s. (\<And>s. length (partIps s ts) \<le> length ts * 2) \<Longrightarrow> length (partIps s (a # ts)) \<le> length (a # ts) * 2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (partIps ?s ts_) \<le> length ts_ * 2

goal (1 subgoal):
 1. length (partIps s (a_ # ts_)) \<le> length (a_ # ts_) * 2
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. length (partIps s ts_) \<le> length ts_ * 2) \<Longrightarrow> (wordinterval_to_set a_ \<subseteq> wordinterval_to_set s \<longrightarrow> (wordinterval_to_set s \<inter> wordinterval_to_set a_ = {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps s ts_) \<le> Suc (length ts_ * 2)) \<and> (wordinterval_to_set s \<inter> wordinterval_to_set a_ \<noteq> {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps (wordinterval_setminus s a_) ts_) \<le> Suc (length ts_ * 2))) \<and> (\<not> wordinterval_to_set a_ \<subseteq> wordinterval_to_set s \<longrightarrow> wordinterval_to_set s \<inter> wordinterval_to_set a_ = {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps s ts_) \<le> Suc (length ts_ * 2))
[PROOF STEP]
using le_Suc_eq
[PROOF STATE]
proof (prove)
using this:
(?m \<le> Suc ?n) = (?m \<le> ?n \<or> ?m = Suc ?n)

goal (1 subgoal):
 1. (\<And>s. length (partIps s ts_) \<le> length ts_ * 2) \<Longrightarrow> (wordinterval_to_set a_ \<subseteq> wordinterval_to_set s \<longrightarrow> (wordinterval_to_set s \<inter> wordinterval_to_set a_ = {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps s ts_) \<le> Suc (length ts_ * 2)) \<and> (wordinterval_to_set s \<inter> wordinterval_to_set a_ \<noteq> {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps (wordinterval_setminus s a_) ts_) \<le> Suc (length ts_ * 2))) \<and> (\<not> wordinterval_to_set a_ \<subseteq> wordinterval_to_set s \<longrightarrow> wordinterval_to_set s \<inter> wordinterval_to_set a_ = {} \<longrightarrow> wordinterval_to_set s \<noteq> {} \<longrightarrow> length (partIps s ts_) \<le> Suc (length ts_ * 2))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (partIps s (a_ # ts_)) \<le> length (a_ # ts_) * 2

goal (1 subgoal):
 1. \<And>s. length (partIps s []) \<le> length [] * 2
[PROOF STEP]
qed(simp)


[STATEMENT]
lemma partitioningIps_length: "length (partitioningIps ss ts) \<le> (2^length ss) * length ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts
[PROOF STEP]
proof(induction ss)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (partitioningIps [] ts) \<le> 2 ^ length [] * length ts
 2. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. length (partitioningIps [] ts) \<le> 2 ^ length [] * length ts
 2. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partitioningIps [] ts) \<le> 2 ^ length [] * length ts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (partitioningIps [] ts) \<le> 2 ^ length [] * length ts

goal (1 subgoal):
 1. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
case (Cons s ss)
[PROOF STATE]
proof (state)
this:
length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts

goal (1 subgoal):
 1. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
have "length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2
[PROOF STEP]
using partIps_length
[PROOF STATE]
proof (prove)
using this:
length (partIps ?s ?ts) \<le> length ?ts * 2

goal (1 subgoal):
 1. length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2

goal (1 subgoal):
 1. \<And>a ss. length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts \<Longrightarrow> length (partitioningIps (a # ss) ts) \<le> 2 ^ length (a # ss) * length ts
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts
length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2
[PROOF STEP]
show  ?case
[PROOF STATE]
proof (prove)
using this:
length (partitioningIps ss ts) \<le> 2 ^ length ss * length ts
length (partIps s (partitioningIps ss ts)) \<le> length (partitioningIps ss ts) * 2

goal (1 subgoal):
 1. length (partitioningIps (s # ss) ts) \<le> 2 ^ length (s # ss) * length ts
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
length (partitioningIps (s # ss) ts) \<le> 2 ^ length (s # ss) * length ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partIps_equi: "map wordinterval_to_set (partIps s ts) =
    partList4 (wordinterval_to_set s) (map wordinterval_to_set ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map wordinterval_to_set (partIps s ts) = partList4 (wordinterval_to_set s) (map wordinterval_to_set ts)
[PROOF STEP]
proof(induction ts arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. map wordinterval_to_set (partIps s []) = partList4 (wordinterval_to_set s) (map wordinterval_to_set [])
 2. \<And>a ts s. (\<And>s. map wordinterval_to_set (partIps s ts) = partList4 (wordinterval_to_set s) (map wordinterval_to_set ts)) \<Longrightarrow> map wordinterval_to_set (partIps s (a # ts)) = partList4 (wordinterval_to_set s) (map wordinterval_to_set (a # ts))
[PROOF STEP]
qed(simp_all)


[STATEMENT]
lemma partitioningIps_equi: "map wordinterval_to_set (partitioningIps ss ts)
       = (partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map wordinterval_to_set (partitioningIps ss ts) = partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts)
[PROOF STEP]
apply(induction ss arbitrary: ts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ts. map wordinterval_to_set (partitioningIps [] ts) = partitioning1 (map wordinterval_to_set []) (map wordinterval_to_set ts)
 2. \<And>a ss ts. (\<And>ts. map wordinterval_to_set (partitioningIps ss ts) = partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts)) \<Longrightarrow> map wordinterval_to_set (partitioningIps (a # ss) ts) = partitioning1 (map wordinterval_to_set (a # ss)) (map wordinterval_to_set ts)
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ss ts. (\<And>ts. map wordinterval_to_set (partitioningIps ss ts) = partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts)) \<Longrightarrow> map wordinterval_to_set (partitioningIps (a # ss) ts) = partitioning1 (map wordinterval_to_set (a # ss)) (map wordinterval_to_set ts)
[PROOF STEP]
apply(simp add: partIps_equi)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma partitioningIps_foldr: "partitioningIps ss ts = foldr partIps ss ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partitioningIps ss ts = foldr partIps ss ts
[PROOF STEP]
by(induction ss) (simp_all)


[STATEMENT]
lemma getParts_foldr: "getParts rs = foldr partIps (extract_IPSets rs) [wordinterval_UNIV]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getParts rs = foldr partIps (extract_IPSets rs) [wordinterval_UNIV]
[PROOF STEP]
by(simp add: getParts_def partitioningIps_foldr)


[STATEMENT]
lemma getParts_length: "length (getParts rs) \<le> 2^(2 * length rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
from partitioningIps_length[where ss="extract_IPSets rs" and ts="[wordinterval_UNIV]"]
[PROOF STATE]
proof (chain)
picking this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs) * length [wordinterval_UNIV]
[PROOF STEP]
have
    1: "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs)"
[PROOF STATE]
proof (prove)
using this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs) * length [wordinterval_UNIV]

goal (1 subgoal):
 1. length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs)

goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
from extract_IPSets_length
[PROOF STATE]
proof (chain)
picking this:
length (extract_IPSets ?rs) \<le> 2 * length ?rs
[PROOF STEP]
have "(2::nat) ^ length (extract_IPSets rs) \<le> 2 ^ (2 * length rs)"
[PROOF STATE]
proof (prove)
using this:
length (extract_IPSets ?rs) \<le> 2 * length ?rs

goal (1 subgoal):
 1. 2 ^ length (extract_IPSets rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ length (extract_IPSets rs) \<le> 2 ^ (2 * length rs)

goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs)
2 ^ length (extract_IPSets rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
have "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ (2 * length rs)"
[PROOF STATE]
proof (prove)
using this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ length (extract_IPSets rs)
2 ^ length (extract_IPSets rs) \<le> 2 ^ (2 * length rs)

goal (1 subgoal):
 1. length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ (2 * length rs)

goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) \<le> 2 ^ (2 * length rs)

goal (1 subgoal):
 1. length (getParts rs) \<le> 2 ^ (2 * length rs)
[PROOF STEP]
by(simp add: getParts_def)
[PROOF STATE]
proof (state)
this:
length (getParts rs) \<le> 2 ^ (2 * length rs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma getParts_ipPartition: "ipPartition (set (map wordinterval_to_set (extract_IPSets rs)))
                                         (set (map wordinterval_to_set (getParts rs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
have hlp_rule: "{} \<notin> set (map wordinterval_to_set ts) \<Longrightarrow> disjoint_list (map wordinterval_to_set ts) \<Longrightarrow>
     (wordinterval_list_to_set ss) \<subseteq> (wordinterval_list_to_set ts) \<Longrightarrow>
     ipPartition (set (map wordinterval_to_set ss))
                 (set (map wordinterval_to_set (partitioningIps ss ts)))" for ts ss::"'a wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{} \<notin> set (map wordinterval_to_set ts); disjoint_list (map wordinterval_to_set ts); wordinterval_list_to_set ss \<subseteq> wordinterval_list_to_set ts\<rbrakk> \<Longrightarrow> ipPartition (set (map wordinterval_to_set ss)) (set (map wordinterval_to_set (partitioningIps ss ts)))
[PROOF STEP]
by (metis ipPartitioning_helper_opt partitioningIps_equi wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>{} \<notin> set (map wordinterval_to_set ?ts); disjoint_list (map wordinterval_to_set ?ts); wordinterval_list_to_set ?ss \<subseteq> wordinterval_list_to_set ?ts\<rbrakk> \<Longrightarrow> ipPartition (set (map wordinterval_to_set ?ss)) (set (map wordinterval_to_set (partitioningIps ?ss ?ts)))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
have "disjoint_list [UNIV]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_list [UNIV]
[PROOF STEP]
by(simp add: disjoint_list_def disjoint_def)
[PROOF STATE]
proof (state)
this:
disjoint_list [UNIV]

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
have "ipPartition (set (map wordinterval_to_set ss))
                   (set (map wordinterval_to_set (partitioningIps ss [wordinterval_UNIV])))"
     for ss::"'a wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set ss)) (set (map wordinterval_to_set (partitioningIps ss [wordinterval_UNIV])))
[PROOF STEP]
apply(rule hlp_rule)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {} \<notin> set (map wordinterval_to_set [wordinterval_UNIV])
 2. disjoint_list (map wordinterval_to_set [wordinterval_UNIV])
 3. wordinterval_list_to_set ss \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]
[PROOF STEP]
apply(simp_all add: wordinterval_list_to_set_def \<open>disjoint_list [UNIV]\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ipPartition (set (map wordinterval_to_set ?ss1)) (set (map wordinterval_to_set (partitioningIps ?ss1 [wordinterval_UNIV])))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set ?ss1)) (set (map wordinterval_to_set (partitioningIps ?ss1 [wordinterval_UNIV])))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
unfolding getParts_def
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set ?ss1)) (set (map wordinterval_to_set (partitioningIps ?ss1 [wordinterval_UNIV])))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV])))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma getParts_complete: "wordinterval_list_to_set (getParts rs) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
have "{} \<notin> set (map wordinterval_to_set ts) \<Longrightarrow>
     (wordinterval_list_to_set ss) \<subseteq> (wordinterval_list_to_set ts) \<Longrightarrow>
     wordinterval_list_to_set (partitioningIps ss ts) = (wordinterval_list_to_set ts)"
     for ss ts::"'a wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{} \<notin> set (map wordinterval_to_set ts); wordinterval_list_to_set ss \<subseteq> wordinterval_list_to_set ts\<rbrakk> \<Longrightarrow> wordinterval_list_to_set (partitioningIps ss ts) = wordinterval_list_to_set ts
[PROOF STEP]
using complete_helper
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{} \<notin> set ?ts; \<Union> (set ?ss) \<subseteq> \<Union> (set ?ts)\<rbrakk> \<Longrightarrow> \<Union> (set ?ts) = \<Union> (set (partitioning1 ?ss ?ts))

goal (1 subgoal):
 1. \<lbrakk>{} \<notin> set (map wordinterval_to_set ts); wordinterval_list_to_set ss \<subseteq> wordinterval_list_to_set ts\<rbrakk> \<Longrightarrow> wordinterval_list_to_set (partitioningIps ss ts) = wordinterval_list_to_set ts
[PROOF STEP]
by (metis partitioningIps_equi wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>{} \<notin> set (map wordinterval_to_set ?ts); wordinterval_list_to_set ?ss \<subseteq> wordinterval_list_to_set ?ts\<rbrakk> \<Longrightarrow> wordinterval_list_to_set (partitioningIps ?ss ?ts) = wordinterval_list_to_set ?ts

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
hence "wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{} \<notin> set (map wordinterval_to_set ?ts); wordinterval_list_to_set ?ss \<subseteq> wordinterval_list_to_set ?ts\<rbrakk> \<Longrightarrow> wordinterval_list_to_set (partitioningIps ?ss ?ts) = wordinterval_list_to_set ?ts

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]
[PROOF STEP]
unfolding getParts_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{} \<notin> set (map wordinterval_to_set ?ts); wordinterval_list_to_set ?ss \<subseteq> wordinterval_list_to_set ?ts\<rbrakk> \<Longrightarrow> wordinterval_list_to_set (partitioningIps ?ss ?ts) = wordinterval_list_to_set ?ts

goal (1 subgoal):
 1. wordinterval_list_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]) = wordinterval_list_to_set [wordinterval_UNIV]
[PROOF STEP]
by(simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
have "\<dots> = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_list_to_set [wordinterval_UNIV] = UNIV
[PROOF STEP]
by (simp add: wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
wordinterval_list_to_set [wordinterval_UNIV] = UNIV

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wordinterval_list_to_set (getParts rs) = UNIV

goal (1 subgoal):
 1. wordinterval_list_to_set (getParts rs) = UNIV
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
wordinterval_list_to_set (getParts rs) = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem getParts_samefw:
  assumes "A \<in> set (map wordinterval_to_set (getParts rs))" "s1 \<in> A" "s2 \<in> A"
  shows "simple_fw rs (p\<lparr>p_src:=s1\<rparr>) = simple_fw rs (p\<lparr>p_src:=s2\<rparr>) \<and>
         simple_fw rs (p\<lparr>p_dst:=s1\<rparr>) = simple_fw rs (p\<lparr>p_dst:=s2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
let ?X="(set (map wordinterval_to_set (getParts rs)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
from getParts_ipPartition
[PROOF STATE]
proof (chain)
picking this:
ipPartition (set (map wordinterval_to_set (extract_IPSets ?rs))) (set (map wordinterval_to_set (getParts ?rs)))
[PROOF STEP]
have "ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) ?X"
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set (extract_IPSets ?rs))) (set (map wordinterval_to_set (getParts ?rs)))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
hence "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) ?X \<and>
         ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) ?X"
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) (set (map wordinterval_to_set (getParts rs)))

goal (1 subgoal):
 1. ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) (set (map wordinterval_to_set (getParts rs))) \<and> ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) (set (map wordinterval_to_set (getParts rs)))
[PROOF STEP]
by(simp add: extract_IPSets ipPartitionUnion image_Un)
[PROOF STATE]
proof (state)
this:
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) (set (map wordinterval_to_set (getParts rs))) \<and> ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) (set (map wordinterval_to_set (getParts rs)))

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) (set (map wordinterval_to_set (getParts rs))) \<and> ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) (set (map wordinterval_to_set (getParts rs)))

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
using assms dst_ipPart src_ipPart
[PROOF STATE]
proof (prove)
using this:
ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) (set (map wordinterval_to_set (getParts rs))) \<and> ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) (set (map wordinterval_to_set (getParts rs)))
A \<in> set (map wordinterval_to_set (getParts rs))
s1 \<in> A
s2 \<in> A
\<lbrakk>ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst ?rs))) ?A; ?B \<in> ?A; ?s1.0 \<in> ?B; ?s2.0 \<in> ?B\<rbrakk> \<Longrightarrow> simple_fw ?rs (?p\<lparr>p_dst := ?s1.0\<rparr>) = simple_fw ?rs (?p\<lparr>p_dst := ?s2.0\<rparr>)
\<lbrakk>ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src ?rs))) ?A; ?B \<in> ?A; ?s1.0 \<in> ?B; ?s2.0 \<in> ?B\<rbrakk> \<Longrightarrow> simple_fw ?rs (?p\<lparr>p_src := ?s1.0\<rparr>) = simple_fw ?rs (?p\<lparr>p_src := ?s2.0\<rparr>)

goal (1 subgoal):
 1. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partIps_nonempty: "ts \<noteq> [] \<Longrightarrow> partIps s ts \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<noteq> [] \<Longrightarrow> partIps s ts \<noteq> []
[PROOF STEP]
by(induction ts arbitrary: s) simp_all


[STATEMENT]
lemma partitioningIps_nonempty: "ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []
[PROOF STEP]
proof(induction ss arbitrary: ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps [] ts \<noteq> []
 2. \<And>a ss ts. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []\<rbrakk> \<Longrightarrow> partitioningIps (a # ss) ts \<noteq> []
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ts \<noteq> []

goal (2 subgoals):
 1. \<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps [] ts \<noteq> []
 2. \<And>a ss ts. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []\<rbrakk> \<Longrightarrow> partitioningIps (a # ss) ts \<noteq> []
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ts \<noteq> []

goal (1 subgoal):
 1. partitioningIps [] ts \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
partitioningIps [] ts \<noteq> []

goal (1 subgoal):
 1. \<And>a ss ts. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []\<rbrakk> \<Longrightarrow> partitioningIps (a # ss) ts \<noteq> []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ss ts. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []\<rbrakk> \<Longrightarrow> partitioningIps (a # ss) ts \<noteq> []
[PROOF STEP]
case (Cons s ss)
[PROOF STATE]
proof (state)
this:
?ts \<noteq> [] \<Longrightarrow> partitioningIps ss ?ts \<noteq> []
ts \<noteq> []

goal (1 subgoal):
 1. \<And>a ss ts. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []\<rbrakk> \<Longrightarrow> partitioningIps (a # ss) ts \<noteq> []
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?ts \<noteq> [] \<Longrightarrow> partitioningIps ss ?ts \<noteq> []
ts \<noteq> []

goal (1 subgoal):
 1. partitioningIps (s # ss) ts \<noteq> []
[PROOF STEP]
apply(cases ts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []; ts = []\<rbrakk> \<Longrightarrow> partitioningIps (s # ss) ts \<noteq> []
 2. \<And>a list. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []; ts = a # list\<rbrakk> \<Longrightarrow> partitioningIps (s # ss) ts \<noteq> []
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts \<noteq> []; ts = a # list\<rbrakk> \<Longrightarrow> partitioningIps (s # ss) ts \<noteq> []
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts = a # list\<rbrakk> \<Longrightarrow> partIps s (partitioningIps ss (a # list)) \<noteq> []
[PROOF STEP]
using partIps_nonempty
[PROOF STATE]
proof (prove)
using this:
?ts \<noteq> [] \<Longrightarrow> partIps ?s ?ts \<noteq> []

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ts. ts \<noteq> [] \<Longrightarrow> partitioningIps ss ts \<noteq> []; ts = a # list\<rbrakk> \<Longrightarrow> partIps s (partitioningIps ss (a # list)) \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
partitioningIps (s # ss) ts \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma getParts_nonempty: "getParts rs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getParts rs \<noteq> []
[PROOF STEP]
by(simp add: getParts_def partitioningIps_nonempty)


[STATEMENT]
lemma getParts_nonempty_elems: "\<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (getParts rs). \<not> wordinterval_empty w
[PROOF STEP]
unfolding getParts_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
have partitioning_nonempty: "\<forall>t \<in> set ts. \<not> wordinterval_empty t \<Longrightarrow>
      {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts))"
      for ts ss::"'a wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts))
[PROOF STEP]
proof(induction ss arbitrary: ts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps [] ts))
 2. \<And>a ss ts. \<lbrakk>\<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts)); \<forall>t\<in>set ts. \<not> wordinterval_empty t\<rbrakk> \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps (a # ss) ts))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ts. \<not> wordinterval_empty t

goal (2 subgoals):
 1. \<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps [] ts))
 2. \<And>a ss ts. \<lbrakk>\<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts)); \<forall>t\<in>set ts. \<not> wordinterval_empty t\<rbrakk> \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps (a # ss) ts))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ts. \<not> wordinterval_empty t

goal (1 subgoal):
 1. {} \<notin> set (map wordinterval_to_set (partitioningIps [] ts))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<notin> set (map wordinterval_to_set (partitioningIps [] ts))

goal (1 subgoal):
 1. \<And>a ss ts. \<lbrakk>\<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts)); \<forall>t\<in>set ts. \<not> wordinterval_empty t\<rbrakk> \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps (a # ss) ts))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ?ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss_ ?ts))
\<forall>t\<in>set ts. \<not> wordinterval_empty t

goal (1 subgoal):
 1. \<And>a ss ts. \<lbrakk>\<And>ts. \<forall>t\<in>set ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss ts)); \<forall>t\<in>set ts. \<not> wordinterval_empty t\<rbrakk> \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps (a # ss) ts))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ?ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ss_ ?ts))
\<forall>t\<in>set ts. \<not> wordinterval_empty t

goal (1 subgoal):
 1. {} \<notin> set (map wordinterval_to_set (partitioningIps (a_ # ss_) ts))
[PROOF STEP]
by (simp add: partIps_equi partList4_empty)
[PROOF STATE]
proof (state)
this:
{} \<notin> set (map wordinterval_to_set (partitioningIps (a_ # ss_) ts))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set ?ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ?ss ?ts))

goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
have "\<forall>t \<in> set [wordinterval_UNIV].\<not> wordinterval_empty t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set [wordinterval_UNIV]. \<not> wordinterval_empty t
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>set [wordinterval_UNIV]. \<not> wordinterval_empty t

goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
with partitioning_nonempty
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>set ?ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ?ss ?ts))
\<forall>t\<in>set [wordinterval_UNIV]. \<not> wordinterval_empty t
[PROOF STEP]
have
      "{} \<notin> set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>set ?ts. \<not> wordinterval_empty t \<Longrightarrow> {} \<notin> set (map wordinterval_to_set (partitioningIps ?ss ?ts))
\<forall>t\<in>set [wordinterval_UNIV]. \<not> wordinterval_empty t

goal (1 subgoal):
 1. {} \<notin> set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{} \<notin> set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))

goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
thus "\<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
using this:
{} \<notin> set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))

goal (1 subgoal):
 1. \<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). \<not> wordinterval_empty w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma getOneIp_elem: "\<not> wordinterval_empty W \<Longrightarrow> wordinterval_element (getOneIp W) W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> wordinterval_empty W \<Longrightarrow> wordinterval_element (getOneIp W) W
[PROOF STEP]
by (induction W) simp_all


[STATEMENT]
lemma getParts_same_fw_behaviour:
  "A \<in> set (map wordinterval_to_set (getParts rs)) \<Longrightarrow>  s1 \<in> A \<Longrightarrow> s2 \<in> A \<Longrightarrow>
   same_fw_behaviour s1 s2 rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (map wordinterval_to_set (getParts rs)); s1 \<in> A; s2 \<in> A\<rbrakk> \<Longrightarrow> same_fw_behaviour s1 s2 rs
[PROOF STEP]
unfolding same_fw_behaviour_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (map wordinterval_to_set (getParts rs)); s1 \<in> A; s2 \<in> A\<rbrakk> \<Longrightarrow> \<forall>p. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
using getParts_samefw
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (map wordinterval_to_set (getParts ?rs)); ?s1.0 \<in> ?A; ?s2.0 \<in> ?A\<rbrakk> \<Longrightarrow> simple_fw ?rs (?p\<lparr>p_src := ?s1.0\<rparr>) = simple_fw ?rs (?p\<lparr>p_src := ?s2.0\<rparr>) \<and> simple_fw ?rs (?p\<lparr>p_dst := ?s1.0\<rparr>) = simple_fw ?rs (?p\<lparr>p_dst := ?s2.0\<rparr>)

goal (1 subgoal):
 1. \<lbrakk>A \<in> set (map wordinterval_to_set (getParts rs)); s1 \<in> A; s2 \<in> A\<rbrakk> \<Longrightarrow> \<forall>p. simple_fw rs (p\<lparr>p_src := s1\<rparr>) = simple_fw rs (p\<lparr>p_src := s2\<rparr>) \<and> simple_fw rs (p\<lparr>p_dst := s1\<rparr>) = simple_fw rs (p\<lparr>p_dst := s2\<rparr>)
[PROOF STEP]
by blast