[STATEMENT]
lemma normalize_ports_generic_preserves_normalized_not_has_disc:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc disc2 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> \<not> has_disc disc2 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> \<not> has_disc disc2 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. 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> \<not> has_disc disc2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc disc2 a\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 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); \<not> has_disc disc2 rst\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (MatchAnd (Match (C spt)) rst)
 5. 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> 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 nodisc)
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc disc2 a\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
subgoal for a
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 a
[PROOF STEP]
thm normalize_match_preserves_nodisc
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 a
[PROOF STEP]
apply(rule_tac m="rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m" in normalize_match_preserves_nodisc)
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
 2. \<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_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))
[PROOF STEP]
apply(simp_all)
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(insert disc2_noProt)
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(elim disjE)
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<forall>a. \<not> disc2 (Prot a)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
 2. \<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_nnf_match a; 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> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
thm rewrite_negated_primitives_not_has_disc[of _ disc2]
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<forall>a. \<not> disc2 (Prot a)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
 2. \<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_nnf_match a; 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> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
subgoal
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<forall>a. \<not> disc2 (Prot a)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(rule rewrite_negated_primitives_not_has_disc[OF n wf_disc_sel nodisc _ disc2_noC])
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<forall>a. \<not> disc2 (Prot a); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>pts. \<not> has_disc disc2 (l4_ports_negate_one C pts)
[PROOF STEP]
using l4_ports_negate_one_nodisc[OF disc2_noC]
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> disc2 (Prot a) \<Longrightarrow> \<not> has_disc disc2 (l4_ports_negate_one C ?pt)

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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); \<forall>a. \<not> disc2 (Prot a); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>pts. \<not> has_disc disc2 (l4_ports_negate_one C pts)
[PROOF STEP]
by blast
[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_nnf_match a; 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> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
using rewrite_negated_primitives_preserves_not_has_disc[OF n wf_disc_sel nodisc _ disc2_noC]
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc False m \<Longrightarrow> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)

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_nnf_match a; 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> \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
by blast
[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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc disc2 a\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(frule_tac m=a in primitive_extractor_correct(4)[OF _ wf_disc_sel])
[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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc disc2 a\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) a = (?as6 a dpts rst, ?ms6 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc disc2 a; \<forall>disc2. \<not> has_disc disc2 a \<longrightarrow> \<not> has_disc disc2 (?ms6 a dpts rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
by blast+


[STATEMENT]
lemma normalize_ports_generic_preserves_normalized_not_has_disc_negated:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc_negated disc2 False 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_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> \<not> has_disc_negated disc2 False 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> \<not> has_disc_negated disc2 False 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. 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> \<not> has_disc_negated disc2 False 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False 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); \<not> has_disc_negated disc2 False rst\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (MatchAnd (Match (C spt)) rst)
 5. 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> 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_noProt nodisc)
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
subgoal for a
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False a
[PROOF STEP]
apply(rule_tac m="rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m" in not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
 2. \<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_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))
[PROOF STEP]
apply(simp_all)
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(rule rewrite_negated_primitives_preserves_not_has_disc_negated[OF n wf_disc_sel ])
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>pts. \<not> has_disc_negated disc2 False (l4_ports_negate_one C pts)
 2. \<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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
[PROOF STEP]
using disc2_noProt l4_ports_negate_one_not_has_disc_negated_generic
[PROOF STATE]
proof (prove)
using this:
(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated disc False m
\<forall>a. \<not> ?disc (Prot a) \<Longrightarrow> \<not> has_disc_negated ?disc False (l4_ports_negate_one ?C ?ports)

goal (2 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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)); has_disc_negated disc False m\<rbrakk> \<Longrightarrow> \<forall>pts. \<not> has_disc_negated disc2 False (l4_ports_negate_one C pts)
 2. \<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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
