Structure util_probTheory

signature util_probTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val disjoint_def : thm
    val from_def : thm
    val lg_def : thm
    val logr_def : thm
    val minimal_def : thm
    val pair_def : thm
    val powr_def : thm
    val prod_sets_def : thm
  
  (*  Theorems  *)
    val DISJOINT_COUNT_FROM : thm
    val DISJOINT_FROM_COUNT : thm
    val EQ_T_IMP : thm
    val FROM_0 : thm
    val GBIGUNION_IMAGE : thm
    val INF_CLOSE : thm
    val INF_DEF_ALT : thm
    val INF_GREATER : thm
    val INF_LE : thm
    val IN_FROM : thm
    val IN_PAIR : thm
    val IN_PROD_SETS : thm
    val IN_o : thm
    val LE_INF : thm
    val LOGR_MONO_LE : thm
    val LOGR_MONO_LE_IMP : thm
    val MINIMAL_EQ : thm
    val MINIMAL_EQ_IMP : thm
    val MINIMAL_EXISTS : thm
    val MINIMAL_EXISTS0 : thm
    val MINIMAL_EXISTS_IMP : thm
    val MINIMAL_SUC : thm
    val MINIMAL_SUC_IMP : thm
    val NUM_2D_BIJ : thm
    val NUM_2D_BIJ_INV : thm
    val NUM_2D_BIJ_NZ : thm
    val NUM_2D_BIJ_NZ_ALT : thm
    val NUM_2D_BIJ_NZ_ALT2 : thm
    val NUM_2D_BIJ_NZ_ALT2_INV : thm
    val NUM_2D_BIJ_NZ_ALT_INV : thm
    val NUM_2D_BIJ_NZ_INV : thm
    val PAIRED_BETA_THM : thm
    val PAIR_UNIV : thm
    val POW_HALF_MONO : thm
    val POW_HALF_POS : thm
    val POW_HALF_SMALL : thm
    val POW_NEG_ODD : thm
    val POW_POS_EVEN : thm
    val PREIMAGE_REAL_COMPL1 : thm
    val PREIMAGE_REAL_COMPL2 : thm
    val PREIMAGE_REAL_COMPL3 : thm
    val PREIMAGE_REAL_COMPL4 : thm
    val REAL_LE_LT_MUL : thm
    val REAL_LE_RDIV_EQ_NEG : thm
    val REAL_LT_LE_MUL : thm
    val REAL_LT_LMUL_0_NEG : thm
    val REAL_LT_LMUL_NEG_0 : thm
    val REAL_LT_LMUL_NEG_0_NEG : thm
    val REAL_LT_RDIV_EQ_NEG : thm
    val REAL_LT_RMUL_0_NEG : thm
    val REAL_LT_RMUL_NEG_0 : thm
    val REAL_LT_RMUL_NEG_0_NEG : thm
    val REAL_MUL_IDEMPOT : thm
    val REAL_NEG_NZ : thm
    val REAL_SUP_LE_X : thm
    val REAL_X_LE_SUP : thm
    val UNION_COUNT_FROM : thm
    val UNION_FROM_COUNT : thm
    val disjointD : thm
    val disjointI : thm
    val disjoint_empty : thm
    val disjoint_sing : thm
    val disjoint_union : thm
    val finite_enumeration_of_sets_has_max_non_empty : thm
    val lg_1 : thm
    val lg_2 : thm
    val lg_inv : thm
    val lg_mul : thm
    val lg_nonzero : thm
    val lg_pow : thm
    val logr_1 : thm
    val logr_div : thm
    val logr_inv : thm
    val logr_mul : thm
    val neg_lg : thm
    val neg_logr : thm
  
  val util_prob_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real_sigma] Parent theory of "util_prob"
   
   [disjoint_def]  Definition
      
      ⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ DISJOINT a b
   
   [from_def]  Definition
      
      ⊢ ∀n. from n = {m | n ≤ m}
   
   [lg_def]  Definition
      
      ⊢ ∀x. lg x = logr 2 x
   
   [logr_def]  Definition
      
      ⊢ ∀a x. logr a x = ln x / ln a
   
   [minimal_def]  Definition
      
      ⊢ ∀p. minimal p = @n. p n ∧ ∀m. m < n ⇒ ¬p m
   
   [pair_def]  Definition
      
      ⊢ ∀X Y. pair X Y = (λ(x,y). x ∈ X ∧ y ∈ Y)
   
   [powr_def]  Definition
      
      ⊢ ∀x a. x powr a = exp (a * ln x)
   
   [prod_sets_def]  Definition
      
      ⊢ ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}
   
   [DISJOINT_COUNT_FROM]  Theorem
      
      ⊢ ∀n. DISJOINT (count n) (from n)
   
   [DISJOINT_FROM_COUNT]  Theorem
      
      ⊢ ∀n. DISJOINT (from n) (count n)
   
   [EQ_T_IMP]  Theorem
      
      ⊢ ∀x. x ⇔ T ⇒ x
   
   [FROM_0]  Theorem
      
      ⊢ from 0 = 𝕌(:num)
   
   [GBIGUNION_IMAGE]  Theorem
      
      ⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))
   
   [INF_CLOSE]  Theorem
      
      ⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e
   
   [INF_DEF_ALT]  Theorem
      
      ⊢ ∀p. inf p = -sup (λr. -r ∈ p)
   
   [INF_GREATER]  Theorem
      
      ⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z
   
   [INF_LE]  Theorem
      
      ⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r
   
   [IN_FROM]  Theorem
      
      ⊢ ∀m n. m ∈ from n ⇔ n ≤ m
   
   [IN_PAIR]  Theorem
      
      ⊢ ∀x X Y. x ∈ pair X Y ⇔ FST x ∈ X ∧ SND x ∈ Y
   
   [IN_PROD_SETS]  Theorem
      
      ⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. (s = t × u) ∧ t ∈ a ∧ u ∈ b
   
   [IN_o]  Theorem
      
      ⊢ ∀x f s. x ∈ s ∘ f ⇔ f x ∈ s
   
   [LE_INF]  Theorem
      
      ⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p
   
   [LOGR_MONO_LE]  Theorem
      
      ⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)
   
   [LOGR_MONO_LE_IMP]  Theorem
      
      ⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y
   
   [MINIMAL_EQ]  Theorem
      
      ⊢ ∀p m. p m ∧ (m = minimal p) ⇔ p m ∧ ∀n. n < m ⇒ ¬p n
   
   [MINIMAL_EQ_IMP]  Theorem
      
      ⊢ ∀m p. p m ∧ (∀n. n < m ⇒ ¬p n) ⇒ (m = minimal p)
   
   [MINIMAL_EXISTS]  Theorem
      
      ⊢ ∀P. (∃n. P n) ⇔ P (minimal P) ∧ ∀n. n < minimal P ⇒ ¬P n
   
   [MINIMAL_EXISTS0]  Theorem
      
      ⊢ (∃n. P n) ⇔ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m
   
   [MINIMAL_EXISTS_IMP]  Theorem
      
      ⊢ ∀P. (∃n. P n) ⇒ ∃m. P m ∧ ∀n. n < m ⇒ ¬P n
   
   [MINIMAL_SUC]  Theorem
      
      ⊢ ∀n p.
            (SUC n = minimal p) ∧ p (SUC n) ⇔
            ¬p 0 ∧ (n = minimal (p ∘ SUC)) ∧ p (SUC n)
   
   [MINIMAL_SUC_IMP]  Theorem
      
      ⊢ ∀n p.
            p (SUC n) ∧ ¬p 0 ∧ (n = minimal (p ∘ SUC)) ⇒
            (SUC n = minimal p)
   
   [NUM_2D_BIJ]  Theorem
      
      ⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) 𝕌(:num)
   
   [NUM_2D_BIJ_INV]  Theorem
      
      ⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num))
   
   [NUM_2D_BIJ_NZ]  Theorem
      
      ⊢ ∃f. BIJ f (𝕌(:num) × (𝕌(:num) DIFF {0})) 𝕌(:num)
   
   [NUM_2D_BIJ_NZ_ALT]  Theorem
      
      ⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) (𝕌(:num) DIFF {0})
   
   [NUM_2D_BIJ_NZ_ALT2]  Theorem
      
      ⊢ ∃f. BIJ f ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0})) 𝕌(:num)
   
   [NUM_2D_BIJ_NZ_ALT2_INV]  Theorem
      
      ⊢ ∃f. BIJ f 𝕌(:num) ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0}))
   
   [NUM_2D_BIJ_NZ_ALT_INV]  Theorem
      
      ⊢ ∃f. BIJ f (𝕌(:num) DIFF {0}) (𝕌(:num) × 𝕌(:num))
   
   [NUM_2D_BIJ_NZ_INV]  Theorem
      
      ⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × (𝕌(:num) DIFF {0}))
   
   [PAIRED_BETA_THM]  Theorem
      
      ⊢ ∀f z. UNCURRY f z = f (FST z) (SND z)
   
   [PAIR_UNIV]  Theorem
      
      ⊢ pair 𝕌(:α) 𝕌(:β) = 𝕌(:α # β)
   
   [POW_HALF_MONO]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m
   
   [POW_HALF_POS]  Theorem
      
      ⊢ ∀n. 0 < (1 / 2) pow n
   
   [POW_HALF_SMALL]  Theorem
      
      ⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e
   
   [POW_NEG_ODD]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
   
   [POW_POS_EVEN]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
   
   [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}
   
   [REAL_LE_LT_MUL]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
   
   [REAL_LE_RDIV_EQ_NEG]  Theorem
      
      ⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)
   
   [REAL_LT_LE_MUL]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
   
   [REAL_LT_LMUL_0_NEG]  Theorem
      
      ⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0
   
   [REAL_LT_LMUL_NEG_0]  Theorem
      
      ⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0
   
   [REAL_LT_LMUL_NEG_0_NEG]  Theorem
      
      ⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y
   
   [REAL_LT_RDIV_EQ_NEG]  Theorem
      
      ⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)
   
   [REAL_LT_RMUL_0_NEG]  Theorem
      
      ⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0
   
   [REAL_LT_RMUL_NEG_0]  Theorem
      
      ⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0
   
   [REAL_LT_RMUL_NEG_0_NEG]  Theorem
      
      ⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x
   
   [REAL_MUL_IDEMPOT]  Theorem
      
      ⊢ ∀r. (r * r = r) ⇔ (r = 0) ∨ (r = 1)
   
   [REAL_NEG_NZ]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ x ≠ 0
   
   [REAL_SUP_LE_X]  Theorem
      
      ⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x
   
   [REAL_X_LE_SUP]  Theorem
      
      ⊢ ∀P x.
            (∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒
            x ≤ sup P
   
   [UNION_COUNT_FROM]  Theorem
      
      ⊢ ∀n. count n ∪ from n = 𝕌(:num)
   
   [UNION_FROM_COUNT]  Theorem
      
      ⊢ ∀n. from n ∪ count n = 𝕌(:num)
   
   [disjointD]  Theorem
      
      ⊢ ∀A a b. disjoint A ⇒ a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b
   
   [disjointI]  Theorem
      
      ⊢ ∀A. (∀a b. a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b) ⇒ disjoint A
   
   [disjoint_empty]  Theorem
      
      ⊢ disjoint ∅
   
   [disjoint_sing]  Theorem
      
      ⊢ ∀a. disjoint {a}
   
   [disjoint_union]  Theorem
      
      ⊢ ∀A B.
            disjoint A ∧ disjoint B ∧ (BIGUNION A ∩ BIGUNION B = ∅) ⇒
            disjoint (A ∪ B)
   
   [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 = ∅)
   
   [lg_1]  Theorem
      
      ⊢ lg 1 = 0
   
   [lg_2]  Theorem
      
      ⊢ lg 2 = 1
   
   [lg_inv]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ (lg x⁻¹ = -lg x)
   
   [lg_mul]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (lg (x * y) = lg x + lg y)
   
   [lg_nonzero]  Theorem
      
      ⊢ ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)
   
   [lg_pow]  Theorem
      
      ⊢ ∀n. lg (2 pow n) = &n
   
   [logr_1]  Theorem
      
      ⊢ ∀b. logr b 1 = 0
   
   [logr_div]  Theorem
      
      ⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x / y) = logr b x − logr b y)
   
   [logr_inv]  Theorem
      
      ⊢ ∀b x. 0 < x ⇒ (logr b x⁻¹ = -logr b x)
   
   [logr_mul]  Theorem
      
      ⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x * y) = logr b x + logr b y)
   
   [neg_lg]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ (-lg x = lg x⁻¹)
   
   [neg_logr]  Theorem
      
      ⊢ ∀b x. 0 < x ⇒ (-logr b x = logr b x⁻¹)
   
   
*)
end

HOL 4, Kananaskis-13