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 ∧ i≠x) = (LEAST i. i ∈ S)"
  proof (rule Least_equality)
    have "∃t. t ∈ S ∧ t≠x"
      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 ∧ s≠x ∧ 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 ≡ ∀x∈A. ∀y∈A. 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 (⋃i≤k. 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::nat⇒nat. 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 ⟷ (∀x∈A. a < x)" 
  and less_sets_singleton2 [simp]: "less_sets A {a} ⟷ (∀x∈A. x < a)"
  by (simp_all add: less_sets_def)

lemma less_sets_atMost [simp]: "less_sets {..a} A ⟷ (∀x∈A. a < x)" 
  and less_sets_alLeast [simp]: "less_sets A {a..} ⟷ (∀x∈A. 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