Theory BT_Prelim

(*  Title:       BT_Prelim.thy
    Author:      Arthur F. Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz, 2026

    Preliminaries shared across the Banach-Tarski formalization.

    This theory introduces conventions used throughout: type abbreviations
    for the unit sphere and unit ball, and a few small structural lemmas
    that recur.
*)

theory BT_Prelim
  imports
    "HOL-Analysis.Analysis"
    "Free-Groups.FreeGroups"
begin

section ‹The unit sphere and unit ball in $\mathbb{R}^3$›

text ‹
  We work throughout with vectors in @{typ "real^3"} (the type
  @{typ "real^3"} from \<^theory>‹HOL-Analysis.Cartesian_Euclidean_Space›).
  These abbreviations name the principal geometric objects of interest.
›

definition sphere2 :: "(real^3) set" where
  "sphere2 = {x. norm x = 1}"

definition ball3 :: "(real^3) set" where
  "ball3 = {x. norm x ≤ 1}"

lemma sphere2_subset_ball3: "sphere2 ⊆ ball3"
  by (auto simp: sphere2_def ball3_def)

lemma zero_in_ball3: "0 ∈ ball3"
  by (simp add: ball3_def)

lemma zero_notin_sphere2: "(0::real^3) ∉ sphere2"
  by (simp add: sphere2_def)


section ‹Disjoint finite covers›

text ‹
  A ∗‹partition› of a set into a finite list of pairwise disjoint pieces
  is the basic combinatorial object underlying ``equidecomposability''.
›

definition pairwise_disjoint :: "'a set list ⇒ bool" where
  "pairwise_disjoint Xs ⟷
     (∀i < length Xs. ∀j < length Xs. i ≠ j ⟶ Xs ! i ∩ Xs ! j = {})"

lemma pairwise_disjoint_Nil [simp]: "pairwise_disjoint []"
  by (simp add: pairwise_disjoint_def)

lemma pairwise_disjoint_singleton [simp]: "pairwise_disjoint [X]"
  by (simp add: pairwise_disjoint_def)

lemma pairwise_disjoint_nthD:
  assumes "pairwise_disjoint Xs"
    and "i < length Xs" and "j < length Xs" and "i ≠ j"
  shows "Xs ! i ∩ Xs ! j = {}"
  using assms bot_set_def pairwise_disjoint_def by auto

lemma indexed_union_set:
  fixes P :: "'a set list"
  shows "(⋃i<length P. P ! i) = ⋃(set P)"
  by (auto simp add: set_conv_nth image_def)

lemma indexed_union_append:
  fixes P Q :: "'a set list"
  shows "(⋃i<length (P @ Q). (P @ Q) ! i) =
    (⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i)"
  by (metis Union_Un_distrib indexed_union_set set_append)

lemma indexed_image_union_zip:
  fixes P :: "'a set list" and G :: "('a ⇒ 'b) list"
  assumes "length P = length G"
  shows "(⋃i<length P. G ! i ` (P ! i)) =
    (⋃(g, A)∈set (zip G P). g ` A)"
  using assms by (auto simp add: set_zip)

lemma indexed_image_union_append:
  fixes P Q :: "'a set list" and G H :: "('a ⇒ 'b) list"
  assumes lenP: "length P = length G" and lenQ: "length Q = length H"
  shows "(⋃i<length (P @ Q). (G @ H) ! i ` ((P @ Q) ! i)) =
    (⋃i<length P. G ! i ` (P ! i)) ∪
    (⋃i<length Q. H ! i ` (Q ! i))"
