(*<*) theory Misc imports Complex_Main begin chapter ‹Basic lemmas which do not belong to the particular domain of Timed Automata› section ‹Reals› subsection ‹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_idempotent: "frac (frac x) = frac x" by (simp add: frac_eq frac_lt_1) 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) section ‹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 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 section ‹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 lemma finite_set_of_finite_funs2: fixes A :: "'a set" and B :: "'b set" and C :: "'c set" and d :: "'c" assumes "finite A" and "finite B" and "finite C" shows "finite {f. ∀x. ∀y. (x ∈ A ∧ y ∈ B ⟶ f x y ∈ C) ∧ (x ∉ A ⟶ f x y = d) ∧ (y ∉ B ⟶ f x y = d)}" proof - let ?S = "{f. ∀x. ∀y. (x ∈ A ∧ y ∈ B ⟶ f x y ∈ C) ∧ (x ∉ A ⟶ f x y = d) ∧ (y ∉ B ⟶ f x y = d)}" let ?R = "{g. ∀x. (x ∈ B ⟶ g x ∈ C) ∧ (x ∉ B ⟶ g x = d)}" let ?Q = "{f. ∀x. (x ∈ A ⟶ f x ∈ ?R) ∧ (x ∉ A ⟶ f x = (λy. d))}" from finite_set_of_finite_funs[OF assms(2,3)] have "finite ?R" . from finite_set_of_finite_funs[OF assms(1) this, of "λ y. d"] have "finite ?Q" . moreover have "?S = ?Q" by auto (case_tac "xa ∈ A", auto) ultimately show ?thesis by simp qed section ‹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 end (*>*)