Theory MFMC_Countable.MFMC_Misc

(* Author: Andreas Lochbihler, ETH Zurich *)

section ‹Preliminaries›

theory MFMC_Misc imports
  "HOL-Probability.Probability"
  "HOL-Library.Transitive_Closure_Table"
  "HOL-Library.Complete_Partial_Order2"
  "HOL-Library.Bourbaki_Witt_Fixpoint"
begin

hide_const (open) cycle
hide_const (open) path
hide_const (open) cut
hide_const (open) orthogonal

lemmas disjE [consumes 1, case_names left right, cases pred] = disjE

lemma inj_on_Pair2 [simp]: "inj_on (Pair x) A"
by(simp add: inj_on_def)

lemma inj_on_Pair1 [simp]: "inj_on (λx. (x, y)) A"
by(simp add: inj_on_def)

lemma inj_map_prod': "⟦ inj f; inj g ⟧ ⟹ inj_on (map_prod f g) X"
by(rule subset_inj_on[OF prod.inj_map subset_UNIV])

lemma not_range_Inr: "x ∉ range Inr ⟷ x ∈ range Inl"
by(cases x) auto

lemma not_range_Inl: "x ∉ range Inl ⟷ x ∈ range Inr"
by(cases x) auto

lemma Chains_into_chain: "M ∈ Chains {(x, y). R x y} ⟹ Complete_Partial_Order.chain R M"
by(simp add: Chains_def chain_def)

lemma chain_dual: "Complete_Partial_Order.chain (≥) = Complete_Partial_Order.chain (≤)"
by(auto simp add: fun_eq_iff chain_def)

lemma Cauchy_real_Suc_diff:
  fixes X :: "nat ⇒ real" and x :: real
  assumes bounded: "⋀n. ¦f (Suc n) - f n¦ ≤ (c / x ^ n)"
  and x: "1 < x"
  shows "Cauchy f"
proof(cases "c > 0")
  case c: True
  show ?thesis
  proof(rule metric_CauchyI)
    fix ε :: real
    assume "0 < ε"

    from bounded[of 0] x have c_nonneg: "0 ≤ c" by simp
    from x have "0 < ln x" by simp
    from reals_Archimedean3[OF this] obtain M :: nat
      where "ln (c * x) - ln (ε * (x - 1)) < real M * ln x" by blast
    hence "exp (ln (c * x) - ln (ε * (x - 1))) < exp (real M * ln x)" by(rule exp_less_mono)
    hence M: "c * (1 / x) ^ M / (1 - 1 / x) < ε" using ‹0 < ε› x c
      by (simp add: exp_diff exp_of_nat_mult field_simps del: ln_mult)

    { fix n m :: nat
      assume "n ≥ M" "m ≥ M"
      then have "¦f m - f n¦ ≤ c * ((1 / x) ^ M - (1 / x) ^ max m n) / (1 - 1 / x)"
      proof(induction n m rule: linorder_wlog)
        case sym thus ?case by(simp add: abs_minus_commute max.commute min.commute)
      next
        case (le m n)
        then show ?case
        proof(induction k≡"n - m" arbitrary: n m)
          case 0 thus ?case using x c_nonneg by(simp add: field_simps mult_left_mono)
        next
          case (Suc k m n)
          from ‹Suc k = _› obtain m' where m: "m = Suc m'" by(cases m) simp_all
          with ‹Suc k = _› Suc.prems have "k = m' - n" "n ≤ m'" "M ≤ n" "M ≤ m'" by simp_all
          hence "¦f m' - f n¦ ≤ c * ((1 / x) ^ M - (1 / x) ^ (max m' n)) / (1 - 1 / x)" by(rule Suc)
          also have "… = c * ((1 / x) ^ M - (1 / x) ^ m') / (1 - 1 / x)" using ‹n ≤ m'› by(simp add: max_def)
          moreover
          from bounded have "¦f m - f m'¦ ≤ (c / x ^ m')" by(simp add: m)
          ultimately have "¦f m' - f n¦ + ¦f m - f m'¦ ≤ c * ((1 / x) ^ M - (1 / x) ^ m') / (1 - 1 / x) + …" by simp
          also have "… ≤ c * ((1 / x) ^ M - (1 / x) ^ m) / (1 - 1 / x)" using m x by(simp add: field_simps)
          also have "¦f m - f n¦ ≤ ¦f m' - f n¦ + ¦f m - f m'¦"
            using abs_triangle_ineq4[of "f m' - f n" "f m - f m'"] by simp
          ultimately show ?case using ‹n ≤ m› by(simp add: max_def)
        qed
      qed
      also have "… < c * (1 / x) ^ M / (1 - 1 / x)" using x c by(auto simp add: field_simps)
      also have "… < ε" using M .
      finally have "¦f m - f n¦ < ε" . }
    thus "∃M. ∀m≥M. ∀n≥M. dist (f m) (f n) < ε" unfolding dist_real_def by blast
  qed
