Structure util_probTheory

signature util_probTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val binary_def : thm
    val disjoint_family_on : thm
    val disjointed : thm
    val prod_sets_def : thm
    val set_liminf_def : thm
    val set_limsup_def : thm
  
  (*  Theorems  *)
    val BIGINTER_OVER_INTER_L : thm
    val BIGINTER_OVER_INTER_R : thm
    val BIGINTER_PAIR : thm
    val BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV : thm
    val BIGUNION_IMAGE_COUNT_IMP_UNIV : thm
    val BIGUNION_IMAGE_UNIV_CROSS_UNIV : thm
    val BIGUNION_OVER_DIFF : thm
    val BIGUNION_OVER_INTER_L : thm
    val BIGUNION_OVER_INTER_R : thm
    val BIGUNION_disjointed : thm
    val BINARY_RANGE : thm
    val COMPL_BIGINTER : thm
    val COMPL_BIGINTER_IMAGE : thm
    val COMPL_BIGUNION : thm
    val COMPL_BIGUNION_IMAGE : thm
    val DIFF_INTER_PAIR : thm
    val DINTER_IMP_FINITE_INTER : thm
    val DISJOINT_CROSS_L : thm
    val DISJOINT_CROSS_R : thm
    val DISJOINT_RESTRICT_L : thm
    val DISJOINT_RESTRICT_R : thm
    val DUNION_IMP_FINITE_UNION : thm
    val FINITE_TWO : thm
    val GBIGUNION_IMAGE : thm
    val GEN_COMPL_BIGINTER : thm
    val GEN_COMPL_BIGINTER_IMAGE : thm
    val GEN_COMPL_BIGUNION : thm
    val GEN_COMPL_BIGUNION_IMAGE : thm
    val GEN_COMPL_FINITE_INTER : thm
    val GEN_COMPL_FINITE_UNION : thm
    val GEN_COMPL_INTER : thm
    val GEN_COMPL_UNION : thm
    val GEN_DIFF_INTER : thm
    val INCREASING_TO_DISJOINT_SETS : thm
    val INCREASING_TO_DISJOINT_SETS' : thm
    val INTER_BINARY : thm
    val IN_LIMINF : thm
    val IN_LIMSUP : thm
    val IN_PROD_SETS : thm
    val LIMSUP_COMPL : thm
    val LIMSUP_DIFF : thm
    val LIMSUP_MONO_STRONG : thm
    val LIMSUP_MONO_STRONGER : thm
    val LIMSUP_MONO_WEAK : thm
    val PREIMAGE_REAL_COMPL1 : thm
    val PREIMAGE_REAL_COMPL2 : thm
    val PREIMAGE_REAL_COMPL3 : thm
    val PREIMAGE_REAL_COMPL4 : thm
    val SETS_TO_DISJOINT_SETS : thm
    val SETS_TO_DISJOINT_SETS' : thm
    val SETS_TO_INCREASING_SETS : thm
    val SETS_TO_INCREASING_SETS' : thm
    val SUBSET_DIFF_DISJOINT : thm
    val SUBSET_DIFF_SUBSET : thm
    val SUBSET_INTER_SUBSET_L : thm
    val SUBSET_INTER_SUBSET_R : thm
    val SUBSET_MONO_DIFF : thm
    val SUBSET_RESTRICT_DIFF : thm
    val SUBSET_RESTRICT_L : thm
    val SUBSET_RESTRICT_R : thm
    val SUBSET_TWO : thm
    val UNION_BINARY : thm
    val UNION_TO_3_DISJOINT_UNIONS : thm
    val count1_def : thm
    val count1_numseg : thm
    val disjoint_family_def : thm
    val disjoint_family_disjoint : thm
    val disjoint_family_on_def : thm
    val disjointed_subset : thm
    val finite_decomposition : thm
    val finite_decomposition_simple : thm
    val finite_disjoint_decomposition : thm
    val finite_disjoint_decomposition' : thm
    val finite_enumeration_of_sets_has_max_non_empty : thm
    val infinitely_often_lemma : thm
    val infinity_bound_lemma : thm
    val set_limsup_alt : thm
    val tail_countable : thm
    val tail_not_empty : thm
  
  val util_prob_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [nets] Parent theory of "util_prob"
   
   [real_sigma] Parent theory of "util_prob"
   
   [binary_def]  Definition
      
      ⊢ ∀a b. binary a b = (λx. if x = 0 then a else b)
   
   [disjoint_family_on]  Definition
      
      ⊢ ∀a s.
          disjoint_family_on a s ⇔
          ∀m n. m ∈ s ∧ n ∈ s ∧ m ≠ n ⇒ a m ∩ a n = ∅
   
   [disjointed]  Definition
      
      ⊢ ∀A n.
          disjointed A n =
          A n DIFF BIGUNION {A i | i ∈ {x | 0 ≤ x ∧ x < n}}
   
   [prod_sets_def]  Definition
      
      ⊢ ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}
   
   [set_liminf_def]  Definition
      
      ⊢ ∀E. liminf E =
            BIGUNION (IMAGE (λm. BIGINTER {E n | m ≤ n}) 𝕌(:num))
   
   [set_limsup_def]  Definition
      
      ⊢ ∀E. limsup E =
            BIGINTER (IMAGE (λm. BIGUNION {E n | m ≤ n}) 𝕌(:num))
   
   [BIGINTER_OVER_INTER_L]  Theorem
      
      ⊢ ∀f s d.
          s ≠ ∅ ⇒
          BIGINTER (IMAGE f s) ∩ d = BIGINTER (IMAGE (λi. f i ∩ d) s)
   
   [BIGINTER_OVER_INTER_R]  Theorem
      
      ⊢ ∀f s d.
          s ≠ ∅ ⇒
          d ∩ BIGINTER (IMAGE f s) = BIGINTER (IMAGE (λi. d ∩ f i) s)
   
   [BIGINTER_PAIR]  Theorem
      
      ⊢ ∀s t. BIGINTER {s; t} = s ∩ t
   
   [BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV]  Theorem
      
      ⊢ ∀f. BIGUNION (IMAGE (λn. BIGUNION (IMAGE (f n) 𝕌(:num))) 𝕌(:num)) =
            BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num))
   
   [BIGUNION_IMAGE_COUNT_IMP_UNIV]  Theorem
      
      ⊢ ∀f g.
          (∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [BIGUNION_IMAGE_UNIV_CROSS_UNIV]  Theorem
      
      ⊢ ∀f h.
          BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
          BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num)) =
          BIGUNION (IMAGE (UNCURRY f ∘ h) 𝕌(:num))
   
   [BIGUNION_OVER_DIFF]  Theorem
      
      ⊢ ∀f s d.
          BIGUNION (IMAGE f s) DIFF d = BIGUNION (IMAGE (λi. f i DIFF d) s)
   
   [BIGUNION_OVER_INTER_L]  Theorem
      
      ⊢ ∀f s d. BIGUNION (IMAGE f s) ∩ d = BIGUNION (IMAGE (λi. f i ∩ d) s)
   
   [BIGUNION_OVER_INTER_R]  Theorem
      
      ⊢ ∀f s d. d ∩ BIGUNION (IMAGE f s) = BIGUNION (IMAGE (λi. d ∩ f i) s)
   
   [BIGUNION_disjointed]  Theorem
      
      ⊢ ∀A. BIGUNION {disjointed A i | i ∈ 𝕌(:num)} =
            BIGUNION {A i | i ∈ 𝕌(:num)}
   
   [BINARY_RANGE]  Theorem
      
      ⊢ ∀a b. IMAGE (binary a b) 𝕌(:num) = {a; b}
   
   [COMPL_BIGINTER]  Theorem
      
      ⊢ ∀c. COMPL (BIGINTER c) = BIGUNION (IMAGE COMPL c)
   
   [COMPL_BIGINTER_IMAGE]  Theorem
      
      ⊢ ∀f. COMPL (BIGINTER (IMAGE f 𝕌(:num))) =
            BIGUNION (IMAGE (COMPL ∘ f) 𝕌(:num))
   
   [COMPL_BIGUNION]  Theorem
      
      ⊢ ∀c. c ≠ ∅ ⇒ COMPL (BIGUNION c) = BIGINTER (IMAGE COMPL c)
   
   [COMPL_BIGUNION_IMAGE]  Theorem
      
      ⊢ ∀f. COMPL (BIGUNION (IMAGE f 𝕌(:num))) =
            BIGINTER (IMAGE (COMPL ∘ f) 𝕌(:num))
   
   [DIFF_INTER_PAIR]  Theorem
      
      ⊢ ∀sp x y. sp DIFF x ∩ y = sp DIFF x ∪ (sp DIFF y)
   
   [DINTER_IMP_FINITE_INTER]  Theorem
      
      ⊢ ∀sts f.
          (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (𝕌(:num) → sts) ⇒
          ∀n. 0 < n ⇒ BIGINTER (IMAGE f (count n)) ∈ sts
   
   [DISJOINT_CROSS_L]  Theorem
      
      ⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s × c) (t × c)
   
   [DISJOINT_CROSS_R]  Theorem
      
      ⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c × s) (c × t)
   
   [DISJOINT_RESTRICT_L]  Theorem
      
      ⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s ∩ c) (t ∩ c)
   
   [DISJOINT_RESTRICT_R]  Theorem
      
      ⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c ∩ s) (c ∩ t)
   
   [DUNION_IMP_FINITE_UNION]  Theorem
      
      ⊢ ∀sts f.
          (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ⇒
          ∀n. 0 < n ∧ (∀i. i < n ⇒ f i ∈ sts) ⇒
              BIGUNION (IMAGE f (count n)) ∈ sts
   
   [FINITE_TWO]  Theorem
      
      ⊢ ∀s t. FINITE {s; t}
   
   [GBIGUNION_IMAGE]  Theorem
      
      ⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))
   
   [GEN_COMPL_BIGINTER]  Theorem
      
      ⊢ ∀sp c.
          (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
          sp DIFF BIGINTER c = BIGUNION (IMAGE (λx. sp DIFF x) c)
   
   [GEN_COMPL_BIGINTER_IMAGE]  Theorem
      
      ⊢ ∀sp f.
          (∀n. f n ⊆ sp) ⇒
          sp DIFF BIGINTER (IMAGE f 𝕌(:num)) =
          BIGUNION (IMAGE (λn. sp DIFF f n) 𝕌(:num))
   
   [GEN_COMPL_BIGUNION]  Theorem
      
      ⊢ ∀sp c.
          c ≠ ∅ ∧ (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
          sp DIFF BIGUNION c = BIGINTER (IMAGE (λx. sp DIFF x) c)
   
   [GEN_COMPL_BIGUNION_IMAGE]  Theorem
      
      ⊢ ∀sp f.
          (∀n. f n ⊆ sp) ⇒
          sp DIFF BIGUNION (IMAGE f 𝕌(:num)) =
          BIGINTER (IMAGE (λn. sp DIFF f n) 𝕌(:num))
   
   [GEN_COMPL_FINITE_INTER]  Theorem
      
      ⊢ ∀sp f n.
          0 < n ⇒
          sp DIFF BIGINTER (IMAGE f (count n)) =
          BIGUNION (IMAGE (λi. sp DIFF f i) (count n))
   
   [GEN_COMPL_FINITE_UNION]  Theorem
      
      ⊢ ∀sp f n.
          0 < n ⇒
          sp DIFF BIGUNION (IMAGE f (count n)) =
          BIGINTER (IMAGE (λi. sp DIFF f i) (count n))
   
   [GEN_COMPL_INTER]  Theorem
      
      ⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF s ∩ t = sp DIFF s ∪ (sp DIFF t)
   
   [GEN_COMPL_UNION]  Theorem
      
      ⊢ ∀sp s t.
          s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF (s ∪ t) = (sp DIFF s) ∩ (sp DIFF t)
   
   [GEN_DIFF_INTER]  Theorem
      
      ⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ s DIFF t = s ∩ (sp DIFF t)
   
   [INCREASING_TO_DISJOINT_SETS]  Theorem
      
      ⊢ ∀f. (∀n. f n ⊆ f (SUC n)) ⇒
            ∃g. g 0 = f 0 ∧ (∀n. 0 < n ⇒ g n = f n DIFF f (PRE n)) ∧
                (∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
                BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [INCREASING_TO_DISJOINT_SETS']  Theorem
      
      ⊢ ∀f. f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
            ∃g. (∀n. g n = f (SUC n) DIFF f n) ∧
                (∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
                BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [INTER_BINARY]  Theorem
      
      ⊢ ∀a b. a ∩ b = BIGINTER {binary a b i | i ∈ 𝕌(:num)}
   
   [IN_LIMINF]  Theorem
      
      ⊢ ∀A x. x ∈ liminf A ⇔ ∃m. ∀n. m ≤ n ⇒ x ∈ A n
   
   [IN_LIMSUP]  Theorem
      
      ⊢ ∀A x. x ∈ limsup A ⇔ ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ x ∈ A n
   
   [IN_PROD_SETS]  Theorem
      
      ⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. s = t × u ∧ t ∈ a ∧ u ∈ b
   
   [LIMSUP_COMPL]  Theorem
      
      ⊢ ∀E. COMPL (liminf E) = limsup (COMPL ∘ E)
   
   [LIMSUP_DIFF]  Theorem
      
      ⊢ ∀sp E. (∀n. E n ⊆ sp) ⇒ sp DIFF liminf E = limsup (λn. sp DIFF E n)
   
   [LIMSUP_MONO_STRONG]  Theorem
      
      ⊢ ∀A B. (∀y n. y ∈ A n ⇒ ∃m. n ≤ m ∧ y ∈ B m) ⇒ limsup A ⊆ limsup B
   
   [LIMSUP_MONO_STRONGER]  Theorem
      
      ⊢ ∀A B.
          (∃d. ∀y n. y ∈ A n ⇒ ∃m. n − d ≤ m ∧ y ∈ B m) ⇒
          limsup A ⊆ limsup B
   
   [LIMSUP_MONO_WEAK]  Theorem
      
      ⊢ ∀A B. (∀n. A n ⊆ B n) ⇒ limsup A ⊆ limsup B
   
   [PREIMAGE_REAL_COMPL1]  Theorem
      
      ⊢ ∀c. COMPL {x | c < x} = {x | x ≤ c}
   
   [PREIMAGE_REAL_COMPL2]  Theorem
      
      ⊢ ∀c. COMPL {x | c ≤ x} = {x | x < c}
   
   [PREIMAGE_REAL_COMPL3]  Theorem
      
      ⊢ ∀c. COMPL {x | x ≤ c} = {x | c < x}
   
   [PREIMAGE_REAL_COMPL4]  Theorem
      
      ⊢ ∀c. COMPL {x | x < c} = {x | c ≤ x}
   
   [SETS_TO_DISJOINT_SETS]  Theorem
      
      ⊢ ∀sp sts f.
          (∀s. s ∈ sts ⇒ s ⊆ sp) ∧ (∀n. f n ∈ sts) ⇒
          ∃g. g 0 = f 0 ∧
              (∀n. 0 < n ⇒
                   g n = f n ∩ BIGINTER (IMAGE (λi. sp DIFF f i) (count n))) ∧
              (∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
              BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [SETS_TO_DISJOINT_SETS']  Theorem
      
      ⊢ ∀f. ∃g.
          g 0 = f 0 ∧
          (∀n. 0 < n ⇒ g n = f n ∩ BIGINTER (IMAGE (COMPL ∘ f) (count n))) ∧
          (∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [SETS_TO_INCREASING_SETS]  Theorem
      
      ⊢ ∀f. ∃g.
          g 0 = f 0 ∧ (∀n. g n = BIGUNION (IMAGE f (count1 n))) ∧
          (∀n. g n ⊆ g (SUC n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [SETS_TO_INCREASING_SETS']  Theorem
      
      ⊢ ∀f. ∃g.
          g 0 = ∅ ∧ (∀n. g n = BIGUNION (IMAGE f (count n))) ∧
          (∀n. g n ⊆ g (SUC n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
   
   [SUBSET_DIFF_DISJOINT]  Theorem
      
      ⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇒ DISJOINT s1 s3
   
   [SUBSET_DIFF_SUBSET]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t
   
   [SUBSET_INTER_SUBSET_L]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t
   
   [SUBSET_INTER_SUBSET_R]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ t
   
   [SUBSET_MONO_DIFF]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t DIFF r
   
   [SUBSET_RESTRICT_DIFF]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ r DIFF t ⊆ r DIFF s
   
   [SUBSET_RESTRICT_L]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t ∩ r
   
   [SUBSET_RESTRICT_R]  Theorem
      
      ⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ r ∩ t
   
   [SUBSET_TWO]  Theorem
      
      ⊢ ∀N s t. N ⊆ {s; t} ∧ N ≠ ∅ ⇒ N = {s} ∨ N = {t} ∨ N = {s; t}
   
   [UNION_BINARY]  Theorem
      
      ⊢ ∀a b. a ∪ b = BIGUNION {binary a b i | i ∈ 𝕌(:num)}
   
   [UNION_TO_3_DISJOINT_UNIONS]  Theorem
      
      ⊢ ∀s t.
          s ∪ t = s DIFF t ∪ s ∩ t ∪ (t DIFF s) ∧
          disjoint {s DIFF t; s ∩ t; t DIFF s}
   
   [count1_def]  Theorem
      
      ⊢ ∀n. count1 n = {m | m ≤ n}
   
   [count1_numseg]  Theorem
      
      ⊢ ∀n. count1 n = {0 .. n}
   
   [disjoint_family_def]  Theorem
      
      ⊢ ∀A. disjoint_family A ⇔ ∀i j. i ≠ j ⇒ DISJOINT (A i) (A j)
   
   [disjoint_family_disjoint]  Theorem
      
      ⊢ ∀A. disjoint_family (disjointed A)
   
   [disjoint_family_on_def]  Theorem
      
      ⊢ ∀A J.
          disjoint_family_on A J ⇔
          ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ DISJOINT (A i) (A j)
   
   [disjointed_subset]  Theorem
      
      ⊢ ∀A n. disjointed A n ⊆ A n
   
   [finite_decomposition]  Theorem
      
      ⊢ ∀c. FINITE c ⇒
            ∃f n.
              (∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n) ∧
              ∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j
   
   [finite_decomposition_simple]  Theorem
      
      ⊢ ∀c. FINITE c ⇒ ∃f n. (∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n)
   
   [finite_disjoint_decomposition]  Theorem
      
      ⊢ ∀c. FINITE c ∧ disjoint c ⇒
            ∃f n.
              (∀i. i < n ⇒ f i ∈ c) ∧ c = IMAGE f (count n) ∧
              (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
              ∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
   
   [finite_disjoint_decomposition']  Theorem
      
      ⊢ ∀c. FINITE c ∧ disjoint c ⇒
            ∃f n.
              (∀i. i < n ⇒ f i ∈ c) ∧ (∀i. n ≤ i ⇒ f i = ∅) ∧
              c = IMAGE f (count n) ∧
              BIGUNION c = BIGUNION (IMAGE f 𝕌(:num)) ∧
              (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
              ∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
   
   [finite_enumeration_of_sets_has_max_non_empty]  Theorem
      
      ⊢ ∀f s.
          FINITE s ∧ (∀x. f x ∈ s) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          ∃N. ∀n. n ≥ N ⇒ f n = ∅
   
   [infinitely_often_lemma]  Theorem
      
      ⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n
   
   [infinity_bound_lemma]  Theorem
      
      ⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N
   
   [set_limsup_alt]  Theorem
      
      ⊢ ∀E. limsup E =
            BIGINTER (IMAGE (λn. BIGUNION (IMAGE E (from n))) 𝕌(:num))
   
   [tail_countable]  Theorem
      
      ⊢ ∀A m. countable {A n | m ≤ n}
   
   [tail_not_empty]  Theorem
      
      ⊢ ∀A m. {A n | m ≤ n} ≠ ∅
   
   
*)
end

HOL 4, Trindemossen-1