Theory TA_Impl_Misc2

theory TA_Impl_Misc2
  imports
    Munta_Base.TA_Impl_Misc
    "HOL-Library.Sublist"
    "List-Index.List_Index"
    Automatic_Refinement.Misc
begin

lemma mem_nth:
  "x ∈ set xs ⟹ ∃ i < length xs. xs ! i = x"
  by (metis index_less_size_conv nth_index)

lemma union_subsetI:
  "A ∪ B ⊆ C ∪ D" if "A ⊆ C" "B ⊆ D"
  using that by blast

lemma map_eq_imageD:
  "f ` set xs = set ys" if "map f xs = ys"
  using that by auto

lemma if_contract:
  "(if a then x else if b then x else y) = (if a ∨ b then x else y)" for a x b y
  by (rule SMT.z3_rule)

paragraph ‹More intros›

named_theorems more_intros
named_theorems more_elims
lemmas [more_intros] =
  image_eqI[rotated] CollectI subsetI

lemmas [more_elims] =
  CollectE

paragraph ‹Finiteness›

lemma finite_prodI:
  "finite {(a,b). P a ∧ Q b}" if "finite {a. P a}" "finite {a. Q a}"
  using that by simp

lemma finite_prodI3:
  "finite {(a,b,c). P a ∧ Q b ∧ Q1 c}"
  if "finite {a. P a}" "finite {a. Q a}" "finite {a. Q1 a}"
  using that by simp

lemma finite_prodI4:
  "finite {(a,b,c,d). P a ∧ Q b ∧ Q1 c ∧ Q2 d}"
  if "finite {a. P a}" "finite {a. Q a}" "finite {a. Q1 a}" "finite {a. Q2 a}"
  using that by simp

lemma finite_prodI5:
  "finite {(a,b,c,d,e). P a ∧ Q b ∧ Q1 c ∧ Q2 d ∧ Q3 e}"
  if "finite {a. P a}" "finite {a. Q a}" "finite {a. Q1 a}" "finite {a. Q2 a}" "finite {a. Q3 a}"
  using that by simp

named_theorems finite_intros
named_theorems more_finite_intros

lemmas [finite_intros] =
  finite_UnI finite_Union finite_imageI
  finite_lists_length_eq finite_lists_length_le
  finite_subset_distinct distinct_finite_set

lemmas [more_finite_intros] =
  finite_prodI finite_prodI3 finite_prodI4 finite_prodI5

paragraph ‹Lists›

lemma fold_evD2:
  assumes
    "P y (fold f xs acc)" "¬ P y acc"
    "⋀ acc x. ¬ P y acc ⟹ Q acc ⟹ P y (f x acc) ⟹ x ∈ set xs ⟹ x = y"
    "Q acc" "⋀ acc x. Q acc ⟹ Q (f x acc)"
    "⋀ acc x. ¬ P y acc ⟹ Q acc ⟹ P y (f x acc) ⟹ R y"
  shows "∃ ys zs. xs = ys @ y # zs ∧ ¬ P y (fold f ys acc) ∧ P y (f y (fold f ys acc)) ∧ R y"
proof -
  from fold_evD'[OF assms(2,1)] obtain x ys zs where *:
    "xs = ys @ x # zs" "¬ P y (fold f ys acc)" "P y (f x (fold f ys acc))"
    by auto
  moreover from assms(4-) have "Q (fold f ys acc)" by (auto intro: fold_acc_preserv)
  moreover from ‹xs = _› have "x ∈ set xs"
    by auto
  ultimately show ?thesis using assms(3,6) by auto
qed

lemmas fold_evD2' = fold_evD2[where R = "λ _. True", simplified]

lemma filter_map_map_filter:
  "filter P (map f xs) = List.map_filter (λ x. let y = f x in if P y then Some y else None) xs"
  by (induction xs; simp add: Let_def List.map_filter_simps)

