Theory: probExtra

Parents

Types

Constants

Definitions

COMPL_def 
|- !s. COMPL s = UNIV DIFF s
inf_def 
|- !P. inf P = ~sup (IMAGE $~ P)

Theorems

ABS_BETWEEN_LE 
|- !x y d. 0 <= d /\ x - d <= y /\ y <= x + d = abs (y - x) <= d
ABS_UNIT_INTERVAL 
|- !x y. 0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1 ==> abs (x - y) <= 1
APPEND_MEM 
|- !x l1 l2. MEM x (APPEND l1 l2) = MEM x l1 \/ MEM x l2
BOOL_BOOL_CASES 
|- !P. P (\b. F) /\ P (\b. T) /\ P (\b. b) /\ P (\b. ~b) ==> !f. P f
BOOL_BOOL_CASES_THM 
|- !f. (f = (\b. F)) \/ (f = (\b. T)) \/ (f = (\b. b)) \/ (f = (\b. ~b))
COMPL_CLAUSES 
|- !s. (COMPL s INTER s = {}) /\ (COMPL s UNION s = UNIV)
COMPL_COMPL 
|- !s. COMPL (COMPL s) = s
COMPL_SPLITS 
|- !p q. p INTER q UNION COMPL p INTER q = q
DIV_THEN_MULT 
|- !p q. SUC q * (p DIV SUC q) <= p
DIV_TWO 
|- !n. n = 2 * (n DIV 2) + n MOD 2
DIV_TWO_BASIC 
|- (0 DIV 2 = 0) /\ (1 DIV 2 = 0) /\ (2 DIV 2 = 1)
DIV_TWO_CANCEL 
|- !n. (2 * n DIV 2 = n) /\ (SUC (2 * n) DIV 2 = n)
DIV_TWO_EXP 
|- !n k. k DIV 2 < 2 ** n = k < 2 ** SUC n
DIV_TWO_MONO 
|- !m n. m DIV 2 < n DIV 2 ==> m < n
DIV_TWO_MONO_EVEN 
|- !m n. EVEN n ==> (m DIV 2 < n DIV 2 = m < n)
DIV_TWO_UNIQUE 
|- !n q r.
     (n = 2 * q + r) /\ ((r = 0) \/ (r = 1)) ==>
     (q = n DIV 2) /\ (r = n MOD 2)
