Theory Timed_Automata.TA_Misc

section ‹Mixed Material›

theory TA_Misc
  imports Main HOL.Real
begin

subsection ‹Reals›

subsubsection ‹Properties of fractions›

lemma frac_add_le_preservation:
  fixes a d :: real and b :: nat
  assumes "a < b" "d < 1 - frac a"
  shows "a + d < b"
proof -
  from assms have "a + d < a + 1 - frac a" by auto
  also have "… = (a - frac a) + 1" by auto
  also have "… = floor a + 1" unfolding frac_def by auto
  also have "… ≤ b" using ‹a < b›
  by (metis floor_less_iff int_less_real_le of_int_1 of_int_add of_int_of_nat_eq) 
  finally show "a + d < b" .
qed

lemma lt_lt_1_ccontr:
  "(a :: int) < b ⟹ b < a + 1 ⟹ False" by auto

lemma int_intv_frac_gt0:
  "(a :: int) < b ⟹ b < a + 1 ⟹ frac b > 0" by auto

lemma floor_frac_add_preservation:
  fixes a d :: real
  assumes "0 < d" "d < 1 - frac a"
  shows "floor a = floor (a + d)"
proof -
  have "frac a ≥ 0" by auto
  with assms(2) have "d < 1" by linarith
  from assms have "a + d < a + 1 - frac a" by auto
  also have "… = (a - frac a) + 1" by auto
  also have "… = (floor a) + 1" unfolding frac_def by auto
  finally have *: "a + d < floor a + 1" .
  have "floor (a + d) ≥ floor a" using ‹d > 0› by linarith
  moreover from * have "floor (a + d) < floor a + 1" by linarith
  ultimately show "floor a = floor (a + d)" by auto
qed

lemma frac_distr:
  fixes a d :: real
  assumes "0 < d" "d < 1 - frac a"
  shows "frac (a + d) > 0" "frac a + d = frac (a + d)"
proof -
  have "frac a ≥ 0" by auto
  with assms(2) have "d < 1" by linarith
  from assms have "a + d < a + 1 - frac a" by auto
  also have "… = (a - frac a) + 1" by auto
  also have "… = (floor a) + 1" unfolding frac_def by auto
  finally have *: "a + d < floor a + 1" .
  have **: "floor a < a + d" using assms(1) by linarith
  have "frac (a + d) ≠ 0"
  proof (rule ccontr, auto, goal_cases)
    case 1
    then obtain b :: int where "b = a + d" by (metis Ints_cases)
    with * ** have "b < floor a + 1" "floor a < b" by auto
    with lt_lt_1_ccontr show ?case by blast
  qed
  then show "frac (a + d) > 0" by auto
  from floor_frac_add_preservation assms have "floor a = floor (a + d)" by auto
  then show "frac a + d = frac (a + d)" unfolding frac_def by force
qed

lemma frac_add_leD:
  fixes a d :: real
  assumes "0 < d" "d < 1 - frac a" "d < 1 - frac b" "frac (a + d) ≤ frac (b + d)"
  shows "frac a ≤ frac b"
proof -
  from floor_frac_add_preservation assms have
    "floor a = floor (a + d)" "floor b = floor (b + d)"
  by auto
  with assms(4) show "frac a ≤ frac b" unfolding frac_def by auto
qed

lemma floor_frac_add_preservation':
  fixes a d :: real
  assumes "0 ≤ d" "d < 1 - frac a"
  shows "floor a = floor (a + d)"
using assms floor_frac_add_preservation by (cases "d = 0") auto

lemma frac_add_leIFF:
  fixes a d :: real
  assumes "0 ≤ d" "d < 1 - frac a" "d < 1 - frac b"
  shows "frac a ≤ frac b ⟷ frac (a + d) ≤ frac (b + d)"
proof -
  from floor_frac_add_preservation' assms have
    "floor a = floor (a + d)" "floor b = floor (b + d)"
  by auto
  then show ?thesis unfolding frac_def by auto
qed

lemma nat_intv_frac_gt0:
  fixes c :: nat fixes x :: real
  assumes "c < x" "x < real (c + 1)"
  shows "frac x > 0"
proof (rule ccontr, auto, goal_cases)
  case 1
  then obtain d :: int where d: "x = d" by (metis Ints_cases)
  with assms have "c < d" "d < int c + 1" by auto
  with int_intv_frac_gt0[OF this] 1 d show False by auto
qed

lemma nat_intv_frac_decomp:
  fixes c :: nat and d :: real
  assumes "c < d" "d < c + 1"
  shows "d = c + frac d"
proof -
  from assms have "int c = ⌊d⌋" by linarith
  thus ?thesis by (simp add: frac_def)
qed

lemma nat_intv_not_int:
  fixes c :: nat
  assumes "real c < d" "d < c + 1"
  shows "d ∉ ℤ"