[PROOF STEP]
apply blast
[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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
[PROOF STEP]
using nodisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc2 False m

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_nnf_match a; a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
[PROOF STEP]
by blast
[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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
subgoal for a dpts rst
[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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply(frule_tac m=a and as=dpts and ms=rst and neg=False in primitive_extractor_correct(6)[OF _ wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (2 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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a\<rbrakk> \<Longrightarrow> primitive_extractor (disc, sel) a = (dpts, rst)
 2. \<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_nnf_match a; primitive_extractor (disc, sel) a = (dpts, rst); getNeg dpts = []; \<not> has_disc_negated disc2 False a; \<forall>disc2. \<not> has_disc_negated disc2 False a \<longrightarrow> \<not> has_disc_negated disc2 False rst\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
by blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma normalize_src_ports:
    assumes generic: "primitive_matcher_generic \<beta>"
    and n: "normalized_nnf_match m"
    shows "match_list (\<beta>, \<alpha>) (normalize_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_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: normalize_src_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (normalize_ports_generic normalize_positive_src_ports rewrite_negated_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(rule normalize_ports_generic[OF n])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (normalize_positive_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>m. normalized_nnf_match m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated ?disc False (rewrite_negated_src_ports m)
[PROOF STEP]
using normalize_positive_src_ports[OF generic]
             rewrite_negated_src_ports[OF generic, where \<alpha>=\<alpha> and a=a and p=p]
             rewrite_negated_src_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Src_Ports False ?m\<rbrakk> \<Longrightarrow> match_list (\<beta>, ?\<alpha>) (normalize_positive_src_ports ?m) ?a ?p = matches (\<beta>, ?\<alpha>) ?m ?a ?p
normalized_nnf_match ?m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_src_ports ?m) a p = matches (\<beta>, \<alpha>) ?m a p
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports ?m)

goal (3 subgoals):
 1. \<And>m. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (normalize_positive_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>m. normalized_nnf_match m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_src_ports m) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated ?disc False (rewrite_negated_src_ports m)
[PROOF STEP]
by blast+


[STATEMENT]
lemma normalize_dst_ports:
    assumes generic: "primitive_matcher_generic \<beta>"
    and n: "normalized_nnf_match m"
    shows "match_list (\<beta>, \<alpha>) (normalize_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_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(simp add: normalize_dst_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (normalize_ports_generic normalize_positive_dst_ports rewrite_negated_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(rule normalize_ports_generic[OF n])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (normalize_positive_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>m. normalized_nnf_match m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated ?disc False (rewrite_negated_dst_ports m)
[PROOF STEP]
using normalize_positive_dst_ports[OF generic]
             rewrite_negated_dst_ports[OF generic, where \<alpha>=\<alpha> and a=a and p=p]
             rewrite_negated_dst_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Dst_Ports False ?m\<rbrakk> \<Longrightarrow> match_list (\<beta>, ?\<alpha>) (normalize_positive_dst_ports ?m) ?a ?p = matches (\<beta>, ?\<alpha>) ?m ?a ?p
normalized_nnf_match ?m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_dst_ports ?m) a p = matches (\<beta>, \<alpha>) ?m a p
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports ?m)

goal (3 subgoals):
 1. \<And>m. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m\<rbrakk> \<Longrightarrow> match_list (\<beta>, \<alpha>) (normalize_positive_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
 2. \<And>m. normalized_nnf_match m \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_negated_dst_ports m) a p = matches (\<beta>, \<alpha>) m a p
 3. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated ?disc False (rewrite_negated_dst_ports m)
[PROOF STEP]
by blast+


[STATEMENT]
lemma normalize_src_ports_normalized_n_primitive:
    assumes n:"normalized_nnf_match m"
    shows "\<forall>m' \<in> set (normalize_src_ports m). normalized_src_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_src_ports m). normalized_src_ports m'
[PROOF STEP]
unfolding normalize_src_ports_def normalized_src_ports_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_ports_generic normalize_positive_src_ports rewrite_negated_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]
apply(rule normalize_ports_generic_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 3. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
using rewrite_negated_src_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports ?m)

goal (3 subgoals):
 1. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 3. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
using normalize_positive_src_ports_nnf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Src_Ports False ?m; ?m' \<in> set (normalize_positive_src_ports ?m)\<rbrakk> \<Longrightarrow> normalized_nnf_match ?m'

goal (2 subgoals):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
unfolding normalized_src_ports_def2[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_src_ports m). normalized_src_ports m'
[PROOF STEP]
using normalize_positive_src_ports_normalized_n_primitive
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Src_Ports False ?m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_src_ports ?m). normalized_src_ports m'

goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_src_ports m). normalized_src_ports m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_dst_ports_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
    shows "\<forall>m' \<in> set (normalize_dst_ports m). normalized_dst_ports m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_dst_ports m). normalized_dst_ports m'
[PROOF STEP]
unfolding normalize_dst_ports_def normalized_dst_ports_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m'\<in>set (normalize_ports_generic normalize_positive_dst_ports rewrite_negated_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]
apply(rule normalize_ports_generic_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 3. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
using rewrite_negated_dst_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports ?m)

goal (3 subgoals):
 1. \<And>m. normalized_nnf_match m \<Longrightarrow> \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 3. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
using normalize_positive_dst_ports_nnf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Dst_Ports False ?m; ?m' \<in> set (normalize_positive_dst_ports ?m)\<rbrakk> \<Longrightarrow> normalized_nnf_match ?m'

goal (2 subgoals):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_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'
[PROOF STEP]
unfolding normalized_dst_ports_def2[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_dst_ports m). normalized_dst_ports m'
[PROOF STEP]
using normalize_positive_dst_ports_normalized_n_primitive
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Dst_Ports False ?m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_dst_ports ?m). normalized_dst_ports m'

goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_positive_dst_ports m). normalized_dst_ports m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_src_ports_nnf:
    assumes n: "normalized_nnf_match m"
    shows "m' \<in> set (normalize_src_ports m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(simp add: normalize_src_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_ports_generic normalize_positive_src_ports rewrite_negated_src_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(erule normalize_ports_generic_nnf[OF n])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> has_disc_negated ?disc False (rewrite_negated_src_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using n rewrite_negated_src_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match m
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Src_Ports False (rewrite_negated_src_ports ?m)

goal (2 subgoals):
 1. \<not> has_disc_negated ?disc False (rewrite_negated_src_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using normalize_positive_src_ports_nnf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Src_Ports False ?m; ?m' \<in> set (normalize_positive_src_ports ?m)\<rbrakk> \<Longrightarrow> normalized_nnf_match ?m'

goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Src_Ports False m; m' \<in> set (normalize_positive_src_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_dst_ports_nnf:
    assumes n: "normalized_nnf_match m"
    shows "m' \<in> set (normalize_dst_ports m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(simp add: normalize_dst_ports_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_ports_generic normalize_positive_dst_ports rewrite_negated_dst_ports m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(erule normalize_ports_generic_nnf[OF n])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> has_disc_negated ?disc False (rewrite_negated_dst_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using n rewrite_negated_dst_ports_not_has_disc_negated
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match m
normalized_nnf_match ?m \<Longrightarrow> \<not> has_disc_negated is_Dst_Ports False (rewrite_negated_dst_ports ?m)

goal (2 subgoals):
 1. \<not> has_disc_negated ?disc False (rewrite_negated_dst_ports m)
 2. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated ?disc False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using normalize_positive_dst_ports_nnf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>normalized_nnf_match ?m; \<not> has_disc_negated is_Dst_Ports False ?m; ?m' \<in> set (normalize_positive_dst_ports ?m)\<rbrakk> \<Longrightarrow> normalized_nnf_match ?m'

goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>normalized_nnf_match m; \<not> has_disc_negated is_Dst_Ports False m; m' \<in> set (normalize_positive_dst_ports m)\<rbrakk> \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_src_ports_preserves_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
      and disc2_noC: "\<forall>a. \<not> disc2 (Src_Ports a)"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m"
    shows "m' \<in> set (normalize_src_ports 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_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_n_primitive[OF n wf_disc_sel_common_primitive(1)])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' \<in> set (normalize_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> \<forall>a. \<not> is_Src_Ports (Prot a)
 2. \<lbrakk>m' \<in> set (normalize_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (Src_Ports a)
 3. \<lbrakk>m' \<in> set (normalize_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m
 4. \<lbrakk>m' \<in> set (normalize_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one) m)
 5. \<lbrakk>m' \<in> set (normalize_src_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m
[PROOF STEP]
by(simp_all add: disc2_noC disc2_noProt normalize_src_ports_def normalize_ports_generic_def
                normalize_positive_src_ports_def rewrite_negated_src_ports_def)


[STATEMENT]
lemma normalize_dst_ports_preserves_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
      and disc2_noC: "\<forall>a. \<not> disc2 (Dst_Ports a)"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m"
    shows "m' \<in> set (normalize_dst_ports 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_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_n_primitive[OF n wf_disc_sel_common_primitive(2)])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' \<in> set (normalize_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> \<forall>a. \<not> is_Dst_Ports (Prot a)
 2. \<lbrakk>m' \<in> set (normalize_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc2 (Dst_Ports a)
 3. \<lbrakk>m' \<in> set (normalize_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m
 4. \<lbrakk>m' \<in> set (normalize_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one) m)
 5. \<lbrakk>m' \<in> set (normalize_dst_ports m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m
[PROOF STEP]
by(simp_all add: disc2_noC disc2_noProt normalize_dst_ports_def normalize_ports_generic_def
                normalize_positive_dst_ports_def rewrite_negated_dst_ports_def)


[STATEMENT]
lemma normalize_src_ports_preserves_normalized_not_has_disc:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc disc2 m"
      and disc2_noC: "\<forall>a. \<not> disc2 (Src_Ports a)"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m"
     shows "m'\<in> set (normalize_src_ports m)
      \<Longrightarrow> \<not> has_disc disc2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc[OF n nodisc wf_disc_sel_common_primitive(1)])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> \<forall>a. \<not> is_Src_Ports (Prot a)
 2. m' \<in> set (normalize_src_ports m) \<Longrightarrow> \<forall>a. \<not> disc2 (Src_Ports a)
 3. m' \<in> set (normalize_src_ports m) \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m
 4. m' \<in> set (normalize_src_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one) m)
