Theory Omega_Omega

section ‹An ordinal partition theorem by Jean A. Larson›

text ‹Jean A. Larson,
     A short proof of a partition theorem for the ordinal $\omega^\omega$.
     \emph{Annals of Mathematical Logic}, 6:129--145, 1973.›

theory Omega_Omega
  imports "HOL-Library.Product_Lexorder" Erdos_Milner

begin

abbreviation "list_of ≡ sorted_list_of_set"

subsection ‹Cantor normal form for ordinals below @{term "ω↑ω"}›

text ‹Unlike @{term Cantor_sum}, there is no list of ordinal exponents,
which are instead taken as consecutive. We obtain an order-isomorphism between @{term "ω↑ω"}
and increasing lists of natural numbers (ordered lexicographically).›

fun omega_sum_aux  where
  Nil: "omega_sum_aux 0 _ = 0"
| Suc: "omega_sum_aux (Suc n) [] = 0"
| Cons: "omega_sum_aux (Suc n) (m#ms) = (ω↑n) * (ord_of_nat m) + omega_sum_aux n ms"

abbreviation omega_sum where "omega_sum ms ≡ omega_sum_aux (length ms) ms"

text ‹A normal expansion has no leading zeroes›
inductive normal:: "nat list ⇒ bool" where
  normal_Nil[iff]: "normal []"
| normal_Cons:     "m > 0 ⟹ normal (m#ms)"

inductive_simps normal_Cons_iff [simp]: "normal (m#ms)"

lemma omega_sum_0_iff [simp]: "normal ns ⟹ omega_sum ns = 0 ⟷ ns = []"
  by (induction ns rule: normal.induct) auto

lemma Ord_omega_sum_aux [simp]: "Ord (omega_sum_aux k ms)"
  by (induction rule: omega_sum_aux.induct) auto

lemma Ord_omega_sum: "Ord (omega_sum ms)"
  by simp

lemma omega_sum_less_ωω [intro]: "omega_sum ms < ω↑ω"
proof (induction ms)
  case (Cons m ms)
  have "ω ↑ (length ms) * ord_of_nat m ∈ elts (ω ↑ Suc (length ms))"
    using Ord_mem_iff_lt by auto
  then have "ω↑(length ms) * ord_of_nat m ∈ elts (ω↑ω)"
    using Ord_ord_of_nat oexp_mono_le omega_nonzero ord_of_nat_le_omega by blast
  with Cons show ?case
    by (auto simp: mult_succ OrdmemD oexp_less indecomposableD indecomposable_ω_power)
qed (auto simp: zero_less_Limit)

lemma omega_sum_aux_less: "omega_sum_aux k ms < ω ↑ k"
proof (induction rule: omega_sum_aux.induct)
  case (3 n m ms)
  have " ω↑n * ord_of_nat m + ω↑n < ω↑n * ω"
    by (metis Ord_ord_of_nat ω_power_succ_gtr mult_succ oexp_succ ord_of_nat.simps(2))
  with 3 show ?case
    using dual_order.strict_trans by force
qed auto

lemma omega_sum_less: "omega_sum ms < ω ↑ (length ms)"
  by (rule omega_sum_aux_less)

lemma omega_sum_ge: "m ≠ 0 ⟹ ω ↑ (length ms) ≤ omega_sum (m#ms)"
  apply clarsimp
  by (metis Ord_ord_of_nat add_le_cancel_left0 le_mult Nat.neq0_conv ord_of_eq_0_iff vsubsetD)

lemma omega_sum_length_less:
  assumes "normal ns" "length ms < length ns"
  shows "omega_sum ms < omega_sum ns"
  using assms
