Theory Misc

(*
  File:    Misc.thy
  Authors: Max W. Haslbeck, Manuel Eberl
*)
section ‹Auxiliary material›
theory Misc
  imports "HOL-Analysis.Analysis"
begin

text ‹Based on @{term sorted_list_of_set} and @{term the_inv_into} we construct a bijection between
  a finite set A of type 'a::linorder and a set of natural numbers @{term "{..< card A}"}

lemma bij_betw_mono_on_the_inv_into:
  fixes A::"'a::linorder set" and B::"'b::linorder set"
  assumes b: "bij_betw f A B" and m: "mono_on A f"
  shows "mono_on B (the_inv_into A f)"
proof (rule ccontr)
  assume "¬ mono_on B (the_inv_into A f)"
  then have "r s. r  B  s  B  r  s  ¬ the_inv_into A f s  the_inv_into A f r"
    unfolding mono_on_def by blast
  then obtain r s where rs: "r  B" "s  B" "r  s" "the_inv_into A f s < the_inv_into A f r"
    by fastforce
  have f: "f (the_inv_into A f b) = b" if "b  B" for b
    using that assms f_the_inv_into_f_bij_betw by metis
  have "the_inv_into A f s  A" "the_inv_into A f r  A"
    using rs assms by (auto simp add: bij_betw_def the_inv_into_into)
  then have "f (the_inv_into A f s)  f (the_inv_into A f r)"
   using rs by (intro mono_onD[OF m]) (auto)
  then have "r = s"
    using rs f by simp
  then show False
    using rs by auto
qed

lemma rev_removeAll_removeAll_rev: "rev (removeAll x xs) = removeAll x (rev xs)"
  by (simp add: removeAll_filter_not_eq rev_filter)

lemma sorted_list_of_set_Min_Cons:
  assumes "finite A" "A  {}"
  shows "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
proof -
  have *: "A = insert (Min A) A"
    using assms Min_in by (auto)
  then have "sorted_list_of_set A = insort (Min A) (sorted_list_of_set (A - {Min A}))"
    using assms by (subst *, intro sorted_list_of_set_insert_remove) auto
  also have " = Min A # sorted_list_of_set (A - {Min A})"
    using assms by (intro insort_is_Cons) (auto)
  finally show ?thesis
    by simp
qed

