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: "yset 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