[STATEMENT]
lemma build_ip_partition_no_empty_elems: "wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
assume "wi \<in> set (build_ip_partition c rs)"
[PROOF STATE]
proof (state)
this:
wi \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
hence assm: "wi \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs)"
[PROOF STATE]
proof (prove)
using this:
wi \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. wi \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs)
[PROOF STEP]
by(simp add: build_ip_partition_def groupWIs3)
[PROOF STATE]
proof (state)
this:
wi \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs)

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
from assm
[PROOF STATE]
proof (chain)
picking this:
wi \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs)
[PROOF STEP]
obtain wi_orig where 1: "wi_orig \<in>  set (groupWIs c rs)" and
       2: "wi = wordinterval_sort (wordinterval_compress (foldr wordinterval_union wi_orig Empty_WordInterval))"
[PROOF STATE]
proof (prove)
using this:
wi \<in> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) ` set (groupWIs c rs)

goal (1 subgoal):
 1. (\<And>wi_orig. \<lbrakk>wi_orig \<in> set (groupWIs c rs); wi = wordinterval_sort (wordinterval_compress (foldr wordinterval_union wi_orig Empty_WordInterval))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wi_orig \<in> set (groupWIs c rs)
wi = wordinterval_sort (wordinterval_compress (foldr wordinterval_union wi_orig Empty_WordInterval))

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
from 1 groupWIs_not_empty_elem
[PROOF STATE]
proof (chain)
picking this:
wi_orig \<in> set (groupWIs c rs)
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> ?V \<noteq> []
[PROOF STEP]
have i1: "wi_orig \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
wi_orig \<in> set (groupWIs c rs)
?V \<in> set (groupWIs ?c ?rs) \<Longrightarrow> ?V \<noteq> []

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

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
from 1 groupWIs_not_empty_elems
[PROOF STATE]
proof (chain)
picking this:
wi_orig \<in> set (groupWIs c rs)
\<lbrakk>?V \<in> set (groupWIs ?c ?rs); ?w \<in> set ?V\<rbrakk> \<Longrightarrow> \<not> wordinterval_empty ?w
[PROOF STEP]
have i2: "\<And>w. w \<in> set wi_orig \<Longrightarrow> \<not> wordinterval_empty w"
[PROOF STATE]
proof (prove)
using this:
wi_orig \<in> set (groupWIs c rs)
\<lbrakk>?V \<in> set (groupWIs ?c ?rs); ?w \<in> set ?V\<rbrakk> \<Longrightarrow> \<not> wordinterval_empty ?w

goal (1 subgoal):
 1. \<And>w. w \<in> set wi_orig \<Longrightarrow> \<not> wordinterval_empty w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?w \<in> set wi_orig \<Longrightarrow> \<not> wordinterval_empty ?w

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
from i1 i2
[PROOF STATE]
proof (chain)
picking this:
wi_orig \<noteq> []
?w \<in> set wi_orig \<Longrightarrow> \<not> wordinterval_empty ?w
[PROOF STEP]
have "wordinterval_to_set (foldr wordinterval_union wi_orig Empty_WordInterval) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
wi_orig \<noteq> []
?w \<in> set wi_orig \<Longrightarrow> \<not> wordinterval_empty ?w

goal (1 subgoal):
 1. wordinterval_to_set (foldr wordinterval_union wi_orig Empty_WordInterval) \<noteq> {}
[PROOF STEP]
by(induction wi_orig) simp_all
[PROOF STATE]
proof (state)
this:
wordinterval_to_set (foldr wordinterval_union wi_orig Empty_WordInterval) \<noteq> {}

goal (1 subgoal):
 1. wi \<in> set (build_ip_partition c rs) \<Longrightarrow> \<not> wordinterval_empty wi
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
wi = wordinterval_sort (wordinterval_compress (foldr wordinterval_union wi_orig Empty_WordInterval))
wordinterval_to_set (foldr wordinterval_union wi_orig Empty_WordInterval) \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wi = wordinterval_sort (wordinterval_compress (foldr wordinterval_union wi_orig Empty_WordInterval))
wordinterval_to_set (foldr wordinterval_union wi_orig Empty_WordInterval) \<noteq> {}

goal (1 subgoal):
 1. \<not> wordinterval_empty wi
[PROOF STEP]
by(simp add: wordinterval_compress wordinterval_sort)
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_empty wi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma build_ip_partition_disjoint:
      "V1 \<in> set (build_ip_partition c rs) \<Longrightarrow> V2 \<in> set (build_ip_partition c rs) \<Longrightarrow>
       V1 \<noteq> V2 \<Longrightarrow>
        wordinterval_to_set V1 \<inter> wordinterval_to_set V2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>V1 \<in> set (build_ip_partition c rs); V2 \<in> set (build_ip_partition c rs); V1 \<noteq> V2\<rbrakk> \<Longrightarrow> wordinterval_to_set V1 \<inter> wordinterval_to_set V2 = {}
[PROOF STEP]
by (metis build_ip_partition_same_fw build_ip_partition_same_fw_min disjoint_iff)


[STATEMENT]
lemma map_wordinterval_to_set_distinct:
  assumes distinct: "distinct xs"
  and disjoint: "(\<forall>x1 \<in> set xs. \<forall>x2 \<in> set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {})"
  and notempty: "\<forall>x \<in> set xs. \<not> wordinterval_empty x"
  shows "distinct (map wordinterval_to_set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map wordinterval_to_set xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (map wordinterval_to_set xs)
[PROOF STEP]
have "\<not> wordinterval_empty x1 \<Longrightarrow>
        wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {} \<Longrightarrow>
        wordinterval_to_set x1 \<noteq> wordinterval_to_set x2" for x1::"('b::len) wordinterval" and x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> wordinterval_empty x1; wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}\<rbrakk> \<Longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> wordinterval_empty ?x1.1; wordinterval_to_set ?x1.1 \<inter> wordinterval_to_set ?x2.1 = {}\<rbrakk> \<Longrightarrow> wordinterval_to_set ?x1.1 \<noteq> wordinterval_to_set ?x2.1

goal (1 subgoal):
 1. distinct (map wordinterval_to_set xs)
[PROOF STEP]
with disjoint notempty
[PROOF STATE]
proof (chain)
picking this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
\<forall>x\<in>set xs. \<not> wordinterval_empty x
\<lbrakk>\<not> wordinterval_empty ?x1.1; wordinterval_to_set ?x1.1 \<inter> wordinterval_to_set ?x2.1 = {}\<rbrakk> \<Longrightarrow> wordinterval_to_set ?x1.1 \<noteq> wordinterval_to_set ?x2.1
[PROOF STEP]
have "(\<forall>x1 \<in> set xs. \<forall>x2 \<in> set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
\<forall>x\<in>set xs. \<not> wordinterval_empty x
\<lbrakk>\<not> wordinterval_empty ?x1.1; wordinterval_to_set ?x1.1 \<inter> wordinterval_to_set ?x2.1 = {}\<rbrakk> \<Longrightarrow> wordinterval_to_set ?x1.1 \<noteq> wordinterval_to_set ?x2.1

goal (1 subgoal):
 1. \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2

goal (1 subgoal):
 1. distinct (map wordinterval_to_set xs)
[PROOF STEP]
with distinct
[PROOF STATE]
proof (chain)
picking this:
distinct xs
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2
[PROOF STEP]
show "distinct (map wordinterval_to_set xs)"
[PROOF STATE]
proof (prove)
using this:
distinct xs
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2

goal (1 subgoal):
 1. distinct (map wordinterval_to_set xs)
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set xs); distinct (a # xs); \<forall>x1\<in>set (a # xs). \<forall>x2\<in>set (a # xs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set (a # xs))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct xs_; \<forall>x1\<in>set xs_. \<forall>x2\<in>set xs_. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set xs_)
distinct (a_ # xs_)
\<forall>x1\<in>set (a_ # xs_). \<forall>x2\<in>set (a_ # xs_). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2

goal (2 subgoals):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set xs); distinct (a # xs); \<forall>x1\<in>set (a # xs). \<forall>x2\<in>set (a # xs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct xs_; \<forall>x1\<in>set xs_. \<forall>x2\<in>set xs_. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set xs_)
distinct (a_ # xs_)
\<forall>x1\<in>set (a_ # xs_). \<forall>x2\<in>set (a_ # xs_). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (a_ # xs_))
[PROOF STEP]
by simp fast
[PROOF STATE]
proof (state)
this:
distinct (map wordinterval_to_set (a_ # xs_))

goal (1 subgoal):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<noteq> wordinterval_to_set x2\<rbrakk> \<Longrightarrow> distinct (map wordinterval_to_set [])
[PROOF STEP]
qed(simp)
[PROOF STATE]
proof (state)
this:
distinct (map wordinterval_to_set xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_getOneIp_distinct: assumes
  distinct: "distinct xs"
  and disjoint: "(\<forall>x1 \<in> set xs. \<forall>x2 \<in> set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {})"
  and notempty: "\<forall>x \<in> set xs. \<not> wordinterval_empty x"
  shows "distinct (map getOneIp xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map getOneIp xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (map getOneIp xs)
[PROOF STEP]
have "\<not> wordinterval_empty x \<Longrightarrow> \<not> wordinterval_empty xa \<Longrightarrow>
          wordinterval_to_set x \<inter> wordinterval_to_set xa = {} \<Longrightarrow> getOneIp x \<noteq> getOneIp xa"
     for x xa::"'b::len wordinterval"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> wordinterval_empty x; \<not> wordinterval_empty xa; wordinterval_to_set x \<inter> wordinterval_to_set xa = {}\<rbrakk> \<Longrightarrow> getOneIp x \<noteq> getOneIp xa
[PROOF STEP]
by(fastforce dest: getOneIp_elem)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> wordinterval_empty ?x1; \<not> wordinterval_empty ?xa1; wordinterval_to_set ?x1 \<inter> wordinterval_to_set ?xa1 = {}\<rbrakk> \<Longrightarrow> getOneIp ?x1 \<noteq> getOneIp ?xa1

goal (1 subgoal):
 1. distinct (map getOneIp xs)
[PROOF STEP]
with disjoint notempty
[PROOF STATE]
proof (chain)
picking this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
\<forall>x\<in>set xs. \<not> wordinterval_empty x
\<lbrakk>\<not> wordinterval_empty ?x1; \<not> wordinterval_empty ?xa1; wordinterval_to_set ?x1 \<inter> wordinterval_to_set ?xa1 = {}\<rbrakk> \<Longrightarrow> getOneIp ?x1 \<noteq> getOneIp ?xa1
[PROOF STEP]
have "(\<forall>x1 \<in> set xs. \<forall>x2 \<in> set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
\<forall>x\<in>set xs. \<not> wordinterval_empty x
\<lbrakk>\<not> wordinterval_empty ?x1; \<not> wordinterval_empty ?xa1; wordinterval_to_set ?x1 \<inter> wordinterval_to_set ?xa1 = {}\<rbrakk> \<Longrightarrow> getOneIp ?x1 \<noteq> getOneIp ?xa1

goal (1 subgoal):
 1. \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2

goal (1 subgoal):
 1. distinct (map getOneIp xs)
[PROOF STEP]
with distinct
[PROOF STATE]
proof (chain)
picking this:
distinct xs
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct xs
\<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2

goal (1 subgoal):
 1. distinct (map getOneIp xs)
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp xs); distinct (a # xs); \<forall>x1\<in>set (a # xs). \<forall>x2\<in>set (a # xs). x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp (a # xs))
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct xs_; \<forall>x1\<in>set xs_. \<forall>x2\<in>set xs_. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp xs_)
distinct (a_ # xs_)
\<forall>x1\<in>set (a_ # xs_). \<forall>x2\<in>set (a_ # xs_). x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2

goal (2 subgoals):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp [])
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct xs; \<forall>x1\<in>set xs. \<forall>x2\<in>set xs. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp xs); distinct (a # xs); \<forall>x1\<in>set (a # xs). \<forall>x2\<in>set (a # xs). x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct xs_; \<forall>x1\<in>set xs_. \<forall>x2\<in>set xs_. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp xs_)
distinct (a_ # xs_)
\<forall>x1\<in>set (a_ # xs_). \<forall>x2\<in>set (a_ # xs_). x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2

goal (1 subgoal):
 1. distinct (map getOneIp (a_ # xs_))
[PROOF STEP]
by simp fast
[PROOF STATE]
proof (state)
this:
distinct (map getOneIp (a_ # xs_))

goal (1 subgoal):
 1. \<lbrakk>distinct []; \<forall>x1\<in>set []. \<forall>x2\<in>set []. x1 \<noteq> x2 \<longrightarrow> getOneIp x1 \<noteq> getOneIp x2\<rbrakk> \<Longrightarrow> distinct (map getOneIp [])
[PROOF STEP]
qed(simp)
[PROOF STATE]
proof (state)
this:
distinct (map getOneIp xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma getParts_disjoint_list: "disjoint_list (map wordinterval_to_set (getParts rs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (getParts rs))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (getParts rs))
[PROOF STEP]
have disjoint_list_partitioningIps:
    "{} \<notin> set (map wordinterval_to_set ts) \<Longrightarrow> disjoint_list (map wordinterval_to_set ts) \<Longrightarrow>
     (wordinterval_list_to_set ss) \<subseteq> (wordinterval_list_to_set ts) \<Longrightarrow>
     disjoint_list (map wordinterval_to_set (partitioningIps ss ts))"
     for ts::"'a::len wordinterval list" and ss
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{} \<notin> set (map wordinterval_to_set ts); disjoint_list (map wordinterval_to_set ts); wordinterval_list_to_set ss \<subseteq> wordinterval_list_to_set ts\<rbrakk> \<Longrightarrow> disjoint_list (map wordinterval_to_set (partitioningIps ss ts))
[PROOF STEP]
by (simp add: partitioning1_disjoint_list partitioningIps_equi wordinterval_list_to_set_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>{} \<notin> set (map wordinterval_to_set ?ts); disjoint_list (map wordinterval_to_set ?ts); wordinterval_list_to_set ?ss \<subseteq> wordinterval_list_to_set ?ts\<rbrakk> \<Longrightarrow> disjoint_list (map wordinterval_to_set (partitioningIps ?ss ?ts))

goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (getParts rs))
[PROOF STEP]
have "{} \<notin> set (map wordinterval_to_set [wordinterval_UNIV])"
  and "disjoint_list (map wordinterval_to_set [wordinterval_UNIV])"
  and "wordinterval_list_to_set (extract_IPSets rs) \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> set (map wordinterval_to_set [wordinterval_UNIV]) &&& disjoint_list (map wordinterval_to_set [wordinterval_UNIV]) &&& wordinterval_list_to_set (extract_IPSets rs) \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]
[PROOF STEP]
by(simp add: wordinterval_list_to_set_def disjoint_list_def disjoint_def)+
[PROOF STATE]
proof (state)
this:
{} \<notin> set (map wordinterval_to_set [wordinterval_UNIV])
disjoint_list (map wordinterval_to_set [wordinterval_UNIV])
wordinterval_list_to_set (extract_IPSets rs) \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]

goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (getParts rs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<notin> set (map wordinterval_to_set [wordinterval_UNIV])
disjoint_list (map wordinterval_to_set [wordinterval_UNIV])
wordinterval_list_to_set (extract_IPSets rs) \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]

goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (getParts rs))
[PROOF STEP]
unfolding getParts_def
[PROOF STATE]
proof (prove)
using this:
{} \<notin> set (map wordinterval_to_set [wordinterval_UNIV])
disjoint_list (map wordinterval_to_set [wordinterval_UNIV])
wordinterval_list_to_set (extract_IPSets rs) \<subseteq> wordinterval_list_to_set [wordinterval_UNIV]

goal (1 subgoal):
 1. disjoint_list (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))
[PROOF STEP]
by(rule disjoint_list_partitioningIps)
[PROOF STATE]
proof (state)
this:
disjoint_list (map wordinterval_to_set (getParts rs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma build_ip_partition_distinct: "distinct (map wordinterval_to_set (build_ip_partition c rs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
have
  "(wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ws
       = \<Union>(set (map wordinterval_to_set ws))" for ws::"'a::len wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ws = \<Union> (set (map wordinterval_to_set ws))
[PROOF STEP]
proof(induction ws)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) [] = \<Union> (set (map wordinterval_to_set []))
 2. \<And>a ws. (wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ws = \<Union> (set (map wordinterval_to_set ws)) \<Longrightarrow> (wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) (a # ws) = \<Union> (set (map wordinterval_to_set (a # ws)))
[PROOF STEP]
qed(simp_all add: wordinterval_compress wordinterval_sort)
[PROOF STATE]
proof (state)
this:
(wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ?ws = \<Union> (set (map wordinterval_to_set ?ws))

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
hence hlp1: "map wordinterval_to_set (build_ip_partition c rs) =
                   map (\<lambda>x. \<Union>(set (map wordinterval_to_set x))) (groupWIs c rs)"
[PROOF STATE]
proof (prove)
using this:
(wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ?ws = \<Union> (set (map wordinterval_to_set ?ws))

goal (1 subgoal):
 1. map wordinterval_to_set (build_ip_partition c rs) = map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupWIs c rs)
[PROOF STEP]
unfolding build_ip_partition_def groupWIs3
[PROOF STATE]
proof (prove)
using this:
(wordinterval_to_set \<circ> (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)))) ?ws = \<Union> (set (map wordinterval_to_set ?ws))

goal (1 subgoal):
 1. map wordinterval_to_set (map (\<lambda>xs. wordinterval_sort (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval))) (groupWIs c rs)) = map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupWIs c rs)
[PROOF STEP]
by auto

  \<comment> \<open>generic rule\<close>
[PROOF STATE]
proof (state)
this:
map wordinterval_to_set (build_ip_partition c rs) = map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupWIs c rs)

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
have "\<forall>x \<in> set xs. \<not> wordinterval_empty x \<Longrightarrow>
         disjoint_list (map wordinterval_to_set xs) \<Longrightarrow>
         distinct (map (\<lambda>x. \<Union>(set (map wordinterval_to_set x))) (groupF f xs))"
         for f::"'x::len wordinterval \<Rightarrow> 'y" and xs::"'x::len wordinterval list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set xs. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set xs)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f xs))
[PROOF STEP]
proof(induction f xs rule: groupF.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set []. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set [])\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f []))
 2. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set []. \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set [])

goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<forall>x\<in>set []. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set [])\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f []))
 2. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set []. \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set [])

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f_ []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f_ []))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
case (2 f x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set (x # xs))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
have hlp_internal:
          "\<Union> (set (map (\<lambda>x. \<Union>(set (map wordinterval_to_set x))) (groupF f xs))) =
           \<Union> (set (map wordinterval_to_set xs))" for f::"'x wordinterval \<Rightarrow> 'y" and xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f xs))) = \<Union> (set (map wordinterval_to_set xs))
[PROOF STEP]
by(induction f xs rule: groupF.induct) (auto)
[PROOF STATE]
proof (state)
this:
\<Union> (set (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF ?f ?xs))) = \<Union> (set (map wordinterval_to_set ?xs))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
from 2(2,3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set (x # xs))
[PROOF STEP]
have "wordinterval_to_set x \<inter> \<Union>(wordinterval_to_set ` set xs) = {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set (x # xs))

goal (1 subgoal):
 1. wordinterval_to_set x \<inter> \<Union> (wordinterval_to_set ` set xs) = {}
[PROOF STEP]
by(auto simp add: disjoint_def disjoint_list_def)
[PROOF STATE]
proof (state)
this:
wordinterval_to_set x \<inter> \<Union> (wordinterval_to_set ` set xs) = {}

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
hence "\<not> (wordinterval_to_set x) \<subseteq> \<Union>(wordinterval_to_set ` set xs)"
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set x \<inter> \<Union> (wordinterval_to_set ` set xs) = {}

goal (1 subgoal):
 1. \<not> wordinterval_to_set x \<subseteq> \<Union> (wordinterval_to_set ` set xs)
[PROOF STEP]
using 2(2)
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set x \<inter> \<Union> (wordinterval_to_set ` set xs) = {}
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x

goal (1 subgoal):
 1. \<not> wordinterval_to_set x \<subseteq> \<Union> (wordinterval_to_set ` set xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_to_set x \<subseteq> \<Union> (wordinterval_to_set ` set xs)

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
hence "\<not> wordinterval_to_set x \<subseteq> \<Union>(set (map wordinterval_to_set [y\<leftarrow>xs . f x \<noteq> f y]))"
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_to_set x \<subseteq> \<Union> (wordinterval_to_set ` set xs)

goal (1 subgoal):
 1. \<not> wordinterval_to_set x \<subseteq> \<Union> (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_to_set x \<subseteq> \<Union> (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
hence "\<not> wordinterval_to_set x \<union> (\<Union>x\<in>{xa \<in> set xs. f x = f xa}.
         wordinterval_to_set x) \<subseteq> \<Union> (set (map (\<lambda>x. \<Union>(set (map wordinterval_to_set x))) (groupF f [y\<leftarrow>xs . f x \<noteq> f y])))"
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_to_set x \<subseteq> \<Union> (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))

goal (1 subgoal):
 1. \<not> wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<subseteq> \<Union> (set (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))))
[PROOF STEP]
unfolding hlp_internal
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_to_set x \<subseteq> \<Union> (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))