[PROOF STEP]
apply(simp add: disc2_noC disc2_noProt)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one) m)
[PROOF STEP]
by (simp add: normalize_ports_generic_def normalize_positive_src_ports_def normalize_src_ports_def rewrite_negated_src_ports_def)


[STATEMENT]
lemma normalize_dst_ports_preserves_normalized_not_has_disc:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc disc2 m"
      and disc2_noC: "\<forall>a. \<not> disc2 (Dst_Ports a)"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m"
     shows "m'\<in> set (normalize_dst_ports m)
      \<Longrightarrow> \<not> has_disc disc2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc[OF n nodisc wf_disc_sel_common_primitive(2)])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> \<forall>a. \<not> is_Dst_Ports (Prot a)
 2. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> \<forall>a. \<not> disc2 (Dst_Ports a)
 3. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m
 4. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one) m)
[PROOF STEP]
apply(simp add: disc2_noC disc2_noProt)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one) m)
[PROOF STEP]
by (simp add: normalize_ports_generic_def normalize_positive_dst_ports_def normalize_dst_ports_def rewrite_negated_dst_ports_def)


[STATEMENT]
lemma normalize_src_ports_preserves_normalized_not_has_disc_negated:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc_negated disc2 False m"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m"
     shows "m'\<in> set (normalize_src_ports m)
      \<Longrightarrow> \<not> has_disc_negated disc2 False m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> \<not> has_disc_negated disc2 False m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc_negated[OF n nodisc wf_disc_sel_common_primitive(1)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> \<forall>a. \<not> is_Src_Ports (Prot a)
 2. m' \<in> set (normalize_src_ports m) \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Src_Ports False m
 3. m' \<in> set (normalize_src_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one) m)
[PROOF STEP]
apply(simp add: disc2_noProt)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_src_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Src_Ports, src_ports_sel) Src_Ports) (rewrite_negated_primitives (is_Src_Ports, src_ports_sel) Src_Ports l4_ports_negate_one) m)
[PROOF STEP]
by (simp add: normalize_ports_generic_def normalize_positive_src_ports_def normalize_src_ports_def rewrite_negated_src_ports_def)


[STATEMENT]
lemma normalize_dst_ports_preserves_normalized_not_has_disc_negated:
    assumes n: "normalized_nnf_match m" and nodisc: "\<not> has_disc_negated disc2 False m"
      and disc2_noProt: "(\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m"
     shows "m'\<in> set (normalize_dst_ports m)
      \<Longrightarrow> \<not> has_disc_negated disc2 False m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> \<not> has_disc_negated disc2 False m'
