Theory Helper

theory Helper
imports Main
begin

section‹Hilfslemmata›


lemma helper_sum_int_if: ‹a ∉ set P ⟹
(∑x∈set P. int (if a = x then A1 x else A2 x) * B x) =
  (∑x∈set P. int (A2 x) * B x)›
  apply(rule sum.cong, simp)
  by fastforce

lemma sum_list_map_eq_sum_count_int:
  fixes f :: ‹'a ⇒ int›
  shows ‹sum_list (map f xs) = sum (λx. (int (count_list xs x)) * f x) (set xs)›
proof(induction ‹xs›)
  case (Cons x xs)
  show ‹?case› (is ‹?l = ?r›)
  proof cases
    assume ‹x ∈ set xs›
    have XXX: ‹(∑xa∈set xs - {x}. int (if x = xa then count_list xs xa + 1 else count_list xs xa) * f xa)
  = (∑xa∈set xs - {x}. int (count_list xs xa) * f xa)›
      thm helper_sum_int_if
      apply(rule sum.cong, simp)
      by auto
    have ‹?l = f x + (∑x∈set xs. (int (count_list xs x)) * f x)› by (simp add: Cons.IH)
    also have ‹set xs = insert x (set xs - {x})› using ‹x ∈ set xs›by blast
    also have ‹f x + (∑x∈insert x (set xs - {x}). (int (count_list xs x)) * f x) = ?r›
      apply(simp add: sum.insert_remove XXX)
      by (simp add: mult.commute ring_class.ring_distribs(1))
    finally show ‹?thesis› .
  next
    assume ‹x ∉ set xs›
    hence ‹⋀xa. xa ∈ set xs ⟹ x ≠ xa› by blast
    thus ‹?thesis› by (simp add: Cons.IH ‹x ∉ set xs›)
  qed
qed simp

lemma count_list_distinct: ‹distinct P ⟹ x ∈ set P ⟹ count_list P x = 1›
  apply(induction ‹P›)
   apply(simp; fail)
  by(auto)


lemma is_singleton_the_elem_as_set: ‹is_singleton A ⟹ the_elem A = a ⟷ A = {a}›
  apply(rule iffI)
   apply (simp add: is_singleton_the_elem)
  apply(simp add: the_elem_def)
  done

(*the simplifier loops with this one, sometimes. If it loops, apply(elim is_singletonE) first.*)
lemma singleton_set_to_all: ‹{a ∈ A. P a} = {b} ⟷ (∀a. (a ∈ A ∧ P a) = (a = b))›
  by fastforce

lemma singleton_set_to_all2: ‹A = {b} ⟷ (∀a. (a ∈ A) = (a = b))›
  by fastforce

lemma is_singleton_bij_image: ‹bij f ⟹ is_singleton (f ` A) = is_singleton A›
  by (metis bij_betw_same_card bij_betw_subset is_singleton_altdef subset_UNIV)



text‹For some reason, I like \<^const>‹List.map_filter›. But standard library support is poor.›
lemma List_map_filter_as_comprehension:
  ‹List.map_filter f xs = [the (f x). x ← xs, f x ≠ None]›
  by(induction ‹xs›) (simp add: List.map_filter_def)+
lemma List_map_filter_as_foldr:
  ‹List.map_filter f xs = foldr (λx acc. case f x of Some a ⇒ a#acc | None ⇒ acc) xs []›
  apply(induction ‹xs›)
  apply(simp add: List.map_filter_def)
  apply(simp add: List.map_filter_def)
  apply(safe, simp)
  done




lemma concat_map_if: ‹concat (map (λx. if P x then [x] else []) xs) = filter P xs›
  by(induction ‹xs›) auto


lemma fold_fun_update_call_helper:
  ‹p ∉ set xs ⟹ fold (λx acc. acc(x := f x)) xs start p = start p›
  by(induction ‹xs› arbitrary: ‹start›) simp+

lemma fold_fun_update_call:
  ‹p ∈ set xs ⟹ distinct xs ⟹ fold (λx acc. acc(x := f x)) xs start p = f p›
  apply(induction ‹xs› arbitrary: ‹start›)
   apply(simp; fail)
  apply(simp)
  apply(safe)
   apply(simp add: fold_fun_update_call_helper; fail)
  apply(simp)
  done

lemma fold_enum_fun_update_call:
  ‹fold (λx acc. acc(x := f x)) Enum.enum start p = f p›
  apply(rule fold_fun_update_call)
   apply(simp add: enum_class.enum_UNIV)
  apply(simp add: enum_class.enum_distinct)
  done

lemma fold_enum_fun_update:
  ‹fold (λx acc. acc(x := f x)) Enum.enum start = f›
  using fold_enum_fun_update_call by auto  
end