Structure util_probTheory
signature util_probTheory =
sig
type thm = Thm.thm
(* Definitions *)
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 EQ_T_IMP : thm
val GBIGUNION_IMAGE : thm
val HALF_CANCEL : thm
val HALF_LT_1 : thm
val HALF_POS : thm
val INCREASING_SEQ : thm
val INF_CLOSE : thm
val INF_DEF_ALT : thm
val INF_GREATER : thm
val INF_LE : thm
val IN_PAIR : thm
val IN_PROD_SETS : thm
val IN_o : thm
val K_PARTIAL : thm
val LE_INF : thm
val LE_SUC : thm
val LT_SUC : thm
val MAX_LE_X : 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_BIG_SQUARE : 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 NUM_2D_BIJ_SMALL_SQUARE : thm
val ONE_MINUS_HALF : thm
val PAIRED_BETA_THM : thm
val PAIR_UNIV : thm
val POS_SUMMABLE : thm
val POW_HALF_MONO : thm
val POW_HALF_POS : thm
val POW_HALF_SER : thm
val POW_HALF_SMALL : 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_LT_LE_MUL : thm
val REAL_MUL_IDEMPOT : thm
val REAL_SUP_LE_X : thm
val REAL_X_LE_SUP : thm
val SEQ_SANDWICH : thm
val SER_POS : thm
val SER_POS_COMPARE : thm
val SER_POS_MONO : thm
val SUMINF_2D : thm
val SUMINF_ADD : thm
val SUMINF_POS : thm
val SUMMABLE_LE : thm
val SUMS_EQ : thm
val SUMS_ZERO : thm
val SUM_CONST_R : thm
val SUM_LT : thm
val SUM_PICK : thm
val TRANSFORM_2D_NUM : thm
val TRIANGLE_2D_NUM : thm
val X_HALF_HALF : thm
val X_LE_MAX : 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"
[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}
[EQ_T_IMP] Theorem
⊢ ∀x. x ⇔ T ⇒ x
[GBIGUNION_IMAGE] Theorem
⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))
[HALF_CANCEL] Theorem
⊢ 2 * (1 / 2) = 1
[HALF_LT_1] Theorem
⊢ 1 / 2 < 1
[HALF_POS] Theorem
⊢ 0 < 1 / 2
[INCREASING_SEQ] Theorem
⊢ ∀f l.
(∀n. f n ≤ f (SUC n)) ∧ (∀n. f n ≤ l) ∧
(∀e. 0 < e ⇒ ∃n. l < f n + e) ⇒
f --> l
[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_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
[K_PARTIAL] Theorem
⊢ ∀x. K x = (λz. x)
[LE_INF] Theorem
⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p
[LE_SUC] Theorem
⊢ ∀a b. a ≤ SUC b ⇔ a ≤ b ∨ (a = SUC b)
[LT_SUC] Theorem
⊢ ∀a b. a < SUC b ⇔ a < b ∨ (a = b)
[MAX_LE_X] Theorem
⊢ ∀m n k. MAX m n ≤ k ⇔ m ≤ k ∧ n ≤ k
[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_BIG_SQUARE] Theorem
⊢ ∀f N.
BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
∃k. IMAGE f (count N) ⊆ count k × count k
[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}))
[NUM_2D_BIJ_SMALL_SQUARE] Theorem
⊢ ∀f k.
BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
∃N. count k × count k ⊆ IMAGE f (count N)
[ONE_MINUS_HALF] Theorem
⊢ 1 − 1 / 2 = 1 / 2
[PAIRED_BETA_THM] Theorem
⊢ ∀f z. UNCURRY f z = f (FST z) (SND z)
[PAIR_UNIV] Theorem
⊢ pair 𝕌(:α) 𝕌(:β) = 𝕌(:α # β)
[POS_SUMMABLE] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃x. ∀n. sum (0,n) f ≤ x) ⇒ summable f
[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_SER] Theorem
⊢ (λn. (1 / 2) pow (n + 1)) sums 1
[POW_HALF_SMALL] Theorem
⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e
[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_LT_LE_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[REAL_MUL_IDEMPOT] Theorem
⊢ ∀r. (r * r = r) ⇔ (r = 0) ∨ (r = 1)
[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
[SEQ_SANDWICH] Theorem
⊢ ∀f g h l. f --> l ∧ h --> l ∧ (∀n. f n ≤ g n ∧ g n ≤ h n) ⇒ g --> l
[SER_POS] Theorem
⊢ ∀f. summable f ∧ (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
[SER_POS_COMPARE] Theorem
⊢ ∀f g.
(∀n. 0 ≤ f n) ∧ summable g ∧ (∀n. f n ≤ g n) ⇒
summable f ∧ suminf f ≤ suminf g
[SER_POS_MONO] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ⇒ mono (λn. sum (0,n) f)
[SUMINF_2D] Theorem
⊢ ∀f g h.
(∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
UNCURRY f ∘ h sums suminf g
[SUMINF_ADD] Theorem
⊢ ∀f g.
summable f ∧ summable g ⇒
summable (λn. f n + g n) ∧
(suminf f + suminf g = suminf (λn. f n + g n))
[SUMINF_POS] Theorem
⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ 0 ≤ suminf f
[SUMMABLE_LE] Theorem
⊢ ∀f x. summable f ∧ (∀n. sum (0,n) f ≤ x) ⇒ suminf f ≤ x
[SUMS_EQ] Theorem
⊢ ∀f x. f sums x ⇔ summable f ∧ (suminf f = x)
[SUMS_ZERO] Theorem
⊢ K 0 sums 0
[SUM_CONST_R] Theorem
⊢ ∀n r. sum (0,n) (K r) = &n * r
[SUM_LT] Theorem
⊢ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r < g r) ∧ 0 < n ⇒
sum (m,n) f < sum (m,n) g
[SUM_PICK] Theorem
⊢ ∀n k x.
sum (0,n) (λm. if m = k then x else 0) = if k < n then x else 0
[TRANSFORM_2D_NUM] Theorem
⊢ ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n
[TRIANGLE_2D_NUM] Theorem
⊢ ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n
[X_HALF_HALF] Theorem
⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x
[X_LE_MAX] Theorem
⊢ ∀m n k. k ≤ MAX m n ⇔ k ≤ m ∨ k ≤ n
[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-11