[PROOF STEP]
apply(rule normalize_ports_generic_preserves_normalized_not_has_disc_negated[OF n nodisc wf_disc_sel_common_primitive(2)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> \<forall>a. \<not> is_Dst_Ports (Prot a)
 2. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> (\<forall>a. \<not> disc2 (Prot a)) \<or> \<not> has_disc_negated is_Dst_Ports False m
 3. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one) m)
[PROOF STEP]
apply(simp add: disc2_noProt)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_dst_ports m) \<Longrightarrow> m' \<in> set (normalize_ports_generic (normalize_positive_ports_step (is_Dst_Ports, dst_ports_sel) Dst_Ports) (rewrite_negated_primitives (is_Dst_Ports, dst_ports_sel) Dst_Ports l4_ports_negate_one) m)
[PROOF STEP]
by (simp add: normalize_ports_generic_def normalize_positive_dst_ports_def normalize_dst_ports_def rewrite_negated_dst_ports_def)


[STATEMENT]
lemma "map opt_MatchAny_match_expr (normalize_src_ports
                (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
                   (MatchAnd (Match (Prot (Proto TCP)))
                        (MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
                 ))) =
 [MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP)))),
  MatchAnd (Match (Src_Ports (L4Ports UDP [(0, 79)]))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP)))),
  MatchAnd (Match (Src_Ports (L4Ports UDP [(81, 0xFFFF)]))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto TCP))))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map opt_MatchAny_match_expr (normalize_src_ports (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8))) (MatchAnd (Match (Prot (Proto TCP))) (MatchNot (Match (Src_Ports (L4Ports UDP [(80, 80)]))))))) = [MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 2130706432 8))) (Match (Prot (Proto TCP)))), MatchAnd (Match (Src_Ports (L4Ports UDP [(0, 79)]))) (MatchAnd (Match (Dst (IpAddrNetmask 2130706432 8))) (Match (Prot (Proto TCP)))), MatchAnd (Match (Src_Ports (L4Ports UDP [(81, 65535)]))) (MatchAnd (Match (Dst (IpAddrNetmask 2130706432 8))) (Match (Prot (Proto TCP))))]
[PROOF STEP]
by eval


[STATEMENT]
lemma "map opt_MatchAny_match_expr (normalize_src_ports
                (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8)))
                   (MatchAnd (Match (Prot (Proto ICMP)))
                     (MatchAnd (Match (Src_Ports (L4Ports TCP [(22,22)])))
                        (MatchNot (Match (Src_Ports (L4Ports UDP [(80,80)]))))
                 ))))
 =
[MatchAnd (Match (Src_Ports (L4Ports TCP [(22, 22)])))
   (MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 0x7F000000 8))) (Match (Prot (Proto ICMP)))))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map opt_MatchAny_match_expr (normalize_src_ports (MatchAnd (Match (Dst (IpAddrNetmask (ipv4addr_of_dotdecimal (127, 0, 0, 0)) 8))) (MatchAnd (Match (Prot (Proto ICMP))) (MatchAnd (Match (Src_Ports (L4Ports TCP [(22, 22)]))) (MatchNot (Match (Src_Ports (L4Ports UDP [(80, 80)])))))))) = [MatchAnd (Match (Src_Ports (L4Ports TCP [(22, 22)]))) (MatchAnd (MatchNot (Match (Prot (Proto UDP)))) (MatchAnd (Match (Dst (IpAddrNetmask 2130706432 8))) (Match (Prot (Proto ICMP)))))]
[PROOF STEP]
by eval


[STATEMENT]
lemma "map opt_MatchAny_match_expr (normalize_src_ports
                (MatchAnd (Match ((Src_Ports (L4Ports UDP [(21,21), (22,22)])) :: 32 common_primitive))
                  (Match (Prot (Proto UDP)))))
  =
