[STATEMENT]
lemma normalize_positive_dst_ports:
    assumes generic: "primitive_matcher_generic \<beta>"
    and n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Dst_Ports False m"
    shows "match_list (\<beta>, \<alpha>) (normalize_positive_dst_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_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: normalize_positive_dst_ports_def normalize_positive_ports_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (case primitive_extractor (is_Dst_Ports, dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(case_tac "primitive_extractor (is_Dst_Ports, dst_ports_sel) m", rename_tac spts rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (is_Dst_Ports, dst_ports_sel) m = (spts, rst) \<Longrightarrow> match_list (\<beta>, \<alpha>) (case primitive_extractor (is_Dst_Ports, dst_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 (Dst_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_Dst_Ports, dst_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 (Dst_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_Dst_Ports, dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. primitive_extractor (is_Dst_Ports, dst_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_Dst_Ports, dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>spts rst. primitive_extractor (is_Dst_Ports, dst_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_Dst_Ports, dst_ports_sel) m = (spts, rst) \<Longrightarrow> getNeg spts = []
 2. \<And>spts rst. \<lbrakk>primitive_extractor (is_Dst_Ports, dst_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 (Dst_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_Dst_Ports, dst_ports_sel) m = (spts_, rst_) \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
apply(drule primitive_extractor_correct(8)[OF n wf_disc_sel_common_primitive(2)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> has_disc_negated is_Dst_Ports False m) = (getNeg spts_ = []) \<Longrightarrow> getNeg spts_ = []
[PROOF STEP]
using noneg
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated is_Dst_Ports False m

goal (1 subgoal):
 1. (\<not> has_disc_negated is_Dst_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_Dst_Ports, dst_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 (Dst_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_Dst_Ports, dst_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 (Dst_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(2), 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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_dst_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 Dst_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> Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 Dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_MatchesAll(2)[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 Dst_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> Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_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 Dst_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 (Dst_Ports spt)) rst) (singletonize_L4Ports x3)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(drule raw_ports_compress_dst_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 Dst_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Dst_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (getPos spts))) a p\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (\<lambda>spt. MatchAnd (Match (Dst_Ports spt)) rst) (singletonize_L4Ports x3)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(insert singletonize_L4Ports_dst[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 Dst_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Dst_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (getPos spts))) a p; \<And>pts. match_list (\<beta>, \<alpha>) (map (Match \<circ> Dst_Ports) (singletonize_L4Ports pts)) a p = matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (map (\<lambda>spt. MatchAnd (Match (Dst_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 Dst_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Dst_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (getPos spts))) a p; \<And>pts. (\<exists>m\<in>set (singletonize_L4Ports pts). matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p) = matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p\<rbrakk> \<Longrightarrow> (\<exists>m\<in>set (singletonize_L4Ports x3). matches (\<beta>, \<alpha>) (MatchAnd (Match (Dst_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 Dst_Ports spts)) a p \<and> matches (\<beta>, \<alpha>) rst a p) = matches (\<beta>, \<alpha>) m a p; matches (\<beta>, \<alpha>) (Match (Dst_Ports x3)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (getPos spts))) a p; \<And>pts. (\<exists>m\<in>set (singletonize_L4Ports pts). matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p) = matches (\<beta>, \<alpha>) (Match (Dst_Ports pts)) a p\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_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


[STATEMENT]
lemma normalize_positive_src_ports_nnf:
    assumes n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Src_Ports False m"
    shows "m' \<in> set (normalize_positive_src_ports m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_positive_src_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(rule normalize_positive_ports_step_nnf[OF n wf_disc_sel_common_primitive(1) noneg])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_positive_src_ports m) \<Longrightarrow> m' \<in> set (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports m)
[PROOF STEP]
by(simp add: normalize_positive_src_ports_def)


[STATEMENT]
lemma normalize_positive_dst_ports_nnf:
    assumes n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Dst_Ports False m"
    shows "m' \<in> set (normalize_positive_dst_ports m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_positive_dst_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(rule normalize_positive_ports_step_nnf[OF n wf_disc_sel_common_primitive(2) noneg])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_positive_dst_ports m) \<Longrightarrow> m' \<in> set (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports m)
[PROOF STEP]
by(simp add: normalize_positive_dst_ports_def)


[STATEMENT]
lemma normalize_positive_src_ports_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Src_Ports False m"
    shows "\<forall>m' \<in> set (normalize_positive_src_ports m). normalized_src_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_src_ports m). normalized_src_ports m'
[PROOF STEP]
unfolding normalized_src_ports_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_src_ports m). normalized_n_primitive (is_Src_Ports, src_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
unfolding normalize_positive_src_ports_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports m). normalized_n_primitive (is_Src_Ports, src_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
using normalize_positive_ports_step_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1) noneg]
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports m). normalized_n_primitive (is_Src_Ports, src_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'

goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports m). normalized_n_primitive (is_Src_Ports, src_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_positive_dst_ports_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
    and noneg: "\<not> has_disc_negated is_Dst_Ports False m"
    shows "\<forall>m' \<in> set (normalize_positive_dst_ports m). normalized_dst_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_dst_ports m). normalized_dst_ports m'
[PROOF STEP]
unfolding normalized_dst_ports_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_dst_ports m). normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
unfolding normalize_positive_dst_ports_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports m). normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
using normalize_positive_ports_step_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2) noneg]
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports m). normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'

goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports m). normalized_n_primitive (is_Dst_Ports, dst_ports_sel) (case_ipt_l4_ports (\<lambda>x pts. length pts \<le> 1)) m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_ports_generic_nnf:
    assumes n: "normalized_nnf_match m"
    and inset: "m' \<in> set (normalize_ports_generic normalize_pos rewrite_neg m)"
    and noNeg: "\<not> has_disc_negated disc False (rewrite_neg m)"
    and normalize_nnf_pos: "\<And>m m'.
        normalized_nnf_match  m \<Longrightarrow> \<not> has_disc_negated disc False m \<Longrightarrow>
          m' \<in> set (normalize_pos m) \<Longrightarrow> normalized_nnf_match m'"
    shows "normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_nnf_match m'
[PROOF STEP]
using inset
[PROOF STATE]
proof (prove)
using this:
m' \<in> set (normalize_ports_generic normalize_pos rewrite_neg m)

goal (1 subgoal):
 1. normalized_nnf_match m'
[PROOF STEP]
apply(simp add: normalize_ports_generic_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>set (normalize_match (rewrite_neg m)). m' \<in> set (normalize_pos x) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(elim bexE, rename_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(subgoal_tac "normalized_nnf_match a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (2 subgoals):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(erule normalize_nnf_pos, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a
[PROOF STEP]
apply(rule not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (?m24 a)
 2. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> a \<in> set (normalize_match (?m24 a))
[PROOF STEP]
using noNeg n
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc False (rewrite_neg m)
normalized_nnf_match m

goal (2 subgoals):
 1. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (?m24 a)
 2. \<And>a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> a \<in> set (normalize_match (?m24 a))
[PROOF STEP]
by blast+


[STATEMENT]
lemma normalize_ports_generic:
    assumes n: "normalized_nnf_match m"
    and normalize_pos: "\<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated disc False m \<Longrightarrow>
                          match_list \<gamma> (normalize_pos m) a p \<longleftrightarrow> matches \<gamma> m a p"
    and rewrite_neg: "\<And>m. normalized_nnf_match m \<Longrightarrow>
                          matches \<gamma> (rewrite_neg m) a p = matches \<gamma> m a p"
    and noNeg: "\<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)"
    shows
        "match_list \<gamma> (normalize_ports_generic normalize_pos rewrite_neg m) a p \<longleftrightarrow> matches \<gamma> m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list \<gamma> (normalize_ports_generic normalize_pos rewrite_neg m) a p = matches \<gamma> m a p
[PROOF STEP]
unfolding normalize_ports_generic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p = matches \<gamma> m a p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p \<Longrightarrow> matches \<gamma> m a p
 2. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
have 1: "ls \<in> set (normalize_match (rewrite_neg m)) \<Longrightarrow>
          match_list \<gamma> (normalize_pos ls) a p \<Longrightarrow> normalized_nnf_match ls \<Longrightarrow> matches \<gamma> m a p"
      for ls
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
apply(subst(asm) normalize_pos)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
 2. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ls
 3. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ls
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ls
[PROOF STEP]
apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
using noNeg n
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg ?m)
normalized_nnf_match m

goal (2 subgoals):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>normalized_nnf_match ls; ls \<in> set (normalize_match (rewrite_neg m))\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
apply(subgoal_tac "matches \<gamma> (rewrite_neg m) a p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls; matches \<gamma> (rewrite_neg m) a p\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> (rewrite_neg m) a p
[PROOF STEP]
using rewrite_neg[OF n]
[PROOF STATE]
proof (prove)
using this:
matches \<gamma> (rewrite_neg m) a p = matches \<gamma> m a p

goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls; matches \<gamma> (rewrite_neg m) a p\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> (rewrite_neg m) a p
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> (rewrite_neg m) a p
[PROOF STEP]
using in_normalized_matches[where \<gamma>=\<gamma> and a=a and p=p]
[PROOF STATE]
proof (prove)
using this:
?ls \<in> set (normalize_match ?m) \<and> matches \<gamma> ?ls a p \<Longrightarrow> matches \<gamma> ?m a p

goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> (rewrite_neg m) a p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ?ls) a p; normalized_nnf_match ?ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p

goal (2 subgoals):
 1. match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p \<Longrightarrow> matches \<gamma> m a p
 2. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
show "match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p \<Longrightarrow> matches \<gamma> m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
apply(simp add: match_list_concat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ls\<in>set (normalize_match (rewrite_neg m)). match_list \<gamma> (normalize_pos ls) a p \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
apply(clarify, rename_tac ls)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
[PROOF STEP]
apply(subgoal_tac "normalized_nnf_match ls")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
 2. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ?ls) a p; normalized_nnf_match ?ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> m a p
 2. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); match_list \<gamma> (normalize_pos ls) a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p \<Longrightarrow> matches \<gamma> m a p