lemma sorted_list_of_set_filter:
  assumes "finite A"
  shows "sorted_list_of_set ({xA. P x}) = filter P (sorted_list_of_set A)"
  using assms proof (induction "sorted_list_of_set A" arbitrary: A)
  case (Cons x xs)
  have x: "x  A"
    using Cons sorted_list_of_set list.set_intros(1) by metis
  have "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
    using Cons by (intro sorted_list_of_set_Min_Cons) auto
  then have 1: "x = Min A" "xs = sorted_list_of_set (A - {x})"
    using Cons by auto
  { assume Px: "P x"
    have 2: "sorted_list_of_set {x  A. P x} = Min {x  A. P x} # sorted_list_of_set ({x  A. P x} - {Min {x  A. P x}})"
      using Px Cons 1 sorted_list_of_set_eq_Nil_iff
      by (intro sorted_list_of_set_Min_Cons) fastforce+
    also have 3: "Min {x  A. P x} = x"
      using Cons 1 Px x by (auto intro!: Min_eqI)
    also have 4: "{x  A. P x} - {x} = {y  A - {x}. P y}"
      by blast
    also have 5: "sorted_list_of_set {y  A - {x}. P y} = filter P (sorted_list_of_set (A - {x}))"
      using 1 Cons by (intro Cons) (auto)
    also have " = filter P xs"
      using 1 by simp
    also have "filter P (sorted_list_of_set A) = x # filter P xs"
      using Px by (simp flip: x # xs = sorted_list_of_set A)
    finally have ?case
      by auto }
  moreover
  { assume Px: "¬ P x"
    then have "{x  A. P x} = {y  A - {x}. P y}"
      by blast
    also have "sorted_list_of_set  = filter P (sorted_list_of_set (A - {x}))"
      using 1 Cons by (intro Cons) auto
    also have  "filter P (sorted_list_of_set (A - {x})) = filter P (sorted_list_of_set A)"
      using 1 Px by (simp flip: x # xs = sorted_list_of_set A)
    finally have ?case
      by simp }
  ultimately show ?case
    by blast
qed (use sorted_list_of_set_eq_Nil_iff in fastforce)

lemma sorted_list_of_set_Max_snoc:
  assumes "finite A" "A  {}"
  shows "sorted_list_of_set A = sorted_list_of_set (A - {Max A}) @ [Max A]"
proof -
  have *: "A = insert (Max A) A"
    using assms Max_in by (auto)
  then have "sorted_list_of_set A = insort (Max A) (sorted_list_of_set (A - {Max A}))"
    using assms by (subst *, intro sorted_list_of_set_insert_remove) auto
  also have " = sorted_list_of_set (A - {Max A}) @ [Max A]"
    using assms by (intro sorted_insort_is_snoc) (auto)
  finally show ?thesis
    by simp
qed

lemma sorted_list_of_set_image:
  assumes "mono_on A g" "inj_on g A"
  shows "(sorted_list_of_set (g ` A)) = map g (sorted_list_of_set A)"
proof (cases "finite A")
  case True
  then show ?thesis
    using assms proof (induction "sorted_list_of_set A" arbitrary: A)
    case Nil
    then show ?case
      using sorted_list_of_set_eq_Nil_iff by fastforce
  next
    case (Cons x xs A)
    have not_empty_A: "A  {}"
      using Cons sorted_list_of_set_eq_Nil_iff by auto
    have *: "Min (g ` A) = g (Min A)"
    proof -
      have "g (Min A)  g a" if "a  A" for a
        using that Cons Min_in Min_le not_empty_A by (auto intro!: mono_onD[of _ g])
      then show ?thesis
        using Cons not_empty_A by (intro Min_eqI) auto
    qed
    have "g ` A  {}" "finite (g ` A)"
      using Cons by auto
    then have "(sorted_list_of_set (g ` A)) =
             Min (g ` A) # sorted_list_of_set ((g ` A) - {Min (g ` A)})"
      by (auto simp add: sorted_list_of_set_Min_Cons)
    also have "(g ` A) - {Min (g ` A)} = g ` (A - {Min A})"
      using Cons Min_in not_empty_A * by (subst inj_on_image_set_diff[of _ A]) auto
    also have "sorted_list_of_set (g ` (A - {Min A})) = map g (sorted_list_of_set (A - {Min A}))"
      using not_empty_A Cons mono_on_subset[of A _ "A - {Min A}"] inj_on_subset[of _ A "A - {Min A}"]
      by (intro Cons) (auto simp add: sorted_list_of_set_Min_Cons)
    finally show ?case
      using Cons not_empty_A * by (auto simp add: sorted_list_of_set_Min_Cons)
  qed
next
  case False
  then show ?thesis
    using assms by (simp add: finite_image_iff)
qed

lemma sorted_list_of_set_length: "length (sorted_list_of_set A) = card A"
  using distinct_card sorted_list_of_set[of A] by (cases "finite A") fastforce+

lemma sorted_list_of_set_bij_betw:
  assumes "finite A"
  shows "bij_betw (λn. sorted_list_of_set A ! n) {..<card A} A"
  by (rule bij_betw_nth) (fastforce simp add: assms sorted_list_of_set_length)+

lemma nth_mono_on:
  assumes "sorted xs" "distinct xs" "set xs = A"
  shows "mono_on {..<card A} (λn. xs ! n)"
  using assms by (intro mono_onI sorted_nth_mono) (auto simp add: distinct_card)

lemma sorted_list_of_set_mono_on:
  "finite A  mono_on {..<card A} (λn. sorted_list_of_set A ! n)"
  by (rule nth_mono_on) (auto)

definition bij_mono_map_set_to_nat :: "'a::linorder set  'a  nat" where
  "bij_mono_map_set_to_nat A =
    (λx. if x  A then the_inv_into {..<card A} ((!) (sorted_list_of_set A)) x
                  else card A)"

lemma bij_mono_map_set_to_nat:
  assumes "finite A"
  shows "bij_betw (bij_mono_map_set_to_nat A) A {..<card A}"
        "mono_on A (bij_mono_map_set_to_nat A)"
        "(bij_mono_map_set_to_nat A) ` A = {..<card A}"
proof -
  let ?f = "bij_mono_map_set_to_nat A"
  have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}"
    using assms sorted_list_of_set_bij_betw  bij_betw_the_inv_into by blast
  moreover have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}
                     = bij_betw ?f A {..<card A}"
    unfolding bij_mono_map_set_to_nat_def by (rule bij_betw_cong) simp
  ultimately show *: "bij_betw (bij_mono_map_set_to_nat A) A {..<card A}"
    by blast
  have "mono_on A (the_inv_into {..<card A} ((!) (sorted_list_of_set A)))"
    using assms sorted_list_of_set_bij_betw
      sorted_list_of_set_mono_on by (intro bij_betw_mono_on_the_inv_into) auto
  then show "mono_on A (bij_mono_map_set_to_nat A)"
    unfolding bij_mono_map_set_to_nat_def using mono_onD by (intro mono_onI) (auto)
  show "?f ` A = {..<card A}"
      using assms bij_betw_imp_surj_on * by blast
qed

end