Theory Auxiliarities

(* Author: Fabian Immler <immler@in.tum.de> *)

theory Auxiliarities
imports Probability
begin

section {* Auxiliarities *}

subsection {* Functions: Injective and Inverse *}

lemma inj_on_vimage_image_eq:
  assumes "inj_on f X" "A ⊆ X" shows "f -` f ` A ∩ X = A"
using assms by (auto simp: vimage_image_eq inj_on_def)

lemma inv_into_inv_into_superset_eq:
  assumes "inj_on f B"
  assumes "bij_betw f A A'" "a ∈ A" "A ⊆ B"
  shows "inv_into A' (inv_into B f) a = f a"
proof -
  let ?f' = "inv_into A f" let ?e' = "inv_into B f"
  let ?f'' = "inv_into A' ?f'" let ?e'' = "inv_into A' ?e'"
  have 1: "bij_betw ?f' A' A" using assms by (auto simp add: bij_betw_inv_into)
  obtain a' where 2: "a' ∈ A'" and 3: "?f' a' = a"
    using 1 `a ∈ A` unfolding bij_betw_def by force
  have "f a = a'" using assms 2 3
    by (auto simp add: bij_betw_def)  
  have "inj_on ?e' A'"
  proof (intro inj_onI)
    { fix x assume "x ∈ A'"
      hence "x ∈ f ` A" using assms(2) by (auto simp: bij_betw_def)
      hence "inv_into A f x ∈ A" by (rule inv_into_into)
      also note `A ⊆ B`
      finally have "inv_into B f x = ?f' x"
        using f_inv_into_f[OF `x ∈ image f A`]
        by (rule inv_into_f_eq[OF `inj_on f B`])
    }
    moreover
    fix x y assume "x ∈ A'" "y ∈ A'" "inv_into B f x = inv_into B f y"
    ultimately
    have "inv_into A f x = inv_into A f y" by simp
    thus "x = y" by (metis "1" `x ∈ A'` `y ∈ A'` bij_betw_imp_inj_on inj_onD)
  qed
  hence "?e'' a = a'" using assms 2 `f a = a'` by (intro inv_into_f_eq) auto
  thus "?e'' a = f a" using `f a = a'` by simp
qed

lemma f_inv_into_onto:
  fixes f::"'a => 'b" and A::"'a set" and B::"'b set"
  assumes "inj_on f A" "B ⊆ f ` A"
  shows "f ` inv_into A f ` B = B"
unfolding image_image using assms
proof safe
  fix x assume "x ∈ B"
  thus "x ∈ (λx. f (inv_into A f x)) ` B"
    unfolding image_def
    using assms `x ∈ B`
    by (auto simp: Bex_def f_inv_into_f intro!: exI[where x=x])
qed (auto simp: f_inv_into_f)

lemma inj_on_image_subset_iff: "inj_on f (A ∪ B) ==> (f`A <= f`B) = (A<=B)"
by (simp add: inj_on_def, blast)

lemma inv_into_eq:
  assumes "inj_on f A" "inj_on g A"
  assumes "x ∈ g ` A"
  assumes "!!i. i ∈ A ==> f i = g i"
  shows "inv_into A f x = inv_into A g x"
proof -
  from assms obtain y where "g y = x" "y ∈ A" by auto
  show ?thesis
    apply (rule inv_into_f_eq[OF `inj_on f A`])
    apply (rule inv_into_into[OF `x ∈ image g A`])
    apply (subst inv_into_f_eq[OF `inj_on g A`])
    using assms `g y = x` `y ∈ A` by auto
qed

lemma inv_into_eq':
  assumes "inj_on f A" "inj_on f B"
  assumes "x ∈ f ` (A ∩ B)"
  shows "inv_into A f x = inv_into B f x"
  using assms
  by (metis (full_types) Int_iff f_inv_into_f inv_into_f_f inv_into_into)

subsection {* Topology *}

lemma borel_def_closed: "borel = sigma UNIV (Collect closed)"
  unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI, safe)
  fix x :: "'a set" assume "open x"
  hence "x = UNIV - (UNIV - x)" by auto
  also have "… ∈ sigma_sets UNIV (Collect closed)"
    by (rule sigma_sets.Compl)
       (auto intro!: sigma_sets.Basic simp: `open x`)
  finally show "x ∈ sigma_sets UNIV (Collect closed)" by simp
