Theory Library_Additions

section ‹Library additions›

theory Library_Additions
  imports "ZFC_in_HOL.Ordinal_Exp" "HOL-Library.Ramsey" "Nash_Williams.Nash_Williams"

begin

lemma finite_enumerate_Diff_singleton:
  fixes S :: "'a::wellorder set"
  assumes "finite S" and i: "i < card S" "enumerate S i < x"
  shows "enumerate (S - {x}) i = enumerate S i"
  using i
proof (induction i)
  case 0
  have "(LEAST i. i  S  ix) = (LEAST i. i  S)"
  proof (rule Least_equality)
    have "t. t  S  tx"
      using 0 finite S finite_enumerate_in_set by blast
    then show "(LEAST i. i  S)  S  (LEAST i. i  S)  x"
      by (metis "0.prems"(2) LeastI enumerate_0 not_less_Least)
  qed (simp add: Least_le)
  then show ?case
    by (auto simp: enumerate_0)
next
  case (Suc i)
  then have x: "enumerate S i < x"
    by (meson enumerate_step finite_enumerate_step less_trans)
  have cardSx: "Suc i < card (S - {x})" and "i < card S"
    using Suc finite S card_Diff_singleton_if[of S] finite_enumerate_Ex by fastforce+
  have "(LEAST s. s  S  sx  enumerate (S - {x}) i < s) = (LEAST s. s  S  enumerate S i < s)"
       (is "_ = ?r")
  proof (intro Least_equality conjI)
    show "?r  S"
      by (metis (lifting) LeastI Suc.prems(1) assms(1) finite_enumerate_in_set finite_enumerate_step)
    show "?r  x"
      using Suc.prems not_less_Least [of _ "λt. t  S  enumerate S i < t"] 
       finite S finite_enumerate_in_set finite_enumerate_step by blast
    show "enumerate (S - {x}) i < ?r"
      by (metis (full_types) Suc.IH Suc.prems(1) i < card S enumerate_Suc'' enumerate_step finite_enumerate_Suc'' finite_enumerate_step x)
    show "y. y  S  y  x  enumerate (S - {x}) i < y  ?r  y"
      by (simp add: Least_le Suc.IH i < card S x)
  qed
  then show ?case
    using Suc assms by (simp add: finite_enumerate_Suc'' cardSx)
qed

lemma hd_lex: "hd ms < hd ns; length ms = length ns; ns  []  (ms, ns)  lex less_than"
  by (metis hd_Cons_tl length_0_conv less_than_iff lexord_cons_cons lexord_lex)

lemma sorted_hd_le:
  assumes "sorted xs" "x  list.set xs"
  shows "hd xs  x"
  using assms by (induction xs) (auto simp: less_imp_le)

lemma sorted_le_last:
  assumes "sorted xs" "x  list.set xs"
  shows "x  last xs"
  using assms by (induction xs) (auto simp: less_imp_le)

lemma hd_list_of:
  assumes "finite A" "A  {}"
  shows "hd (sorted_list_of_set A) = Min A" 
proof (rule antisym)
  have "Min A  A"
    by (simp add: assms)
  then show "hd (sorted_list_of_set A)  Min A"
    by (simp add: sorted_hd_le finite A)
