[STATEMENT]
lemma rewrite_negated_primitives_normalized_preserves_unrelated_helper:
    assumes wf_disc_sel: "wf_disc_sel (disc, sel) C"
    and disc: "\<forall>a. \<not> disc2 (C a)"
    and disc_p: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m" (*either we do not disc on protocol or the is no negated port*)
    shows "normalized_nnf_match m \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f m \<Longrightarrow>
         a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f  a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
have helper_a_normalized: "a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)) \<Longrightarrow>
        normalized_n_primitive (disc, sel) f x \<Longrightarrow>
        (\<forall>s \<in> set spts. normalized_n_primitive (disc, sel) f s) \<Longrightarrow>
        normalized_n_primitive (disc, sel) f rst \<Longrightarrow>
             normalized_n_primitive (disc, sel) f a"
        for a x spts rst f disc and sel::"'a common_primitive \<Rightarrow> 'b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f a
[PROOF STEP]
apply(subgoal_tac "\<exists> s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; \<exists>s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f a
 2. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst\<rbrakk> \<Longrightarrow> \<exists>s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst\<rbrakk> \<Longrightarrow> \<exists>s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)
 2. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; \<exists>s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; \<exists>s r. a = MatchAnd x (MatchAnd s r) \<and> s \<in> set spts \<and> r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f a
[PROOF STEP]
apply(elim exE conjE, rename_tac s r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>a \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; a = MatchAnd x (MatchAnd s r); s \<in> set spts; r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f a
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s r. \<lbrakk>MatchAnd x (MatchAnd s r) \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; a = MatchAnd x (MatchAnd s r); s \<in> set spts; r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f r
[PROOF STEP]
using normalize_match_preserves_normalized_n_primitive
[PROOF STATE]
proof (prove)
using this:
normalized_n_primitive ?disc_sel ?f ?rst \<Longrightarrow> \<forall>m\<in>set (normalize_match ?rst). normalized_n_primitive ?disc_sel ?f m

goal (1 subgoal):
 1. \<And>s r. \<lbrakk>MatchAnd x (MatchAnd s r) \<in> MatchAnd x ` (\<Union>x\<in>set spts. MatchAnd x ` set (normalize_match rst)); normalized_n_primitive (disc, sel) f x; \<forall>s\<in>set spts. normalized_n_primitive (disc, sel) f s; normalized_n_primitive (disc, sel) f rst; a = MatchAnd x (MatchAnd s r); s \<in> set spts; r \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> MatchAnd ?x ` (\<Union>x\<in>set ?spts. MatchAnd x ` set (normalize_match ?rst)); normalized_n_primitive (?disc, ?sel) ?f ?x; \<forall>s\<in>set ?spts. normalized_n_primitive (?disc, ?sel) ?f s; normalized_n_primitive (?disc, ?sel) ?f ?rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (?disc, ?sel) ?f ?a

goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
show "normalized_nnf_match m \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f m \<Longrightarrow>
         a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f  a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(case_tac "\<not> has_disc_negated disc False m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
 2. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<not> \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
using rewrite_negated_primitives_normalized_no_modification[OF wf_disc_sel]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> has_disc_negated disc False ?m; normalized_nnf_match ?m; ?a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one ?m))\<rbrakk> \<Longrightarrow> ?a = ?m

goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<not> \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(simp add: rewrite_negated_primitives_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac spts rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(subgoal_tac "normalized_n_primitive (disc2, sel2) f rst")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
 2. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
 2. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
subgoal for spts rst
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
apply(drule primitive_extractor_correct(5)[OF _ wf_disc_sel, where P="f"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) m = (?as, ?ms)
 2. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f ?ms\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(insert disc_p, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(drule(1) primitive_extractor_correct(8)[OF _ wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); (\<not> has_disc_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts)))). a \<in> MatchAnd x ` (\<Union>x\<in>set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))). MatchAnd x ` set (normalize_match rst)); has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(elim bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts)))); a \<in> MatchAnd x ` (\<Union>x\<in>set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))). MatchAnd x ` set (normalize_match rst))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a
[PROOF STEP]
apply(erule helper_a_normalized)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
 2. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> \<forall>s\<in>set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))). normalized_n_primitive (disc2, sel2) f s
 3. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
subgoal for spts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x_
[PROOF STEP]
apply(rule_tac pts="(getNeg spts)" in negated_normalized_folded_ports_normalized_n_primitive[where C=C])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (C a)
 2. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> getNeg spts = []
 3. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> disc2 (C a)

