[STATEMENT]
lemma simple_conn_matches_simple_match_any: "simple_conn_matches simple_match_any c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_conn_matches simple_match_any c
[PROOF STEP]
apply (simp add: simple_conn_matches_def simple_match_any_def match_ifaceAny)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc_sport c \<le> 65535 \<and> pc_dport c \<le> 65535
[PROOF STEP]
apply (subgoal_tac "(65535::16 word) = - 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 65535 = - 1 \<Longrightarrow> pc_sport c \<le> 65535 \<and> pc_dport c \<le> 65535
 2. 65535 = - 1
[PROOF STEP]
apply (simp only:)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 65535 = - 1 \<Longrightarrow> pc_sport c \<le> - 1 \<and> pc_dport c \<le> - 1
 2. 65535 = - 1
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma has_default_policy_simple_conn_matches:
    "has_default_policy rs \<Longrightarrow> has_default_policy [r\<leftarrow>rs . simple_conn_matches (match_sel r) c]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)
[PROOF STEP]
apply(induction rs rule: has_default_policy.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. has_default_policy [] \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) [])
 2. \<And>m uu_. has_default_policy [SimpleRule m uu_] \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) [SimpleRule m uu_])
 3. \<And>uv_ v va. \<lbrakk>has_default_policy (v # va) \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (v # va)); has_default_policy (uv_ # v # va)\<rbrakk> \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (uv_ # v # va))
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m uu_. has_default_policy [SimpleRule m uu_] \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) [SimpleRule m uu_])
 2. \<And>uv_ v va. \<lbrakk>has_default_policy (v # va) \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (v # va)); has_default_policy (uv_ # v # va)\<rbrakk> \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (uv_ # v # va))
[PROOF STEP]
apply(simp add: simple_conn_matches_simple_match_any; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uv_ v va. \<lbrakk>has_default_policy (v # va) \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (v # va)); has_default_policy (uv_ # v # va)\<rbrakk> \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) (uv_ # v # va))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uv_ v va. \<lbrakk>has_default_policy (if simple_conn_matches (match_sel v) c then v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va else filter (\<lambda>r. simple_conn_matches (match_sel r) c) va); has_default_policy (v # va)\<rbrakk> \<Longrightarrow> (simple_conn_matches (match_sel v) c \<longrightarrow> simple_conn_matches (match_sel uv_) c \<longrightarrow> has_default_policy (v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va)) \<and> (\<not> simple_conn_matches (match_sel v) c \<longrightarrow> simple_conn_matches (match_sel uv_) c \<longrightarrow> has_default_policy (uv_ # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va))
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uv_ v va. \<lbrakk>has_default_policy (if simple_conn_matches (match_sel v) c then v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va else filter (\<lambda>r. simple_conn_matches (match_sel r) c) va); has_default_policy (v # va)\<rbrakk> \<Longrightarrow> simple_conn_matches (match_sel v) c \<longrightarrow> simple_conn_matches (match_sel uv_) c \<longrightarrow> has_default_policy (v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va)
 2. \<And>uv_ v va. \<lbrakk>has_default_policy (if simple_conn_matches (match_sel v) c then v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va else filter (\<lambda>r. simple_conn_matches (match_sel r) c) va); has_default_policy (v # va)\<rbrakk> \<Longrightarrow> \<not> simple_conn_matches (match_sel v) c \<longrightarrow> simple_conn_matches (match_sel uv_) c \<longrightarrow> has_default_policy (uv_ # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va)
[PROOF STEP]
apply(simp split: if_split_asm; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uv_ v va. \<lbrakk>has_default_policy (if simple_conn_matches (match_sel v) c then v # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va else filter (\<lambda>r. simple_conn_matches (match_sel r) c) va); has_default_policy (v # va)\<rbrakk> \<Longrightarrow> \<not> simple_conn_matches (match_sel v) c \<longrightarrow> simple_conn_matches (match_sel uv_) c \<longrightarrow> has_default_policy (uv_ # filter (\<lambda>r. simple_conn_matches (match_sel r) c) va)
[PROOF STEP]
apply(simp add: has_default_policy_fst split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma filter_conn_fw_lem:
    "runFw s d c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) = runFw s d c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runFw s d c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) = runFw s d c rs
[PROOF STEP]
apply(simp add: runFw_def simple_conn_matches_def match_sel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
[PROOF STEP]
apply(induction rs "\<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c,
                         p_src = s, p_dst = d, p_proto = pc_proto c,
                         p_sport = pc_sport c, p_dport = pc_dport c,
                         p_tcp_flags = {TCP_SYN},p_payload=''''\<rparr>"
          rule: simple_fw.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) []) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw [] \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
 2. \<And>m rs. (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<Longrightarrow> simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>) \<Longrightarrow> simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) (SimpleRule m Accept # rs)) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (SimpleRule m Accept # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
 3. \<And>m rs. (\<not> simple_matches m \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> \<Longrightarrow> simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw rs \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>) \<Longrightarrow> simple_fw (filter (\<lambda>r. match_iface (iiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_iiface c) \<and> match_iface (oiface (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_oiface c) \<and> match_proto (proto (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_proto c) \<and> simple_match_port (sports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_sport c) \<and> simple_match_port (dports (case r of SimpleRule x1 x2 \<Rightarrow> x1)) (pc_dport c)) (SimpleRule m Drop # rs)) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr> = simple_fw (SimpleRule m Drop # rs) \<lparr>p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c, p_tcp_flags = {TCP_SYN}, p_payload = []\<rparr>
[PROOF STEP]
apply(simp add: simple_matches.simps)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma groupWIs1_groupWIs2_equi: "groupWIs2 c rs = groupWIs1 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs1 c rs
[PROOF STEP]
by(simp add: groupWIs2_def groupWIs1_def filter_conn_fw_lem)


[STATEMENT]
lemma groupWIs_code[code]: "groupWIs c rs = groupWIs2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs c rs = groupWIs2 c rs
[PROOF STEP]
using groupWIs1_groupWIs2_equi groupWIs_groupWIs1_equi
[PROOF STATE]
proof (prove)
using this:
groupWIs2 ?c ?rs = groupWIs1 ?c ?rs
groupWIs1 ?c ?rs = groupWIs ?c ?rs

goal (1 subgoal):
 1. groupWIs c rs = groupWIs2 c rs
[PROOF STEP]
by metis


[STATEMENT]
lemma matching_dsts_pull_out_accu:
    "wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1
[PROOF STEP]
apply(induction s rs a2 arbitrary: a1 a2 rule: matching_dsts.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ _ a1 a2. wordinterval_to_set (matching_dsts uu_ [] (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts uu_ [] a2) - wordinterval_to_set a1
 2. \<And>s m rs acc_dropped a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (SimpleRule m Accept # rs) (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s (SimpleRule m Accept # rs) a2) - wordinterval_to_set a1
 3. \<And>s m rs acc_dropped a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (SimpleRule m Drop # rs) (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s (SimpleRule m Drop # rs) a2) - wordinterval_to_set a1
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s m rs a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> simple_match_ip (src m) s \<longrightarrow> wordinterval_to_set (ipcidr_tuple_to_wordinterval (dst m)) - (wordinterval_to_set a1 \<union> wordinterval_to_set a2) \<union> (wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1) = wordinterval_to_set (ipcidr_tuple_to_wordinterval (dst m)) - wordinterval_to_set a2 \<union> wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1
 2. \<And>s m rs a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (src m) s \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> simple_match_ip (src m) s \<longrightarrow> wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1 - wordinterval_to_set (ipcidr_tuple_to_wordinterval (dst m)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set (ipcidr_tuple_to_wordinterval (dst m)) - wordinterval_to_set a1
[PROOF STEP]
by blast+


[STATEMENT]
lemma matching_srcs_pull_out_accu:
    "wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1
[PROOF STEP]
apply(induction d rs a2 arbitrary: a1 a2 rule: matching_srcs.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ _ a1 a2. wordinterval_to_set (matching_srcs uu_ [] (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs uu_ [] a2) - wordinterval_to_set a1
 2. \<And>d m rs acc_dropped a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (SimpleRule m Accept # rs) (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d (SimpleRule m Accept # rs) a2) - wordinterval_to_set a1
 3. \<And>d m rs acc_dropped a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (SimpleRule m Drop # rs) (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d (SimpleRule m Drop # rs) a2) - wordinterval_to_set a1
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>d m rs a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> simple_match_ip (dst m) d \<longrightarrow> wordinterval_to_set (ipcidr_tuple_to_wordinterval (src m)) - (wordinterval_to_set a1 \<union> wordinterval_to_set a2) \<union> (wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1) = wordinterval_to_set (ipcidr_tuple_to_wordinterval (src m)) - wordinterval_to_set a2 \<union> wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1
 2. \<And>d m rs a1 a2. \<lbrakk>\<And>a1 a2. simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1; \<And>a1 a2. \<not> simple_match_ip (dst m) d \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1\<rbrakk> \<Longrightarrow> simple_match_ip (dst m) d \<longrightarrow> wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1 - wordinterval_to_set (ipcidr_tuple_to_wordinterval (src m)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set (ipcidr_tuple_to_wordinterval (src m)) - wordinterval_to_set a1
[PROOF STEP]
by blast+


[STATEMENT]
lemma matching_dsts: "\<forall>r \<in> set rs. simple_conn_matches (match_sel r) c \<Longrightarrow>
          wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>r\<in>set []. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s [] Empty_WordInterval) = {d. runFw s d c [] = Decision FinalAllow}
 2. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set []. simple_conn_matches (match_sel r) c

goal (2 subgoals):
 1. \<forall>r\<in>set []. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s [] Empty_WordInterval) = {d. runFw s d c [] = Decision FinalAllow}
 2. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set []. simple_conn_matches (match_sel r) c

goal (1 subgoal):
 1. wordinterval_to_set (matching_dsts s [] Empty_WordInterval) = {d. runFw s d c [] = Decision FinalAllow}
[PROOF STEP]
by (simp add: runFw_def)
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_dsts s [] Empty_WordInterval) = {d. runFw s d c [] = Decision FinalAllow}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
obtain m a where r: "r = SimpleRule m a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m a. r = SimpleRule m a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases r, blast)
[PROOF STATE]
proof (state)
this:
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
from Cons.prems r
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a
[PROOF STEP]
have simple_match_ip_Accept: "\<And>d. simple_match_ip (src m) s \<Longrightarrow>
        runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow \<longleftrightarrow> simple_match_ip (dst m) d \<or> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>d. simple_match_ip (src m) s \<Longrightarrow> (runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (dst m) d \<or> runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
[PROOF STATE]
proof (state)
this:
simple_match_ip (src m) s \<Longrightarrow> (runFw s ?d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (dst m) ?d \<or> runFw s ?d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
simple_match_ip (src m) s \<Longrightarrow> (runFw s ?d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (dst m) ?d \<or> runFw s ?d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
fix d a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
have "\<not> simple_match_ip (src m) s \<Longrightarrow>
         runFw s d c (SimpleRule m a # rs) = Decision FinalAllow \<longleftrightarrow> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> simple_match_ip (src m) s \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> simple_match_ip (src m) s; a = Accept\<rbrakk> \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
 2. \<lbrakk>\<not> simple_match_ip (src m) s; a = Drop\<rbrakk> \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)+
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (src m) s \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (src m) s \<Longrightarrow> (runFw s ?d2 c (SimpleRule m ?aa2 # rs) = Decision FinalAllow) = (runFw s ?d2 c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
note not_simple_match_ip=this
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (src m) s \<Longrightarrow> (runFw s ?d2 c (SimpleRule m ?aa2 # rs) = Decision FinalAllow) = (runFw s ?d2 c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
from Cons.prems r
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a
[PROOF STEP]
have simple_match_ip_Drop: "\<And>d. simple_match_ip (src m) s \<Longrightarrow>
             runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow \<longleftrightarrow> \<not> simple_match_ip (dst m) d \<and> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>d. simple_match_ip (src m) s \<Longrightarrow> (runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow) = (\<not> simple_match_ip (dst m) d \<and> runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
[PROOF STATE]
proof (state)
this:
simple_match_ip (src m) s \<Longrightarrow> (runFw s ?d c (SimpleRule m Drop # rs) = Decision FinalAllow) = (\<not> simple_match_ip (dst m) ?d \<and> runFw s ?d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s (a # rs) Empty_WordInterval) = {d. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
proof(cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Accept \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
 2. a = Drop \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
case Accept
[PROOF STATE]
proof (state)
this:
a = Accept

goal (2 subgoals):
 1. a = Accept \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
 2. a = Drop \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
with r Cons
[PROOF STATE]
proof (chain)
picking this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Accept
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Accept

goal (1 subgoal):
 1. wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp, intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> wordinterval_to_set (ipcidr_tuple_to_wordinterval (dst m)) \<union> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: simple_match_ip_Accept wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>simple_conn_matches m c; r = SimpleRule m Accept; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c; a = Accept; simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> Collect (simple_match_ip (dst m)) \<union> {d. runFw s d c rs = Decision FinalAllow} = {d. simple_match_ip (dst m) d \<or> runFw s d c rs = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: not_simple_match_ip; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}

goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
case Drop
[PROOF STATE]
proof (state)
this:
a = Drop

goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
with r Cons
[PROOF STATE]
proof (chain)
picking this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Drop
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Drop

goal (1 subgoal):
 1. wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp,intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_dsts s rs (wordinterval_union (ipcidr_tuple_to_wordinterval (dst m)) Empty_WordInterval)) = {d. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: simple_match_ip_Drop matching_dsts_pull_out_accu wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>simple_conn_matches m c; r = SimpleRule m Drop; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c; a = Drop; simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} - Collect (simple_match_ip (dst m)) = {d. \<not> simple_match_ip (dst m) d \<and> runFw s d c rs = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (src m) s\<rbrakk> \<Longrightarrow> {d. runFw s d c rs = Decision FinalAllow} = {d. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: not_simple_match_ip; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_dsts s (r # rs) Empty_WordInterval) = {d. runFw s d c (r # rs) = Decision FinalAllow}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matching_srcs: "\<forall>r \<in> set rs. simple_conn_matches (match_sel r) c \<Longrightarrow>
          wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
[PROOF STEP]
proof(induction rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>r\<in>set []. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d [] Empty_WordInterval) = {s. runFw s d c [] = Decision FinalAllow}
 2. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set []. simple_conn_matches (match_sel r) c

goal (2 subgoals):
 1. \<forall>r\<in>set []. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d [] Empty_WordInterval) = {s. runFw s d c [] = Decision FinalAllow}
 2. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set []. simple_conn_matches (match_sel r) c

goal (1 subgoal):
 1. wordinterval_to_set (matching_srcs d [] Empty_WordInterval) = {s. runFw s d c [] = Decision FinalAllow}
[PROOF STEP]
by (simp add: runFw_def)
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_srcs d [] Empty_WordInterval) = {s. runFw s d c [] = Decision FinalAllow}

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
case (Cons r rs)
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
obtain m a where r: "r = SimpleRule m a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m a. r = SimpleRule m a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases r, blast)
[PROOF STATE]
proof (state)
this:
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
from Cons.prems r
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a
[PROOF STEP]
have simple_match_ip_Accept: "\<And>s. simple_match_ip (dst m) d \<Longrightarrow>
         runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow \<longleftrightarrow>
          simple_match_ip (src m) s \<or> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>s. simple_match_ip (dst m) d \<Longrightarrow> (runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (src m) s \<or> runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
[PROOF STATE]
proof (state)
this:
simple_match_ip (dst m) d \<Longrightarrow> (runFw ?s d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (src m) ?s \<or> runFw ?s d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
simple_match_ip (dst m) d \<Longrightarrow> (runFw ?s d c (SimpleRule m Accept # rs) = Decision FinalAllow) = (simple_match_ip (src m) ?s \<or> runFw ?s d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
fix s a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
have "\<not> simple_match_ip (dst m) d \<Longrightarrow>
         runFw s d c (SimpleRule m a # rs) = Decision FinalAllow \<longleftrightarrow> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> simple_match_ip (dst m) d \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> simple_match_ip (dst m) d; a = Accept\<rbrakk> \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
 2. \<lbrakk>\<not> simple_match_ip (dst m) d; a = Drop\<rbrakk> \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)+
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (dst m) d \<Longrightarrow> (runFw s d c (SimpleRule m a # rs) = Decision FinalAllow) = (runFw s d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (dst m) d \<Longrightarrow> (runFw ?s2 d c (SimpleRule m ?aa2 # rs) = Decision FinalAllow) = (runFw ?s2 d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
note not_simple_match_ip=this
[PROOF STATE]
proof (state)
this:
\<not> simple_match_ip (dst m) d \<Longrightarrow> (runFw ?s2 d c (SimpleRule m ?aa2 # rs) = Decision FinalAllow) = (runFw ?s2 d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
from Cons.prems r
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a
[PROOF STEP]
have simple_match_ip_Drop: "\<And>s. simple_match_ip (dst m) d \<Longrightarrow>
         runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow \<longleftrightarrow>
          \<not> simple_match_ip (src m) s \<and> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
r = SimpleRule m a

goal (1 subgoal):
 1. \<And>s. simple_match_ip (dst m) d \<Longrightarrow> (runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow) = (\<not> simple_match_ip (src m) s \<and> runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
[PROOF STATE]
proof (state)
this:
simple_match_ip (dst m) d \<Longrightarrow> (runFw ?s d c (SimpleRule m Drop # rs) = Decision FinalAllow) = (\<not> simple_match_ip (src m) ?s \<and> runFw ?s d c rs = Decision FinalAllow)

goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (a # rs). simple_conn_matches (match_sel r) c\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d (a # rs) Empty_WordInterval) = {s. runFw s d c (a # rs) = Decision FinalAllow}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
proof(cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = Accept \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
 2. a = Drop \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
case Accept
[PROOF STATE]
proof (state)
this:
a = Accept

goal (2 subgoals):
 1. a = Accept \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
 2. a = Drop \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
with r Cons
[PROOF STATE]
proof (chain)
picking this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Accept
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Accept

goal (1 subgoal):
 1. wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp, intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> wordinterval_to_set (ipcidr_tuple_to_wordinterval (src m)) \<union> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: simple_match_ip_Accept wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>simple_conn_matches m c; r = SimpleRule m Accept; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c; a = Accept; simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> Collect (simple_match_ip (src m)) \<union> {s. runFw s d c rs = Decision FinalAllow} = {s. simple_match_ip (src m) s \<or> runFw s d c rs = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = SimpleRule m Accept; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Accept; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Accept; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: not_simple_match_ip; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}

goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
case Drop
[PROOF STATE]
proof (state)
this:
a = Drop

goal (1 subgoal):
 1. a = Drop \<Longrightarrow> wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
with r Cons
[PROOF STATE]
proof (chain)
picking this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Drop
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = SimpleRule m a
\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}
\<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c
a = Drop

goal (1 subgoal):
 1. wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp,intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> wordinterval_to_set (matching_srcs d rs (wordinterval_union (ipcidr_tuple_to_wordinterval (src m)) Empty_WordInterval)) = {s. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: simple_match_ip_Drop matching_srcs_pull_out_accu wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>simple_conn_matches m c; r = SimpleRule m Drop; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c; a = Drop; simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} - Collect (simple_match_ip (src m)) = {s. \<not> simple_match_ip (src m) s \<and> runFw s d c rs = Decision FinalAllow}
 2. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = SimpleRule m Drop; wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; simple_conn_matches m c \<and> (\<forall>r\<in>set rs. simple_conn_matches (match_sel r) c); a = Drop; r = SimpleRule m a; \<forall>r\<in>set rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}; \<forall>r\<in>set (r # rs). simple_conn_matches (match_sel r) c; a = Drop; \<not> simple_match_ip (dst m) d\<rbrakk> \<Longrightarrow> {s. runFw s d c rs = Decision FinalAllow} = {s. runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow}
[PROOF STEP]
apply(simp add: not_simple_match_ip; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (matching_srcs d (r # rs) Empty_WordInterval) = {s. runFw s d c (r # rs) = Decision FinalAllow}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs3_default_policy_groupWIs2:
  fixes rs :: "'i::len simple_rule list"
  assumes "has_default_policy rs"
  shows "groupWIs2 c rs = groupWIs3_default_policy c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
fix filterW s d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
from matching_dsts[where c=c]
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set ?rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts ?s ?rs Empty_WordInterval) = {d. runFw ?s d c ?rs = Decision FinalAllow}
[PROOF STEP]
have "filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow>
           wordinterval_element d (matching_dsts s filterW Empty_WordInterval) \<longleftrightarrow> runFw s d c filterW = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set ?rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_dsts ?s ?rs Empty_WordInterval) = {d. runFw ?s d c ?rs = Decision FinalAllow}

goal (1 subgoal):
 1. filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element d (matching_dsts s filterW Empty_WordInterval) = (runFw s d c filterW = Decision FinalAllow)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element d (matching_dsts s filterW Empty_WordInterval) = (runFw s d c filterW = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element ?d2 (matching_dsts ?s2 ?filterW2 Empty_WordInterval) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
note matching_dsts_filterW=this[simplified]
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> (?d2 \<in> wordinterval_to_set (matching_dsts ?s2 ?filterW2 Empty_WordInterval)) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> (?d2 \<in> wordinterval_to_set (matching_dsts ?s2 ?filterW2 Empty_WordInterval)) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
fix filterW s d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
from matching_srcs[where c=c]
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>set ?rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs ?d ?rs Empty_WordInterval) = {s. runFw s ?d c ?rs = Decision FinalAllow}
[PROOF STEP]
have "filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow>
            wordinterval_element s (matching_srcs d filterW Empty_WordInterval) \<longleftrightarrow> runFw s d c filterW = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set ?rs. simple_conn_matches (match_sel r) c \<Longrightarrow> wordinterval_to_set (matching_srcs ?d ?rs Empty_WordInterval) = {s. runFw s ?d c ?rs = Decision FinalAllow}

goal (1 subgoal):
 1. filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element s (matching_srcs d filterW Empty_WordInterval) = (runFw s d c filterW = Decision FinalAllow)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element s (matching_srcs d filterW Empty_WordInterval) = (runFw s d c filterW = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> wordinterval_element ?s2 (matching_srcs ?d2 ?filterW2 Empty_WordInterval) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
note matching_srcs_filterW=this[simplified]
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> (?s2 \<in> wordinterval_to_set (matching_srcs ?d2 ?filterW2 Empty_WordInterval)) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?filterW2 = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs \<Longrightarrow> (?s2 \<in> wordinterval_to_set (matching_srcs ?d2 ?filterW2 Empty_WordInterval)) = (runFw ?s2 ?d2 c ?filterW2 = Decision FinalAllow)

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
fix W and rs :: "'i::len simple_rule list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
assume assms': "has_default_policy rs"
[PROOF STATE]
proof (state)
this:
has_default_policy rs

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
have "groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W),
                           map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W =
             groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W),
                           map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
(*unused fresh generic variables. 'a is used for the tuple already*)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
fix f1::"'w \<Rightarrow> 'u \<Rightarrow> 'v" and f2::" 'w \<Rightarrow> 'u \<Rightarrow> 'x" and x and y and g1::"'w \<Rightarrow> 'u \<Rightarrow> 'y" and g2::"'w \<Rightarrow> 'u \<Rightarrow> 'z" and W::"'u list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W__))) W__ = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W__))) W__
[PROOF STEP]
assume 1: "\<forall>w \<in> set W. (f1 x) w = (f1 y) w \<longleftrightarrow> (f2 x) w =  (f2 y) w"
               and 2: "\<forall>w \<in> set W. (g1 x) w = (g1 y) w \<longleftrightarrow> (g2 x) w =  (g2 y) w"
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set W. (f1 x w = f1 y w) = (f2 x w = f2 y w)
\<forall>w\<in>set W. (g1 x w = g1 y w) = (g2 x w = g2 y w)

goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W__))) W__ = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W__))) W__
[PROOF STEP]
have "
                 ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W))
                 \<longleftrightarrow>
                 ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set W. (f1 x w = f1 y w) = (f2 x w = f2 y w)
[PROOF STEP]
have p1: "(map (f1 x) W = map (f1 y) W \<longleftrightarrow> map (f2 x) W = map (f2 y) W)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set W. (f1 x w = f1 y w) = (f2 x w = f2 y w)

goal (1 subgoal):
 1. (map (f1 x) W = map (f1 y) W) = (map (f2 x) W = map (f2 y) W)
[PROOF STEP]
by(induction W)(simp_all)
[PROOF STATE]
proof (state)
this:
(map (f1 x) W = map (f1 y) W) = (map (f2 x) W = map (f2 y) W)

goal (1 subgoal):
 1. ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set W. (g1 x w = g1 y w) = (g2 x w = g2 y w)
[PROOF STEP]
have p2: "(map (g1 x) W = map (g1 y) W \<longleftrightarrow> map (g2 x) W = map (g2 y) W)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set W. (g1 x w = g1 y w) = (g2 x w = g2 y w)

goal (1 subgoal):
 1. (map (g1 x) W = map (g1 y) W) = (map (g2 x) W = map (g2 y) W)
[PROOF STEP]
by(induction W)(simp_all)
[PROOF STATE]
proof (state)
this:
(map (g1 x) W = map (g1 y) W) = (map (g2 x) W = map (g2 y) W)

goal (1 subgoal):
 1. ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))
[PROOF STEP]
from p1 p2
[PROOF STATE]
proof (chain)
picking this:
(map (f1 x) W = map (f1 y) W) = (map (f2 x) W = map (f2 y) W)
(map (g1 x) W = map (g1 y) W) = (map (g2 x) W = map (g2 y) W)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(map (f1 x) W = map (f1 y) W) = (map (f2 x) W = map (f2 y) W)
(map (g1 x) W = map (g1 y) W) = (map (g2 x) W = map (g2 y) W)

goal (1 subgoal):
 1. ((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((map (f1 x) W, map (g1 x) W) = (map (f1 y) W, map (g1 y) W)) = ((map (f2 x) W, map (g2 x) W) = (map (f2 y) W, map (g2 y) W))

goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W__))) W__ = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W__), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W__))) W__
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>w\<in>set ?Wa2. (?f1.2 ?x2 w = ?f1.2 ?y2 w) = (?f2.2 ?x2 w = ?f2.2 ?y2 w); \<forall>w\<in>set ?Wa2. (?g1.2 ?x2 w = ?g1.2 ?y2 w) = (?g2.2 ?x2 w = ?g2.2 ?y2 w)\<rbrakk> \<Longrightarrow> ((map (?f1.2 ?x2) ?Wa2, map (?g1.2 ?x2) ?Wa2) = (map (?f1.2 ?y2) ?Wa2, map (?g1.2 ?y2) ?Wa2)) = ((map (?f2.2 ?x2) ?Wa2, map (?g2.2 ?x2) ?Wa2) = (map (?f2.2 ?y2) ?Wa2, map (?g2.2 ?y2) ?Wa2))

goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
note map_over_tuples_equal_helper=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>w\<in>set ?Wa2. (?f1.2 ?x2 w = ?f1.2 ?y2 w) = (?f2.2 ?x2 w = ?f2.2 ?y2 w); \<forall>w\<in>set ?Wa2. (?g1.2 ?x2 w = ?g1.2 ?y2 w) = (?g2.2 ?x2 w = ?g2.2 ?y2 w)\<rbrakk> \<Longrightarrow> ((map (?f1.2 ?x2) ?Wa2, map (?g1.2 ?x2) ?Wa2) = (map (?f1.2 ?y2) ?Wa2, map (?g1.2 ?y2) ?Wa2)) = ((map (?f2.2 ?x2) ?Wa2, map (?g2.2 ?x2) ?Wa2) = (map (?f2.2 ?y2) ?Wa2, map (?g2.2 ?y2) ?Wa2))

goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W
[PROOF STEP]
apply(rule groupF_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set W. \<forall>y\<in>set W. ((map (\<lambda>d. runFw (getOneIp x) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp x) c rs = Decision FinalAllow) (map getOneIp W)) = (map (\<lambda>d. runFw (getOneIp y) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp y) c rs = Decision FinalAllow) (map getOneIp W))) = ((map (\<lambda>d. runFw (getOneIp x) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp x) c rs) (map getOneIp W)) = (map (\<lambda>d. runFw (getOneIp y) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp y) c rs) (map getOneIp W)))
[PROOF STEP]
apply(intro ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set W; y \<in> set W\<rbrakk> \<Longrightarrow> ((map (\<lambda>d. runFw (getOneIp x) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp x) c rs = Decision FinalAllow) (map getOneIp W)) = (map (\<lambda>d. runFw (getOneIp y) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp y) c rs = Decision FinalAllow) (map getOneIp W))) = ((map (\<lambda>d. runFw (getOneIp x) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp x) c rs) (map getOneIp W)) = (map (\<lambda>d. runFw (getOneIp y) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp y) c rs) (map getOneIp W)))
[PROOF STEP]
apply(rule map_over_tuples_equal_helper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set W; y \<in> set W\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (map getOneIp W). ((runFw (getOneIp x) w c rs = Decision FinalAllow) = (runFw (getOneIp y) w c rs = Decision FinalAllow)) = (runFw (getOneIp x) w c rs = runFw (getOneIp y) w c rs)
 2. \<And>x y. \<lbrakk>x \<in> set W; y \<in> set W\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (map getOneIp W). ((runFw w (getOneIp x) c rs = Decision FinalAllow) = (runFw w (getOneIp y) c rs = Decision FinalAllow)) = (runFw w (getOneIp x) c rs = runFw w (getOneIp y) c rs)
[PROOF STEP]
using has_default_policy_runFw[OF assms']
[PROOF STATE]
proof (prove)
using this:
runFw ?s ?d ?c rs = Decision FinalAllow \<or> runFw ?s ?d ?c rs = Decision FinalDeny

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> set W; y \<in> set W\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (map getOneIp W). ((runFw (getOneIp x) w c rs = Decision FinalAllow) = (runFw (getOneIp y) w c rs = Decision FinalAllow)) = (runFw (getOneIp x) w c rs = runFw (getOneIp y) w c rs)
 2. \<And>x y. \<lbrakk>x \<in> set W; y \<in> set W\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (map getOneIp W). ((runFw w (getOneIp x) c rs = Decision FinalAllow) = (runFw w (getOneIp y) c rs = Decision FinalAllow)) = (runFw w (getOneIp x) c rs = runFw w (getOneIp y) c rs)
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs = Decision FinalAllow) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs = Decision FinalAllow) (map getOneIp W))) W = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp W), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp W))) W

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
has_default_policy ?rsa2 \<Longrightarrow> groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c ?rsa2 = Decision FinalAllow) (map getOneIp ?W2), map (\<lambda>s. runFw s (getOneIp wi) c ?rsa2 = Decision FinalAllow) (map getOneIp ?W2))) ?W2 = groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c ?rsa2) (map getOneIp ?W2), map (\<lambda>s. runFw s (getOneIp wi) c ?rsa2) (map getOneIp ?W2))) ?W2

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
note has_default_policy_groupF=this[simplified]
[PROOF STATE]
proof (state)
this:
has_default_policy ?rsa2 \<Longrightarrow> groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c ?rsa2 = Decision FinalAllow) \<circ> getOneIp) ?W2, map ((\<lambda>s. runFw s (getOneIp wi) c ?rsa2 = Decision FinalAllow) \<circ> getOneIp) ?W2)) ?W2 = groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c ?rsa2) \<circ> getOneIp) ?W2, map ((\<lambda>s. runFw s (getOneIp wi) c ?rsa2) \<circ> getOneIp) ?W2)) ?W2

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
has_default_policy rs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
has_default_policy rs

goal (1 subgoal):
 1. groupWIs2 c rs = groupWIs3_default_policy c rs
[PROOF STEP]
apply(simp add: groupWIs3_default_policy_def groupWIs_code[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> groupWIs c rs = (let P = getParts rs; filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs in map (map fst) (groupF snd (map (\<lambda>x. (x, map ((\<lambda>d. d \<in> wordinterval_to_set (matching_dsts (getOneIp x) filterW Empty_WordInterval)) \<circ> getOneIp) P, map ((\<lambda>s. s \<in> wordinterval_to_set (matching_srcs (getOneIp x) filterW Empty_WordInterval)) \<circ> getOneIp) P)) P)))
[PROOF STEP]
apply(subst groupF_tuple[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> groupWIs c rs = (let P = getParts rs; filterW = filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs in groupF (\<lambda>x. (map ((\<lambda>d. d \<in> wordinterval_to_set (matching_dsts (getOneIp x) filterW Empty_WordInterval)) \<circ> getOneIp) P, map ((\<lambda>s. s \<in> wordinterval_to_set (matching_srcs (getOneIp x) filterW Empty_WordInterval)) \<circ> getOneIp) P)) P)
[PROOF STEP]
apply(simp add: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> groupWIs c rs = groupF (\<lambda>x. (map ((\<lambda>d. d \<in> wordinterval_to_set (matching_dsts (getOneIp x) (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) Empty_WordInterval)) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. s \<in> wordinterval_to_set (matching_srcs (getOneIp x) (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) Empty_WordInterval)) \<circ> getOneIp) (getParts rs))) (getParts rs)
[PROOF STEP]
apply(simp add: matching_srcs_filterW matching_dsts_filterW)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> groupWIs c rs = groupF (\<lambda>x. (map ((\<lambda>d. runFw (getOneIp x) d c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) = Decision FinalAllow) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp x) c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs) = Decision FinalAllow) \<circ> getOneIp) (getParts rs))) (getParts rs)
[PROOF STEP]
apply(subst has_default_policy_groupF)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. has_default_policy rs \<Longrightarrow> has_default_policy (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)
 2. has_default_policy rs \<Longrightarrow> groupWIs c rs = groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)) \<circ> getOneIp) (getParts rs))) (getParts rs)
[PROOF STEP]
apply(simp add: has_default_policy_simple_conn_matches; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_default_policy rs \<Longrightarrow> groupWIs c rs = groupF (\<lambda>wi. (map ((\<lambda>d. runFw (getOneIp wi) d c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)) \<circ> getOneIp) (getParts rs), map ((\<lambda>s. runFw s (getOneIp wi) c (filter (\<lambda>r. simple_conn_matches (match_sel r) c) rs)) \<circ> getOneIp) (getParts rs))) (getParts rs)
[PROOF STEP]
apply(simp add: groupWIs_def Let_def filter_conn_fw_lem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
groupWIs2 c rs = groupWIs3_default_policy c rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma groupWIs3: "groupWIs3 = groupWIs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. groupWIs3 = groupWIs
[PROOF STEP]
by(simp add: fun_eq_iff groupWIs3_def groupWIs_code groupWIs3_default_policy_groupWIs2)


[STATEMENT]
theorem build_ip_partition_same_fw: "V \<in> set (build_ip_partition c rs) \<Longrightarrow>
                               \<forall>ip1::'i::len word \<in> wordinterval_to_set V.
                               \<forall>ip2::'i::len word \<in> wordinterval_to_set V.
                               same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> set (build_ip_partition c rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set V. \<forall>ip2\<in>wordinterval_to_set V. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
apply(simp add: build_ip_partition_def groupWIs3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set V. \<forall>ip2\<in>wordinterval_to_set V. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
using wordinterval_list_to_set_compressed groupParts_same_fw_wi2 wordinterval_sort
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set (wordinterval_compress (foldr wordinterval_union ?xs Empty_WordInterval)) = wordinterval_list_to_set ?xs
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set ?V. \<forall>ip2\<in>wordinterval_list_to_set ?V. same_fw_behaviour_one ip1 ip2 ?c ?rs
wordinterval_to_set (wordinterval_sort ?w) = wordinterval_to_set ?w

goal (1 subgoal):
 1. V \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs) \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set V. \<forall>ip2\<in>wordinterval_to_set V. same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
by blast


[STATEMENT]
theorem build_ip_partition_same_fw_min: "A \<in> set (build_ip_partition c rs) \<Longrightarrow> B \<in> set (build_ip_partition c rs) \<Longrightarrow>
                                A \<noteq> B \<Longrightarrow>
                                \<forall>ip1::'i::len word \<in> wordinterval_to_set A.
                                \<forall>ip2::'i::len word \<in> wordinterval_to_set B.
                                \<not> same_fw_behaviour_one ip1 ip2 c rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> set (build_ip_partition c rs); B \<in> set (build_ip_partition c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set A. \<forall>ip2\<in>wordinterval_to_set B. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
apply(simp add: build_ip_partition_def groupWIs3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs); B \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set A. \<forall>ip2\<in>wordinterval_to_set B. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
using  groupWIs_same_fw_not2 wordinterval_list_to_set_compressed wordinterval_sort
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> set (groupWIs ?c ?rs); ?B \<in> set (groupWIs ?c ?rs); ?A \<noteq> ?B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_list_to_set ?A. \<forall>ip2\<in>wordinterval_list_to_set ?B. \<not> same_fw_behaviour_one ip1 ip2 ?c ?rs
wordinterval_to_set (wordinterval_compress (foldr wordinterval_union ?xs Empty_WordInterval)) = wordinterval_list_to_set ?xs
wordinterval_to_set (wordinterval_sort ?w) = wordinterval_to_set ?w

goal (1 subgoal):
 1. \<lbrakk>A \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs); B \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs); A \<noteq> B\<rbrakk> \<Longrightarrow> \<forall>ip1\<in>wordinterval_to_set A. \<forall>ip2\<in>wordinterval_to_set B. \<not> same_fw_behaviour_one ip1 ip2 c rs
[PROOF STEP]
by blast


[STATEMENT]
theorem build_ip_partition_complete: "(\<Union>x\<in>set (build_ip_partition c rs). wordinterval_to_set x) = (UNIV :: 'i::len word set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (build_ip_partition c rs)) = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (build_ip_partition c rs)) = UNIV
[PROOF STEP]
have "wordinterval_to_set (foldr wordinterval_union x Empty_WordInterval) = \<Union>(set (map wordinterval_to_set x))"
    for x::"'i wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wordinterval_to_set (foldr wordinterval_union x Empty_WordInterval) = \<Union> (set (map wordinterval_to_set x))
[PROOF STEP]
by(induction x) simp_all
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (foldr wordinterval_union ?x Empty_WordInterval) = \<Union> (set (map wordinterval_to_set ?x))

goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (build_ip_partition c rs)) = UNIV
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set (foldr wordinterval_union ?x Empty_WordInterval) = \<Union> (set (map wordinterval_to_set ?x))

goal (1 subgoal):
 1. \<Union> (wordinterval_to_set ` set (build_ip_partition c rs)) = UNIV
[PROOF STEP]
apply(simp add: build_ip_partition_def groupWIs3 wordinterval_compress wordinterval_sort)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. wordinterval_to_set (foldr wordinterval_union x Empty_WordInterval) = \<Union> (wordinterval_to_set ` set x)) \<Longrightarrow> (\<Union>x\<in>set (groupWIs c rs). \<Union> (wordinterval_to_set ` set x)) = UNIV
[PROOF STEP]
using groupWIs_complete[simplified wordinterval_list_to_set_def]
[PROOF STATE]
proof (prove)
using this:
(\<Union>x\<in>set (groupWIs ?c ?rs). \<Union> (set (map wordinterval_to_set x))) = UNIV

goal (1 subgoal):
 1. (\<And>x. wordinterval_to_set (foldr wordinterval_union x Empty_WordInterval) = \<Union> (wordinterval_to_set ` set x)) \<Longrightarrow> (\<Union>x\<in>set (groupWIs c rs). \<Union> (wordinterval_to_set ` set x)) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (wordinterval_to_set ` set (build_ip_partition c rs)) = UNIV

goal:
No subgoals!
[PROOF STEP]
qed