next
  show "Min A  hd (sorted_list_of_set A)"
    by (metis Min_le assms hd_in_set set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
qed

lemma sorted_hd_le_last:
  assumes "sorted xs" "xs  []"
  shows "hd xs  last xs"
  using assms by (simp add: sorted_hd_le)

lemma sorted_list_of_set_set_of [simp]: "strict_sorted l  sorted_list_of_set (list.set l) = l"
  by (simp add: strict_sorted_equal)

lemma range_strict_mono_ext:
  fixes f::"nat  'a::linorder"
  assumes eq: "range f = range g"
      and sm: "strict_mono f" "strict_mono g"
    shows "f = g"
proof
  fix n
  show "f n = g n"
  proof (induction n rule: less_induct)
    case (less n)
    obtain x y where xy: "f n = g y" "f x = g n"
      by (metis eq imageE rangeI)
    then have "n = y"
      by (metis (no_types) less.IH neq_iff sm strict_mono_less xy)
    then show ?case using xy by auto
  qed
qed

subsection ‹Other material›

definition strict_mono_sets :: "['a::order set, 'a::order  'b::order set]  bool" where
  "strict_mono_sets A f  xA. yA. x < y  less_sets (f x) (f y)"

lemma strict_mono_setsD:
  assumes "strict_mono_sets A f" "x < y" "x  A" "y  A"
  shows "less_sets (f x) (f y)"
  using assms by (auto simp: strict_mono_sets_def)

lemma strict_mono_sets_imp_disjoint:
  fixes A :: "'a::linorder set"
  assumes "strict_mono_sets A f"
  shows "pairwise (λx y. disjnt (f x) (f y)) A"
  using assms unfolding strict_mono_sets_def pairwise_def
  by (meson antisym_conv3 disjnt_sym less_sets_imp_disjnt)

lemma strict_mono_sets_subset:
  assumes "strict_mono_sets B f" "A  B"
  shows "strict_mono_sets A f"
  using assms by (auto simp: strict_mono_sets_def)

lemma strict_mono_less_sets_Min:
  assumes "strict_mono_sets I f" "finite I" "I  {}"
  shows "less_sets (f (Min I)) ( (f ` (I - {Min I})))"
  using assms by (simp add: strict_mono_sets_def less_sets_UN2 dual_order.strict_iff_order)

lemma pair_less_iff1 [simp]: "((x,y), (x,z))  pair_less  y<z"
  by (simp add: pair_less_def)

lemma infinite_finite_Inter:
  assumes "finite 𝒜" "𝒜{}" "A. A  𝒜  infinite A"
    and "A B. A  𝒜; B  𝒜  A  B  𝒜"
  shows "infinite (𝒜)"
  by (simp add: assms finite_Inf_in)

lemma atLeast_less_sets: "less_sets A {x}; B  {x..}  less_sets A B"
  by (force simp: less_sets_def subset_iff)



subsection ‹The list-of function›

lemma sorted_list_of_set_insert_remove_cons:
  assumes "finite A" "less_sets {a} A"
  shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A"
proof -
  have "strict_sorted (a # sorted_list_of_set A)"
    using assms less_setsD by auto
  moreover have "list.set (a # sorted_list_of_set A) = insert a A"
    using assms by force
  moreover have "length (a # sorted_list_of_set A) = card (insert a A)"
    using assms card_insert_if less_setsD by fastforce
  ultimately show ?thesis
    by (metis finite A finite_insert sorted_list_of_set_unique)
qed

lemma sorted_list_of_set_Un:
  assumes AB: "less_sets A B" and fin: "finite A" "finite B"
  shows "sorted_list_of_set (A  B) = sorted_list_of_set A @ sorted_list_of_set B"
proof -
  have "strict_sorted (sorted_list_of_set A @ sorted_list_of_set B)"
    using AB unfolding less_sets_def
    by (metis fin set_sorted_list_of_set sorted_wrt_append strict_sorted_list_of_set)
  moreover have "card A + card B = card (A  B)"
    using less_sets_imp_disjnt [OF AB]
    by (simp add: assms card_Un_disjoint disjnt_def)
  ultimately show ?thesis
    by (simp add: assms strict_sorted_equal)
qed

lemma sorted_list_of_set_UN_lessThan:
  fixes k::nat
  assumes sm: "strict_mono_sets {..<k} A" and "i. i < k  finite (A i)"
  shows "sorted_list_of_set (i<k. A i) = concat (map (sorted_list_of_set  A) (sorted_list_of_set {..<k}))"
  using assms
proof (induction k)
  case 0
  then show ?case
    by auto
next
  case (Suc k)
  have ls: "less_sets ( (A ` {..<k})) (A k)"
    using sm Suc.prems(1) strict_mono_setsD by (force simp: less_sets_UN1)
  have "sorted_list_of_set ( (A ` {..<Suc k})) = sorted_list_of_set ( (A ` {..<k})  A k)"
    by (simp add: Un_commute lessThan_Suc)
  also have " = sorted_list_of_set ( (A ` {..<k})) @ sorted_list_of_set (A k)"
    by (rule sorted_list_of_set_Un) (auto simp: Suc.prems ls)
  also have " = concat (map (sorted_list_of_set  A) (sorted_list_of_set {..<k})) @ sorted_list_of_set (A k)"
    using Suc strict_mono_sets_def by fastforce
  also have " = concat (map (sorted_list_of_set  A) (sorted_list_of_set {..<Suc k}))"
    using strict_mono_sets_def by fastforce
  finally show ?case .
qed

lemma sorted_list_of_set_UN_atMost:
  fixes k::nat
  assumes "strict_mono_sets {..k} A" and "i. i  k  finite (A i)"
  shows "sorted_list_of_set (ik. A i) = concat (map (sorted_list_of_set  A) (sorted_list_of_set {..k}))"
  by (metis assms lessThan_Suc_atMost less_Suc_eq_le sorted_list_of_set_UN_lessThan)

subsection ‹Monotonic enumeration of a countably infinite set›

abbreviation "enum  enumerate"

text ‹Could be generalised to infinite countable sets of any type›
lemma nat_infinite_iff:
  fixes N :: "nat set"
  shows "infinite N  (f::natnat. N = range f  strict_mono f)"
proof safe
  assume "infinite N"
  then show "f. N = range (f::nat  nat)  strict_mono f"
    by (metis bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_mono_def)
next
  fix f :: "nat  nat"
  assume "strict_mono f" and "N = range f" and "finite (range f)"
  then show False
    using range_inj_infinite strict_mono_imp_inj_on by blast
qed

lemma enum_works:
  fixes N :: "nat set"
  assumes "infinite N"
  shows "N = range (enum N)  strict_mono (enum N)"
  by (metis assms bij_betw_imp_surj_on bij_enumerate enumerate_mono strict_monoI)

lemma range_enum: "range (enum N) = N" and strict_mono_enum: "strict_mono (enum N)"
  if "infinite N" for N :: "nat set"
  using enum_works [OF that] by auto

lemma enum_0_eq_Inf:
  fixes N :: "nat set"
  assumes "infinite N"
  shows "enum N 0 = Inf N"
proof -
  have "enum N 0  N"
    using assms range_enum by auto
  moreover have "x. x  N  enum N 0  x"
    by (metis (mono_tags, opaque_lifting) assms imageE le0 less_mono_imp_le_mono range_enum strict_monoD strict_mono_enum)
  ultimately show ?thesis
    by (metis cInf_eq_minimum)
qed

lemma enum_works_finite:
  fixes N :: "nat set"
  assumes "finite N"
  shows "N = enum N ` {..<card N}  strict_mono_on {..<card N} (enum N)"
  using assms
  by (metis bij_betw_imp_surj_on finite_bij_enumerate finite_enumerate_mono lessThan_iff strict_mono_onI)

lemma enum_obtain_index_finite:
  fixes N :: "nat set"
  assumes "x  N" "finite N" 
  obtains i where "i < card N" "x = enum N i"
  by (metis x  N finite N enum_works_finite imageE lessThan_iff)

lemma enum_0_eq_Inf_finite:
  fixes N :: "nat set"
  assumes "finite N" "N  {}"
  shows "enum N 0 = Inf N"
proof -
  have "enum N 0  N"
    by (metis Nat.neq0_conv assms empty_is_image enum_works_finite image_eqI lessThan_empty_iff lessThan_iff)
  moreover have "enum N 0  x" if "x  N" for x
  proof -
    obtain i where "i < card N" "x = enum N i"
      by (metis x  N finite N enum_obtain_index_finite)
    with assms show ?thesis
      by (metis Nat.neq0_conv finite_enumerate_mono less_or_eq_imp_le)
  qed
  ultimately show ?thesis
    by (metis cInf_eq_minimum)
qed

lemma greaterThan_less_enum:
  fixes N :: "nat set"
  assumes "N  {x<..}" "infinite N"
  shows "x < enum N i"
  using assms range_enum by fastforce

lemma atLeast_le_enum:
  fixes N :: "nat set"
  assumes "N  {x..}" "infinite N"
  shows "x  enum N i"
  using assms range_enum by fastforce

lemma less_sets_empty1 [simp]: "less_sets {} A" and less_sets_empty2 [simp]: "less_sets A {}"
  by (simp_all add: less_sets_def)

lemma less_sets_singleton1 [simp]: "less_sets {a} A  (xA. a < x)" 
  and less_sets_singleton2 [simp]: "less_sets A {a}  (xA. x < a)"
  by (simp_all add: less_sets_def)

lemma less_sets_atMost [simp]: "less_sets {..a} A  (xA. a < x)" 
  and less_sets_alLeast [simp]: "less_sets A {a..}  (xA. x < a)"
  by (auto simp: less_sets_def)

lemma less_sets_imp_strict_mono_sets:
  assumes "i. less_sets (A i) (A (Suc i))" "i. i>0  A i  {}"
  shows "strict_mono_sets UNIV A"
proof (clarsimp simp: strict_mono_sets_def)
  fix i j::nat
  assume "i < j"
  then show "less_sets (A i) (A j)"
  proof (induction "j-i" arbitrary: i j)
    case (Suc x)
    then show ?case
      by (metis Suc_diff_Suc Suc_inject Suc_mono assms less_Suc_eq less_sets_trans zero_less_Suc)
  qed auto
qed

lemma less_sets_Suc_Max:  
  assumes "finite A"
  shows "less_sets A {Suc (Max A)..}"
proof (cases "A = {}")
  case False
  then show ?thesis
    by (simp add: assms less_Suc_eq_le)
qed auto

lemma infinite_nat_greaterThan:
  fixes m::nat
  assumes "infinite N"
  shows "infinite (N  {m<..})"
proof -
  have "N  -{m<..}  (N  {m<..})"
    by blast
  moreover have "finite (-{m<..})"
    by simp
  ultimately show ?thesis
    using assms finite_subset by blast
qed

end