proof -
  have len_append: "length (P @ Q) = length (G @ H)"
    using lenP lenQ by simp
  have "(⋃i<length (P @ Q). (G @ H) ! i ` ((P @ Q) ! i)) =
      (⋃(g, A)∈set (zip (G @ H) (P @ Q)). g ` A)"
    using indexed_image_union_zip[OF len_append] .
  also have "… =
      (⋃(g, A)∈set (zip G P). g ` A) ∪
      (⋃(g, A)∈set (zip H Q). g ` A)"
    using lenP by simp
  also have "… =
      (⋃i<length P. G ! i ` (P ! i)) ∪
      (⋃i<length Q. H ! i ` (Q ! i))"
    using indexed_image_union_zip[OF lenP] indexed_image_union_zip[OF lenQ] by simp
  finally show ?thesis .
qed

lemma indexed_union_map_fst:
  fixes xs :: "('a set × 'b) list"
  shows "(⋃i<length (map fst xs). map fst xs ! i) =
    (⋃x∈set xs. fst x)"
  by (auto simp add: set_conv_nth)

lemma indexed_image_union_pairs:
  fixes xs :: "('a set × ('a ⇒ 'b)) list"
  shows "(⋃i<length (map fst xs). map snd xs ! i ` (map fst xs ! i)) =
    (⋃x∈set xs. snd x ` fst x)"
  by (auto simp add: set_conv_nth)

lemma pairwise_disjoint_map_fstI:
  fixes xs :: "('a set × 'b) list"
  assumes distinct: "distinct xs"
    and disj: "⋀x y. ⟦x ∈ set xs; y ∈ set xs; x ≠ y⟧
      ⟹ fst x ∩ fst y = {}"
  shows "pairwise_disjoint (map fst xs)"
  unfolding pairwise_disjoint_def
proof (intro allI impI)
  fix i j
  assume i: "i < length (map fst xs)" and j: "j < length (map fst xs)" and ij: "i ≠ j"
  have xi: "xs ! i ∈ set xs" and xj: "xs ! j ∈ set xs"
    using i j by auto
  have neq: "xs ! i ≠ xs ! j"
    using distinct i j ij by (simp add: nth_eq_iff_index_eq)
  show "map fst xs ! i ∩ map fst xs ! j = {}"
    using disj[OF xi xj neq] i j by simp
qed

lemma pairwise_disjoint_appendI:
  assumes xs: "pairwise_disjoint xs"
    and ys: "pairwise_disjoint ys"
    and cross: "⋀x y. ⟦x ∈ set xs; y ∈ set ys⟧ ⟹ x ∩ y = {}"
  shows "pairwise_disjoint (xs @ ys)"
  unfolding pairwise_disjoint_def
proof (intro allI impI)
  fix i j
  assume i: "i < length (xs @ ys)" and j: "j < length (xs @ ys)" and ij: "i ≠ j"
  show "(xs @ ys) ! i ∩ (xs @ ys) ! j = {}"
  proof (cases "i < length xs")
    case True
    show ?thesis
    proof (cases "j < length xs")
      case True
      have "xs ! i ∩ xs ! j = {}"
        by (rule pairwise_disjoint_nthD[OF xs ‹i < length xs› True ij])
      with ‹i < length xs› True show ?thesis
        by (simp add: nth_append)
    next
      case False
      hence "(xs @ ys) ! j ∈ set ys"
        using j by (simp add: nth_append)
      moreover have "(xs @ ys) ! i ∈ set xs"
        by (simp add: True nth_append_left)
      ultimately show ?thesis
        using cross by simp
    qed
  next
    case False
    show ?thesis
    proof (cases "j < length xs")
      case True
      hence "(xs @ ys) ! j ∈ set xs"
      proof -
        have "(xs @ ys) ! j = xs ! j"
          using True by (simp add: nth_append)
        moreover have "xs ! j ∈ set xs"
          by (rule nth_mem[OF True])
        ultimately show ?thesis
          by simp
      qed
      moreover have "(xs @ ys) ! i ∈ set ys"
        using False i by (simp add: nth_append)
      ultimately have "(xs @ ys) ! j ∩ (xs @ ys) ! i = {}"
        using cross by blast
      thus ?thesis
        by (simp add: Int_commute)
    next
      case False
      have "ys ! (i - length xs) ∩ ys ! (j - length xs) = {}"
        by (rule pairwise_disjoint_nthD[OF ys]) (use False ‹¬ i < length xs› i j ij in auto)
      with False ‹¬ i < length xs› i j show ?thesis
        by (simp add: nth_append)
    qed
  qed
qed

lemma pairwise_disjoint_appendD1:
  assumes "pairwise_disjoint (xs @ ys)"
  shows "pairwise_disjoint xs"
  unfolding pairwise_disjoint_def
proof (intro allI impI)
  fix i j
  assume i: "i < length xs" and j: "j < length xs" and ij: "i ≠ j"
  have "(xs @ ys) ! i ∩ (xs @ ys) ! j = {}"
    by (rule pairwise_disjoint_nthD[OF assms]) (use i j ij in simp_all)
  thus "xs ! i ∩ xs ! j = {}"
    using i j by (simp add: nth_append)
qed

lemma pairwise_disjoint_appendD2:
  assumes "pairwise_disjoint (xs @ ys)"
  shows "pairwise_disjoint ys"
  unfolding pairwise_disjoint_def
proof (intro allI impI)
  fix i j
  assume i: "i < length ys" and j: "j < length ys" and ij: "i ≠ j"
  have "length xs + i < length (xs @ ys)" and "length xs + j < length (xs @ ys)"
    using i j by simp_all
  moreover have "length xs + i ≠ length xs + j"
    using ij by simp
  ultimately have "(xs @ ys) ! (length xs + i) ∩ (xs @ ys) ! (length xs + j) = {}"
    by (rule pairwise_disjoint_nthD[OF assms])
  thus "ys ! i ∩ ys ! j = {}"
    using i j by simp
qed

lemma pairwise_disjoint_append_crossD:
  assumes "pairwise_disjoint (xs @ ys)"
    and "i < length xs" and "j < length ys"
  shows "xs ! i ∩ ys ! j = {}"
proof -
  have "i < length (xs @ ys)" and "length xs + j < length (xs @ ys)"
    using assms by simp_all
  moreover have "i ≠ length xs + j"
    using assms(2) by simp
  ultimately have "(xs @ ys) ! i ∩ (xs @ ys) ! (length xs + j) = {}"
    by (rule pairwise_disjoint_nthD[OF assms(1)])
  moreover have "(xs @ ys) ! i = xs ! i"
    using assms(2) by (simp add: nth_append)
  moreover have "(xs @ ys) ! (length xs + j) = ys ! j"
    using assms(3) by (simp add: nth_append)
  ultimately show ?thesis
    by simp
qed

lemma pairwise_disjoint_pair_imagesI:
  fixes xs :: "('a set × ('a ⇒ 'b)) list"
  assumes distinct: "distinct xs"
    and disj: "⋀x y. ⟦x ∈ set xs; y ∈ set xs; x ≠ y⟧
      ⟹ snd x ` fst x ∩ snd y ` fst y = {}"
  shows "pairwise_disjoint (map2 (λg A. g ` A) (map snd xs) (map fst xs))"
