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)
    apply(simp add: bunch_of_lemmata_about_matches)+
  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
  by (simp add: andfold_MatchExp_not_discI)

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