proof (standard, goal_cases)
  case 1
  then obtain k :: int where "d = k" using Ints_cases by auto
  then have "frac d = 0" by auto
  moreover from nat_intv_frac_decomp[OF assms] have *: "d = c + frac d" by auto
  ultimately have "d = c" by linarith
  with assms show ?case by auto
qed

lemma frac_nat_add_id: "frac ((n :: nat) + (r :: real)) = frac r" ― ‹Found by sledgehammer›
proof -
  have "⋀r. frac (r::real) < 1"
    by (meson frac_lt_1)
  then show ?thesis
    by (simp add: floor_add frac_def)
qed

lemma floor_nat_add_id: "0 ≤ (r :: real) ⟹ r < 1 ⟹ floor (real (n::nat) + r) = n" by linarith

lemma int_intv_frac_gt_0':
  "(a :: real) ∈ ℤ ⟹ (b :: real) ∈ ℤ ⟹ a ≤ b ⟹ a ≠ b ⟹ a ≤ b - 1"
proof (goal_cases)
  case 1
  then have "a < b" by auto
  from 1(1,2) obtain k l :: int where "a = real_of_int k" "b = real_of_int l" by (metis Ints_cases)
  with ‹a < b› show ?case by auto
qed

lemma int_lt_Suc_le:
  "(a :: real) ∈ ℤ ⟹ (b :: real) ∈ ℤ ⟹ a < b + 1 ⟹ a ≤ b"
proof (goal_cases)
  case 1
  from 1(1,2) obtain k l :: int where "a = real_of_int k" "b = real_of_int l" by (metis Ints_cases)
  with ‹a < b + 1› show ?case by auto
qed

lemma int_lt_neq_Suc_lt:
  "(a :: real) ∈ ℤ ⟹ (b :: real) ∈ ℤ ⟹ a < b ⟹ a + 1 ≠ b ⟹ a + 1 < b"
proof (goal_cases)
  case 1
  from 1(1,2) obtain k l :: int where "a = real_of_int k" "b = real_of_int l" by (metis Ints_cases)
  with 1 show ?case by auto
qed

lemma int_lt_neq_prev_lt:
  "(a :: real) ∈ ℤ ⟹ (b :: real) ∈ ℤ ⟹ a - 1 < b ⟹ a ≠ b ⟹ a < b"
proof (goal_cases)
  case 1
  from 1(1,2) obtain k l :: int where "a = real_of_int k" "b = real_of_int l" by (metis Ints_cases)
  with 1 show ?case by auto
qed

lemma ints_le_add_frac1:
  fixes a b x :: real
  assumes "0 < x" "x < 1" "a ∈ ℤ" "b ∈ ℤ" "a + x ≤ b"
  shows "a ≤ b"
using assms by auto

lemma ints_le_add_frac2:
  fixes a b x :: real
  assumes "0 ≤ x" "x < 1" "a ∈ ℤ" "b ∈ ℤ" "b ≤ a + x"
  shows "b ≤ a"
using assms
by (metis add.commute add_le_cancel_left add_mono_thms_linordered_semiring(1) int_lt_Suc_le leD le_less_linear)

subsection ‹Ordering Fractions›

lemma distinct_twice_contradiction:
  "xs ! i = x ⟹ xs ! j = x ⟹ i < j ⟹ j < length xs ⟹ ¬ distinct xs"
proof (rule ccontr, simp, induction xs arbitrary: i j)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  show ?case
  proof (cases "i = 0")
    case True
    with Cons have "y = x" by auto
    moreover from True Cons have "x ∈ set xs" by auto
    ultimately show False using Cons(6) by auto
  next
    case False
    with Cons have
      "xs ! (i - 1) = x" "xs ! (j - 1) = x" "i - 1 < j - 1" "j - 1 < length xs" "distinct xs"
    by auto
    from Cons.IH[OF this] show False .
  qed
qed

lemma distinct_nth_unique:
  "xs ! i = xs ! j ⟹ i < length xs ⟹ j < length xs ⟹ distinct xs ⟹ i = j"
  apply (rule ccontr)
  apply (cases "i < j")
  apply auto
  apply (auto dest: distinct_twice_contradiction)
using distinct_twice_contradiction by fastforce

lemma (in linorder) linorder_order_fun:
  fixes S :: "'a set"
  assumes "finite S"
  obtains f :: "'a ⇒ nat"
  where "(∀ x ∈ S. ∀ y ∈ S. f x ≤ f y ⟷ x ≤ y)" and "range f ⊆ {0..card S - 1}"