proof -
  have map_eq: "map2 (λg A. g ` A) (map snd xs) (map fst xs) =
      map (λx. snd x ` fst x) xs"
    by (induction xs) simp_all
  show ?thesis
    unfolding map_eq pairwise_disjoint_def
  proof (intro allI impI)
    fix i j
    assume i: "i < length (map (λx. snd x ` fst x) xs)"
      and j: "j < length (map (λx. snd x ` fst x) xs)" and ij: "i ≠ j"
    have xi: "xs ! i ∈ set xs" and xj: "xs ! j ∈ set xs"
      using i j by auto
    have neq: "xs ! i ≠ xs ! j"
      using distinct i j ij by (simp add: nth_eq_iff_index_eq)
    show "map (λx. snd x ` fst x) xs ! i ∩
        map (λx. snd x ` fst x) xs ! j = {}"
      using disj[OF xi xj neq] i j by simp
  qed
qed


section ‹Transporting finite partitions›

definition transfer_piece ::
  "'a set list ⇒ ('a ⇒ 'a) list ⇒ 'a set list ⇒
    ('a ⇒ 'a) list ⇒ 'a set list ⇒ nat ⇒ nat ⇒ nat ⇒ 'a set"
where
  "transfer_piece A e P g B k i l =
    {x ∈ A ! k. (e ! k) x ∈ P ! i ∧ (g ! i) ((e ! k) x) ∈ B ! l}"

definition transfer_map ::
  "('a ⇒ 'a) list ⇒ ('a ⇒ 'a) list ⇒
    ('a ⇒ 'a) list ⇒ nat ⇒ nat ⇒ nat ⇒ ('a ⇒ 'a)"
where
  "transfer_map t g e k i l = (t ! l) ∘ (g ! i) ∘ (e ! k)"

definition transfer_pairs ::
  "'a set list ⇒ ('a ⇒ 'a) list ⇒ 'a set list ⇒
    ('a ⇒ 'a) list ⇒ 'a set list ⇒ ('a ⇒ 'a) list ⇒
    ('a set × ('a ⇒ 'a)) set"
where
  "transfer_pairs A e P g B t =
    {(transfer_piece A e P g B k i l, transfer_map t g e k i l) |
       k i l. k < length A ∧ i < length P ∧ l < length B}"

lemma finite_transfer_pairs [simp]: "finite (transfer_pairs A e P g B t)"
proof -
  have "transfer_pairs A e P g B t ⊆
      (λ((k, i), l). (transfer_piece A e P g B k i l, transfer_map t g e k i l)) `
        (({..<length A} × {..<length P}) × {..<length B})"
  proof
    fix p
    assume "p ∈ transfer_pairs A e P g B t"
    then obtain k i l where k: "k < length A" and i: "i < length P" and l: "l < length B"
      and p_eq: "p = (transfer_piece A e P g B k i l, transfer_map t g e k i l)"
      unfolding transfer_pairs_def by blast
    have tril_in: "((k, i), l) ∈ ({..<length A} × {..<length P}) × {..<length B}"
      using k i l by simp
    show "p ∈
      (λ((k, i), l). (transfer_piece A e P g B k i l, transfer_map t g e k i l)) `
        (({..<length A} × {..<length P}) × {..<length B})"
      using p_eq tril_in by force
  qed
  thus ?thesis
    by (rule finite_subset) simp
qed

lemma transfer_source_cover:
  assumes A_cover: "Y = (⋃k<length A. A ! k)"
    and B_cover: "X = (⋃k<length B. B ! k)"
    and e_into_B: "⋀k x. ⟦k < length A; x ∈ A ! k⟧ ⟹ (e ! k) x ∈ B ! k"
    and len_AB: "length A = length B"
    and source_cover: "X = (⋃i<length P. P ! i) ∪ (⋃j<length Q. Q ! j)"
    and imageP_cover: "X = (⋃i<length P. gP ! i ` (P ! i))"
    and imageQ_cover: "X = (⋃j<length Q. gQ ! j ` (Q ! j))"
  shows "Y =
    (⋃p∈transfer_pairs A e P gP B t. fst p) ∪
    (⋃q∈transfer_pairs A e Q gQ B t. fst q)"