next
  case False
  with bounded[of 0] have [simp]: "c = 0" by simp
  have eq: "f m = f 0" for m
  proof(induction m)
    case (Suc m) from bounded[of m] Suc.IH show ?case by simp
  qed simp
  show ?thesis by(rule metric_CauchyI)(subst (1 2) eq; simp)
qed

lemma complete_lattice_ccpo_dual:
  "class.ccpo Inf (≥) ((>) :: _ :: complete_lattice ⇒ _)"
by(unfold_locales)(auto intro: Inf_lower Inf_greatest)

lemma card_eq_1_iff: "card A = Suc 0 ⟷ (∃x. A = {x})"
using card_eq_SucD by auto

lemma nth_rotate1: "n < length xs ⟹ rotate1 xs ! n = xs ! (Suc n mod length xs)"
apply(cases xs; clarsimp simp add: nth_append not_less)
apply(subgoal_tac "n = length list"; simp)
done

lemma set_zip_rightI: "⟦ x ∈ set ys; length xs ≥ length ys ⟧ ⟹ ∃z. (z, x) ∈ set (zip xs ys)"
by(fastforce simp add: in_set_zip in_set_conv_nth simp del: length_greater_0_conv intro!: nth_zip conjI[rotated])

lemma map_eq_append_conv:
  "map f xs = ys @ zs ⟷ (∃ys' zs'. xs = ys' @ zs' ∧ ys = map f ys' ∧ zs = map f zs')"
by(auto 4 4 intro: exI[where x="take (length ys) xs"] exI[where x="drop (length ys) xs"] simp add: append_eq_conv_conj take_map drop_map dest: sym)

lemma rotate1_append:
  "rotate1 (xs @ ys) = (if xs = [] then rotate1 ys else tl xs @ ys @ [hd xs])"
by(clarsimp simp add: neq_Nil_conv)

lemma in_set_tlD: "x ∈ set (tl xs) ⟹ x ∈ set xs"
by(cases xs) simp_all

lemma countable_converseI:
  assumes "countable A"
  shows "countable (converse A)"
proof -
  have "converse A = prod.swap ` A" by auto
  then show ?thesis using assms by simp
qed

lemma countable_converse [simp]: "countable (converse A) ⟷ countable A"
using countable_converseI[of A] countable_converseI[of "converse A"] by auto

lemma nn_integral_count_space_reindex:
  "inj_on f A ⟹(∫⇧+ y. g y ∂count_space (f ` A)) = (∫⇧+ x. g (f x) ∂count_space A)"
by(simp add: embed_measure_count_space'[symmetric] nn_integral_embed_measure' measurable_embed_measure1)

syntax
  "_nn_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  ("(2∑⇧+ _∈_./ _)" [0, 51, 10] 10)
  "_nn_sum_UNIV" :: "pttrn ⇒ 'b ⇒ 'b::comm_monoid_add" ("(2∑⇧+ _./ _)" [0, 10] 10)
translations
  "∑⇧+ i∈A. b" ⇌ "CONST nn_integral (CONST count_space A) (λi. b)"
  "∑⇧+ i. b" ⇌ "∑⇧+ i∈CONST UNIV. b"

inductive_simps rtrancl_path_simps:
  "rtrancl_path R x [] y"
  "rtrancl_path R x (a # bs) y"

definition restrict_rel :: "'a set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where "restrict_rel A R = {(x, y)∈R. x ∈ A ∧ y ∈ A}"

lemma in_restrict_rel_iff: "(x, y) ∈ restrict_rel A R ⟷ (x, y) ∈ R ∧ x ∈ A ∧ y ∈ A"
by(simp add: restrict_rel_def)

lemma restrict_relE: "⟦ (x, y) ∈ restrict_rel A R; ⟦ (x, y) ∈ R; x ∈ A; y ∈ A ⟧ ⟹ thesis ⟧ ⟹ thesis"
by(simp add: restrict_rel_def)

lemma restrict_relI [intro!]: "⟦ (x, y) ∈ R; x ∈ A; y ∈ A ⟧ ⟹ (x, y) ∈ restrict_rel A R"
by(simp add: restrict_rel_def)

lemma Field_restrict_rel_subset: "Field (restrict_rel A R) ⊆ A ∩ Field R"
by(auto simp add: Field_def in_restrict_rel_iff)

lemma Field_restrict_rel [simp]: "Refl R ⟹ Field (restrict_rel A R) = A ∩ Field R"
using Field_restrict_rel_subset[of A R]
by auto (auto simp add: Field_def dest: refl_onD)

lemma Partial_order_restrict_rel:
  assumes "Partial_order R"
  shows "Partial_order (restrict_rel A R)"