goal (1 subgoal):
 1. \<not> wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<subseteq> \<Union> (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<subseteq> \<Union> (set (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
hence g1: "wordinterval_to_set x \<union> (\<Union>x\<in>{xa \<in> set xs. f x = f xa}. wordinterval_to_set x)
        \<notin> (\<lambda>x. \<Union>x\<in>set x. wordinterval_to_set x) ` set (groupF f [y\<leftarrow>xs . f x \<noteq> f y])"
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<subseteq> \<Union> (set (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))))

goal (1 subgoal):
 1. wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<notin> (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) ` set (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<notin> (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) ` set (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
from 2(3)
[PROOF STATE]
proof (chain)
picking this:
disjoint_list (map wordinterval_to_set (x # xs))
[PROOF STEP]
have "distinct (map wordinterval_to_set [y\<leftarrow>xs . f x \<noteq> f y])"
[PROOF STATE]
proof (prove)
using this:
disjoint_list (map wordinterval_to_set (x # xs))

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))
[PROOF STEP]
by (simp add: disjoint_list_def  distinct_map_filter)
[PROOF STATE]
proof (state)
this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set (x # xs))
[PROOF STEP]
have "disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x
disjoint_list (map wordinterval_to_set (x # xs))

goal (1 subgoal):
 1. disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})
[PROOF STEP]
by(simp add: disjoint_def disjoint_list_def)
[PROOF STATE]
proof (state)
this:
disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))
disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})
[PROOF STEP]
have g2: "distinct (map (\<lambda>x. \<Union>x\<in>set x. wordinterval_to_set x) (groupF f [y\<leftarrow>xs . f x \<noteq> f y]))"
[PROOF STATE]
proof (prove)
using this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))
disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
using 2(1,2)
[PROOF STATE]
proof (prove)
using this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))
disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})
\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
unfolding disjoint_list_def
[PROOF STATE]
proof (prove)
using this:
distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))
disjoint (wordinterval_to_set ` {xa \<in> set xs. f x \<noteq> f xa})
\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; distinct (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)) \<and> disjoint (set (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs)))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
\<forall>x\<in>set (x # xs). \<not> wordinterval_empty x

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))

