Quelle  TA_Misc.thy

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
  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    proof (rule
  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›
      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> in
      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. ∀hence "[<^bold>lparr^>P<>in
      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 ≺ using oa_facts_1[deduction] bysimp
      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 ≠ he "[lbrace F\rbrace) in v]"
  qed
qed

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

  non_empty_set_has_least:
 "S ⊆ T ==> S ≠ {} ==> least S ∈ S ∧ (∀ y ∈ S. least S ≠ y ⟶ ¬ y ≺ least S)"
  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
 

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

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

  f_set:
 "S ⊆ T ==> n = card S ==> set (f S n) = S"
  (induction n arbitrary: S)
 case 0 then show ?case using finite by (auto simp: finite_subset)
 
 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
 

  f_distinct:
 "S ⊆ T ==> n = card S ==> distinct (f S n)"
  (induction n arbitrary: S)
 case 0 then show ?case using finite by (auto simp: finite_subset)
 
 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
 

  f_sorted:
 "S ⊆end
  (induction n arbitrary: S)
 case 0 then show ?case by auto
 
 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)
 

  sorted_nth_mono:
 "sorted xs ==> i < j ==> j < length xs ==> xs!i ≺ xs!j"
  (induction xs arbitrary: i j)
 case Nil thus ?case by auto
 
 case (Cons x xs)
 show ?case
 proof (cases "i = 0")
 case True
 with Con.prems sh ?th by (auto e: 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
 

  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}"
  -
 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
 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 ≺
 }
 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 ..
 

 

  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"
  -
 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) ∈
 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 ∈o_[PLM]:
 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
java.lang.NullPointerException
 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 proof -
 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 h have "(?R A,? B) ∈in> 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 ∈using qml_4[xiom_instance, con] .
 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_des'[OF **(13), of y] *(4)hav**:"?A x \noteq ?Ay" by a
 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 "…
 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 ..
 

  ‹Finiteness›

  pairwise_finiteI:
 assumes "finite {b. ∃a. P a b}" (is "finite ?B")
 es "finit {a. \exists.P a b}
 shows "finite {(a,b). P a b}" (is "finite ?C")
  -
 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)
 

  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")
  -
 have "?B ⊆ ?A" by auto
 with assms show ?thesis by (blast intro: finite_subset)
 

  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")
  -
 have "?B ⊆ ?A" by auto
 with assms show ?thesis by (blast intro: finite_subset)
 


  ‹

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

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

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

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

  distinct_zip_inj:
 "distinct ys ==> (a, b) ∈ set (zip xs ys) ==> (c, b) ∈ set (zip xs ys) ==> a = c"
  (induction ys arbitrary: xs)
 case Nil then show ?case by auto
 
 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
 

  map_of_zip_distinct_inj:
 "distinct B ==> length A = length B ==> inj_on (the o map_of (zip A B)) (set A)"
  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
 

  nat_not_ge_1D: "¬ Suc 0 ≤ x ==> x = 0" by auto

  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"
  -
 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 
 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 ..
 

  ‹Products›

  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)