proof -
  obtain l where l_def: "l = sorted_list_of_set S" by auto
  with sorted_list_of_set(1)[OF assms] have l: "set l = S" "sorted l" "distinct l"
    by auto
  from l(1,3) ‹finite S› have len: "length l = card S" using distinct_card by force 
  let ?f = "λ x. if x ∉ S then 0 else THE i. i < length l ∧ l ! i = x"
  { fix x y assume A: "x ∈ S" "y ∈ S" "x < y"
    with l(1) obtain i j where *: "l ! i = x" "l ! j = y" "i < length l" "j < length l"
    by (meson in_set_conv_nth)
    have "i < j"
    proof (rule ccontr, goal_cases)
      case 1
      with sorted_nth_mono[OF l(2)] ‹i < length l› have "l ! j ≤ l ! i" by auto
      with * A(3) show False by auto
    qed
    moreover have "?f x = i" using * l(3) A(1) by (auto) (rule, auto intro: distinct_nth_unique)
    moreover have "?f y = j" using * l(3) A(2) by (auto) (rule, auto intro: distinct_nth_unique)
    ultimately have "?f x < ?f y" by auto
  } moreover
  { fix x y assume A: "x ∈ S" "y ∈ S" "?f x < ?f y"
    with l(1) obtain i j where *: "l ! i = x" "l ! j = y" "i < length l" "j < length l"
    by (meson in_set_conv_nth)
    moreover have "?f x = i" using * l(3) A(1) by (auto) (rule, auto intro: distinct_nth_unique)
    moreover have "?f y = j" using * l(3) A(2) by (auto) (rule, auto intro: distinct_nth_unique)
    ultimately have **: "l ! ?f x = x" "l ! ?f y = y" "i < j" using A(3) by auto
    have "x < y"
    proof (rule ccontr, goal_cases)
      case 1
      then have "y ≤ x" by simp
      moreover from sorted_nth_mono[OF l(2), of i j] **(3) * have "x ≤ y" by auto
      ultimately show False using distinct_nth_unique[OF _ *(3,4) l(3)] *(1,2) **(3) by fastforce
    qed
  }
  ultimately have "∀ x ∈ S. ∀ y ∈ S. ?f x ≤ ?f y ⟷ x ≤ y" by force
  moreover have "range ?f ⊆ {0..card S - 1}"
  proof (auto, goal_cases)
    case (1 x)
    with l(1) obtain i where *: "l ! i = x" "i < length l" by (meson in_set_conv_nth)
    then have "?f x = i" using l(3) 1 by (auto) (rule, auto intro: distinct_nth_unique)
    with len show ?case using *(2) 1 by auto
  qed
  ultimately show ?thesis ..
qed

locale enumerateable =
  fixes T :: "'a set"
  fixes less :: "'a ⇒ 'a ⇒ bool" (infix ‹≺› 50)
  assumes finite: "finite T"
  assumes total:  "∀ x ∈ T. ∀ y ∈ T. x ≠ y ⟶ (x ≺ y) ∨ (y ≺ x)"
  assumes trans:  "∀x ∈ T. ∀ y ∈ T. ∀ z ∈ T. (x :: 'a) ≺ y ⟶ y ≺ z ⟶ x ≺ z"
  assumes asymmetric: "∀ x ∈ T. ∀ y ∈ T. x ≺ y ⟶ ¬ (y ≺ x)"
begin

lemma non_empty_set_has_least':
  "S ⊆ T ⟹ S ≠ {} ⟹ ∃ x ∈ S. ∀ y ∈ S. x ≠ y ⟶ ¬ y ≺ x"
proof (rule ccontr, induction "card S" arbitrary: S)
  case 0 then show ?case using finite by (auto simp: finite_subset)
next
  case (Suc n)
  then obtain x where x: "x ∈ S" by blast
  from finite Suc.prems(1) have finite: "finite S" by (auto simp: finite_subset)
  let ?S = "S - {x}"
  show ?case
  proof (cases "S = {x}")
    case True
    with Suc.prems(3) show False by auto
  next
    case False
    then have S: "?S ≠ {}" using x by blast
    show False
    proof (cases "∃x ∈ ?S. ∀y∈?S. x ≠ y ⟶ ¬ y ≺ x")
      case False
      have "n = card ?S" using Suc.hyps finite by (simp add: x)
      from Suc.hyps(1)[OF this _ S False] Suc.prems(1) show False by auto
    next
      case True
      then obtain x' where x': "∀y∈?S. x' ≠ y ⟶ ¬ y ≺ x'" "x' ∈ ?S" "x ≠ x'" by auto
      from total Suc.prems(1) x'(2) have "⋀ y. y ∈ S ⟹ x' ≠ y ⟹ ¬ y ≺ x' ⟹ x' ≺ y" by auto
      from total Suc.prems(1) x'(1,2) have *: "∀ y ∈ ?S. x' ≠ y ⟶ x' ≺ y" by auto
      from Suc.prems(3) x'(1,2) have **: "x ≺ x'" by auto
      have "∀ y ∈ ?S. x ≺ y"
      proof
        fix y assume y: "y ∈ S - {x}"
        show "x ≺ y"
        proof (cases "y = x'")
          case True then show ?thesis using ** by simp
        next
          case False
          with * y have "x' ≺ y" by auto
          with trans Suc.prems(1) ** y x'(2) x ** show ?thesis by auto
        qed
      qed
      with x Suc.prems(1,3) show False using asymmetric by blast
    qed
  qed
