--- a/src/HOL/Import/HOL/HOL4Prob.thy Mon Sep 26 02:06:44 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Mon Sep 26 02:27:14 2005 +0200
@@ -4,16 +4,22 @@
;setup_theory prob_extra
-lemma BOOL_BOOL_CASES_THM: "ALL f. f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
+lemma BOOL_BOOL_CASES_THM: "ALL f::bool => bool.
+ f = (%b::bool. False) |
+ f = (%b::bool. True) | f = (%b::bool. b) | f = Not"
by (import prob_extra BOOL_BOOL_CASES_THM)
-lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
+lemma EVEN_ODD_BASIC: "EVEN (0::nat) &
+~ EVEN (1::nat) &
+EVEN (2::nat) & ~ ODD (0::nat) & ODD (1::nat) & ~ ODD (2::nat)"
by (import prob_extra EVEN_ODD_BASIC)
-lemma EVEN_ODD_EXISTS_EQ: "ALL n. EVEN n = (EX m. n = 2 * m) & ODD n = (EX m. n = Suc (2 * m))"
+lemma EVEN_ODD_EXISTS_EQ: "ALL n::nat.
+ EVEN n = (EX m::nat. n = (2::nat) * m) &
+ ODD n = (EX m::nat. n = Suc ((2::nat) * m))"
by (import prob_extra EVEN_ODD_EXISTS_EQ)
-lemma DIV_THEN_MULT: "ALL p q. Suc q * (p div Suc q) <= p"
+lemma DIV_THEN_MULT: "ALL (p::nat) q::nat. Suc q * (p div Suc q) <= p"
by (import prob_extra DIV_THEN_MULT)
lemma DIV_TWO_UNIQUE: "(All::(nat => bool) => bool)
@@ -62,7 +68,8 @@
lemma DIV_TWO: "ALL n::nat. n = (2::nat) * (n div (2::nat)) + n mod (2::nat)"
by (import prob_extra DIV_TWO)
-lemma MOD_TWO: "ALL n. n mod 2 = (if EVEN n then 0 else 1)"
+lemma MOD_TWO: "(ALL (n::nat).
+ ((n mod (2::nat)) = (if (EVEN n) then (0::nat) else (1::nat))))"
by (import prob_extra MOD_TWO)
lemma DIV_TWO_BASIC: "(0::nat) div (2::nat) = (0::nat) &
@@ -112,13 +119,14 @@
((op <::nat => nat => bool) m n))))"
by (import prob_extra DIV_TWO_MONO_EVEN)
-lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
+lemma DIV_TWO_CANCEL: "ALL n::nat.
+ (2::nat) * n div (2::nat) = n & Suc ((2::nat) * n) div (2::nat) = n"
by (import prob_extra DIV_TWO_CANCEL)
lemma EXP_DIV_TWO: "ALL n::nat. (2::nat) ^ Suc n div (2::nat) = (2::nat) ^ n"
by (import prob_extra EXP_DIV_TWO)
-lemma EVEN_EXP_TWO: "ALL n. EVEN (2 ^ n) = (n ~= 0)"
+lemma EVEN_EXP_TWO: "ALL n::nat. EVEN ((2::nat) ^ n) = (n ~= (0::nat))"
by (import prob_extra EVEN_EXP_TWO)
lemma DIV_TWO_EXP: "ALL (n::nat) k::nat.
@@ -129,12 +137,12 @@
inf :: "(real => bool) => real"
defs
- inf_primdef: "inf == %P. - sup (IMAGE uminus P)"
-
-lemma inf_def: "ALL P. inf P = - sup (IMAGE uminus P)"
+ inf_primdef: "inf == %P::real => bool. - sup (IMAGE uminus P)"
+
+lemma inf_def: "ALL P::real => bool. inf P = - sup (IMAGE uminus P)"
by (import prob_extra inf_def)
-lemma INF_DEF_ALT: "ALL P. inf P = - sup (%r. P (- r))"
+lemma INF_DEF_ALT: "ALL P::real => bool. inf P = - sup (%r::real. P (- r))"
by (import prob_extra INF_DEF_ALT)
lemma REAL_SUP_EXISTS_UNIQUE: "(All::((real => bool) => bool) => bool)
@@ -275,13 +283,15 @@
lemma POW_HALF_EXP: "ALL n::nat. ((1::real) / (2::real)) ^ n = inverse (real ((2::nat) ^ n))"
by (import prob_extra POW_HALF_EXP)
-lemma INV_SUC_POS: "ALL n. 0 < 1 / real (Suc n)"
+lemma INV_SUC_POS: "ALL n::nat. (0::real) < (1::real) / real (Suc n)"
by (import prob_extra INV_SUC_POS)
-lemma INV_SUC_MAX: "ALL x. 1 / real (Suc x) <= 1"
+lemma INV_SUC_MAX: "ALL x::nat. (1::real) / real (Suc x) <= (1::real)"
by (import prob_extra INV_SUC_MAX)
-lemma INV_SUC: "ALL n. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
+lemma INV_SUC: "ALL n::nat.
+ (0::real) < (1::real) / real (Suc n) &
+ (1::real) / real (Suc n) <= (1::real)"
by (import prob_extra INV_SUC)
lemma ABS_UNIT_INTERVAL: "(All::(real => bool) => bool)
@@ -301,181 +311,200 @@
(1::real))))"
by (import prob_extra ABS_UNIT_INTERVAL)
-lemma MEM_NIL: "ALL l. (ALL x. ~ x mem l) = (l = [])"
+lemma MEM_NIL: "ALL l::'a::type list. (ALL x::'a::type. ~ x mem l) = (l = [])"
by (import prob_extra MEM_NIL)
-lemma MAP_MEM: "ALL f l x. x mem map f l = (EX y. y mem l & x = f y)"
+lemma MAP_MEM: "ALL (f::'a::type => 'b::type) (l::'a::type list) x::'b::type.
+ x mem map f l = (EX y::'a::type. y mem l & x = f y)"
by (import prob_extra MAP_MEM)
-lemma MEM_NIL_MAP_CONS: "ALL x l. ~ [] mem map (op # x) l"
+lemma MEM_NIL_MAP_CONS: "ALL (x::'a::type) l::'a::type list list. ~ [] mem map (op # x) l"
by (import prob_extra MEM_NIL_MAP_CONS)
-lemma FILTER_TRUE: "ALL l. [x:l. True] = l"
+lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type:l. True] = l"
by (import prob_extra FILTER_TRUE)
-lemma FILTER_FALSE: "ALL l. [x:l. False] = []"
+lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type:l. False] = []"
by (import prob_extra FILTER_FALSE)
-lemma FILTER_MEM: "(All::(('a => bool) => bool) => bool)
- (%P::'a => bool.
- (All::('a => bool) => bool)
- (%x::'a.
- (All::('a list => bool) => bool)
- (%l::'a list.
+lemma FILTER_MEM: "(All::(('a::type => bool) => bool) => bool)
+ (%P::'a::type => bool.
+ (All::('a::type => bool) => bool)
+ (%x::'a::type.
+ (All::('a::type list => bool) => bool)
+ (%l::'a::type list.
(op -->::bool => bool => bool)
- ((op mem::'a => 'a list => bool) x
- ((filter::('a => bool) => 'a list => 'a list) P l))
+ ((op mem::'a::type => 'a::type list => bool) x
+ ((filter::('a::type => bool)
+ => 'a::type list => 'a::type list)
+ P l))
(P x))))"
by (import prob_extra FILTER_MEM)
-lemma MEM_FILTER: "(All::(('a => bool) => bool) => bool)
- (%P::'a => bool.
- (All::('a list => bool) => bool)
- (%l::'a list.
- (All::('a => bool) => bool)
- (%x::'a.
+lemma MEM_FILTER: "(All::(('a::type => bool) => bool) => bool)
+ (%P::'a::type => bool.
+ (All::('a::type list => bool) => bool)
+ (%l::'a::type list.
+ (All::('a::type => bool) => bool)
+ (%x::'a::type.
(op -->::bool => bool => bool)
- ((op mem::'a => 'a list => bool) x
- ((filter::('a => bool) => 'a list => 'a list) P l))
- ((op mem::'a => 'a list => bool) x l))))"
+ ((op mem::'a::type => 'a::type list => bool) x
+ ((filter::('a::type => bool)
+ => 'a::type list => 'a::type list)
+ P l))
+ ((op mem::'a::type => 'a::type list => bool) x l))))"
by (import prob_extra MEM_FILTER)
-lemma FILTER_OUT_ELT: "ALL x l. x mem l | [y:l. y ~= x] = l"
+lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type:l. y ~= x] = l"
by (import prob_extra FILTER_OUT_ELT)
-lemma IS_PREFIX_NIL: "ALL x. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
+lemma IS_PREFIX_NIL: "ALL x::'a::type list. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
by (import prob_extra IS_PREFIX_NIL)
-lemma IS_PREFIX_REFL: "ALL x. IS_PREFIX x x"
+lemma IS_PREFIX_REFL: "ALL x::'a::type list. IS_PREFIX x x"
by (import prob_extra IS_PREFIX_REFL)
-lemma IS_PREFIX_ANTISYM: "(All::('a list => bool) => bool)
- (%x::'a list.
- (All::('a list => bool) => bool)
- (%y::'a list.
+lemma IS_PREFIX_ANTISYM: "(All::('a::type list => bool) => bool)
+ (%x::'a::type list.
+ (All::('a::type list => bool) => bool)
+ (%y::'a::type list.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((IS_PREFIX::'a list => 'a list => bool) y x)
- ((IS_PREFIX::'a list => 'a list => bool) x y))
- ((op =::'a list => 'a list => bool) x y)))"
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) y x)
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) x y))
+ ((op =::'a::type list => 'a::type list => bool) x y)))"
by (import prob_extra IS_PREFIX_ANTISYM)
-lemma IS_PREFIX_TRANS: "(All::('a list => bool) => bool)
- (%x::'a list.
- (All::('a list => bool) => bool)
- (%y::'a list.
- (All::('a list => bool) => bool)
- (%z::'a list.
+lemma IS_PREFIX_TRANS: "(All::('a::type list => bool) => bool)
+ (%x::'a::type list.
+ (All::('a::type list => bool) => bool)
+ (%y::'a::type list.
+ (All::('a::type list => bool) => bool)
+ (%z::'a::type list.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((IS_PREFIX::'a list => 'a list => bool) x y)
- ((IS_PREFIX::'a list => 'a list => bool) y z))
- ((IS_PREFIX::'a list => 'a list => bool) x z))))"
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) x y)
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) y z))
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) x z))))"
by (import prob_extra IS_PREFIX_TRANS)
-lemma IS_PREFIX_BUTLAST: "ALL x y. IS_PREFIX (x # y) (butlast (x # y))"
+lemma IS_PREFIX_BUTLAST: "ALL (x::'a::type) y::'a::type list. IS_PREFIX (x # y) (butlast (x # y))"
by (import prob_extra IS_PREFIX_BUTLAST)
-lemma IS_PREFIX_LENGTH: "(All::('a list => bool) => bool)
- (%x::'a list.
- (All::('a list => bool) => bool)
- (%y::'a list.
+lemma IS_PREFIX_LENGTH: "(All::('a::type list => bool) => bool)
+ (%x::'a::type list.
+ (All::('a::type list => bool) => bool)
+ (%y::'a::type list.
(op -->::bool => bool => bool)
- ((IS_PREFIX::'a list => 'a list => bool) y x)
- ((op <=::nat => nat => bool) ((size::'a list => nat) x)
- ((size::'a list => nat) y))))"
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) y x)
+ ((op <=::nat => nat => bool) ((size::'a::type list => nat) x)
+ ((size::'a::type list => nat) y))))"
by (import prob_extra IS_PREFIX_LENGTH)
-lemma IS_PREFIX_LENGTH_ANTI: "(All::('a list => bool) => bool)
- (%x::'a list.
- (All::('a list => bool) => bool)
- (%y::'a list.
+lemma IS_PREFIX_LENGTH_ANTI: "(All::('a::type list => bool) => bool)
+ (%x::'a::type list.
+ (All::('a::type list => bool) => bool)
+ (%y::'a::type list.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((IS_PREFIX::'a list => 'a list => bool) y x)
- ((op =::nat => nat => bool) ((size::'a list => nat) x)
- ((size::'a list => nat) y)))
- ((op =::'a list => 'a list => bool) x y)))"
+ ((IS_PREFIX::'a::type list => 'a::type list => bool) y x)
+ ((op =::nat => nat => bool) ((size::'a::type list => nat) x)
+ ((size::'a::type list => nat) y)))
+ ((op =::'a::type list => 'a::type list => bool) x y)))"
by (import prob_extra IS_PREFIX_LENGTH_ANTI)
-lemma IS_PREFIX_SNOC: "ALL x y z. IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
+lemma IS_PREFIX_SNOC: "ALL (x::'a::type) (y::'a::type list) z::'a::type list.
+ IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
by (import prob_extra IS_PREFIX_SNOC)
-lemma FOLDR_MAP: "ALL (f::'b => 'c => 'c) (e::'c) (g::'a => 'b) l::'a list.
- foldr f (map g l) e = foldr (%x::'a. f (g x)) l e"
+lemma FOLDR_MAP: "ALL (f::'b::type => 'c::type => 'c::type) (e::'c::type)
+ (g::'a::type => 'b::type) l::'a::type list.
+ foldr f (map g l) e = foldr (%x::'a::type. f (g x)) l e"
by (import prob_extra FOLDR_MAP)
-lemma LAST_MEM: "ALL h t. last (h # t) mem h # t"
+lemma LAST_MEM: "ALL (h::'a::type) t::'a::type list. last (h # t) mem h # t"
by (import prob_extra LAST_MEM)
lemma LAST_MAP_CONS: "ALL (b::bool) (h::bool list) t::bool list list.
EX x::bool list. last (map (op # b) (h # t)) = b # x"
by (import prob_extra LAST_MAP_CONS)
-lemma EXISTS_LONGEST: "(All::('a list => bool) => bool)
- (%x::'a list.
- (All::('a list list => bool) => bool)
- (%y::'a list list.
- (Ex::('a list => bool) => bool)
- (%z::'a list.
+lemma EXISTS_LONGEST: "(All::('a::type list => bool) => bool)
+ (%x::'a::type list.
+ (All::('a::type list list => bool) => bool)
+ (%y::'a::type list list.
+ (Ex::('a::type list => bool) => bool)
+ (%z::'a::type list.
(op &::bool => bool => bool)
- ((op mem::'a list => 'a list list => bool) z
- ((op #::'a list => 'a list list => 'a list list) x y))
- ((All::('a list => bool) => bool)
- (%w::'a list.
+ ((op mem::'a::type list => 'a::type list list => bool) z
+ ((op #::'a::type list
+ => 'a::type list list => 'a::type list list)
+ x y))
+ ((All::('a::type list => bool) => bool)
+ (%w::'a::type list.
(op -->::bool => bool => bool)
- ((op mem::'a list => 'a list list => bool) w
- ((op #::'a list => 'a list list => 'a list list) x
- y))
+ ((op mem::'a::type list
+ => 'a::type list list => bool)
+ w ((op #::'a::type list
+ => 'a::type list list
+=> 'a::type list list)
+ x y))
((op <=::nat => nat => bool)
- ((size::'a list => nat) w)
- ((size::'a list => nat) z)))))))"
+ ((size::'a::type list => nat) w)
+ ((size::'a::type list => nat) z)))))))"
by (import prob_extra EXISTS_LONGEST)
-lemma UNION_DEF_ALT: "ALL s t. pred_set.UNION s t = (%x. s x | t x)"
+lemma UNION_DEF_ALT: "ALL (s::'a::type => bool) t::'a::type => bool.
+ pred_set.UNION s t = (%x::'a::type. s x | t x)"
by (import prob_extra UNION_DEF_ALT)
-lemma INTER_UNION_RDISTRIB: "ALL p q r.
+lemma INTER_UNION_RDISTRIB: "ALL (p::'a::type => bool) (q::'a::type => bool) r::'a::type => bool.
pred_set.INTER (pred_set.UNION p q) r =
pred_set.UNION (pred_set.INTER p r) (pred_set.INTER q r)"
by (import prob_extra INTER_UNION_RDISTRIB)
-lemma SUBSET_EQ: "ALL x xa. (x = xa) = (SUBSET x xa & SUBSET xa x)"
+lemma SUBSET_EQ: "ALL (x::'a::type => bool) xa::'a::type => bool.
+ (x = xa) = (SUBSET x xa & SUBSET xa x)"
by (import prob_extra SUBSET_EQ)
-lemma INTER_IS_EMPTY: "ALL s t. (pred_set.INTER s t = EMPTY) = (ALL x. ~ s x | ~ t x)"
+lemma INTER_IS_EMPTY: "ALL (s::'a::type => bool) t::'a::type => bool.
+ (pred_set.INTER s t = EMPTY) = (ALL x::'a::type. ~ s x | ~ t x)"
by (import prob_extra INTER_IS_EMPTY)
-lemma UNION_DISJOINT_SPLIT: "(All::(('a => bool) => bool) => bool)
- (%s::'a => bool.
- (All::(('a => bool) => bool) => bool)
- (%t::'a => bool.
- (All::(('a => bool) => bool) => bool)
- (%u::'a => bool.
+lemma UNION_DISJOINT_SPLIT: "(All::(('a::type => bool) => bool) => bool)
+ (%s::'a::type => bool.
+ (All::(('a::type => bool) => bool) => bool)
+ (%t::'a::type => bool.
+ (All::(('a::type => bool) => bool) => bool)
+ (%u::'a::type => bool.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((op =::('a => bool) => ('a => bool) => bool)
- ((pred_set.UNION::('a => bool)
-=> ('a => bool) => 'a => bool)
+ ((op =::('a::type => bool) => ('a::type => bool) => bool)
+ ((pred_set.UNION::('a::type => bool)
+=> ('a::type => bool) => 'a::type => bool)
s t)
- ((pred_set.UNION::('a => bool)
-=> ('a => bool) => 'a => bool)
+ ((pred_set.UNION::('a::type => bool)
+=> ('a::type => bool) => 'a::type => bool)
s u))
((op &::bool => bool => bool)
- ((op =::('a => bool) => ('a => bool) => bool)
- ((pred_set.INTER::('a => bool)
- => ('a => bool) => 'a => bool)
+ ((op =::('a::type => bool)
+ => ('a::type => bool) => bool)
+ ((pred_set.INTER::('a::type => bool)
+ => ('a::type => bool) => 'a::type => bool)
s t)
- (EMPTY::'a => bool))
- ((op =::('a => bool) => ('a => bool) => bool)
- ((pred_set.INTER::('a => bool)
- => ('a => bool) => 'a => bool)
+ (EMPTY::'a::type => bool))
+ ((op =::('a::type => bool)
+ => ('a::type => bool) => bool)
+ ((pred_set.INTER::('a::type => bool)
+ => ('a::type => bool) => 'a::type => bool)
s u)
- (EMPTY::'a => bool))))
- ((op =::('a => bool) => ('a => bool) => bool) t u))))"
+ (EMPTY::'a::type => bool))))
+ ((op =::('a::type => bool) => ('a::type => bool) => bool) t
+ u))))"
by (import prob_extra UNION_DISJOINT_SPLIT)
-lemma GSPEC_DEF_ALT: "ALL f. GSPEC f = (%v. EX x. (v, True) = f x)"
+lemma GSPEC_DEF_ALT: "ALL f::'a::type => 'b::type * bool.
+ GSPEC f = (%v::'b::type. EX x::'a::type. (v, True) = f x)"
by (import prob_extra GSPEC_DEF_ALT)
;end_setup
@@ -486,9 +515,12 @@
alg_twin :: "bool list => bool list => bool"
defs
- alg_twin_primdef: "alg_twin == %x y. EX l. x = SNOC True l & y = SNOC False l"
-
-lemma alg_twin_def: "ALL x y. alg_twin x y = (EX l. x = SNOC True l & y = SNOC False l)"
+ alg_twin_primdef: "alg_twin ==
+%(x::bool list) y::bool list.
+ EX l::bool list. x = SNOC True l & y = SNOC False l"
+
+lemma alg_twin_def: "ALL (x::bool list) y::bool list.
+ alg_twin x y = (EX l::bool list. x = SNOC True l & y = SNOC False l)"
by (import prob_canon alg_twin_def)
constdefs
@@ -618,9 +650,9 @@
alg_order :: "bool list => bool list => bool"
defs
- alg_order_primdef: "alg_order == %x x1. alg_order_tupled (x, x1)"
-
-lemma alg_order_curried_def: "ALL x x1. alg_order x x1 = alg_order_tupled (x, x1)"
+ alg_order_primdef: "alg_order == %(x::bool list) x1::bool list. alg_order_tupled (x, x1)"
+
+lemma alg_order_curried_def: "ALL (x::bool list) x1::bool list. alg_order x x1 = alg_order_tupled (x, x1)"
by (import prob_canon alg_order_curried_def)
lemma alg_order_ind: "(All::((bool list => bool list => bool) => bool) => bool)
@@ -658,10 +690,10 @@
(%x::bool list. (All::(bool list => bool) => bool) (P x))))"
by (import prob_canon alg_order_ind)
-lemma alg_order_def: "alg_order [] (v6 # v7) = True &
+lemma alg_order_def: "alg_order [] ((v6::bool) # (v7::bool list)) = True &
alg_order [] [] = True &
-alg_order (v2 # v3) [] = False &
-alg_order (h # t) (h' # t') =
+alg_order ((v2::bool) # (v3::bool list)) [] = False &
+alg_order ((h::bool) # (t::bool list)) ((h'::bool) # (t'::bool list)) =
(h = True & h' = False | h = h' & alg_order t t')"
by (import prob_canon alg_order_def)
@@ -670,18 +702,30 @@
defs
alg_sorted_primdef: "alg_sorted ==
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_sorted.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_sorted::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ alg_order v2 v6 & alg_sorted (v6 # v7))))"
lemma alg_sorted_primitive_def: "alg_sorted =
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_sorted.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_sorted::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ alg_order v2 v6 & alg_sorted (v6 # v7))))"
by (import prob_canon alg_sorted_primitive_def)
lemma alg_sorted_ind: "(All::((bool list list => bool) => bool) => bool)
@@ -712,8 +756,9 @@
((All::(bool list list => bool) => bool) P))"
by (import prob_canon alg_sorted_ind)
-lemma alg_sorted_def: "alg_sorted (x # y # z) = (alg_order x y & alg_sorted (y # z)) &
-alg_sorted [v] = True & alg_sorted [] = True"
+lemma alg_sorted_def: "alg_sorted ((x::bool list) # (y::bool list) # (z::bool list list)) =
+(alg_order x y & alg_sorted (y # z)) &
+alg_sorted [v::bool list] = True & alg_sorted [] = True"
by (import prob_canon alg_sorted_def)
consts
@@ -721,18 +766,30 @@
defs
alg_prefixfree_primdef: "alg_prefixfree ==
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_prefixfree.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_prefixfree::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
lemma alg_prefixfree_primitive_def: "alg_prefixfree =
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_prefixfree.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_prefixfree::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
by (import prob_canon alg_prefixfree_primitive_def)
lemma alg_prefixfree_ind: "(All::((bool list list => bool) => bool) => bool)
@@ -763,8 +820,9 @@
((All::(bool list list => bool) => bool) P))"
by (import prob_canon alg_prefixfree_ind)
-lemma alg_prefixfree_def: "alg_prefixfree (x # y # z) = (~ IS_PREFIX y x & alg_prefixfree (y # z)) &
-alg_prefixfree [v] = True & alg_prefixfree [] = True"
+lemma alg_prefixfree_def: "alg_prefixfree ((x::bool list) # (y::bool list) # (z::bool list list)) =
+(~ IS_PREFIX y x & alg_prefixfree (y # z)) &
+alg_prefixfree [v::bool list] = True & alg_prefixfree [] = True"
by (import prob_canon alg_prefixfree_def)
consts
@@ -772,18 +830,30 @@
defs
alg_twinfree_primdef: "alg_twinfree ==
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_twinfree.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_twinfree::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
lemma alg_twinfree_primitive_def: "alg_twinfree =
-WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
- (%alg_twinfree.
+WFREC
+ (SOME R::bool list list => bool list list => bool.
+ WF R &
+ (ALL (x::bool list) (z::bool list list) y::bool list.
+ R (y # z) (x # y # z)))
+ (%alg_twinfree::bool list list => bool.
list_case True
- (%v2. list_case True
- (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
+ (%v2::bool list.
+ list_case True
+ (%(v6::bool list) v7::bool list list.
+ ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
by (import prob_canon alg_twinfree_primitive_def)
lemma alg_twinfree_ind: "(All::((bool list list => bool) => bool) => bool)
@@ -814,24 +884,29 @@
((All::(bool list list => bool) => bool) P))"
by (import prob_canon alg_twinfree_ind)
-lemma alg_twinfree_def: "alg_twinfree (x # y # z) = (~ alg_twin x y & alg_twinfree (y # z)) &
-alg_twinfree [v] = True & alg_twinfree [] = True"
+lemma alg_twinfree_def: "alg_twinfree ((x::bool list) # (y::bool list) # (z::bool list list)) =
+(~ alg_twin x y & alg_twinfree (y # z)) &
+alg_twinfree [v::bool list] = True & alg_twinfree [] = True"
by (import prob_canon alg_twinfree_def)
consts
alg_longest :: "bool list list => nat"
defs
- alg_longest_primdef: "alg_longest == FOLDR (%h t. if t <= length h then length h else t) 0"
-
-lemma alg_longest_def: "alg_longest = FOLDR (%h t. if t <= length h then length h else t) 0"
+ alg_longest_primdef: "alg_longest ==
+FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t)
+ (0::nat)"
+
+lemma alg_longest_def: "alg_longest =
+FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t)
+ (0::nat)"
by (import prob_canon alg_longest_def)
consts
alg_canon_prefs :: "bool list => bool list list => bool list list"
-specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l. alg_canon_prefs l [] = [l]) &
-(ALL l h t.
+specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l::bool list. alg_canon_prefs l [] = [l]) &
+(ALL (l::bool list) (h::bool list) t::bool list list.
alg_canon_prefs l (h # t) =
(if IS_PREFIX h l then alg_canon_prefs l t else l # h # t))"
by (import prob_canon alg_canon_prefs_def)
@@ -839,8 +914,8 @@
consts
alg_canon_find :: "bool list => bool list list => bool list list"
-specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l. alg_canon_find l [] = [l]) &
-(ALL l h t.
+specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l::bool list. alg_canon_find l [] = [l]) &
+(ALL (l::bool list) (h::bool list) t::bool list list.
alg_canon_find l (h # t) =
(if alg_order h l
then if IS_PREFIX l h then h # t else h # alg_canon_find l t
@@ -859,8 +934,8 @@
consts
alg_canon_merge :: "bool list => bool list list => bool list list"
-specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l. alg_canon_merge l [] = [l]) &
-(ALL l h t.
+specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l::bool list. alg_canon_merge l [] = [l]) &
+(ALL (l::bool list) (h::bool list) t::bool list list.
alg_canon_merge l (h # t) =
(if alg_twin l h then alg_canon_merge (butlast h) t else l # h # t))"
by (import prob_canon alg_canon_merge_def)
@@ -878,34 +953,35 @@
alg_canon :: "bool list list => bool list list"
defs
- alg_canon_primdef: "alg_canon == %l. alg_canon2 (alg_canon1 l)"
-
-lemma alg_canon_def: "ALL l. alg_canon l = alg_canon2 (alg_canon1 l)"
+ alg_canon_primdef: "alg_canon == %l::bool list list. alg_canon2 (alg_canon1 l)"
+
+lemma alg_canon_def: "ALL l::bool list list. alg_canon l = alg_canon2 (alg_canon1 l)"
by (import prob_canon alg_canon_def)
consts
algebra_canon :: "bool list list => bool"
defs
- algebra_canon_primdef: "algebra_canon == %l. alg_canon l = l"
-
-lemma algebra_canon_def: "ALL l. algebra_canon l = (alg_canon l = l)"
+ algebra_canon_primdef: "algebra_canon == %l::bool list list. alg_canon l = l"
+
+lemma algebra_canon_def: "ALL l::bool list list. algebra_canon l = (alg_canon l = l)"
by (import prob_canon algebra_canon_def)
-lemma ALG_TWIN_NIL: "ALL l. ~ alg_twin l [] & ~ alg_twin [] l"
+lemma ALG_TWIN_NIL: "ALL l::bool list. ~ alg_twin l [] & ~ alg_twin [] l"
by (import prob_canon ALG_TWIN_NIL)
-lemma ALG_TWIN_SING: "ALL x l.
+lemma ALG_TWIN_SING: "ALL (x::bool) l::bool list.
alg_twin [x] l = (x = True & l = [False]) &
alg_twin l [x] = (l = [True] & x = False)"
by (import prob_canon ALG_TWIN_SING)
-lemma ALG_TWIN_CONS: "ALL x y z h t.
+lemma ALG_TWIN_CONS: "ALL (x::bool) (y::bool) (z::bool list) (h::bool) t::bool list.
alg_twin (x # y # z) (h # t) = (x = h & alg_twin (y # z) t) &
alg_twin (h # t) (x # y # z) = (x = h & alg_twin t (y # z))"
by (import prob_canon ALG_TWIN_CONS)
-lemma ALG_TWIN_REDUCE: "ALL h t t'. alg_twin (h # t) (h # t') = alg_twin t t'"
+lemma ALG_TWIN_REDUCE: "ALL (h::bool) (t::bool list) t'::bool list.
+ alg_twin (h # t) (h # t') = alg_twin t t'"
by (import prob_canon ALG_TWIN_REDUCE)
lemma ALG_TWINS_PREFIX: "(All::(bool list => bool) => bool)
@@ -924,10 +1000,10 @@
l))))))"
by (import prob_canon ALG_TWINS_PREFIX)
-lemma ALG_ORDER_NIL: "ALL x. alg_order [] x & alg_order x [] = (x = [])"
+lemma ALG_ORDER_NIL: "ALL x::bool list. alg_order [] x & alg_order x [] = (x = [])"
by (import prob_canon ALG_ORDER_NIL)
-lemma ALG_ORDER_REFL: "ALL x. alg_order x x"
+lemma ALG_ORDER_REFL: "ALL x::bool list. alg_order x x"
by (import prob_canon ALG_ORDER_REFL)
lemma ALG_ORDER_ANTISYM: "(All::(bool list => bool) => bool)
@@ -954,7 +1030,7 @@
((alg_order::bool list => bool list => bool) x z))))"
by (import prob_canon ALG_ORDER_TRANS)
-lemma ALG_ORDER_TOTAL: "ALL x y. alg_order x y | alg_order y x"
+lemma ALG_ORDER_TOTAL: "ALL (x::bool list) y::bool list. alg_order x y | alg_order y x"
by (import prob_canon ALG_ORDER_TOTAL)
lemma ALG_ORDER_PREFIX: "(All::(bool list => bool) => bool)
@@ -1007,7 +1083,7 @@
((IS_PREFIX::bool list => bool list => bool) x z)))))"
by (import prob_canon ALG_ORDER_PREFIX_TRANS)
-lemma ALG_ORDER_SNOC: "ALL x l. ~ alg_order (SNOC x l) l"
+lemma ALG_ORDER_SNOC: "ALL (x::bool) l::bool list. ~ alg_order (SNOC x l) l"
by (import prob_canon ALG_ORDER_SNOC)
lemma ALG_SORTED_MIN: "(All::(bool list => bool) => bool)
@@ -1066,15 +1142,15 @@
z)))))"
by (import prob_canon ALG_SORTED_MONO)
-lemma ALG_SORTED_TLS: "ALL l b. alg_sorted (map (op # b) l) = alg_sorted l"
+lemma ALG_SORTED_TLS: "ALL (l::bool list list) b::bool. alg_sorted (map (op # b) l) = alg_sorted l"
by (import prob_canon ALG_SORTED_TLS)
-lemma ALG_SORTED_STEP: "ALL l1 l2.
+lemma ALG_SORTED_STEP: "ALL (l1::bool list list) l2::bool list list.
alg_sorted (map (op # True) l1 @ map (op # False) l2) =
(alg_sorted l1 & alg_sorted l2)"
by (import prob_canon ALG_SORTED_STEP)
-lemma ALG_SORTED_APPEND: "ALL h h' t t'.
+lemma ALG_SORTED_APPEND: "ALL (h::bool list) (h'::bool list) (t::bool list list) t'::bool list list.
alg_sorted ((h # t) @ h' # t') =
(alg_sorted (h # t) & alg_sorted (h' # t') & alg_order (last (h # t)) h')"
by (import prob_canon ALG_SORTED_APPEND)
@@ -1144,15 +1220,16 @@
x)))))))"
by (import prob_canon ALG_PREFIXFREE_ELT)
-lemma ALG_PREFIXFREE_TLS: "ALL l b. alg_prefixfree (map (op # b) l) = alg_prefixfree l"
+lemma ALG_PREFIXFREE_TLS: "ALL (l::bool list list) b::bool.
+ alg_prefixfree (map (op # b) l) = alg_prefixfree l"
by (import prob_canon ALG_PREFIXFREE_TLS)
-lemma ALG_PREFIXFREE_STEP: "ALL l1 l2.
+lemma ALG_PREFIXFREE_STEP: "ALL (l1::bool list list) l2::bool list list.
alg_prefixfree (map (op # True) l1 @ map (op # False) l2) =
(alg_prefixfree l1 & alg_prefixfree l2)"
by (import prob_canon ALG_PREFIXFREE_STEP)
-lemma ALG_PREFIXFREE_APPEND: "ALL h h' t t'.
+lemma ALG_PREFIXFREE_APPEND: "ALL (h::bool list) (h'::bool list) (t::bool list list) t'::bool list list.
alg_prefixfree ((h # t) @ h' # t') =
(alg_prefixfree (h # t) &
alg_prefixfree (h' # t') & ~ IS_PREFIX h' (last (h # t)))"
@@ -1182,7 +1259,8 @@
((alg_twinfree::bool list list => bool) t)))"
by (import prob_canon ALG_TWINFREE_TL)
-lemma ALG_TWINFREE_TLS: "ALL l b. alg_twinfree (map (op # b) l) = alg_twinfree l"
+lemma ALG_TWINFREE_TLS: "ALL (l::bool list list) b::bool.
+ alg_twinfree (map (op # b) l) = alg_twinfree l"
by (import prob_canon ALG_TWINFREE_TLS)
lemma ALG_TWINFREE_STEP1: "(All::(bool list list => bool) => bool)
@@ -1258,21 +1336,22 @@
((alg_twinfree::bool list list => bool) l2)))))"
by (import prob_canon ALG_TWINFREE_STEP)
-lemma ALG_LONGEST_HD: "ALL h t. length h <= alg_longest (h # t)"
+lemma ALG_LONGEST_HD: "ALL (h::bool list) t::bool list list. length h <= alg_longest (h # t)"
by (import prob_canon ALG_LONGEST_HD)
-lemma ALG_LONGEST_TL: "ALL h t. alg_longest t <= alg_longest (h # t)"
+lemma ALG_LONGEST_TL: "ALL (h::bool list) t::bool list list. alg_longest t <= alg_longest (h # t)"
by (import prob_canon ALG_LONGEST_TL)
-lemma ALG_LONGEST_TLS: "ALL h t b. alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
+lemma ALG_LONGEST_TLS: "ALL (h::bool list) (t::bool list list) b::bool.
+ alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
by (import prob_canon ALG_LONGEST_TLS)
-lemma ALG_LONGEST_APPEND: "ALL l1 l2.
+lemma ALG_LONGEST_APPEND: "ALL (l1::bool list list) l2::bool list list.
alg_longest l1 <= alg_longest (l1 @ l2) &
alg_longest l2 <= alg_longest (l1 @ l2)"
by (import prob_canon ALG_LONGEST_APPEND)
-lemma ALG_CANON_PREFS_HD: "ALL l b. hd (alg_canon_prefs l b) = l"
+lemma ALG_CANON_PREFS_HD: "ALL (l::bool list) b::bool list list. hd (alg_canon_prefs l b) = l"
by (import prob_canon ALG_CANON_PREFS_HD)
lemma ALG_CANON_PREFS_DELETES: "(All::(bool list => bool) => bool)
@@ -1332,7 +1411,7 @@
((op #::bool list => bool list list => bool list list) l b))))"
by (import prob_canon ALG_CANON_PREFS_CONSTANT)
-lemma ALG_CANON_FIND_HD: "ALL l h t.
+lemma ALG_CANON_FIND_HD: "ALL (l::bool list) (h::bool list) t::bool list list.
hd (alg_canon_find l (h # t)) = l | hd (alg_canon_find l (h # t)) = h"
by (import prob_canon ALG_CANON_FIND_HD)
@@ -1395,10 +1474,10 @@
((op #::bool list => bool list list => bool list list) l b))))"
by (import prob_canon ALG_CANON_FIND_CONSTANT)
-lemma ALG_CANON1_SORTED: "ALL x. alg_sorted (alg_canon1 x)"
+lemma ALG_CANON1_SORTED: "ALL x::bool list list. alg_sorted (alg_canon1 x)"
by (import prob_canon ALG_CANON1_SORTED)
-lemma ALG_CANON1_PREFIXFREE: "ALL l. alg_prefixfree (alg_canon1 l)"
+lemma ALG_CANON1_PREFIXFREE: "ALL l::bool list list. alg_prefixfree (alg_canon1 l)"
by (import prob_canon ALG_CANON1_PREFIXFREE)
lemma ALG_CANON1_CONSTANT: "(All::(bool list list => bool) => bool)
@@ -1577,7 +1656,7 @@
((alg_canon2::bool list list => bool list list) l) l))"
by (import prob_canon ALG_CANON2_CONSTANT)
-lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l.
+lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l::bool list list.
alg_sorted (alg_canon l) &
alg_prefixfree (alg_canon l) & alg_twinfree (alg_canon l)"
by (import prob_canon ALG_CANON_SORTED_PREFIXFREE_TWINFREE)
@@ -1593,16 +1672,19 @@
((alg_canon::bool list list => bool list list) l) l))"
by (import prob_canon ALG_CANON_CONSTANT)
-lemma ALG_CANON_IDEMPOT: "ALL l. alg_canon (alg_canon l) = alg_canon l"
+lemma ALG_CANON_IDEMPOT: "ALL l::bool list list. alg_canon (alg_canon l) = alg_canon l"
by (import prob_canon ALG_CANON_IDEMPOT)
-lemma ALGEBRA_CANON_DEF_ALT: "ALL l. algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
+lemma ALGEBRA_CANON_DEF_ALT: "ALL l::bool list list.
+ algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
by (import prob_canon ALGEBRA_CANON_DEF_ALT)
-lemma ALGEBRA_CANON_BASIC: "algebra_canon [] & algebra_canon [[]] & (ALL x. algebra_canon [x])"
+lemma ALGEBRA_CANON_BASIC: "algebra_canon [] &
+algebra_canon [[]] & (ALL x::bool list. algebra_canon [x])"
by (import prob_canon ALGEBRA_CANON_BASIC)
-lemma ALG_CANON_BASIC: "alg_canon [] = [] & alg_canon [[]] = [[]] & (ALL x. alg_canon [x] = [x])"
+lemma ALG_CANON_BASIC: "alg_canon [] = [] &
+alg_canon [[]] = [[]] & (ALL x::bool list. alg_canon [x] = [x])"
by (import prob_canon ALG_CANON_BASIC)
lemma ALGEBRA_CANON_TL: "(All::(bool list => bool) => bool)
@@ -1615,10 +1697,11 @@
((algebra_canon::bool list list => bool) t)))"
by (import prob_canon ALGEBRA_CANON_TL)
-lemma ALGEBRA_CANON_NIL_MEM: "ALL l. (algebra_canon l & [] mem l) = (l = [[]])"
+lemma ALGEBRA_CANON_NIL_MEM: "ALL l::bool list list. (algebra_canon l & [] mem l) = (l = [[]])"
by (import prob_canon ALGEBRA_CANON_NIL_MEM)
-lemma ALGEBRA_CANON_TLS: "ALL l b. algebra_canon (map (op # b) l) = algebra_canon l"
+lemma ALGEBRA_CANON_TLS: "ALL (l::bool list list) b::bool.
+ algebra_canon (map (op # b) l) = algebra_canon l"
by (import prob_canon ALGEBRA_CANON_TLS)
lemma ALGEBRA_CANON_STEP1: "(All::(bool list list => bool) => bool)
@@ -1828,10 +1911,12 @@
((algebra_canon::bool list list => bool) l) (P l))))"
by (import prob_canon ALGEBRA_CANON_INDUCTION)
-lemma MEM_NIL_STEP: "ALL l1 l2. ~ [] mem map (op # True) l1 @ map (op # False) l2"
+lemma MEM_NIL_STEP: "ALL (l1::bool list list) l2::bool list list.
+ ~ [] mem map (op # True) l1 @ map (op # False) l2"
by (import prob_canon MEM_NIL_STEP)
-lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l. (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
+lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l::bool list list.
+ (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
by (import prob_canon ALG_SORTED_PREFIXFREE_MEM_NIL)
lemma ALG_SORTED_PREFIXFREE_EQUALITY: "(All::(bool list list => bool) => bool)
@@ -1863,33 +1948,34 @@
SHD :: "(nat => bool) => bool"
defs
- SHD_primdef: "SHD == %f. f 0"
-
-lemma SHD_def: "ALL f. SHD f = f 0"
+ SHD_primdef: "SHD == %f::nat => bool. f (0::nat)"
+
+lemma SHD_def: "ALL f::nat => bool. SHD f = f (0::nat)"
by (import boolean_sequence SHD_def)
consts
STL :: "(nat => bool) => nat => bool"
defs
- STL_primdef: "STL == %f n. f (Suc n)"
-
-lemma STL_def: "ALL f n. STL f n = f (Suc n)"
+ STL_primdef: "STL == %(f::nat => bool) n::nat. f (Suc n)"
+
+lemma STL_def: "ALL (f::nat => bool) n::nat. STL f n = f (Suc n)"
by (import boolean_sequence STL_def)
consts
SCONS :: "bool => (nat => bool) => nat => bool"
-specification (SCONS_primdef: SCONS) SCONS_def: "(ALL h t. SCONS h t 0 = h) & (ALL h t n. SCONS h t (Suc n) = t n)"
+specification (SCONS_primdef: SCONS) SCONS_def: "(ALL (h::bool) t::nat => bool. SCONS h t (0::nat) = h) &
+(ALL (h::bool) (t::nat => bool) n::nat. SCONS h t (Suc n) = t n)"
by (import boolean_sequence SCONS_def)
consts
SDEST :: "(nat => bool) => bool * (nat => bool)"
defs
- SDEST_primdef: "SDEST == %s. (SHD s, STL s)"
-
-lemma SDEST_def: "SDEST = (%s. (SHD s, STL s))"
+ SDEST_primdef: "SDEST == %s::nat => bool. (SHD s, STL s)"
+
+lemma SDEST_def: "SDEST = (%s::nat => bool. (SHD s, STL s))"
by (import boolean_sequence SDEST_def)
consts
@@ -1904,32 +1990,32 @@
consts
STAKE :: "nat => (nat => bool) => bool list"
-specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s. STAKE 0 s = []) &
-(ALL n s. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
+specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s::nat => bool. STAKE (0::nat) s = []) &
+(ALL (n::nat) s::nat => bool. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
by (import boolean_sequence STAKE_def)
consts
SDROP :: "nat => (nat => bool) => nat => bool"
-specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n. SDROP (Suc n) = SDROP n o STL)"
+specification (SDROP_primdef: SDROP) SDROP_def: "SDROP (0::nat) = I & (ALL n::nat. SDROP (Suc n) = SDROP n o STL)"
by (import boolean_sequence SDROP_def)
-lemma SCONS_SURJ: "ALL x. EX xa t. x = SCONS xa t"
+lemma SCONS_SURJ: "ALL x::nat => bool. EX (xa::bool) t::nat => bool. x = SCONS xa t"
by (import boolean_sequence SCONS_SURJ)
-lemma SHD_STL_ISO: "ALL h t. EX x. SHD x = h & STL x = t"
+lemma SHD_STL_ISO: "ALL (h::bool) t::nat => bool. EX x::nat => bool. SHD x = h & STL x = t"
by (import boolean_sequence SHD_STL_ISO)
-lemma SHD_SCONS: "ALL h t. SHD (SCONS h t) = h"
+lemma SHD_SCONS: "ALL (h::bool) t::nat => bool. SHD (SCONS h t) = h"
by (import boolean_sequence SHD_SCONS)
-lemma STL_SCONS: "ALL h t. STL (SCONS h t) = t"
+lemma STL_SCONS: "ALL (h::bool) t::nat => bool. STL (SCONS h t) = t"
by (import boolean_sequence STL_SCONS)
-lemma SHD_SCONST: "ALL b. SHD (SCONST b) = b"
+lemma SHD_SCONST: "ALL b::bool. SHD (SCONST b) = b"
by (import boolean_sequence SHD_SCONST)
-lemma STL_SCONST: "ALL b. STL (SCONST b) = SCONST b"
+lemma STL_SCONST: "ALL b::bool. STL (SCONST b) = SCONST b"
by (import boolean_sequence STL_SCONST)
;end_setup
@@ -1939,15 +2025,16 @@
consts
alg_embed :: "bool list => (nat => bool) => bool"
-specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s. alg_embed [] s = True) &
-(ALL h t s. alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
+specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s::nat => bool. alg_embed [] s = True) &
+(ALL (h::bool) (t::bool list) s::nat => bool.
+ alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
by (import prob_algebra alg_embed_def)
consts
algebra_embed :: "bool list list => (nat => bool) => bool"
specification (algebra_embed_primdef: algebra_embed) algebra_embed_def: "algebra_embed [] = EMPTY &
-(ALL h t.
+(ALL (h::bool list) t::bool list list.
algebra_embed (h # t) = pred_set.UNION (alg_embed h) (algebra_embed t))"
by (import prob_algebra algebra_embed_def)
@@ -1955,29 +2042,36 @@
measurable :: "((nat => bool) => bool) => bool"
defs
- measurable_primdef: "measurable == %s. EX b. s = algebra_embed b"
-
-lemma measurable_def: "ALL s. measurable s = (EX b. s = algebra_embed b)"
+ measurable_primdef: "measurable ==
+%s::(nat => bool) => bool. EX b::bool list list. s = algebra_embed b"
+
+lemma measurable_def: "ALL s::(nat => bool) => bool.
+ measurable s = (EX b::bool list list. s = algebra_embed b)"
by (import prob_algebra measurable_def)
-lemma HALVES_INTER: "pred_set.INTER (%x. SHD x = True) (%x. SHD x = False) = EMPTY"
+lemma HALVES_INTER: "pred_set.INTER (%x::nat => bool. SHD x = True)
+ (%x::nat => bool. SHD x = False) =
+EMPTY"
by (import prob_algebra HALVES_INTER)
-lemma INTER_STL: "ALL p q. pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
+lemma INTER_STL: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
+ pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
by (import prob_algebra INTER_STL)
-lemma COMPL_SHD: "ALL b. COMPL (%x. SHD x = b) = (%x. SHD x = (~ b))"
+lemma COMPL_SHD: "ALL b::bool.
+ COMPL (%x::nat => bool. SHD x = b) = (%x::nat => bool. SHD x = (~ b))"
by (import prob_algebra COMPL_SHD)
lemma ALG_EMBED_BASIC: "alg_embed [] = pred_set.UNIV &
-(ALL h t.
- alg_embed (h # t) = pred_set.INTER (%x. SHD x = h) (alg_embed t o STL))"
+(ALL (h::bool) t::bool list.
+ alg_embed (h # t) =
+ pred_set.INTER (%x::nat => bool. SHD x = h) (alg_embed t o STL))"
by (import prob_algebra ALG_EMBED_BASIC)
-lemma ALG_EMBED_NIL: "ALL c. All (alg_embed c) = (c = [])"
+lemma ALG_EMBED_NIL: "ALL c::bool list. All (alg_embed c) = (c = [])"
by (import prob_algebra ALG_EMBED_NIL)
-lemma ALG_EMBED_POPULATED: "ALL b. Ex (alg_embed b)"
+lemma ALG_EMBED_POPULATED: "ALL b::bool list. Ex (alg_embed b)"
by (import prob_algebra ALG_EMBED_POPULATED)
lemma ALG_EMBED_PREFIX: "(All::(bool list => bool) => bool)
@@ -1995,17 +2089,18 @@
((IS_PREFIX::bool list => bool list => bool) c b)))))"
by (import prob_algebra ALG_EMBED_PREFIX)
-lemma ALG_EMBED_PREFIX_SUBSET: "ALL b c. SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
+lemma ALG_EMBED_PREFIX_SUBSET: "ALL (b::bool list) c::bool list.
+ SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
by (import prob_algebra ALG_EMBED_PREFIX_SUBSET)
-lemma ALG_EMBED_TWINS: "ALL l.
+lemma ALG_EMBED_TWINS: "ALL l::bool list.
pred_set.UNION (alg_embed (SNOC True l)) (alg_embed (SNOC False l)) =
alg_embed l"
by (import prob_algebra ALG_EMBED_TWINS)
lemma ALGEBRA_EMBED_BASIC: "algebra_embed [] = EMPTY &
algebra_embed [[]] = pred_set.UNIV &
-(ALL b. algebra_embed [[b]] = (%s. SHD s = b))"
+(ALL b::bool. algebra_embed [[b]] = (%s::nat => bool. SHD s = b))"
by (import prob_algebra ALGEBRA_EMBED_BASIC)
lemma ALGEBRA_EMBED_MEM: "(All::(bool list list => bool) => bool)
@@ -2021,31 +2116,35 @@
((alg_embed::bool list => (nat => bool) => bool) l x)))))"
by (import prob_algebra ALGEBRA_EMBED_MEM)
-lemma ALGEBRA_EMBED_APPEND: "ALL l1 l2.
+lemma ALGEBRA_EMBED_APPEND: "ALL (l1::bool list list) l2::bool list list.
algebra_embed (l1 @ l2) =
pred_set.UNION (algebra_embed l1) (algebra_embed l2)"
by (import prob_algebra ALGEBRA_EMBED_APPEND)
-lemma ALGEBRA_EMBED_TLS: "ALL l b.
- algebra_embed (map (op # b) l) (SCONS h t) = (h = b & algebra_embed l t)"
+lemma ALGEBRA_EMBED_TLS: "ALL (l::bool list list) b::bool.
+ algebra_embed (map (op # b) l) (SCONS (h::bool) (t::nat => bool)) =
+ (h = b & algebra_embed l t)"
by (import prob_algebra ALGEBRA_EMBED_TLS)
-lemma ALG_CANON_PREFS_EMBED: "ALL l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
+lemma ALG_CANON_PREFS_EMBED: "ALL (l::bool list) b::bool list list.
+ algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
by (import prob_algebra ALG_CANON_PREFS_EMBED)
-lemma ALG_CANON_FIND_EMBED: "ALL l b. algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
+lemma ALG_CANON_FIND_EMBED: "ALL (l::bool list) b::bool list list.
+ algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
by (import prob_algebra ALG_CANON_FIND_EMBED)
-lemma ALG_CANON1_EMBED: "ALL x. algebra_embed (alg_canon1 x) = algebra_embed x"
+lemma ALG_CANON1_EMBED: "ALL x::bool list list. algebra_embed (alg_canon1 x) = algebra_embed x"
by (import prob_algebra ALG_CANON1_EMBED)
-lemma ALG_CANON_MERGE_EMBED: "ALL l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
+lemma ALG_CANON_MERGE_EMBED: "ALL (l::bool list) b::bool list list.
+ algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
by (import prob_algebra ALG_CANON_MERGE_EMBED)
-lemma ALG_CANON2_EMBED: "ALL x. algebra_embed (alg_canon2 x) = algebra_embed x"
+lemma ALG_CANON2_EMBED: "ALL x::bool list list. algebra_embed (alg_canon2 x) = algebra_embed x"
by (import prob_algebra ALG_CANON2_EMBED)
-lemma ALG_CANON_EMBED: "ALL l. algebra_embed (alg_canon l) = algebra_embed l"
+lemma ALG_CANON_EMBED: "ALL l::bool list list. algebra_embed (alg_canon l) = algebra_embed l"
by (import prob_algebra ALG_CANON_EMBED)
lemma ALGEBRA_CANON_UNIV: "(All::(bool list list => bool) => bool)
@@ -2061,7 +2160,8 @@
([]::bool list) ([]::bool list list)))))"
by (import prob_algebra ALGEBRA_CANON_UNIV)
-lemma ALG_CANON_REP: "ALL b c. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
+lemma ALG_CANON_REP: "ALL (b::bool list list) c::bool list list.
+ (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
by (import prob_algebra ALG_CANON_REP)
lemma ALGEBRA_CANON_EMBED_EMPTY: "(All::(bool list list => bool) => bool)
@@ -2090,20 +2190,22 @@
([]::bool list) ([]::bool list list)))))"
by (import prob_algebra ALGEBRA_CANON_EMBED_UNIV)
-lemma MEASURABLE_ALGEBRA: "ALL b. measurable (algebra_embed b)"
+lemma MEASURABLE_ALGEBRA: "ALL b::bool list list. measurable (algebra_embed b)"
by (import prob_algebra MEASURABLE_ALGEBRA)
lemma MEASURABLE_BASIC: "measurable EMPTY &
-measurable pred_set.UNIV & (ALL b. measurable (%s. SHD s = b))"
+measurable pred_set.UNIV &
+(ALL b::bool. measurable (%s::nat => bool. SHD s = b))"
by (import prob_algebra MEASURABLE_BASIC)
-lemma MEASURABLE_SHD: "ALL b. measurable (%s. SHD s = b)"
+lemma MEASURABLE_SHD: "ALL b::bool. measurable (%s::nat => bool. SHD s = b)"
by (import prob_algebra MEASURABLE_SHD)
-lemma ALGEBRA_EMBED_COMPL: "ALL l. EX l'. COMPL (algebra_embed l) = algebra_embed l'"
+lemma ALGEBRA_EMBED_COMPL: "ALL l::bool list list.
+ EX l'::bool list list. COMPL (algebra_embed l) = algebra_embed l'"
by (import prob_algebra ALGEBRA_EMBED_COMPL)
-lemma MEASURABLE_COMPL: "ALL s. measurable (COMPL s) = measurable s"
+lemma MEASURABLE_COMPL: "ALL s::(nat => bool) => bool. measurable (COMPL s) = measurable s"
by (import prob_algebra MEASURABLE_COMPL)
lemma MEASURABLE_UNION: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2136,28 +2238,30 @@
s t))))"
by (import prob_algebra MEASURABLE_INTER)
-lemma MEASURABLE_STL: "ALL p. measurable (p o STL) = measurable p"
+lemma MEASURABLE_STL: "ALL p::(nat => bool) => bool. measurable (p o STL) = measurable p"
by (import prob_algebra MEASURABLE_STL)
-lemma MEASURABLE_SDROP: "ALL n p. measurable (p o SDROP n) = measurable p"
+lemma MEASURABLE_SDROP: "ALL (n::nat) p::(nat => bool) => bool.
+ measurable (p o SDROP n) = measurable p"
by (import prob_algebra MEASURABLE_SDROP)
-lemma MEASURABLE_INTER_HALVES: "ALL p.
- (measurable (pred_set.INTER (%x. SHD x = True) p) &
- measurable (pred_set.INTER (%x. SHD x = False) p)) =
+lemma MEASURABLE_INTER_HALVES: "ALL p::(nat => bool) => bool.
+ (measurable (pred_set.INTER (%x::nat => bool. SHD x = True) p) &
+ measurable (pred_set.INTER (%x::nat => bool. SHD x = False) p)) =
measurable p"
by (import prob_algebra MEASURABLE_INTER_HALVES)
-lemma MEASURABLE_HALVES: "ALL p q.
+lemma MEASURABLE_HALVES: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
measurable
- (pred_set.UNION (pred_set.INTER (%x. SHD x = True) p)
- (pred_set.INTER (%x. SHD x = False) q)) =
- (measurable (pred_set.INTER (%x. SHD x = True) p) &
- measurable (pred_set.INTER (%x. SHD x = False) q))"
+ (pred_set.UNION (pred_set.INTER (%x::nat => bool. SHD x = True) p)
+ (pred_set.INTER (%x::nat => bool. SHD x = False) q)) =
+ (measurable (pred_set.INTER (%x::nat => bool. SHD x = True) p) &
+ measurable (pred_set.INTER (%x::nat => bool. SHD x = False) q))"
by (import prob_algebra MEASURABLE_HALVES)
-lemma MEASURABLE_INTER_SHD: "ALL b p.
- measurable (pred_set.INTER (%x. SHD x = b) (p o STL)) = measurable p"
+lemma MEASURABLE_INTER_SHD: "ALL (b::bool) p::(nat => bool) => bool.
+ measurable (pred_set.INTER (%x::nat => bool. SHD x = b) (p o STL)) =
+ measurable p"
by (import prob_algebra MEASURABLE_INTER_SHD)
;end_setup
@@ -2167,8 +2271,10 @@
consts
alg_measure :: "bool list list => real"
-specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
-(ALL l rest. alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
+specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = (0::real) &
+(ALL (l::bool list) rest::bool list list.
+ alg_measure (l # rest) =
+ ((1::real) / (2::real)) ^ length l + alg_measure rest)"
by (import prob alg_measure_def)
consts
@@ -2176,11 +2282,16 @@
defs
algebra_measure_primdef: "algebra_measure ==
-%b. inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
-
-lemma algebra_measure_def: "ALL b.
+%b::bool list list.
+ inf (%r::real.
+ EX c::bool list list.
+ algebra_embed b = algebra_embed c & alg_measure c = r)"
+
+lemma algebra_measure_def: "ALL b::bool list list.
algebra_measure b =
- inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
+ inf (%r::real.
+ EX c::bool list list.
+ algebra_embed b = algebra_embed c & alg_measure c = r)"
by (import prob algebra_measure_def)
consts
@@ -2188,11 +2299,16 @@
defs
prob_primdef: "prob ==
-%s. sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
-
-lemma prob_def: "ALL s.
+%s::(nat => bool) => bool.
+ sup (%r::real.
+ EX b::bool list list.
+ algebra_measure b = r & SUBSET (algebra_embed b) s)"
+
+lemma prob_def: "ALL s::(nat => bool) => bool.
prob s =
- sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
+ sup (%r::real.
+ EX b::bool list list.
+ algebra_measure b = r & SUBSET (algebra_embed b) s)"
by (import prob prob_def)
lemma ALG_TWINS_MEASURE: "ALL l::bool list.
@@ -2201,42 +2317,49 @@
((1::real) / (2::real)) ^ length l"
by (import prob ALG_TWINS_MEASURE)
-lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
-alg_measure [[]] = 1 & (ALL b. alg_measure [[b]] = 1 / 2)"
+lemma ALG_MEASURE_BASIC: "alg_measure [] = (0::real) &
+alg_measure [[]] = (1::real) &
+(ALL b::bool. alg_measure [[b]] = (1::real) / (2::real))"
by (import prob ALG_MEASURE_BASIC)
-lemma ALG_MEASURE_POS: "ALL l. 0 <= alg_measure l"
+lemma ALG_MEASURE_POS: "ALL l::bool list list. (0::real) <= alg_measure l"
by (import prob ALG_MEASURE_POS)
-lemma ALG_MEASURE_APPEND: "ALL l1 l2. alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
+lemma ALG_MEASURE_APPEND: "ALL (l1::bool list list) l2::bool list list.
+ alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
by (import prob ALG_MEASURE_APPEND)
-lemma ALG_MEASURE_TLS: "ALL l b. 2 * alg_measure (map (op # b) l) = alg_measure l"
+lemma ALG_MEASURE_TLS: "ALL (l::bool list list) b::bool.
+ (2::real) * alg_measure (map (op # b) l) = alg_measure l"
by (import prob ALG_MEASURE_TLS)
-lemma ALG_CANON_PREFS_MONO: "ALL l b. alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
+lemma ALG_CANON_PREFS_MONO: "ALL (l::bool list) b::bool list list.
+ alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
by (import prob ALG_CANON_PREFS_MONO)
-lemma ALG_CANON_FIND_MONO: "ALL l b. alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
+lemma ALG_CANON_FIND_MONO: "ALL (l::bool list) b::bool list list.
+ alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
by (import prob ALG_CANON_FIND_MONO)
-lemma ALG_CANON1_MONO: "ALL x. alg_measure (alg_canon1 x) <= alg_measure x"
+lemma ALG_CANON1_MONO: "ALL x::bool list list. alg_measure (alg_canon1 x) <= alg_measure x"
by (import prob ALG_CANON1_MONO)
-lemma ALG_CANON_MERGE_MONO: "ALL l b. alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
+lemma ALG_CANON_MERGE_MONO: "ALL (l::bool list) b::bool list list.
+ alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
by (import prob ALG_CANON_MERGE_MONO)
-lemma ALG_CANON2_MONO: "ALL x. alg_measure (alg_canon2 x) <= alg_measure x"
+lemma ALG_CANON2_MONO: "ALL x::bool list list. alg_measure (alg_canon2 x) <= alg_measure x"
by (import prob ALG_CANON2_MONO)
-lemma ALG_CANON_MONO: "ALL l. alg_measure (alg_canon l) <= alg_measure l"
+lemma ALG_CANON_MONO: "ALL l::bool list list. alg_measure (alg_canon l) <= alg_measure l"
by (import prob ALG_CANON_MONO)
-lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l. algebra_measure l = alg_measure (alg_canon l)"
+lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l::bool list list. algebra_measure l = alg_measure (alg_canon l)"
by (import prob ALGEBRA_MEASURE_DEF_ALT)
-lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
-algebra_measure [[]] = 1 & (ALL b. algebra_measure [[b]] = 1 / 2)"
+lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = (0::real) &
+algebra_measure [[]] = (1::real) &
+(ALL b::bool. algebra_measure [[b]] = (1::real) / (2::real))"
by (import prob ALGEBRA_MEASURE_BASIC)
lemma ALGEBRA_CANON_MEASURE_MAX: "(All::(bool list list => bool) => bool)
@@ -2247,7 +2370,7 @@
((alg_measure::bool list list => real) l) (1::real)))"
by (import prob ALGEBRA_CANON_MEASURE_MAX)
-lemma ALGEBRA_MEASURE_MAX: "ALL l. algebra_measure l <= 1"
+lemma ALGEBRA_MEASURE_MAX: "ALL l::bool list list. algebra_measure l <= (1::real)"
by (import prob ALGEBRA_MEASURE_MAX)
lemma ALGEBRA_MEASURE_MONO_EMBED: "(All::(bool list list => bool) => bool)
@@ -2332,11 +2455,12 @@
((alg_measure::bool list list => real) d)))))))))"
by (import prob ALG_MEASURE_ADDITIVE)
-lemma PROB_ALGEBRA: "ALL l. prob (algebra_embed l) = algebra_measure l"
+lemma PROB_ALGEBRA: "ALL l::bool list list. prob (algebra_embed l) = algebra_measure l"
by (import prob PROB_ALGEBRA)
-lemma PROB_BASIC: "prob EMPTY = 0 &
-prob pred_set.UNIV = 1 & (ALL b. prob (%s. SHD s = b) = 1 / 2)"
+lemma PROB_BASIC: "prob EMPTY = (0::real) &
+prob pred_set.UNIV = (1::real) &
+(ALL b::bool. prob (%s::nat => bool. SHD s = b) = (1::real) / (2::real))"
by (import prob PROB_BASIC)
lemma PROB_ADDITIVE: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2377,7 +2501,9 @@
((prob::((nat => bool) => bool) => real) s))))"
by (import prob PROB_COMPL)
-lemma PROB_SUP_EXISTS1: "ALL s. EX x b. algebra_measure b = x & SUBSET (algebra_embed b) s"
+lemma PROB_SUP_EXISTS1: "ALL s::(nat => bool) => bool.
+ EX (x::real) b::bool list list.
+ algebra_measure b = x & SUBSET (algebra_embed b) s"
by (import prob PROB_SUP_EXISTS1)
lemma PROB_SUP_EXISTS2: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2452,7 +2578,7 @@
((prob::((nat => bool) => bool) => real) t))))"
by (import prob PROB_SUBSET_MONO)
-lemma PROB_ALG: "ALL x. prob (alg_embed x) = (1 / 2) ^ length x"
+lemma PROB_ALG: "ALL x::bool list. prob (alg_embed x) = ((1::real) / (2::real)) ^ length x"
by (import prob PROB_ALG)
lemma PROB_STL: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2536,25 +2662,26 @@
((prob::((nat => bool) => bool) => real) p)))))"
by (import prob PROB_INTER_SHD)
-lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l"
+lemma ALGEBRA_MEASURE_POS: "ALL l::bool list list. (0::real) <= algebra_measure l"
by (import prob ALGEBRA_MEASURE_POS)
-lemma ALGEBRA_MEASURE_RANGE: "ALL l. 0 <= algebra_measure l & algebra_measure l <= 1"
+lemma ALGEBRA_MEASURE_RANGE: "ALL l::bool list list.
+ (0::real) <= algebra_measure l & algebra_measure l <= (1::real)"
by (import prob ALGEBRA_MEASURE_RANGE)
-lemma PROB_POS: "ALL p. 0 <= prob p"
+lemma PROB_POS: "ALL p::(nat => bool) => bool. (0::real) <= prob p"
by (import prob PROB_POS)
-lemma PROB_MAX: "ALL p. prob p <= 1"
+lemma PROB_MAX: "ALL p::(nat => bool) => bool. prob p <= (1::real)"
by (import prob PROB_MAX)
-lemma PROB_RANGE: "ALL p. 0 <= prob p & prob p <= 1"
+lemma PROB_RANGE: "ALL p::(nat => bool) => bool. (0::real) <= prob p & prob p <= (1::real)"
by (import prob PROB_RANGE)
-lemma ABS_PROB: "ALL p. abs (prob p) = prob p"
+lemma ABS_PROB: "ALL p::(nat => bool) => bool. abs (prob p) = prob p"
by (import prob ABS_PROB)
-lemma PROB_SHD: "ALL b. prob (%s. SHD s = b) = 1 / 2"
+lemma PROB_SHD: "ALL b::bool. prob (%s::nat => bool. SHD s = b) = (1::real) / (2::real)"
by (import prob PROB_SHD)
lemma PROB_COMPL_LE1: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2591,41 +2718,42 @@
pseudo_linear_tl :: "nat => nat => nat => nat => nat"
defs
- pseudo_linear_tl_primdef: "pseudo_linear_tl == %a b n x. (a * x + b) mod (2 * n + 1)"
-
-lemma pseudo_linear_tl_def: "ALL a b n x. pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
+ pseudo_linear_tl_primdef: "pseudo_linear_tl ==
+%(a::nat) (b::nat) (n::nat) x::nat.
+ (a * x + b) mod ((2::nat) * n + (1::nat))"
+
+lemma pseudo_linear_tl_def: "ALL (a::nat) (b::nat) (n::nat) x::nat.
+ pseudo_linear_tl a b n x = (a * x + b) mod ((2::nat) * n + (1::nat))"
by (import prob_pseudo pseudo_linear_tl_def)
-lemma PSEUDO_LINEAR1_EXECUTE: "EX x. (ALL xa. SHD (x xa) = pseudo_linear_hd xa) &
- (ALL xa.
- STL (x xa) =
- x (pseudo_linear_tl
- (NUMERAL
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT2
- (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
- (NUMERAL
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
- (NUMERAL
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT1
- (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
- xa))"
+lemma PSEUDO_LINEAR1_EXECUTE: "EX x::nat => nat => bool.
+ (ALL xa::nat. SHD (x xa) = pseudo_linear_hd xa) &
+ (ALL xa::nat.
+ STL (x xa) =
+ x (pseudo_linear_tl
+ (NUMERAL
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
+ (NUMERAL
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
+ (NUMERAL
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1
+ (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
+ xa))"
by (import prob_pseudo PSEUDO_LINEAR1_EXECUTE)
consts
pseudo_linear1 :: "nat => nat => bool"
-specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
-(ALL x.
+specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x::nat. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
+(ALL x::nat.
STL (pseudo_linear1 x) =
pseudo_linear1
(pseudo_linear_tl
@@ -2665,10 +2793,10 @@
defs
indep_set_primdef: "indep_set ==
-%p q. measurable p &
- measurable q & prob (pred_set.INTER p q) = prob p * prob q"
-
-lemma indep_set_def: "ALL p q.
+%(p::(nat => bool) => bool) q::(nat => bool) => bool.
+ measurable p & measurable q & prob (pred_set.INTER p q) = prob p * prob q"
+
+lemma indep_set_def: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
indep_set p q =
(measurable p &
measurable q & prob (pred_set.INTER p q) = prob p * prob q)"
@@ -2679,9 +2807,10 @@
defs
alg_cover_set_primdef: "alg_cover_set ==
-%l. alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
-
-lemma alg_cover_set_def: "ALL l.
+%l::bool list list.
+ alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
+
+lemma alg_cover_set_def: "ALL l::bool list list.
alg_cover_set l =
(alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV)"
by (import prob_indep alg_cover_set_def)
@@ -2690,25 +2819,33 @@
alg_cover :: "bool list list => (nat => bool) => bool list"
defs
- alg_cover_primdef: "alg_cover == %l x. SOME b. b mem l & alg_embed b x"
-
-lemma alg_cover_def: "ALL l x. alg_cover l x = (SOME b. b mem l & alg_embed b x)"
+ alg_cover_primdef: "alg_cover ==
+%(l::bool list list) x::nat => bool.
+ SOME b::bool list. b mem l & alg_embed b x"
+
+lemma alg_cover_def: "ALL (l::bool list list) x::nat => bool.
+ alg_cover l x = (SOME b::bool list. b mem l & alg_embed b x)"
by (import prob_indep alg_cover_def)
consts
- indep :: "((nat => bool) => 'a * (nat => bool)) => bool"
+ indep :: "((nat => bool) => 'a::type * (nat => bool)) => bool"
defs
indep_primdef: "indep ==
-%f. EX l r.
+%f::(nat => bool) => 'a::type * (nat => bool).
+ EX (l::bool list list) r::bool list => 'a::type.
+ alg_cover_set l &
+ (ALL s::nat => bool.
+ f s =
+ (let c::bool list = alg_cover l s in (r c, SDROP (length c) s)))"
+
+lemma indep_def: "ALL f::(nat => bool) => 'a::type * (nat => bool).
+ indep f =
+ (EX (l::bool list list) r::bool list => 'a::type.
alg_cover_set l &
- (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s)))"
-
-lemma indep_def: "ALL f.
- indep f =
- (EX l r.
- alg_cover_set l &
- (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s))))"
+ (ALL s::nat => bool.
+ f s =
+ (let c::bool list = alg_cover l s in (r c, SDROP (length c) s))))"
by (import prob_indep indep_def)
lemma INDEP_SET_BASIC: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2724,7 +2861,8 @@
(pred_set.UNIV::(nat => bool) => bool) p)))"
by (import prob_indep INDEP_SET_BASIC)
-lemma INDEP_SET_SYM: "ALL p q. indep_set p q = indep_set p q"
+lemma INDEP_SET_SYM: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
+ indep_set p q = indep_set p q"
by (import prob_indep INDEP_SET_SYM)
lemma INDEP_SET_DISJOINT_DECOMP: "(All::(((nat => bool) => bool) => bool) => bool)
@@ -2809,10 +2947,10 @@
l))))"
by (import prob_indep MAP_CONS_TL_FILTER)
-lemma ALG_COVER_SET_CASES_THM: "ALL l.
+lemma ALG_COVER_SET_CASES_THM: "ALL l::bool list list.
alg_cover_set l =
(l = [[]] |
- (EX x xa.
+ (EX (x::bool list list) xa::bool list list.
alg_cover_set x &
alg_cover_set xa & l = map (op # True) x @ map (op # False) xa))"
by (import prob_indep ALG_COVER_SET_CASES_THM)
@@ -3191,144 +3329,162 @@
q)))"
by (import prob_indep INDEP_SET_LIST)
-lemma INDEP_INDEP_SET: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::(nat => bool) => 'a * (nat => bool).
- (All::(('a => bool) => bool) => bool)
- (%p::'a => bool.
+lemma INDEP_INDEP_SET: "(All::(((nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::(nat => bool) => 'a::type * (nat => bool).
+ (All::(('a::type => bool) => bool) => bool)
+ (%p::'a::type => bool.
(All::(((nat => bool) => bool) => bool) => bool)
(%q::(nat => bool) => bool.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
+ ((indep::((nat => bool) => 'a::type * (nat => bool))
+ => bool)
+ f)
((measurable::((nat => bool) => bool) => bool) q))
((indep_set::((nat => bool) => bool)
=> ((nat => bool) => bool) => bool)
- ((op o::('a => bool)
- => ((nat => bool) => 'a) => (nat => bool) => bool)
- p ((op o::('a * (nat => bool) => 'a)
- => ((nat => bool) => 'a * (nat => bool))
- => (nat => bool) => 'a)
- (fst::'a * (nat => bool) => 'a) f))
+ ((op o::('a::type => bool)
+ => ((nat => bool) => 'a::type)
+ => (nat => bool) => bool)
+ p ((op o::('a::type * (nat => bool) => 'a::type)
+ => ((nat => bool) => 'a::type * (nat => bool))
+ => (nat => bool) => 'a::type)
+ (fst::'a::type * (nat => bool) => 'a::type) f))
((op o::((nat => bool) => bool)
=> ((nat => bool) => nat => bool)
=> (nat => bool) => bool)
- q ((op o::('a * (nat => bool) => nat => bool)
- => ((nat => bool) => 'a * (nat => bool))
+ q ((op o::('a::type * (nat => bool) => nat => bool)
+ => ((nat => bool) => 'a::type * (nat => bool))
=> (nat => bool) => nat => bool)
- (snd::'a * (nat => bool) => nat => bool) f))))))"
+ (snd::'a::type * (nat => bool) => nat => bool)
+ f))))))"
by (import prob_indep INDEP_INDEP_SET)
-lemma INDEP_UNIT: "ALL x. indep (UNIT x)"
+lemma INDEP_UNIT: "ALL x::'a::type. indep (UNIT x)"
by (import prob_indep INDEP_UNIT)
lemma INDEP_SDEST: "indep SDEST"
by (import prob_indep INDEP_SDEST)
-lemma BIND_STEP: "ALL f. BIND SDEST (%k. f o SCONS k) = f"
+lemma BIND_STEP: "ALL f::(nat => bool) => 'a::type * (nat => bool).
+ BIND SDEST (%k::bool. f o SCONS k) = f"
by (import prob_indep BIND_STEP)
-lemma INDEP_BIND_SDEST: "(All::((bool => (nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::bool => (nat => bool) => 'a * (nat => bool).
+lemma INDEP_BIND_SDEST: "(All::((bool => (nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::bool => (nat => bool) => 'a::type * (nat => bool).
(op -->::bool => bool => bool)
((All::(bool => bool) => bool)
(%x::bool.
- (indep::((nat => bool) => 'a * (nat => bool)) => bool) (f x)))
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool)
+ (indep::((nat => bool) => 'a::type * (nat => bool)) => bool)
+ (f x)))
+ ((indep::((nat => bool) => 'a::type * (nat => bool)) => bool)
((BIND::((nat => bool) => bool * (nat => bool))
- => (bool => (nat => bool) => 'a * (nat => bool))
- => (nat => bool) => 'a * (nat => bool))
+ => (bool => (nat => bool) => 'a::type * (nat => bool))
+ => (nat => bool) => 'a::type * (nat => bool))
(SDEST::(nat => bool) => bool * (nat => bool)) f)))"
by (import prob_indep INDEP_BIND_SDEST)
-lemma INDEP_BIND: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::(nat => bool) => 'a * (nat => bool).
- (All::(('a => (nat => bool) => 'b * (nat => bool)) => bool) => bool)
- (%g::'a => (nat => bool) => 'b * (nat => bool).
+lemma INDEP_BIND: "(All::(((nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::(nat => bool) => 'a::type * (nat => bool).
+ (All::(('a::type => (nat => bool) => 'b::type * (nat => bool)) => bool)
+ => bool)
+ (%g::'a::type => (nat => bool) => 'b::type * (nat => bool).
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
- ((All::('a => bool) => bool)
- (%x::'a.
- (indep::((nat => bool) => 'b * (nat => bool)) => bool)
+ ((indep::((nat => bool) => 'a::type * (nat => bool)) => bool)
+ f)
+ ((All::('a::type => bool) => bool)
+ (%x::'a::type.
+ (indep::((nat => bool) => 'b::type * (nat => bool))
+ => bool)
(g x))))
- ((indep::((nat => bool) => 'b * (nat => bool)) => bool)
- ((BIND::((nat => bool) => 'a * (nat => bool))
- => ('a => (nat => bool) => 'b * (nat => bool))
- => (nat => bool) => 'b * (nat => bool))
+ ((indep::((nat => bool) => 'b::type * (nat => bool)) => bool)
+ ((BIND::((nat => bool) => 'a::type * (nat => bool))
+ => ('a::type
+ => (nat => bool) => 'b::type * (nat => bool))
+ => (nat => bool) => 'b::type * (nat => bool))
f g))))"
by (import prob_indep INDEP_BIND)
-lemma INDEP_PROB: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::(nat => bool) => 'a * (nat => bool).
- (All::(('a => bool) => bool) => bool)
- (%p::'a => bool.
+lemma INDEP_PROB: "(All::(((nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::(nat => bool) => 'a::type * (nat => bool).
+ (All::(('a::type => bool) => bool) => bool)
+ (%p::'a::type => bool.
(All::(((nat => bool) => bool) => bool) => bool)
(%q::(nat => bool) => bool.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
+ ((indep::((nat => bool) => 'a::type * (nat => bool))
+ => bool)
+ f)
((measurable::((nat => bool) => bool) => bool) q))
((op =::real => real => bool)
((prob::((nat => bool) => bool) => real)
((pred_set.INTER::((nat => bool) => bool)
=> ((nat => bool) => bool) => (nat => bool) => bool)
- ((op o::('a => bool)
- => ((nat => bool) => 'a)
+ ((op o::('a::type => bool)
+ => ((nat => bool) => 'a::type)
=> (nat => bool) => bool)
- p ((op o::('a * (nat => bool) => 'a)
- => ((nat => bool) => 'a * (nat => bool))
- => (nat => bool) => 'a)
- (fst::'a * (nat => bool) => 'a) f))
+ p ((op o::('a::type * (nat => bool) => 'a::type)
+ => ((nat => bool)
+=> 'a::type * (nat => bool))
+ => (nat => bool) => 'a::type)
+ (fst::'a::type * (nat => bool) => 'a::type) f))
((op o::((nat => bool) => bool)
=> ((nat => bool) => nat => bool)
=> (nat => bool) => bool)
- q ((op o::('a * (nat => bool) => nat => bool)
- => ((nat => bool) => 'a * (nat => bool))
+ q ((op o::('a::type * (nat => bool) => nat => bool)
+ => ((nat => bool)
+=> 'a::type * (nat => bool))
=> (nat => bool) => nat => bool)
- (snd::'a * (nat => bool) => nat => bool) f))))
+ (snd::'a::type * (nat => bool) => nat => bool)
+ f))))
((op *::real => real => real)
((prob::((nat => bool) => bool) => real)
- ((op o::('a => bool)
- => ((nat => bool) => 'a)
+ ((op o::('a::type => bool)
+ => ((nat => bool) => 'a::type)
=> (nat => bool) => bool)
- p ((op o::('a * (nat => bool) => 'a)
- => ((nat => bool) => 'a * (nat => bool))
- => (nat => bool) => 'a)
- (fst::'a * (nat => bool) => 'a) f)))
+ p ((op o::('a::type * (nat => bool) => 'a::type)
+ => ((nat => bool)
+=> 'a::type * (nat => bool))
+ => (nat => bool) => 'a::type)
+ (fst::'a::type * (nat => bool) => 'a::type) f)))
((prob::((nat => bool) => bool) => real) q))))))"
by (import prob_indep INDEP_PROB)
-lemma INDEP_MEASURABLE1: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::(nat => bool) => 'a * (nat => bool).
- (All::(('a => bool) => bool) => bool)
- (%p::'a => bool.
+lemma INDEP_MEASURABLE1: "(All::(((nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::(nat => bool) => 'a::type * (nat => bool).
+ (All::(('a::type => bool) => bool) => bool)
+ (%p::'a::type => bool.
(op -->::bool => bool => bool)
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
+ ((indep::((nat => bool) => 'a::type * (nat => bool)) => bool) f)
((measurable::((nat => bool) => bool) => bool)
- ((op o::('a => bool)
- => ((nat => bool) => 'a) => (nat => bool) => bool)
- p ((op o::('a * (nat => bool) => 'a)
- => ((nat => bool) => 'a * (nat => bool))
- => (nat => bool) => 'a)
- (fst::'a * (nat => bool) => 'a) f)))))"
+ ((op o::('a::type => bool)
+ => ((nat => bool) => 'a::type)
+ => (nat => bool) => bool)
+ p ((op o::('a::type * (nat => bool) => 'a::type)
+ => ((nat => bool) => 'a::type * (nat => bool))
+ => (nat => bool) => 'a::type)
+ (fst::'a::type * (nat => bool) => 'a::type) f)))))"
by (import prob_indep INDEP_MEASURABLE1)
-lemma INDEP_MEASURABLE2: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
- (%f::(nat => bool) => 'a * (nat => bool).
+lemma INDEP_MEASURABLE2: "(All::(((nat => bool) => 'a::type * (nat => bool)) => bool) => bool)
+ (%f::(nat => bool) => 'a::type * (nat => bool).
(All::(((nat => bool) => bool) => bool) => bool)
(%q::(nat => bool) => bool.
(op -->::bool => bool => bool)
((op &::bool => bool => bool)
- ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
+ ((indep::((nat => bool) => 'a::type * (nat => bool)) => bool)
+ f)
((measurable::((nat => bool) => bool) => bool) q))
((measurable::((nat => bool) => bool) => bool)
((op o::((nat => bool) => bool)
=> ((nat => bool) => nat => bool)
=> (nat => bool) => bool)
- q ((op o::('a * (nat => bool) => nat => bool)
- => ((nat => bool) => 'a * (nat => bool))
+ q ((op o::('a::type * (nat => bool) => nat => bool)
+ => ((nat => bool) => 'a::type * (nat => bool))
=> (nat => bool) => nat => bool)
- (snd::'a * (nat => bool) => nat => bool) f)))))"
+ (snd::'a::type * (nat => bool) => nat => bool) f)))))"
by (import prob_indep INDEP_MEASURABLE2)
lemma PROB_INDEP_BOUND: "(All::(((nat => bool) => nat * (nat => bool)) => bool) => bool)
@@ -3363,15 +3519,22 @@
defs
unif_bound_primdef: "unif_bound ==
-WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
- (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
+WFREC
+ (SOME R::nat => nat => bool.
+ WF R & (ALL v::nat. R (Suc v div (2::nat)) (Suc v)))
+ (%unif_bound::nat => nat.
+ nat_case (0::nat) (%v1::nat. Suc (unif_bound (Suc v1 div (2::nat)))))"
lemma unif_bound_primitive_def: "unif_bound =
-WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
- (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
+WFREC
+ (SOME R::nat => nat => bool.
+ WF R & (ALL v::nat. R (Suc v div (2::nat)) (Suc v)))
+ (%unif_bound::nat => nat.
+ nat_case (0::nat) (%v1::nat. Suc (unif_bound (Suc v1 div (2::nat)))))"
by (import prob_uniform unif_bound_primitive_def)
-lemma unif_bound_def: "unif_bound 0 = 0 & unif_bound (Suc v) = Suc (unif_bound (Suc v div 2))"
+lemma unif_bound_def: "unif_bound (0::nat) = (0::nat) &
+unif_bound (Suc (v::nat)) = Suc (unif_bound (Suc v div (2::nat)))"
by (import prob_uniform unif_bound_def)
lemma unif_bound_ind: "(All::((nat => bool) => bool) => bool)
@@ -3394,35 +3557,47 @@
constdefs
unif_tupled :: "nat * (nat => bool) => nat * (nat => bool)"
"unif_tupled ==
-WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
- (%unif_tupled (v, v1).
- case v of 0 => (0, v1)
- | Suc v3 =>
- let (m, s') = unif_tupled (Suc v3 div 2, v1)
- in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
+WFREC
+ (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
+ WF R &
+ (ALL (s::nat => bool) v2::nat. R (Suc v2 div (2::nat), s) (Suc v2, s)))
+ (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
+ v1::nat => bool).
+ case v of 0 => (0::nat, v1)
+ | Suc (v3::nat) =>
+ let (m::nat, s'::nat => bool) =
+ unif_tupled (Suc v3 div (2::nat), v1)
+ in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m,
+ STL s'))"
lemma unif_tupled_primitive_def: "unif_tupled =
-WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
- (%unif_tupled (v, v1).
- case v of 0 => (0, v1)
- | Suc v3 =>
- let (m, s') = unif_tupled (Suc v3 div 2, v1)
- in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
+WFREC
+ (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
+ WF R &
+ (ALL (s::nat => bool) v2::nat. R (Suc v2 div (2::nat), s) (Suc v2, s)))
+ (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
+ v1::nat => bool).
+ case v of 0 => (0::nat, v1)
+ | Suc (v3::nat) =>
+ let (m::nat, s'::nat => bool) =
+ unif_tupled (Suc v3 div (2::nat), v1)
+ in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m,
+ STL s'))"
by (import prob_uniform unif_tupled_primitive_def)
consts
unif :: "nat => (nat => bool) => nat * (nat => bool)"
defs
- unif_primdef: "unif == %x x1. unif_tupled (x, x1)"
-
-lemma unif_curried_def: "ALL x x1. unif x x1 = unif_tupled (x, x1)"
+ unif_primdef: "unif == %(x::nat) x1::nat => bool. unif_tupled (x, x1)"
+
+lemma unif_curried_def: "ALL (x::nat) x1::nat => bool. unif x x1 = unif_tupled (x, x1)"
by (import prob_uniform unif_curried_def)
-lemma unif_def: "unif 0 s = (0, s) &
-unif (Suc v2) s =
-(let (m, s') = unif (Suc v2 div 2) s
- in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
+lemma unif_def: "unif (0::nat) (s::nat => bool) = (0::nat, s) &
+unif (Suc (v2::nat)) s =
+(let (m::nat, s'::nat => bool) = unif (Suc v2 div (2::nat)) s
+ in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m, STL s'))"
by (import prob_uniform unif_def)
lemma unif_ind: "(All::((nat => (nat => bool) => bool) => bool) => bool)
@@ -3648,9 +3823,10 @@
uniform :: "nat => nat => (nat => bool) => nat * (nat => bool)"
defs
- uniform_primdef: "uniform == %x x1 x2. uniform_tupled (x, x1, x2)"
-
-lemma uniform_curried_def: "ALL x x1 x2. uniform x x1 x2 = uniform_tupled (x, x1, x2)"
+ uniform_primdef: "uniform == %(x::nat) (x1::nat) x2::nat => bool. uniform_tupled (x, x1, x2)"
+
+lemma uniform_curried_def: "ALL (x::nat) (x1::nat) x2::nat => bool.
+ uniform x x1 x2 = uniform_tupled (x, x1, x2)"
by (import prob_uniform uniform_curried_def)
lemma uniform_ind: "(All::((nat => nat => (nat => bool) => bool) => bool) => bool)
@@ -3695,19 +3871,19 @@
(%xa::nat. (All::((nat => bool) => bool) => bool) (P x xa)))))"
by (import prob_uniform uniform_ind)
-lemma uniform_def: "uniform 0 (Suc n) s = (0, s) &
-uniform (Suc t) (Suc n) s =
-(let (xa, x) = unif n s
+lemma uniform_def: "uniform (0::nat) (Suc (n::nat)) (s::nat => bool) = (0::nat, s) &
+uniform (Suc (t::nat)) (Suc n) s =
+(let (xa::nat, x::nat => bool) = unif n s
in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
by (import prob_uniform uniform_def)
-lemma SUC_DIV_TWO_ZERO: "ALL n. (Suc n div 2 = 0) = (n = 0)"
+lemma SUC_DIV_TWO_ZERO: "ALL n::nat. (Suc n div (2::nat) = (0::nat)) = (n = (0::nat))"
by (import prob_uniform SUC_DIV_TWO_ZERO)
-lemma UNIF_BOUND_LOWER: "ALL n. n < 2 ^ unif_bound n"
+lemma UNIF_BOUND_LOWER: "ALL n::nat. n < (2::nat) ^ unif_bound n"
by (import prob_uniform UNIF_BOUND_LOWER)
-lemma UNIF_BOUND_LOWER_SUC: "ALL n. Suc n <= 2 ^ unif_bound n"
+lemma UNIF_BOUND_LOWER_SUC: "ALL n::nat. Suc n <= (2::nat) ^ unif_bound n"
by (import prob_uniform UNIF_BOUND_LOWER_SUC)
lemma UNIF_BOUND_UPPER: "(All::(nat => bool) => bool)
@@ -3729,39 +3905,71 @@
n)))"
by (import prob_uniform UNIF_BOUND_UPPER)
-lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)"
+lemma UNIF_BOUND_UPPER_SUC: "ALL n::nat. (2::nat) ^ unif_bound n <= Suc ((2::nat) * n)"
by (import prob_uniform UNIF_BOUND_UPPER_SUC)
-lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
-(ALL n.
+lemma UNIF_DEF_MONAD: "unif (0::nat) = UNIT (0::nat) &
+(ALL n::nat.
unif (Suc n) =
- BIND (unif (Suc n div 2))
- (%m. BIND SDEST (%b. UNIT (if b then 2 * m + 1 else 2 * m))))"
+ BIND (unif (Suc n div (2::nat)))
+ (%m::nat.
+ BIND SDEST
+ (%b::bool.
+ UNIT (if b then (2::nat) * m + (1::nat) else (2::nat) * m))))"
by (import prob_uniform UNIF_DEF_MONAD)
-lemma UNIFORM_DEF_MONAD: "(ALL x. uniform 0 (Suc x) = UNIT 0) &
-(ALL x xa.
+lemma UNIFORM_DEF_MONAD: "(ALL x::nat. uniform (0::nat) (Suc x) = UNIT (0::nat)) &
+(ALL (x::nat) xa::nat.
uniform (Suc x) (Suc xa) =
- BIND (unif xa) (%m. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
+ BIND (unif xa)
+ (%m::nat. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
by (import prob_uniform UNIFORM_DEF_MONAD)
-lemma INDEP_UNIF: "ALL n. indep (unif n)"
+lemma INDEP_UNIF: "ALL n::nat. indep (unif n)"
by (import prob_uniform INDEP_UNIF)
-lemma INDEP_UNIFORM: "ALL t n. indep (uniform t (Suc n))"
+lemma INDEP_UNIFORM: "ALL (t::nat) n::nat. indep (uniform t (Suc n))"
by (import prob_uniform INDEP_UNIFORM)
-lemma PROB_UNIF: "ALL n k.
- prob (%s. fst (unif n s) = k) =
- (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
+lemma PROB_UNIF: "(All::(nat => bool) => bool)
+ (%n::nat.
+ (All::(nat => bool) => bool)
+ (%k::nat.
+ (op =::real => real => bool)
+ ((prob::((nat => bool) => bool) => real)
+ (%s::nat => bool.
+ (op =::nat => nat => bool)
+ ((fst::nat * (nat => bool) => nat)
+ ((unif::nat => (nat => bool) => nat * (nat => bool)) n
+ s))
+ k))
+ ((If::bool => real => real => real)
+ ((op <::nat => nat => bool) k
+ ((op ^::nat => nat => nat)
+ ((number_of::bin => nat)
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit)))
+ ((unif_bound::nat => nat) n)))
+ ((op ^::real => nat => real)
+ ((op /::real => real => real) (1::real)
+ ((number_of::bin => real)
+ ((op BIT::bin => bit => bin)
+ ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
+ (bit.B1::bit))
+ (bit.B0::bit))))
+ ((unif_bound::nat => nat) n))
+ (0::real))))"
by (import prob_uniform PROB_UNIF)
-lemma UNIF_RANGE: "ALL n s. fst (unif n s) < 2 ^ unif_bound n"
+lemma UNIF_RANGE: "ALL (n::nat) s::nat => bool. fst (unif n s) < (2::nat) ^ unif_bound n"
by (import prob_uniform UNIF_RANGE)
-lemma PROB_UNIF_PAIR: "ALL n k k'.
- (prob (%s. fst (unif n s) = k) = prob (%s. fst (unif n s) = k')) =
- ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
+lemma PROB_UNIF_PAIR: "ALL (n::nat) (k::nat) k'::nat.
+ (prob (%s::nat => bool. fst (unif n s) = k) =
+ prob (%s::nat => bool. fst (unif n s) = k')) =
+ ((k < (2::nat) ^ unif_bound n) = (k' < (2::nat) ^ unif_bound n))"
by (import prob_uniform PROB_UNIF_PAIR)
lemma PROB_UNIF_BOUND: "(All::(nat => bool) => bool)
@@ -3796,10 +4004,11 @@
((unif_bound::nat => nat) n))))))"
by (import prob_uniform PROB_UNIF_BOUND)
-lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)"
+lemma PROB_UNIF_GOOD: "ALL n::nat.
+ (1::real) / (2::real) <= prob (%s::nat => bool. fst (unif n s) < Suc n)"
by (import prob_uniform PROB_UNIF_GOOD)
-lemma UNIFORM_RANGE: "ALL t n s. fst (uniform t (Suc n) s) < Suc n"
+lemma UNIFORM_RANGE: "ALL (t::nat) (n::nat) s::nat => bool. fst (uniform t (Suc n) s) < Suc n"
by (import prob_uniform UNIFORM_RANGE)
lemma PROB_UNIFORM_LOWER_BOUND: "(All::(real => bool) => bool)