lemma distinct_map_filterI:
  "distinct (List.map_filter f xs)"
  if "∀x ∈ set xs. ∀y ∈ set xs. ∀a. f x = Some a ∧ f y = Some a ⟶ x = y" "distinct xs"
  using that by (induction xs) (auto simp: map_filter_simps set_map_filter split: option.split)

lemma filter_eqI:
  assumes
    "subseq ys xs" "∀x ∈ set ys. P x"
    "∀zs. subseq zs xs ∧ length zs > length ys ⟶ (∃ x ∈ set zs. ¬ P x)"
  shows "filter P xs = ys"
  using assms
proof (induction xs arbitrary: ys rule: list.induct)
  case Nil
  then show ?case
    by - (cases ys; simp)
next
  case (Cons x xs)
  show ?case
  proof (cases "P x")
    case True
    show ?thesis
    proof (cases ys)
      case Nil
      have "subseq [x] (x # xs)"
        by auto
      with Cons.prems Nil ‹P x› show ?thesis
        by fastforce
    next
      case (Cons y ys')
      have "x = y"
      proof (rule ccontr)
        assume "x ≠ y"
        with ‹subseq ys (x # xs)› ‹ys = _› have "subseq (x # ys) (x # xs)"
          by simp
        with Cons.prems(2-) ‹P x› show False
          by fastforce
      qed
      have "∃x∈set zs. ¬ P x" if "subseq zs xs" and "length ys' < length zs" for zs
      proof -
        from ‹subseq zs xs› have "subseq (x # zs) (x # xs)"
          by simp
        with ‹length ys' < length zs› Cons.prems(3) ‹ys = _› have "∃x∈set (x # zs). ¬ P x"
          by (intro Cons.prems(3)[rule_format]; simp)
        with ‹P x› show ?thesis
          by auto
      qed
      with Cons.prems ‹P x› ‹ys = _› ‹x = y› show ?thesis
        by (auto intro!: Cons.IH)
    qed
  next
    case False
    with Cons.prems show ?thesis
      by (cases ys) (auto split: if_split_asm intro!: Cons.IH)
  qed
qed

lemma filter_greatest_subseqD:
  "∃ x ∈ set zs. ¬ P x" if "subseq zs xs" "length zs > length (filter P xs)"
  using that by (metis filter_id_conv not_subseq_length subseq_filter)

lemma filter_eq_iff_greatest_subseq:
  "filter P xs = ys ⟷
  subseq ys xs ∧ (∀x ∈ set ys. P x) ∧
  (∀zs. subseq zs xs ∧ length zs > length ys ⟶ (∃ x ∈ set zs. ¬ P x))"
  using filter_greatest_subseqD filter_eqI by auto

lemma subseq_subsetD:
  "set xs ⊆ set ys" if "subseq xs ys"
  using that
  by (intro subsetI) (unfold subseq_singleton_left[symmetric], erule subseq_order.trans)

lemma subseq_distinct:
  "distinct xs" if "distinct ys" "subseq xs ys"
  using subseqs_distinctD that by simp

lemma finite_subseqs:
  "finite {xs. subseq xs ys}" (is "finite ?S")
proof -
  have "?S ⊆ {xs. set xs ⊆ set ys ∧ length xs ≤ length ys}"
    using not_subseq_length by (force dest: subseq_subsetD)
  also have "finite …"
    by (auto intro: finite_lists_length_le)
  finally (finite_subset) show ?thesis .
qed

lemma filter_distinct_eqI:
  assumes
    "subseq ys xs" "∀x ∈ set ys. P x" "∀x ∈ set xs. x ∉ set ys ⟶ ¬ P x" "distinct xs"
  shows "filter P xs = ys"
proof (intro filter_eqI, safe)
  fix zs assume prems: "subseq zs xs" "length ys < length zs"
  obtain x where "x ∈ set zs" "x ∉ set ys"
  proof (atomize_elim, rule ccontr)
    assume "∄x. x ∈ set zs ∧ x ∉ set ys"
    then have "set zs ⊆ set ys"
      by auto
    moreover from prems assms have "distinct zs" "distinct ys"
      by (blast intro: subseq_distinct)+
    ultimately show False
      using ‹length ys < length zs›
      by (auto dest: card_mono[rotated] simp: distinct_card[symmetric])
  qed
  with prems assms show "∃x∈set zs. ¬ P x"
    by (auto 4 3 dest: subseq_subsetD)
qed (use assms in blast)+

lemma subseq_sorted_wrt:
  "sorted_wrt R xs" if "sorted_wrt R ys" "subseq xs ys"
  using that
  by (induction xs arbitrary: ys)
     (auto 0 4 dest: subseq_subsetD list_emb_ConsD subseq_Cons' simp: sorted_wrt_append)

lemma subseq_sorted:
  "sorted xs" if "sorted ys" "subseq xs ys"
  using that by (rule subseq_sorted_wrt)

lemma sorted_distinct_subset_subseqI:
  assumes "sorted xs" "distinct xs" "sorted ys" "set xs ⊆ set ys"
  shows "subseq xs ys"
  using assms
proof (induction ys arbitrary: xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons y ys xs)
  from Cons.prems show ?case
    by (cases xs; simp) (safe; rule Cons.IH; auto 4 4)
qed

lemma sorted_distinct_subseq_iff:
  assumes "sorted ys" "distinct ys"
  shows "subseq xs ys ⟷ (sorted xs ∧ distinct xs ∧ set xs ⊆ set ys)"
  using assms
  by safe
     (erule
       subseq_subsetD[THEN subsetD] sorted_distinct_subset_subseqI subseq_distinct subseq_sorted;
       assumption
     )+

lemma subseq_mapE:
  assumes "subseq xs (map f ys)"
  obtains xs' where "subseq xs' ys" "map f xs' = xs"
  using assms
  by (induct x1 ≡ xs x2 ≡ "map f ys" arbitrary: xs ys rule: list_emb.induct)
     (auto, metis map_consI(1) subseq_Cons2)

lemma list_all2_map_fst_aux:
  assumes "list_all2 (λx y. x ∈ Pair y ` (zs y)) xs ys"
  shows "list_all2 (=) (map fst xs) ys"
  using assms by (smt fstI imageE list.rel_mono_strong list_all2_map1)

lemma list_all2_fst_aux:
  "map fst xs = ys" if "list_all2 (λx y. fst x = y) xs ys"
  using that by (induction) auto

text ‹Stronger version of @{thm Map.map_of_mapk_SomeI}›
theorem map_of_mapk_SomeI':
  assumes "inj_on f (fst ` set t)"
    and "map_of t k = Some x"
  shows "map_of (map (λ(k, y). (f k, g y)) t) (f k) = Some (g x)"
  using assms
  apply (induction t)
   apply (solves simp)
  apply (clarsimp split: if_split_asm)
  apply (metis DiffI imageI img_fst map_of_SomeD singletonD)
  done

theorem map_of_mapk_SomeI:
  assumes "inj f"
    and "map_of t k = Some x"
  shows "map_of (map (λ(k, y). (f k, g y)) t) (f k) = Some (g x)"
  using assms by - (rule map_of_mapk_SomeI', erule inj_on_subset, auto)

lemma list_all2_map_eq_iff:
  "list_all2 (λx y. f x = g y) xs ys ⟷ map f xs = map g ys"
proof
  assume "list_all2 (λx y. f x = g y) xs ys"
  then show "map f xs = map g ys"
    by induction auto
next
  assume "map f xs = map g ys"
  then have "length xs = length ys"
    by (rule map_eq_imp_length_eq)
  then show "list_all2 (λx y. f x = g y) xs ys"
    using ‹map f xs = _› by (induction rule: list_induct2; simp)
qed

end