next
  fix x :: "'a set" assume "closed x"
  hence "x = UNIV - (UNIV - x)" by auto
  also have "… ∈ sigma_sets UNIV (Collect open)"
    by (rule sigma_sets.Compl)
       (auto intro!: sigma_sets.Basic simp: `closed x`)
  finally show "x ∈ sigma_sets UNIV (Collect open)" by simp
qed simp_all

lemma compactE':
  assumes "compact S" "∀n≥m. f n ∈ S"
  obtains l r where "l ∈ S" "subseq r" "((f o r) ---> l) sequentially"
proof atomize_elim
  have "subseq (op + m)" by (simp add: subseq_def)
  have "∀n. (f o (λi. m + i)) n ∈ S" using assms by auto  
  from compactE[OF `compact S` this] guess l r .
  hence "l ∈ S" "subseq ((λi. m + i) o r) ∧ (f o ((λi. m + i) o r)) ----> l"
    using subseq_o[OF `subseq (op + m)` `subseq r`] by (auto simp: o_def)
  thus "∃l r. l ∈ S ∧ subseq r ∧ (f o r) ----> l" by blast
qed

lemma compact_Union [intro]: "finite S ==> ∀T∈S. compact T ==> compact (\<Union>S)"
  by (induct set: finite) auto

lemma closed_UN [intro]: "finite A ==> ∀x∈A. compact (B x) ==> compact (\<Union>x∈A. B x)"
  unfolding SUP_def by (rule compact_Union) auto

subsection {* Measures *}

lemma
  UN_finite_countable_eq_Un:
  fixes f :: "'a::countable set => _"
  assumes "!!s. P s ==> finite s"
  shows "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})"
proof safe
  fix x X s assume "x ∈ f s" "P s"
  moreover with assms obtain l where "s = set l" using finite_list by auto
  ultimately show "x ∈ (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
    by (auto intro!: exI[where x="to_nat l"])
next
  fix x n assume "x ∈ (let s = set (from_nat n) in if P s then f s else {})"
  thus "x ∈ \<Union>{f s|s. P s}" using assms by (auto simp: Let_def split: split_if_asm)
qed

lemma
  countable_finite_comprehension:
  fixes f :: "'a::countable set => _"
  assumes "!!s. P s ==> finite s"
  assumes "!!s. P s ==> f s ∈ sets M"
  shows "\<Union>{f s|s. P s} ∈ sets M"
proof -
  from UN_finite_countable_eq_Un[of P f] assms
  have "\<Union>{f s|s. P s} = (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" by simp
  also have "… ∈ sets M" using assms by (auto simp: Let_def)
  finally show ?thesis .
qed

lemma (in ring_of_sets) union:
  assumes f: "positive M f" "additive M f" and "A ∈ M" "B ∈ M"
  shows "f (A ∪ B) = f A + f (B - A)"
  using assms by (subst additiveD[OF `additive M f`, symmetric]) auto

lemma (in ring_of_sets) plus:
  assumes f: "positive M f" "additive M f" and "A ∈ M" "B ∈ M"
  shows "f B = f (A ∩ B) + f (B - A)"
proof -
  have "A ∩ B ∪ (B - A) = B" by auto
  thus ?thesis using assms
    by (subst additiveD[OF `additive M f`, symmetric]) auto
qed

lemma (in ring_of_sets) union_inter_minus_equality:
  assumes f: "positive M f" "additive M f" and "A ∈ M" "B ∈ M"
  shows "f (A ∪ B) + f (A ∩ B) + f (B - A) = f A + f B + f (B - A)"
  using union[OF assms] plus[OF assms] by (simp add: ac_simps)

lemma (in ring_of_sets) union_plus_inter_equality:
  assumes f: "positive M f" "additive M f" and "A ∈ M" "B ∈ M"
  shows "f (A ∪ B) + f (A ∩ B) = f A + f B"
proof cases
  assume "f (B - A) = ∞" hence "f B = ∞" "f (A ∪ B) = ∞"
    using plus[OF assms] union[OF assms] by simp_all
  thus ?thesis by simp
