# 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)
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)

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)
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)

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)

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(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(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)

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)
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)

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)
done

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)
next
case 3 thus ?case
apply(simp split: if_split_asm)
apply(clarify)
next
case (4 m1 m2 as ms)
from 4 show ?case
apply(simp)
apply(simp split: prod.split_asm)
apply(clarify)
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)

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)

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)

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}
\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"
also have "... ⟷ match_list γ (normalize_primitive_extract disc_sel C f m) a p"
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)

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(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(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(clarify)
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)"
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(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)

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(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)))"
from disc have x2: "¬ has_disc disc2 (alist_and' (NegPos_map C (map Neg is_neg)))"
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(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)))"
from disc have x2: "¬ has_disc_negated disc2 neg (alist_and' (NegPos_map C (map Neg is_neg)))"
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(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(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')"

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*)
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

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