[STATEMENT]
lemma raw_ports_compress_src_MatchExpr:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  and c: "l4_ports_compress pss = MatchExpr m"
  shows "matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
l4_ports_compress pss = MatchExpr m

goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p
[PROOF STEP]
apply(induction pss arbitrary: m rule: l4_ports_compress.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. l4_ports_compress [] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [])) a p
 2. \<And>proto ps m. l4_ports_compress [L4Ports proto ps] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto ps])) a p
 3. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto ps m. l4_ports_compress [L4Ports proto ps] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto ps])) a p
 2. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l4_ports_compress [L4Ports proto_ ps_] = MatchExpr m_ \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m_)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) [L4Ports proto_ ps_])) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_))) = m_ \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m_)) a p = matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto_ ps_))) a p
[PROOF STEP]
apply(drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ = L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_))) \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_)))))) a p = matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto_ ps_))) a p
[PROOF STEP]
by(simp add: primitive_matcher_generic.Ports_single[OF generic] wordinterval_compress l2wi_wi2l ports_to_set_wordinterval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(case_tac m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m; m = L4Ports x1 x2\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Src_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports x1 x2))) a p = (matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2)))))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2)))))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p) = (matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto2 ps1))) a p \<and> matches (\<beta>, \<alpha>) (Match (Src_Ports (L4Ports proto2 ps2))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p)
[PROOF STEP]
apply(simp add: primitive_matcher_generic.Ports_single[OF generic])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; (x1 = p_proto p \<and> p_sport p \<in> ports_to_set x2) = (proto2 = p_proto p \<and> p_sport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (proto2 = p_proto p \<and> p_sport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p) = (proto2 = p_proto p \<and> p_sport p \<in> ports_to_set ps1 \<and> proto2 = p_proto p \<and> p_sport p \<in> ports_to_set ps2 \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p)
[PROOF STEP]
apply(simp add: l2wi_wi2l ports_to_set_wordinterval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; (x1 = p_proto p \<and> p_sport p \<in> wordinterval_to_set (l2wi x2)) = (proto2 = p_proto p \<and> p_sport p \<in> wordinterval_to_set (l2wi ps1) \<and> p_sport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (proto2 = p_proto p \<and> p_sport p \<in> wordinterval_to_set (l2wi ps1) \<and> p_sport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p) = (proto2 = p_proto p \<and> p_sport p \<in> wordinterval_to_set (l2wi ps1) \<and> proto2 = p_proto p \<and> p_sport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Src_Ports) pss)) a p)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma raw_ports_compress_dst_MatchExpr:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  and c: "l4_ports_compress pss = MatchExpr m"
  shows "matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
l4_ports_compress pss = MatchExpr m

goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p
[PROOF STEP]
apply(induction pss arbitrary: m rule: l4_ports_compress.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m. l4_ports_compress [] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [])) a p
 2. \<And>proto ps m. l4_ports_compress [L4Ports proto ps] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto ps])) a p
 3. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>proto ps m. l4_ports_compress [L4Ports proto ps] = MatchExpr m \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto ps])) a p
 2. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l4_ports_compress [L4Ports proto_ ps_] = MatchExpr m_ \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m_)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) [L4Ports proto_ ps_])) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_))) = m_ \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m_)) a p = matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto_ ps_))) a p
