Theory Primitive_Normalization

theory Primitive_Normalization
imports Negation_Type_Matching
begin

section‹Primitive Normalization›

subsection‹Normalized Primitives›

text‹
  Test if a ‹disc› is in the match expression.
  For example, it call tell whether there are some matches for ‹Src ip›.
›
fun has_disc :: "('a ⇒ bool) ⇒ 'a match_expr ⇒ bool" where
  "has_disc _ MatchAny = False" |
  "has_disc disc (Match a) = disc a" |
  "has_disc disc (MatchNot m) = has_disc disc m" |
  "has_disc disc (MatchAnd m1 m2) = (has_disc disc m1 ∨ has_disc disc m2)"

fun has_disc_negated :: "('a ⇒ bool) ⇒ bool ⇒ 'a match_expr ⇒ bool" where
  "has_disc_negated _    _   MatchAny = False" |
  "has_disc_negated disc neg (Match a) = (if disc a then neg else False)" |
  "has_disc_negated disc neg (MatchNot m) = has_disc_negated disc (¬ neg) m" |
  "has_disc_negated disc neg (MatchAnd m1 m2) = (has_disc_negated disc neg m1 ∨ has_disc_negated disc neg m2)"

lemma "¬ has_disc_negated (λx::nat. x = 0) False (MatchAnd (Match 0) (MatchNot (Match 1)))" by eval
lemma "has_disc_negated (λx::nat. x = 0) False (MatchAnd (Match 0) (MatchNot (Match 0)))" by eval
lemma "has_disc_negated (λx::nat. x = 0) True (MatchAnd (Match 0) (MatchNot (Match 1)))" by eval
lemma "¬ has_disc_negated (λx::nat. x = 0) True (MatchAnd (Match 1) (MatchNot (Match 0)))" by eval
lemma "has_disc_negated (λx::nat. x = 0) True (MatchAnd (Match 0) (MatchNot (Match 0)))" by eval

― ‹We want false on the right hand side, because this is how the algorithm should be started›
lemma has_disc_negated_MatchNot:
  "has_disc_negated disc True (MatchNot m) ⟷ has_disc_negated disc False m"
  "has_disc_negated disc True m ⟷ has_disc_negated disc False (MatchNot m)"
  by(induction m) (simp_all)

lemma has_disc_negated_has_disc: "has_disc_negated disc neg m ⟹ has_disc disc m"
  apply(induction m arbitrary: neg)
     apply(simp_all split: if_split_asm)
  by blast

lemma has_disc_negated_positiv_has_disc: "has_disc_negated disc neg m ∨ has_disc_negated disc (¬ neg) m ⟷ has_disc disc m"
by(induction disc neg m arbitrary: neg rule:has_disc_negated.induct) auto


lemma has_disc_negated_disj_split: 
    "has_disc_negated (λa. P a ∨ Q a) neg m ⟷ has_disc_negated P neg m ∨ has_disc_negated Q neg m"
  apply(induction "(λa. P a ∨ Q a)" neg m rule: has_disc_negated.induct)
     apply(simp_all)
  by blast

lemma has_disc_alist_and: "has_disc disc (alist_and as) ⟷ (∃ a ∈ set as. has_disc disc (negation_type_to_match_expr a))"
  proof(induction as rule: alist_and.induct)
  qed(simp_all add: negation_type_to_match_expr_simps)
lemma has_disc_negated_alist_and: "has_disc_negated disc neg (alist_and as) ⟷ (∃ a ∈ set as. has_disc_negated disc neg (negation_type_to_match_expr a))"
  proof(induction as rule: alist_and.induct)
  qed(simp_all add: negation_type_to_match_expr_simps)
  

lemma has_disc_alist_and': "has_disc disc (alist_and' as) ⟷ (∃ a ∈ set as. has_disc disc (negation_type_to_match_expr a))"
  proof(induction as rule: alist_and'.induct)
  qed(simp_all add: negation_type_to_match_expr_simps)
lemma has_disc_negated_alist_and': "has_disc_negated disc neg (alist_and' as) ⟷ (∃ a ∈ set as. has_disc_negated disc neg (negation_type_to_match_expr a))"
  proof(induction as rule: alist_and'.induct)
  qed(simp_all add: negation_type_to_match_expr_simps)


lemma has_disc_alist_and'_append:
  "has_disc disc' (alist_and' (ls1 @ ls2)) ⟷
      has_disc disc' (alist_and' ls1) ∨ has_disc disc' (alist_and' ls2)"
apply(induction ls1 arbitrary: ls2 rule: alist_and'.induct)
    apply(simp_all)
 apply(case_tac [!] ls2)
   apply(simp_all)
done
lemma has_disc_negated_alist_and'_append:
  "has_disc_negated disc' neg (alist_and' (ls1 @ ls2)) ⟷
      has_disc_negated disc' neg (alist_and' ls1) ∨ has_disc_negated disc' neg (alist_and' ls2)"