next
  assume "f (B - A) ≠ ∞" thus ?thesis using union_inter_minus_equality[OF assms] f assms
    by (subst (asm) ereal_add_cancel_right) (auto dest: positiveD2[where A="B-A"])
qed

lemma emeasure_union_plus_inter_equality:
  assumes "A ∈ sets M" "B ∈ sets M"
  shows "M (A ∪ B) + M (A ∩ B) = M A + M B"
  by (rule union_plus_inter_equality[OF emeasure_positive emeasure_additive assms])

lemma (in finite_measure) measure_union:
  assumes "A ∈ sets M" "B ∈ sets M"
  shows "measure M (A ∪ B) = measure M A + measure M B - measure M (A ∩ B)"
  using union_plus_inter_equality[OF emeasure_positive emeasure_additive assms]
  by (simp add: emeasure_eq_measure)

lemma (in ring_of_sets) subtractive:
  assumes f: "positive M f" "additive M f" and "A ∈ M" "B ∈ M" and "A ⊆ B"
    and "f A < ∞"
  shows "f (B - A) = f B - f A"
proof -
  note union_inter_minus_equality[OF assms(1-4)]
  moreover have "A ∪ B = B" using assms by auto
  ultimately have "f B = f A + f (B - A)" using assms
    by (subst additiveD[OF `additive M f`, symmetric]) auto
  hence "f B - f A = f A + f (B - A) - f A" using assms by simp
  also have "… = f (B - A) + f A - f A" using assms by (auto simp: ac_simps)
  also have "… = f (B - A) + (f A - f A)"
    by (metis ab_semigroup_add_class.add_ac(1) ereal_minus(6) ereal_uminus_uminus)
  also have "f A - f A = 0" using assms by (auto simp: positive_def)
  finally show ?thesis by simp
qed

lemma (in ring_of_sets) subadditive:
  assumes f: "positive M f" "additive M f" and A: "range A ⊆ M" and S: "finite S"
  shows "f (\<Union>i∈S. A i) ≤ (∑i∈S. f (A i))"
using S
proof (induct S)
  case empty thus ?case using f by (auto simp: positive_def)
next
  case (insert x F)
  hence in_M: "A x ∈ M" "(\<Union> i∈F. A i) ∈ M" "(\<Union> i∈F. A i) - A x ∈ M" using A by force+
  have subs: "(\<Union> i∈F. A i) - A x ⊆ (\<Union> i∈F. A i)" by auto
  have "(\<Union> i∈(insert x F). A i) = A x ∪ ((\<Union> i∈F. A i) - A x)" by auto
  hence "f (\<Union> i∈(insert x F). A i) = f (A x ∪ ((\<Union> i∈F. A i) - A x))"
    by simp
  also have "… = f (A x) + f ((\<Union> i∈F. A i) - A x)"
    using f(2) by (rule additiveD) (insert in_M, auto)
  also have "… ≤ f (A x) + f (\<Union> i∈F. A i)"
    using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
  also have "… ≤ f (A x) + (∑i∈F. f (A i))" using insert by (auto intro: add_left_mono)
  finally show "f (\<Union> i∈(insert x F). A i) ≤ (∑i∈(insert x F). f (A i))" using insert by simp
qed

lemma  finite_Union:
  fixes A::"'a::countable set"
  assumes "!!i. i ∈ A ==> B i ∈ sigma_sets sp C"
  shows "\<Union>B ` A ∈ sigma_sets sp C"
proof cases
  assume "A = {}" thus ?thesis by (simp add: Empty)
next
  assume "A ≠ {}" then obtain a where "a ∈ A" by auto
  have UN: "UNION A B =
    UNION UNIV (λi. if from_nat i ∈ A then B (from_nat i) else B a)" using `a ∈ A`
    apply auto
  proof -
    case goal1 thus ?case
    by (auto intro: exI[where x="to_nat xa"])
  next
    case goal2 thus ?case by (auto split: split_if_asm simp add: Bex_def)
  qed
  show ?thesis using assms `a∈A` by (auto intro: Union simp: UN)
qed

subsection {* Enumeration of Finite Set *}

definition "enum_finite_max J = (SOME n. ∃ f. J = f ` {i. i < n} ∧ inj_on f {i. i < n})"