goal (3 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (C a)
 2. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> getNeg spts = []
 3. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> getNeg spts = []
 2. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))
[PROOF STEP]
using disc_p primitive_extractor_correct(8)[OF _ wf_disc_sel]
[PROOF STATE]
proof (prove)
using this:
(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m
\<lbrakk>normalized_nnf_match ?m; primitive_extractor (disc, sel) ?m = (?as, ?ms)\<rbrakk> \<Longrightarrow> (\<not> has_disc_negated disc False ?m) = (getNeg ?as = [])

goal (2 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> getNeg spts = []
 2. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> \<forall>s\<in>set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))). normalized_n_primitive (disc2, sel2) f s
 2. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x))))\<rbrakk> \<Longrightarrow> \<forall>s\<in>set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x)))). normalized_n_primitive (disc2, sel2) f s
[PROOF STEP]
apply(intro ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x)))); s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f s
[PROOF STEP]
apply(rule andfold_MatchExp_normalized_normalized_n_primitive_single[where C=C])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x)))); s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x))))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (C a)
 2. \<And>s. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x)))); s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x))))\<rbrakk> \<Longrightarrow> s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (?xs1 s))))
[PROOF STEP]
using disc disc_p
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> disc2 (C a)
(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m

goal (2 subgoals):
 1. \<And>s. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x)))); s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x))))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (C a)
 2. \<And>s. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (x, rst_); normalized_n_primitive (disc2, sel2) f rst_; \<forall>a. \<not> disc2 (Prot a); getNeg x \<noteq> []; x_ \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg x)))); s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (getPos x))))\<rbrakk> \<Longrightarrow> s \<in> set (normalize_match (andfold_MatchExp (map (Match \<circ> C) (?xs1 s))))
[PROOF STEP]
by(simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x. \<lbrakk>normalized_n_primitive (disc2, sel2) f m; has_disc_negated disc False m; primitive_extractor (disc, sel) m = (spts, rst); normalized_n_primitive (disc2, sel2) f rst; \<forall>a. \<not> disc2 (Prot a); getNeg spts \<noteq> []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) (getNeg spts))))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>normalized_nnf_match m; normalized_n_primitive (disc2, sel2) f m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rewrite_negated_src_ports:
  assumes generic: "primitive_matcher_generic \<beta>"  and n: "normalized_nnf_match m"
  shows "matches (\<beta>, \<alpha>) (rewrite_negated_src_ports m) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (rewrite_negated_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: rewrite_negated_src_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(rule rewrite_negated_primitives)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (is_Src_Ports, src_ports_sel) Src_Ports
 3. \<forall>pts. matches (\<beta>, \<alpha>) (l4_ports_negate_one Src_Ports pts) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports pts))) a p
[PROOF STEP]
by(simp add: l4_ports_negate_one[OF generic] n wf_disc_sel_common_primitive(1))+


[STATEMENT]
lemma rewrite_negated_dst_ports:
  assumes generic: "primitive_matcher_generic \<beta>"  and n: "normalized_nnf_match m"
  shows "matches (\<beta>, \<alpha>) (rewrite_negated_dst_ports m) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (rewrite_negated_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: rewrite_negated_dst_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(rule rewrite_negated_primitives)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (is_Dst_Ports, dst_ports_sel) Dst_Ports
 3. \<forall>pts. matches (\<beta>, \<alpha>) (l4_ports_negate_one Dst_Ports pts) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports pts))) a p
[PROOF STEP]
by(simp add: l4_ports_negate_one[OF generic] n wf_disc_sel_common_primitive(2))+


[STATEMENT]
lemma rewrite_negated_src_ports_not_has_disc_negated:
  assumes n: "normalized_nnf_match m"
  shows  "\<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports m)