[PROOF STEP]
apply(drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ = L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_))) \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto_ (wi2l (wordinterval_compress (l2wi ps_)))))) a p = matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto_ ps_))) a p
[PROOF STEP]
by(simp add: primitive_matcher_generic.Ports_single[OF generic] wordinterval_compress l2wi_wi2l ports_to_set_wordinterval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(case_tac m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>\<And>m. \<lbrakk>\<not> proto1 \<noteq> proto2; l4_ports_compress (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr m\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss))) a p; l4_ports_compress (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss) = MatchExpr m; m = L4Ports x1 x2\<rbrakk> \<Longrightarrow> matches (\<beta>, \<alpha>) (Match (Dst_Ports m)) a p = matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) (L4Ports proto1 ps1 # L4Ports proto2 ps2 # pss))) a p
[PROOF STEP]
apply(simp add: bunch_of_lemmata_about_matches split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports x1 x2))) a p = (matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2)))))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2)))))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p) = (matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto2 ps1))) a p \<and> matches (\<beta>, \<alpha>) (Match (Dst_Ports (L4Ports proto2 ps2))) a p \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p)
[PROOF STEP]
apply(simp add: primitive_matcher_generic.Ports_single[OF generic])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; (x1 = p_proto p \<and> p_dport p \<in> ports_to_set x2) = (proto2 = p_proto p \<and> p_dport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (proto2 = p_proto p \<and> p_dport p \<in> ports_to_set (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p) = (proto2 = p_proto p \<and> p_dport p \<in> ports_to_set ps1 \<and> proto2 = p_proto p \<and> p_dport p \<in> ports_to_set ps2 \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p)
[PROOF STEP]
apply(simp add: l2wi_wi2l ports_to_set_wordinterval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto1 ps1 proto2 ps2 pss m x1 x2. \<lbrakk>m = L4Ports x1 x2; (x1 = p_proto p \<and> p_dport p \<in> wordinterval_to_set (l2wi x2)) = (proto2 = p_proto p \<and> p_dport p \<in> wordinterval_to_set (l2wi ps1) \<and> p_dport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p); proto1 = proto2; l4_ports_compress (L4Ports proto2 (wi2l (wordinterval_intersection (l2wi ps1) (l2wi ps2))) # pss) = MatchExpr (L4Ports x1 x2)\<rbrakk> \<Longrightarrow> (proto2 = p_proto p \<and> p_dport p \<in> wordinterval_to_set (l2wi ps1) \<and> p_dport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p) = (proto2 = p_proto p \<and> p_dport p \<in> wordinterval_to_set (l2wi ps1) \<and> proto2 = p_proto p \<and> p_dport p \<in> wordinterval_to_set (l2wi ps2) \<and> matches (\<beta>, \<alpha>) (alist_and (map (Pos \<circ> Dst_Ports) pss)) a p)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma l4_ports_negate_one:
  fixes p :: "('i::len, 'a) tagged_packet_scheme"
  assumes generic: "primitive_matcher_generic \<beta>"
  shows "matches (\<beta>, \<alpha>) (l4_ports_negate_one Src_Ports ports) a p \<longleftrightarrow>
          matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports ports))) a p"
  and "matches (\<beta>, \<alpha>) (l4_ports_negate_one Dst_Ports ports) a p \<longleftrightarrow>
          matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports ports))) a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (l4_ports_negate_one Src_Ports ports) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports ports))) a p &&& matches (\<beta>, \<alpha>) (l4_ports_negate_one Dst_Ports ports) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports ports))) a p
[PROOF STEP]
apply(case_tac [!] ports)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (l4_ports_negate_one Src_Ports ports) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Src_Ports ports))) a p
 2. \<And>x1 x2. ports = L4Ports x1 x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (l4_ports_negate_one Dst_Ports ports) a p = matches (\<beta>, \<alpha>) (MatchNot (Match (Dst_Ports ports))) a p
[PROOF STEP]
by(auto simp add: primitive_matcher_generic.Ports_single_not[OF generic]
                    MatchOr bunch_of_lemmata_about_matches
                    primitive_matcher_generic.Prot_single_not[OF generic]
                    primitive_matcher_generic.Ports_single[OF generic]
                    raw_ports_invert)


[STATEMENT]
lemma l4_ports_negate_one_nodisc:
    "\<forall>a. \<not> disc (C a) \<Longrightarrow> \<forall>a. \<not> disc (Prot a) \<Longrightarrow> \<not> has_disc disc (l4_ports_negate_one C pt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); \<forall>a. \<not> disc (Prot a)\<rbrakk> \<Longrightarrow> \<not> has_disc disc (l4_ports_negate_one C pt)