qed

lemma non_empty_set_has_least'':
  "S ⊆ T ⟹ S ≠ {} ⟹ ∃! x ∈ S. ∀ y ∈ S. x ≠ y ⟶ ¬ y ≺ x"
proof (intro ex_ex1I, goal_cases)
  case 1
  with non_empty_set_has_least'[OF this] show ?case by auto
next
  case (2 x y)
  show ?case
  proof (rule ccontr)
    assume "x ≠ y"
    with 2 total have "x ≺ y ∨ y ≺ x" by blast
    with 2(2-) ‹x ≠ y› show False by auto
  qed
qed

abbreviation "least S ≡ THE t :: 'a. t ∈ S ∧ (∀ y ∈ S. t ≠ y ⟶ ¬ y ≺ t)"

lemma non_empty_set_has_least:
  "S ⊆ T ⟹ S ≠ {} ⟹ least S ∈ S ∧ (∀ y ∈ S. least S ≠ y ⟶ ¬ y ≺ least S)"
proof goal_cases
  case 1
  note A = this
  show ?thesis
  proof (rule theI', goal_cases)
    case 1
    from non_empty_set_has_least''[OF A] show ?case .
  qed
qed

fun f :: "'a set ⇒ nat ⇒ 'a list"
where
  "f S 0 = []" |
  "f S (Suc n) = least S # f (S - {least S}) n"

inductive sorted :: "'a list ⇒ bool" where
  Nil [iff]: "sorted []"
| Cons: "∀y∈set xs. x ≺ y ⟹ sorted xs ⟹ sorted (x # xs)"

lemma f_set:
  "S ⊆ T ⟹ n = card S ⟹ set (f S n) = S"
proof (induction n arbitrary: S)
  case 0 then show ?case using finite by (auto simp: finite_subset)
next
  case (Suc n)
  then have fin: "finite S" using finite by (auto simp: finite_subset)
  with Suc.prems have "S ≠ {}" by auto
  from non_empty_set_has_least[OF Suc.prems(1) this] have least: "least S ∈ S" by blast
  let ?S = "S - {least S}"
  from fin least Suc.prems have "?S ⊆ T" "n = card ?S" by auto
  from Suc.IH[OF this] have "set (f ?S n) = ?S" .
  with least show ?case by auto
qed

lemma f_distinct:
  "S ⊆ T ⟹ n = card S ⟹ distinct (f S n)"
proof (induction n arbitrary: S)
  case 0 then show ?case using finite by (auto simp: finite_subset)
next
  case (Suc n)
  then have fin: "finite S" using finite by (auto simp: finite_subset)
  with Suc.prems have "S ≠ {}" by auto
  from non_empty_set_has_least[OF Suc.prems(1) this] have least: "least S ∈ S" by blast
  let ?S = "S - {least S}"
  from fin least Suc.prems have "?S ⊆ T" "n = card ?S" by auto
  from Suc.IH[OF this] f_set[OF this] have "distinct (f ?S n)" "set (f ?S n) = ?S" .
  then show ?case by simp
qed

lemma f_sorted:
  "S ⊆ T ⟹ n = card S ⟹ sorted (f S n)"
proof (induction n arbitrary: S)
  case 0 then show ?case by auto
next
  case (Suc n)
  then have fin: "finite S" using finite by (auto simp: finite_subset)
  with Suc.prems have "S ≠ {}" by auto
  from non_empty_set_has_least[OF Suc.prems(1) this] have least:
    "least S ∈ S" "(∀ y ∈ S. least S ≠ y ⟶ ¬ y ≺ least S)"
  by blast+
  let ?S = "S - {least S}"
  { fix x assume x: "x ∈ ?S"
    with least have "¬ x ≺ least S" by auto
    with total x Suc.prems(1) least(1) have "least S ≺ x" by blast
  } note le = this
  from fin least Suc.prems have "?S ⊆ T" "n = card ?S" by auto
  from f_set[OF this] Suc.IH[OF this] have *: "set (f ?S n) = ?S" "sorted (f ?S n)" .
  with le have "∀ x ∈ set (f ?S n). least S ≺ x" by auto
  with *(2) show ?case by (auto intro: Cons)
qed

lemma sorted_nth_mono:
  "sorted xs ⟹ i < j ⟹ j < length xs ⟹ xs!i ≺ xs!j"
proof (induction xs arbitrary: i j)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  show ?case
  proof (cases "i = 0")
    case True
    with Cons.prems show ?thesis by (auto elim: sorted.cases)
  next
    case False
    from Cons.prems have "sorted xs" by (auto elim: sorted.cases)
    from Cons.IH[OF this] Cons.prems False show ?thesis by auto
  qed
qed

lemma order_fun:
  fixes S :: "'a set"
  assumes "S ⊆ T"
  obtains f :: "'a ⇒ nat" where "∀ x ∈ S. ∀ y ∈ S. f x < f y ⟷ x ≺ y" and "range f ⊆ {0..card S - 1}"
proof -
  obtain l where l_def: "l = f S (card S)" by auto
  with f_set f_distinct f_sorted assms have l: "set l = S" "sorted l" "distinct l" by auto
  then have len: "length l = card S" using distinct_card by force
  let ?f = "λ x. if x ∉ S then 0 else THE i. i < length l ∧ l ! i = x"
  { fix x y :: 'a assume A: "x ∈ S" "y ∈ S" "x ≺ y"
    with l(1) obtain i j where *: "l ! i = x" "l ! j = y" "i < length l" "j < length l"
    by (meson in_set_conv_nth)
    have "i ≠ j"
    proof (rule ccontr, goal_cases)
      case 1
      with A * have "x ≺ x" by auto
      with asymmetric A assms show False by auto
    qed
    have "i < j"
    proof (rule ccontr, goal_cases)
      case 1
      with ‹i ≠ j› sorted_nth_mono[OF l(2)] ‹i < length l› have "l ! j ≺ l ! i" by auto
      with * A(3) A assms asymmetric show False by auto
    qed
    moreover have "?f x = i" using * l(3) A(1) by (auto) (rule, auto intro: distinct_nth_unique)
    moreover have "?f y = j" using * l(3) A(2) by (auto) (rule, auto intro: distinct_nth_unique)
    ultimately have "?f x < ?f y" by auto
  } moreover
  { fix x y assume A: "x ∈ S" "y ∈ S" "?f x < ?f y"
    with l(1) obtain i j where *: "l ! i = x" "l ! j = y" "i < length l" "j < length l"
    by (meson in_set_conv_nth)
    moreover have "?f x = i" using * l(3) A(1) by (auto) (rule, auto intro: distinct_nth_unique)
    moreover have "?f y = j" using * l(3) A(2) by (auto) (rule, auto intro: distinct_nth_unique)
    ultimately have **: "l ! ?f x = x" "l ! ?f y = y" "i < j" using A(3) by auto
    from sorted_nth_mono[OF l(2), of i j] **(3) * have "x ≺ y" by auto
  }
  ultimately have "∀ x ∈ S. ∀ y ∈ S. ?f x < ?f y ⟷ x ≺ y" by force
  moreover have "range ?f ⊆ {0..card S - 1}"
  proof (auto, goal_cases)
    case (1 x)
    with l(1) obtain i where *: "l ! i = x" "i < length l" by (meson in_set_conv_nth)
    then have "?f x = i" using l(3) 1 by (auto) (rule, auto intro: distinct_nth_unique)
    with len show ?case using *(2) 1 by auto
  qed
  ultimately show ?thesis ..
qed

end

lemma finite_total_preorder_enumeration:
  fixes X :: "'a set"
  fixes r :: "'a rel"
  assumes fin:   "finite X"
  assumes tot:   "total_on X r"
  assumes refl:  "refl_on X r"
  assumes trans: "trans r"
  obtains f :: "'a ⇒ nat" where "∀ x ∈ X. ∀ y ∈ X. f x ≤ f y ⟷ (x, y) ∈ r"
proof -
  let ?A = "λ x. {y ∈ X . (y, x) ∈ r ∧ (x, y) ∈ r}"
  have ex: "∀ x ∈ X. x ∈ ?A x" using refl unfolding refl_on_def by auto
  let ?R = "λ S. SOME y. y ∈ S"
  let ?T = "{?A x | x.  x ∈ X}"
  { fix A assume A: "A ∈ ?T"
    then obtain x where x: "x ∈ X" "?A x = A" by auto
    then have "x ∈ A" using refl unfolding refl_on_def by auto
    then have "?R A ∈ A" by (auto intro: someI)
    with x(2) have "(?R A, x) ∈ r" "(x, ?R A) ∈ r" by auto
    with trans have "(?R A, ?R A) ∈ r" unfolding trans_def by blast
  } note refl_lifted = this
  { fix A assume A: "A ∈ ?T"
    then obtain x where x: "x ∈ X" "?A x = A" by auto
    then have "x ∈ A" using refl unfolding refl_on_def by auto
    then have "?R A ∈ A" by (auto intro: someI)
  } note R_in = this
  { fix A y z assume A: "A ∈ ?T" and y: "y ∈ A" and z: "z ∈ A"
    from A obtain x where x: "x ∈ X" "?A x = A" by auto
    then have "x ∈ A" using refl unfolding refl_on_def by auto
    with x y have "(x, y) ∈ r" "(y, x) ∈ r" by auto
    moreover from x z have "(x,z) ∈ r" "(z,x) ∈ r" by auto
    ultimately have "(y, z) ∈ r" "(z, y) ∈ r" using trans unfolding trans_def by blast+
  } note A_dest' = this
  { fix A y assume "A ∈ ?T" and "y ∈ A"
    with A_dest'[OF _ _ R_in] have "(?R A, y) ∈ r" "(y, ?R A) ∈ r" by blast+
  } note A_dest = this
  { fix A y z assume A: "A ∈ ?T" and y: "y ∈ A" and z: "z ∈ X" and r: "(y, z) ∈ r" "(z, y) ∈ r"
    from A obtain x where x: "x ∈ X" "?A x = A" by auto
    then have "x ∈ A" using refl unfolding refl_on_def by auto
    with x y have "(x,y) ∈ r" "(y, x) ∈ r" by auto
    with r have "(x,z) ∈ r" "(z,x) ∈ r" using trans unfolding trans_def by blast+
    with x z have "z ∈ A" by auto
  } note A_intro' = this
  { fix A y assume A: "A ∈ ?T" and y: "y ∈ X" and r: "(?R A, y) ∈ r" "(y, ?R A) ∈ r"
    with A_intro' R_in have "y ∈ A" by blast
  } note A_intro = this
  { fix A B C
    assume r1: "(?R A, ?R B) ∈ r" and r2: "(?R B, ?R C) ∈ r"
    with trans have "(?R A, ?R C) ∈ r" unfolding trans_def by blast
  } note trans_lifted[intro] = this
  { fix A B a b
    assume A: "A ∈ ?T" and B: "B ∈ ?T"
    and a: "a ∈ A" and b: "b ∈ B"
    and r: "(a, b) ∈ r" "(b, a) ∈ r"
    with R_in have "?R A ∈ A" "?R B ∈ B" by blast+
    have "A = B"
    proof auto
      fix x assume x: "x ∈ A"
      with A have "x ∈ X" by auto
      from A_intro'[OF B b this] A_dest'[OF A x a] r trans[unfolded trans_def] show "x ∈ B" by blast
    next
      fix x assume x: "x ∈ B"
      with B have "x ∈ X" by auto
      from A_intro'[OF A a this] A_dest'[OF B x b] r trans[unfolded trans_def] show "x ∈ A" by blast
    qed
  } note eq_lifted'' = this
  { fix A B C
    assume A: "A ∈ ?T" and B: "B ∈ ?T" and r: "(?R A, ?R B) ∈ r" "(?R B, ?R A) ∈ r"
    with eq_lifted'' R_in have "A = B" by blast
  } note eq_lifted' = this
  { fix A B C
    assume A: "A ∈ ?T" and B: "B ∈ ?T" and eq: "?R A = ?R B"
    from R_in[OF A] A have "?R A ∈ X" by auto
    with refl have "(?R A, ?R A) ∈ r" unfolding refl_on_def by auto
    with eq_lifted'[OF A B] eq have "A = B" by auto
  } note eq_lifted = this
  { fix A B
    assume A: "A ∈ ?T" and B: "B ∈ ?T" and neq: "A ≠ B"
    from neq eq_lifted[OF A B] have "?R A ≠ ?R B" by metis
    moreover from A B R_in have "?R A ∈ X" "?R B ∈ X" by auto
    ultimately have "(?R A, ?R B) ∈ r ∨ (?R B, ?R A) ∈ r" using tot unfolding total_on_def by auto
  } note total_lifted = this
  { fix x y assume x: "x ∈ X" and y: "y ∈ X"
    from x y have "?A x ∈ ?T" "?A y ∈ ?T" by auto
    from R_in[OF this(1)] R_in[OF this(2)] have "?R (?A x) ∈ ?A x" "?R (?A y) ∈ ?A y" by auto
    then have "(x, ?R (?A x)) ∈ r" "(?R (?A y), y) ∈ r" "(?R (?A x), x) ∈ r" "(y, ?R (?A y)) ∈ r" by auto
    with trans[unfolded trans_def] have "(x, y) ∈ r ⟷ (?R (?A x), ?R (?A y)) ∈ r" by meson
  } note repr = this
  interpret interp: enumerateable "{?A x | x.  x ∈ X}" "λ A B. A ≠ B ∧ (?R A, ?R B) ∈ r"
  proof (standard, goal_cases)
    case 1
    from fin show ?case by auto
  next
    case 2
    with total_lifted show ?case by auto
  next
    case 3
    then show ?case unfolding transp_def
    proof (standard, standard, standard, standard, standard, goal_cases)
      case (1 A B C)
      note A = this
      with trans_lifted have "(?R A,?R C) ∈ r" by blast
      moreover have "A ≠ C"
      proof (rule ccontr, goal_cases)
        case 1
        with A have "(?R A,?R B) ∈ r" "(?R B,?R A) ∈ r" by auto
        with eq_lifted'[OF A(1,2)] A show False by auto
      qed
      ultimately show ?case by auto
    qed
  next
    case 4
    { fix A B assume A: "A ∈ ?T" and B: "B ∈ ?T" and neq: "A ≠ B" "(?R A, ?R B) ∈ r"
      with eq_lifted'[OF A B] neq have "¬ (?R B, ?R A) ∈ r" by auto
    }
    then show ?case by auto
  qed
  from interp.order_fun[OF subset_refl] obtain f :: "'a set ⇒ nat" where
    f: "∀ x ∈ ?T. ∀ y ∈ ?T. f x < f y ⟷ x ≠ y ∧ (?R x, ?R y) ∈ r" "range f ⊆ {0..card ?T - 1}"
  by auto
  let ?f = "λ x. if x ∈ X then f (?A x) else 0"
  { fix x y assume x: "x ∈ X" and y: "y ∈ X"
    have "?f x ≤ ?f y ⟷ (x, y) ∈ r"
    proof (cases "x = y")
      case True
      with refl x show ?thesis unfolding refl_on_def by auto
    next
      case False
      note F = this
      from ex x y have *: "?A x ∈ ?T" "?A y ∈ ?T" "x ∈ ?A x" "y ∈ ?A y" by auto
      show ?thesis
      proof (cases "(x, y) ∈ r ∧ (y, x) ∈ r")
        case True
        from eq_lifted''[OF *] True x y have "?f x = ?f y" by auto
        with True show ?thesis by auto
      next
        case False
        with A_dest'[OF *(1,3), of y] *(4) have **: "?A x ≠ ?A y" by auto
        from total_lifted[OF *(1,2) this] have "(?R (?A x), ?R (?A y)) ∈ r ∨ (?R (?A y), ?R (?A x)) ∈ r" .
        then have neq: "?f x ≠ ?f y"
        proof (standard, goal_cases)
          case 1
          with f *(1,2) ** have "f (?A x) < f (?A y)" by auto
          with * show ?case by auto
        next
          case 2
          with f *(1,2) ** have "f (?A y) < f (?A x)" by auto
          with * show ?case by auto
        qed
        then have "?thesis = (?f x < ?f y ⟷ (x, y) ∈ r)" by linarith
        moreover from f ** * have "(?f x < ?f y ⟷ (?R (?A x), ?R (?A y)) ∈ r)" by auto
        moreover from repr * have "… ⟷ (x, y) ∈ r" by auto
        ultimately show ?thesis by auto
      qed
    qed
  }
  then have "∀ x ∈ X. ∀ y ∈ X. ?f x ≤ ?f y ⟷ (x, y) ∈ r" by blast
  then show ?thesis ..
qed

subsection ‹Finiteness›

lemma pairwise_finiteI:
  assumes "finite {b. ∃a. P a b}" (is "finite ?B")
  assumes "finite {a. ∃b. P a b}"
  shows "finite {(a,b). P a b}" (is "finite ?C")
proof -
  from assms(1) have "finite ?B" .
  let ?f = "λ b. {(a,b) | a. P a b}"
  { fix b
    have "?f b ⊆ {(a,b) | a. ∃b. P a b}" by blast
    moreover have "finite …" using assms(2) by auto 
    ultimately have "finite (?f b)" by (blast intro: finite_subset)
  }
  with assms(1) have "finite (⋃ (?f ` ?B))" by auto
  moreover have "?C ⊆ ⋃ (?f ` ?B)" by auto
  ultimately show ?thesis by (blast intro: finite_subset)
qed

lemma finite_ex_and1:
  assumes "finite {b. ∃a. P a b}" (is "finite ?A")
  shows "finite {b. ∃a. P a b ∧ Q a b}" (is "finite ?B")
proof -
  have "?B ⊆ ?A" by auto
  with assms show ?thesis by (blast intro: finite_subset)
qed

lemma finite_ex_and2:
  assumes "finite {b. ∃a. Q a b}" (is "finite ?A")
  shows "finite {b. ∃a. P a b ∧ Q a b}" (is "finite ?B")
proof -
  have "?B ⊆ ?A" by auto
  with assms show ?thesis by (blast intro: finite_subset)
qed


subsection ‹Numbering the elements of finite sets›

lemma upt_last_append: "a ≤ b ⟹ [a..<b] @ [b] = [a ..< Suc b]" by (induction b) auto

lemma map_of_zip_dom_to_range:
  "a ∈ set A ⟹ length B = length A ⟹ the (map_of (zip A B) a) ∈ set B"
by (metis map_of_SomeD map_of_zip_is_None option.collapse set_zip_rightD)

lemma zip_range_id:
  "length A = length B ⟹ snd ` set (zip A B) = set B"
by (metis map_snd_zip set_map)

lemma map_of_zip_in_range:
  "distinct A ⟹ length B = length A ⟹ b ∈ set B ⟹ ∃ a ∈ set A. the (map_of (zip A B) a) = b"
proof goal_cases
  case 1
  from ran_distinct[of "zip A B"] 1(1,2) have
    "ran (map_of (zip A B)) = set B"
  by (auto simp: zip_range_id)
  with 1(3) obtain a where "map_of (zip A B) a = Some b" unfolding ran_def by auto
  with map_of_zip_is_Some[OF 1(2)[symmetric]] have "the (map_of (zip A B) a) = b" "a ∈ set A" by auto
  then show ?case by blast
qed

lemma distinct_zip_inj:
  "distinct ys ⟹ (a, b) ∈ set (zip xs ys) ⟹ (c, b) ∈ set (zip xs ys) ⟹ a = c"
proof (induction ys arbitrary: xs)
  case Nil then show ?case by auto
next
  case (Cons y ys)
  from this(3) have "xs ≠ []" by auto
  then obtain z zs where xs: "xs = z # zs" by (cases xs) auto
  show ?case
  proof (cases "(a, b) ∈ set (zip zs ys)")
    case True
    note T = this
    then have b: "b ∈ set ys" by (meson in_set_zipE) 
    show ?thesis
    proof (cases "(c, b) ∈ set (zip zs ys)")
      case True
      with T Cons show ?thesis by auto
    next
      case False
      with Cons.prems xs b show ?thesis by auto
    qed
  next
    case False
    with Cons.prems xs have b: "a = z" "b = y" by auto
    show ?thesis
    proof (cases "(c, b) ∈ set (zip zs ys)")
      case True
      then have "b ∈ set ys" by (meson in_set_zipE)
      with b ‹distinct (y#ys)› show ?thesis by auto
    next
      case False
      with Cons.prems xs b show ?thesis by auto
    qed
  qed
qed

lemma map_of_zip_distinct_inj:
  "distinct B ⟹ length A = length B ⟹ inj_on (the o map_of (zip A B)) (set A)"
unfolding inj_on_def proof (clarify, goal_cases)
  case (1 x y)
  with map_of_zip_is_Some[OF 1(2)] obtain a where
    "map_of (zip A B) x = Some a" "map_of (zip A B) y = Some a"
  by auto
  then have "(x, a) ∈ set (zip A B)" "(y, a) ∈ set (zip A B)" using map_of_SomeD by metis+
  from distinct_zip_inj[OF _ this] 1 show ?case by auto
qed

lemma nat_not_ge_1D: "¬ Suc 0 ≤ x ⟹ x = 0" by auto

lemma standard_numbering:
  assumes "finite A"
  obtains v :: "'a ⇒ nat" and n where "bij_betw v A {1..n}"
  and "∀ c ∈ A. v c > 0"
  and "∀ c. c ∉ A ⟶ v c > n"
proof -
  from assms obtain L where L: "distinct L" "set L = A" by (meson finite_distinct_list)
  let ?N = "length L + 1"
  let ?P = "zip L [1..<?N]"
  let ?v = "λ x. let v = map_of ?P x in if v = None then ?N else the v"
  from length_upt have len: "length [1..<?N] = length L" by auto (cases L, auto)
  then have lsimp: "length [Suc 0 ..<Suc (length L)] = length L" by simp
  note * = map_of_zip_dom_to_range[OF _ len]
  have "bij_betw ?v A {1..length L}" unfolding bij_betw_def
  proof
    show "?v ` A = {1..length L}" apply auto
      apply (auto simp: L)[] 
      apply (auto simp only: upt_last_append)[] using * apply force
      using * apply (simp only: upt_last_append) apply force
      apply (simp only: upt_last_append) using L(2) apply (auto dest: nat_not_ge_1D)
      apply (subgoal_tac "x ∈ set [1..< length L +1]")
      apply (force dest!: map_of_zip_in_range[OF L(1) len])
      apply auto
    done
  next
    from L map_of_zip_distinct_inj[OF distinct_upt, of L 1 "length L + 1"] len
    have "inj_on (the o map_of ?P) A" by auto
    moreover have "inj_on (the o map_of ?P) A = inj_on ?v A"
    using len L(2) by - (rule inj_on_cong, auto)
    ultimately show "inj_on ?v A" by blast
  qed
  moreover have "∀ c ∈ A. ?v c > 0"
  proof
    fix c
    show "?v c > 0"
    proof (cases "c ∈ set L")
      case False
      then show ?thesis by auto
    next
      case True
      with dom_map_of_zip[OF len[symmetric]] obtain x where
        "Some x = map_of ?P c" "x ∈ set [1..<length L + 1]"
      by (metis * domIff option.collapse)
      then have "?v c ∈ set [1..<length L + 1]" using * True len by auto
      then show ?thesis by auto
    qed
  qed
  moreover have "∀ c. c ∉ A ⟶ ?v c > length L" using L by auto
  ultimately show ?thesis ..
qed

subsection ‹Products›

lemma prod_set_fst_id:
  "x = y" if "∀ a ∈ x. fst a = b" "∀ a ∈ y. fst a = b" "snd ` x = snd ` y"
  using that by (auto 4 6 simp: fst_def snd_def image_def split: prod.splits)

end