goal (1 subgoal):
 1. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
have 1: "ls \<in> set (normalize_match (rewrite_neg m)) \<Longrightarrow>
          matches \<gamma> ls a p \<Longrightarrow>
          normalized_nnf_match ls \<Longrightarrow>
          match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p" for ls
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(simp add: match_list_concat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> \<exists>ls\<in>set (normalize_match (rewrite_neg m)). match_list \<gamma> (normalize_pos ls) a p
[PROOF STEP]
apply(rule_tac x=ls in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (normalize_pos ls) a p
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (normalize_pos ls) a p
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (normalize_pos ls) a p
[PROOF STEP]
apply(subst normalize_pos)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ls
 3. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> matches \<gamma> ls a p
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ls
[PROOF STEP]
apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
using noNeg n
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg ?m)
normalized_nnf_match m

goal (2 subgoals):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> ls \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ?ls a p; normalized_nnf_match ?ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p

goal (1 subgoal):
 1. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
show "matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(subst(asm) rewrite_neg[OF n, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches \<gamma> (rewrite_neg m) a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(subst(asm) matches_to_match_list_normalize)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list \<gamma> (normalize_match (rewrite_neg m)) a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(subst(asm) match_list_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<in>set (normalize_match (rewrite_neg m)). matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(elim bexE, rename_tac ls)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
[PROOF STEP]
apply(subgoal_tac "normalized_nnf_match ls")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
 2. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ?ls a p; normalized_nnf_match ?ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p

goal (2 subgoals):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p; normalized_nnf_match ls\<rbrakk> \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p
 2. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (1 subgoal):
 1. \<And>ls. \<lbrakk>ls \<in> set (normalize_match (rewrite_neg m)); matches \<gamma> ls a p\<rbrakk> \<Longrightarrow> normalized_nnf_match ls
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
matches \<gamma> m a p \<Longrightarrow> match_list \<gamma> (concat (map normalize_pos (normalize_match (rewrite_neg m)))) a p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normalize_ports_generic_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"  and wf_disc_sel: "wf_disc_sel (disc,sel) C"
    and noNeg: "\<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)"
    and normalize_nnf_pos: "\<And>m m'.
        normalized_nnf_match  m \<Longrightarrow> \<not> has_disc_negated disc False m \<Longrightarrow>
          m' \<in> set (normalize_pos m) \<Longrightarrow> normalized_nnf_match m'"
    and normalize_pos: "\<And>m m'.
        normalized_nnf_match m \<Longrightarrow>  \<not> has_disc_negated disc False m \<Longrightarrow>
          \<forall>m'\<in>set (normalize_pos m).
                 normalized_n_primitive (disc,sel) (\<lambda>ps. case ps of L4Ports _ pts \<Rightarrow> length pts \<le> 1) m'"
    shows "\<forall>m' \<in> set (normalize_ports_generic normalize_pos rewrite_neg 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_ports_generic normalize_pos rewrite_neg m). normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
unfolding normalize_ports_generic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (concat (map normalize_pos (normalize_match (rewrite_neg 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 (concat (map normalize_pos (normalize_match (rewrite_neg 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>x\<in>set (normalize_match (rewrite_neg m)). m' \<in> set (normalize_pos x) \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply(elim bexE, rename_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<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_nnf_match a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<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_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<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 "\<not> has_disc_negated disc False a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
subgoal for ls
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a_
[PROOF STEP]
(*TODO: same is already above!*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a_
[PROOF STEP]
apply(rule_tac m="rewrite_neg m" in not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> a_ \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
using noNeg n
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg ?m)
normalized_nnf_match m

goal (2 subgoals):
 1. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_neg m)
 2. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> a_ \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_ \<in> set (normalize_match (rewrite_neg m)); ls \<in> set (normalize_pos a_); normalized_nnf_match a_\<rbrakk> \<Longrightarrow> a_ \<in> set (normalize_match (rewrite_neg m))
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<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_nnf_match m'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a; normalized_nnf_match m'\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a; normalized_nnf_match m'\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
using normalize_nnf_pos
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated disc False ?m; ?m' \<in> set (normalize_pos ?m)\<rbrakk> \<Longrightarrow> normalized_nnf_match ?m'

goal (2 subgoals):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a; normalized_nnf_match 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 blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a; normalized_nnf_match m'\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'
[PROOF STEP]
using normalize_pos
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated disc False ?m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_pos ?m). normalized_n_primitive (disc, sel) (\<lambda>ps. case ps of L4Ports x pts \<Rightarrow> length pts \<le> 1) m'

goal (1 subgoal):
 1. \<And>m' a. \<lbrakk>a \<in> set (normalize_match (rewrite_neg m)); m' \<in> set (normalize_pos a); normalized_nnf_match a; \<not> has_disc_negated disc False a; normalized_nnf_match m'\<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 normalize_ports_generic_normalize_positive_ports_step_erule:
    assumes n: "normalized_nnf_match m"
      and wf_disc_sel: "wf_disc_sel (disc, sel) C"
      and noProt: "\<forall>a. \<not> disc (Prot a)" (*disc is src_ports or dst_ports anyway*)
      and P: "P (disc2, sel2) m"
      and P1: "\<And>a. normalized_nnf_match a \<Longrightarrow>
                a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)) \<Longrightarrow>
                P (disc2, sel2) a"
      and P2: "\<And>a dpts rst. normalized_nnf_match a \<Longrightarrow>
                    primitive_extractor (disc, sel) a = (dpts, rst) \<Longrightarrow>
                    getNeg dpts = [] \<Longrightarrow> P (disc2, sel2) a \<Longrightarrow> P (disc2, sel2) rst"
      and P3: "\<And> a spt rst. P (disc2, sel2) rst \<Longrightarrow> P (disc2, sel2) (MatchAnd (Match (C spt)) rst)"
    shows "m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) \<Longrightarrow>
          P (disc2, sel2) m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P (disc2, sel2) m

goal (1 subgoal):
 1. m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(simp add: normalize_ports_generic_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>x\<in>set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)). m' \<in> set (normalize_positive_ports_step (disc, sel) C x); P (disc2, sel2) m\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(elim bexE, rename_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(subgoal_tac "normalized_nnf_match a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
 2. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (2 subgoals):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a)\<rbrakk> \<Longrightarrow> normalized_nnf_match a
 2. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (normalize_positive_ports_step (disc, sel) C a); normalized_nnf_match a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(simp add: normalize_positive_ports_step_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<exists>uu_ uua_. (uua_, uu_) = primitive_extractor (disc, sel) a \<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)); normalized_nnf_match a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(elim exE conjE, rename_tac rst dpts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; (dpts, rst) = primitive_extractor (disc, sel) a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m))\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
(*primitive extractor*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(subgoal_tac "getNeg dpts = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
 2. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> getNeg dpts = []
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> getNeg dpts = []
 2. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
subgoal for a rst dpts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> getNeg dpts = []
[PROOF STEP]
apply(erule iffD1[OF primitive_extractor_correct(8)[OF _ wf_disc_sel]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) a = (dpts, ?ms1)
 2. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False a
[PROOF STEP]
apply(rule not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False ?m8
 2. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> a \<in> set (normalize_match ?m8)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(rule rewrite_negated_primitives_not_has_disc_negated[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>pts. \<not> has_disc_negated disc False (l4_ports_negate_one C pts)
[PROOF STEP]
apply(intro allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (l4_ports_negate_one C pts)
[PROOF STEP]
apply(rule l4_ports_negate_one_not_has_disc_negated_generic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc (Prot a)
[PROOF STEP]
by(simp add: noProt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(subgoal_tac "P (disc2, sel2) a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
 2. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) a
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) a
 2. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (disc2, sel2) m; a_ \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a_; m' \<in> set (case getNeg dpts_ of [] \<Rightarrow> case l4_ports_compress (getPos dpts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a_ = (dpts_, rst_); getNeg dpts_ = []\<rbrakk> \<Longrightarrow> P (disc2, sel2) a_
[PROOF STEP]
apply(rule P1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P (disc2, sel2) m; a_ \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a_; m' \<in> set (case getNeg dpts_ of [] \<Rightarrow> case l4_ports_compress (getPos dpts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a_ = (dpts_, rst_); getNeg dpts_ = []\<rbrakk> \<Longrightarrow> normalized_nnf_match a_
 2. \<lbrakk>P (disc2, sel2) m; a_ \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a_; m' \<in> set (case getNeg dpts_ of [] \<Rightarrow> case l4_ports_compress (getPos dpts_) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst_] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst_) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a_ = (dpts_, rst_); getNeg dpts_ = []\<rbrakk> \<Longrightarrow> a_ \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(frule_tac a=a in P2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) a = (?dpts28 a rst dpts, ?rst28 a rst dpts)
 2. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> getNeg (?dpts28 a rst dpts) = []
 3. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a\<rbrakk> \<Longrightarrow> P (disc2, sel2) a
 4. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a; P (disc2, sel2) (?rst28 a rst dpts)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts. \<lbrakk>P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; m' \<in> set (case getNeg dpts of [] \<Rightarrow> case l4_ports_compress (getPos dpts) of CannotMatch \<Rightarrow> [] | MatchesAll \<Rightarrow> [rst] | MatchExpr m \<Rightarrow> map (\<lambda>spt. MatchAnd (Match (C spt)) rst) (singletonize_L4Ports m)); primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a; P (disc2, sel2) rst\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
apply(simp split: match_compress.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a rst dpts x3. \<lbrakk>primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a; P (disc2, sel2) rst; P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; l4_ports_compress (getPos dpts) = MatchExpr x3; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports x3)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
using P3
[PROOF STATE]
proof (prove)
using this:
P (disc2, sel2) ?rst \<Longrightarrow> P (disc2, sel2) (MatchAnd (Match (C ?spt)) ?rst)

goal (1 subgoal):
 1. \<And>a rst dpts x3. \<lbrakk>primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; P (disc2, sel2) a; P (disc2, sel2) rst; P (disc2, sel2) m; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); normalized_nnf_match a; l4_ports_compress (getPos dpts) = MatchExpr x3; m' \<in> (\<lambda>spt. MatchAnd (Match (C spt)) rst) ` set (singletonize_L4Ports x3)\<rbrakk> \<Longrightarrow> P (disc2, sel2) m'
[PROOF STEP]
by auto


[STATEMENT]
lemma normalize_ports_generic_preserves_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
      and wf_disc_sel: "wf_disc_sel (disc, sel) C"
      and noProt: "\<forall>a. \<not> disc (Prot a)" (*disc is src_ports or dst_ports anyway*)
      and disc2_noC: "\<forall>a. \<not> disc2 (C a)"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m"
    shows "m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m) \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f m \<Longrightarrow>
          normalized_n_primitive (disc2, sel2) f m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
thm normalize_ports_generic_normalize_positive_ports_step_erule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(rule normalize_ports_generic_normalize_positive_ports_step_erule[OF n wf_disc_sel noProt])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m
 2. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; 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
 3. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
 4. \<And>a spt rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_n_primitive (disc2, sel2) f rst\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f (MatchAnd (Match (C spt)) rst)
 5. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m)
[PROOF STEP]
apply(simp_all add: disc2_noC disc2_noProt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; 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
 2. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
apply(rule rewrite_negated_primitives_normalized_preserves_unrelated_helper[OF wf_disc_sel _ _ n])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (C a)
 2. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m
 3. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m
 4. \<And>a. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))
 5. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
apply(simp_all add: disc2_noC disc2_noProt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
apply(frule_tac m=a in primitive_extractor_correct(5)[OF _ wf_disc_sel, where P=f])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) a = (?as13 a dpts rst, ?ms13 a dpts rst)
 2. \<And>a dpts rst. \<lbrakk>m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (disc, sel) C) (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one) m); normalized_n_primitive (disc2, sel2) f m; normalized_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; normalized_n_primitive (disc2, sel2) f a; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f a \<longrightarrow> normalized_n_primitive (disc2, sel2) f (?ms13 a dpts rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f rst
[PROOF STEP]
by blast+