definition enum_finite where
  "enum_finite J =
    (SOME f. J = f ` {i::nat. i < enum_finite_max J} ∧ inj_on f {i. i < enum_finite_max J})"

lemma enum_finite_max:
  assumes "finite J"
  shows "∃f::nat=>'a. J = f ` {i. i < enum_finite_max J} ∧ inj_on f {i. i < enum_finite_max J}"
    unfolding enum_finite_max_def
    by (rule someI_ex) (rule finite_imp_nat_seg_image_inj_on[OF `finite J`])

lemma enum_finite:
  assumes "finite J"
  shows "J = enum_finite J ` {i::nat. i < enum_finite_max J} ∧
    inj_on (enum_finite J) {i::nat. i < enum_finite_max J}"
  unfolding enum_finite_def
  by (rule someI_ex[of "λf. J = f ` {i::nat. i < enum_finite_max J} ∧
      inj_on f {i. i < enum_finite_max J}"])
    (rule enum_finite_max[OF `finite J`])

lemma in_set_enum_exist:
  assumes "finite A"
  assumes "y ∈ A"
  shows "∃i. y = enum_finite A i"
  using assms enum_finite by auto

subsection {* Enumeration of Countable Union of Finite Sets *}

locale finite_set_sequence =
  fixes Js::"nat => 'a set"
  assumes finite_seq[simp]: "finite (Js n)"
begin

definition set_of_Un where "set_of_Un j = (LEAST n. j ∈ Js n)"

definition index_in_set where "index_in_set J j = (SOME n. j = enum_finite J n)"

definition Un_to_nat where
  "Un_to_nat j = to_nat (set_of_Un j, index_in_set (Js (set_of_Un j)) j)"

lemma inj_on_Un_to_nat:
  shows "inj_on Un_to_nat (\<Union>n::nat. Js n)"
proof (rule inj_onI)
  fix x y
  assume "x ∈ (\<Union>n. Js n)" "y ∈ (\<Union>n. Js n)"
  then obtain ix iy where ix: "x ∈ Js ix" and iy: "y ∈ Js iy" by blast
  assume "Un_to_nat x = Un_to_nat y"
  hence "set_of_Un x = set_of_Un y"
    "index_in_set (Js (set_of_Un y)) y = index_in_set (Js (set_of_Un x)) x"
    by (auto simp: Un_to_nat_def)
  moreover
  have "y ∈ Js (set_of_Un y)" unfolding set_of_Un_def using iy by (rule LeastI)
  have "x ∈ Js (set_of_Un x)" unfolding set_of_Un_def using ix by (rule LeastI)
  have "y = enum_finite (Js (set_of_Un y)) (index_in_set (Js (set_of_Un y)) y)"
    unfolding index_in_set_def
    apply (rule someI_ex) 
    using `y ∈ Js (set_of_Un y)` finite_seq
    apply (auto intro!: in_set_enum_exist)
    done
  moreover have "x = enum_finite (Js (set_of_Un x)) (index_in_set (Js (set_of_Un x)) x)"
    unfolding index_in_set_def
    apply (rule someI_ex) 
    using `x ∈ Js (set_of_Un x)` finite_seq
    apply (auto intro!: in_set_enum_exist)
    done
  ultimately show "x = y" by simp
qed

lemma inj_Un[simp]:
  shows "inj_on (Un_to_nat) (Js n)"
  by (intro subset_inj_on[OF inj_on_Un_to_nat]) (auto simp: assms)

lemma Un_to_nat_injectiveD:
  assumes "Un_to_nat x = Un_to_nat y"
  assumes "x ∈ Js i" "y ∈ Js j"
  shows "x = y"
  using assms
  by (intro inj_onD[OF inj_on_Un_to_nat]) auto

end

subsection {* Sequence of Properties on Subsequences *}

lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
  using assms by (auto simp: subseq_def)

locale subseqs =
  fixes P::"nat=>(nat=>nat)=>(nat=>nat)=>bool"
  assumes ex_subseq: "!!n s. subseq s ==> ∃r'. subseq r' ∧ P n s r'"
begin

primrec seqseq where
  "seqseq 0 = id"
| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' ∧ P n (seqseq n) r')"

lemma seqseq_ex:
  shows "subseq (seqseq n) ∧
  (∃r'. seqseq (Suc n) = seqseq n o r' ∧ subseq r' ∧ P n (seqseq n) r')"
proof (induct n)
  case 0
  let ?P = "λr'. subseq r' ∧ P 0 id r'"
  let ?r = "Eps ?P"
  have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def)
  thus ?case by (auto simp: subseq_def) (simp add: id_def)
next
  case (Suc n)
  then obtain r' where
    Suc': "seqseq (Suc n) = seqseq n o r'" "subseq (seqseq n)" "subseq r'"
      "P n (seqseq n) r'"
    by blast
  let ?P = "λr'a. subseq (r'a ) ∧ P (Suc n) (seqseq n o r') r'a"
  let ?r = "Eps ?P"
  have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc'
    by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc)
  moreover have "seqseq (Suc (Suc n)) = seqseq n o r' o ?r"
    by (subst seqseq.simps) (simp only: Suc' o_assoc)
  moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`]
  ultimately show ?case unfolding Suc' by (auto simp: o_def)
qed

lemma subseq_seqseq:
  shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto

definition reducer where "reducer n = (SOME r'. subseq r' ∧ P n (seqseq n) r')"

lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n) (reducer n)"
  unfolding atomize_conj unfolding reducer_def using subseq_seqseq
  by (rule someI_ex[OF ex_subseq])

lemma seqseq_reducer[simp]:
  "seqseq (Suc n) = seqseq n o reducer n"
  by (simp add: reducer_def)

declare seqseq.simps(2)[simp del]

definition diagseq where "diagseq i = seqseq i i"

lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
  unfolding diagseq_def seqseq_reducer o_def
  by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer)

lemma subseq_diagseq: "subseq diagseq"
  using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)

primrec fold_reduce where
  "fold_reduce n 0 = id"
| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)"

lemma subseq_fold_reduce: "subseq (fold_reduce n k)"
proof (induct k)
  case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def)
qed (simp add: subseq_def)

lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
  by (induct k) simp_all

lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
  by (induct n) (simp_all)

lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
  using seqseq_fold_reduce by (simp add: diagseq_def)

lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
  by (induct n) simp_all

lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
proof -
  have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
    by (simp add: diagseq_fold_reduce)
  also have "… = (seqseq k o fold_reduce k n) (k + n)"
    unfolding fold_reduce_add seqseq_fold_reduce ..
  finally show ?thesis .
qed

lemma diagseq_sub:
  assumes "m ≤ n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
  using diagseq_add[of m "n - m"] assms by simp

lemma subseq_diagonal_rest: "subseq (λx. fold_reduce k x (k + x))"
  unfolding subseq_Suc_iff fold_reduce.simps o_def
  by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble
      subseq_reducer)

lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (λx. fold_reduce k x (k + x)))"
  by (auto simp: o_def diagseq_add)

lemma eventually_sequentially_diagseq:
  assumes "!!n s r. P n s r = (∀i. Q n ((s o r) i))"
  shows "eventually (λi. Q n (diagseq i)) sequentially"
  unfolding eventually_sequentially
  apply (intro exI[where x="Suc n"])
  apply safe
  apply (subst diagseq_sub) apply simp
  using reducer_reduces[of n, simplified assms, simplified seqseq_reducer[symmetric]]
  apply simp
  done
  
lemma diagseq_holds:
  assumes seq_property: "!!n s r. P n s r = Q n (s o r)"
  assumes subseq_closed: "!!n s r. subseq r ==> Q n s ==> Q n (s o r)"
  shows "P n diagseq (op + (Suc n))"
  unfolding seq_property diagseq_seqseq
  by (intro subseq_closed subseq_diagonal_rest)
     (auto simp: reducer_reduces seq_property[symmetric])

end

subsection {* Product Sets *}

lemma PiE_def': "Pi⇣E I A = {f. (∀i ∈ I. f i ∈ A i) ∧ f = restrict f I}"
  apply auto
  apply (metis extensional_restrict)
  apply (metis restrict_extensional)
  done

lemma prod_emb_def': "prod_emb I M J X = {a ∈ Pi⇣E I (λi. space (M i)). restrict a J ∈ X}"
  by (auto simp: prod_emb_def)

lemma prod_emb_subsetI:
  assumes "F ⊆ G"
  shows "prod_emb A M B F ⊆ prod_emb A M B G"
  using assms by (auto simp: prod_emb_def)

end