[PROOF STEP]
apply(cases pt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<forall>a. \<not> disc (C a); \<forall>a. \<not> disc (Prot a); pt = L4Ports x1 x2\<rbrakk> \<Longrightarrow> \<not> has_disc disc (l4_ports_negate_one C pt)
[PROOF STEP]
by(simp add: MatchOr_def)


[STATEMENT]
lemma l4_ports_negate_one_not_has_disc_negated_generic:
    assumes noProt: "\<forall>a. \<not> disc (Prot a)"
    shows "\<not> has_disc_negated disc False (l4_ports_negate_one C ports)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc False (l4_ports_negate_one C ports)
[PROOF STEP]
apply(cases ports, rename_tac proto pts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>proto pts. ports = L4Ports proto pts \<Longrightarrow> \<not> has_disc_negated disc False (l4_ports_negate_one C ports)
[PROOF STEP]
by(simp add: MatchOr_def noProt)


[STATEMENT]
lemma l4_ports_negate_one_not_has_disc_negated:
    "\<not> has_disc_negated is_Src_Ports False (l4_ports_negate_one Src_Ports ports)"
    "\<not> has_disc_negated is_Dst_Ports False (l4_ports_negate_one Dst_Ports ports)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated is_Src_Ports False (l4_ports_negate_one Src_Ports ports) &&& \<not> has_disc_negated is_Dst_Ports False (l4_ports_negate_one Dst_Ports ports)
[PROOF STEP]
by(simp add: l4_ports_negate_one_not_has_disc_negated_generic)+


[STATEMENT]
lemma negated_normalized_folded_ports_nodisc:
    "\<forall>a. \<not> disc (C a) \<Longrightarrow> (\<forall>a. \<not> disc (Prot a)) \<or> pts = [] \<Longrightarrow>
     m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))) \<Longrightarrow>
      \<not> has_disc disc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply(subgoal_tac "\<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply(rule andfold_MatchExp_not_discI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map (l4_ports_negate_one C) pts). \<not> has_disc disc m
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply(elim disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<forall>a. \<not> disc (Prot a)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 2. \<lbrakk>\<forall>a. \<not> disc (C a); m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); pts = []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 3. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
using l4_ports_negate_one_nodisc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>a. \<not> ?disc (?C a); \<forall>a. \<not> ?disc (Prot a)\<rbrakk> \<Longrightarrow> \<not> has_disc ?disc (l4_ports_negate_one ?C ?pt)

goal (3 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<forall>a. \<not> disc (Prot a)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 2. \<lbrakk>\<forall>a. \<not> disc (C a); m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); pts = []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 3. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); pts = []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set pts. \<not> has_disc disc (l4_ports_negate_one C m)
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
apply(simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
using normalize_match_preserves_nodisc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> has_disc ?disc ?m; ?m' \<in> set (normalize_match ?m)\<rbrakk> \<Longrightarrow> \<not> has_disc ?disc ?m'

goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; m \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))); \<not> has_disc disc (andfold_MatchExp (map (l4_ports_negate_one C) pts))\<rbrakk> \<Longrightarrow> \<not> has_disc disc m
[PROOF STEP]
by blast


[STATEMENT]
lemma negated_normalized_folded_ports_normalized_n_primitive:
    "\<forall>a. \<not> disc (C a) \<Longrightarrow> (\<forall>a. \<not> disc (Prot a)) \<or> pts = [] \<Longrightarrow>
     x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts))) \<Longrightarrow>
      normalized_n_primitive (disc, sel) f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc, sel) f x
[PROOF STEP]
apply(rule normalized_n_primitive_if_no_primitive)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> normalized_nnf_match x
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc x
[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. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> normalized_nnf_match x
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<not> has_disc disc x
[PROOF STEP]
apply(rule negated_normalized_folded_ports_nodisc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> \<forall>a. \<not> disc (?C28 a)
 2. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> (\<forall>a. \<not> disc (Prot a)) \<or> ?pts28 = []
 3. \<lbrakk>\<forall>a. \<not> disc (C a); (\<forall>a. \<not> disc (Prot a)) \<or> pts = []; x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one C) pts)))\<rbrakk> \<Longrightarrow> x \<in> set (normalize_match (andfold_MatchExp (map (l4_ports_negate_one ?C28) ?pts28)))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma "\<not> normalized_nnf_match (l4_ports_negate_one C ports)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> normalized_nnf_match (l4_ports_negate_one C ports)
[PROOF STEP]
by(cases ports) (simp add: MatchOr_def)


[STATEMENT]
lemma "\<forall>a. \<not> disc (C a) \<Longrightarrow> \<not> normalized_n_primitive (disc, sel) f (l4_ports_negate_one C a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. \<not> disc (C a) \<Longrightarrow> \<not> normalized_n_primitive (disc, sel) f (l4_ports_negate_one C a)
[PROOF STEP]
by(cases a)(simp add: MatchOr_def)