proof (induction rule: normal.induct)
  case (normal_Cons n ns')
  have "ω ↑ length ms ≤ ω ↑ length ns'"
    using normal_Cons oexp_mono_le by auto
  then show ?case
    by (metis gr_implies_not_zero less_le_trans normal_Cons.hyps omega_sum_aux_less omega_sum_ge)
qed auto

lemma omega_sum_length_leD:
  assumes "omega_sum ms ≤ omega_sum ns" "normal ms"
  shows "length ms ≤ length ns"
  by (meson assms leD leI omega_sum_length_less)

lemma omega_sum_less_eqlen_iff_cases [simp]:
  assumes "length ms = length ns"
   shows "omega_sum (m#ms) < omega_sum (n#ns) ⟷ m<n ∨ m=n ∧ omega_sum ms < omega_sum ns"
  using omega_sum_less [of ms] omega_sum_less [of ns]
  by (metis Kirby.add_less_cancel_left Omega_Omega.Cons Ord_ω Ord_oexp Ord_omega_sum Ord_ord_of_nat assms length_Cons linorder_neqE_nat mult_nat_less_add_less order_less_asym)

lemma omega_sum_less_iff_cases:
  assumes "m > 0" "n > 0"
  shows "omega_sum (m#ms) < omega_sum (n#ns)
          ⟷ length ms < length ns
            ∨ length ms = length ns ∧ m<n
            ∨ length ms = length ns ∧ m=n ∧ omega_sum ms < omega_sum ns"
  by (smt (verit) assms length_Cons less_eq_Suc_le less_le_not_le nat_less_le normal_Cons not_le 
      omega_sum_length_less omega_sum_less_eqlen_iff_cases)

lemma omega_sum_less_iff:
  "((length ms, omega_sum ms), (length ns, omega_sum ns)) ∈ less_than <*lex*> VWF
   ⟷ (ms,ns) ∈ lenlex less_than"
proof (induction ms arbitrary: ns)
  case (Cons m ms)
  then show ?case
  proof (induction ns)
    case (Cons n ns')
    show ?case
      using Cons.prems Cons_lenlex_iff omega_sum_less_eqlen_iff_cases by fastforce
  qed auto
qed auto

lemma eq_omega_sum_less_iff:
  assumes "length ms = length ns"
  shows "(omega_sum ms, omega_sum ns) ∈ VWF ⟷ (ms,ns) ∈ lenlex less_than"
  by (metis assms in_lex_prod less_not_refl less_than_iff omega_sum_less_iff)

lemma eq_omega_sum_eq_iff:
  assumes "length ms = length ns"
  shows "omega_sum ms = omega_sum ns ⟷ ms=ns"
proof
  assume "omega_sum ms = omega_sum ns"
  then have "(omega_sum ms, omega_sum ns) ∉ VWF" "(omega_sum ns, omega_sum ms) ∉ VWF"
    by auto
  then obtain "(ms,ns) ∉ lenlex less_than" "(ns,ms) ∉ lenlex less_than"
    using assms eq_omega_sum_less_iff by metis
  moreover have "total (lenlex less_than)"
    by (simp add: total_lenlex total_less_than)
  ultimately show "ms=ns"
    by (meson UNIV_I total_on_def)
qed auto

lemma inj_omega_sum: "inj_on omega_sum {l. length l = n}"
  unfolding inj_on_def using eq_omega_sum_eq_iff by fastforce

lemma Ex_omega_sum: "γ ∈ elts (ω↑n) ⟹ ∃ns. γ = omega_sum ns ∧ length ns = n"
proof (induction n arbitrary: γ)
  case 0
  then show ?case
    by (rule_tac x="[]" in exI) auto
next
  case (Suc n)
  then obtain k::nat where k: "γ ∈ elts (ω ↑ n * k)"
       and kmin: "⋀k'. k'<k ⟹ γ ∉ elts (ω ↑ n * k')"
    by (metis Ord_ord_of_nat elts_mult_ωE oexp_succ ord_of_nat.simps(2))
  show ?case
  proof (cases k)
    case (Suc k')
    then obtain δ where δ: "γ = (ω ↑ n * k') + δ"
      by (metis lessI mult_succ ord_of_nat.simps(2) k kmin mem_plus_V_E)
    then have δin: "δ ∈ elts (ω ↑ n)"
      using Suc k mult_succ by auto
    then obtain ns where ns: "δ = omega_sum ns" and len: "length ns = n"
      using Suc.IH by auto
    moreover have "omega_sum ns < ω↑n"
      using OrdmemD ns δin by auto
    ultimately show ?thesis
      by (rule_tac x="k'#ns" in exI) (simp add: δ)
  qed (use k in auto)
qed

lemma omega_sum_drop [simp]: "omega_sum (dropWhile (λn. n=0) ns) = omega_sum ns"
  by (induction ns) auto

lemma normal_drop [simp]: "normal (dropWhile (λn. n=0) ns)"
  by (induction ns) auto

lemma omega_sum_ωω:
  assumes "γ ∈ elts (ω↑ω)"
  obtains ns where "γ = omega_sum ns" "normal ns"
proof -
  obtain ms where "γ = omega_sum ms"
    using assms Ex_omega_sum by (auto simp: oexp_Limit elts_ω)
  then show thesis
    by (metis normal_drop omega_sum_drop that)
qed

definition Cantor_ωω :: "V ⇒ nat list"
  where "Cantor_ωω ≡ λx. SOME ns. x = omega_sum ns ∧ normal ns"

lemma
  assumes "γ ∈ elts (ω↑ω)"
  shows Cantor_ωω: "omega_sum (Cantor_ωω γ) = γ"
    and normal_Cantor_ωω: "normal (Cantor_ωω γ)"
  by (metis (mono_tags, lifting) Cantor_ωω_def assms omega_sum_ωω someI)+


subsection ‹Larson's set $W(n)$›

definition WW :: "nat list set"
  where "WW ≡ {l. strict_sorted l}"

fun into_WW :: "nat ⇒ nat list ⇒ nat list" where
  "into_WW k [] = []"
| "into_WW k (n#ns) = (k+n) # into_WW (Suc (k+n)) ns"

fun from_WW :: "nat ⇒ nat list ⇒ nat list" where
  "from_WW k [] = []"
| "from_WW k (n#ns) = (n - k) # from_WW (Suc n) ns"

lemma from_into_WW [simp]: "from_WW k (into_WW k ns) = ns"
  by (induction ns arbitrary: k) auto

lemma inj_into_WW: "inj (into_WW k)"
  by (metis from_into_WW injI)

lemma into_from_WW_aux:
  "⟦strict_sorted ns; ∀n∈list.set ns. k ≤ n⟧ ⟹ into_WW k (from_WW k ns) = ns"
  by (induction ns arbitrary: k) (auto simp: Suc_leI)

lemma into_from_WW [simp]: "strict_sorted ns ⟹ into_WW 0 (from_WW 0 ns) = ns"
  by (simp add: into_from_WW_aux)

lemma into_WW_imp_ge: "y ∈ List.set (into_WW x ns) ⟹ x ≤ y"
  by (induction ns arbitrary: x) fastforce+

lemma strict_sorted_into_WW: "strict_sorted (into_WW x ns)"
  by (induction ns arbitrary: x) (auto simp: dest: into_WW_imp_ge)

lemma length_into_WW: "length (into_WW x ns) = length ns"
  by (induction ns arbitrary: x) auto

lemma WW_eq_range_into: "WW = range (into_WW 0)"
proof -
  have "⋀ns. strict_sorted ns ⟹ ns ∈ range (into_WW 0)"
    by (metis into_from_WW rangeI)
  then show ?thesis by (auto simp: WW_def strict_sorted_into_WW)
qed

lemma into_WW_lenlex_iff: "(into_WW k ms, into_WW k ns) ∈ lenlex less_than ⟷ (ms, ns) ∈ lenlex less_than"
proof (induction ms arbitrary: ns k)
  case Nil
  then show ?case
    by simp (metis length_0_conv length_into_WW)
next
  case (Cons m ms)
  then show ?case
    by (induction ns) (auto simp: Cons_lenlex_iff length_into_WW)
qed

lemma wf_llt [simp]: "wf (lenlex less_than)" and trans_llt [simp]: "trans (lenlex less_than)"
  by blast+

lemma total_llt [simp]: "total_on A (lenlex less_than)"
  by (meson UNIV_I total_lenlex total_less_than total_on_def)

lemma omega_sum_1_less:
  assumes "(ms,ns) ∈ lenlex less_than" shows "omega_sum (1#ms) < omega_sum (1#ns)"
proof -
  have "omega_sum (1#ms) < omega_sum (1#ns)" if "length ms < length ns"
    using omega_sum_less_iff_cases that zero_less_one by blast
  then show ?thesis
    using assms by (auto simp: mult_succ simp flip: omega_sum_less_iff)
qed

lemma ordertype_WW_1: "ordertype WW (lenlex less_than) ≤ ordertype UNIV (lenlex less_than)"
  by (rule ordertype_mono) auto

lemma ordertype_WW_2: "ordertype UNIV (lenlex less_than) ≤ ω↑ω"
proof (rule ordertype_inc_le_Ord)
  show "range (λms. omega_sum (1#ms)) ⊆ elts (ω↑ω)"
    by (meson Ord_ω Ord_mem_iff_lt Ord_oexp Ord_omega_sum image_subset_iff omega_sum_less_ωω)
qed (use omega_sum_1_less in auto)

lemma ordertype_WW_3: "ω↑ω ≤ ordertype WW (lenlex less_than)"
proof -
  define π where "π ≡ into_WW 0 ∘ Cantor_ωω"
  have ωω: "ω↑ω = tp (elts (ω↑ω))"
    by simp
  also have "… ≤ ordertype WW (lenlex less_than)"
  proof (rule ordertype_inc_le)
    fix α β
    assume α: "α ∈ elts (ω↑ω)" and β: "β ∈ elts (ω↑ω)" and "(α, β) ∈ VWF"
    then obtain *: "Ord α" "Ord β" "α<β"
      by (metis Ord_in_Ord Ord_ordertype VWF_iff_Ord_less ωω)
    then have "length (Cantor_ωω α) ≤ length (Cantor_ωω β)"
      using α β by (simp add: Cantor_ωω normal_Cantor_ωω omega_sum_length_leD)
    with α β * have "(Cantor_ωω α, Cantor_ωω β) ∈ lenlex less_than"
      by (auto simp: Cantor_ωω simp flip: omega_sum_less_iff)
    then show "(π α, π β) ∈ lenlex less_than"
      by (simp add: π_def into_WW_lenlex_iff)
  qed (auto simp: π_def WW_def strict_sorted_into_WW)
  finally show "ω↑ω ≤ ordertype WW (lenlex less_than)" .
qed

lemma ordertype_WW: "ordertype WW (lenlex less_than) = ω↑ω"
  and ordertype_UNIV_ωω: "ordertype UNIV (lenlex less_than) = ω↑ω"
  using ordertype_WW_1 ordertype_WW_2 ordertype_WW_3 by auto


lemma ordertype_ωω:
  fixes F :: "nat ⇒ nat list set"
  assumes "⋀j::nat. ordertype (F j) (lenlex less_than) = ω↑j"
  shows "ordertype (⋃j. F j) (lenlex less_than) = ω↑ω"
proof (rule antisym)
  show "ordertype (⋃ (range F)) (lenlex less_than) ≤ ω ↑ ω"
    by (metis ordertype_UNIV_ωω ordertype_mono small top_greatest trans_llt wf_llt)
  have "⋀n. ω ↑ ord_of_nat n ≤ ordertype (⋃ (range F)) (lenlex less_than)"
    by (metis TC_small Union_upper assms ordertype_mono rangeI trans_llt wf_llt)
  then show "ω ↑ ω ≤ ordertype (⋃ (range F)) (lenlex less_than)"
    by (auto simp: oexp_ω_Limit ZFC_in_HOL.SUP_le_iff elts_ω)
qed



definition WW_seg :: "nat ⇒ nat list set"
  where "WW_seg n ≡ {l ∈ WW. length l = n}"

lemma WW_seg_subset_WW: "WW_seg n ⊆ WW"
  by (auto simp: WW_seg_def)

lemma WW_eq_UN_WW_seg: "WW = (⋃ n. WW_seg n)"
  by (auto simp: WW_seg_def)

lemma ordertype_list_seg: "ordertype {l. length l = n} (lenlex less_than) = ω↑n"
proof -
  have "bij_betw omega_sum {l. length l = n} (elts (ω↑n))"
    unfolding WW_seg_def bij_betw_def
    by (auto simp: inj_omega_sum Ord_mem_iff_lt omega_sum_less dest: Ex_omega_sum)
  then show ?thesis
    by (force simp: ordertype_eq_iff simp flip: eq_omega_sum_less_iff)
qed

lemma ordertype_WW_seg: "ordertype (WW_seg n) (lenlex less_than) = ω↑n"
  (is "ordertype ?W ?R = ω↑n")
proof -
  have "ordertype {l. length l = n} ?R = ordertype ?W ?R"
  proof (subst ordertype_eq_ordertype)
    show "∃f. bij_betw f {l. length l = n} ?W ∧ (∀x∈{l. length l = n}. ∀y∈{l. length l = n}. ((f x, f y) ∈ lenlex less_than) = ((x, y) ∈ lenlex less_than))"
    proof (intro exI conjI)
      have "inj_on (into_WW 0) {l. length l = n}"
        by (metis from_into_WW inj_onI)
      then show "bij_betw (into_WW 0) {l. length l = n} ?W"
        by (auto simp: bij_betw_def WW_seg_def WW_eq_range_into length_into_WW)
    qed (simp add: into_WW_lenlex_iff)
  qed auto
  then show ?thesis
    using ordertype_list_seg by auto
qed


subsection ‹Definitions required for the lemmas›

subsubsection ‹Larson's "$<$"-relation on ordered lists›

instantiation list :: (ord)ord
begin

definition "xs < ys ≡ xs ≠ [] ∧ ys ≠ [] ⟶ last xs < hd ys" for xs ys :: "'a list"
definition "xs ≤ ys ≡ xs < ys ∨ xs = ys" for xs ys :: "'a list"

instance
  by standard

end

lemma less_Nil [simp]: "xs < []" "[] < xs"
  by (auto simp: less_list_def)

lemma less_sets_imp_list_less:
  assumes "list.set xs ≪ list.set ys"
  shows "xs < ys"
  by (metis assms last_in_set less_list_def less_sets_def list.set_sel(1))

lemma less_sets_imp_sorted_list_of_set:
  assumes "A ≪ B" "finite A" "finite B"
  shows "list_of A < list_of B"
  by (simp add: assms less_sets_imp_list_less)

lemma sorted_list_of_set_imp_less_sets:
  assumes "xs < ys" "sorted xs" "sorted ys"
  shows "list.set xs ≪ list.set ys"
  using assms sorted_hd_le sorted_le_last
  by (force simp: less_list_def less_sets_def intro: order.trans)

lemma less_list_iff_less_sets:
  assumes "sorted xs" "sorted ys"
  shows "xs < ys ⟷ list.set xs ≪ list.set ys"
  using assms sorted_hd_le sorted_le_last
  by (force simp: less_list_def less_sets_def intro: order.trans)

lemma strict_sorted_append_iff:
  "strict_sorted (xs @ ys) ⟷ xs < ys ∧ strict_sorted xs ∧ strict_sorted ys"
  by (metis less_list_iff_less_sets less_setsD sorted_wrt_append strict_sorted_imp_less_sets strict_sorted_imp_sorted)

lemma singleton_less_list_iff: "sorted xs ⟹ [n] < xs ⟷ {..n} ∩ list.set xs = {}"
  apply (simp add: less_list_def disjoint_iff)
  by (metis empty_iff less_le_trans list.set(1) list.set_sel(1) not_le sorted_hd_le)

lemma less_hd_imp_less: "xs < [hd ys] ⟹ xs < ys"
  by (simp add: less_list_def)

lemma strict_sorted_concat_I:
  assumes "⋀x. x ∈ list.set xs ⟹ strict_sorted x"
          "⋀n. Suc n < length xs ⟹ xs!n < xs!Suc n"
          "xs ∈ lists (- {[]})"
  shows "strict_sorted (concat xs)"
  using assms
proof (induction xs)
  case (Cons x xs)
  then have "x < concat xs"
    apply (simp add: less_list_def)
    by (metis Compl_iff hd_concat insertI1 length_greater_0_conv length_pos_if_in_set list.sel(1) lists.cases nth_Cons_0)
  with Cons show ?case
    by (force simp: strict_sorted_append_iff)
qed auto


subsection ‹Nash Williams for lists›

subsubsection ‹Thin sets of lists›

inductive initial_segment :: "'a list ⇒ 'a list ⇒ bool"
  where "initial_segment xs (xs@ys)"

definition thin :: "'a list set ⇒ bool"
  where "thin A ≡ ¬ (∃x y. x ∈ A ∧ y ∈ A ∧ x ≠ y ∧ initial_segment x y)"

lemma initial_segment_ne:
  assumes "initial_segment xs ys" "xs ≠ []"
  shows "ys ≠ [] ∧ hd ys = hd xs"
  using assms by (auto elim!: initial_segment.cases)

lemma take_initial_segment:
  assumes "initial_segment xs ys" "k ≤ length xs"
  shows "take k xs = take k ys"
  by (metis append_eq_conv_conj assms initial_segment.cases min_def take_take)

lemma initial_segment_length_eq:
  assumes "initial_segment xs ys" "length xs = length ys"
  shows "xs = ys"
  using assms initial_segment.cases by fastforce

lemma initial_segment_Nil [simp]: "initial_segment [] ys"
  by (simp add: initial_segment.simps)

lemma initial_segment_Cons [simp]: "initial_segment (x#xs) (y#ys) ⟷ x=y ∧ initial_segment xs ys"
  by (metis append_Cons initial_segment.simps list.inject)

lemma init_segment_iff_initial_segment:
  assumes "strict_sorted xs" "strict_sorted ys"
  shows "init_segment (list.set xs) (list.set ys) ⟷ initial_segment xs ys" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain S' where S': "list.set ys = list.set xs ∪ S'" "list.set xs ≪ S'"
    by (auto simp: init_segment_def)
  then have "finite S'"
    by (metis List.finite_set finite_Un)
  have "ys = xs @ list_of S'"
    using S' ‹strict_sorted xs›
  proof (induction xs)
    case Nil
    with ‹strict_sorted ys› show ?case
      by auto
  next
    case (Cons a xs)
    with ‹finite S'› have "ys = a # xs @ list_of S'"
      by (metis List.finite_set append_Cons assms(2) sorted_list_of_set_Un sorted_list_of_set_set_of)
    then show ?case
      by (auto simp: Cons)
  qed
  then show ?rhs
    using initial_segment.intros by blast
next
  assume ?rhs
  then show ?lhs
  proof cases
    case (1 ys)
    with assms show ?thesis
      by (simp add: init_segment_Un strict_sorted_imp_less_sets)
  qed
qed

theorem Nash_Williams_WW:
  fixes h :: "nat list ⇒ nat"
  assumes "infinite M" and h: "h ` {l ∈ A. List.set l ⊆ M} ⊆ {..<2}" and "thin A" "A ⊆ WW"
  obtains i N where "i < 2" "infinite N" "N ⊆ M" "h ` {l ∈ A. List.set l ⊆ N} ⊆ {i}"
proof -
  define AM where "AM ≡ {l ∈ A. List.set l ⊆ M}"
  have "thin_set (list.set ` A)"
    using ‹thin A› ‹A ⊆ WW› unfolding thin_def thin_set_def WW_def
    by (auto simp: subset_iff init_segment_iff_initial_segment)
  then have "thin_set (list.set ` AM)"
    by (simp add: AM_def image_subset_iff thin_set_def)
  then have "Ramsey (list.set ` AM) 2"
    using Nash_Williams_2 by metis
  moreover have "(h ∘ list_of) ∈ list.set ` AM → {..<2}"
    unfolding AM_def
  proof clarsimp
    fix l
    assume "l ∈ A" "list.set l ⊆ M"
    then have "strict_sorted l"
      using WW_def ‹A ⊆ WW› by blast
    then show "h (list_of (list.set l)) < 2"
      using h ‹l ∈ A› ‹list.set l ⊆ M› by auto
  qed
  ultimately obtain N i where N: "N ⊆ M" "infinite N" "i<2" 
              and "list.set ` AM ∩ Pow N ⊆ (h ∘ list_of) -` {i}"
    unfolding Ramsey_eq by (metis ‹infinite M›)
  then have N_disjoint: "(h ∘ list_of) -` {1-i} ∩ (list.set ` AM) ∩ Pow N = {}"
    unfolding subset_vimage_iff less_2_cases_iff by force
  have "h ` {l ∈ A. list.set l ⊆ N} ⊆ {i}"
  proof clarify
    fix l
    assume "l ∈ A" and "list.set l ⊆ N"
    then have "h l < 2"
      using h ‹N ⊆ M› by force
    with ‹i<2› have "h l ≠ Suc 0 - i ⟹ h l = i"
      by (auto simp: eval_nat_numeral less_Suc_eq)
    moreover have "strict_sorted l"
      using ‹A ⊆ WW› ‹l ∈ A› unfolding WW_def by blast
    moreover have "h (list_of (list.set l)) = 1 - i ⟶ ¬ (list.set l ⊆ N)"
      using N_disjoint ‹N ⊆ M› ‹l ∈ A› by (auto simp: AM_def)
    ultimately show "h l = i"
      using N ‹N ⊆ M› ‹l ∈ A› ‹list.set l ⊆ N›
      by (auto simp: vimage_def set_eq_iff AM_def WW_def subset_iff)
  qed
  then show thesis
    using that ‹i<2› N by auto
qed

subsection ‹Specialised functions on lists›

lemma mem_lists_non_Nil: "xss ∈ lists (- {[]}) ⟷ (∀x ∈ list.set xss. x ≠ [])"
  by auto

fun acc_lengths :: "nat ⇒ 'a list list ⇒ nat list"
  where "acc_lengths acc [] = []"
      | "acc_lengths acc (l#ls) = (acc + length l) # acc_lengths (acc + length l) ls"

lemma length_acc_lengths [simp]: "length (acc_lengths acc ls) = length ls"
  by (induction ls arbitrary: acc) auto

lemma acc_lengths_eq_Nil_iff [simp]: "acc_lengths acc ls = [] ⟷ ls = []"
  by (metis length_0_conv length_acc_lengths)

lemma set_acc_lengths:
  assumes "ls ∈ lists (- {[]})" shows "list.set (acc_lengths acc ls) ⊆ {acc<..}"
  using assms by (induction ls rule: acc_lengths.induct) fastforce+

text ‹Useful because @{text acc_lengths.simps} will sometimes be deleted from the simpset.›
lemma hd_acc_lengths [simp]: "hd (acc_lengths acc (l#ls)) = acc + length l"
  by simp

lemma last_acc_lengths [simp]:
  "ls ≠ [] ⟹ last (acc_lengths acc ls) = acc + sum_list (map length ls)"
by (induction acc ls rule: acc_lengths.induct) auto

lemma nth_acc_lengths [simp]:
  "⟦ls ≠ []; k < length ls⟧ ⟹ acc_lengths acc ls ! k = acc + sum_list (map length (take (Suc k) ls))"
  by (induction acc ls arbitrary: k rule: acc_lengths.induct) (fastforce simp: less_Suc_eq nth_Cons')+

lemma acc_lengths_plus: "acc_lengths (m+n) as = map ((+)m) (acc_lengths n as)"
  by (induction n as arbitrary: m rule: acc_lengths.induct) (auto simp: add.assoc)

lemma acc_lengths_shift: "NO_MATCH 0 acc ⟹ acc_lengths acc as = map ((+)acc) (acc_lengths 0 as)"
  by (metis acc_lengths_plus add.comm_neutral)

lemma length_concat_acc_lengths:
  "ls ≠ [] ⟹ k + length (concat ls) ∈ list.set (acc_lengths k ls)"
  by (metis acc_lengths_eq_Nil_iff last_acc_lengths last_in_set length_concat)

lemma strict_sorted_acc_lengths:
  assumes "ls ∈ lists (- {[]})" shows "strict_sorted (acc_lengths acc ls)"
  using assms
proof (induction ls rule: acc_lengths.induct)
  case (2 acc l ls)
  then have "strict_sorted (acc_lengths (acc + length l) ls)"
    by auto
  then show ?case
    using set_acc_lengths "2.prems" by auto
qed auto

lemma acc_lengths_append:
  "acc_lengths acc (xs @ ys)
   = acc_lengths acc xs @ acc_lengths (acc + sum_list (map length xs)) ys"
by (induction acc xs rule: acc_lengths.induct) (auto simp: add.assoc)


lemma length_concat_ge:
  assumes "as ∈ lists (- {[]})"
  shows "length (concat as) ≥ length as"
  using assms
proof (induction as)
  case (Cons a as)
  then have "length a ≥ Suc 0" "⋀l. l ∈ list.set as ⟹ length l ≥ Suc 0"
    by (auto simp: Suc_leI)
  then show ?case
    using Cons.IH by force
qed auto


fun interact :: "'a list list ⇒ 'a list list ⇒ 'a list"
  where
  "interact [] ys = concat ys"
| "interact xs [] = concat xs"
| "interact (x#xs) (y#ys) = x @ y @ interact xs ys"

lemma (in monoid_add) length_interact:
  "length (interact xs ys) = sum_list (map length xs) + sum_list (map length ys)"
  by (induction rule: interact.induct) (auto simp: length_concat)

lemma length_interact_ge:
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "length (interact xs ys) ≥ length xs + length ys"
  by (metis add_mono assms length_concat length_concat_ge length_interact)

lemma set_interact [simp]:
  shows "list.set (interact xs ys) = list.set (concat xs) ∪ list.set (concat ys)"
by (induction rule: interact.induct) auto

lemma interact_eq_Nil_iff [simp]:
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "interact xs ys = [] ⟷ xs=[] ∧ ys=[]"
  using length_interact_ge [OF assms]  by fastforce

lemma interact_sing [simp]: "interact [x] ys = x @ concat ys"
  by (metis (no_types) concat.simps(2) interact.simps neq_Nil_conv)

lemma hd_interact: "⟦xs ≠ []; hd xs ≠ []⟧ ⟹ hd (interact xs ys) = hd (hd xs)"
  by (smt (verit, best) hd_append2 hd_concat interact.elims list.sel(1))

lemma acc_lengths_concat_injective:
  assumes "concat as' = concat as" "acc_lengths n as' = acc_lengths n as"
  shows "as' = as"
  using assms
proof (induction as arbitrary: n as')
  case Nil
  then show ?case
    by (metis acc_lengths_eq_Nil_iff)
next
  case (Cons a as)
  then obtain a' bs where "as' = a'#bs"
    by (metis Suc_length_conv length_acc_lengths)
  with Cons show ?case
    by simp
qed

lemma acc_lengths_interact_injective:
  assumes "interact as' bs' = interact as bs" "acc_lengths a as' = acc_lengths a as" "acc_lengths b bs' = acc_lengths b bs"
  shows "as' = as ∧ bs' = bs"
  using assms
proof (induction as bs arbitrary: a b as' bs' rule: interact.induct)
  case (1 cs) then show ?case
    by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(1))
next
  case (2 c cs)
  then show ?case
    by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(2) list.exhaust)
next
  case (3 x xs y ys) 
  then obtain a' us b' vs where "as' = a'#us" "bs' = b'#vs"
    by (metis length_Suc_conv length_acc_lengths)
  with 3 show ?case
    by auto
qed


lemma strict_sorted_interact_I:
  assumes "length ys ≤ length xs" "length xs ≤ Suc (length ys)"
    "⋀x. x ∈ list.set xs ⟹ strict_sorted x"
    "⋀y. y ∈ list.set ys ⟹ strict_sorted y"
    "⋀n. n < length ys ⟹ xs!n < ys!n"
    "⋀n. Suc n < length xs ⟹ ys!n < xs!Suc n"
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "strict_sorted (interact xs ys)"
  using assms
proof (induction rule: interact.induct)
  case (3 x xs y ys)
  then have "x < y"
    by force
  moreover have "strict_sorted (interact xs ys)"
    using 3 by simp (metis Suc_less_eq nth_Cons_Suc)
  moreover have "y < interact xs ys"
    using 3 apply (simp add: less_list_def)
    by (metis hd_interact le_zero_eq length_greater_0_conv list.sel(1) list.set_sel(1) list.size(3) lists.simps mem_lists_non_Nil nth_Cons_0)
  ultimately show ?case
    using 3 by (simp add: strict_sorted_append_iff less_list_def)
qed auto


subsection ‹Forms and interactions›

subsubsection ‹Forms›

inductive Form_Body :: "[nat, nat, nat list, nat list, nat list] ⇒ bool"
  where "Form_Body ka kb xs ys zs"
  if "length xs < length ys" "xs = concat (a#as)" "ys = concat (b#bs)"
          "a#as ∈ lists (- {[]})" "b#bs ∈ lists (- {[]})"
          "length (a#as) = ka" "length (b#bs) = kb"
          "c = acc_lengths 0 (a#as)"
          "d = acc_lengths 0 (b#bs)"
          "zs = concat [c, a, d, b] @ interact as bs"
          "strict_sorted zs"


inductive Form :: "[nat, nat list set] ⇒ bool"
  where "Form 0 {xs,ys}" if "length xs = length ys" "xs ≠ ys"
      | "Form (2*k-1) {xs,ys}" if "Form_Body k k xs ys zs" "k > 0"
      | "Form (2*k)   {xs,ys}" if "Form_Body (Suc k) k xs ys zs" "k > 0"

inductive_cases Form_0_cases_raw: "Form 0 u"

lemma Form_elim_upair:
  assumes "Form l U"
  obtains xs ys where "xs ≠ ys" "U = {xs,ys}" "length xs ≤ length ys"
  using assms
  by (smt (verit, best) Form.simps Form_Body.cases less_or_eq_imp_le nat_neq_iff)


lemma assumes "Form_Body ka kb xs ys zs"
  shows Form_Body_WW: "zs ∈ WW" 
    and Form_Body_nonempty: "length zs > 0" 
    and Form_Body_length: "length xs < length ys"
  using Form_Body.cases [OF assms] by (fastforce simp: WW_def)+

lemma form_cases:
  fixes l::nat
  obtains (zero) "l = 0" | (nz) ka kb where "l = ka+kb - 1" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
proof -
  have "l = 0 ∨ (∃ka kb. l = ka+kb - 1 ∧ 0 < kb ∧ kb ≤ ka ∧ ka ≤ Suc kb)"
    by presburger
  then show thesis
    using nz zero by blast
qed

subsubsection ‹Interactions›

lemma interact:
  assumes "Form l U" "l>0"
  obtains ka kb xs ys zs where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys zs" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  using assms
  unfolding Form.simps
  by (smt (verit, best) add_Suc diff_Suc_1 lessI mult_2 nat_less_le order_refl)


definition inter_scheme :: "nat ⇒ nat list set ⇒ nat list"
  where "inter_scheme l U ≡ 
          SOME zs. ∃k xs ys. U = {xs,ys} ∧ 
            (l = 2*k-1 ∧ Form_Body k k xs ys zs ∨ l = 2*k ∧ Form_Body (Suc k) k xs ys zs)"


lemma inter_scheme:
  assumes "Form l U" "l>0"
  obtains ka kb xs ys where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys (inter_scheme l U)" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  using interact [OF ‹Form l U›]
proof cases
  case (2 ka kb xs ys zs)
  then have §: "⋀ka kb zs. ¬ Form_Body ka kb ys xs zs"
    using Form_Body_length less_asym' by blast
  have "Form_Body ka kb xs ys (inter_scheme l U)"
  proof (cases "ka = kb")
    case True 
    with 2 have l: "∀k. l ≠ k * 2"
      by presburger
    have [simp]: "⋀k. kb + kb - Suc 0 = k * 2 - Suc 0 ⟷ k=kb"
      by auto
    show ?thesis
      unfolding inter_scheme_def using 2 l True
      by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex)
  next
    case False
    with 2 have l: "∀k. l ≠ k * 2 - Suc 0" and [simp]: "ka = Suc kb"
      by presburger+
    have [simp]: "⋀k. kb + kb = k * 2 ⟷ k=kb"
      by auto
    show ?thesis
      unfolding inter_scheme_def using 2 l False
      by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex)
  qed
  then show ?thesis
    by (simp add: 2 that)
qed (use ‹l > 0› in auto)

lemma inter_scheme_strict_sorted:
  assumes "Form l U" "l>0"
  shows "strict_sorted (inter_scheme l U)"
  using Form_Body.simps assms inter_scheme by fastforce

lemma inter_scheme_simple:
  assumes "Form l U" "l>0"
  shows "inter_scheme l U ∈ WW ∧ length (inter_scheme l U) > 0"
  using inter_scheme [OF assms] by (meson Form_Body_WW Form_Body_nonempty)

subsubsection ‹Injectivity of interactions›

proposition inter_scheme_injective:
  assumes "Form l U" "Form l U'" "l > 0" and eq: "inter_scheme l U' = inter_scheme l U"
  shows "U' = U"
proof -
  obtain ka kb xs ys 
    where l: "l = ka+kb - 1" and U: "U = {xs,ys}" 
      and FB: "Form_Body ka kb xs ys (inter_scheme l U)" 
      and kb: "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
    using assms inter_scheme by blast
  then obtain a as b bs c d
    where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)"
      and len: "length (a#as) = ka" "length (b#bs) = kb"
      and c: "c = acc_lengths 0 (a#as)"
      and d: "d = acc_lengths 0 (b#bs)"
      and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs"
    by (auto simp: Form_Body.simps)
  obtain ka' kb' xs' ys' 
    where l': "l = ka'+kb' - 1" and U': "U' = {xs',ys'}" 
      and FB': "Form_Body ka' kb' xs' ys' (inter_scheme l U')" 
      and kb': "0 < kb'" "kb' ≤ ka'" "ka' ≤ Suc kb'"
    using assms inter_scheme by blast
  then obtain a' as' b' bs' c' d'
    where xs': "xs' = concat (a'#as')" and ys': "ys' = concat (b'#bs')"
      and len': "length (a'#as') = ka'" "length (b'#bs') = kb'"
      and c': "c' = acc_lengths 0 (a'#as')"
      and d': "d' = acc_lengths 0 (b'#bs')"
      and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'"
    using Form_Body.simps by auto
  have [simp]: "ka' = ka ∧ kb' = kb"
    using ‹l > 0› l l' kb kb' le_SucE le_antisym mult_2 by linarith 
  have [simp]: "length c = length c'" "length d = length d'"
    using c c' d d' len' len by auto
  have c_off: "c' = c" "a' @ d' @ b' @ interact as' bs' = a @ d @ b @ interact as bs"
    using eq by (auto simp: Ueq Ueq')
  then have len_a: "length a' = length a"
    by (metis acc_lengths.simps(2) add.left_neutral c c' nth_Cons_0)
  with c_off have §: "a' = a" "d' = d" "b' @ interact as' bs' = b @ interact as bs"
    by auto
  then have "length (interact as' bs') = length (interact as bs)"
    by (metis acc_lengths.simps(2) add_left_cancel append_eq_append_conv d d' list.inject)
  with § have "b' = b" "interact as' bs' = interact as bs"
    by auto
  moreover have "acc_lengths 0 as' = acc_lengths 0 as"
    using ‹a' = a› ‹c' = c› by (simp add: c' c acc_lengths_shift)
  moreover have "acc_lengths 0 bs' = acc_lengths 0 bs"
    using ‹b' = b› ‹d' = d› by (simp add: d' d acc_lengths_shift)
  ultimately have "as' = as ∧ bs' = bs"
    using acc_lengths_interact_injective by blast
  then show ?thesis
    by (simp add: ‹a' = a› U U' ‹b' = b› xs xs' ys ys')
qed


lemma strict_sorted_interact_imp_concat:
    "strict_sorted (interact as bs) ⟹ strict_sorted (concat as) ∧ strict_sorted (concat bs)"
proof (induction as bs rule: interact.induct)
  case (3 x xs y ys)
  have "x < concat xs"
    using "3.prems"
    by (smt (verit, del_insts) Un_iff hd_in_set interact.simps(3) last_in_set less_list_def set_append set_interact sorted_wrt_append)
  moreover have "y < concat ys"
    using 3 sorted_wrt_append strict_sorted_append_iff by fastforce 
  ultimately show ?case
    using 3 by (auto simp add: strict_sorted_append_iff)
qed auto


lemma strict_sorted_interact_hd:
  "⟦strict_sorted (interact cs ds); cs ≠ []; ds ≠ []; hd cs ≠ []; hd ds ≠ []⟧
       ⟹ hd (hd cs) < hd (hd ds)"
  by (metis append_is_Nil_conv hd_append2 hd_in_set interact.simps(3) list.exhaust_sel sorted_wrt_append)


text ‹the lengths of the two lists can differ by one›
proposition interaction_scheme_unique_aux:
  assumes "concat as = concat as'" and ys': "concat bs = concat bs'"
    and "as ∈ lists (- {[]})" "bs ∈ lists (- {[]})"
    and "strict_sorted (interact as bs)"
    and "length bs ≤ length as" "length as ≤ Suc (length bs)"
    and "as' ∈ lists (- {[]})" "bs' ∈ lists (- {[]})"
    and "strict_sorted (interact as' bs')"
    and "length bs' ≤ length as'" "length as' ≤ Suc (length bs')"
    and "length as = length as'" "length bs = length bs'"
  shows "as = as' ∧ bs = bs'"
  using assms
proof (induction "length as" arbitrary: as bs as' bs')
  case 0 then show ?case
    by auto
next
  case SUC: (Suc k)
  show ?case
  proof (cases k)
    case 0
    with SUC obtain a a' where aa': "as = [a]" "as' = [a']"
      by (metis Suc_length_conv length_0_conv)
    show ?thesis
    proof
      show "as = as'"
        using aa' ‹concat as = concat as'› by force
      with SUC 0 show "bs = bs'"
        by (metis Suc_leI append_Nil2 concat.simps impossible_Cons le_antisym length_greater_0_conv list.exhaust)
    qed
  next
    case (Suc k')
    then obtain a cs b ds where eq: "as = a#cs" "bs = b#ds"
      using SUC
      by (metis le0 list.exhaust list.size(3) not_less_eq_eq)
    have "length as' ≠ 0"
      using SUC by force
    then obtain a' cs' b' ds' where eq': "as' = a'#cs'" "bs' = b'#ds'"
      by (metis ‹length bs = length bs'› eq(2) length_0_conv list.exhaust)
    obtain k: "k = length cs" "k ≤ Suc (length ds)"
      using eq SUC by auto
    case (Suc k')
    obtain [simp]: "b ≠ []" "b' ≠ []" "a ≠ []" "a' ≠ []"
      using SUC by (simp add: eq eq')
    then have "hd b' = hd b"
      using SUC by (metis concat.simps(2) eq'(2) eq(2) hd_append2)
    have ss_ab: "strict_sorted (concat as)" "strict_sorted (concat bs)"
      using strict_sorted_interact_imp_concat SUC.prems(5) by blast+
    have sw_ab: "strict_sorted (a @ b @ interact cs ds)"
      by (metis SUC.prems(5) eq interact.simps(3))
    then obtain "a < b" "strict_sorted a" "strict_sorted b"
      by (metis append_assoc strict_sorted_append_iff)
    have b_cs: "strict_sorted (concat (b # cs))"
      by (metis append.simps(1) concat.simps(2) interact.simps(3) strict_sorted_interact_imp_concat sw_ab)
    then have "b < concat cs"
      using strict_sorted_append_iff by auto
    have "strict_sorted (a @ concat cs)"
      using eq(1) ss_ab(1) by force
    have "list.set a = list.set (concat as) ∩ {..< hd b}"
    proof -
      have "x ∈ list.set a"
        if "x < hd b" and "l ∈ list.set cs" and "x ∈ list.set l" for x l
        using b_cs sorted_hd_le strict_sorted_imp_sorted that by fastforce
      then show ?thesis
        using ‹b ≠ []› sw_ab by (force simp: strict_sorted_append_iff sorted_wrt_append eq)
    qed
    moreover
    have ss_ab': "strict_sorted (concat as')" "strict_sorted (concat bs')"
      using strict_sorted_interact_imp_concat SUC.prems(10) by blast+
    have sw_ab': "strict_sorted (a' @ b' @ interact cs' ds')"
      by (metis SUC.prems(10) eq' interact.simps(3))
    then obtain "a' < b'" "strict_sorted a'" "strict_sorted b'"
      by (metis append_assoc strict_sorted_append_iff)
    have b_cs': "strict_sorted (concat (b' # cs'))"
      by (metis (no_types) SUC.prems(10) append_Nil eq' interact.simps(3) strict_sorted_append_iff strict_sorted_interact_imp_concat)
    then have "b' < concat cs'"
      by (simp add: strict_sorted_append_iff)
    then have "hd b' ∉ list.set (concat cs')"
      by (metis Un_iff ‹b' ≠ []› list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append sw_ab')
    have "strict_sorted (a' @ concat cs')"
      using eq'(1) ss_ab'(1) by force
    then have b_cs': "strict_sorted (b' @ concat cs')"
      using ‹b' < concat cs'› eq'(2) ss_ab'(2) strict_sorted_append_iff by auto
    have "list.set a' = list.set (concat as') ∩ {..< hd b'}"
    proof -
      have "x ∈ list.set a'"
        if "x < hd b'" and "l ∈ list.set cs'" and "x ∈ list.set l" for x l
        using b_cs' sorted_hd_le strict_sorted_imp_sorted that by fastforce
      then show ?thesis
        using ‹b' ≠ []› sw_ab' by (force simp: strict_sorted_append_iff sorted_wrt_append eq')
    qed
    ultimately have "a=a'"
      by (simp add: SUC.prems(1) ‹hd b' = hd b› ‹strict_sorted a'› ‹strict_sorted a› strict_sorted_equal)
    moreover
    have ccat_cs_cs': "concat cs = concat cs'"
      using SUC.prems(1) ‹a = a'› eq'(1) eq(1) by fastforce
    have "b=b'"
    proof (cases "ds = [] ∨ ds' = []")
      case True
      then show ?thesis
        using SUC eq'(2) eq(2) by fastforce
    next
      case False
      then have "ds ≠ []" "ds' ≠ []" "sorted (concat ds)" "sorted (concat ds')"
        using eq(2) ss_ab(2) eq'(2) ss_ab'(2) strict_sorted_append_iff strict_sorted_imp_sorted by auto
      have "strict_sorted b" "strict_sorted b'"
        using b_cs b_cs' sorted_wrt_append by auto
      moreover
      have "cs ≠ []"
        using k local.Suc by auto
      then obtain "hd cs ≠ []" "hd ds ≠ []"
        using SUC.prems(3) SUC.prems(4) eq list.set_sel(1)
        by (simp add: ‹ds ≠ []› mem_lists_non_Nil)
      then have "concat cs ≠ []"
        using ‹cs ≠ []› hd_in_set by auto
      have "hd (concat cs) < hd (concat ds)"
        using strict_sorted_interact_hd
        by (metis ‹cs ≠ []› ‹ds ≠ []› ‹hd cs ≠ []› ‹hd ds ≠ []› hd_concat sorted_wrt_append sw_ab)

      have "list.set b = list.set (concat bs) ∩ {..< hd (concat cs)}"
      proof -
        have 1: "x ∈ list.set b"
          if "x < hd (concat cs)" and "l ∈ list.set ds" and "x ∈ list.set l" for x l
          using ‹hd (concat cs) < hd (concat ds)› ‹sorted (concat ds)› sorted_hd_le that by fastforce
        have 2: "l < hd (concat cs)" if "l ∈ list.set b" for l
          by (metis ‹concat cs ≠ []› b_cs concat.simps(2) list.set_sel(1) sorted_wrt_append that)
        show ?thesis
          using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq)
      qed
      moreover
      have "cs' ≠ []"
        using k Suc ‹concat cs ≠ []› ccat_cs_cs' by auto
      then obtain "hd cs' ≠ []" "hd ds' ≠ []"
        using SUC.prems(8,9) ‹ds' ≠ []› eq'(1) eq'(2) list.set_sel(1) by auto
      then have "concat cs' ≠ []"
        using ‹cs' ≠ []› hd_in_set by auto
      have "hd (concat cs') < hd (concat ds')"
        using strict_sorted_interact_hd
        by (metis ‹cs' ≠ []› ‹ds' ≠ []› ‹hd cs' ≠ []› ‹hd ds' ≠ []› hd_concat sorted_wrt_append sw_ab')
      have "list.set b' = list.set (concat bs') ∩ {..< hd (concat cs')}"
      proof -
        have 1: "x ∈ list.set b'"
          if "x < hd (concat cs')" and "l ∈ list.set ds'" and "x ∈ list.set l" for x l
          using ‹hd (concat cs') < hd (concat ds')› ‹sorted (concat ds')› sorted_hd_le that by fastforce
        have 2: "l < hd (concat cs')" if "l ∈ list.set b'" for l
          by (metis ‹concat cs' ≠ []› b_cs' list.set_sel(1) sorted_wrt_append that)
        show ?thesis
          using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq')
      qed
      ultimately show "b = b'"
        by (simp add: SUC.prems(2) ccat_cs_cs' strict_sorted_equal)
    qed
    moreover
    have "cs = cs' ∧ ds = ds'"
    proof (rule SUC.hyps)
      show "k = length cs"
        using eq SUC.hyps(2) by auto[1]
      show "concat ds = concat ds'"
        using SUC.prems(2) ‹b = b'› eq'(2) eq(2) by auto
      show "strict_sorted (interact cs ds)"
        using eq SUC.prems(5) strict_sorted_append_iff by auto
      show "length ds ≤ length cs" "length cs ≤ Suc (length ds)"
        using eq SUC k by auto
      show "strict_sorted (interact cs' ds')"
        using eq' SUC.prems(10) strict_sorted_append_iff by auto
      show "length cs = length cs'"
        using SUC eq'(1) k(1) by force
    qed (use ccat_cs_cs' eq eq' SUC.prems in auto)
    ultimately show ?thesis
      by (simp add: ‹a = a'› ‹b = b'› eq eq')
  qed
qed


proposition Form_Body_unique:
  assumes "Form_Body ka kb xs ys zs" "Form_Body ka kb xs ys zs'" and "kb ≤ ka" "ka ≤ Suc kb"
  shows "zs' = zs"
proof -
  obtain a as b bs c d
      where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)"
        and ne: "a#as ∈ lists (- {[]})" "b#bs ∈ lists (- {[]})"
        and len: "length (a#as) = ka" "length (b#bs) = kb"
        and c: "c = acc_lengths 0 (a#as)"
        and d: "d = acc_lengths 0 (b#bs)"
        and Ueq: "zs = concat [c, a, d, b] @ interact as bs"
        and ss_zs: "strict_sorted zs"
    using Form_Body.cases [OF assms(1)] by (metis (no_types))
  obtain a' as' b' bs' c' d'
      where xs': "xs = concat (a'#as')" and ys': "ys = concat (b'#bs')"
        and ne': "a'#as' ∈ lists (- {[]})" "b'#bs' ∈ lists (- {[]})"
        and len': "length (a'#as') = ka" "length (b'#bs') = kb"
        and c': "c' = acc_lengths 0 (a'#as')"
        and d': "d' = acc_lengths 0 (b'#bs')"
        and Ueq': "zs' = concat [c', a', d', b'] @ interact as' bs'"
        and ss_zs': "strict_sorted zs'"
    using Form_Body.cases [OF assms(2)] by (metis (no_types))
  have [simp]: "length c = length c'" "length d = length d'"
    using c c' d d' len' len by auto
  note acc_lengths.simps [simp del]
  have "a < b"
    using ss_zs by (auto simp: Ueq strict_sorted_append_iff less_list_def c d)
  have "a' < b'"
    using ss_zs' by (auto simp: Ueq' strict_sorted_append_iff less_list_def c' d')
  have "a#as = a'#as' ∧ b#bs = b'#bs'"
  proof (rule interaction_scheme_unique_aux)
    show "strict_sorted (interact (a # as) (b # bs))"
      using ss_zs ‹a < b› by (auto simp: Ueq strict_sorted_append_iff less_list_def d)
    show "strict_sorted (interact (a' # as') (b' # bs'))"
      using ss_zs' ‹a' < b'› by (auto simp: Ueq' strict_sorted_append_iff less_list_def d')
    show "length (b # bs) ≤ length (a # as)" "length (b' # bs') ≤ length (a' # as')"
      using ‹kb ≤ ka› len len' by auto
    show "length (a # as) ≤ Suc (length (b # bs))"
      using ‹ka ≤ Suc kb› len by linarith
    then show "length (a' # as') ≤ Suc (length (b' # bs'))"
      using len len' by fastforce
  qed (use len len' xs xs' ys ys' ne ne' in fastforce)+
  then show ?thesis
    using Ueq Ueq' c c' d d' by blast
qed


lemma Form_Body_imp_inter_scheme:
  assumes FB: "Form_Body ka kb xs ys zs" and "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  shows "zs = inter_scheme ((ka+kb) - Suc 0) {xs,ys}"
proof -
  have "length xs < length ys"
    by (meson Form_Body_length assms(1))
  have [simp]: "a + a = b + b ⟷ a=b"  "a + a - Suc 0 = b + b - Suc 0 ⟷ a=b" for a b::nat
    by auto
  show ?thesis
  proof (cases "ka = kb")
    case True
    show ?thesis
      unfolding inter_scheme_def
      apply (rule some_equality [symmetric], metis One_nat_def True FB mult_2)
      using assms ‹length xs < length ys›
      by (auto simp: True mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger)
  next
    case False
    then have eq: "ka = Suc kb"
      using assms by linarith
    show ?thesis
      unfolding inter_scheme_def
      apply (rule some_equality [symmetric], use assms False mult_2 one_is_add eq in fastforce)
      using assms ‹length xs < length ys›
      by (auto simp: eq mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger)
  qed
qed


subsection ‹For Lemma 3.8 AND PROBABLY 3.7›

definition grab :: "nat set ⇒ nat ⇒ nat set × nat set"
  where "grab N n ≡ (N ∩ enumerate N ` {..<n}, N ∩ {enumerate N n..})"

lemma grab_0 [simp]: "grab N 0 = ({}, N)"
  by (fastforce simp: grab_def enumerate_0 Least_le)

lemma less_sets_grab:
  "infinite N ⟹ fst (grab N n) ≪ snd (grab N n)"
  by (auto simp: grab_def less_sets_def intro: enumerate_mono less_le_trans)

lemma finite_grab [iff]: "finite (fst (grab N n))"
  by (simp add: grab_def)

lemma card_grab [simp]:
  assumes "infinite N" shows "card (fst (grab N n)) = n"
proof -
  have "N ∩ enumerate N ` {..<n} = enumerate N ` {..<n}"
    using assms by (auto simp: enumerate_in_set)
  with assms show ?thesis
    by (simp add: card_image grab_def strict_mono_enum strict_mono_imp_inj_on)
qed

lemma fst_grab_subset: "fst (grab N n) ⊆ N"
  using grab_def range_enum by fastforce

lemma snd_grab_subset: "snd (grab N n) ⊆ N"
  by (auto simp: grab_def)

lemma grab_Un_eq:
  assumes "infinite N" shows "fst (grab N n) ∪ snd (grab N n) = N"
proof
  show "N ⊆ fst (grab N n) ∪ snd (grab N n)"
    unfolding grab_def
    using assms enumerate_Ex le_less_linear strict_mono_enum strict_mono_less by fastforce
qed (simp add: grab_def)

lemma finite_grab_iff [simp]: "finite (snd (grab N n)) ⟷ finite N"
  by (metis finite_grab grab_Un_eq infinite_Un infinite_super snd_grab_subset)

lemma grab_eqD:
    "⟦grab N n = (A,M); infinite N⟧
    ⟹ A ≪ M ∧ finite A ∧ card A = n ∧ infinite M ∧ A ⊆ N ∧ M ⊆ N"
  using card_grab grab_def less_sets_grab finite_grab_iff by auto

lemma less_sets_fst_grab: "A ≪ N ⟹ A ≪ fst (grab N n)"
  by (simp add: fst_grab_subset less_sets_weaken2)

text‹Possibly redundant, given @{term grab}›
definition nxt where "nxt ≡ λN. λn::nat. N ∩ {n<..}"

lemma infinite_nxtN: "infinite N ⟹ infinite (nxt N n)"
  by (simp add: infinite_nat_greaterThan nxt_def)

lemma nxt_subset: "nxt N n ⊆ N"
  unfolding nxt_def by blast

lemma nxt_subset_greaterThan: "m ≤ n ⟹ nxt N n ⊆ {m<..}"
  by (auto simp: nxt_def)

lemma nxt_subset_atLeast: "m ≤ n ⟹ nxt N n ⊆ {m..}"
  by (auto simp: nxt_def)

lemma enum_nxt_ge: "infinite N ⟹ a ≤ enum (nxt N a) n"
  by (simp add: atLeast_le_enum infinite_nxtN nxt_subset_atLeast)

lemma inj_enum_nxt: "infinite N ⟹ inj_on (enum (nxt N a)) A"
  by (simp add: infinite_nxtN strict_mono_enum strict_mono_imp_inj_on)


subsection ‹Larson's Lemma 3.11›

text ‹Again from Jean A. Larson,
     A short proof of a partition theorem for the ordinal $\omega^\omega$.
     \emph{Annals of Mathematical Logic}, 6:129--145, 1973.›

lemma lemma_3_11:
  assumes "l > 0"
  shows "thin (inter_scheme l ` {U. Form l U})"
  using form_cases [of l]
proof cases
  case zero
  then show ?thesis
    using assms by auto
next
  case (nz ka kb)
  note acc_lengths.simps [simp del]
  show ?thesis
    unfolding thin_def
  proof clarify
    fix U U'
    assume ne: "inter_scheme l U ≠ inter_scheme l U'" and init: "initial_segment (inter_scheme l U) (inter_scheme l U')"
    assume "Form l U"
    then obtain kp kq xs ys where "l = kp+kq - 1" "U = {xs,ys}" 
            and U: "Form_Body kp kq xs ys (inter_scheme l U)" and "0 < kq" "kq ≤ kp" "kp ≤ Suc kq"
      using assms inter_scheme by blast
    then have "kp = ka ∧ kq = kb"
      using nz by linarith
    then obtain a as b bs c d
      where len: "length (a#as) = ka" "length (b#bs) = kb"
        and c: "c = acc_lengths 0 (a#as)"
        and d: "d = acc_lengths 0 (b#bs)"
        and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs"
      using U by (auto simp: Form_Body.simps)
    assume "Form l U'"
    then obtain kp' kq' xs' ys'  where "l = kp'+kq' - 1" "U' = {xs',ys'}" 
            and U': "Form_Body kp' kq' xs' ys' (inter_scheme l U')" and "0 < kq'" "kq' ≤ kp'" "kp' ≤ Suc kq'"
      using assms inter_scheme by blast
    then have "kp' = ka ∧ kq' = kb"
      using nz by linarith
    then obtain a' as' b' bs' c' d'
      where len': "length (a'#as') = ka" "length (b'#bs') = kb"
        and c': "c' = acc_lengths 0 (a'#as')"
        and d': "d' = acc_lengths 0 (b'#bs')"
        and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'"
      using U' by (auto simp: Form_Body.simps)
    have [simp]: "length bs' = length bs" "length as' = length as"
      using len len' by auto
    have "inter_scheme l U ≠ []" "inter_scheme l U' ≠ []"
      using Form_Body_nonempty U U' by auto
    define u1 where "u1 ≡ hd (inter_scheme l U)"
    have u1_eq': "u1 = hd (inter_scheme l U')"
      using ‹inter_scheme l U ≠ []› init u1_def initial_segment_ne by fastforce
    have au1: "u1 = length a"
      by (simp add: u1_def Ueq c)
    have au1': "u1 = length a'"
      by (simp add: u1_eq' Ueq' c')
    have len_eqk: "length c' = ka" "length d' = kb" "length c' = ka" "length d' = kb"
      using c d len c' d' len' by auto
    have take: "take (ka + u1 + kb) (c @ a @ d @ l) = c @ a @ d"
               "take (ka + u1 + kb) (c' @ a' @ d' @ l) = c' @ a' @ d'" for l
      using c d c' d' len by (simp_all flip: au1 au1')
    have leU: "ka + u1 + kb ≤ length (inter_scheme l U)"
      using c d len by (simp add: au1 Ueq)
    then have "take (ka + u1 + kb) (inter_scheme l U) = take (ka + u1 + kb) (inter_scheme l U')"
      using take_initial_segment init by blast
    then have §: "c @ a @ d = c' @ a' @ d'"
      by (metis Ueq Ueq' append.assoc concat.simps(2) take)
    have "length (inter_scheme l U) = ka + (c @ a @ d)!(ka-1) + kb + last d"
      by (simp add: Ueq c d length_interact nth_append flip: len)
    moreover have "length (inter_scheme l U') = ka + (c' @ a' @ d')!(ka-1) + kb + last d'"
      by (simp add: Ueq' c' d' length_interact nth_append flip: len')
    moreover have "last d = last d'"
      using "§" c d d' len'(1) len_eqk(1) by auto
    ultimately have "length (inter_scheme l U) = length (inter_scheme l U')"
      by (simp add: §)
    then show False
      using init initial_segment_length_eq ne by blast
  qed
qed


subsection ‹Larson's Lemma 3.6›

proposition lemma_3_6:
  fixes g :: "nat list set ⇒ nat"
  assumes g: "g ∈ [WW]⇗2⇖ → {0,1}"
  obtains N j where "infinite N"
    and "⋀k u. ⟦k > 0; u ∈ [WW]⇗2⇖; Form k u; [enum N k] < inter_scheme k u; List.set (inter_scheme k u) ⊆ N⟧ ⟹ g u = j k"
proof -
  define Φ where "Φ ≡ λm::nat. λM. infinite M ∧ m < Inf M"
  define Ψ where "Ψ ≡ λl m n::nat. λM N j. n > m ∧ N ⊆ M ∧ n ∈ M 
                     ∧ (∀U. Form l U ∧ U ⊆ WW ∧ [n] < inter_scheme l U ∧ list.set (inter_scheme l U) ⊆ N ⟶ g U = j)"
  have *: "∃n N j. Φ n N ∧ Ψ l m n M N j" if "l > 0" "Φ m M" for l m::nat and M :: "nat set"
  proof -
    define FF where "FF ≡ {U ∈ [WW]⇗2⇖. Form l U}"
    define h where "h ≡ λzs. g (inv_into FF (inter_scheme l) zs)"
    have "thin (inter_scheme l ` FF)"
      using ‹l > 0› lemma_3_11 by (simp add: thin_def FF_def)
    moreover
    have "inter_scheme l ` FF ⊆ WW"
      using inter_scheme_simple ‹0 < l› FF_def by blast
    moreover
    have "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ M} ⊆ {..<2}"
      using g inv_into_into[of concl: "FF" "inter_scheme l"]
      by (force simp: h_def FF_def Pi_iff)
    ultimately
    obtain j N where "j < 2" "infinite N" "N ⊆ M" and hj: "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ N} ⊆ {j}"
      using ‹Φ m M› unfolding Φ_def by (blast intro: Nash_Williams_WW [of M])
    let ?n = "Inf N"
    have "?n > m"
      using ‹Φ m M› ‹infinite N› unfolding Φ_def Inf_nat_def infinite_nat_iff_unbounded
      by (metis LeastI_ex ‹N ⊆ M› le_less_trans not_less not_less_Least subsetD)
    have "g U = j" if "Form l U" "U ⊆ WW" "[?n] < inter_scheme l U" "list.set (inter_scheme l U) ⊆ N - {?n}" for U
    proof -
      obtain xs ys where xys: "xs ≠ ys" "U = {xs,ys}"
        using Form_elim_upair ‹Form l U› by blast
      moreover have "inj_on (inter_scheme l) FF"
        using ‹0 < l› inj_on_def inter_scheme_injective FF_def by blast
      moreover 
      have "g (inv_into FF (inter_scheme l) (inter_scheme l U)) = j"
        using hj that xys subset_Diff_insert by (fastforce simp: h_def FF_def image_iff)
      ultimately show ?thesis
        using that FF_def by auto
    qed
    moreover have "?n < Inf (N - {?n})"
      by (metis Diff_iff Inf_nat_def Inf_nat_def1 ‹infinite N› finite.emptyI infinite_remove linorder_neqE_nat not_less_Least singletonI)
    moreover have "?n ∈ M"
      by (metis Inf_nat_def1 ‹N ⊆ M› ‹infinite N› finite.emptyI subsetD)
    ultimately have "Φ ?n (N - {?n}) ∧ Ψ l m ?n M (N - {?n}) j"
      using ‹Φ m M› ‹infinite N› ‹N ⊆ M› ‹?n > m› by (auto simp: Φ_def Ψ_def)
    then show ?thesis
      by blast
  qed
  have base: "Φ 0 {0<..}"
    unfolding Φ_def by (metis infinite_Ioi Inf_nat_def1 greaterThan_iff greaterThan_non_empty)
  have step: "Ex (λ(n,N,j). Φ n N ∧ Ψ l m n M N j)" if "Φ m M" "l > 0" for m M l
    using * [of l m M] that by (auto simp: Φ_def)
  define G where "G ≡ λl m M. @(n,N,j). Φ n N ∧ Ψ (Suc l) m n M N j"
  have GΦ: "(λ(n,N,j). Φ n N) (G l m M)" and GΨ: "(λ(n,N,j). Ψ (Suc l) m n M N j) (G l m M)"
    if "Φ m M" for l m M
    using step [OF that, of "Suc l"] by (force simp: G_def dest: some_eq_imp)+
  have G_increasing: "(λ(n,N,j). n > m ∧ N ⊆ M ∧ n ∈ M) (G l m M)"  if "Φ m M" for l m M
    using GΨ [OF that, of l] that by (simp add: Ψ_def split: prod.split_asm)
  define H where "H ≡ rec_nat (0,{0<..},0) (λl (m,M,j). G l m M)"
  have H_simps: "H 0 = (0,{0<..},0)" "⋀l. H (Suc l) = (case H l of (m,M,j) ⇒ G l m M)"
    by (simp_all add: H_def)
  have HΦ: "(λ(n,N,j). Φ n N) (H l)" for l
    by (induction l) (use base GΦ in ‹auto simp: H_simps split: prod.split_asm›)
  define ν where "ν ≡ (λl. case H l of (n,M,j) ⇒ n)"
  have H_inc: "ν l ≥ l" for l
  proof (induction l)
    case (Suc l)
    then show ?case
      using HΦ [of l] G_increasing [of "ν l"]
      apply (clarsimp simp: H_simps ν_def split: prod.split)
      by (metis (no_types, lifting) case_prodD leD le_less_trans not_less_eq_eq)
  qed auto
  let ?N = "range ν"
  define j where "j ≡ λl. case H l of (n,M,j) ⇒ j"
  have H_increasing_Suc: "(case H k of (n, N, j') ⇒ N) ⊇ (case H (Suc k) of (n, N, j') ⇒ insert n N)" for k
    using HΦ [of k]
    by (force simp: H_simps split: prod.split dest: G_increasing [where l=k])
  have H_increasing_superset: "(case H k of (n, N, j') ⇒ N