# Theory MatchExpr_Fold

```section‹Combine Match Expressions›
theory MatchExpr_Fold
imports Primitive_Normalization
begin

fun andfold_MatchExp :: "'a match_expr list ⇒ 'a match_expr" where
"andfold_MatchExp [] = MatchAny" |
"andfold_MatchExp [e] = e" |
"andfold_MatchExp (e#es) = MatchAnd e (andfold_MatchExp es)"

lemma andfold_MatchExp_alist_and: "alist_and' (map Pos ls) = andfold_MatchExp (map Match ls)"
apply(induction ls)
apply(simp)
apply(simp)
apply(rename_tac l ls)
apply(case_tac "ls")
by(simp)+

lemma andfold_MatchExp_matches:
"matches γ (andfold_MatchExp ms) a p ⟷ (∀m ∈ set ms. matches γ m a p)"
apply(induction ms rule: andfold_MatchExp.induct)
done

lemma andfold_MatchExp_not_discI:
"∀m ∈ set ms. ¬ has_disc disc m ⟹ ¬ has_disc disc (andfold_MatchExp ms)"
by(induction ms rule: andfold_MatchExp.induct) (simp)+

lemma andfold_MatchExp_not_disc_negatedI:
"∀m ∈ set ms. ¬ has_disc_negated disc neg m ⟹ ¬ has_disc_negated disc neg (andfold_MatchExp ms)"
by(induction ms rule: andfold_MatchExp.induct) (simp)+

lemma andfold_MatchExp_not_disc_negated_mapMatch:
"¬ has_disc_negated disc False (andfold_MatchExp (map (Match ∘ C) ls))"
apply(induction ls)
apply(simp; fail)
apply(simp)
apply(rename_tac ls, case_tac ls)
by(simp)+

lemma andfold_MatchExp_not_disc_mapMatch:
"∀a. ¬ disc (C a) ⟹ ¬ has_disc disc (andfold_MatchExp (map (Match ∘ C) ls))"
apply(induction ls)
apply(simp; fail)
apply(simp)
apply(rename_tac ls, case_tac ls)
by(simp)+

lemma andfold_MatchExp_normalized_nnf: "∀m ∈ set ms. normalized_nnf_match m ⟹
normalized_nnf_match (andfold_MatchExp ms)"
by(induction ms rule: andfold_MatchExp.induct)(simp)+

lemma andfold_MatchExp_normalized_n_primitive: "∀m ∈ set ms. normalized_n_primitive (disc, sel) f m ⟹
normalized_n_primitive (disc, sel) f (andfold_MatchExp ms)"
by(induction ms rule: andfold_MatchExp.induct)(simp)+

lemma andfold_MatchExp_normalized_normalized_n_primitive_single:
"∀a. ¬ disc (C a) ⟹
s ∈ set (normalize_match (andfold_MatchExp (map (Match ∘ C) xs))) ⟹
normalized_n_primitive (disc, sel) f s"
apply(rule normalized_n_primitive_if_no_primitive)
using normalized_nnf_match_normalize_match apply blast
apply(rule normalize_match_preserves_nodisc[where m="(andfold_MatchExp (map (Match ∘ C) xs))"])
apply simp_all

lemma normalize_andfold_MatchExp_normalized_n_primitive:
"∀ m ∈ set ms. ∀ s' ∈ set (normalize_match m). normalized_n_primitive (disc, sel) f s' ⟹
s ∈ set (normalize_match (andfold_MatchExp ms)) ⟹
normalized_n_primitive (disc, sel) f s"
proof(induction ms arbitrary: s rule: andfold_MatchExp.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by simp
next
case (3 v1 v2 va)
have IH: "s' ∈ set (normalize_match (andfold_MatchExp (v2 # va))) ⟹
normalized_n_primitive (disc, sel) f s'" for s'
using 3(1)[of s'] (*without this, simp loops*)
apply(simp)
using 3(2) by force
from 3(2,3) IH show ?case by(clarsimp)
qed
end
```