[MatchAnd (Match (Src_Ports (L4Ports UDP [(21, 22)]))) (Match (Prot (Proto UDP)))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map opt_MatchAny_match_expr (normalize_src_ports (MatchAnd (Match (Src_Ports (L4Ports UDP [(21, 21), (22, 22)]))) (Match (Prot (Proto UDP))))) = [MatchAnd (Match (Src_Ports (L4Ports UDP [(21, 22)]))) (Match (Prot (Proto UDP)))]
[PROOF STEP]
by eval


[STATEMENT]
lemma "normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) [])) = [MatchAny]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) [])) = [MatchAny]
[PROOF STEP]
by(simp)


[STATEMENT]
lemma replace_primitive_matchexpr_unchanged_if_not_has_disc:
  assumes n: "normalized_nnf_match m"
  and wf_disc_sel: "wf_disc_sel (disc,sel) C" (*any C*)
  and noDisc: "\<not> has_disc disc m"
  shows "replace_primitive_matchexpr (disc,sel) replace_f m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replace_primitive_matchexpr (disc, sel) replace_f m = m
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst) = m
[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. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst) = m
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map replace_f spts)) rst = m
[PROOF STEP]
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); (\<not> has_disc disc m) = (spts = [] \<and> rst = m)\<rbrakk> \<Longrightarrow> spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map replace_f spts)) rst = m
[PROOF STEP]
using noDisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc m

goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); (\<not> has_disc disc m) = (spts = [] \<and> rst = m)\<rbrakk> \<Longrightarrow> spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map replace_f spts)) rst = m
[PROOF STEP]
by blast+


[STATEMENT]
lemma replace_primitive_matchexpr:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel disc_sel C"
  and replace_f: "\<forall>pt. matches \<gamma> (replace_f pt) a p \<longleftrightarrow>
                        matches \<gamma> (negation_type_to_match_expr_f C pt) a p"
  shows "matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p \<longleftrightarrow> matches \<gamma> m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
obtain spts rst where pext: "primitive_extractor disc_sel m = (spts, rst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>spts rst. primitive_extractor disc_sel m = (spts, rst) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "primitive_extractor disc_sel m") simp
[PROOF STATE]
proof (state)
this:
primitive_extractor disc_sel m = (spts, rst)

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
obtain disc sel where disc_sel: "disc_sel = (disc, sel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>disc sel. disc_sel = (disc, sel) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases disc_sel) simp
[PROOF STATE]
proof (state)
this:
disc_sel = (disc, sel)

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
with wf_disc_sel
[PROOF STATE]
proof (chain)
picking this:
wf_disc_sel disc_sel C
disc_sel = (disc, sel)
[PROOF STEP]
have wf_disc_sel': "wf_disc_sel (disc, sel) C"
[PROOF STATE]
proof (prove)
using this:
wf_disc_sel disc_sel C
disc_sel = (disc, sel)

goal (1 subgoal):
 1. wf_disc_sel (disc, sel) C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf_disc_sel (disc, sel) C

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
from disc_sel pext
[PROOF STATE]
proof (chain)
picking this:
disc_sel = (disc, sel)
primitive_extractor disc_sel m = (spts, rst)
[PROOF STEP]
have pext': "primitive_extractor (disc, sel) m = (spts, rst)"
[PROOF STATE]
proof (prove)
using this:
disc_sel = (disc, sel)
primitive_extractor disc_sel m = (spts, rst)

goal (1 subgoal):
 1. primitive_extractor (disc, sel) m = (spts, rst)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
primitive_extractor (disc, sel) m = (spts, rst)

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
have "matches \<gamma> (andfold_MatchExp (map replace_f spts)) a p \<and> matches \<gamma> rst a p \<longleftrightarrow>
       matches \<gamma> m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (matches \<gamma> (andfold_MatchExp (map replace_f spts)) a p \<and> matches \<gamma> rst a p) = matches \<gamma> m a p