proof -
  from assms have "Refl R" by(simp add: order_on_defs)
  from Field_restrict_rel[OF this, of A] assms show ?thesis
    by(simp add: order_on_defs trans_def antisym_def)
      (auto intro: FieldI1 FieldI2 intro!: refl_onI simp add: in_restrict_rel_iff elim: refl_onD)
qed

lemma Chains_restrict_relD: "M ∈ Chains (restrict_rel A leq) ⟹ M ∈ Chains leq"
by(auto simp add: Chains_def in_restrict_rel_iff)

lemma bourbaki_witt_fixpoint_restrict_rel:
  assumes leq: "Partial_order leq"
  and chain_Field: "⋀M. ⟦ M ∈ Chains (restrict_rel A leq); M ≠ {} ⟧ ⟹ lub M ∈ A"
  and lub_least: "⋀M z. ⟦ M ∈ Chains leq; M ≠ {}; ⋀x. x ∈ M ⟹ (x, z) ∈ leq ⟧ ⟹ (lub M, z) ∈ leq"
  and lub_upper: "⋀M z. ⟦ M ∈ Chains leq; z ∈ M ⟧ ⟹ (z, lub M) ∈ leq"
  and increasing: "⋀x. ⟦ x ∈ A; x ∈ Field leq ⟧ ⟹ (x, f x) ∈ leq ∧ f x ∈ A"
  shows "bourbaki_witt_fixpoint lub (restrict_rel A leq) f"
proof
  show "Partial_order (restrict_rel A leq)" using leq by(rule Partial_order_restrict_rel)
next
  from leq have Refl: "Refl leq" by(simp add: order_on_defs)

  { fix M z
    assume M: "M ∈ Chains (restrict_rel A leq)"
    presume z: "z ∈ M"
    hence "M ≠ {}" by auto
    with M have lubA: "lub M ∈ A" by(rule chain_Field)
    from M have M': "M ∈ Chains leq" by(rule Chains_restrict_relD)
    then have *: "(z, lub M) ∈ leq" using z by(rule lub_upper)
    hence "lub M ∈ Field leq" by(rule FieldI2)
    with lubA show "lub M ∈ Field (restrict_rel A leq)" by(simp add: Field_restrict_rel[OF Refl])
    from Chains_FieldD[OF M z] have "z ∈ A" by(simp add: Field_restrict_rel[OF Refl])
    with * lubA show "(z, lub M ) ∈ restrict_rel A leq" by auto

    fix z
    assume upper: "⋀x. x ∈ M ⟹ (x, z) ∈ restrict_rel A leq"
    from upper[OF z] have "z ∈ Field (restrict_rel A leq)" by(auto simp add: Field_def)
    with Field_restrict_rel_subset[of A leq] have "z ∈ A" by blast
    moreover from lub_least[OF M' ‹M ≠ {}›] upper have "(lub M, z) ∈ leq"
      by(auto simp add: in_restrict_rel_iff)
    ultimately show "(lub M, z) ∈ restrict_rel A leq" using lubA by(simp add: in_restrict_rel_iff) }
  { fix x
    assume "x ∈ Field (restrict_rel A leq)"
    hence "x ∈ A" "x ∈ Field leq" by(simp_all add: Field_restrict_rel[OF Refl])
    with increasing[OF this] show "(x, f x) ∈ restrict_rel A leq" by auto }
  show "(SOME x. x ∈ M) ∈ M" "(SOME x. x ∈ M) ∈ M" if "M ≠ {}" for M :: "'a set"
    using that by(auto intro: someI)
qed

lemma Field_le [simp]: "Field {(x :: _ :: preorder, y). x ≤ y} = UNIV"
by(auto intro: FieldI1)

lemma Field_ge [simp]: "Field {(x :: _ :: preorder, y). y ≤ x} = UNIV"
by(auto intro: FieldI1)

lemma refl_le [simp]: "refl {(x :: _ :: preorder, y). x ≤ y}"
by(auto intro!: refl_onI simp add: Field_def)

lemma refl_ge [simp]: "refl {(x :: _ :: preorder, y). y ≤ x}"
by(auto intro!: refl_onI simp add: Field_def)

lemma partial_order_le [simp]: "partial_order_on UNIV {(x :: _ :: order, x'). x ≤ x'}"
by(auto simp add: order_on_defs trans_def antisym_def)

lemma partial_order_ge [simp]: "partial_order_on UNIV {(x :: _ :: order, x'). x' ≤ x}"
by(auto simp add: order_on_defs trans_def antisym_def)

lemma incseq_chain_range: "incseq f ⟹ Complete_Partial_Order.chain (≤) (range f)"
apply(rule chainI; clarsimp)
 using linear by (auto dest: incseqD)

end