# 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`