DIVISION_TWO 
|- !n. (n = 2 * (n DIV 2) + n MOD 2) /\ ((n MOD 2 = 0) \/ (n MOD 2 = 1))
EQ_EXT_EQ 
|- !f g. (!x. f x = g x) = (f = g)
EVEN_EXP_TWO 
|- !n. EVEN (2 ** n) = ~(n = 0)
EVEN_ODD_BASIC 
|- EVEN 0 /\ ~EVEN 1 /\ EVEN 2 /\ ~ODD 0 /\ ODD 1 /\ ~ODD 2
EVEN_ODD_EXISTS_EQ 
|- !n. (EVEN n = ?m. n = 2 * m) /\ (ODD n = ?m. n = SUC (2 * m))
EXISTS_LONGEST 
|- !x y. ?z. MEM z (x::y) /\ !w. MEM w (x::y) ==> LENGTH w <= LENGTH z
EXP_DIV_TWO 
|- !n. 2 ** SUC n DIV 2 = 2 ** n
FILTER_FALSE 
|- !l. FILTER (\x. F) l = []
FILTER_MEM 
|- !P x l. MEM x (FILTER P l) ==> P x
FILTER_OUT_ELT 
|- !x l. MEM x l \/ (FILTER (\y. ~(y = x)) l = l)
FILTER_TRUE 
|- !l. FILTER (\x. T) l = l
FOLDR_MAP 
|- !f e g l. FOLDR f e (MAP g l) = FOLDR (\x y. f (g x) y) e l
GSPEC_DEF_ALT 
|- !f. GSPEC f = (\v. ?x. (v,T) = f x)
HALF_CANCEL 
|- 2 * (1 / 2) = 1
HALF_LT_1 
|- 1 / 2 < 1
HALF_POS 
|- 0 < 1 / 2
IN_COMPL 
|- !x s. x IN COMPL s = ~(x IN s)
IN_EMPTY 
|- !x. ~(x IN {})
INF_DEF_ALT 
|- !P. inf P = ~sup (\r. P ~r)
INTER_IS_EMPTY 
|- !s t. (s INTER t = {}) = !x. ~s x \/ ~t x
INTER_UNION_COMPL 
|- !s t. s INTER t = COMPL (COMPL s UNION COMPL t)
INTER_UNION_RDISTRIB 
|- !p q r. (p UNION q) INTER r = p INTER r UNION q INTER r
INV_SUC 
|- !n. 0 < 1 / & (SUC n) /\ 1 / & (SUC n) <= 1
INV_SUC_MAX 
|- !n. 1 / & (SUC n) <= 1
INV_SUC_POS 
|- !n. 0 < 1 / & (SUC n)
IS_PREFIX_ANTISYM 
|- !x y. IS_PREFIX y x /\ IS_PREFIX x y ==> (x = y)
IS_PREFIX_BUTLAST 
|- !x y. IS_PREFIX (x::y) (BUTLAST (x::y))
IS_PREFIX_LENGTH 
|- !x y. IS_PREFIX y x ==> LENGTH x <= LENGTH y
IS_PREFIX_LENGTH_ANTI 
|- !x y. IS_PREFIX y x /\ (LENGTH x = LENGTH y) ==> (x = y)
IS_PREFIX_NIL 
|- !x. IS_PREFIX x [] /\ (IS_PREFIX [] x = (x = []))
IS_PREFIX_REFL 
|- !x. IS_PREFIX x x
IS_PREFIX_SNOC 
|- !x y z. IS_PREFIX (SNOC x y) z = IS_PREFIX y z \/ (z = SNOC x y)
IS_PREFIX_TRANS 
|- !x y z. IS_PREFIX x y /\ IS_PREFIX y z ==> IS_PREFIX x z
LAST_MAP_CONS 
|- !b h t. ?x. LAST (MAP (CONS b) (h::t)) = b::x
LAST_MEM 
|- !h t. MEM (LAST (h::t)) (h::t)
LENGTH_FILTER 
|- !P l. LENGTH (FILTER P l) <= LENGTH l
MAP_ID 
|- !l. MAP (\x. x) l = l
MAP_MEM 
|- !f l x. MEM x (MAP f l) = ?y. MEM y l /\ (x = f y)
MEM_FILTER 
|- !P l x. MEM x (FILTER P l) ==> MEM x l
MEM_NIL 
|- !l. (!x. ~MEM x l) = (l = [])
MEM_NIL_MAP_CONS 
|- !x l. ~MEM [] (MAP (CONS x) l)
MOD_TWO 
|- !n. n MOD 2 = (if EVEN n then 0 else 1)
ONE_MINUS_HALF 
|- 1 - 1 / 2 = 1 / 2
POW_HALF_EXP 
|- !n. (1 / 2) pow n = inv (& (2 ** n))
POW_HALF_MONO 
|- !m n. m <= n ==> (1 / 2) pow n <= (1 / 2) pow m
POW_HALF_POS 
|- !n. 0 < (1 / 2) pow n
POW_HALF_TWICE 
|- !n. (1 / 2) pow n = 2 * (1 / 2) pow SUC n
RAND_THM 
|- !f x y. (x = y) ==> (f x = f y)
REAL_INF_MIN 
|- !P z. P z /\ (!x. P x ==> z <= x) ==> (inf P = z)
REAL_INVINV_ALL 
|- !x. inv (inv x) = x
REAL_LE_EQ 
|- !x y. x <= y /\ y <= x ==> (x = y)
REAL_LE_INV_LE 
|- !x y. 0 < x /\ x <= y ==> inv y <= inv x
REAL_POW 
|- !m n. & m pow n = & (m ** n)
REAL_SUP_EXISTS_UNIQUE 
|- !P.
     (?x. P x) /\ (?z. !x. P x ==> x <= z) ==>
     ?!s. !y. (?x. P x /\ y < x) = y < s
REAL_SUP_LE_X 
|- !P x. (?r. P r) /\ (!r. P r ==> r <= x) ==> sup P <= x
REAL_SUP_MAX 
|- !P z. P z /\ (!x. P x ==> x <= z) ==> (sup P = z)
REAL_X_LE_SUP 
|- !P x.
     (?r. P r) /\ (?z. !r. P r ==> r <= z) /\ (?r. P r /\ x <= r) ==>
     x <= sup P
SET_EQ_EXT 
|- !s t. (s = t) = !v. v IN s = v IN t
SUBSET_EQ 
|- !s t. (s = t) = s SUBSET t /\ t SUBSET s
SUBSET_EQ_DECOMP 
|- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)
UNION_DEF_ALT 
|- !s t. s UNION t = (\x. s x \/ t x)
UNION_DISJOINT_SPLIT 
|- !s t u.
     (s UNION t = s UNION u) /\ (s INTER t = {}) /\ (s INTER u = {}) ==>
     (t = u)
X_HALF_HALF 
|- !x. 1 / 2 * x + 1 / 2 * x = x