proof
  show "Y ⊆
      (⋃p∈transfer_pairs A e P gP B t. fst p) ∪
      (⋃q∈transfer_pairs A e Q gQ B t. fst q)"
  proof
    fix x
    assume xY: "x ∈ Y"
    then obtain k where k: "k < length A" and xA: "x ∈ A ! k"
      using A_cover by blast
    have ex: "(e ! k) x ∈ X"
      using B_cover e_into_B k len_AB xA by auto
    from source_cover ex have ex_cases:
      "(e ! k) x ∈ (⋃i<length P. P ! i) ∨
       (e ! k) x ∈ (⋃j<length Q. Q ! j)"
      by blast
    thus "x ∈
        (⋃p∈transfer_pairs A e P gP B t. fst p) ∪
        (⋃q∈transfer_pairs A e Q gQ B t. fst q)"
    proof
      assume "(e ! k) x ∈ (⋃i<length P. P ! i)"
      then obtain i where i: "i < length P" and xP: "(e ! k) x ∈ P ! i"
        by blast
      have gxX: "(gP ! i) ((e ! k) x) ∈ X"
        using imageP_cover i xP by blast
      then obtain l where l: "l < length B" and gxB: "(gP ! i) ((e ! k) x) ∈ B ! l"
        using B_cover by blast
      have pair_in: "(transfer_piece A e P gP B k i l, transfer_map t gP e k i l)
          ∈ transfer_pairs A e P gP B t"
        using k i l unfolding transfer_pairs_def by blast
      have x_piece: "x ∈ transfer_piece A e P gP B k i l"
        using xA xP gxB by (simp add: transfer_piece_def)
      have set_in: "fst (transfer_piece A e P gP B k i l, transfer_map t gP e k i l) ∈
          ((λp. fst p) ` transfer_pairs A e P gP B t)"
        by (rule imageI[OF pair_in])
      have x_fst: "x ∈ fst (transfer_piece A e P gP B k i l, transfer_map t gP e k i l)"
        using x_piece by simp
      have "x ∈ ⋃ ((λp. fst p) ` transfer_pairs A e P gP B t)"
        using set_in x_fst by (rule UnionI)
      thus ?thesis
        by simp
    next
      assume "(e ! k) x ∈ (⋃j<length Q. Q ! j)"
      then obtain j where j: "j < length Q" and xQ: "(e ! k) x ∈ Q ! j"
        by blast
      have gxX: "(gQ ! j) ((e ! k) x) ∈ X"
        using imageQ_cover j xQ by blast
      then obtain l where l: "l < length B" and gxB: "(gQ ! j) ((e ! k) x) ∈ B ! l"
        using B_cover by blast
      have pair_in: "(transfer_piece A e Q gQ B k j l, transfer_map t gQ e k j l)
          ∈ transfer_pairs A e Q gQ B t"
        using k j l unfolding transfer_pairs_def by blast
      have x_piece: "x ∈ transfer_piece A e Q gQ B k j l"
        using xA xQ gxB by (simp add: transfer_piece_def)
      have set_in: "fst (transfer_piece A e Q gQ B k j l, transfer_map t gQ e k j l) ∈
          ((λq. fst q) ` transfer_pairs A e Q gQ B t)"
        by (rule imageI[OF pair_in])
      have x_fst: "x ∈ fst (transfer_piece A e Q gQ B k j l, transfer_map t gQ e k j l)"
        using x_piece by simp
      have "x ∈ ⋃ ((λq. fst q) ` transfer_pairs A e Q gQ B t)"
        using set_in x_fst by (rule UnionI)
      thus ?thesis
        by simp
    qed
  qed
  show "(⋃p∈transfer_pairs A e P gP B t. fst p) ∪
      (⋃q∈transfer_pairs A e Q gQ B t. fst q) ⊆ Y"
    using A_cover unfolding transfer_pairs_def transfer_piece_def by auto
qed

lemma transfer_image_cover:
  assumes A_cover: "Y = (⋃k<length A. A ! k)"
    and B_cover: "X = (⋃k<length B. B ! k)"
    and len_AB: "length A = length B"
    and e_left: "⋀k x. ⟦k < length A; x ∈ A ! k⟧
      ⟹ (e ! k) x ∈ B ! k ∧ (t ! k) ((e ! k) x) = x"
    and t_left: "⋀k y. ⟦k < length B; y ∈ B ! k⟧
      ⟹ (t ! k) y ∈ A ! k ∧ (e ! k) ((t ! k) y) = y"
    and P_sub: "⋀i. i < length P ⟹ P ! i ⊆ X"
    and image_cover: "X = (⋃i<length P. g ! i ` (P ! i))"
  shows "Y = (⋃p∈transfer_pairs A e P g B t. snd p ` fst p)"
proof
  show "Y ⊆ (⋃p∈transfer_pairs A e P g B t. snd p ` fst p)"
  proof
    fix y
    assume yY: "y ∈ Y"
    then obtain l where l: "l < length A" and yA: "y ∈ A ! l"
      using A_cover by blast
    have eyB: "(e ! l) y ∈ B ! l" and tey: "(t ! l) ((e ! l) y) = y"
      using e_left[OF l yA] by auto
    have eyX: "(e ! l) y ∈ X"
      using B_cover eyB l len_AB by auto
    then obtain i x where i: "i < length P" and xP: "x ∈ P ! i"
      and ey_eq: "(e ! l) y = (g ! i) x"
      using image_cover by blast
    have lB: "l < length B"
      using l len_AB by simp
    have xX: "x ∈ X"
      using P_sub[OF i] xP by (rule subsetD)
    then obtain k where k: "k < length B" and xB: "x ∈ B ! k"
      using B_cover by blast
    have txA: "(t ! k) x ∈ A ! k" and etx: "(e ! k) ((t ! k) x) = x"
      using t_left[OF k xB] by auto
    have kA: "k < length A"
      using k len_AB by simp
    have piece_in: "(t ! k) x ∈ transfer_piece A e P g B k i l"
      using txA etx xP eyB ey_eq by (simp add: transfer_piece_def)
    have pair_in: "(transfer_piece A e P g B k i l, transfer_map t g e k i l)
        ∈ transfer_pairs A e P g B t"
      using kA i lB unfolding transfer_pairs_def by blast
    have "transfer_map t g e k i l ((t ! k) x) = y"
      using etx ey_eq tey by (simp add: transfer_map_def)
    thus "y ∈ (⋃p∈transfer_pairs A e P g B t. snd p ` fst p)"
      using pair_in piece_in by force
  qed
  show "(⋃p∈transfer_pairs A e P g B t. snd p ` fst p) ⊆ Y"
  proof
    fix y
    assume "y ∈ (⋃p∈transfer_pairs A e P g B t. snd p ` fst p)"
    then obtain k i l x where k: "k < length A" and i: "i < length P"
      and l: "l < length B" and x_piece: "x ∈ transfer_piece A e P g B k i l"
      and y_eq: "y = transfer_map t g e k i l x"
      unfolding transfer_pairs_def by auto
    have gxB: "(g ! i) ((e ! k) x) ∈ B ! l"
      using x_piece by (simp add: transfer_piece_def)
    have tyA: "(t ! l) ((g ! i) ((e ! k) x)) ∈ A ! l"
      using t_left[OF l gxB] by auto
    hence "y ∈ A ! l"
      using y_eq by (simp add: transfer_map_def)
    moreover have "A ! l ⊆ Y"
      using A_cover l len_AB by auto
    ultimately show "y ∈ Y"
      by blast
  qed