goal (1 subgoal):
 1. \<And>f x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set (filter (\<lambda>y. f x \<noteq> f y) xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (filter (\<lambda>y. f x \<noteq> f y) xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))); \<forall>x\<in>set (x # xs). \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set (x # xs))\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
from g1 g2
[PROOF STATE]
proof (chain)
picking this:
wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<notin> (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) ` set (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))
distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wordinterval_to_set x \<union> \<Union> (wordinterval_to_set ` {xa \<in> set xs. f x = f xa}) \<notin> (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) ` set (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs))
distinct (map (\<lambda>x. \<Union> (wordinterval_to_set ` set x)) (groupF f (filter (\<lambda>y. f x \<noteq> f y) xs)))

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF f (x # xs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set ?xs1. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set ?xs1)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF ?f1 ?xs1))

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
with getParts_disjoint_list getParts_nonempty_elems
[PROOF STATE]
proof (chain)
picking this:
disjoint_list (map wordinterval_to_set (getParts ?rs))
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w
\<lbrakk>\<forall>x\<in>set ?xs1. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set ?xs1)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF ?f1 ?xs1))
[PROOF STEP]
have
      "distinct
     (map (\<lambda>x. \<Union>(set (map wordinterval_to_set x)))
       (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)),
                      map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs))))
         (getParts rs)))"