[STATEMENT]
lemma "((normalize_match (l4_ports_negate_one Src_Ports (L4Ports TCP [(22,22),(80,90)]))):: 32 common_primitive match_expr list)
    =
    [ MatchNot (Match (Prot (Proto TCP)))
    , Match (Src_Ports (L4Ports 6 [(0, 21), (23, 79), (91, 0xFFFF)]))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize_match (l4_ports_negate_one Src_Ports (L4Ports TCP [(22, 22), (80, 90)])) = [MatchNot (Match (Prot (Proto TCP))), Match (Src_Ports (L4Ports 6 [(0, 21), (23, 79), (91, 65535)]))]
[PROOF STEP]
by eval


[STATEMENT]
lemma rewrite_negated_primitives_unchanged_if_not_has_disc_negated:
  assumes n: "normalized_nnf_match m"
  and wf_disc_sel: "wf_disc_sel (disc,sel) C"
  and noDisc: "\<not> has_disc_negated disc False m"
  shows "rewrite_negated_primitives (disc,sel) C negate_f m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rewrite_negated_primitives (disc, sel) C negate_f m = m
[PROOF STEP]
apply(simp add: rewrite_negated_primitives_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) 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 (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) 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> getNeg spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst) = m
[PROOF STEP]
apply(frule primitive_extractor_correct(8)[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_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> getNeg spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst) = m
[PROOF STEP]
using noDisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc False m

goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); (\<not> has_disc_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> getNeg spts \<noteq> [] \<longrightarrow> MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst) = m
[PROOF STEP]
by blast


[STATEMENT]
lemma rewrite_negated_primitives_normalized_no_modification:
    assumes wf_disc_sel: "wf_disc_sel (disc, sel) C"
    and disc_p: "\<not> has_disc_negated disc False m"
    and n: "normalized_nnf_match m"
    and a: "a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))"
    shows "a = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = m
[PROOF STEP]
from rewrite_negated_primitives_unchanged_if_not_has_disc_negated[OF n wf_disc_sel disc_p]
[PROOF STATE]
proof (chain)
picking this:
rewrite_negated_primitives (disc, sel) C ?negate_f m = m
[PROOF STEP]
have m: "rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m = m"
[PROOF STATE]
proof (prove)
using this:
rewrite_negated_primitives (disc, sel) C ?negate_f m = m

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

goal (1 subgoal):
 1. a = m
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> set (normalize_match (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m))

goal (1 subgoal):
 1. a = m