[PROOF STEP]
apply(subst primitive_extractor_correct(1)[OF n wf_disc_sel' pext', symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (matches \<gamma> (andfold_MatchExp (map replace_f spts)) a p \<and> matches \<gamma> rst a p) = (matches \<gamma> (alist_and (NegPos_map C spts)) a p \<and> matches \<gamma> rst a p)
[PROOF STEP]
apply(simp add: andfold_MatchExp_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>m\<in>set spts. matches \<gamma> (replace_f m) a p) \<and> matches \<gamma> rst a p) = (matches \<gamma> (alist_and (NegPos_map C spts)) a p \<and> matches \<gamma> rst a p)
[PROOF STEP]
apply(simp add: replace_f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>m\<in>set spts. matches \<gamma> (negation_type_to_match_expr_f C m) a p) \<and> matches \<gamma> rst a p) = (matches \<gamma> (alist_and (NegPos_map C spts)) a p \<and> matches \<gamma> rst a p)
[PROOF STEP]
using alist_and_negation_type_to_match_expr_f_matches
[PROOF STATE]
proof (prove)
using this:
matches ?\<gamma> (alist_and (NegPos_map ?C ?spts)) ?a ?p = (\<forall>m\<in>set ?spts. matches ?\<gamma> (negation_type_to_match_expr_f ?C m) ?a ?p)

goal (1 subgoal):
 1. ((\<forall>m\<in>set spts. matches \<gamma> (negation_type_to_match_expr_f C m) a p) \<and> matches \<gamma> rst a p) = (matches \<gamma> (alist_and (NegPos_map C spts)) a p \<and> matches \<gamma> rst a p)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(matches \<gamma> (andfold_MatchExp (map replace_f spts)) a p \<and> matches \<gamma> rst a p) = matches \<gamma> m a p

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(matches \<gamma> (andfold_MatchExp (map replace_f spts)) a p \<and> matches \<gamma> rst a p) = matches \<gamma> m a p

goal (1 subgoal):
 1. matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p
[PROOF STEP]
by(simp add: replace_primitive_matchexpr_def pext bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (state)
this:
matches \<gamma> (replace_primitive_matchexpr disc_sel replace_f m) a p = matches \<gamma> m a p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma replace_primitive_matchexpr_replaces_disc:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc, sel) C"
  and replace_f: "\<forall>a. \<not> has_disc disc (replace_f a)"
  shows "\<not> has_disc disc (replace_primitive_matchexpr (disc, sel) replace_f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc (replace_primitive_matchexpr (disc, sel) replace_f m)
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)
[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. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> \<not> has_disc disc (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc rst)
[PROOF STEP]
apply(frule primitive_extractor_correct(3)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc rst)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc disc m) = (spts = [] \<and> rst = m)\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc disc m) = (spts = [] \<and> rst = m)\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> rst = m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(case_tac "\<not> has_disc disc m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc disc m) = (spts = [] \<and> rst = m); \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> rst = m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc disc m) = (spts = [] \<and> rst = m); \<not> \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> rst = m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc disc m) = (spts = [] \<and> rst = m); \<not> \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> rst = m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; spts = [] \<longrightarrow> rst \<noteq> m; has_disc disc m\<rbrakk> \<Longrightarrow> spts \<noteq> [] \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(frule(1) primitive_extractor_correct(9)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; spts = [] \<longrightarrow> rst \<noteq> m; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> spts \<noteq> [] \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc (andfold_MatchExp (map replace_f spts))
[PROOF STEP]
apply(rule MatchExpr_Fold.andfold_MatchExp_not_discI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map replace_f spts). \<not> has_disc disc m
[PROOF STEP]
using replace_f
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> has_disc disc (replace_f a)

goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map replace_f spts). \<not> has_disc disc m
[PROOF STEP]
by simp