apply(induction ls1 arbitrary: ls2 rule: alist_and'.induct)
    apply(simp_all)
 apply(case_tac [!] ls2)
   apply(simp_all)
done

lemma match_list_to_match_expr_not_has_disc: 
    "∀a. ¬ disc (X a) ⟹ ¬ has_disc disc (match_list_to_match_expr (map (Match ∘ X) ls))"
  apply(induction ls)
   apply(simp; fail)
  by(simp add: MatchOr_def)


lemma "matches ((λx _. bool_to_ternary (disc x)), (λ_ _. False)) (Match x) a p ⟷ has_disc disc (Match x)"
by(simp add: match_raw_ternary bool_to_ternary_simps split: ternaryvalue.split )


fun normalized_n_primitive :: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒ ('b ⇒ bool) ⇒ 'a match_expr ⇒ bool" where
  "normalized_n_primitive _ _ MatchAny = True" |
  "normalized_n_primitive (disc, sel) n (Match P) = (if disc P then n (sel P) else True)" |
  "normalized_n_primitive (disc, sel) n (MatchNot (Match P)) = (if disc P then False else True)" |
  "normalized_n_primitive (disc, sel) n (MatchAnd m1 m2) = (normalized_n_primitive (disc, sel) n m1 ∧ normalized_n_primitive (disc, sel) n m2)" |
  "normalized_n_primitive _ _ (MatchNot (MatchAnd _ _)) = False" |
  (*"normalized_n_primitive _ _ (MatchNot _) = True" *)
  "normalized_n_primitive _ _ (MatchNot (MatchNot _)) = False" | (*not nnf normalized*)
  "normalized_n_primitive _ _ (MatchNot MatchAny) = True"


lemma normalized_nnf_match_opt_MatchAny_match_expr:
  "normalized_nnf_match m ⟹ normalized_nnf_match (opt_MatchAny_match_expr m)"
  proof-
  have "normalized_nnf_match m ⟹ normalized_nnf_match (opt_MatchAny_match_expr_once m)"
  for m :: "'a match_expr"
  by(induction m rule: opt_MatchAny_match_expr_once.induct) (simp_all)
  thus "normalized_nnf_match m ⟹ normalized_nnf_match (opt_MatchAny_match_expr m)"
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(induction rule: repeat_stabilize_induct)
     by(simp)+
  qed

lemma normalized_n_primitive_opt_MatchAny_match_expr:
  "normalized_n_primitive disc_sel f m ⟹ normalized_n_primitive disc_sel f (opt_MatchAny_match_expr m)"
  proof-

  have "normalized_n_primitive disc_sel f m ⟹ normalized_n_primitive disc_sel f (opt_MatchAny_match_expr_once m)"
  for m
    proof-
    { fix disc::"('a ⇒ bool)" and sel::"('a ⇒ 'b)" and n m1 m2
      have "normalized_n_primitive (disc, sel) n (opt_MatchAny_match_expr_once m1) ⟹
           normalized_n_primitive (disc, sel) n (opt_MatchAny_match_expr_once m2) ⟹
           normalized_n_primitive (disc, sel) n m1 ∧ normalized_n_primitive (disc, sel) n m2 ⟹
           normalized_n_primitive (disc, sel) n (opt_MatchAny_match_expr_once (MatchAnd m1 m2))"
    by(induction "(MatchAnd m1 m2)" rule: opt_MatchAny_match_expr_once.induct) (auto)
    }note x=this
    assume "normalized_n_primitive disc_sel f m"
    thus ?thesis
      apply(induction disc_sel f m rule: normalized_n_primitive.induct)
            apply simp_all
      using x by simp
    qed
  from this show
    "normalized_n_primitive disc_sel f m ⟹ normalized_n_primitive disc_sel f (opt_MatchAny_match_expr m)"
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(induction rule: repeat_stabilize_induct)
     by(simp)+ 
  qed


lemma normalized_n_primitive_imp_not_disc_negated:
  "wf_disc_sel (disc,sel) C ⟹ normalized_n_primitive (disc,sel) f m ⟹ ¬ has_disc_negated disc False m"
  apply(induction "(disc,sel)" f m rule: normalized_n_primitive.induct)
  by(simp add: wf_disc_sel.simps split: if_split_asm)+

lemma normalized_n_primitive_alist_and: "normalized_n_primitive disc_sel P (alist_and as) ⟷
      (∀ a ∈ set as. normalized_n_primitive disc_sel P (negation_type_to_match_expr a))"
  proof(induction as)
  case Nil thus ?case by simp
  next
  case (Cons a as) thus ?case
    apply(cases disc_sel, cases a)
    by(simp_all add: negation_type_to_match_expr_simps)
  qed

lemma normalized_n_primitive_alist_and': "normalized_n_primitive disc_sel P (alist_and' as) ⟷
      (∀ a ∈ set as. normalized_n_primitive disc_sel P (negation_type_to_match_expr a))"
  apply(cases disc_sel)
  apply(induction as rule: alist_and'.induct)
      by(simp_all add: negation_type_to_match_expr_simps)

lemma not_has_disc_NegPos_map: "∀a. ¬ disc (C a) ⟹ ∀a∈set (NegPos_map C ls).
        ¬ has_disc disc (negation_type_to_match_expr a)"
by(induction C ls rule: NegPos_map.induct) (simp add: negation_type_to_match_expr_def)+

lemma not_has_disc_negated_NegPos_map: "∀a. ¬ disc (C a) ⟹ ∀a∈set (NegPos_map C ls).
        ¬ has_disc_negated disc False (negation_type_to_match_expr a)"
by(induction C ls rule: NegPos_map.induct) (simp add: negation_type_to_match_expr_def)+

lemma normalized_n_primitive_impossible_map: "∀a. ¬ disc (C a) ⟹
  ∀m∈set (map (Match ∘ (C ∘ x)) ls).
     normalized_n_primitive (disc, sel) f m"
  apply(intro ballI)
  apply(induction ls)
   apply(simp; fail)
  apply(simp)
  apply(case_tac m, simp_all) (*3 cases are impossible*)
   apply(fastforce)
  by force

lemma normalized_n_primitive_alist_and'_append:
  "normalized_n_primitive (disc, sel) f (alist_and' (ls1 @ ls2)) ⟷
      normalized_n_primitive (disc, sel) f (alist_and' ls1) ∧ normalized_n_primitive (disc, sel) f (alist_and' ls2)"
apply(induction ls1 arbitrary: ls2 rule: alist_and'.induct)
    apply(simp_all)
 apply(case_tac [!] ls2)
   apply(simp_all)
done

lemma normalized_n_primitive_if_no_primitive: "normalized_nnf_match m ⟹ ¬ has_disc disc m ⟹ 
       normalized_n_primitive (disc, sel) f m"
  by(induction "(disc, sel)" f m rule: normalized_n_primitive.induct) (simp)+

lemma normalized_n_primitive_false_eq_notdisc: "normalized_nnf_match m ⟹
  normalized_n_primitive (disc, sel) (λ_. False) m ⟷ ¬ has_disc disc m"
proof -
  have "normalized_nnf_match m ⟹ false = (λ_. False) ⟹
  ¬ has_disc disc m ⟷ normalized_n_primitive (disc, sel) false m" for false
  by(induction "(disc, sel)" false m rule: normalized_n_primitive.induct)
  (simp)+
  thus "normalized_nnf_match m ⟹ ?thesis" by simp
qed

lemma normalized_n_primitive_MatchAnd_combine_map: "normalized_n_primitive disc_sel f rst ⟹
       ∀m' ∈ (λspt. Match (C spt)) ` set pts. normalized_n_primitive disc_sel f m' ⟹
        m' ∈ (λspt. MatchAnd (Match (C spt)) rst) ` set pts ⟹ normalized_n_primitive disc_sel f m'"
  by(induction disc_sel f m' rule: normalized_n_primitive.induct)
     fastforce+

subsection‹Primitive Extractor›

text‹
  The following function takes a tuple of functions (@{typ "(('a ⇒ bool) × ('a ⇒ 'b))"}) and a @{typ "'a match_expr"}.
  The passed function tuple must be the discriminator and selector of the datatype package.
  ‹primitive_extractor› filters the @{typ "'a match_expr"} and returns a tuple.
  The first element of the returned tuple is the filtered primitive matches, the second element is the remaining match expression.

  It requires a @{const normalized_nnf_match}.
›
fun primitive_extractor :: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒ 'a match_expr ⇒ ('b negation_type list × 'a match_expr)" where
 "primitive_extractor _ MatchAny = ([], MatchAny)" |
 "primitive_extractor (disc,sel) (Match a) = (if disc a then ([Pos (sel a)], MatchAny) else ([], Match a))" |
 "primitive_extractor (disc,sel) (MatchNot (Match a)) = (if disc a then ([Neg (sel a)], MatchAny) else ([], MatchNot (Match a)))" |
 "primitive_extractor C (MatchAnd ms1 ms2) = (
        let (a1', ms1') = primitive_extractor C ms1; 
            (a2', ms2') = primitive_extractor C ms2
        in (a1'@a2', MatchAnd ms1' ms2'))" |
 "primitive_extractor _ _ = undefined"

text‹
  The first part returned by @{const primitive_extractor}, here ‹as›:
    A list of primitive match expressions.
    For example, let ‹m = MatchAnd (Src ip1) (Dst ip2)› then, using the src ‹(disc, sel)›, the result is ‹[ip1]›.
    Note that ‹Src› is stripped from the result.

    The second part, here ‹ms› is the match expression which was not extracted.

    Together, the first and second part match iff ‹m› matches.
›


(*unused*)
lemma primitive_extractor_fst_simp2:
  fixes m'::"'a match_expr ⇒ 'a match_expr ⇒ 'a match_expr"
  shows "fst (case primitive_extractor (disc, sel) m1 of (a1', ms1') ⇒ case primitive_extractor (disc, sel) m2 of (a2', ms2') ⇒ (a1' @ a2', m' ms1' ms2')) =
           fst (primitive_extractor (disc, sel) m1) @ fst (primitive_extractor (disc, sel) m2)"
      apply(cases "primitive_extractor (disc, sel) m1", simp)
      apply(cases "primitive_extractor (disc, sel) m2", simp)
      done

theorem primitive_extractor_correct: assumes 
  "normalized_nnf_match m" and "wf_disc_sel (disc, sel) C" and "primitive_extractor (disc, sel) m = (as, ms)" 
  shows "matches γ (alist_and (NegPos_map C as)) a p ∧ matches γ ms a p ⟷ matches γ m a p"
  and "normalized_nnf_match ms"
  and "¬ has_disc disc ms"
  and "∀disc2. ¬ has_disc disc2 m ⟶ ¬ has_disc disc2 ms"
  and "∀disc2 sel2. normalized_n_primitive (disc2, sel2) P m ⟶ normalized_n_primitive (disc2, sel2) P ms"
  and "∀disc2. ¬ has_disc_negated disc2 neg m ⟶ ¬ has_disc_negated disc2 neg ms"
  and "¬ has_disc disc m ⟷ as = [] ∧ ms = m"
  and "¬ has_disc_negated disc False m ⟷ getNeg as = []"
  and "has_disc disc m ⟹ as ≠ []"
proof -
  ― ‹better simplification rule›
  from assms have assm3': "(as, ms) = primitive_extractor (disc, sel) m" by simp
  with assms(1) assms(2) show "matches γ (alist_and (NegPos_map C as)) a p ∧ matches γ ms a p ⟷ matches γ m a p"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
    case 4 thus ?case
      apply(simp split: if_split_asm prod.split_asm add: NegPos_map_append)
      apply(auto simp add: alist_and_append bunch_of_lemmata_about_matches)
      done
    qed(simp_all add: bunch_of_lemmata_about_matches wf_disc_sel.simps split: if_split_asm)

  from assms(1) assm3' show "normalized_nnf_match ms"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
         case 2 thus ?case by(simp split: if_split_asm)
         next
         case 3 thus ?case by(simp split: if_split_asm)
         next
         case 4 thus ?case 
           apply(clarify) (*if i don't clarify, the simplifier loops*)
           apply(simp split: prod.split_asm)
           done
    qed(simp_all)

  from assms(1) assm3' show "¬ has_disc disc ms"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
    qed(simp_all split: if_split_asm prod.split_asm)


  from assms(1) assm3' show "∀disc2. ¬ has_disc disc2 m ⟶ ¬ has_disc disc2 ms"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
         case 2 thus ?case by(simp split: if_split_asm)
         next
         case 3 thus ?case by(simp split: if_split_asm)
         next
         case 4 thus ?case by(simp split: prod.split_asm)
    qed(simp_all)


  from assms(1) assm3' show "∀disc2. ¬ has_disc_negated disc2 neg m ⟶ ¬ has_disc_negated disc2 neg ms"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
         case 2 thus ?case by(simp split: if_split_asm)
         next
         case 3 thus ?case by(simp split: if_split_asm)
         next
         case 4 thus ?case by(simp split: prod.split_asm)
    qed(simp_all)


  from assms(1) assm3' show "∀disc2 sel2. normalized_n_primitive (disc2, sel2) P m ⟶ normalized_n_primitive (disc2, sel2) P ms"
    apply(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
          apply(simp)
         apply(simp split: if_split_asm)
        apply(simp split: if_split_asm)
       apply(simp split: prod.split_asm)
      apply(simp_all)
    done

   from assms(1) assm3' show "¬ has_disc disc m ⟷ as = [] ∧ ms = m"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
    case 2 thus ?case by(simp split: if_split_asm)
    next
    case 3 thus ?case by(simp split: if_split_asm)
    next
    case 4 thus ?case by(auto split: prod.split_asm)
    qed(simp_all)

   from assms(1) assm3' show "¬ has_disc_negated disc False m ⟷ getNeg as = []"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
    case 2 thus ?case by(simp split: if_split_asm)
    next
    case 3 thus ?case by(simp split: if_split_asm)
    next
    case 4 thus ?case by(simp add: getNeg_append split: prod.split_asm)
    qed(simp_all)

   from assms(1) assm3' show "has_disc disc m ⟹ as ≠ []"
    proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
    case 4 thus ?case apply(simp split: prod.split_asm)
      by metis
    qed(simp_all)
qed


lemma has_disc_negated_primitive_extractor:
  assumes "normalized_nnf_match m"
  shows "has_disc_negated disc False m ⟷ (∃a. Neg a ∈ set (fst (primitive_extractor (disc, sel) m)))"
proof -
  obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
  hence "has_disc_negated disc False m ⟷ (∃a. Neg a ∈ set as)"
    using assms proof(induction m arbitrary: as ms)
    case Match thus ?case
       by(simp split: if_split_asm) fastforce
    next
    case (MatchNot m)
      thus ?case
      proof(induction m)
      case Match thus ?case by (simp, fastforce)
      qed(simp_all)
    next
    case (MatchAnd m1 m2) thus ?case
      apply(cases "primitive_extractor (disc, sel) m1")
      apply(cases "primitive_extractor (disc, sel) m2")
      by auto
  qed(simp_all split: if_split_asm)
  thus ?thesis using asms by simp
qed



(*if i extract something and put it together again unchanged, things do not change*)
lemma primitive_extractor_reassemble_preserves:
  "wf_disc_sel (disc, sel) C ⟹
   normalized_nnf_match m ⟹
   P m ⟹
   P MatchAny ⟹
   primitive_extractor (disc, sel) m = (as, ms) ⟹ ― ‹turn eqality around to simplify proof›
   (⋀m1 m2. P (MatchAnd m1 m2) ⟷ P m1 ∧ P m2) ⟹
   (⋀ls1 ls2. P (alist_and' (ls1 @ ls2)) ⟷ P (alist_and' ls1) ∧ P (alist_and' ls2)) ⟹
   P (alist_and' (NegPos_map C as))"
  proof(induction "(disc, sel)" m  arbitrary: as ms rule: primitive_extractor.induct)
  case 2 thus ?case
    apply(simp split: if_split_asm)
    apply(clarify)
    by(simp add: wf_disc_sel.simps)
  next
  case 3 thus ?case
    apply(simp split: if_split_asm)
    apply(clarify)
    by(simp add: wf_disc_sel.simps)
  next
  case (4 m1 m2 as ms)
    from 4 show ?case
      apply(simp)
      apply(simp split: prod.split_asm)
      apply(clarify)
      apply(simp add: NegPos_map_append)
    done
qed(simp_all split: if_split_asm)

lemma primitive_extractor_reassemble_not_has_disc:
  "wf_disc_sel (disc, sel) C ⟹
   normalized_nnf_match m ⟹ ¬ has_disc disc' m ⟹
   primitive_extractor (disc, sel) m = (as, ms) ⟹
     ¬ has_disc disc' (alist_and' (NegPos_map C as))"
  apply(rule primitive_extractor_reassemble_preserves)
        by(simp_all add: NegPos_map_append has_disc_alist_and'_append)

lemma primitive_extractor_reassemble_not_has_disc_negated:
  "wf_disc_sel (disc, sel) C ⟹
   normalized_nnf_match m ⟹ ¬ has_disc_negated disc' neg m ⟹
   primitive_extractor (disc, sel) m = (as, ms) ⟹ 
     ¬ has_disc_negated disc' neg (alist_and' (NegPos_map C as))"
  apply(rule primitive_extractor_reassemble_preserves)
        by(simp_all add: NegPos_map_append has_disc_negated_alist_and'_append)

lemma primitive_extractor_reassemble_normalized_n_primitive:
  "wf_disc_sel (disc, sel) C ⟹
   normalized_nnf_match m ⟹ normalized_n_primitive (disc1, sel1) f m ⟹
   primitive_extractor (disc, sel) m = (as, ms) ⟹
     normalized_n_primitive (disc1, sel1) f (alist_and' (NegPos_map C as))"
  apply(rule primitive_extractor_reassemble_preserves)
        by(simp_all add: NegPos_map_append normalized_n_primitive_alist_and'_append)



lemma primitive_extractor_matchesE: "wf_disc_sel (disc,sel) C ⟹ normalized_nnf_match m ⟹ primitive_extractor (disc, sel) m = (as, ms)
  ⟹
  (normalized_nnf_match ms ⟹ ¬ has_disc disc ms ⟹ (∀disc2. ¬ has_disc disc2 m ⟶ ¬ has_disc disc2 ms) ⟹ matches_other ⟷  matches γ ms a p)
  ⟹
  matches γ (alist_and (NegPos_map C as)) a p ∧ matches_other ⟷  matches γ m a p"
using primitive_extractor_correct(1,2,3,4) by metis

lemma primitive_extractor_matches_lastE: "wf_disc_sel (disc,sel) C ⟹ normalized_nnf_match m ⟹ primitive_extractor (disc, sel) m = (as, ms)
  ⟹
  (normalized_nnf_match ms ⟹ ¬ has_disc disc ms ⟹ (∀disc2. ¬ has_disc disc2 m ⟶ ¬ has_disc disc2 ms) ⟹ matches γ ms a p)
  ⟹
  matches γ (alist_and (NegPos_map C as)) a p  ⟷  matches γ m a p"
using primitive_extractor_correct(1,2,3,4) by metis

text‹The lemmas @{thm primitive_extractor_matchesE} and @{thm primitive_extractor_matches_lastE} can be used as
  erule to solve goals about consecutive application of @{const primitive_extractor}.
  They should be used as ‹primitive_extractor_matchesE[OF wf_disc_sel_for_first_extracted_thing]›.
›



subsection‹Normalizing and Optimizing Primitives›
  text‹
    Normalize primitives by a function ‹f› with type @{typ "'b negation_type list ⇒ 'b list"}.
    @{typ "'b"} is a primitive type, e.g. ipt-ipv4range.
    ‹f› takes a conjunction list of negated primitives and must compress them such that:
    \begin{enumerate}
      \item no negation occurs in the output
      \item the output is a disjunction of the primitives, i.e. multiple primitives in one rule are compressed to at most one primitive (leading to multiple rules)
    \end{enumerate}
    Example with IP addresses:
    \begin{verbatim}
      f [10.8.0.0/16, 10.0.0.0/8] = [10.0.0.0/8]  f compresses to one range
      f [10.0.0.0, 192.168.0.01] = []    range is empty, rule can be dropped
      f [Neg 41] = [{0..40}, {42..ipv4max}]   one rule is translated into multiple rules to translate negation
      f [Neg 41, {20..50}, {30..50}] = [{30..40}, {42..50}]   input: conjunction list, output disjunction list!
    \end{verbatim}
›
  definition normalize_primitive_extract :: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒
                               ('b ⇒ 'a) ⇒
                               ('b negation_type list ⇒ 'b list) ⇒
                               'a match_expr ⇒ 
                               'a match_expr list" where 
    "normalize_primitive_extract (disc_sel) C f m ≡ (case primitive_extractor (disc_sel) m 
                of (spts, rst) ⇒ map (λspt. (MatchAnd (Match (C spt))) rst) (f spts))"
  
                (*if f spts is empty, we get back an empty list. *)
  
  text‹
    If ‹f› has the properties described above, then @{const normalize_primitive_extract} is a valid transformation of a match expression›
  lemma normalize_primitive_extract: assumes "normalized_nnf_match m" and "wf_disc_sel disc_sel C" and
        "∀ml. (match_list γ (map (Match ∘ C) (f ml)) a p ⟷ matches γ (alist_and (NegPos_map C ml)) a p)"
        shows "match_list γ (normalize_primitive_extract disc_sel C f m) a p ⟷ matches γ m a p"
    proof -
      obtain as ms where pe: "primitive_extractor disc_sel m = (as, ms)" by fastforce

      from pe primitive_extractor_correct(1)[OF assms(1), where γ=γ and  a=a and p=p] assms(2) have 
        "matches γ m a p ⟷ matches γ (alist_and (NegPos_map C as)) a p ∧ matches γ ms a p" by(cases disc_sel, blast)
      also have "… ⟷ match_list γ (map (Match ∘ C) (f as)) a p ∧ matches γ ms a p" using assms(3) by simp
      also have "… ⟷ match_list γ (map (λspt. MatchAnd (Match (C spt)) ms) (f as)) a p"
        by(simp add: match_list_matches bunch_of_lemmata_about_matches)
      also have "... ⟷ match_list γ (normalize_primitive_extract disc_sel C f m) a p"
        by(simp add: normalize_primitive_extract_def pe) 
      finally show ?thesis by simp
    qed

  thm match_list_semantics[of γ "(map (Match ∘ C) (f ml))" a p "[(alist_and (NegPos_map C ml))]"]

  corollary normalize_primitive_extract_semantics:  assumes "normalized_nnf_match m" and "wf_disc_sel disc_sel C" and
        "∀ml. (match_list γ (map (Match ∘ C) (f ml)) a p ⟷ matches γ (alist_and (NegPos_map C ml)) a p)"
        shows "approximating_bigstep_fun γ p (map (λm. Rule m a) (normalize_primitive_extract disc_sel C f m)) s = 
              approximating_bigstep_fun γ p [Rule m a] s"
  proof -
    from normalize_primitive_extract[OF assms(1) assms(2) assms(3)] have
      "match_list γ (normalize_primitive_extract disc_sel C f m) a p = matches γ m a p" .
    also have "… ⟷ match_list γ [m] a p" by simp
    finally show ?thesis using match_list_semantics[of γ "(normalize_primitive_extract disc_sel C f m)" a p "[m]"] by simp
  qed


  lemma normalize_primitive_extract_preserves_nnf_normalized:
  assumes "normalized_nnf_match m"
      and "wf_disc_sel (disc, sel) C"
    shows "∀mn ∈ set (normalize_primitive_extract (disc, sel) C f m). normalized_nnf_match mn"
    proof
      fix mn
      assume assm2: "mn ∈ set (normalize_primitive_extract (disc, sel) C f m)"
      obtain as ms where as_ms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
      from primitive_extractor_correct(2)[OF assms(1) assms(2) as_ms] have "normalized_nnf_match ms" by simp
      from assm2 as_ms have normalize_primitive_extract_unfolded: "mn ∈ ((λspt. MatchAnd (Match (C spt)) ms) ` set (f as))"
        unfolding normalize_primitive_extract_def by force
      with ‹normalized_nnf_match ms› show "normalized_nnf_match mn" by fastforce
    qed

  lemma normalize_rules_primitive_extract_preserves_nnf_normalized:
    "∀r ∈ set rs. normalized_nnf_match (get_match r) ⟹ wf_disc_sel disc_sel C ⟹
     ∀r ∈ set (normalize_rules (normalize_primitive_extract disc_sel C f) rs). normalized_nnf_match (get_match r)"
  apply(rule normalize_rules_preserves[where P="normalized_nnf_match" and f="(normalize_primitive_extract disc_sel C f)"])
   apply(simp; fail)
  apply(cases disc_sel)
  using normalize_primitive_extract_preserves_nnf_normalized by fast

  text‹If something is normalized for disc2 and disc2 ‹≠› disc1 and we do something on disc1, then disc2 remains normalized›
  lemma normalize_primitive_extract_preserves_unrelated_normalized_n_primitive:
  assumes "normalized_nnf_match m"
      and "normalized_n_primitive (disc2, sel2) P m"
      and "wf_disc_sel (disc1, sel1) C"
      and "∀a. ¬ disc2 (C a)" ― ‹disc1 and disc2 match for different stuff. e.g. @{text Src_Ports} and @{text Dst_Ports}›
    shows "∀mn ∈ set (normalize_primitive_extract (disc1, sel1) C f m). normalized_n_primitive (disc2, sel2) P mn"
    proof
      fix mn
      assume assm2: "mn ∈ set (normalize_primitive_extract (disc1, sel1) C f m)"
      obtain as ms where as_ms: "primitive_extractor (disc1, sel1) m = (as, ms)" by fastforce
      from as_ms primitive_extractor_correct[OF assms(1) assms(3)] have 
                      "¬ has_disc disc1 ms"
                  and "normalized_n_primitive (disc2, sel2) P ms"
        apply -
        apply(fast)
        using assms(2) by(fast)
      from assm2 as_ms have normalize_primitive_extract_unfolded: "mn ∈ ((λspt. MatchAnd (Match (C spt)) ms) ` set (f as))"
        unfolding normalize_primitive_extract_def by force
      
      from normalize_primitive_extract_unfolded obtain Casms where Casms: "mn = (MatchAnd (Match (C Casms)) ms)" by blast

      from ‹normalized_n_primitive (disc2, sel2) P ms› assms(4) have "normalized_n_primitive (disc2, sel2) P (MatchAnd (Match (C Casms)) ms)"
        by(simp)

      with Casms show "normalized_n_primitive (disc2, sel2) P mn" by blast
    qed

  
  lemma normalize_primitive_extract_normalizes_n_primitive:
  fixes disc::"('a ⇒ bool)" and sel::"('a ⇒ 'b)" and f::"('b negation_type list ⇒ 'b list)"
  assumes "normalized_nnf_match m"
      and "wf_disc_sel (disc, sel) C"
      and np: "∀as. (∀ a' ∈ set (f as). P a')" (*not quite, sel f   ∀as ∈ {x. disc (v x)}. *)
    shows "∀m' ∈ set (normalize_primitive_extract (disc, sel) C f m). normalized_n_primitive (disc, sel) P m'"
    proof
    fix m' assume a: "m'∈set (normalize_primitive_extract (disc, sel) C f m)"

    have nnf: "∀m' ∈ set (normalize_primitive_extract (disc, sel) C f m). normalized_nnf_match m'"
      using normalize_primitive_extract_preserves_nnf_normalized assms by blast
    with a have normalized_m': "normalized_nnf_match m'" by simp

    from a obtain as ms where as_ms: "primitive_extractor (disc, sel) m = (as, ms)"
      unfolding normalize_primitive_extract_def by fastforce
    with a have prems: "m' ∈ set (map (λspt. MatchAnd (Match (C spt)) ms) (f as))"
      unfolding normalize_primitive_extract_def by simp


    from primitive_extractor_correct(2)[OF assms(1) assms(2) as_ms] have "normalized_nnf_match ms" .
    
    show "normalized_n_primitive (disc, sel) P m'"
    proof(cases "f as = []")
    case True thus "normalized_n_primitive (disc, sel) P m'" using prems by simp
    next
    case False
      with prems obtain spt where "m' = MatchAnd (Match (C spt)) ms" and "spt ∈ set (f as)" by auto

      from primitive_extractor_correct(3)[OF assms(1) assms(2) as_ms] have "¬ has_disc disc ms" .
      with ‹normalized_nnf_match ms› have "normalized_n_primitive (disc, sel) P ms"
        by(induction "(disc, sel)" P ms rule: normalized_n_primitive.induct) simp_all

      from ‹wf_disc_sel (disc, sel) C› have "(sel (C spt)) = spt" by(simp add: wf_disc_sel.simps)
      with np ‹spt ∈ set (f as)› have "P (sel (C spt))" by simp

      show "normalized_n_primitive (disc, sel) P m'"
      apply(simp add: ‹m' = MatchAnd (Match (C spt)) ms›)
      apply(rule conjI)
       apply(simp_all add: ‹normalized_n_primitive (disc, sel) P ms›)
      apply(simp add: ‹P (sel (C spt))›)
      done
    qed
  qed

 lemma primitive_extractor_negation_type_matching1:
    assumes wf: "wf_disc_sel (disc, sel) C"
        and normalized: "normalized_nnf_match m"
        and a1: "primitive_extractor (disc, sel) m = (as, rest)"
        and a2: "matches γ m a p"
    shows "(∀m∈set (map C (getPos as)). matches γ (Match m) a p) ∧ 
           (∀m∈set (map C (getNeg as)). matches γ (MatchNot (Match m)) a p)"
  proof -
      from primitive_extractor_correct(1)[OF normalized wf a1] a2 have
        "matches γ (alist_and (NegPos_map C as)) a p ∧ matches γ rest a p" by fast
      hence "matches γ (alist_and (NegPos_map C as)) a p" by blast
      with Negation_Type_Matching.matches_alist_and have
        "(∀m∈set (getPos (NegPos_map C as)). matches γ (Match m) a p) ∧ 
         (∀m∈set (getNeg (NegPos_map C as)). matches γ (MatchNot (Match m)) a p)" by metis
      with getPos_NegPos_map_simp2 getNeg_NegPos_map_simp2 show ?thesis by metis
  qed


text‹@{const normalized_n_primitive} does NOT imply @{const normalized_nnf_match}›
lemma "∃m. normalized_n_primitive disc_sel f m ⟶ ¬ normalized_nnf_match m"
  by(rule_tac x="MatchNot MatchAny" in exI) (simp)


lemma remove_unknowns_generic_not_has_disc: "¬ has_disc C m ⟹ ¬ has_disc C (remove_unknowns_generic γ a m)"
  by(induction γ a m rule: remove_unknowns_generic.induct) (simp_all add: remove_unknowns_generic_simps2)

lemma remove_unknowns_generic_not_has_disc_negated: "¬ has_disc_negated C neg m ⟹ ¬ has_disc_negated C neg (remove_unknowns_generic γ a m)"
  by(induction γ a m rule: remove_unknowns_generic.induct) (simp_all add: remove_unknowns_generic_simps2)

lemma remove_unknowns_generic_normalized_n_primitive: "normalized_n_primitive disc_sel f m ⟹ 
    normalized_n_primitive disc_sel f (remove_unknowns_generic γ a m)"
  proof(induction γ a m rule: remove_unknowns_generic.induct)
    case 6 thus ?case by(case_tac disc_sel, simp add: remove_unknowns_generic_simps2)
  qed(simp_all add: remove_unknowns_generic_simps2)



lemma normalize_match_preserves_disc_negated: 
    shows "(∃m_DNF ∈ set (normalize_match m). has_disc_negated disc neg m_DNF) ⟹ has_disc_negated disc neg m"
  proof(induction m rule: normalize_match.induct)
  case 3 thus ?case by (simp) blast
  next
  case 4
    from 4 show ?case by(simp) blast
  qed(simp_all)
text‹@{const has_disc_negated} is a structural property and @{const normalize_match} is a semantical property.
  @{const normalize_match} removes subexpressions which cannot match. Thus, we cannot show (without complicated assumptions)
  the opposite direction of @{thm normalize_match_preserves_disc_negated}, because a negated primitive
  might occur in a subexpression which will be optimized away.›


corollary i_m_giving_this_a_funny_name_so_i_can_thank_my_future_me_when_sledgehammer_will_find_this_one_day:
  "¬ has_disc_negated disc neg m ⟹ ∀ m_DNF ∈ set (normalize_match m). ¬ has_disc_negated disc neg m_DNF"
using normalize_match_preserves_disc_negated by blast


lemma not_has_disc_opt_MatchAny_match_expr:
  "¬ has_disc disc m ⟹ ¬ has_disc disc (opt_MatchAny_match_expr m)"
  proof -
    have "¬ has_disc disc m ⟹ ¬ has_disc disc (opt_MatchAny_match_expr_once m)" for m
    by(induction m rule: opt_MatchAny_match_expr_once.induct) simp_all
  thus "¬ has_disc disc m ⟹ ¬ has_disc disc (opt_MatchAny_match_expr m)"
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(rule repeat_stabilize_induct)
     by(simp)+
  qed
lemma not_has_disc_negated_opt_MatchAny_match_expr:
  "¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (opt_MatchAny_match_expr m)"
  proof -
    have "¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (opt_MatchAny_match_expr_once m)"
    for m
    by(induction m arbitrary: neg rule:opt_MatchAny_match_expr_once.induct) (simp_all)
  thus "¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (opt_MatchAny_match_expr m)"
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(rule repeat_stabilize_induct)
     by(simp)+
  qed

lemma normalize_match_preserves_nodisc:
  "¬ has_disc disc m ⟹ m' ∈ set (normalize_match m) ⟹ ¬ has_disc disc m'"
  proof - 
    (*no idea why this statement is necessary*)
    have "¬ has_disc disc m ⟶ (∀m' ∈ set (normalize_match m). ¬ has_disc disc m')"
    by(induction m rule: normalize_match.induct) (safe,auto) ― ‹need safe, otherwise simplifier loops›
  thus "¬ has_disc disc m ⟹ m' ∈ set (normalize_match m) ⟹ ¬ has_disc disc m'" by blast
qed

lemma not_has_disc_normalize_match:
  "¬ has_disc_negated disc neg  m ⟹ m' ∈ set (normalize_match m) ⟹ ¬ has_disc_negated disc neg m'"
  using i_m_giving_this_a_funny_name_so_i_can_thank_my_future_me_when_sledgehammer_will_find_this_one_day by blast

lemma normalize_match_preserves_normalized_n_primitive:
  "normalized_n_primitive disc_sel f rst ⟹
        ∀ m ∈ set (normalize_match rst). normalized_n_primitive disc_sel f m"
apply(cases disc_sel, simp)
apply(induction rst rule: normalize_match.induct)
      apply(simp; fail)
     apply(simp; fail)
    apply(simp; fail)
   using normalized_n_primitive.simps(5) apply metis (*simp loops*)
  by simp+




subsection‹Optimizing a match expression›

  text‹Optimizes a match expression with a function that takes @{typ "'b negation_type list"}
  and returns @{typ "('b list × 'b list) option"}.
  The function should return @{const None} if the match expression cannot match.
  It returns @{term "Some (as_pos, as_neg)"} where @{term as_pos} and @{term as_neg} are lists of
  primitives. Positive and Negated.
  The result is one match expression.

  In contrast @{const normalize_primitive_extract} returns a list of match expression, to be read es their disjunction.›

  definition compress_normalize_primitive :: "(('a ⇒ bool) × ('a ⇒ 'b)) ⇒ ('b ⇒ 'a) ⇒
                                              ('b negation_type list ⇒ ('b list × 'b list) option) ⇒ 
                                              'a match_expr ⇒ 'a match_expr option" where 
    "compress_normalize_primitive disc_sel C f m ≡ (case primitive_extractor disc_sel m of (as, rst) ⇒
      (map_option (λ(as_pos, as_neg). MatchAnd
                                       (alist_and' (NegPos_map C ((map Pos as_pos)@(map Neg as_neg))))
                                       rst
                  ) (f as)))"



  lemma compress_normalize_primitive_nnf: "wf_disc_sel disc_sel C ⟹ 
      normalized_nnf_match m ⟹ compress_normalize_primitive disc_sel C f m = Some m' ⟹
    normalized_nnf_match m'"
    apply(case_tac "primitive_extractor disc_sel m")
    apply(simp add: compress_normalize_primitive_def)
    apply(clarify)
    apply (simp add: normalized_nnf_match_alist_and')
    apply(cases disc_sel, simp)
    using primitive_extractor_correct(2) by blast


  lemma compress_normalize_primitive_not_introduces_C:
    assumes notdisc: "¬ has_disc disc m"
        and wf: "wf_disc_sel (disc,sel) C'" (*C is allowed to be different from C'*)
        and nm: "normalized_nnf_match m"
        and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
        and f_preserves: "⋀as_pos as_neg. f [] = Some (as_pos, as_neg) ⟹ as_pos = [] ∧ as_neg = []"
     shows "¬ has_disc disc m'"
   proof -
        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
        from notdisc primitive_extractor_correct(4)[OF nm wf asms] have 1: "¬ has_disc disc ms" by simp
        from notdisc primitive_extractor_correct(7)[OF nm wf asms] have 2: "as = [] ∧ ms = m" by simp
        from 1 2 some show ?thesis by(auto dest: f_preserves simp add: compress_normalize_primitive_def asms)
   qed

  lemma compress_normalize_primitive_not_introduces_C_negated:
    assumes notdisc: "¬ has_disc_negated disc False m"
        and wf: "wf_disc_sel (disc,sel) C"
        and nm: "normalized_nnf_match m"
        and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
        and f_preserves: "⋀as as_pos as_neg. f as = Some (as_pos, as_neg) ⟹ getNeg as = [] ⟹ as_neg = []"
     shows "¬ has_disc_negated disc False m'"
   proof -
        obtain as ms where asms: "primitive_extractor (disc,sel) m = (as, ms)" by fastforce
        from notdisc primitive_extractor_correct(6)[OF nm wf asms] have 1: "¬ has_disc_negated disc False ms" by simp
        from asms notdisc has_disc_negated_primitive_extractor[OF nm, where disc=disc and sel=sel] have
          "∀a. Neg a ∉ set as" by(simp)
        hence "getNeg as = []" by (meson NegPos_set(5) image_subset_iff last_in_set)
        with f_preserves have f_preserves': "⋀as_pos as_neg. f as = Some (as_pos, as_neg) ⟹ as_neg = []" by simp
        from 1 have "⋀ a b.¬ has_disc_negated disc False (MatchAnd (alist_and' (NegPos_map C (map Pos a))) ms)"
          by(simp add: has_disc_negated_alist_and' NegPos_map_map_Pos negation_type_to_match_expr_simps)
        with some show ?thesis by(auto dest: f_preserves' simp add: compress_normalize_primitive_def asms)
   qed




  lemma compress_normalize_primitive_Some:
  assumes normalized: "normalized_nnf_match m"
      and wf: "wf_disc_sel (disc,sel) C"
      and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
      and f_correct: "⋀as as_pos as_neg. f as = Some (as_pos, as_neg) ⟹
            matches γ (alist_and (NegPos_map C ((map Pos as_pos)@(map Neg as_neg)))) a p ⟷
            matches γ (alist_and (NegPos_map C as)) a p"
    shows "matches γ m' a p ⟷ matches γ m a p"
    using some
    apply(simp add: compress_normalize_primitive_def)
    apply(case_tac "primitive_extractor (disc,sel) m")
    apply(rename_tac as rst, simp)
    apply(drule primitive_extractor_correct(1)[OF normalized wf, where γ=γ and a=a and p=p])
    apply(elim exE conjE)
    apply(drule f_correct)
    by (meson matches_alist_and_alist_and' bunch_of_lemmata_about_matches(1))
    

  lemma compress_normalize_primitive_None:
  assumes normalized: "normalized_nnf_match m"
      and wf: "wf_disc_sel (disc,sel) C"
      and none: "compress_normalize_primitive (disc,sel) C f m = None"
      and f_correct: "⋀as. f as = None ⟹ ¬ matches γ (alist_and (NegPos_map C as)) a p"
    shows "¬ matches γ m a p"
    using none
    apply(simp add: compress_normalize_primitive_def)
    apply(case_tac "primitive_extractor (disc, sel) m")
    apply(auto dest: primitive_extractor_correct(1)[OF assms(1) wf] f_correct)
    done



  (* only for arbitrary discs that do not match C*)
  lemma compress_normalize_primitive_hasdisc:
    assumes am: "¬ has_disc disc2 m"
        and wf: "wf_disc_sel (disc,sel) C"
        and disc: "(∀a. ¬ disc2 (C a))"
        and nm: "normalized_nnf_match m"
        and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
     shows "normalized_nnf_match m' ∧ ¬ has_disc disc2 m'"
   proof -
        from compress_normalize_primitive_nnf[OF wf nm some] have goal1: "normalized_nnf_match m'" .
        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
        from am primitive_extractor_correct(4)[OF nm wf asms] have 1: "¬ has_disc disc2 ms" by simp
        { fix is_pos is_neg
          from disc have x1: "¬ has_disc disc2 (alist_and' (NegPos_map C (map Pos is_pos)))"
            by(simp add: has_disc_alist_and' NegPos_map_map_Pos negation_type_to_match_expr_simps)
          from disc have x2: "¬ has_disc disc2 (alist_and' (NegPos_map C (map Neg is_neg)))"
            by(simp add: has_disc_alist_and' NegPos_map_map_Neg negation_type_to_match_expr_simps)
          from x1 x2 have "¬ has_disc disc2 (alist_and' (NegPos_map C (map Pos is_pos @ map Neg is_neg)))"
            apply(simp add: NegPos_map_append has_disc_alist_and') by blast
        }
        with some have "¬ has_disc disc2 m'"
          apply(simp add: compress_normalize_primitive_def asms)
          apply(elim exE conjE)
          using 1 by fastforce
        with goal1 show ?thesis by simp
   qed
  lemma compress_normalize_primitive_hasdisc_negated:
    assumes am: "¬ has_disc_negated disc2 neg m"
        and wf: "wf_disc_sel (disc,sel) C"
        and disc: "(∀a. ¬ disc2 (C a))"
        and nm: "normalized_nnf_match m"
        and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
     shows "normalized_nnf_match m' ∧ ¬ has_disc_negated disc2 neg m'"
   proof -
        from compress_normalize_primitive_nnf[OF wf nm some] have goal1: "normalized_nnf_match m'" .
        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
        from am primitive_extractor_correct(6)[OF nm wf asms] have 1: "¬ has_disc_negated disc2 neg ms" by simp
        { fix is_pos is_neg
          from disc have x1: "¬ has_disc_negated disc2 neg (alist_and' (NegPos_map C (map Pos is_pos)))"
            by(simp add: has_disc_negated_alist_and' NegPos_map_map_Pos negation_type_to_match_expr_simps)
          from disc have x2: "¬ has_disc_negated disc2 neg (alist_and' (NegPos_map C (map Neg is_neg)))"
            by(simp add: has_disc_negated_alist_and' NegPos_map_map_Neg negation_type_to_match_expr_simps)
          from x1 x2 have "¬ has_disc_negated disc2 neg (alist_and' (NegPos_map C (map Pos is_pos @ map Neg is_neg)))"
            apply(simp add: NegPos_map_append has_disc_negated_alist_and') by blast
        }
        with some have "¬ has_disc_negated disc2 neg m'"
          apply(simp add: compress_normalize_primitive_def asms)
          apply(elim exE conjE)
          using 1 by fastforce
          
        with goal1 show ?thesis by simp
   qed


  thm normalize_primitive_extract_preserves_unrelated_normalized_n_primitive (*is similar*)
  lemma compress_normalize_primitve_preserves_normalized_n_primitive:
    assumes am: "normalized_n_primitive (disc2, sel2) P m"
        and wf: "wf_disc_sel (disc,sel) C"
        and disc: "(∀a. ¬ disc2 (C a))"
        and nm: "normalized_nnf_match m"
        and some: "compress_normalize_primitive (disc,sel) C f m = Some m'"
     shows "normalized_nnf_match m' ∧ normalized_n_primitive (disc2, sel2) P m'"
   proof -
        from compress_normalize_primitive_nnf[OF wf nm some] have goal1: "normalized_nnf_match m'" .
        obtain as ms where asms: "primitive_extractor (disc, sel) m = (as, ms)" by fastforce
        from am primitive_extractor_correct[OF nm wf asms] have 1: "normalized_n_primitive (disc2, sel2) P ms" by fast
        { fix iss
          from disc have "normalized_n_primitive (disc2, sel2) P (alist_and (NegPos_map C iss))"
            apply(induction iss)
             apply(simp_all)
            apply(rename_tac i iss, case_tac i)
             apply(simp_all)
            done
        }
        with some have "normalized_n_primitive (disc2, sel2) P m'"
          apply(simp add: compress_normalize_primitive_def asms)
          apply(elim exE conjE)
          using 1 normalized_n_primitive_alist_and' normalized_n_primitive_alist_and
                 normalized_n_primitive.simps(4) by blast 
        with goal1 show ?thesis by simp
   qed



subsection‹Processing a list of normalization functions›

fun compress_normalize_primitive_monad :: "('a match_expr ⇒ 'a match_expr option) list ⇒ 'a match_expr ⇒ 'a match_expr option" where
  "compress_normalize_primitive_monad [] m = Some m" |
  "compress_normalize_primitive_monad (f#fs) m = (case f m of None ⇒ None
                                                           |  Some m' ⇒ compress_normalize_primitive_monad fs m')"

lemma compress_normalize_primitive_monad: 
      assumes "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ matches γ m' a p ⟷ matches γ m a p"
          and "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m'"
          and "normalized_nnf_match m"
          and "(compress_normalize_primitive_monad fs m) = Some m'"
      shows "matches γ m' a p ⟷ matches γ m a p" (is ?goal1)
        and "normalized_nnf_match m'"              (is ?goal2)
  proof -
    (*everything in one big induction*)
    have goals: "?goal1 ∧ ?goal2"
    using assms proof(induction fs arbitrary: m)
    case Nil thus ?case by simp
    next
    case (Cons f fs)
      from Cons.prems(1) have IH_prem1:
        "(⋀f m m'. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ matches γ m' a p = matches γ m a p)" by auto
      from Cons.prems(2) have IH_prem2:
        "(⋀f m m'. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m')" by auto
      from Cons.IH IH_prem1 IH_prem2 have
        IH: "⋀m. normalized_nnf_match m ⟹ compress_normalize_primitive_monad fs m = Some m' ⟹
                  (matches γ m' a p ⟷ matches γ m a p) ∧ ?goal2" by fast
      show ?case
        proof(cases "f m")
          case None thus ?thesis using Cons.prems by auto
        next
          case(Some m'')
            from Some Cons.prems(1)[of f] Cons.prems(3) have 1: "matches γ m'' a p = matches γ m a p" by simp
            from Some Cons.prems(2)[of f] Cons.prems(3) have 2: "normalized_nnf_match m''" by simp
            from Some have "compress_normalize_primitive_monad (f # fs) m = compress_normalize_primitive_monad fs m''" by simp
            thus ?thesis using Cons.prems(4) IH 1 2 by auto 
        qed
    qed
    from goals show ?goal1 by simp
    from goals show ?goal2 by simp
  qed

(*proof is a bit sledgehammered*)
lemma compress_normalize_primitive_monad_None: 
      assumes "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ matches γ m' a p ⟷ matches γ m a p"
          and "⋀m f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = None ⟹ ¬ matches γ m a p"
          and "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m'"
          and "normalized_nnf_match m"
          and "(compress_normalize_primitive_monad fs m) = None"
      shows "¬ matches γ m a p"
    using assms proof(induction fs arbitrary: m)
    case Nil thus ?case by simp
    next
    case (Cons f fs)
      from Cons.prems(1) have IH_prem1:
        "(⋀f m m'. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ matches γ m' a p = matches γ m a p)" by auto
      from Cons.prems(2) have IH_prem2:
        "(⋀f m m'. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = None ⟹ ¬ matches γ m a p)" by auto
      from Cons.prems(3) have IH_prem3:
        "(⋀f m m'. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m')" by auto
      from Cons.IH IH_prem1 IH_prem2 IH_prem3 have
        IH: "⋀m. normalized_nnf_match m ⟹ compress_normalize_primitive_monad fs m = None ⟹ ¬  matches γ m a p" by blast
      show ?case
        proof(cases "f m")
          case None thus ?thesis using Cons.prems(4) Cons.prems(2) Cons.prems(3) by auto
        next
          case(Some m'')
            from Some Cons.prems(3)[of f] Cons.prems(4) have 2: "normalized_nnf_match m''" by simp
            from Some have "compress_normalize_primitive_monad (f # fs) m = compress_normalize_primitive_monad fs m''" by simp
            hence "¬ matches γ m'' a p" using Cons.prems(5) IH 2 by simp
            thus ?thesis using Cons.prems(1) Cons.prems(4) Some by auto 
        qed
    qed


lemma compress_normalize_primitive_monad_preserves:
      assumes "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ f m = Some m' ⟹ normalized_nnf_match m'"
          and "⋀m m' f. f ∈ set fs ⟹ normalized_nnf_match m ⟹ P m ⟹ f m = Some m' ⟹ P m'"
          and "normalized_nnf_match m"
          and "P m"
          and "(compress_normalize_primitive_monad fs m) = Some m'"
      shows "normalized_nnf_match m' ∧ P m'"
    using assms proof(induction fs arbitrary: m)
    case Nil thus ?case by simp
    next
    case (Cons f fs) thus ?case by(simp split: option.split_asm) blast (*1s*)
    qed




(*TODO: move to generic place and use? ? ? *)
datatype 'a match_compress = CannotMatch | MatchesAll | MatchExpr 'a


end