qed

lemma transfer_source_disjoint_same:
  assumes A_disj: "pairwise_disjoint A"
    and P_disj: "pairwise_disjoint P"
    and B_disj: "pairwise_disjoint B"
    and x_in: "x ∈ transfer_pairs A e P g B t"
    and y_in: "y ∈ transfer_pairs A e P g B t"
    and xy: "x ≠ y"
  shows "fst x ∩ fst y = {}"
proof (rule ccontr)
  assume nonempty: "fst x ∩ fst y ≠ {}"
  obtain k i l where k: "k < length A" and i: "i < length P" and l: "l < length B"
    and x_eq: "x = (transfer_piece A e P g B k i l, transfer_map t g e k i l)"
    using x_in unfolding transfer_pairs_def by blast
  obtain k' i' l' where k': "k' < length A" and i': "i' < length P" and l': "l' < length B"
    and y_eq: "y = (transfer_piece A e P g B k' i' l', transfer_map t g e k' i' l')"
    using y_in unfolding transfer_pairs_def by blast
  from nonempty obtain z where zx: "z ∈ fst x" and zy: "z ∈ fst y"
    by blast
  have zA: "z ∈ A ! k" and zeP: "(e ! k) z ∈ P ! i"
    and zgB: "(g ! i) ((e ! k) z) ∈ B ! l"
    using zx x_eq by (auto simp: transfer_piece_def)
  have zA': "z ∈ A ! k'" and zeP': "(e ! k') z ∈ P ! i'"
    and zgB': "(g ! i') ((e ! k') z) ∈ B ! l'"
    using zy y_eq by (auto simp: transfer_piece_def)
  show False
  proof (cases "k = k'")
    case False
    have "A ! k ∩ A ! k' = {}"
      by (rule pairwise_disjoint_nthD[OF A_disj k k' False])
    with zA zA' show False
      by blast
  next
    case k_eq: True
    show False
    proof (cases "i = i'")
      case False
      have "P ! i ∩ P ! i' = {}"
        by (rule pairwise_disjoint_nthD[OF P_disj i i' False])
      moreover have "(e ! k) z ∈ P ! i'"
        using zeP' k_eq by simp
      ultimately show False
        using zeP by blast
    next
      case i_eq: True
      show False
      proof (cases "l = l'")
        case False
        have "B ! l ∩ B ! l' = {}"
          by (rule pairwise_disjoint_nthD[OF B_disj l l' False])
        moreover have "(g ! i) ((e ! k) z) ∈ B ! l'"
          using zgB' k_eq i_eq by simp
        ultimately show False
          using zgB by blast
      next
        case l_eq: True
        have "x = y"
          using x_eq y_eq k_eq i_eq l_eq by simp
        with xy show False
          by contradiction
      qed
    qed
  qed
qed

lemma transfer_source_disjoint_cross:
  assumes A_disj: "pairwise_disjoint A"
    and PQ_cross: "⋀i j. ⟦i < length P; j < length Q⟧ ⟹ P ! i ∩ Q ! j = {}"
    and B_disj: "pairwise_disjoint B"
    and x_in: "x ∈ transfer_pairs A e P gP B t"
    and y_in: "y ∈ transfer_pairs A e Q gQ B t"
  shows "fst x ∩ fst y = {}"
proof (rule ccontr)
  assume nonempty: "fst x ∩ fst y ≠ {}"
  obtain k i l where k: "k < length A" and i: "i < length P" and l: "l < length B"
    and x_eq: "x = (transfer_piece A e P gP B k i l, transfer_map t gP e k i l)"
    using x_in unfolding transfer_pairs_def by blast
  obtain k' j l' where k': "k' < length A" and j: "j < length Q" and l': "l' < length B"
    and y_eq: "y = (transfer_piece A e Q gQ B k' j l', transfer_map t gQ e k' j l')"
    using y_in unfolding transfer_pairs_def by blast
  from nonempty obtain z where zx: "z ∈ fst x" and zy: "z ∈ fst y"
    by blast
  have zA: "z ∈ A ! k" and zeP: "(e ! k) z ∈ P ! i"
    using zx x_eq by (auto simp: transfer_piece_def)
  have zA': "z ∈ A ! k'" and zeQ: "(e ! k') z ∈ Q ! j"
    using zy y_eq by (auto simp: transfer_piece_def)
  show False
  proof (cases "k = k'")
    case False
    have "A ! k ∩ A ! k' = {}"
      by (rule pairwise_disjoint_nthD[OF A_disj k k' False])
    with zA zA' show False
      by blast
  next
    case k_eq: True
    have "P ! i ∩ Q ! j = {}"
      by (rule PQ_cross[OF i j])
    moreover have "(e ! k) z ∈ Q ! j"
      using zeQ k_eq by simp
    ultimately show False
      using zeP by blast
  qed
qed

lemma transfer_image_disjoint_same:
  assumes len_AB: "length A = length B"
    and A_disj: "pairwise_disjoint A"
    and B_disj: "pairwise_disjoint B"
    and image_disj: "pairwise_disjoint (map2 (λh C. h ` C) g P)"
    and len: "length P = length g"
    and g_inj: "⋀i. i < length P ⟹ inj (g ! i)"
    and e_into_B: "⋀k x. ⟦k < length A; x ∈ A ! k⟧ ⟹ (e ! k) x ∈ B ! k"
    and t_left: "⋀l y. ⟦l < length B; y ∈ B ! l⟧
      ⟹ (t ! l) y ∈ A ! l ∧ (e ! l) ((t ! l) y) = y"
    and x_in: "x ∈ transfer_pairs A e P g B t"
    and y_in: "y ∈ transfer_pairs A e P g B t"
    and xy: "x ≠ y"
  shows "snd x ` fst x ∩ snd y ` fst y = {}"
proof (rule ccontr)
  assume nonempty: "snd x ` fst x ∩ snd y ` fst y ≠ {}"
  obtain k i l where k: "k < length A" and i: "i < length P" and l: "l < length B"
    and x_eq: "x = (transfer_piece A e P g B k i l, transfer_map t g e k i l)"
    using x_in unfolding transfer_pairs_def by blast
  obtain k' i' l' where k': "k' < length A" and i': "i' < length P" and l': "l' < length B"
    and y_eq: "y = (transfer_piece A e P g B k' i' l', transfer_map t g e k' i' l')"
    using y_in unfolding transfer_pairs_def by blast
  from nonempty obtain z where zx: "z ∈ snd x ` fst x" and zy: "z ∈ snd y ` fst y"
    by blast
  then obtain a b where
      a_piece: "a ∈ transfer_piece A e P g B k i l"
    and z_a: "z = transfer_map t g e k i l a"
    and b_piece: "b ∈ transfer_piece A e P g B k' i' l'"
    and z_b: "z = transfer_map t g e k' i' l' b"
    using x_eq y_eq by auto
  have aA: "a ∈ A ! k" and aeP: "(e ! k) a ∈ P ! i"
    and gaB: "(g ! i) ((e ! k) a) ∈ B ! l"
    using a_piece by (auto simp: transfer_piece_def)
  have bA: "b ∈ A ! k'" and beP: "(e ! k') b ∈ P ! i'"
    and gbB: "(g ! i') ((e ! k') b) ∈ B ! l'"
    using b_piece by (auto simp: transfer_piece_def)
  have lA: "l < length A" and lA': "l' < length A"
    using l l' len_AB by simp_all
  have zA_l: "z ∈ A ! l"
    using t_left[OF l gaB] z_a by (simp add: transfer_map_def)
  have zA_l': "z ∈ A ! l'"
    using t_left[OF l' gbB] z_b by (simp add: transfer_map_def)
  show False
  proof (cases "l = l'")
    case False
    have "A ! l ∩ A ! l' = {}"
      by (rule pairwise_disjoint_nthD[OF A_disj lA lA' False])
    with zA_l zA_l' show False
      by blast
  next
    case l_eq: True
    have ez_a: "(e ! l) z = (g ! i) ((e ! k) a)"
      using t_left[OF l gaB] z_a by (simp add: transfer_map_def)
    have ez_b: "(e ! l) z = (g ! i') ((e ! k') b)"
      using t_left[OF l' gbB] z_b l_eq by (simp add: transfer_map_def)
    have g_eq: "(g ! i) ((e ! k) a) = (g ! i') ((e ! k') b)"
      using ez_a ez_b by simp
    show False
    proof (cases "i = i'")
      case False then 
      have img_i: "(g ! i) ((e ! k) a) ∈ map2 (λh C. h ` C) g P ! i"
        using aeP i len by simp
      have img_i': "(g ! i') ((e ! k') b) ∈ map2 (λh C. h ` C) g P ! i'"
        using beP i' len by simp
      have "map2 (λh C. h ` C) g P ! i ∩
          map2 (λh C. h ` C) g P ! i' = {}"
        by (rule pairwise_disjoint_nthD[OF image_disj]) (use i i' False len in simp_all)
      moreover have "(g ! i) ((e ! k) a) ∈ map2 (λh C. h ` C) g P ! i'"
        using img_i' g_eq by simp
      ultimately show False
        using img_i by auto
    next
      case i_eq: True
      have e_eq: "(e ! k) a = (e ! k') b"
        using g_eq i_eq g_inj[OF i] by (auto dest: injD)
      show False
      proof (cases "k = k'")
        case False
        have kB: "k < length B" and kB': "k' < length B"
          using k k' len_AB by simp_all
        have eaB: "(e ! k) a ∈ B ! k"
          by (rule e_into_B[OF k aA])
        have ebB: "(e ! k') b ∈ B ! k'"
          by (rule e_into_B[OF k' bA])
        have "B ! k ∩ B ! k' = {}"
          by (rule pairwise_disjoint_nthD[OF B_disj kB kB' False])
        moreover have "(e ! k) a ∈ B ! k'"
          using ebB e_eq by simp
        ultimately show False
          using eaB by auto
      next
        case k_eq: True
        have "x = y"
          using x_eq y_eq k_eq i_eq l_eq by simp
        with xy show False
          by contradiction
      qed
    qed
  qed
qed

lemma transfer_partitioned_paradox:
  assumes len_AB: "length A = length B"
    and A_cover: "Y = (⋃k<length A. A ! k)"
    and A_disj: "pairwise_disjoint A"
    and B_cover: "X = (⋃k<length B. B ! k)"
    and B_disj: "pairwise_disjoint B"
    and e_left: "⋀k x. ⟦k < length A; x ∈ A ! k⟧
      ⟹ (e ! k) x ∈ B ! k ∧ (t ! k) ((e ! k) x) = x"
    and t_left: "⋀k y. ⟦k < length B; y ∈ B ! k⟧
      ⟹ (t ! k) y ∈ A ! k ∧ (e ! k) ((t ! k) y) = y"
    and lenP: "length P = length gP"
    and lenQ: "length Q = length gQ"
    and source_disj: "pairwise_disjoint (P @ Q)"
    and source_cover: "X = (⋃i<length P. P ! i) ∪ (⋃j<length Q. Q ! j)"
    and imageP_disj: "pairwise_disjoint (map2 (λh C. h ` C) gP P)"
    and imageQ_disj: "pairwise_disjoint (map2 (λh C. h ` C) gQ Q)"
    and imageP_cover: "X = (⋃i<length P. gP ! i ` (P ! i))"
    and imageQ_cover: "X = (⋃j<length Q. gQ ! j ` (Q ! j))"
    and gP_inj: "⋀i. i < length P ⟹ inj (gP ! i)"
    and gQ_inj: "⋀j. j < length Q ⟹ inj (gQ ! j)"
    and mapsP: "⋀k i l. ⟦k < length A; i < length P; l < length B⟧
      ⟹ transfer_map t gP e k i l ∈ M"
    and mapsQ: "⋀k j l. ⟦k < length A; j < length Q; l < length B⟧
      ⟹ transfer_map t gQ e k j l ∈ M"
  shows "∃P' Q' :: 'a set list. ∃gP' gQ' :: ('a ⇒ 'a) list.
      length P' = length gP' ∧ length Q' = length gQ' ∧
      set gP' ⊆ M ∧ set gQ' ⊆ M ∧
      pairwise_disjoint (P' @ Q') ∧
      pairwise_disjoint (map2 (λh C. h ` C) gP' P') ∧
      pairwise_disjoint (map2 (λh C. h ` C) gQ' Q') ∧
      Y = (⋃i<length P'. P' ! i) ∪ (⋃j<length Q'. Q' ! j) ∧
      Y = (⋃i<length P'. gP' ! i ` (P' ! i)) ∧
      Y = (⋃j<length Q'. gQ' ! j ` (Q' ! j))"
proof -
  let ?CP = "transfer_pairs A e P gP B t"
  let ?CQ = "transfer_pairs A e Q gQ B t"
  have finite_CP: "finite ?CP"
    by simp
  have finite_CQ: "finite ?CQ"
    by simp
  obtain pairsP where setP: "set pairsP = ?CP" and distinctP: "distinct pairsP"
    using finite_distinct_list[OF finite_CP] by blast
  obtain pairsQ where setQ: "set pairsQ = ?CQ" and distinctQ: "distinct pairsQ"
    using finite_distinct_list[OF finite_CQ] by blast
  let ?P' = "map fst pairsP"
  let ?Q' = "map fst pairsQ"
  let ?gP' = "map snd pairsP"
  let ?gQ' = "map snd pairsQ"

  have P_disj: "pairwise_disjoint P"
    by (rule pairwise_disjoint_appendD1[OF source_disj])
  have Q_disj: "pairwise_disjoint Q"
    by (rule pairwise_disjoint_appendD2[OF source_disj])
  have PQ_cross: "⋀i j. ⟦i < length P; j < length Q⟧ ⟹ P ! i ∩ Q ! j = {}"
    by (rule pairwise_disjoint_append_crossD[OF source_disj])

  have P'_disj: "pairwise_disjoint ?P'"
  proof (rule pairwise_disjoint_map_fstI[OF distinctP])
    fix x y
    assume "x ∈ set pairsP" "y ∈ set pairsP" "x ≠ y"
    thus "fst x ∩ fst y = {}"
      using setP transfer_source_disjoint_same[OF A_disj P_disj B_disj] by blast
  qed
  have Q'_disj: "pairwise_disjoint ?Q'"
    by (metis A_disj B_disj Q_disj distinctQ pairwise_disjoint_map_fstI setQ transfer_source_disjoint_same)
  have cross_disj: "⋀x y. ⟦x ∈ set ?P'; y ∈ set ?Q'⟧ ⟹ x ∩ y = {}"
  proof -
    fix x y
    assume x: "x ∈ set ?P'" and y: "y ∈ set ?Q'"
    then obtain px qy where px: "px ∈ set pairsP" and qy: "qy ∈ set pairsQ"
      and x_eq: "x = fst px" and y_eq: "y = fst qy"
      by auto
    show "x ∩ y = {}"
      using transfer_source_disjoint_cross[OF A_disj PQ_cross B_disj]
        setP setQ px qy x_eq y_eq by blast
  qed
  have source_disj': "pairwise_disjoint (?P' @ ?Q')"
    by (rule pairwise_disjoint_appendI[OF P'_disj Q'_disj cross_disj])

  have imageP_disj': "pairwise_disjoint (map2 (λh C. h ` C) ?gP' ?P')"
  proof (rule pairwise_disjoint_pair_imagesI[OF distinctP])
    fix x y
    assume "x ∈ set pairsP" "y ∈ set pairsP" "x ≠ y"
    thus "snd x ` fst x ∩ snd y ` fst y = {}"
      using setP transfer_image_disjoint_same[
        OF len_AB A_disj B_disj imageP_disj lenP gP_inj _ t_left]
        e_left by blast
  qed
  have imageQ_disj': "pairwise_disjoint (map2 (λh C. h ` C) ?gQ' ?Q')"
  proof (rule pairwise_disjoint_pair_imagesI[OF distinctQ])
    fix x y
    assume "x ∈ set pairsQ" "y ∈ set pairsQ" "x ≠ y"
    thus "snd x ` fst x ∩ snd y ` fst y = {}"
      using setQ transfer_image_disjoint_same[
        OF len_AB A_disj B_disj imageQ_disj lenQ gQ_inj _ t_left]
        e_left by blast
  qed

  have P_sub: "⋀i. i < length P ⟹ P ! i ⊆ X"
    using source_cover by blast
  have Q_sub: "⋀j. j < length Q ⟹ Q ! j ⊆ X"
    using source_cover by blast

  have source_cover': "Y = (⋃i<length ?P'. ?P' ! i) ∪ (⋃j<length ?Q'. ?Q' ! j)"
  proof -
    have "Y = (⋃p∈?CP. fst p) ∪ (⋃q∈?CQ. fst q)"
      by (rule transfer_source_cover[OF A_cover B_cover _ len_AB source_cover imageP_cover imageQ_cover])
        (use e_left in auto)
    also have "… = (⋃i<length ?P'. ?P' ! i) ∪ (⋃j<length ?Q'. ?Q' ! j)"
      using setP setQ indexed_union_map_fst[of pairsP] indexed_union_map_fst[of pairsQ]
      by simp
    finally show ?thesis .
  qed
  have imageP_cover': "Y = (⋃i<length ?P'. ?gP' ! i ` (?P' ! i))"
  proof -
    have "Y = (⋃p∈?CP. snd p ` fst p)"
      by (rule transfer_image_cover[OF A_cover B_cover len_AB e_left t_left P_sub imageP_cover])
    also have "… = (⋃i<length ?P'. ?gP' ! i ` (?P' ! i))"
      using setP indexed_image_union_pairs[of pairsP] by simp
    finally show ?thesis .
  qed
  have imageQ_cover': "Y = (⋃j<length ?Q'. ?gQ' ! j ` (?Q' ! j))"
  proof -
    have "Y = (⋃q∈?CQ. snd q ` fst q)"
      by (rule transfer_image_cover[OF A_cover B_cover len_AB e_left t_left Q_sub imageQ_cover])
    also have "… = (⋃j<length ?Q'. ?gQ' ! j ` (?Q' ! j))"
      using setQ indexed_image_union_pairs[of pairsQ] by simp
    finally show ?thesis .
  qed

  have mapsP': "set ?gP' ⊆ M"
    using setP mapsP unfolding transfer_pairs_def by auto
  have mapsQ': "set ?gQ' ⊆ M"
    using setQ mapsQ unfolding transfer_pairs_def by auto

  show ?thesis
  proof (intro exI conjI)
    show "length ?P' = length ?gP'"
      by simp
    show "length ?Q' = length ?gQ'"
      by simp
    show "set ?gP' ⊆ M"
      by (rule mapsP')
    show "set ?gQ' ⊆ M"
      by (rule mapsQ')
    show "pairwise_disjoint (?P' @ ?Q')"
      by (rule source_disj')
    show "pairwise_disjoint (map2 (λh C. h ` C) ?gP' ?P')"
      by (rule imageP_disj')
    show "pairwise_disjoint (map2 (λh C. h ` C) ?gQ' ?Q')"
      by (rule imageQ_disj')
    show "Y = (⋃i<length ?P'. ?P' ! i) ∪ (⋃j<length ?Q'. ?Q' ! j)"
      by (rule source_cover')
    show "Y = (⋃i<length ?P'. ?gP' ! i ` (?P' ! i))"
      by (rule imageP_cover')
    show "Y = (⋃j<length ?Q'. ?gQ' ! j ` (?Q' ! j))"
      by (rule imageQ_cover')
  qed
qed

end