[STATEMENT]
lemma replace_primitive_matchexpr_preserves_not_has_disc:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
  and nodisc: "\<not> has_disc disc2 m"
  and replace_f: "has_disc disc m \<Longrightarrow> \<forall>pts. \<not> has_disc disc2 (replace_f pts)"
  shows "\<not> has_disc disc2 (replace_primitive_matchexpr (disc,sel) replace_f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc2 (replace_primitive_matchexpr (disc, sel) replace_f m)
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc2 (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)
[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. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> \<not> has_disc disc2 (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(frule primitive_extractor_correct(4)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(case_tac "\<not> has_disc disc m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; \<not> \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primitive_extractor (disc, sel) m = (spts_, rst_); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst_; \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts_ = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts_ \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts_)) \<and> \<not> has_disc disc2 rst_)
[PROOF STEP]
apply(frule primitive_extractor_correct(7)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primitive_extractor (disc, sel) m = (spts_, rst_); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst_; \<not> has_disc disc m; (\<not> has_disc disc m) = (spts_ = [] \<and> rst_ = m)\<rbrakk> \<Longrightarrow> (spts_ = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts_ \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts_)) \<and> \<not> has_disc disc2 rst_)
[PROOF STEP]
using nodisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc2 m

goal (1 subgoal):
 1. \<lbrakk>primitive_extractor (disc, sel) m = (spts_, rst_); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst_; \<not> has_disc disc m; (\<not> has_disc disc m) = (spts_ = [] \<and> rst_ = m)\<rbrakk> \<Longrightarrow> (spts_ = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts_ \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts_)) \<and> \<not> has_disc disc2 rst_)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; \<not> \<not> has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m\<rbrakk> \<Longrightarrow> (spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts)) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts = []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
using nodisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc2 m

goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts = []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f spts))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(rule andfold_MatchExp_not_discI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map replace_f spts). \<not> has_disc disc2 m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(simp add: replace_f; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
using nodisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc2 m

goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; has_disc disc m; spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
by blast


[STATEMENT]
lemma normalize_replace_primitive_matchexpr_preserves_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
      and wf_disc_sel: "wf_disc_sel (disc, sel) C"
      and replace_f:
        "\<And>a m'. m' \<in> set (normalize_match (replace_f a)) \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'"
      and nprim: "normalized_n_primitive (disc2, sel2) f m"
      and m': "m' \<in> set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))"
    shows "normalized_n_primitive (disc2, sel2) f m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
have x: "x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow>
          normalized_n_primitive (disc2, sel2) f x" for x as
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
apply(rule normalize_andfold_MatchExp_normalized_n_primitive )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow> \<forall>m\<in>set ?ms. \<forall>s'\<in>set (normalize_match m). normalized_n_primitive (disc2, sel2) f s'
 2. x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow> x \<in> set (normalize_match (andfold_MatchExp ?ms))
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow> \<forall>m\<in>set as. \<forall>x\<in>set (normalize_match (replace_f m)). normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
using replace_f
[PROOF STATE]
proof (prove)
using this:
?m' \<in> set (normalize_match (replace_f ?a)) \<Longrightarrow> normalized_n_primitive (disc2, sel2) f ?m'

goal (1 subgoal):
 1. x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))) \<Longrightarrow> \<forall>m\<in>set as. \<forall>x\<in>set (normalize_match (replace_f m)). normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> set (normalize_match (andfold_MatchExp (map replace_f ?as))) \<Longrightarrow> normalized_n_primitive (disc2, sel2) f ?x

goal (1 subgoal):
 1. normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
from m'
[PROOF STATE]
proof (chain)
picking this:
m' \<in> set (normalize_match (replace_primitive_matchexpr (disc, sel) replace_f m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m' \<in> set (normalize_match (replace_primitive_matchexpr (disc, sel) replace_f m))

goal (1 subgoal):
 1. normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)) \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)); primitive_extractor (disc, sel) m = (as, rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
using normalize_match_preserves_normalized_n_primitive nprim
[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
normalized_n_primitive (disc2, sel2) f m

goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(frule_tac P=f in primitive_extractor_correct(5)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match 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 m'
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f (MatchAnd x xa)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x \<and> normalized_n_primitive (disc2, sel2) f xa
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
 2. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f xa
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f xa
 2. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
using normalize_match_preserves_normalized_n_primitive nprim
[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
normalized_n_primitive (disc2, sel2) f m

goal (2 subgoals):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f xa
 2. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xa. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2 sel2. normalized_n_primitive (disc2, sel2) f m \<longrightarrow> normalized_n_primitive (disc2, sel2) f rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); xa \<in> set (normalize_match rst); m' = MatchAnd x xa\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f x
[PROOF STEP]
by(simp add: x)
[PROOF STATE]
proof (state)
this:
normalized_n_primitive (disc2, sel2) f m'

goal:
No subgoals!
[PROOF STEP]
qed