[PROOF STEP]
apply(subst(asm) m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set (normalize_match m) \<Longrightarrow> a = m
[PROOF STEP]
using normalize_match_already_normalized[OF n]
[PROOF STATE]
proof (prove)
using this:
normalize_match m = [m]

goal (1 subgoal):
 1. a \<in> set (normalize_match m) \<Longrightarrow> a = m
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a = m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rewrite_negated_primitives_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 noNeg: "\<not> has_disc_negated disc False m"
  and disc2_noC: "\<forall>a. \<not> disc2 (C a)"
  shows "\<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C l4_ports_negate_one m)
[PROOF STEP]
apply(subst rewrite_negated_primitives_unchanged_if_not_has_disc_negated)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (disc, sel) C
 3. \<not> has_disc_negated disc False m
 4. \<not> has_disc disc2 m
[PROOF STEP]
using n wf_disc_sel noNeg nodisc
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match m
wf_disc_sel (disc, sel) C
\<not> has_disc_negated disc False m
\<not> has_disc disc2 m

goal (4 subgoals):
 1. normalized_nnf_match m
 2. wf_disc_sel (disc, sel) C
 3. \<not> has_disc_negated disc False m
 4. \<not> has_disc disc2 m
[PROOF STEP]
by(simp)+


[STATEMENT]
lemma rewrite_negated_primitives:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel disc_sel C"
  and negate_f: "\<forall>pts. matches \<gamma> (negate_f C pts) a p \<longleftrightarrow> matches \<gamma> (MatchNot (Match (C pts))) a p"
  shows "matches \<gamma> (rewrite_negated_primitives disc_sel C negate_f m) a p \<longleftrightarrow> matches \<gamma> m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches \<gamma> (rewrite_negated_primitives disc_sel C negate_f m) a p = matches \<gamma> m a p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matches \<gamma> (rewrite_negated_primitives disc_sel C negate_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> (rewrite_negated_primitives disc_sel C negate_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> (rewrite_negated_primitives disc_sel C negate_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> (rewrite_negated_primitives disc_sel C negate_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> (rewrite_negated_primitives disc_sel C negate_f m) a p = matches \<gamma> m a p
[PROOF STEP]
have "matches \<gamma> (andfold_MatchExp (map (negate_f C) (getNeg spts))) a p \<and>
          matches \<gamma> (andfold_MatchExp (map (Match \<circ> C) (getPos 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 (negate_f C) (getNeg spts))) a p \<and> matches \<gamma> (andfold_MatchExp (map (Match \<circ> C) (getPos 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 (negate_f C) (getNeg spts))) a p \<and> matches \<gamma> (andfold_MatchExp (map (Match \<circ> C) (getPos 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 (getNeg spts). matches \<gamma> (negate_f C m) a p) \<and> (\<forall>m\<in>set (getPos spts). matches \<gamma> (Match (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]
apply(simp add: negate_f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>m\<in>set (getNeg spts). matches \<gamma> (MatchNot (Match (C m))) a p) \<and> (\<forall>m\<in>set (getPos spts). matches \<gamma> (Match (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_NegPos_map_getNeg_getPos_matches
[PROOF STATE]
proof (prove)
using this:
((\<forall>m\<in>set (getNeg ?spts). matches ?\<gamma> (MatchNot (Match (?C m))) ?a ?p) \<and> (\<forall>m\<in>set (getPos ?spts). matches ?\<gamma> (Match (?C m)) ?a ?p)) = matches ?\<gamma> (alist_and (NegPos_map ?C ?spts)) ?a ?p

goal (1 subgoal):
 1. ((\<forall>m\<in>set (getNeg spts). matches \<gamma> (MatchNot (Match (C m))) a p) \<and> (\<forall>m\<in>set (getPos spts). matches \<gamma> (Match (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 (negate_f C) (getNeg spts))) a p \<and> matches \<gamma> (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) a p \<and> matches \<gamma> rst a p) = matches \<gamma> m a p

goal (1 subgoal):
 1. matches \<gamma> (rewrite_negated_primitives disc_sel C negate_f m) a p = matches \<gamma> m a p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(matches \<gamma> (andfold_MatchExp (map (negate_f C) (getNeg spts))) a p \<and> matches \<gamma> (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) a p \<and> matches \<gamma> rst a p) = matches \<gamma> m a p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rewrite_negated_primitives_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"
  (*only need a condition for negate_f if it is actually applied*)
  and negate_f: "has_disc_negated disc False m \<Longrightarrow> \<forall>pts. \<not> has_disc disc2 (negate_f C pts)"
  and no_disc: "\<forall>a. \<not> disc2 (C a)"
  shows  "\<not> has_disc disc2 (rewrite_negated_primitives (disc,sel) C negate_f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc2 (rewrite_negated_primitives (disc, sel) C negate_f m)
[PROOF STEP]
apply(simp add: rewrite_negated_primitives_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc disc2 (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) 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 (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos 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> (getNeg spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(frule primitive_extractor_correct(8)[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; (\<not> has_disc_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc disc2 m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc disc2 rst)
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (4 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_negated disc False m) = (getNeg spts = []); getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 4. \<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_negated disc False m) = (getNeg spts = []); getNeg 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 (4 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_negated disc False m) = (getNeg spts = []); getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 4. \<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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(simp; fail)
[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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (negate_f C) (getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(rule andfold_MatchExp_not_discI)
[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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map (negate_f C) (getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply(simp add: negate_f; 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
using andfold_MatchExp_not_disc_mapMatch no_disc
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> ?disc (?C a) \<Longrightarrow> \<not> has_disc ?disc (andfold_MatchExp (map (Match \<circ> ?C) ?ls))
\<forall>a. \<not> disc2 (C a)

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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map (Match \<circ> C) (getPos 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
apply 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> has_disc_negated disc False m) = (getNeg spts = []); getNeg 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; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 rst
[PROOF STEP]
by blast


[STATEMENT]
lemma rewrite_negated_primitives_not_has_disc_negated:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
  and negate_f: "has_disc_negated disc False m \<Longrightarrow> \<forall>pts. \<not> has_disc_negated disc False (negate_f C pts)"
  shows  "\<not> has_disc_negated disc False (rewrite_negated_primitives (disc,sel) C negate_f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc False (rewrite_negated_primitives (disc, sel) C negate_f m)
[PROOF STEP]
apply(simp add: rewrite_negated_primitives_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc False (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) 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_negated disc False (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc False 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> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc False rst)
[PROOF STEP]
apply(frule primitive_extractor_correct(8)[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_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc False rst)
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts = []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (negate_f C) (getNeg spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 4. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (negate_f C) (getNeg spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
apply(rule andfold_MatchExp_not_disc_negatedI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map (negate_f C) (getNeg spts)). \<not> has_disc_negated disc False m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
apply(simp add: negate_f; fail)
[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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
using andfold_MatchExp_not_disc_negated_mapMatch
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated ?disc False (andfold_MatchExp (map (Match \<circ> ?C) ?ls))

goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
apply blast
[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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc False rst
[PROOF STEP]
using has_disc_negated_has_disc
[PROOF STATE]
proof (prove)
using this:
has_disc_negated ?disc ?neg ?m \<Longrightarrow> has_disc ?disc ?m

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


[STATEMENT]
lemma rewrite_negated_primitives_preserves_not_has_disc_negated:
  assumes n: "normalized_nnf_match m" and wf_disc_sel: "wf_disc_sel (disc,sel) C"
  and negate_f: "has_disc_negated disc False m \<Longrightarrow> \<forall>pts. \<not> has_disc_negated disc2 False (negate_f C pts)"
  and no_disc: "\<not> has_disc_negated disc2 False m"
  shows  "\<not> has_disc_negated disc2 False (rewrite_negated_primitives (disc,sel) C negate_f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc2 False (rewrite_negated_primitives (disc, sel) C negate_f m)
[PROOF STEP]
apply(simp add: rewrite_negated_primitives_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_disc_negated disc2 False (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) 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_negated disc2 False (case primitive_extractor (disc, sel) m of (spts, rst) \<Rightarrow> if getNeg spts = [] then m else MatchAnd (andfold_MatchExp (map (negate_f C) (getNeg spts))) (MatchAnd (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) rst))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. primitive_extractor (disc, sel) m = (spts, rst) \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc2 False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc2 False 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> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc2 False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc2 False rst)
[PROOF STEP]
apply(frule primitive_extractor_correct(8)[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_negated disc False m) = (getNeg spts = [])\<rbrakk> \<Longrightarrow> (getNeg spts = [] \<longrightarrow> \<not> has_disc_negated disc2 False m) \<and> (getNeg spts \<noteq> [] \<longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts))) \<and> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts))) \<and> \<not> has_disc_negated disc2 False rst)
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts = []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 4. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
using no_disc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc2 False m

goal (4 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts = []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 4. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (negate_f C) (getNeg spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply(rule andfold_MatchExp_not_disc_negatedI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>m\<in>set (map (negate_f C) (getNeg spts)). \<not> has_disc_negated disc2 False m
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 3. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply(simp add: negate_f; fail)
[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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
using andfold_MatchExp_not_disc_negated_mapMatch
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated ?disc False (andfold_MatchExp (map (Match \<circ> ?C) ?ls))

goal (2 subgoals):
 1. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False (andfold_MatchExp (map (Match \<circ> C) (getPos spts)))
 2. \<And>spts rst. \<lbrakk>primitive_extractor (disc, sel) m = (spts, rst); \<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply blast
[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_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
apply(drule primitive_extractor_correct(6)[OF n wf_disc_sel, where neg=False])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>spts rst. \<lbrakk>\<not> has_disc disc rst; (\<not> has_disc_negated disc False m) = (getNeg spts = []); getNeg spts \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 False m \<longrightarrow> \<not> has_disc_negated disc2 False rst\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 False rst
[PROOF STEP]
using no_disc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc2 False m

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