[PROOF STATE]
proof (prove)
using this:
disjoint_list (map wordinterval_to_set (getParts ?rs))
\<forall>w\<in>set (getParts ?rs). \<not> wordinterval_empty w
\<lbrakk>\<forall>x\<in>set ?xs1. \<not> wordinterval_empty x; disjoint_list (map wordinterval_to_set ?xs1)\<rbrakk> \<Longrightarrow> distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF ?f1 ?xs1))

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))

goal (1 subgoal):
 1. distinct (map wordinterval_to_set (build_ip_partition c rs))
[PROOF STEP]
unfolding hlp1 groupWIs_def Let_def
[PROOF STATE]
proof (prove)
using this:
distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))

goal (1 subgoal):
 1. distinct (map (\<lambda>x. \<Union> (set (map wordinterval_to_set x))) (groupF (\<lambda>wi. (map (\<lambda>d. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)), map (\<lambda>s. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs)))) (getParts rs)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
distinct (map wordinterval_to_set (build_ip_partition c rs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma build_ip_partition_distinct': "distinct (build_ip_partition c rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (build_ip_partition c rs)
[PROOF STEP]
using build_ip_partition_distinct distinct_mapI
[PROOF STATE]
proof (prove)
using this:
distinct (map wordinterval_to_set (build_ip_partition ?c ?rs))
distinct (map ?f ?l) \<Longrightarrow> distinct ?l

goal (1 subgoal):
 1. distinct (build_ip_partition c rs)
[PROOF STEP]
by blast


[STATEMENT]
lemma simple_fw_no_interfaces:
  assumes no_ifaces: "simple_firewall_without_interfaces rs"
  shows "simple_fw rs p = simple_fw rs (p\<lparr> p_iiface:= x, p_oiface:= y\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
[PROOF STEP]
from no_ifaces
[PROOF STATE]
proof (chain)
picking this:
simple_firewall_without_interfaces rs
[PROOF STEP]
have "\<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny"
[PROOF STATE]
proof (prove)
using this:
simple_firewall_without_interfaces rs

goal (1 subgoal):
 1. \<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny
[PROOF STEP]
by(simp add: simple_firewall_without_interfaces_def)
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny

goal (1 subgoal):
 1. simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny

goal (1 subgoal):
 1. simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
[PROOF STEP]
apply(induction rs p rule:simple_fw.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_. \<forall>r\<in>set []. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny \<Longrightarrow> simple_fw [] uu_ = simple_fw [] (uu_\<lparr>p_iiface := x, p_oiface := y\<rparr>)
 2. \<And>m rs p. \<lbrakk>\<lbrakk>\<not> simple_matches m p; \<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny\<rbrakk> \<Longrightarrow> simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>); \<forall>r\<in>set (SimpleRule m Accept # rs). iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m Accept # rs) p = simple_fw (SimpleRule m Accept # rs) (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
 3. \<And>m rs p. \<lbrakk>\<lbrakk>\<not> simple_matches m p; \<forall>r\<in>set rs. iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny\<rbrakk> \<Longrightarrow> simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>); \<forall>r\<in>set (SimpleRule m Drop # rs). iiface (match_sel r) = ifaceAny \<and> oiface (match_sel r) = ifaceAny\<rbrakk> \<Longrightarrow> simple_fw (SimpleRule m Drop # rs) p = simple_fw (SimpleRule m Drop # rs) (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)
[PROOF STEP]
by(simp_all add: simple_matches.simps match_ifaceAny)
[PROOF STATE]
proof (state)
this:
simple_fw rs p = simple_fw rs (p\<lparr>p_iiface := x, p_oiface := y\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma runFw_no_interfaces:
  assumes no_ifaces: "simple_firewall_without_interfaces rs"
  shows "runFw s d c rs = runFw s d (c\<lparr> pc_iiface:= x, pc_oiface:= y\<rparr>) rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runFw s d c rs = runFw s d (c\<lparr>pc_iiface := x, pc_oiface := y\<rparr>) rs
[PROOF STEP]
apply(simp add: runFw_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> = simple_fw rs \<lparr>p_iiface = x, p_oiface = y, 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(subst simple_fw_no_interfaces[OF no_ifaces])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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>\<lparr>p_iiface := ?x, p_oiface := ?y\<rparr>) = simple_fw rs \<lparr>p_iiface = x, p_oiface = y, 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]
by(simp)


[STATEMENT]
lemma access_matrix_nodes_defined:
      "(V,E) = access_matrix c rs \<Longrightarrow> (s, d) \<in> set E \<Longrightarrow> s \<in> dom (map_of V)" and
      "(V,E) = access_matrix c rs \<Longrightarrow> (s, d) \<in> set E \<Longrightarrow> d \<in> dom (map_of V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(V, E) = access_matrix c rs; (s, d) \<in> set E\<rbrakk> \<Longrightarrow> s \<in> dom (map_of V)) &&& (\<lbrakk>(V, E) = access_matrix c rs; (s, d) \<in> set E\<rbrakk> \<Longrightarrow> d \<in> dom (map_of V))
[PROOF STEP]
by(auto simp add: access_matrix_def Let_def all_pairs_def)


[STATEMENT]
lemma "(V,E) = access_matrix c rs \<Longrightarrow> (s, d) \<in> set E \<Longrightarrow> runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(V, E) = access_matrix c rs; (s, d) \<in> set E\<rbrakk> \<Longrightarrow> runFw s d c rs = Decision FinalAllow
[PROOF STEP]
by(auto simp add: access_matrix_def Let_def)


[STATEMENT]
lemma map_of_zip_map: "map_of (zip (map f rs) rs) k = Some v \<Longrightarrow> k = f v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (zip (map f rs) rs) k = Some v \<Longrightarrow> k = f v
[PROOF STEP]
apply(induction rs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map_of (zip (map f []) []) k = Some v \<Longrightarrow> k = f v
 2. \<And>a rs. \<lbrakk>map_of (zip (map f rs) rs) k = Some v \<Longrightarrow> k = f v; map_of (zip (map f (a # rs)) (a # rs)) k = Some v\<rbrakk> \<Longrightarrow> k = f v
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rs. \<lbrakk>map_of (zip (map f rs) rs) k = Some v \<Longrightarrow> k = f v; map_of (zip (map f (a # rs)) (a # rs)) k = Some v\<rbrakk> \<Longrightarrow> k = f v
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma access_matrix_sound: assumes matrix: "(V,E) = access_matrix c rs" and
              repr: "(s_repr, d_repr) \<in> set E" and
              s_range: "(map_of V) s_repr = Some s_range" and s: "s \<in> wordinterval_to_set s_range" and
              d_range: "(map_of V) d_repr = Some d_range" and d: "d \<in> wordinterval_to_set d_range"
      shows "runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
let ?part="(build_ip_partition c rs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
have V: "V = (zip (map getOneIp ?part) ?part)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
using matrix
[PROOF STATE]
proof (prove)
using this:
(V, E) = access_matrix c rs

goal (1 subgoal):
 1. V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
by(simp add: access_matrix_def Let_def)
[PROOF STATE]
proof (state)
this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
(*have "E = [(s, d)\<leftarrow>all_pairs (map getOneIp ?part). runFw s d c rs = Decision FinalAllow]"
      using matrix by(simp add: access_matrix_def Let_def)
    with repr have "(s_repr, d_repr) \<in> set (all_pairs (map getOneIp ?part))" by simp
    hence "s_repr \<in> set (map getOneIp ?part)" and
          "d_repr \<in> set (map getOneIp ?part)"
      by(simp add: all_pairs_set)+*)
    (*from s_range have "(s_repr, s_range) \<in> set V" by (simp add: map_of_SomeD)*)
[PROOF STATE]
proof (state)
this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from matrix repr
[PROOF STATE]
proof (chain)
picking this:
(V, E) = access_matrix c rs
(s_repr, d_repr) \<in> set E
[PROOF STEP]
have repr_Allow: "runFw s_repr d_repr c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
(V, E) = access_matrix c rs
(s_repr, d_repr) \<in> set E

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
by(auto simp add: access_matrix_def Let_def)
[PROOF STATE]
proof (state)
this:
runFw s_repr d_repr c rs = Decision FinalAllow

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
have s_range_in_part: "s_range \<in> set ?part"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
using V s_range
[PROOF STATE]
proof (prove)
using this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V s_repr = Some s_range

goal (1 subgoal):
 1. s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
by (fastforce elim: in_set_zipE dest: map_of_SomeD)
[PROOF STATE]
proof (state)
this:
s_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with build_ip_partition_no_empty_elems
[PROOF STATE]
proof (chain)
picking this:
?wi \<in> set (build_ip_partition ?c ?rs) \<Longrightarrow> \<not> wordinterval_empty ?wi
s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have "\<not> wordinterval_empty s_range"
[PROOF STATE]
proof (prove)
using this:
?wi \<in> set (build_ip_partition ?c ?rs) \<Longrightarrow> \<not> wordinterval_empty ?wi
s_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. \<not> wordinterval_empty s_range
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_empty s_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
have d_range_in_part: "d_range \<in> set ?part"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
using V d_range
[PROOF STATE]
proof (prove)
using this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V d_repr = Some d_range

goal (1 subgoal):
 1. d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
by (fastforce elim: in_set_zipE dest: map_of_SomeD)
[PROOF STATE]
proof (state)
this:
d_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with build_ip_partition_no_empty_elems
[PROOF STATE]
proof (chain)
picking this:
?wi \<in> set (build_ip_partition ?c ?rs) \<Longrightarrow> \<not> wordinterval_empty ?wi
d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have "\<not> wordinterval_empty d_range"
[PROOF STATE]
proof (prove)
using this:
?wi \<in> set (build_ip_partition ?c ?rs) \<Longrightarrow> \<not> wordinterval_empty ?wi
d_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. \<not> wordinterval_empty d_range
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> wordinterval_empty d_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from map_of_zip_map V s_range
[PROOF STATE]
proof (chain)
picking this:
map_of (zip (map ?f ?rs) ?rs) ?k = Some ?v \<Longrightarrow> ?k = ?f ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V s_repr = Some s_range
[PROOF STEP]
have "s_repr = getOneIp s_range"
[PROOF STATE]
proof (prove)
using this:
map_of (zip (map ?f ?rs) ?rs) ?k = Some ?v \<Longrightarrow> ?k = ?f ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V s_repr = Some s_range

goal (1 subgoal):
 1. s_repr = getOneIp s_range
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
s_repr = getOneIp s_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with \<open>\<not> wordinterval_empty s_range\<close> getOneIp_elem wordinterval_element_set_eq
[PROOF STATE]
proof (chain)
picking this:
\<not> wordinterval_empty s_range
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
wordinterval_element ?el ?rg = (?el \<in> wordinterval_to_set ?rg)
s_repr = getOneIp s_range
[PROOF STEP]
have "s_repr \<in> wordinterval_to_set s_range"
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_empty s_range
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
wordinterval_element ?el ?rg = (?el \<in> wordinterval_to_set ?rg)
s_repr = getOneIp s_range

goal (1 subgoal):
 1. s_repr \<in> wordinterval_to_set s_range
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s_repr \<in> wordinterval_to_set s_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from map_of_zip_map V d_range
[PROOF STATE]
proof (chain)
picking this:
map_of (zip (map ?f ?rs) ?rs) ?k = Some ?v \<Longrightarrow> ?k = ?f ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V d_repr = Some d_range
[PROOF STEP]
have "d_repr = getOneIp d_range"
[PROOF STATE]
proof (prove)
using this:
map_of (zip (map ?f ?rs) ?rs) ?k = Some ?v \<Longrightarrow> ?k = ?f ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V d_repr = Some d_range

goal (1 subgoal):
 1. d_repr = getOneIp d_range
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
d_repr = getOneIp d_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with \<open>\<not> wordinterval_empty d_range\<close> getOneIp_elem wordinterval_element_set_eq
[PROOF STATE]
proof (chain)
picking this:
\<not> wordinterval_empty d_range
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
wordinterval_element ?el ?rg = (?el \<in> wordinterval_to_set ?rg)
d_repr = getOneIp d_range
[PROOF STEP]
have "d_repr \<in> wordinterval_to_set d_range"
[PROOF STATE]
proof (prove)
using this:
\<not> wordinterval_empty d_range
\<not> wordinterval_empty ?W \<Longrightarrow> wordinterval_element (getOneIp ?W) ?W
wordinterval_element ?el ?rg = (?el \<in> wordinterval_to_set ?rg)
d_repr = getOneIp d_range

goal (1 subgoal):
 1. d_repr \<in> wordinterval_to_set d_range
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d_repr \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from s_range_in_part
[PROOF STATE]
proof (chain)
picking this:
s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have s_range_in_part': "s_range \<in> set (build_ip_partition c rs)"
[PROOF STATE]
proof (prove)
using this:
s_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from d_range_in_part
[PROOF STATE]
proof (chain)
picking this:
d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have d_range_in_part': "d_range \<in> set (build_ip_partition c rs)"
[PROOF STATE]
proof (prove)
using this:
d_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from build_ip_partition_same_fw[OF s_range_in_part', unfolded same_fw_behaviour_one_def] s
                                                        \<open>s_repr \<in> wordinterval_to_set s_range\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip1\<in>wordinterval_to_set s_range. \<forall>ip2\<in>wordinterval_to_set s_range. \<forall>d s. runFw ip1 d c rs = runFw ip2 d c rs \<and> runFw s ip1 c rs = runFw s ip2 c rs
s \<in> wordinterval_to_set s_range
s_repr \<in> wordinterval_to_set s_range
[PROOF STEP]
have
      "\<forall>d. runFw s_repr d c rs = runFw s d c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip1\<in>wordinterval_to_set s_range. \<forall>ip2\<in>wordinterval_to_set s_range. \<forall>d s. runFw ip1 d c rs = runFw ip2 d c rs \<and> runFw s ip1 c rs = runFw s ip2 c rs
s \<in> wordinterval_to_set s_range
s_repr \<in> wordinterval_to_set s_range

goal (1 subgoal):
 1. \<forall>d. runFw s_repr d c rs = runFw s d c rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>d. runFw s_repr d c rs = runFw s d c rs

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with repr_Allow
[PROOF STATE]
proof (chain)
picking this:
runFw s_repr d_repr c rs = Decision FinalAllow
\<forall>d. runFw s_repr d c rs = runFw s d c rs
[PROOF STEP]
have 1: "runFw s d_repr c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
runFw s_repr d_repr c rs = Decision FinalAllow
\<forall>d. runFw s_repr d c rs = runFw s d c rs

goal (1 subgoal):
 1. runFw s d_repr c rs = Decision FinalAllow
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
runFw s d_repr c rs = Decision FinalAllow

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
from build_ip_partition_same_fw[OF d_range_in_part', unfolded same_fw_behaviour_one_def] d
                                                        \<open>d_repr \<in> wordinterval_to_set d_range\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip1\<in>wordinterval_to_set d_range. \<forall>ip2\<in>wordinterval_to_set d_range. \<forall>d s. runFw ip1 d c rs = runFw ip2 d c rs \<and> runFw s ip1 c rs = runFw s ip2 c rs
d \<in> wordinterval_to_set d_range
d_repr \<in> wordinterval_to_set d_range
[PROOF STEP]
have
      "\<forall>s. runFw s d_repr c rs = runFw s d c rs"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip1\<in>wordinterval_to_set d_range. \<forall>ip2\<in>wordinterval_to_set d_range. \<forall>d s. runFw ip1 d c rs = runFw ip2 d c rs \<and> runFw s ip1 c rs = runFw s ip2 c rs
d \<in> wordinterval_to_set d_range
d_repr \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. \<forall>s. runFw s d_repr c rs = runFw s d c rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>s. runFw s d_repr c rs = runFw s d c rs

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
runFw s d_repr c rs = Decision FinalAllow
\<forall>s. runFw s d_repr c rs = runFw s d c rs
[PROOF STEP]
have 2: "runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
runFw s d_repr c rs = Decision FinalAllow
\<forall>s. runFw s d_repr c rs = runFw s d c rs

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
runFw s d c rs = Decision FinalAllow

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
runFw s d c rs = Decision FinalAllow

goal (1 subgoal):
 1. runFw s d c rs = Decision FinalAllow
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
runFw s d c rs = Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_map_getOneIp_obtain: "v \<in> set xs \<Longrightarrow> distinct (map getOneIp xs) \<Longrightarrow>
  \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v \<in> set []; distinct (map getOneIp [])\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp []) []) s_repr = Some v
 2. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
v \<in> set []
distinct (map getOneIp [])

goal (2 subgoals):
 1. \<lbrakk>v \<in> set []; distinct (map getOneIp [])\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp []) []) s_repr = Some v
 2. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
v \<in> set []
distinct (map getOneIp [])

goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp []) []) s_repr = Some v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp []) []) s_repr = Some v

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v
v \<in> set (x # xs)
distinct (map getOneIp (x # xs))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
consider "v = x" | "v \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = x \<Longrightarrow> thesis; v \<in> set xs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
v \<in> set (x # xs)

goal (1 subgoal):
 1. \<lbrakk>v = x \<Longrightarrow> thesis; v \<in> set xs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>v = x \<Longrightarrow> ?thesis; v \<in> set xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v; v \<in> set (a # xs); distinct (map getOneIp (a # xs))\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (a # xs)) (a # xs)) s_repr = Some v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v = x \<Longrightarrow> ?thesis; v \<in> set xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
 2. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
v = x

goal (2 subgoals):
 1. v = x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
 2. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = x

goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v

goal (1 subgoal):
 1. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
v \<in> set xs

goal (1 subgoal):
 1. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
with Cons.IH Cons.prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v
distinct (map getOneIp (x # xs))
v \<in> set xs
[PROOF STEP]
obtain s_repr where
      s_repr: "map_of (zip (map getOneIp xs) xs) s_repr = Some v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>v \<in> set xs; distinct (map getOneIp xs)\<rbrakk> \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v
distinct (map getOneIp (x # xs))
v \<in> set xs

goal (1 subgoal):
 1. (\<And>s_repr. map_of (zip (map getOneIp xs) xs) s_repr = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
map_of (zip (map getOneIp xs) xs) s_repr = Some v

goal (1 subgoal):
 1. v \<in> set xs \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
proof(cases "s_repr \<noteq> getOneIp x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
 2. \<not> s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s_repr \<noteq> getOneIp x

goal (2 subgoals):
 1. s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
 2. \<not> s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
with Cons.prems s_repr
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (x # xs)
distinct (map getOneIp (x # xs))
map_of (zip (map getOneIp xs) xs) s_repr = Some v
s_repr \<noteq> getOneIp x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> set (x # xs)
distinct (map getOneIp (x # xs))
map_of (zip (map getOneIp xs) xs) s_repr = Some v
s_repr \<noteq> getOneIp x

goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
by(rule_tac x=s_repr in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v

goal (1 subgoal):
 1. \<not> s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> s_repr \<noteq> getOneIp x

goal (1 subgoal):
 1. \<not> s_repr \<noteq> getOneIp x \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
with Cons.prems s_repr
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (x # xs)
distinct (map getOneIp (x # xs))
map_of (zip (map getOneIp xs) xs) s_repr = Some v
\<not> s_repr \<noteq> getOneIp x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> set (x # xs)
distinct (map getOneIp (x # xs))
map_of (zip (map getOneIp xs) xs) s_repr = Some v
\<not> s_repr \<noteq> getOneIp x

goal (1 subgoal):
 1. \<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v
[PROOF STEP]
by(fastforce elim: in_set_zipE)
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s_repr. map_of (zip (map getOneIp (x # xs)) (x # xs)) s_repr = Some v

goal:
No subgoals!
[PROOF STEP]
qed