[PROOF STEP]
apply(simp add: rewrite_negated_src_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated is_Src_Ports False (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one m)
[PROOF STEP]
apply(rule rewrite_negated_primitives_not_has_disc_negated)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (is_Src_Ports, src_ports_sel) Src_Ports
 3. has_disc_negated is_Src_Ports False m \<Longrightarrow> \<forall>pts. \<not> has_disc_negated is_Src_Ports False (l4_ports_negate_one Src_Ports pts)
[PROOF STEP]
by(simp add: n wf_disc_sel_common_primitive(1) l4_ports_negate_one_not_has_disc_negated)+


[STATEMENT]
lemma rewrite_negated_dst_ports_not_has_disc_negated:
  assumes n: "normalized_nnf_match m"
  shows  "\<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports m)
[PROOF STEP]
apply(simp add: rewrite_negated_dst_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one m)
[PROOF STEP]
apply(rule rewrite_negated_primitives_not_has_disc_negated)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (is_Dst_Ports, dst_ports_sel) Dst_Ports
 3. has_disc_negated is_Dst_Ports False m \<Longrightarrow> \<forall>pts. \<not> has_disc_negated is_Dst_Ports False (l4_ports_negate_one Dst_Ports pts)
[PROOF STEP]
by(simp add: n wf_disc_sel_common_primitive(2) l4_ports_negate_one_not_has_disc_negated)+


[STATEMENT]
lemma "\<not> has_disc_negated disc t m \<Longrightarrow> \<forall>m' \<in> set (normalize_match m). \<not> has_disc_negated disc t m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc t m \<Longrightarrow> \<forall>m'\<in>set (normalize_match m). \<not> has_disc_negated disc t m'
[PROOF STEP]
by(fact i_m_giving_this_a_funny_name_so_i_can_thank_my_future_me_when_sledgehammer_will_find_this_one_day)


[STATEMENT]
lemma singletonize_L4Ports_src: assumes generic: "primitive_matcher_generic \<beta>"
   shows "match_list (\<beta>, \<alpha>) (map (Match \<circ> Src_Ports) (singletonize_L4Ports pts)) a p \<longleftrightarrow>
    matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (map (Match \<circ> Src_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p
[PROOF STEP]
apply(cases pts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (Match \<circ> Src_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p
[PROOF STEP]
apply(simp add: match_list_matches primitive_matcher_generic.Ports_single[OF generic])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> (x1 = p_proto p \<and> (\<exists>m\<in>set x2. p_sport p \<in> ports_to_set [m])) = (x1 = p_proto p \<and> p_sport p \<in> ports_to_set x2)
[PROOF STEP]
apply(simp add: ports_to_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> (x1 = p_proto p \<and> (\<exists>m\<in>set x2. \<exists>x. (\<exists>s e. x = {s..e} \<and> (s, e) = m) \<and> p_sport p \<in> x)) = (x1 = p_proto p \<and> (\<exists>x. (\<exists>s e. x = {s..e} \<and> (s, e) \<in> set x2) \<and> p_sport p \<in> x))
[PROOF STEP]
by auto


[STATEMENT]
lemma singletonize_L4Ports_dst: assumes generic: "primitive_matcher_generic \<beta>"
   shows "match_list (\<beta>, \<alpha>) (map (Match \<circ> Dst_Ports) (singletonize_L4Ports pts)) a p \<longleftrightarrow>
    matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (map (Match \<circ> Dst_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p
[PROOF STEP]
apply(cases pts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (Match \<circ> Dst_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p
[PROOF STEP]
apply(simp add: match_list_matches primitive_matcher_generic.Ports_single[OF generic])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> (x1 = p_proto p \<and> (\<exists>m\<in>set x2. p_dport p \<in> ports_to_set [m])) = (x1 = p_proto p \<and> p_dport p \<in> ports_to_set x2)
[PROOF STEP]
apply(simp add: ports_to_set)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. pts = L4Ports x1 x2 \<Longrightarrow> (x1 = p_proto p \<and> (\<exists>m\<in>set x2. \<exists>x. (\<exists>s e. x = {s..e} \<and> (s, e) = m) \<and> p_dport p \<in> x)) = (x1 = p_proto p \<and> (\<exists>x. (\<exists>s e. x = {s..e} \<and> (s, e) \<in> set x2) \<and> p_dport p \<in> x))
[PROOF STEP]
by auto


[STATEMENT]
lemma singletonize_L4Ports_normalized_generic:
    assumes wf_disc_sel: "wf_disc_sel (disc,sel) C"
    and "m' \<in> (\<lambda>spt. Match (C spt)) ` set (singletonize_L4Ports pt)"
    shows "normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1))  m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_disc_sel (disc, sel) C
m' \<in> (\<lambda>spt. Match (C spt)) ` set (singletonize_L4Ports pt)

goal (1 subgoal):
 1. normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
apply(case_tac pt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; m' \<in> (\<lambda>spt. Match (C spt)) ` set (singletonize_L4Ports pt); pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; m' \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'
[PROOF STEP]
apply(induction m')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; Match x \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) (Match x)
 2. \<And>m' x1 x2. \<lbrakk>\<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; m' \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'; wf_disc_sel (disc, sel) C; MatchNot m' \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) (MatchNot m')
 3. \<And>m'1 m'2 x1 x2. \<lbrakk>\<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; m'1 \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'1; \<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; m'2 \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'2; wf_disc_sel (disc, sel) C; MatchAnd m'1 m'2 \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) (MatchAnd m'1 m'2)
 4. \<And>x1 x2. \<lbrakk>wf_disc_sel (disc, sel) C; MatchAny \<in> (\<lambda>x. Match (C x)) ` (\<lambda>p. L4Ports x1 [p]) ` set x2; pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) MatchAny
[PROOF STEP]
by(auto simp: wf_disc_sel.simps)


[STATEMENT]
lemma singletonize_L4Ports_normalized_src_ports:
    "m' \<in> (\<lambda>spt. Match (Src_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_src_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Src_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_src_ports m'
[PROOF STEP]
apply(simp add: normalized_src_ports_def2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Src_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_n_primitive (is_Src_Ports, src_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel_common_primitive(1)]
[PROOF STATE]
proof (prove)
using this:
?m' \<in> (\<lambda>spt. Match (Src_Ports spt)) ` set (singletonize_L4Ports ?pt) \<Longrightarrow> normalized_n_primitive (is_Src_Ports, src_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) ?m'

goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Src_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_n_primitive (is_Src_Ports, src_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
by blast


[STATEMENT]
lemma singletonize_L4Ports_normalized_dst_ports:
    "m' \<in> (\<lambda>spt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_dst_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_dst_ports m'
[PROOF STEP]
apply(simp add: normalized_dst_ports_def2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel_common_primitive(2)]
[PROOF STATE]
proof (prove)
using this:
?m' \<in> (\<lambda>spt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports ?pt) \<Longrightarrow> normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) ?m'

goal (1 subgoal):
 1. m' \<in> (\<lambda>spt. Match (Dst_Ports spt)) ` set (singletonize_L4Ports pt) \<Longrightarrow> normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalized_ports_singletonize_combine_rst:
    assumes wf_disc_sel: "wf_disc_sel (disc,sel) C"
    shows "normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) rst \<Longrightarrow>
    m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt) \<Longrightarrow>
    normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'
[PROOF STEP]
apply(rule normalized_n_primitive_MatchAnd_combine_map)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) ?rst1
 2. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> \<forall>m'\<in>(\<lambda>spt. Match (?C1 spt)) ` set ?pts1. normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) m'
 3. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> m' \<in> (\<lambda>spt. MatchAnd (Match (?C1 spt)) ?rst1) ` set ?pts1
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (singletonize_L4Ports pt). disc (C x) \<longrightarrow> (case sel (C x) of L4Ports x pts \<Rightarrow> length pts \<le> Suc 0)
[PROOF STEP]
using singletonize_L4Ports_normalized_generic[OF wf_disc_sel]
[PROOF STATE]
proof (prove)
using this:
?m' \<in> (\<lambda>spt. Match (C spt)) ` set (singletonize_L4Ports ?pt) \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) ?m'

goal (1 subgoal):
 1. \<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> Suc 0)) rst; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports pt)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (singletonize_L4Ports pt). disc (C x) \<longrightarrow> (case sel (C x) of L4Ports x pts \<Rightarrow> length pts \<le> Suc 0)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma normalize_positive_ports_step_nnf:
    assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
    and noneg: "\<not> has_disc_negated disc False m"
    shows "m' \<in> set (normalize_positive_ports_step (disc,sel) C m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_positive_ports_step (disc, sel) C m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(simp add: normalize_positive_ports_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uu_ uua_. (uua_, uu_) = primitive_extractor (disc, sel) m \<and> m' \<in> set (case getNeg uua_ of [] \<Rightarrow> case l4_ports_compress (getPos uua_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [uu_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) uu_) (singletonize_L4Ports m)) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(elim exE conjE, rename_tac rst spts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts. \<lbrakk>(spts, rst) = primitive_extractor (disc, sel) m; m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m))\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
(*switch primitive_extrartor = *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(subgoal_tac "getNeg spts = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst\<rbrakk> \<Longrightarrow> getNeg spts = []
[PROOF STEP]
(*duplication above*)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst\<rbrakk> \<Longrightarrow> getNeg spts = []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst\<rbrakk> \<Longrightarrow> getNeg spts = []
 2. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts_, rst_); normalized_nnf_match rst_\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); normalized_nnf_match rst_; (\<not> has_disc_negated disc False m) = (getNeg spts_ = [])\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
using noneg
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc False m

goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); normalized_nnf_match rst_; (\<not> has_disc_negated disc False m) = (getNeg spts_ = [])\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
by simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(simp split: match_compress.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rst spts x3. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; getNeg spts = []; l4_ports_compress (getPos spts) = MatchExpr x3; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports x3)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma normalize_positive_ports_step_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"  and wf_disc_sel: "wf_disc_sel (disc,sel) C"
    and noneg: "\<not> has_disc_negated disc False m"
    shows "\<forall>m' \<in> set (normalize_positive_ports_step (disc,sel) C m).
            normalized_n_primitive (disc,sel) (\<lambda>ps. case ps of L4Ports _ pts \<Rightarrow> length pts \<le> 1) m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_ports_step (disc, sel) C m). normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
unfolding normalize_positive_ports_step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (let (spts, rst) = primitive_extractor (disc, sel) m in case (getPos spts, getNeg spts) of (pspts, []) \<Rightarrow> case l4_ports_compress pspts of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)). normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(intro ballI, rename_tac m')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m'. m' \<in> set (let (spts, rst) = primitive_extractor (disc, sel) m in case (getPos spts, getNeg spts) of (pspts, []) \<Rightarrow> case l4_ports_compress pspts of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)) \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m'. \<exists>uu_ uua_. (uua_, uu_) = primitive_extractor (disc, sel) m \<and> m' \<in> set (case getNeg uua_ of [] \<Rightarrow> case l4_ports_compress (getPos uua_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [uu_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) uu_) (singletonize_L4Ports m)) \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(elim exE conjE, rename_tac rst spts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>(spts, rst) = primitive_extractor (disc, sel) m; m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
(*switch primitive_extrartor = *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(frule primitive_extractor_correct(2)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(subgoal_tac "getNeg spts = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> getNeg spts = []
[PROOF STEP]
(*duplication above*)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> getNeg spts = []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> getNeg spts = []
 2. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m'_ \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts_, rst_); normalized_nnf_match rst_; \<not> has_disc disc rst_\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m'_ \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); normalized_nnf_match rst_; \<not> has_disc disc rst_; (\<not> has_disc_negated disc False m) = (getNeg spts_ = [])\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
using noneg
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc False m

goal (1 subgoal):
 1. \<lbrakk>m'_ \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); normalized_nnf_match rst_; \<not> has_disc disc rst_; (\<not> has_disc_negated disc False m) = (getNeg spts_ = [])\<rbrakk> \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
by simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(subgoal_tac "normalized_n_primitive (disc,sel) (\<lambda>ps. case ps of L4Ports _ pts \<Rightarrow> length pts \<le> 1) rst")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []; normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst
 2. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []; normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m'_ \<in> set (case getNeg spts_ of [] \<Rightarrow> case l4_ports_compress (getPos spts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts_, rst_); normalized_nnf_match rst_; \<not> has_disc disc rst_; getNeg spts_ = []\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst_
[PROOF STEP]
by(drule(2) normalized_n_primitive_if_no_primitive)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts. \<lbrakk>m' \<in> set (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []; normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(simp split: match_compress.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' rst spts x3. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []; normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst; l4_ports_compress (getPos spts) = MatchExpr x3; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports x3)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
using normalized_ports_singletonize_combine_rst[OF wf_disc_sel]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) ?rst; ?m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) ?rst) ` set (singletonize_L4Ports ?pt)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) ?m'

goal (1 subgoal):
 1. \<And>m' rst spts x3. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); normalized_nnf_match rst; \<not> has_disc disc rst; getNeg spts = []; normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) rst; l4_ports_compress (getPos spts) = MatchExpr x3; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports x3)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
by blast


[STATEMENT]
lemma noNeg_mapNegPos_helper: "getNeg ls = [] \<Longrightarrow>
           map (Pos \<circ> C) (getPos ls) = NegPos_map C ls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getNeg ls = [] \<Longrightarrow> map (Pos \<circ> C) (getPos ls) = NegPos_map C ls
[PROOF STEP]
by(induction ls rule: getPos.induct) simp+


[STATEMENT]
lemma normalize_positive_src_ports:
    assumes generic: "primitive_matcher_generic \<beta>"
    and n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Src_Ports False m"
    shows
        "match_list (\<beta>, \<alpha>) (normalize_positive_src_ports m) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (normalize_positive_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: normalize_positive_src_ports_def normalize_positive_ports_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (case primitive_extractor (is_Src_Ports, src_ports_sel) m of (spts, rst) \<Rightarrow> case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(case_tac "primitive_extractor (is_Src_Ports, src_ports_sel) m", rename_tac spts rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst) \<Longrightarrow> match_list (\<beta>, \<alpha>) (case primitive_extractor (is_Src_Ports, src_ports_sel) m of (spts, rst) \<Rightarrow> case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst) \<Longrightarrow> match_list (\<beta>, \<alpha>) (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(subgoal_tac "getNeg spts = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst); getNeg spts = []\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst) \<Longrightarrow> getNeg spts = []
[PROOF STEP]
(*needs assumption for this step *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst); getNeg spts = []\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst) \<Longrightarrow> getNeg spts = []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst) \<Longrightarrow> getNeg spts = []
 2. \<And>spts rst. \<lbrakk>primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst); getNeg spts = []\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts_, rst_) \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel_common_primitive(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> has_disc_negated is_Src_Ports False m) = (getNeg spts_ = []) \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
using noneg
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated is_Src_Ports False m

goal (1 subgoal):
 1. (\<not> has_disc_negated is_Src_Ports False m) = (getNeg spts_ = []) \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
by simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst); getNeg spts = []\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case getNeg spts of [] \<Rightarrow> case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (is_Src_Ports, src_ports_sel) m = (spts, rst); getNeg spts = []\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule primitive_extractor_correct(1)[OF n wf_disc_sel_common_primitive(1), where \<gamma>="(\<beta>, \<alpha>)" and a=a and p=p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(case_tac "l4_ports_compress (getPos spts)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = CannotMatch\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchesAll\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = CannotMatch\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchesAll\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_src_CannotMatch[OF generic, where \<alpha>=\<alpha> and a=a and p=p])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; \<not> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p\<rbrakk> \<Longrightarrow> \<not> matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchesAll\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: noNeg_mapNegPos_helper; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchesAll\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchesAll\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) rst a p \<longrightarrow> matches (\<beta>, \<alpha>) m a p) \<and> (\<not> matches (\<beta>, \<alpha>) rst a p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) m a p)
 2. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_MatchesAll[OF generic, where \<alpha>=\<alpha> and a=a and p=p])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) rst a p \<longrightarrow> matches (\<beta>, \<alpha>) m a p) \<and> (\<not> matches (\<beta>, \<alpha>) rst a p \<longrightarrow> \<not> matches (\<beta>, \<alpha>) m a p)
 2. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: noNeg_mapNegPos_helper; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (case l4_ports_compress (getPos spts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; l4_ports_compress (getPos spts) = MatchExpr x3\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports x3)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_src_MatchExpr[OF generic, where \<alpha>=\<alpha> and a=a and p=p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Src_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports x3)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(insert singletonize_L4Ports_src[OF generic, where \<alpha>=\<alpha> and a=a and p=p])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Src_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p; \<And>pts. match_list (\<beta>, \<alpha>) (map (Match \<circ> Src_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (\<lambda>spt. MatchAnd (Match (Src_Ports spt)) rst) (singletonize_L4Ports x3)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: match_list_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Src_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p; \<And>pts. (\<exists>m\<in>set (singletonize_L4Ports pts). matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p) = matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p\<rbrakk> \<Longrightarrow> (\<exists>m\<in>set (singletonize_L4Ports x3). matches (\<beta>, \<alpha>) (MatchAnd (Match (Src_Ports m)) rst) a p) = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst x3. \<lbrakk>getNeg spts = []; (matches (\<beta>, \<alpha>) (alist_and (NegPos_map Src_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Src_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p; \<And>pts. (\<exists>m\<in>set (singletonize_L4Ports pts). matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p) = matches (\<beta>, \<alpha>) (Match (Src_Ports pts)) a p\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (getPos spts))) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: noNeg_mapNegPos_helper; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done